Serverless Computing is a recent approach to cloud computing that provides programmers an interface to run functions on the cloud. Programmers does not have to think about resource allocation, or even configure the runtime environment. The serverless platform takes care of automatically managing dependencies, compiles code, allocates processor and RAM. With this model, programmers only need to focus on the application code. Recently several serverless platforms have appeared and some of the popular ones are: Microsoft Azure, Google Cloud Functions, Amazon AWS Lambda, and Apache OpenWhisk.
Unfortunately, writing correct serverless platforms and using this abstraction in the application, programmers need to know about low-level details of these serverless platforms. For example, when the deployed function is called from an application, the serverless platforms does not ensure that the function will be called right away. Instead the function can be called after any time. Another example is when the serverless platform fails to execute the function. In short, "Serverless Functions are not like ordinary functions". The programmer has to handle these cases in the application.
In this project, we developed operational semantics for serverless computing, λ. λ formalizes the internals of a serverless platform. λ describes the low-level behaviors of these serverless platforms, that includes failures, concurremcy, function restarts, and instance reuse. Programmers can use these semantics to guide the development of programming tools and extensions to serverless platforms.
To know more about our work checkout our paper Formal Foundations of Serverless Computing.