Formal Foundations of Serverless Computing

Serverless functions are super convenient, but the underlying cloud platforms (such as AWS Lambda) nondeterministically reuse or restart the containers inside of which code is run, leading to bugs in real-world code. Documentation and online tutorials offer spotty guidance on what exactly this behavior is, and how a programmer can guarantee their code is safe. We help explain these dynamics by building a framework for analyzing the semantics of serverless functions, which others built on when designing richer serverless abstractions, such as Microsoft Azure’s Durable Functions. This work was presented at OOPSLA 2019, and received a distinguished paper award.