Document Open Access Logo

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

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

PDF
Thumbnail PDF

File

OASIcs.Gabbrielli.5.pdf
  • Filesize: 0.51 MB
  • 21 pages

Document Identifiers

Author Details

Saverio Giallorenzo
  • University of Southern Denmark, Odense, Denmark (former)
  • University of Bologna/INRIA, Italy (current)
Ivan Lanese
  • University of Bologna/INRIA, Italy
Fabrizio Montesi
  • University of Southern Denmark, Odense, Denmark
Davide Sangiorgi
  • University of Bologna/INRIA, Italy
Stefano Pio Zingaro
  • University of Bologna/INRIA, Italy

Funding

  • Montesi, Fabrizio: Partially supported by Villum Fonden (grant no. 29518).
  • Sangiorgi, Davide: Partially supported by MIUR-PRIN project "Analysis of Program Analyses" (ASPRA, ID 201784YSZ5_004).

Cite As Get BibTex

Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Davide Sangiorgi, and Stefano Pio Zingaro. The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/OASIcs.Gabbrielli.5

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 ! )

Subject Classification

ACM Subject Classification
  • Computer systems organization → Cloud computing
  • Theory of computation → Concurrency
Keywords
  • Serverless computing
  • Process calculi
  • Pi-calculus

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Davide Ancona et al. Behavioral types in programming languages. Foundations and Trends in Programming Languages, 3(2-3):95-230, 2016. Google Scholar
  2. Ioana Baldini, Paul C. Castro, Kerry Shih-Ping Chang, Perry Cheng, Stephen Fink, Vatche Ishakian, Nick Mitchell, Vinod Muthusamy, Rodric Rabbah, Aleksander Slominski, and Philippe Suter. Serverless computing: Current trends and open problems. In Sanjay Chaudhary, Gaurav Somani, and Rajkumar Buyya, editors, Research Advances in Cloud Computing, pages 1-20. Springer, 2017. URL: https://doi.org/10.1007/978-981-10-5026-8_1.
  3. Michele Boreale and Davide Sangiorgi. Some congruence properties for π-calculus bisimilarities. Theor. Computer Science, 198:159-176, 1998. Google Scholar
  4. Tomasz Brengos and Marco Peressotti. A uniform framework for timed automata. In CONCUR, volume 59 of LIPIcs, pages 26:1-26:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  5. Tomasz Brengos and Marco Peressotti. Behavioural equivalences for timed systems. Logical Methods in Computer Science, 15(1), 2019. Google Scholar
  6. Marco Carbone and Fabrizio Montesi. Deadlock-freedom-by-design: multiparty asynchronous global programming. In POPL, pages 263-274. ACM, 2013. Google Scholar
  7. Luís Cruz-Filipe and Fabrizio Montesi. A core model for choreographic programming. In FACS, Lecture Notes in Computer Science, pages 17-35. Springer, 2016. Google Scholar
  8. Mila Dalla Preda, Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, and Jacopo Mauro. Dynamic choreographies: Theory and implementation. Logical Methods in Computer Science, 13(2), 2017. Google Scholar
  9. Romain Demangeon, Daniel Hirschkoff, and Davide Sangiorgi. Termination in impure concurrent languages. In Proc. 21th Conf. on Concurrency Theory, volume 6269 of Lecture Notes in Computer Science, pages 328-342. Springer, 2010. Google Scholar
  10. Nicola Dragoni et al. Microservices: Yesterday, today, and tomorrow. In Present and Ulterior Software Engineering, pages 195-216. Springer, 2017. Google Scholar
  11. Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi. Eager functions as processes. In 33nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. IEEE Computer Society, 2018. Google Scholar
  12. Yoav Freund and Robert E Schapire. Large margin classification using the perceptron algorithm. Machine learning, 37(3):277-296, 1999. Google Scholar
  13. Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Marco Peressotti, and Stefano Pio Zingaro. No more, no less - A formal model for serverless computing. In Coordination Models and Languages - 21st International Conference, COORDINATION 2019, volume 11533 of Lecture Notes in Computer Science, pages 148-157. Springer, 2019. Google Scholar
  14. Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, and Stefano Pio Zingaro. A language-based approach for interoperability of IoT platforms. In Tung Bui, editor, 51st Hawaii International Conference on System Sciences, HICSS 2018, Hilton Waikoloa Village, Hawaii, USA, January 3-6, 2018, pages 1-10. ScholarSpace / AIS Electronic Library (AISeL), 2018. URL: http://hdl.handle.net/10125/50603.
  15. Saverio Giallorenzo, Fabrizio Montesi, and Maurizio Gabbrielli. Applied choreographies. In FORTE, Lecture Notes in Computer Science, pages 21-40. Springer, 2018. Google Scholar
  16. Saverio Giallorenzo, Fabrizio Montesi, and Marco Peressotti. Choreographies as objects. CoRR, abs/2005.09520, 2020. URL: http://arxiv.org/abs/2005.09520.
  17. Joseph M. Hellerstein et al. Serverless computing: One step forward, two steps back. In CIDR. www.cidrdb.org, 2019. Google Scholar
  18. Daniel Hirschkoff, Enguerrand Prebet, and Davide Sangiorgi. On the representation of references in the pi-calculus. In CONCUR'20, LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2020. Google Scholar
  19. Hans Hüttel et al. Foundations of session types and behavioural contracts. ACM Comput. Surv., 49(1):3:1-3:36, 2016. Google Scholar
  20. Abhinav Jangda, Donald Pinckney, Yuriy Brun, and Arjun Guha. Formal foundations of serverless computing. Proc. ACM Program. Lang., 3(OOPSLA):149:1-149:26, 2019. URL: https://doi.org/10.1145/3360575.
  21. Eric Jonas et al. Cloud programming simplified: A Berkeley view on serverless computing. Technical report, EECS Department, University of California, Berkeley, February 2019. Google Scholar
  22. Nickolas Kavantzas, David Burdett, Gregory Ritzinger, Tony Fletcher, Charlton Barreto, and Yves Lafon. Web services choreography description language version 1.0, W3C candidate recommendation. Technical report, W3C, 2005. URL: http://www.w3.org/TR/ws-cdl-10.
  23. Leslie Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput., 28(9):690-691, September 1979. Google Scholar
  24. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. Google Scholar
  25. Robin Milner. The polyadic π-calculus: a tutorial. Technical Report ECS-LFCS-91-180, LFCS, Dept. of Comp. Sci., Edinburgh Univ., October 1991. Also in Logic and Algebra of Specification, ed. F.L. Bauer, W. Brauer and H. Schwichtenberg, Springer Verlag, 1993. Google Scholar
  26. Robin Milner. Functions as processes. Math. Struct. in Computer Science, 2(2):119-141, 1992. Google Scholar
  27. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I. Inf. Comput., 100(1):1-40, 1992. URL: https://doi.org/10.1016/0890-5401(92)90008-4.
  28. Robin Milner and Davide Sangiorgi. Barbed bisimulation. In W. Kuich, editor, ICALP, volume 623 of Lecture Notes in Computer Science, pages 685-695. Springer, 1992. Google Scholar
  29. Fabrizio Montesi. Choreographic Programming. Ph.D. Thesis, IT University of Copenhagen, 2013. URL: http://www.fabriziomontesi.com/files/choreographic_programming.pdf.
  30. Fabrizio Montesi, Claudio Guidi, and Gianluigi Zavattaro. Service-oriented programming with Jolie. In Athman Bouguettaya, Quan Z. Sheng, and Florian Daniel, editors, Web Services Foundations, pages 81-107. Springer, 2014. URL: https://doi.org/10.1007/978-1-4614-7518-7_4.
  31. Joachim Niehren, Jan Schwinghammer, and Gert Smolka. A concurrent lambda calculus with futures. Theor. Comput. Sci., 364(3):338-356, 2006. Google Scholar
  32. Christos H. Papadimitriou. The serializability of concurrent database updates. J. ACM, 26(4):631-653, 1979. Google Scholar
  33. Benjamin Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. Math. Struct. in Computer Science, 6(5):409-454, 1996. Google Scholar
  34. Frank Rosenblatt. The perceptron: a probabilistic model for information storage and organization in the brain. Psychological review, 65(6):386, 1958. Google Scholar
  35. Mark Sandler, Andrew Howard, Menglong Zhu, Andrey Zhmoginov, and Liang-Chieh Chen. MobileNetV2: Inverted Residuals and Linear Bottlenecks. In 2018 IEEE/CVF Conference on Computer Vision and Pattern Recognition, pages 4510-4520. IEEE, 2018. URL: https://doi.org/10.1109/CVPR.2018.00474.
  36. Davide Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis CST-99-93, Department of Computer Science, University of Edinburgh, 1992. Google Scholar
  37. Davide Sangiorgi. An investigation into functions as processes. In Proc. Math. Foundations of Programming Semantics, volume 802 of Lecture Notes in Computer Science, pages 143-159. Springer, 1993. Google Scholar
  38. Davide Sangiorgi. The name discipline of uniform receptiveness. Theoretical Computer Science, 221:457-493, 1999. Google Scholar
  39. Davide Sangiorgi. Typed π-calculus at work: a correctness proof of Jones’s parallelisation transformation on concurrent objects. Theory and Practice of Object Systems, 5(1):25-34, 1999. Google Scholar
  40. Davide Sangiorgi. Termination of processes. Math. Struct. in Computer Science, 16(1):1-39, 2006. Google Scholar
  41. Davide Sangiorgi and David Walker. The Pi-Calculus - a theory of mobile processes. Cambridge University Press, 2001. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact