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

Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Davide Sangiorgi, Stefano Pio Zingaro [2020].
In proceedings of Gabbrielli's Festschrift 2020, pp. 5:1-5:21.

Abstract

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.

Links

doi.org

Additional notes

None

Cite (BibTeX)

Click to expand

@inproceedings{DBLP:conf/birthday/GiallorenzoLMSZ20,
  author       = {Saverio Giallorenzo and
                  Ivan Lanese and
                  Fabrizio Montesi and
                  Davide Sangiorgi and
                  Stefano Pio Zingaro},
  editor       = {Frank S. de Boer and
                  Jacopo Mauro},
  title        = {The Servers of Serverless Computing: {A} Formal Revisitation of Functions
                  as a Service},
  booktitle    = {Recent Developments in the Design and Implementation of Programming
                  Languages, Gabbrielli's Festschrift, November 27, 2020, Bologna, Italy},
  series       = {OASIcs},
  volume       = {86},
  pages        = {5:1--5:21},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2020},
  url          = {https://doi.org/10.4230/OASIcs.Gabbrielli.5},
  doi          = {10.4230/OASICS.GABBRIELLI.5},
  timestamp    = {Sat, 30 Sep 2023 09:35:34 +0200},
  biburl       = {https://dblp.org/rec/conf/birthday/GiallorenzoLMSZ20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

A PDF is available (possibly a preprint):