No More, No Less

Serverless computing [24], also known as Functions-as-a-Service, narrows the development of Cloud applications to the definition and composition of stateless functions, while the provider handles the deployment, scaling, and balancing of the host infrastructure. Hence, although a bit of a misnomer—as servers are of course involved—the “less” in serverless refers to the removal of some server-related concerns, namely, their maintenance, scaling, and expenses related to a sub-optimal management (e.g. idle servers). Essentially, serverless pushes to the extreme the per-usage model of Cloud Computing: in serverless, users pay only for the computing resources used at each function invocation. This is why recent reports [18, 24] address serverless computing as the actual realisation of the long-standing promise of the Cloud to deliver computation as a commodity. AWS Lambda [4], launched in 2014, is the first and most widely-used serverless implementation, however many players like Google, Microsoft, Apache, IBM, and also open-source communities recently joined the serverless market [3, 16, 19, 21, 22, 29]. Current serverless proposals support the definition of functions—written in mainstream languages such as Go, Java, Javascript or Python—activated by specific events in the system, like a user request to a web gateway, the delivery of content from a message broker or a notification from a database. The serverless infrastructure transparently handles the instantiation of functions, as well as monitoring, logging, and fault tolerance.

Serverless offerings have become more and more common, yet the technology is still in its infancy and presents limitations [6, 18, 24] which hinder its wide adoption. For example, current serverless implementations favour operational flexibility (asynchrony and scalability) over developer control (function composition). Concretely, they do not support the direct composition of functions, which must call some stateful service in the infrastructure (e.g. a message broker) which will take care of triggering an event bound to the callee. On the one hand, that limitation is beneficial, since programmers must develop their functions as highly fine-grained, re-usable components (reminiscent of service-oriented architectures and microservices [12]). On the other hand, such openness and fine granularity increases the complexity of the system: programmers cannot assume sequential consistency or serialisability among their functions, which complicates reasoning on the semantics of the transformations applied to the global state of their architecture. This holds true also when estimating resource usage/costs, due to the complexity of unfolding all possible concurrent computations.

The above criticisms pushed us to investigate a core calculus for serverless computing, to reason on the paradigm, to model desirable features of future implementations, and to formalise guarantees over programs. In Sect. 2 we introduce the Serverless Kernel Calculus (SKC); as far as we know, the first core formal model for serverless computing. SKC combines ideas from both the \(\lambda \)-calculus (for functions) and the \(\pi \)-calculus (for communication). In Sect. 2, we also extend SKC to capture limitations of current serverless implementations. In Sect. 3 we use our extension to model a real-world serverless architecture [1], implemented on AWS Lambda. Finally, in Sect. 4 we discuss future developments of SKC.

Our kernel calculus defines a serverless architecture as a pair , where S is the system of running functions and \(\mathcal D\) is a definition repository, containing function definitions. The repository \(\mathcal D\) is a partial function from function names to function bodies M. M includes function application ( ), asynchronous execution of new functions ( ), function names , and values V. Values include variables , \(\lambda \)-abstractions , named futures [5, 17, 32] , and the unit value . A system S contains running functions , where c will contain the result of the computation of the function M. Systems can be composed in parallel \(\mathbin {\texttt {|}}\) and include the empty system . Futures can be restricted in systems via \(\mathop {\nu c}S\).

We assume futures to appear only at runtime and not in initial systems. Moreover, we consider a standard structural congruence \(\equiv \) that supports changing the scope of restrictions to avoid name capture, and where parallel composition is associative, commutative, and has as neutral element.

We define the semantics of our calculus using evaluation contexts \(\mathcal {E}\) and \(\mathcal {E}_{\lambda }\), to evaluate, respectively, systems and functions.

SKC reduction semantics.

Full size image

We report in Fig. 1 the semantics of serverless architectures , expressed as reduction rules. Rule is the traditional function application of \(\lambda \)-calculus. Rule retrieves the body of function from the definition repository \(\mathcal {D}\). Rule models the execution of new functions: it creates a fresh future c and, in parallel, it executes function M so that c will store the evaluation of M. When the evaluation of a function reduces to a value, rule returns the value to the associated future and removes both the terminated function and its restriction. Rules , and perform the closure under, respectively, structural congruence, restriction, and parallel composition. We include in SKC standard components (conditionals, etc.) and extend evaluation contexts (\(\mathcal {E}\)) accordingly:

We define standard macros for and declarations, and pairs.

2.1 SKC\(_\sigma \) - A Stateful Extension of SKC

SKC considers static definition repositories, i.e. no rules mutate the state of \(\mathcal {D}\). We now present SKC\(_\sigma \), an extension of SKC which includes two primitives to define transformations on definition repositories. As shown in Sect. 3, SKC\(_\sigma \) is powerful enough to encode stateful services, like databases and message queues.

The first primitive included in SKC\(_\sigma \) is , which updates the definition repository \(\mathcal {D}\) to map to M: users can use the primitive to deploy new function definitions or update/override existing ones. The second primitive is , which removes the definition of from \(\mathcal {D}\), returning it to the caller. We report below the semantics of the new primitives.

The only restriction on the application of rule is that the body M of the newly deployed function does not contain futures (futures(M) is the set of futures occurring in M). This preserves the semantics of restriction of futures in function evaluations (cf. rules and ). In the reductum, the rule returns the name of the deployed function, useful to invoke it in the continuation. Rule removes the definition M of a deployed function . For simplicity, we define applicable only if is defined. In the reductum, the caller of the obtains the declaration of the function (useful for internal application) while the association for is removed from \(\mathcal D\) by function \(\texttt {undef}\).

2.2 SKC\(_{\mathtt e}\) - Event-Based Function Composition in SKC

We present an idiom of SKC, called SKC\(_{\mathtt {e}}\), which models event-based function composition. SKC\(_{\mathtt e}\) captures one of the main limitations of current serverless vendors: the lack of support for direct function invocation, replaced by an event-handling/event-triggering invocation model. Indeed, current serverless implementations, such as AWS Lambda, work as follows: they include infrastructural stateful services, such as API gateways, that we can model using our stateful extension SKC\(_{\mathtt \sigma }\), and these services throw events. User-defined functions are invoked as handlers of these events. User-defined functions can then invoke the infrastructural services above. Notably, a user-defined function cannot directly invoke another user-defined function. We will see an instance of the event-based pattern in Sect. 3, while we describe below event handling mechanisms.

We model events ( and variations thereof) inside SKC as function names associated with peculiar function bodies in the repository \(\mathcal {D}\) that asynchronously evaluate the corresponding event handler and discard the handler result. For convenience, (i) we package the asynchronous call of an event handler in the helper function below (hereafter, we assume that \(\mathcal {D}\) contains ) and (ii) we write for unused variable symbols in binding constructs.

Event is defined in \(\mathcal D\) as and its event handler as ; we wrap the name in a lambda abstraction to avoid expansion (via ) since function names are not values. Raising an event with some parameter results in asynchronously executing the corresponding handler, as shown by the derivation below (we abbreviate as and label reductions with the names of the most relevant applied rules).

Scheme of the Autodesk Tailor system. Top, excerpt considered in the example. Bottom, full architecture (circled elements belong to the excerpt).

Full size image

Let SKC\(_{\sigma \mathtt e}\) be the compound of SKC\(_\sigma \) and SKC\(_{\mathtt e}\) presented in Sect. 2. Here, we illustrate how SKC\(_{\sigma {\mathtt e}}\) can capture real-world serverless systems by encoding a relevant portion (depicted in Fig. 2) of Tailor [1], an architecture for user registration, developed by Autodesk over AWS Lambda. Tailor mixes serverless functions with vendor-specific services: API Gateways, key-value databases (DynamoDB), and queue-based notification services (SNS). In the architecture, each function defines a fragment of the logic of a user-registration procedure, like the initiation of registration requests ( ), request validation ( ), etc. To model Fig. 2 in , first, we install in \(\mathcal {D}\) the event handlers for the API Gateway, the DynamoDB, and SNS services^{Footnote 1}:

Then, we define the functions called by the handlers installed above, using the same names of the AWS Lambda functions in Fig. 2. Handler calls function , which validates the request and inserts the information of the user in the key/value database. For brevity, we omit the behaviour of in case of invalid requests and the definition of auxiliary functions in \(\mathcal D\):

Handler invokes function , which retrieves from the database the of task , checks if it is complete, and sends a notification on SNS. We omit the definitions of functions and and of the branch.

We conclude illustrating the definitions of functions , and in \(\mathcal D\), which exemplify how SKC\(_{\sigma \mathtt {e}}\) can encode stateful, event-triggering services. Keys are represented as function names and values are stored in \(\mathcal {D}\); thus keys are passed around wrapped in lambda abstractions ( ) as done for events.

Function takes a key (wrapped as ) and a value as parameters, writes on the database by to the body of a function called , and notifies the write, invoking ^{Footnote 2}. Function simply unwraps the key thus enabling retrieval from \(\mathcal {D}\). Similarly to , function publishes ( ) a message on an SNS topic (represented as a function name) and triggers .

Remark 3.1

The example illustrates how SKC can capture (but not be restricted by) one of the most prominent limitations of current serverless platform [18], i.e. that i) user-defined functions can be only invoked by raising an event that executes a new function (as done by , using the primitive) and ii) functions can invoke other functions only by interacting with some event-triggering infrastructural service (e.g. a database, represented by function , or a notification queue, represented by function ).

We propose SKC, the first core formal model to reason on serverless computing. While the design of SKC strives for minimality, it captures the main ingredients [18, 24] of serverless architectures: (i) the deployment and instantiation of event-triggered, stateless functions and (ii) the desiderata of direct function-to-function invocation based on futures—in Sect. 3 we show how this mechanism is powerful enough to cover also the current setting of serverless vendors, where function invocation must rely on third-party services that handle event triggering.

Futures [5, 17], which are the main communication mechanism in SKC, are becoming one of the de-facto standards in asynchronous systems [13, 15, 35, 37]. We considered using named channels (as in CCS/\(\pi \)-calculus [30, 34]) instead of futures, but we found them too general for the needs of the serverless model (they are bi-directional and re-usable). Besides, futures can encode channels [32].

The work closest to ours is [23], appeared during the submission of this work, in the form of a technical report. It presents a detailed operational semantics that captures the low-level details of current serverless implementations (e.g. cold/warm components, storage, and transactions are primitive features of their model) whereas SKC identifies a kernel model of serverless computing. Another work close to SKC is [32], where the authors introduce a \(\lambda \)-calculus with futures. Since the aim of [32] 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 encode safe non-deterministic concurrent operations, which can be encoded as macros in SKC. An interesting research direction is to investigate which results from [23, 32] can be adapted to SKC.

Being the first core framework to reason on serverless architectures, SKC opens multiple avenues of future research. For example, current serverless technologies offer little guarantee on sequential execution across functions, which compels the investigation of new tools to enforce sequential consistency [28] or serialisability [33] of the transformations of the global state [18]. That challenge can be tackled developing static analysis techniques and type disciplines [2, 20] for SKC. Another direction concerns programming models, which should give to programmers an overview over the overall logic of the distributed functions and capture the loosely-consistent execution model of serverless [18]. Choreographic Programming [10, 31] is a promising candidate for that task, as choreographies are designed to capture the global interactions in distributed systems [26], and recent results [9, 11, 14] confirmed their applicability to microservices [12], a neighbouring domain to that of serverless architectures. Other possible research directions, that we do not discuss for space constraints, include monitoring, various kinds of security analysis including “self-DDoS attacks” [25, 27, 36] and performance analysis. This last one is particularly relevant in the per-usage model of serverless architectures, yet requires to extend SKC with an explicit notion of time in order to support quantitative behavioural reasoning for timed systems [7, 8].