Saverio Giallorenzo
email: saverio.giallorenzo@gmail.com

Ivan Lanese
email: ivan.lanese@gmail.com

Fabrizio Montesi
email: fmontesi@imada.sdu.dk

Davide Sangiorgi
email: davide.sangiorgi@unibo.it

Stefano Pio Zingaro
email: stefanopio.zingaro@unibo.it

Stefano Pio

The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service

Keywords: 2012 ACM Subject Classification Computer systems organization → Cloud computing; Theory of computation → Concurrency Serverless computing, Process calculi, Pi-calculus Digital Object Identifier 10.4230/OASIcs.Gabbrielli.2020.5

Serverless computing is a paradigm for programming cloud applications in terms of stateless functions, executed and scaled in proportion to inbound requests. Here, we revisit SKC, a calculus capturing the essential features of serverless programming. By exploring the design space of the language, we refined the integration between the fundamental features of the two calculi that inspire SKC: the λ-and the π-calculus. That investigation led us to a revised syntax and semantics, which support an increase in the expressiveness of the language. In particular, now function names are first-class citizens and can be passed around. To illustrate the new features, we present step-by-step examples and two non-trivial use cases from artificial intelligence, which model, respectively, a perceptron and an image tagging system into compositions of serverless functions. We also illustrate how SKC supports reasoning on serverless implementations, i.e., the underlying network of communicating, concurrent, and mobile processes which execute serverless functions in the cloud. To that aim, we show an encoding from SKC to the asynchronous π-calculus and prove it correct in terms of an operational correspondence.

Introduction

Background

Serverless computing, or Functions as a Service (FaaS), is a recent paradigm for programming cloud applications [START_REF] Baldini | Serverless computing: Current trends and open problems[END_REF]. Programmers code applications in terms of functions. Function definitions can be stored inside of dedicated repositories, and their execution can be triggered by events. An underlying cloud framework is responsible for executing functions whenever triggered, by utilising efficiently a pool of servers. Asynchronous interaction is prominent in this setting, since a function might trigger the execution of another function on another server, and then fetch the result later on to perform further computation.

A framework for serverless computing consists of two layers: a language layer, which programmers use to code their applications in terms of (asynchronous) functions; and an implementation layer, which executes applications written in the language layer by leveraging a distributed system (the cloud). One can see the first layer as the frontend for developers, and the second layer as the backend that makes serverless systems tick.

Both the language and implementation layers of serverless are complex. Different vendors implement them in different ways with different limitations, in particular regarding how programs can be composed and reasoned about [START_REF] Baldini | Serverless computing: Current trends and open problems[END_REF][START_REF] Jonas | Cloud programming simplified: A Berkeley view on serverless computing[END_REF][START_REF] Hellerstein | Serverless computing: One step forward, two steps back[END_REF]. This motivated recent studies on formal "core" languages for serverless computing, which aim at providing solid foundations for developing and reasoning on serverless systems [START_REF] Gabbrielli | No more, no less -A formal model for serverless computing[END_REF][START_REF] Jangda | Formal foundations of serverless computing[END_REF]. We call such core languages serverless calculi.

Serverless calculi are based on the λ-calculus: the language layer of serverless frameworks deals with functions, and the λ-calculus is the undisputed reference model for functional programming. The Serverless Kernel Calculus (SKC, or "sketch") is a concurrent λ-calculus enriched with asynchronous function evaluation, futures, and a stateful function repository [START_REF] Gabbrielli | No more, no less -A formal model for serverless computing[END_REF]. SKC leverages the call-by-value evaluation strategy for the λ-calculus to provide a uniform treatment of substitutions for both local and remote serverless computations: evaluating a function synchronously or asynchronously leads to the same substitution carrying the result to the caller.

Motivation

Our work originates from two main motivations.

The first motivation regards the design of the language layer. Both calculi from [START_REF] Gabbrielli | No more, no less -A formal model for serverless computing[END_REF][START_REF] Jangda | Formal foundations of serverless computing[END_REF] enhance the λ-calculus with features from process calculi to represent concurrent execution of functions. However, some of these features are slightly different and sometimes more limited. For example, the calculus in [START_REF] Jangda | Formal foundations of serverless computing[END_REF] uses a "fresh name" condition to transfer the result of function evaluations instead of an explicit operator for name scoping, like name restriction in the π-calculus [START_REF] Milner | A calculus of mobile processes[END_REF]. SKC adopts a restriction operator to create private names of futures, which are used for the same purpose. Yet, it does not support the creation of new function names that can be stored in the shared function repository, so it is not possible to create private function definitions or private stored data. Furthermore, the expressiveness of SKC is only briefly discussed in [START_REF] Gabbrielli | No more, no less -A formal model for serverless computing[END_REF].

Our second motivation regards the implementation layer. Implementing a serverless framework requires dealing with communication and mobility, in the sense that the connections among the underlying cloud servers and the concurrent processes that run within them change at runtime. The reference theory for mobile processes is the π-calculus, but to the best of our knowledge there is still no exploration of how serverless calculi can be formally linked to it.

This article

In this article, we revisit the theory of SKC and provide a more extensive presentation of its features.

Our new version of SKC (Section 2) provides a few improvements, which are given by a better integration of the essential features of the λ-calculus and the π-calculus. Specifically, functions can now be parametric on the names of other functions available in a serverless system, whereas before all references to functions in the repository were statically fixed; it is now possible to create new function names for the repository dynamically, so the repository of available functions can now grow freely at runtime. These new features enhance the expressiveness of the language, which we illustrate through small examples (Section 2) and two use cases (Section 3) from artificial intelligence, one implementing the perceptron algorithm and one for distributed tagging of large images.

We present two semantic interpretations for our version of SKC. The first (Section 2) is a refinement of the original reduction semantics from [START_REF] Gabbrielli | No more, no less -A formal model for serverless computing[END_REF], which supports the aforementioned improvements. This high-level semantics is intended for developers to reason abstractly about SKC programs. The second semantic interpretation is a formalisation of a possible implementation layer for SKC, given in terms of an encoding (Section 5) from SKC to the asynchronous π-calculus [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF] (recalled in Section 4). The encoding is inspired by Milner's encoding of the call-by-value λ-calculus [START_REF] Milner | Functions as processes[END_REF]. It shows how serverless functions can be implemented by servers (replicated processes in the π-calculus) that can be triggered by messages from clients, and how a serverless implementation layer can be modelled in terms of communications among processes. We prove that the encoding is correct in terms of an operational correspondence result.

Our results show that standard techniques from process calculi can be useful to understand the two layers of serverless calculi. Hopefully, this understanding could also provide foundations for tackling some outstanding questions in serverless computing. For example, predicting resource usage and costs is challenging in general, since it requires knowing how functions are executed by the implementation layer.

2

The Serverless Kernel Calculus, Revised

We now present our refined version of the Serverless Kernel Calculus (SKC).

Configurations C

::= S, D | νn C Definition repository D ::= {(f 1 , M 1 ), . . . , (f k , M k )} (k ≥ 0) Systems S, S ::= c M | S | S | νn S | 0 Functions M, N ::= M N | V | call h | store h N M | take h | νf M | async M | c Values V, V ::= x | λx. M | f Restrictable names n ::= c | f h ::= f | x Function names f ∈ Fun Future names c ∈ Fut Variables x ∈ Var Figure 1 Syntax of SKC.

Gabbrielli's Festschrift

5:4

A Formal Revisitation of Functions as a Service

Syntax

The syntax of SKC terms is given in Figure 1, and described in the following. We assume three disjoint enumerable sets of names: function names, ranged over by f ; future names, ranged over by c; and the usual variables of λ-calculus, ranged over by x.

Configurations and definition repositories

A configuration C represents a running serverless architecture. In a configuration of the form S, D : S is a system composed of functions that are currently being evaluated; and D is a repository of function definitions that can be triggered (and updated) at runtime.

We treat definition repositories D as partial maps from function names (ranged over by f ) to function bodies (ranged over by M ). Thus, for example, the writings D(f ) = M and (f, M ) ∈ D are equivalent. Definition repositories are mutable: their content can change at runtime, as we are going to see when we discuss the syntax of functions.

The configuration term νn C restricts the scope of a name n to C, binding n in C. A restrictable name n can be either a function name f or a future name c.

Systems

A system S is a composition of functions that are being evaluated in parallel.

Term c M represents a function under evaluation, whose result will be made available under the future name c upon termination.

Systems of running functions can be composed in parallel, written S | S . Term 0 is the unit of parallel composition.

Names of futures and functions can be restricted in systems as well, using the term νn S.

The restriction operator ν binds stronger than the parallel operator |. Thus, for example, νn S | S is interpreted as (νn S) | S .

Functions

The language of functions includes the usual terms of λ-calculus: the variable term x, the application term M N , and the abstraction term λx. M . We distinguish the syntactic category of values (V ) to make the presentation of our call-by-value semantics easier later on.

We extend the usual syntax of functions with terms for using the definition repository and futures.

A function f in the definition repository can be invoked by term call f , which abstractly represents the "triggering" of a function in the definition repository by an event. The syntax is actually more general: in term call h, h can be either a function name or a variable. This enables abstracting over function names, as in λx. call x. Passing a function name as an argument is enabled since term f is a value.

The primitives store and take manipulate the definition repository. Specifically, term store h N M updates the definition repository with the mapping (h, N )h is now mapped to N -and then proceeds by evaluating M . Dually, term take h removes the function with name h from the definition repository and then proceeds as its body. For example, assuming that the definition repository contains a mapping (f, M ), then take f would erase that mapping and proceed as M .

We allow for function names to be restricted, written νf M , which allows for the definition of functions in the repository that have "private names".

Moving to futures, term async M starts the asynchronous execution of M . The idea is that M is going to run in parallel, and that this execution is going to be connected to the original term async M through a fresh future name that is created automatically. For example, a system running c async M would reduce to νc (c c | c M ). Term c represents a function waiting for a future to be resolved: it will be replaced with the result of the parallel running function c M once M produces a value that can be returned. Note that futures c are not values, hence they cannot be, e.g., passed to functions. One may increase flexibility e.g., by "thunking" futures such that async M becomes the value λx. c instead of the non-value c. We leave the exploration of this direction for future work.

Equality and substitution

The ν and λ operators bind names, giving rise to the expected notions of free names (fn(-)) and bound names (bn(-)). Names (n(-)) are the union of free and bound names. Thus, we obtain the usual notions of α-equivalence, written = α , and capture-avoiding substitution for functions, written M {V /x} (read "V replaces x in M ").

In the remainder, we equate α-equivalent systems, and the same for functions. Consistently with viewing definition repositories as maps, equality of definition repositories allows for swap -the order in which definitions are given inside of D does not matter. This is equivalent to extensional equality over finite maps: D = D if and only if D and D have the same domain of definition F ⊂ Fun and D(f ) = D (f ) for all f ∈ F .

Semantics

We present now the semantics of SKC, given in terms of structural equivalence of terms and a reduction relation that captures term dynamics.

Both structural equivalence and the reduction relation make use of the auxiliary definition of evaluation contexts, given in Figure 2. An evaluation context E is a running function with a hole [•] that can be replaced with a function term M . We write E[M ] for the term obtained by replacing the hole in E with M .

E ::= c E λ E λ ::= [•] | λx. M E λ | E λ M Figure 2 SKC, evaluation contexts.

Structural equivalence

Terms in SKC give rise to the expected equivalences regarding name scoping and parallel composition. This is formalised by the structural equivalence ≡ between terms, which is the smallest congruence on SKC terms satisfying the rules in Figure 3.

These rules are straightforward adaptations of the typical rules for scoping and the parallel operator found in process calculi. The first row of rules axiomatise that parallel composition (|) behaves as a commutative monoid with 0 as identity element. The second row deals with extrusion of function names in evaluation contexts. The third row contains rules for garbage collection of restrictions, swapping of restrictions, and name extrusion in systems and configurations.

5:6

A Formal Revisitation of Functions as a Service

S | S ≡ S | S S | (S | S ) ≡ (S | S ) | S S | 0 ≡ S f / ∈ fn(E) νf E[M ] ≡ E[νf M ] f / ∈ fn(E λ ) νf E λ [M ] ≡ E λ [νf M ] νn 0 ≡ 0 νn νn S ≡ νn νn S n / ∈ fn(S ) νn (S | S ) ≡ νn S | S n / ∈ fn(D) νn S, D ≡ νn S, D Figure 3 SKC, rules for structural congruence. E[(λx. M ) V ], D --→ E[M {V /x}], D β c / ∈ fn(M ) c / ∈ n(E) E[async M ], D --→ νc (E[c] | c M ), D async E[c] | c V, D --→ E[V ] | c V, D push E[store f N M ], D --→ E[M ], D[f → N ] store E[call f ], D --→ E[D(f )], D call E[take f ], D --→ E[D(f )], undef(D, f ) take S, D --→ S , D νn S, D --→ νn S , D res-s S 1 , D --→ S 1 , D S 1 | S 2 , D --→ S 1 | S 2 , D par C --→ C νn C --→ νn C res-c C 1 ≡ C 1 C 1 --→ C 2 C 2 ≡ C 2 C 1 --→ C 2 str

Reductions

We can now define the reduction relation --→, which formalises the execution of terms in SKC. Relation --→ is the smallest relation closed under the rules displayed in Figure 4.

The semantics of SKC is based on the call-by-value evaluation strategy for λ-calculus. Specifically, rule β allows for an application to reduce only when its argument is a value (V ).

Rule async models the asynchronous execution of a function M : it creates a new future c, a parallel running function to compute the result of M in c, and binds c to the parallel composition of the caller (which is now waiting to receive the result) and the new running function. When the created running function reduces to a result value, the caller can collect this result by rule push.

In rule store, a term store f N M updates the definition repository D with the mapping (f, N ). The notation D[f → N ] means that D is updated to contain the mapping (f, N ): if f was already mapped to something, the old mapping is discarded.

In rule call, a term call f retrieves the body of the function f from the definition repository, if it is defined, and runs it. A term call f is stuck if the definition repository does not contain any mapping for f (but can become unstuck if a mapping appears later on). Rule take is similar, but the mapping for the called function is removed from the definition repository: we write undef(D, f ) for the repository obtained by removing the mapping for f from D.

The other rules are the expected ones for dealing with restriction (res-s and res-c), parallel composition (par), and structural equivalence (str): reductions under restriction and parallel composition can be lifted, and the reduction relation --→ is closed under the structural equivalence ≡.

Example 1 (Local vs Async execution).

As we are going to see in Section 3, the definition repository is useful to store data and functions that are commonly reused. By itself, term call f retrieves the body of function f from the repository and runs it locally. One can combine call with async to execute the retrieved function asynchronously, which gives some control on how functions from the repository should be executed.

The caller of a function does not need to worry about which strategy is used by the callee, since the semantics of SKC makes both to eventually reduce to the same result. For example, assume that D(f ) = V . The following reduction chains show the respective behaviours of the two strategies.

c call f, D --→ c V, D (1)
c async call f, D --→ νc (c c | c call f ), D --→ νc (c c | c V ), D --→ νc (c V | c V ), D (2)
The resulting term has the same behaviour of the one resulting from the local execution. One could make the two terms syntactically equal by implementing garbage collection for unused futures (and the related values).

Example 2 (Shared state). The definition repository can be used to store and share state. A simple example is keeping a counter of requests. We abuse notation and use arithmetic operators and natural numbers in SKC -as presented in Section 3. The counter can be initialised with (store counter V 0 M ) where V 0 is the initial value, and incremented with (λx. store counter (call sum 1 x) M ) (take counter)

In both the cases M is a continuation.

Example 3 (Libraries).

Updating shared state as in the previous example happens often in serverless computing. One could think of offering a replace primitive as syntactic sugar.

replace h N M (λx. store h (N x) M ) (take h)
We can then rewrite our previous counter example as follows.

replace counter (call sum 1) M Gabbrielli's Festschrift 5:8

A Formal Revisitation of Functions as a Service

We can actually use the definition repository of SKC to offer these kinds of user-defined functions as libraries. For example, the replace function above can be put in a repository and then invoked by programs as follows.

c (call replace) counter (call sum 1) M, {(replace, λname. λop. λcont. (λx. store name (op x) cont) (take name))} Example 4 (Private state). By combining the restriction operator with the primitives for manipulating the definition repository, we obtain private storage. This can be used, for example, to implement a log in a composition of function calls.

The library function newLog below creates a private log and initialises it with an empty list (nil, cf. Section 3).

(newLog, νlog (store log nil log))

A function can now create a log and pass it to other functions that it invokes, as follows (we omit the concrete composed functions M and N ). We assume the existence of a library function pair that takes two arguments and returns a pair (we show the definition of pair in Section 3).

(λx. (call pair ((M x)(N x))) x) (call newLog)
The functions M and N can internally use the library function replace to update the log by appending messages to the list. The idea is that N x is evaluated first, the result of which is then taken by M along with x (the name of the private log). The function pair retrieved from the repository then takes the final result from M and the x as the elements of the pair.

Notice that if the programmer wishes to run M and/or N asynchronously, they can just prepend the inner calls to these functions with the async keyword.

Using similar devices, one can implement stack traces and other tracing mechanisms with different scoping rules (per session, per client, etc.).

Use Cases

In this section, we present a couple of non-trivial SKC programs as use cases to show and comment how developers can use SKC to reason about their serverless implementations.

For the use cases, we take inspiration from the context of artificial intelligence (specifically, machine learning), which can benefit considerably from the dynamic scalability of serverless architectures [START_REF] Hellerstein | Serverless computing: One step forward, two steps back[END_REF][START_REF] Jonas | Cloud programming simplified: A Berkeley view on serverless computing[END_REF].

First, we present an implementation of the perceptron [START_REF] Rosenblatt | The perceptron: a probabilistic model for information storage and organization in the brain[END_REF][START_REF] Freund | Large margin classification using the perceptron algorithm[END_REF], an algorithm for binary classification which can decide to which of two classes an input, represented by a vector of numbers, belongs. Then, we present a scatter-gather algorithm that uses a neural network trained for image classification to infer the semantic content of an input image.

Before presenting the examples, we assume to extend SKC with the syntax for conditionals if M then M else M , with the traditional semantics. Moreover, we assume that the definition repository D executing our examples includes the definition of the Church encodings for pairs and lists.

A Serverless Perceptron Algorithm

The perceptron, first introduced by Rosenblatt [START_REF] Rosenblatt | The perceptron: a probabilistic model for information storage and organization in the brain[END_REF], is an algorithm for binary classification that, given an input and a set of weights, produces an output representing the predicted class.

A simple application of Rosenblatt's perceptron is the prediction of the logical conjunction.

Given the list of inputs (0, 0), (0, 1), (0, 1), and (1, 1), we aim at predicting the target values 0, 0, 0, and 1 respectively.

To obtain a trained model, i.e., a list of weights enabling the perceptron to find the targets corresponding to some given inputs, we start from a zero-initialised vector of weights (a list with the same cardinality of the inputs whose elements are all 0). The training algorithm consists of an iteration over a set of inputs labelled with the correct classification to return a new list of updated weights, aligned with the new provided "knowledge". Concretely, a training set for the logical conjunction contains pairs like ((0, 1), 0) and ((1, 1), 1), where the left element is the list of input's features and the right one is the classifying label -in this case, the binary representation of the truth value of the conjunction of the two elements in the list. Once trained, the weights can be used to predict the classification of further inputs. To complete the scenario, both the predict and training functions take a bias parameter that, in the perceptron algorithm, acts as the y-intercept of the line that separates the feature space. Without this added parameter it would not be possible to find a solution for the classification problem.

We start by describing the predict function, defined in Figure 5, which the training function uses to calculate an adjustment gradient and update the weights. Mathematically, the classification is based on the formula comp(f, w, bias) = bias Given a list of features f , a list of weights w and a bias parameter, the predict function calculates the classification of the individual, represented by the list of features, by summing the bias with the recursive sum of the pair-wise products of the elements in the two lists. To perform the recursive call, we use the let-bound function comp. All executions of the comp function are asynchronous -called using the async primitive, both inside the definition of comp (async ρ . . .) and at the initial invocation (async comp . . .).

+ |f | i=0 w i * f i : the item is classified with label "1" if the result is positive, "0" otherwise. D(predict) = λ ft. λ ws. λ bias. let comp ← (λ f . λ w. λ ρ. call sum (call prod (call head f )(call head w)) if (call isNil (call tail f )) then 0 else async ρ (call tail f ) (call tail w) ρ ) in if (call gt
The training function, defined in Figure 6, takes a list of features, a list of weights, a label classifying the individual represented by the features and the bias parameter. First, the function (asynchronously) tests whether the weights are already trained to correctly recognise the individual (i.e., the prediction equates the label) and, in that case, it returns a pair containing the current weights and the bias. Otherwise, we define a let-bound routine function that performs the training by recursively adjusting the weights (w) with respect to the features (f ) and a gradient parameter.

The training corresponds to the application of the following mathematical formula, which returns a list of adjusted weights: routine(f, w, grad) = [w 0 + grad * f 0 , . . . ,

w |w| + grad * f |f | ].
Similarly to the predict function described above, we use the async primitive to parallelise the execution of the adjustment of the weights. This is done with the initial asynchronous invocation of the routine function (async routine . . .) and the asynchronous recursive call within the definition routine (async ρ . . .).

Finally, we first define (through the let construct) the gradient parameter, which corresponds to the distance (i.e., the subtraction) between the label and the prediction (also executed asynchronously) and then we return a new pair containing the result of the execution of the routine function -which returns the adjusted weights -and the calculated gradientrepresenting the new bias of the adjusted weights.

Example 5 (Training and Prediction

). Now that we have defined both the predict and train functions, we can use them to "emulate" the logical conjunction (where the weights 0 and 1 represent false and true values). First, we introduce in the definition repository the utility function trainAndStore which, given the weights and bias of the model -stored as a pair by a function wsName in the definition repository -, some features, and a label, performs the training of the model and replaces the "old" weights and bias with the new, trained ones. To ensure atomicity, trainAndStore uses the take primitive to remove the "weights" from the definition environment while it is computing the new ones. In this way, if other clients are trying to access the same weights (name-wise), they are blocked until it finishes computing and it executes the store instruction to "release" them in the definition repository.

We can now train our model to emulate the logical conjunction (wa represents the weights and bias of the model) -below we omit D for compactness. Above, the running function at the bottom (with future c 5 ) uses the trained weights -at any possible stage of the training, due to the interleaving of the execution -to predict the result of the conjunction of the Boolean values 0 and 1.

In the example above, we showed an initial configuration already featuring some running functions. Indeed, since we consider a reduction semantics, we do not model the invocation of functions from outside the system. To consider also the point of view of the user of the serverless system, one could equip SKC with a labelled semantics supporting both the invocation of functions and the retrieval of the results of the evaluation from outside the system. We leave this direction for future work.

A Serverless Large Image Tagger

In the following, we illustrate the use of the proposed language abstractions in order to model a simple system for tagging large images. The example takes advantage of an Artificial Intelligence (AI) algorithm to extract semantic content from an image. In computer vision it is common practice to segment the content of a photo to assign a label indicating the nature of the object(s) represented in each segment, for example a person, an animal, or a thing. Although modern AI techniques and in particular deep convolutional neural networks are able to predict the semantic content of an image with extreme accuracy, these algorithms normally take small inputs and are not adequate to classify images at ultra-high resolutions, e.g., the recent 4K format corresponding to 3840 × 2160 pixels. As a reference, MobileNetV2 [START_REF] Sandler | MobileNetV2: Inverted Residuals and Linear Bottlenecks[END_REF] is a well-known neural network architecture able to achieve fast object classification with accuracy of around 90% over 3-channel colour image inputs of 224 × 224 pixels.

With the purpose to build a system for annotating ultra-high resolution images, we want to exploit the parallel execution of inference processes to find the labels associated with each image portion and aggregate them at the end of the single computations. The scenario lends itself well to a serverless deployment strategy and can benefit from the language constructs provided by the SKC language. Summarising, our strategy is to split the image into portions that can be quickly annotated by the AI and to aggregate the results computed for each of these parts. This can be simply rendered in SKC by the tag function below: where function split splits the image and function aggregate classifies each portion and aggregates the results.

We discuss below in detail function aggregate, defined in Figure 7, which scatters the asynchronous computations over the fixed-side portions of the original image (as obtained from the split function, omitted here) and assembles their results. In the snippet in Figure 7, we use the functions to manage pairs and lists already existing in the D repository, defined at the beginning of this section. A function infer is also left undefined in the example. In principle, the infer function could be any machine learning algorithm that performs the actual recognition task for the image content given its feature set. Notably, we use function isNil from the previous section to calculate the condition of the block if and check whether the result list contains further elements. If not, the algorithm terminates and returns the generated list.

D(aggregate

The aggregation function takes a vector of splits, parts of the image, and returns a list containing for each portion its identifier and the list of associated labels. An example of the output for an image representing a seascape in the vicinity of a harbour will take the form ((((0, 0), (223, 223)), (house, sea)), (((0, 224), (224, 447)), (house, boat, sea)), . . . ). Each identifier contains the coordinates of the portion of the image, represented as two pairs of pixel coordinates. For simplicity, we assume that the result of the split function is a list of pairs, the first element of each pair contains the coordinates of the portion while the second element contains the actual portion features.

The infer function, that computes the single-portion prediction, retrieves a list of strings, which represents the image tags. The aggregate function concatenates the result of the prediction of the first portion of the image with the result of the recursive call on the rest of the split list. Note that both the calls of infer and of aggregate are made using the async construct. This allows for parallel execution. The result is nevertheless deterministic since the asynchronous functions are independent.

The example presented is intuitive but complex enough to show a highly distributed behaviour. The serverless deployment scenario takes advantage of the constructs for asynchronous execution and helps the programmer to think about the system in a compositional and holistic way. Background: the π-calculus

In this section we introduce the syntax and semantics of π-calculus, and some elements of its theory, to be used in Section 5 to define and prove the correctness of the encoding of SKC into the π-calculus itself. In the encoding, we actually use the asynchronous π-calculus, as normal when encoding functional languages, though we usually still call it π-calculus. The asynchronous π-calculus has some striking algebraic properties that fail in the ordinary π-calculus [START_REF] Boreale | Some congruence properties for π-calculus bisimilarities[END_REF], and that will be important in our study. The encoding of a λ-term will be parametric on a name. Such parametric processes are called abstractions. The actual instantiation of the parameters of an abstraction F is done via the application construct F ã . Processes and abstractions form the set of π-agents (or simply agents). Small letters a, b, . . . , x, y, . . . range over the infinite set of names and ã denotes a tuple of such names. The grammar of the π-calculus is thus:

Agents A := P | F Processes P := 0 | a( b). P | a b . P | νa P | P 1 | P 2 | !a( b). P | F ã Abstractions F := (ã) P
In the grammar for processes, 0 is the inactive process. An input-prefixed process a( b). P , where b has pairwise distinct components, waits for a tuple of names c to be sent along a and then behaves like P { c/ b}, where { c/ b} is the simultaneous substitution of names b with names c. An output particle a b emits names b at a. Parallel composition allows one to run two processes in parallel. The restriction νa P makes name a local, or private, to P . A replication !a(x). P stands for a countable infinite amount of copies of a(x). P in parallel.

When the tuple b is empty, the surrounding brackets in prefixes will be omitted. We abbreviate νaνbP as (νa, b)P . An input prefix a( b). P , a restriction νbP , and an abstraction ( b) P are binders for names b and b, respectively, and give rise in the expected way to the definition of free names (fn(-)) and bound names (bn(-)) of a term or a prefix, and αconversion.

Since the calculus is polyadic, a type system is needed to avoid disagreements in the arities of the tuples of names carried by a given name and in applications of abstractions. We will not present the typing system, however, because not really essential. A context E of π is a π-agent in which some subterms have been replaced by the hole [•]; then E[A] is the agent resulting from replacing the hole with the term A. Of course it is assumed that, under a type system, we only relate (e.g., using barbed congruence, described later on) agents obeying the same typing, and then we insert them only in contexts that respect such a typing. We assign parallel composition the lowest precedence among the operators.

The operational semantics of the π-calculus is standard [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF] and given in Figure 8. The reference behavioural equivalence for π-calculus will be the usual barbed congruence [START_REF] Milner | Barbed bisimulation[END_REF]. We recall its definition. We write P ⇓ a if P µ =⇒ P , for some P and µ is an output action at a. (We make only output observable because this is standard in asynchronous calculi.) A repository of terms is modelled as the parallel composition ( denotes indeed n-ary parallel composition) of the encodings of the individual terms, in which a function name f is used to obtain access to the location of the λ-term referred to by f . The imperative nature of the repository is reflected in the reference-like usage of function names. A repository in which f is assigned to M becomes, in the π-calculus, an output f a where a is a fresh name that gives access to (the location of) M . This also explains the encoding of the constructs take f and call f , in which the current content of f is read (as an input). Only in call f such content is then re-emitted; take f does not, as it is supposed to remove f from the repository. Construct store f N M introduces the appropriate output at f , so to add f to the repository.

The encodings use different kinds of names: location names, ranged over by p, q; value names, ranged over by x, y, for accessing the body of a value; function names, ranged over by f , for accessing functions in the repository; future names, ranged over by c; support names, ranged over by a, b, used to access terms in the repository. In the encoding, as well as in the syntax of SKC, h ranges over value and function names. We assume a type system in the π-calculus in which these kinds of names are separated. Depending on the types of SKC, these kinds may correspond to collections of π-calculus types (we recall that the encoding of pure untyped λ-calculus can be refined to an encoding of typed λ-calculus [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF]). A sorting system, à la Milner [START_REF] Milner | The polyadic π-calculus: a tutorial[END_REF], may be used to keep track of the arities of the names. However we need at least to impose I/O capabilities [START_REF] Pierce | Typing and subtyping for mobile processes[END_REF] to make sure that only the output capability of the value and support names is communicated. This is essential for the correctness results below. The typing could however be more precise, by stipulating that function names should follow the discipline of reference names of the π-calculus [START_REF] Hirschkoff | On the representation of references in the pi-calculus[END_REF] (precisely, a destructive variant in which at any time at most one output at one of these names is available). Similarly, a more precise typing would set value and support names as ω-receptive names [START_REF] Sangiorgi | The name discipline of uniform receptiveness[END_REF]. For proving more refined correctness properties on the encoding, or using the encoding to validate program transformations or optimisations (e.g., [START_REF] Sangiorgi | Typed π-calculus at work: a correctness proof of Jones's parallelisation transformation on concurrent objects[END_REF][START_REF] Sangiorgi | Termination of processes[END_REF][START_REF] Demangeon | Termination in impure concurrent languages[END_REF]), such refined types would have to be taken into account.

In the encodings of store and async, a τ prefix is added so to make sure that a reduction in SKC corresponds to at least one reduction in π-calculus. This is also needed for Lemma 8. The encodings are extended to contexts and evaluation contexts, in the expected manner, exploiting the compositionality of the encoding.

Lemma 8 shows that only the translation of evaluation contexts yields evaluation contexts in the π-calculus. An occurrence of a term in a π-calculus expression is unguarded if that occurrence is not underneath a prefix.

Lemma 8. For any function context E, the hole of the

π-calculus context [[E]] is unguarded iff E is an evaluation context. Lemma 9. For all M, V , we have: [[(λx. M )V ]] ≈ [[M { V /x}]].
Proof. We follow a case analysis on V . The case when V = x or V = f is easy. When V is an abstraction, we proceed by induction on M , exploiting the Replication Theorem 7 (here, the output capability on names x, y is essential).

The induction is similar to that in the proof of validity of β-reduction for the pure call-by-value λ-calculus [START_REF] Sangiorgi | Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms[END_REF], the main difference is that there are more cases to consider, however the reasoning is analogous. Proof. We proceed by rule induction. The inductive part follows from the compositionality of the encoding. For the base case, we make a case analysis on the rule applied. Rule β. We use Lemma 9.

Encoding of functions [[M

N ]] def = (p) νq [[M ]] q | q(y). νr ([[N ]] r | r(w). y w, p ) [[call h]] def = (p) (h(a). (h a | a p ) [[async M ]] def = (p) τ . νc ([[c]] p | [[c M ]] * ) [[store h N M ]] def = (p) τ . ([[M ]] p | νa (h a | !a(q). [[N ]] q )) [[take h]] def = (p) h(y). y p [[νf M ]] def = (p) νf [[M ]] p [[c]]

Encoding of values

[[λx. M ]] def = (p) νy p y . !y(x, q). [[M ]] q [[h]] def = (p) p h
Rule async. We use the definition of the encoding and Lemma 8.

Rule push. We have (omitting the store, which does not contribute) Proof. Using a case analysis similar to that in the proof of Theorem 10, taking on applications, when applicable, the clauses of the optimised encoding.

E[c] | c V -→ E[V ] | c V
Both Theorems 10 and 12 can be extended to multi-step reductions (i.e., relation =⇒ in place of the one-step reduction -→).

Discussion and Conclusion

In this work, we explore the SKC serverless calculus under two aspects: its design space (the language layer) and its usefulness in reasoning on serverless implementations (the implementation layer). Towards the first aim, we consider features from process calculi to represent the concurrent execution of functions and to better integrate the essential features of the two calculi that inspire SKC: the λ-and the π-calculus. Part of that redesign consists in having functions parametric on the names of other functions. That inclusion allows us to create new function names for the function-definition repository dynamically, so the repository of available functions can grow freely at runtime, as well as holding private function definitions and private stored data. As part of that exploration, we present a refined syntax and semantics for SKC, supporting the aforementioned improvements, and we illustrate how those new features enhance the expressiveness of the language through small examples and two use cases from artificial intelligence.

Then, to illustrate how SKC supports reasoning on the implementation layer, we focus on how to translate SKC-defined architectures (of functions) into a network of communicating, concurrent, and mobile processes, representing the actual network of concurrent processes that run those serverless functions in the cloud. We tackle this second task by presenting an encoding from SKC to the asynchronous π-calculus and proving it correct in terms of an operational correspondence result, using standard techniques -whose side-effect is to cast a good outlook on the affordability of extending results from the literature to SKC.

We remark that the choice of using futures as one of the main building blocks of SKC comes from a careful consideration on the minimality of the language. Indeed, if one might consider named channels (as in CCS/π-calculus [START_REF] Milner | A Calculus of Communicating Systems[END_REF][START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF]) a standard choice of communicating systems, in the case of SKC they would increase the distance between the language and concrete serverless implementations. For example, with channels one could have re-usable, bidirectional communication between functions, which is a feature no serverless implementation currently provides. Moreover, our encoding shows a way to define futures using channels while the opposite is also possible [START_REF] Niehren | A concurrent lambda calculus with futures[END_REF].

Regarding related work, the proposal closest to SKC is [START_REF] Jangda | Formal foundations of serverless computing[END_REF], where a calculus more involved than SKC is presented. It captures the low-level details of current serverless implementations (e.g., cold/warm components, storage, and transactions are primitive features of their model), essentially mixing the language and implementation layers. Contrarily, SKC strives to be a kernel model of serverless computing, with the suggested strategy to reason on implementations via encodings. Another work close to SKC is [START_REF] Niehren | A concurrent lambda calculus with futures[END_REF], where the authors introduce a λ-calculus with futures. Since the aim of [START_REF] Niehren | A concurrent lambda calculus with futures[END_REF] is to formalise and reason on a concurrent extension of Standard ML, their calculus is more involved than SKC, as it contains primitive operators (handlers and cells) to capture safe non-deterministic concurrent operations, which we can encode as macros in SKC. An interesting future work is to investigate which results from [START_REF] Jangda | Formal foundations of serverless computing[END_REF][START_REF] Niehren | A concurrent lambda calculus with futures[END_REF] we can adapt to SKC.

Other future directions of research on SKC include the exploration of guarantees on sequential execution across functions, which compels the investigation of new tools to enforce sequential consistency [START_REF] Lamport | How to make a multiprocessor computer that correctly executes multiprocess programs[END_REF] or serialisability [START_REF] Papadimitriou | The serializability of concurrent database updates[END_REF] of the transformations of the global state [START_REF] Hellerstein | Serverless computing: One step forward, two steps back[END_REF]. That challenge can be tackled developing static analysis techniques and type disciplines [START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF][START_REF] Ancona | Behavioral types in programming languages[END_REF] for SKC. Another direction concerns programming models, which should give to programmers an overview of the overall logic of the distributed functions and capture the loosely-consistent execution model of serverless [START_REF] Hellerstein | Serverless computing: One step forward, two steps back[END_REF]. Choreographic Programming [START_REF] Montesi | Choreographic Programming[END_REF][START_REF] Cruz | A core model for choreographic programming[END_REF] is a promising candidate for that task, as choreographies are designed to capture the global interactions in distributed systems [START_REF] Kavantzas | Web services choreography description language version 1.0, W3C candidate recommendation[END_REF], and recent results [START_REF] Carbone | Deadlock-freedom-by-design: multiparty asynchronous global programming[END_REF][START_REF] Dalla Preda | Dynamic choreographies: Theory and implementation[END_REF][START_REF] Giallorenzo | Applied choreographies[END_REF][START_REF] Giallorenzo | Choreographies as objects[END_REF] confirmed their applicability to microservices [START_REF] Dragoni | Microservices: Yesterday, today, and tomorrow[END_REF], a neighbouring domain to that of serverless architectures. Such an approach can also cover Edge and Internet-of-Things scenarios (as targeted by projects like AWS Greengrass1 ), using language abstractions borrowed from the world of microservice systems [START_REF] Gabbrielli | A languagebased approach for interoperability of IoT platforms[END_REF]. The language extensions and results on the encoding presented in this paper are stepping stones for a transformation framework between serverless and microservice architectures. There, the final goal would be to provide an infrastructure where, depending on the application context (e.g., the amount of stateful interactions) and inbound load (steadier traffic benefit the always-on microservices deployment, while serverless is more efficient when considering traffic bursts), users (or automatic optimisation systems) can decide whether to deploy a given architecture (or part of it) as a network of serverless functions or microservices. Indeed, if SKC is the model for serverless and π-calculus-inspired process calculi [START_REF] Montesi | Service-oriented programming with Jolie[END_REF] represent microservices, our encoding is a first result towards a framework for the semantic-preserving transition between the two implementation/deployment paradigms.

A clearer understanding of the implementation layer also provides foundations for tackling some outstanding questions in serverless computing. For example, predicting resource usage and costs is challenging in general, since it requires knowing how functions are executed by the implementation layer. This last one is particularly relevant in the per-usage model of serverless architectures, yet it requires to extend SKC with an explicit notion of time to support quantitative behavioural reasoning for timed systems [START_REF] Brengos | Behavioural equivalences for timed systems[END_REF][START_REF] Brengos | A uniform framework for timed automata[END_REF]. A starting point could be to use the encoding into π-calculus to prove termination properties of the source SKC language, combining type techniques from functional and concurrent languages [START_REF] Demangeon | Termination in impure concurrent languages[END_REF].

Figure 4

 4 Figure 4 SKC, reduction rules.

D

  (pair) = λx. λy. λz. z x y D(isNil) = call first D(first) = λp. p(λx. λy. x) D(cons) = λh. λt. call pair false (call pair h t) D(second) = λp. p(λx. λy. y) D(head) = λz. call first (call second z) D(nil) = call pair true true D(tail) = λz. call second (call second z)Hence, for example, we can write the list 1, 2, 3 as (call cons 1 (call cons 2 (call cons 3 call nil))).We also assume to extend SKC with the standard arithmetic (+, -, * ) and relational (>, =) operators, on which we build the following functions, also assumed present in the definition repository D. D(sum) = λx. λy. x + y D(prod) = λx. λy. x * y D(sub) = λx. λy. x -y D(gt) = λx. λy. x > y D(eq) = λx. λy. x = y Finally, we extend SKC with let expressions: let x ← M in M (λx. M ) M .

Figure 5

 5 Figure 5 Function predict.

D

  (trainAndStore) = λ wsName. λ fs. λ label. ( λ ws. (store wsName (call train fs (call first ws) label (call second ws)) ()) take wsName)

5 : 12 A

 512 Formal Revisitation of Functions as a Service D(tag) = λ image. (call aggregate (call split image))

Figure 7

 7 Figure 7 Function aggregate.

  Transitions are of the form P a( b) --→ P (an input, b are the bound names of the input prefix that has been fired), P ν d a b ----→ P (an output, where d ⊆ b are private names extruded in the output), and P τ -→ P (an internal action). As usual, =⇒ is the reflexive and transitive closure of

Theorem 10 (: 16 A

 1016 Operational correspondence, from SKC to π). If C -→ C then [[C]] * -→≈ [[C ]] * . 5Formal Revisitation of Functions as a Service Encoding of definition repositories [[D]] * def = Π (f,M )∈D νa (f a | !a(q). [[M ]] q ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Encoding of configurations [[ S, D ]] * def = [[S]] * | [[D]] * [[νn C]] * def = νn [[C]] * . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Encoding of systems [[c M ]] * def = νp ([[M ]] p | p(y). !c(z). z y ) [[S | S ]] * def = [[S]] * | [[S ]] * [[νc S]] * def = νc [[S]] * [[0]] * def = 0 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  def = (p) c p . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 9

 9 Figure 9The encoding of SKC into the π-calculus.

11 .

 11 For any C, we have [[C]] * ≈ {[C]} * . We state the converse of Theorem 10 on the optimised encoding {[-]}. Theorem 12 (Operational correspondence, from π to SKC). If {[C]} * -→ P then there is C with C -→ C and P ≈ [[C ]] * .

  D(train) = λ features. λ weights. λ label. λ bias.if call eq (async call predict features weights bias) label then call pair weights bias else let routine ← ( λ f . λ w. λ grad. λ ρ.

	call cons
	call sum (call head w) (call prod grad (call head f ))
	if call isNil (call tail f )
	then call nil
	else async ρ (call tail f ) (call tail w) grad ρ
	) in
	let gradient ← (call sub label (async call predict features weights bias))
	in call pair
	async routine features weights gradient routine
	gradient
	)
	Figure 6 Function train.

  c0 store wa (call pair (call cons 0 call cons 0 call nil) 1) ()

| c1 call trainAndStore wa (call pair (call cons 0 call cons 0 call nil) 0) | c2 call trainAndStore wa (call pair (call cons 0 call cons 1 call nil) 0) | c3 call trainAndStore wa (call pair (call cons 1 call cons 0 call nil) 0) | c4 call trainAndStore wa (call pair (call cons 1 call cons 1 call nil) 1) | c5 λ w. (call predict (call cons 0 call cons 1 call nil) (call first w) (call second w)) call wa

Gabbrielli's Festschrift

https://aws.amazon.com/greengrass/

Funding Fabrizio Montesi: Partially supported by Villum Fonden (grant no. 29518). Davide Sangiorgi: Partially supported by MIUR-PRIN project "Analysis of Program Analyses" (ASPRA, ID 201784YSZ5_004).

Definition 6 (Barbed congruence). Barbed bisimilarity is the largest symmetric relation • on π-calculus processes such that P • Q implies:

As explained in the description of the encoding, we will need capability types [START_REF] Pierce | Typing and subtyping for mobile processes[END_REF] for the π-calculus (or their ω-receptive refinement [START_REF] Sangiorgi | The name discipline of uniform receptiveness[END_REF]), so to allow us to use the following replication theorem in the correctness proof of the encoding.

Theorem 7 (Replication theorem). Suppose only the output capability of x can be communicated (or that x is ω-receptive); then we have:

Encoding SKC into π-calculus

In this section, based on Milner's encoding of call-by-value λ-calculus [START_REF] Milner | Functions as processes[END_REF], we study an encoding of SKC into π-calculus. We follow the investigation of the correctness of the representation of pure functions in π-calculus, in particular [START_REF] Milner | Functions as processes[END_REF][START_REF] Sangiorgi | An investigation into functions as processes[END_REF]. We assume a base type system in SKC that at least distinguishes function values such as λx. M from nominal values such as f (of course, depending on how the type system for SKC is defined, function values and nominal values could be collections of types; we do not go into the details of the types as they would obscure the readability of the encoding and its correctness proofs). Moreover, the type system ensures us that whenever a nominal value f is used with the store construct then the repository is not defined on f (thus the replacement of an element of the repository needs a take and then a store).

The encoding is presented in Figure 9. We have to distinguish the encoding of functions and values, that returns an abstraction, from the encoding of the other syntactic categories, that returns a process. We use [[-]] for the former, and [[-]] * for the latter.

In the encoding of functions and values, the parameter may be thought of as the location of that term. A term that becomes a value signals so at its location name and provides access to the body of the value. Such body is replicated and thus may be copied several times. When the value is a λ-function, it receives two names: (the access to) its value-argument, and the location for the resulting term.

We assume V is an abstraction (the case when it is a function name is simpler); we then abbreviate the encoding of an abstraction λx. M as

[[λx. M ]] p = νy (p y | [[M ]] y

V ) In the encoding, we have, for some p::

where in the second use of ≈ we exploit the Replication Theorem 7 (i.e., the output capability constraint on y). Rule store. The rule is

We have, for some Q that does not contain f , and some p:

for M = D(f ). We have, for some Q that does not contain f , and some p:

where in the first application of ≈ we exploit the τ -insensitiveness property of the name a (equivalently, the Replication Theorem 7 on a). The case of rule take is easy.

The converse direction is more delicate because the π-calculus encoding presents a number of administrative reductions, which do not correspond to actual reductions in the source calculus. We overcome the problem following [START_REF] Durier | Eager functions as processes[END_REF], which presents an optimisation of Milner's encoding of application (and hence of the encoding of SKC). The optimised encoding, indicated as {[-]} below, is obtained from the initial one by performing a few (deterministic) reductions, at the price of a more complex definition. These reductions are performed in the clause for application, when at least one of the two involved terms is a value. We only show the definition for the different clauses. In the last clause below it is intended that N is not a value. The three clauses are applied only on applications M N in which both M and N are closed (i.e., they have no free λ-variables); if they are applicable they have priority over the clauses of the initial encoding [[-]]. Moreover the first clause has priority over the last one. The following lemma establishes the correctness of the optimised encoding.


Anna Santarsiero

Antonella Bochicchio

Maria Funicello

Paolo Lupattelli

Sabine Choppin

Françoise Colobert

Gilles Hanquet

Lucie Schiavo

Paolo Convertini
email: paolo.convertini@uky.edu

Lucia Chiummiento
email: lucia.chiummiento@unibas.it

Vittoria Infantino

New synthesized polyoxygenated diarylheptanoids suppress lipopolysaccharide-induced neuroinflammation

Keywords: neuroinflammation, microglia, diarylheptanoids, anti-neuroinflammatory activity, NF-κB, ATP citrate lyase

Introduction

Chronic neuroinflammation has a pivotal role in the onset and progression of a broad range of neurodegenerative diseases such as Alzheimer´s disease, Huntington's disease, Parkinson's disease and multiple sclerosis [START_REF] Spangenberg | Inflammation in Alzheimer's disease: Lessons learned from microglia-depletion models[END_REF]. Neuroinflammation is a consequence of the activation of microglia, the resident immune cells of the central nervous system. Microglial cells influence brain development and constantly survey the microenvironment of parenchyma, but they also act as the first line of defence against injury and invading pathogens. When the homeostasis is disrupted, microglia becomes activated and undergoes morphological and phenotypical changes into one of the two extremes of polarization: the classically activated M1 or alternatively activated M2 macrophages. M1 microglia secretes pro-inflammatory cytokines (e.g. TNF-α, IL-1β, IL-6), chemokines, prostaglandin E2 (PGE2), reactive oxygen species (ROS), and reactive nitrogen species [START_REF] Moss | Activation of murine microglial cell lines by lipopolysaccharide and interferon-gamma causes NO-mediated decreases in mitochondrial and cellular function[END_REF], which elicit detrimental effects on adjacent neurons and further exacerbate tissue inflammation and damage. By contrast, in M2 microglial cells the expression of anti-inflammatory mediators is up-regulated and they contribute in neuroprotection and tissue recovery and remodelling [START_REF] Subhramanyam | Microglia-mediated neuroinflammation in neurodegenerative diseases[END_REF]. Therefore, neuroinflammation is a double-edged sword because of its beneficial or harmful effects on central nervous system, which depend on the type of microglia activation and the duration of inflammatory response. In fact, acute events scavenge harmful substances playing a protective role for nervous tissue while chronic ones are always dangerous due to the production and release of pro-inflammatory and cytotoxic factors [START_REF] Block | Neuroinflammation: modulating mighty microglia[END_REF].

In neurodegenerative diseases the equilibrium between microglial surveillance and activation is disrupted and growing evidence demonstrates that the control of microglia activation could attenuate their severity [START_REF] Perry | Microglial priming in neurodegenerative disease[END_REF]. Therefore, the discovery of antineuroinflammatory compounds able to inhibit the microglia activation could be helpful in neurodegenerative disorders.

Diarylheptanoids (C6-C7-C6), a class of oxygenated compounds with a 1,7diphenylheptane skeleton, have been isolated from wood, bark or leaves of many hardwoods including Betulaceae, Leguminosae, Myricaceae and Proteaceae. They are increasingly recognized as potential therapeutic agents for their wide spectrum of biological and pharmacological activities such as anti-inflammatory, antioxidant, antitumor, estrogenic, leishmanicidal, melanogenesis, hepatoprotective, neuroprotective proprieties [START_REF] Lv | Naturally occurring diarylheptanoids[END_REF]. To this class of natural products belongs myricanol, a cyclic and not symmetric diarylheptanoid extracted from Myrica species, and curcumin, the main curcuminoid isolated from Curcuma longa (Fig. 1). It has been shown that myricanol reduces the levels of the microtubuleassociated protein tau resulting in anti-Alzheimer's disease effect [START_REF] Martin | Synthesis, stereochemical analysis, and derivatization of myricanol provide new probes that promote autophagic tau clearance[END_REF] and curcumin exerts neuroprotective and anti-inflammatory activities [START_REF] Garcia-Alloza | Curcumin labels amyloid pathology in vivo, disrupts existing plaques, and partially restores distorted neurites in an Alzheimer mouse model[END_REF][START_REF] Li | Curcumin by down-regulating NF-kB and elevating Nrf2, reduces brain edema and neurological dysfunction after cerebral I/R[END_REF][START_REF] Parada | Microglial HO-1 induction by curcumin provides antioxidant, antineuroinflammatory, and glioprotective effects[END_REF]. In particular, curcumin inhibits PGE2, nitric oxide (NO), and tumor necrosis factor α (TNF-α) release following lipopolysaccharide (LPS) stimulation in RAW 264.7 murine macrophages [START_REF] Pae | Dimethoxycurcumin, a synthetic curcumin analogue with higher metabolic stability, inhibits NO production, inducible NO synthase expression and NF-kappaB activation in RAW264.7 macrophages activated with LPS[END_REF] and switches the polarization of LPS-activated BV2 microglial cells from M1 phenotype to a predominantly M2 phenotype [START_REF] Zhang | Curcumin inhibits LPS-induced neuroinflammation by promoting microglial M2 polarization via TREM2/ TLR4/ NF-kappaB pathways in BV2 cells[END_REF].

Taking into consideration the biological importance of linear diarylheptanoids in general, and myricanol and curcumin in particular, we planned a straightforward access to a series of linear diarylheptanoid derivatives using the cross-metathesis reaction on readily available precursors 1a,b, 2a,b and 3 [START_REF] Bochicchio | Selective Claisen rearrangement and iodination for the synthesis of polyoxygenated allyl phenol derivatives[END_REF][START_REF] Bochicchio | Convergent total synthesis of (+/-) myricanol, a cyclic natural diarylheptanoid[END_REF][START_REF] Massé | Unintended Formation of a 26-Membered Cycle in the Course of a Novel Approach to Myricanol, a Strained [7,0]-Metacyclophane[END_REF]. Terminal olefins 1-3 [START_REF] Bochicchio | Convergent total synthesis of (+/-) myricanol, a cyclic natural diarylheptanoid[END_REF] were easily prepared and used to give access to new linear diarylheptanoids and to the cyclic one, myricanol. Herein some of these were differently protected, halogenated and reduced. Eleven of the new synthesized diarylheptanoids were tested on a cell line model of neuroinflammation: LPS-triggered BV-2 cells. Their effect on different mediators of inflammation was evaluated in comparison with curcumin and celecoxib, a COX-2 selective non-steroidal anti-inflammatory drug (Fig. 1). Celecoxib, in a rat model with LPStriggered neuroinflammation, significantly decreased the rate of microglia activation and levels of IL-1β and TNF-α pro-inflammatory cytokines [START_REF] Fan | Celecoxib attenuates systemic lipopolysaccharide-induced brain inflammation and white matter injury in the neonatal rats[END_REF]. Finally, the ability of the new synthesized diarylheptanoids to reduce NF-κB and ATP citrate lyase (ACLY) -a metabolic pro-inflammatory enzyme -was also investigated.

Material and Methods

Cell culture, treatment and cell viability assay

The immortalized murine BV-2 microglial cell line was maintained in Roswell Park Memorial Institute 1640 Medium supplemented with 10% heat inactivated fetal bovine serum, 4 mM L-Glutamine, 100 U/ml penicillin and 100 μg/ml streptomycin at 37°C and 5% CO2. Where indicated BV-2 cells were activated with 200 ng/ml LPS from Salmonella enterica serotype typhimurium (LPS, Sigma-Aldrich, St. Louis, MO, United States). Cell viability was evaluated by using CellTiter 96® Non-Radioactive Cell Proliferation Assay (Promega, Madison, WI, USA) according to manufacturer's instructions. The details are given in Supplementary data.

Enzyme-linked immunosorbent assay (ELISA)

The concentration of pro-inflammatory cytokines IL-6 (Cat. n° 32670069U1, ImmunoTools, Friesoythe, Germany) and TNF-α (Cat. n° 32673019U1, ImmunoTools) in cell culture media was measured with ELISA kits following the manufacturer's recommendations. The levels of PGE2 were quantified by using DetectX® Prostaglandin E2 High Sensitivity Immunoassay Kit (Arbor Assays, Ann Arbor, MI, USA) as per manufacturer's protocol.

ROS and NO detection

Reactive oxygen species and nitric oxide levels were measured by using 6-Carboxy-2',7'-

Dichlorodihydrofluorescein

Diacetate and 4-Amino-5-Methylamino-2',7'-Difluorofluorescein Diacetate (Thermo Fisher Scientific, San Jose, CA, USA), respectively, as previously described [START_REF] Convertini | The contribution of the citrate pathway to oxidative stress in Down syndrome[END_REF].

Western blotting

Western blotting experiments were carried-out as reported previously [START_REF] Infantino | Epigenetic upregulation and functional role of the mitochondrial aspartate/glutamate carrier isoform 1 in hepatocellular carcinoma[END_REF] using anti-NF-κB/p65 (ab7970), anti-ATP citrate lyase (ab157098) or anti-β-actin (ab8227) primary antibodies (Abcam, Cambridge, MA). More details are reported in Supplementary data.

Statistical analysis

Statistical significance of differences was determined by using Student's t-test. Results are shown as means ± SD of, at least, four independent experiments. Differences were considered as significant (*p < 0.05), very significant (**p < 0.01) and highly significant (***p < 0.001).

Results

Preparation of diarylheptanoids 4-6

The requisite allylphenols 1a and 1b were accessed in two steps from commercially available 2,3dimethoxyphenol [START_REF] Bochicchio | Selective Claisen rearrangement and iodination for the synthesis of polyoxygenated allyl phenol derivatives[END_REF]. Coupling partners 2a, b and 3 were readily prepared from commercial methyl 3-(4-benzyloxyphenyl)propanoate [START_REF] Bochicchio | Convergent total synthesis of (+/-) myricanol, a cyclic natural diarylheptanoid[END_REF][START_REF] Massé | Unintended Formation of a 26-Membered Cycle in the Course of a Novel Approach to Myricanol, a Strained [7,0]-Metacyclophane[END_REF]. With the key fragments 1a, 1b, 2a, 2b and 3 in hands, we attempted cross metathesis (CM) reactions as depicted in Scheme 1 [START_REF] Bochicchio | Convergent total synthesis of (+/-) myricanol, a cyclic natural diarylheptanoid[END_REF][START_REF] Connon | Recent developments in olefin cross-metathesis[END_REF][START_REF] Nicolaou | Metathesis reactions in total synthesis[END_REF]. Hence, treatment of 1a (4 equiv.) with 2a or 2b (1 equiv.) in the presence of G-II catalyst (5mol%) in dichloromethane from -78°C to room temperature provided diarylheptanoid 4a and 4c in a gratifying 81% and 83% yield, respectively, if compared to the examples of CM at low temperature reported in literature [START_REF] Rogano | The Biomimetic Synthesis and First Characterization of the (+)-and (-)-Isocentrolobines, 2,6-cis-and 2,6-trans-Disubstituted Tetrahydro-2H-pyrans[END_REF].

Addition of G-II catalyst at -78°C was mandatory to obtain good yields. Excess of partner 1a and its homocoupled were almost fully recovered after chromatography.

Cross metathesis between 1b and 2a afforded coupling product 4b in only 35% yield without formation of homocoupling product resulting from dimerization of 1b. While positive effect of free OH (phenol or alcohol) on CM reactions, already reported in literature [START_REF] Forman | A Convenient System for Improving the Efficiency of First-Generation Ruthenium Olefin Metathesis Catalysts[END_REF][START_REF] Lin | The allylic chalcogen effect in olefin metathesis[END_REF][START_REF] Maishal | Effect of a proximal oxygen substituent on the efficacy of ruthenium-catalyzed cross-metathesis and RCM[END_REF], could explain the excellent yield obtained to produce 4a (81% yield), an opposite behavior was observed in the preparation of compound 4b (Scheme 1) despite the presence of two free OH on the starting catechol 1b.

Probably the lower solubility of catechol 1b in DCM at -78°C prevented the metathesis reaction which started only increasing the temperature (20°C). No dimerization of 1b was observed or after column chromatography. Moreover reaction between 1a and 2b gave rise to compound 4c in high yield (82%) and cross metathesis between 1a and 3 afforded alkene 4e in only 32% of yield.

Subsequent transformations were performed in order to have different protections and different functionalities(double bond, ketone or halide) on the same parent scaffold.

Therefore, the acetylation of 4a by Ac2O in pyridine afforded 4d in a quantitative yield, while the methylation of 4e furnished the allylketone 4f in 30% of yield.

Hydrogenation of the double-bond and concurrent debenzylation of 4a resulted in the quantitative formation of 5a which was selectively protected on phenols as methyl ethers 5d. Chemoselective hydrogenation of 4c by o-NO2PhSO2Cl and N2H2 [START_REF] Marsh | One-Pot o-Nitrobenzenesulfonylhydrazide (NBSH) Formation-Diimide Alkene Reduction Protocol[END_REF] furnished 5b in high yield, preserving the benzyl protecting group and the iodine atom of 4c. Oxidation of compound 5d using DMP in DCM afforded the ketone 5e with 63% yield. Compounds 5a and 5b were completely protected on phenol and carbinol functions as tribenzylethers 6a

and 6b using BnBr, NaH, NaI in DMF. Subsequently regioselective bromination of 6a furnished the mono-brominated 6c and the di-brominated 6d in quantitative yield when 1.2 or 2.4 equiv of NBS was used, respectively.

Novel polyoxygenated diarylheptanoids do not affect microglial cell viability

BV-2 microglial cells were treated with curcumin, celecoxib or the novel polyoxygenated diarylheptanoids at 0.01, 0.1 and 1 M and their cytotoxic effects were determined by MTT assay after 72 hours (Fig. S1). Curcumin and celecoxib as well as the new-synthesized diarylheptanoids exhibited minimal or null toxic effect. We chose the lowest concentration (0.01 M) as optimal concentration to evaluate the anti-inflammatory activity.

Impact of treatment with the linear polyoxygenated diarylheptanoids on IL-6, TNF-α and NF-κB

When stimulated with lipopolysaccharide, the macrophages secrete different mediators among which IL-6 and TNF-α have a primary role for the initiation and propagation of inflammation [START_REF] Singh | TNF-alpha and IL-6 inhibitors: Conjugates of N-substituted indole and aminophenylmorpholin-3-one as anti-inflammatory agents[END_REF].

Therefore, to probe the effect of the novel molecules on IL-6 and TNF-α secretion, BV-2 cells were stimulated with LPS in the presence or absence of each compound at the concentration of 0.01 M (Fig. 2). Twenty-four hours later, the levels of IL-6 and TNF-α were measured in cell culture media.

LPS induced a significant release of IL-6 (Fig. 2A; LPS vs. CONTROL, p<0.001) and TNF-α (Fig. 2B; LPS vs. CONTROL, p<0.001). Celecoxib resulted more active than curcumin in lowering IL-6 levels compared to cells activated only with LPS (Fig. 2A, ***p<0.001). The majority of the tested compounds was able to reduce the secretion of IL-6; exceptions were molecules 4a, 5a, 5c and 5d, which had no significant effect (Fig. 2A). Interestingly, compound 4b was effective as celecoxib in lowering IL-6 levels, while compounds 5e, 6c and 6d had an effect similar to curcumin. In the meantime, the diarylheptanoid 6d did not affect TNF-α release following LPS stimulation as well as compounds 4b, 4d, 5a, 5d and 5e (Fig. 2B). The remaining molecules 4a, 4f, 5c, 6b and 6c acted like celecoxib and curcumin in letting TNF-α concentration down (Fig. 2B, compounds vs. LPS, ***p<0.001).

Then we investigated the effect of the new synthesized compounds on NF-κB, a crucial transcription factor whose activation leads to the induction of multiple genes regulating the immune and the inflammatory responses [START_REF] Liu | NF-kappaB signaling in inflammation[END_REF]. Therefore, to verify if NF-κB could be a target for the polyoxygenated diarylheptanoids, LPS-triggered BV-2 cells were treated with the novel compounds, curcumin, or celecoxib. The protein levels of NF-κB subunit p65 were quantified via western blot. Surprisingly, all compounds were able to reduce the expression of NF-κB in the same manner as celecoxib and curcumin (Fig. 2C). Molecules 4d and 4f were the less active; however, they led to the reduction of about 30% in NF-κB protein levels with respect to BV-2 cells stimulated only with LPS (Fig. 2D).

Effect of the novel polyoxygenated diarylheptanoids on ACLY expression and PGE 2 , NO and ROS production

Since the new synthesized compounds reduced NF-κB expression and ACLY up-regulation in LPS-induced macrophages is under control of NF-κB transcription factor [START_REF] Infantino | ATP-citrate lyase is essential for macrophage inflammatory response[END_REF], we evaluated the protein levels of ACLY (Fig. 3A). Of note, ACLY is a metabolic enzyme -recently identified as a new player of the immunometabolism -which splits glucose-derived citrate into acetyl-CoA and oxaloacetate (OAA). Acetyl-CoA provides units for lipid elongation, including arachidonic acid, precursor of prostaglandins. OAA leads to NADPH production, necessary for NADPH oxidase and iNOS to generate ROS and NO, respectively, in LPS-activated macrophages [START_REF] Infantino | Metabolic Routes in Inflammation: The Citrate Pathway and its Potential as Therapeutic Target[END_REF]. In BV-2 cells primed with LPS, curcumin and celecoxib were able to reduce ACLY expression levels (Fig. 3A).

Among the new synthesized diarylheptanoids, the molecule 6d was the most active, even better than celecoxib, in lowering ACLY protein; on the contrary, molecules 4b, 4d and 5e had no activity. The remaining compounds were able to reduce the expression of ACLY (Fig. 3A).

Taking into consideration the inhibitory effect of ACLY by some of novel diarylheptanoids, we decided to monitor the levels of inflammatory mediators linked to the citrate pathway: PGE2, NO and ROS. When BV-2 microglial cells were activated with LPS we found a strong increase in PGE2 levels compared with untreated cells (Fig. 3B, CONTROL vs. LPS p<0.001). Celecoxib worked better than curcumin in modulating the production of PGE2, bringing the levels of PGE2 back to those of the untreated cells (Fig. 3B, CELECOXIB vs. LPS ***p<0.001). The majority of the tested diarylheptanoids acted as curcumin with the exception of compound 4d, 4f, 5a and 5e. Molecules 4f and 5a had no effect: the levels of PGE2 in BV-2 cells were similar to cells treated only with LPS. On the contrary, compound 4d was the only tested diarylheptanoid more active than curcumin but less effective than celecoxib in reducing PGE2 levels (Fig. 3B).

Then, efforts were dedicated to NO and ROS evaluation. Intense production of both ROS and NO was observed in various diseases [START_REF] Valko | Free radicals and antioxidants in normal physiological functions and human disease[END_REF] and can be correlated to neurodegenerative disorders [START_REF] Calabrese | Nitric oxide and cellular stress response in brain aging and neurodegenerative disorders: the role of vitagenes[END_REF][START_REF] Pimentel | Oxidative stress in Alzheimer's and Parkinson's diseases: insights from the yeast Saccharomyces cerevisiae[END_REF]. Celecoxib resulted more active then curcumin in lowering NO and ROS levels compared to cells activated only with LPS (Fig. 3C-D, p<0.001). The majority of the tested compounds had similar effect of curcumin with the exception of 6b and 6c, the most active in the reduction of NO with an effect similar to celecoxib (Fig. 3C, 6b, 6c vs. LPS, ***p<0.001). By contrary, all the tested polyoxygenated diarylheptanoids, except 6d, showed a higher reduction of ROS levels with respect to the leading curcumin. Compounds 4a, 4d, 5e and 6b had the strongest inhibitor effect on LPSinduced ROS production in BV-2 cells (Fig. 3D, compounds vs. LPS, ***p<0.001). Meanwhile, compound 5d was completely inactive: it even led to a significant increase in NO (Fig. 3C, 6c vs.

LPS, ***p<0.001) as well as in ROS (Fig. 3D, 6c vs. LPS, ***p<0.001) levels.

Discussion

In our investigation, we reported the prospect of new eleven linear polyoxygenated diarylheptanoids as a source of alternative anti-neuroinflammatory compounds. To this end, they were synthesized according to known methodology [START_REF] Bochicchio | Convergent total synthesis of (+/-) myricanol, a cyclic natural diarylheptanoid[END_REF] and screened in LPS-triggered BV-2 microglial cells. The tested diarylheptanoids could be classified into three class: a) with double bond (4a, 4b, 4d and 4f); b) without double bond (5a, 5c, 5d, and 5e) and c) with one or two halides on the aryl rings and completely protected on hydroxyl groups (6b, 6c and 6d).

Our findings showed that the acetylation of OHs had made more efficient compound 4d in lowering PGE2, NO and ROS levels with respect to 4a and 4b with one and two free phenolic group, respectively. Moreover, the presence of the carbonyl and the additional methyl ether in compound 4f made it with similar activity of 4b in reducing NO and ROS production and none inhibitory effect on PGE2 release. An opposite behaviour was observed in IL-6 and TNF-α secretion, where compound 4d was completely inactive while 4f had a high ability. Furthermore, molecule 4b reduced IL-6 concentration of about 30% similarly to celecoxib and 4a had a strong inhibitory effect on TNF-α secretion. From the second class of compounds (5a, 5c, 5d, 5e) it is apparent that the absence of the double bond leads to a reduction in activity. For example, compound 5d did not have any inhibitory effect of IL-6 and TNF-α release and it even led an increase in NO and ROS levels with respect to BV-2 cells activated with LPS. Beneficial effects were found with benzyl ethers derivatives (third class) and in presence of just one halide (iodine or bromine) on one aryl ring, as in 6b and 6c, respectively. These last compounds reduced the concentration of all inflammatory mediators analyzed and NF-κB and ACLY protein levels, while the presence of two bromine in the compound 6d induced loss of activity in lowering TNF-α, NO and ROS levels.

However, the compound 6d had the strongest inhibitory effect on ACLY.

The great anti-neuroinflammatory activity of the compounds 6b and 6c could be linked to their lipophilic nature and to a possible passive membrane permeability. Despite molecular weights equal to 757 and 710 Da and predicted partition coefficients, logP, of 11.88 ± 0.47 and 11.69 ± 0.59 for the molecules 6b and 6c respectively, anti-neuroinflammatory effects for compounds with similar values beyond Lipinski's Rule of 5 were recorded [START_REF] Banks | Characteristics of compounds that cross the blood-brain barrier[END_REF][START_REF] Pye | Nonclassical Size Dependence of Permeation Defines Bounds for Passive Adsorption of Large Drug Molecules[END_REF]. In addition, it has been recently demonstrated that linear diarylheptanoids with a halide atom and the benzyl ethers as protective groups on the rings have biological activity [START_REF] Motiur Rahman | Linear diarylheptanoids as potential anticancer therapeutics: synthesis, biological evaluation, and structure-activity relationship studies[END_REF].

Noteworthy, all polyoxygenated diarylheptanoids exhibited an inhibitory effect on NF-κB, transcription factor that regulates the expression of many genes involved in the inflammatory response among which IL-6, TNFα and ACLY genes [START_REF] Liu | NF-kappaB signaling in inflammation[END_REF][START_REF] Infantino | ATP-citrate lyase is essential for macrophage inflammatory response[END_REF]. Therefore, the effects exerted by the novel diarylheptanoids on these latter targets could be whether direct inhibitory effects or consequence of NF-κB inhibition.

Surprisingly, the new synthesized molecules showed anti-neuroinflammatory features at 0.01 µM, a very low concentration respect to the reported cyclic ether diarylheptanoids [START_REF] Maurent | Synthesis and biological evaluation of diarylheptanoids as potential antioxidant and antiinflammatory agents[END_REF] and respect to the natural linear diaryheptanoids [START_REF] Woo | Antiinflammatory diarylheptanoids from rhizomes of Dioscorea nipponica[END_REF] which showed anti-inflammatory and antioxidant proprieties at higher concentration, 30 µM and 13 µM, respectively.

All these results shed light on chemical groups and/or modifications that look promising to improve anti-neuroinflammatory activity. Future investigation could demonstrate whether these compounds have other molecular targets in inflammation. differences between CONTROL and LPS were highly significant (p<0.001, Student's t test). Where

Founding

  This research was supported by Funding for Basic Research (FFABR) from the Italian Ministry of Education, University and Research and French government for LC PhD fellow.

Figure 1 .

 1 Figure 1. Myricanol, curcumin, celecoxib and diarylheptanoids structures.

Figure 2 .

 2 Figure 2. Effect of polyoxygenated diarylheptanoids on IL-6 and TNF-α release and NF-κB/ p65

Figure 3 .

 3 Figure 3. Effect of polyoxygenated diarylheptanoids on ACLY expression levels and PGE 2 , NO