Formal Foundations of Serverless Computing
by Abhinav Jangda, Donald Pinckney, Yuriy Brun, Arjun Guha
Abstract:

Serverless computing (also known as functions as a service) is a new cloud computing abstraction that makes it easier to write robust, large-scale web services. In serverless computing, programmers write what are called serverless functions, and the cloud platform transparently manages the operating system, resource allocation, load-balancing, and fault tolerance. When demand for the service spikes, the platform automatically allocates additional hardware to the service and manages load-balancing; when demand falls, the platform silently deallocates idle resources; and when the platform detects a failure, it transparently retries affected requests. In 2014, Amazon Web Services introduced the first serverless platform, AWS Lambda, and similar abstractions are now available on all major cloud computing platforms.

Unfortunately, the serverless computing abstraction exposes several low-level operational details that make it hard for programmers to write and reason about their code. This paper sheds light on this problem by presenting $\lambda_\lambda$, an operational semantics of the essence of serverless computing. Despite being a small (half a page) core calculus, $\lambda_\lambda$ models all the low-level details that serverless functions can observe. To show that $\lambda_\lambda$ is useful, we present three applications. First, to ease reasoning about code, we present a simplified $\lambda_\lambda$ semantics of serverless execution and precisely characterize when the $\lambda_\lambda$ semantics and $\lambda_\lambda$ coincide. Second, we augment $\lambda_\lambda$ with a key-value store to allow reasoning about stateful serverless functions. Third, since a handful of serverless platforms support serverless function composition, we show how to extend $\lambda_\lambda$ with a composition language. We have implemented this composition language and show that it outperforms prior work.

Citation:
Abhinav Jangda, Donald Pinckney, Yuriy Brun, and Arjun Guha, Formal Foundations of Serverless Computing, Proceedings of the ACM on Programming Languages (PACMPL) Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) issue, vol. 3, October 2019, pp. 149:1–149:26 (ACM SIGPLAN Distinguished Paper Award).
Bibtex:
@article{Jangda19oopsla,
  author = {Abhinav Jangda and Donald Pinckney and Yuriy Brun and Arjun Guha},
  title =
  {\href{http://people.cs.umass.edu/brun/pubs/pubs/Jangda19oopsla.pdf}{Formal Foundations of Serverless Computing}},
  journal = {Proceedings of the ACM on Programming Languages (PACMPL) Object-Oriented Programming, Systems, Languages, and Applications
  (OOPSLA) issue},
  venue = {OOPSLA},
  volume = {3},
  pages = {149:1--149:26},
  address = {Athens, Greece},
  month = {October},
  date = {20--25},
  year = {2019},
  issn = {2475-1421},

  doi = {10.1145/3360575},
  note = {ACM SIGPLAN Distinguished Paper Award.
  \href{https://doi.org/10.1145/3360575}{DOI: 10.1145/3360575}},
  comment = {<span class="emphasis">ACM SIGPLAN Distinguished Paper Award</span>},

  accept = {$\frac{72}{201} \approx 35\%$},

  abstract = {<p>Serverless computing (also known as functions as a service) is a new cloud
  computing abstraction that makes it easier to write robust, large-scale web
  services. In serverless computing, programmers write what are called
  serverless functions, and the cloud platform transparently manages the
  operating system, resource allocation, load-balancing, and fault tolerance.
  When demand for the service spikes, the platform automatically allocates
  additional hardware to the service and manages load-balancing; when demand
  falls, the platform silently deallocates idle resources; and when the
  platform detects a failure, it transparently retries affected requests. In
  2014, Amazon Web Services introduced the first serverless platform, AWS
  Lambda, and similar abstractions are now available on all major cloud
  computing platforms.</p>
  <p>Unfortunately, the serverless computing abstraction exposes several low-level
  operational details that make it hard for programmers to write and reason
  about their code. This paper sheds light on this problem by presenting
  $\lambda_\lambda$, an operational semantics of the essence of serverless
  computing. Despite being a small (half a page) core calculus,
  $\lambda_\lambda$ models all the low-level details that serverless functions
  can observe. To show that $\lambda_\lambda$ is useful, we present three
  applications. First, to ease reasoning about code, we present a simplified
  $\lambda_\lambda$ semantics of serverless execution and precisely
  characterize when the $\lambda_\lambda$ semantics and $\lambda_\lambda$
  coincide. Second, we augment $\lambda_\lambda$ with a key-value store to
  allow reasoning about stateful serverless functions. Third, since a handful
  of serverless platforms support serverless function composition, we show how
  to extend $\lambda_\lambda$ with a composition language. We have implemented
  this composition language and show that it outperforms prior work.</p>},
  
  fundedBy = {CNS-1413985, NSF CCF-1453474, NSF CNS-1513055},
}