License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.Gabbrielli.5
URN: urn:nbn:de:0030-drops-132271
URL: https://drops.dagstuhl.de/opus/volltexte/2020/13227/
Go to the corresponding OASIcs Volume Portal


Giallorenzo, Saverio ; Lanese, Ivan ; Montesi, Fabrizio ; Sangiorgi, Davide ; Zingaro, Stefano Pio

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

pdf-format:
OASIcs-Gabbrielli-5.pdf (0.5 MB)


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. Dedicated to Maurizio Gabbrielli, on his 60th birthday (... rob da mët ! )

BibTeX - Entry

@InProceedings{giallorenzo_et_al:OASIcs:2020:13227,
  author =	{Saverio Giallorenzo and Ivan Lanese and Fabrizio Montesi and Davide Sangiorgi and Stefano Pio Zingaro},
  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},
  pages =	{5:1--5:21},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{Frank S. de Boer and Jacopo Mauro},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13227},
  URN =		{urn:nbn:de:0030-drops-132271},
  doi =		{10.4230/OASIcs.Gabbrielli.5},
  annote =	{Keywords: Serverless computing, Process calculi, Pi-calculus}
}

Keywords: Serverless computing, Process calculi, Pi-calculus
Collection: Recent Developments in the Design and Implementation of Programming Languages
Issue Date: 2020
Date of publication: 27.11.2020


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI