Top

Published in:

2019 | OriginalPaper | Chapter

No More, No Less

A Formal Model for Serverless Computing

Authors : Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Marco Peressotti, Stefano Pio Zingaro

Published in: Coordination Models and Languages

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Serverless computing, also known as Functions-as-a-Service, is a recent paradigm aimed at simplifying the programming of cloud applications. The idea is that developers design applications in terms of functions, which are then deployed on a cloud infrastructure. The infrastructure takes care of executing the functions whenever requested by remote clients, dealing automatically with distribution and scaling with respect to inbound traffic.

While vendors already support a variety of programming languages for serverless computing (e.g. Go, Java, Javascript, Python), as far as we know there is no reference model yet to formally reason on this paradigm. In this paper, we propose the first core formal programming model for serverless computing, which combines ideas from both the \(\lambda \)-calculus (for functions) and the \(\pi \)-calculus (for communication). To illustrate our proposal, we model a real-world serverless system. Thanks to our model, we capture limitations of current vendors and formalise possible amendments.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Bridging the Gap Between Supervisory Control and Coordination of Services: Synthesis of Orchestrations and Choreographies

next chapter Verification of Concurrent Design Patterns with Data

We omit the name of the function called by

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-22397-7_9/MediaObjects/478673_1_En_9_Figbf_HTML.gif

, excluded in the excerpt of Fig. 2.

More involved variants of the database are possible. E.g. to avoid clashes among services using the same key for different elements, we can either use scoping or prefix key names with service names—e.g. Tailor uses service-specific tables in DynamoDB.

Williams, A.: Tailor - the AWS Account Provisioning Service. https://github.com/alanwill/aws-tailor. Accessed Feb 2019

Ancona, D., et al.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2–3), 95–230 (2016)CrossRef

Apache: OpenWhisk. https://github.com/apache/incubator-openwhisk. Accessed Feb 2019

AWS: Lambda. https://aws.amazon.com/lambda/. Accessed Feb 2019

Baker Jr., H.C., Hewitt, C.: The incremental garbage collection of processes. ACM Sigplan Not. 12(8), 55–59 (1977)CrossRef

Baldini, I., et al.: Serverless computing: current trends and open problems. In: Chaudhary, S., Somani, G., Buyya, R. (eds.) Research Advances in Cloud Computing, pp. 1–20. Springer, Singapore (2017). https://doi.org/10.1007/978-981-10-5026-8_1CrossRef

Brengos, T., Peressotti, M.: A uniform framework for timed automata. In: CONCUR. LIPIcs, vol. 59, pp. 26:1–26:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)

Brengos, T., Peressotti, M.: Behavioural equivalences for timed systems. Log. Methods Comput. Sci. 15(1), 17:1–17:41 (2019)MathSciNetMATH

Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: POPL, pp. 263–274. ACM (2013)CrossRef

10.

Cruz-Filipe, L., Montesi, F.: A core model for choreographic programming. In: Kouchnarenko, O., Khosravi, R. (eds.) FACS 2016. LNCS, vol. 10231, pp. 17–35. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57666-4_3CrossRef

11.

Dalla Preda, M., et al.: Dynamic choreographies: theory and implementation. Log. Methods Comput. Sci. 13(2), 1–57 (2017)MathSciNetMATH

12.

Dragoni, N., et al.: Microservices: yesterday, today, and tomorrow. Present and Ulterior Software Engineering, pp. 195–216. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67425-4_12CrossRef

13.

Ecmascript 2018 language specification. http://ecma-international.org/ecma-262/9.0/index.html. Accessed Feb 2019

14.

Giallorenzo, S., Montesi, F., Gabbrielli, M.: Applied choreographies. In: Baier, C., Caires, L. (eds.) FORTE 2018. LNCS, vol. 10854, pp. 21–40. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-92612-4_2CrossRef

15.

Goetz, B., et al.: Java Concurrency in Practice. Pearson Education, London (2006)

16.

Google: Cloud Functions. https://cloud.google.com/functions. Accessed Feb 2019

17.

Halstead Jr., R.H.: Multilisp: a language for concurrent symbolic computation. ACM Trans. Program. Languages Syst. (TOPLAS) 7(4), 501–538 (1985)CrossRef

18.

Hellerstein, J.M., et al.: Serverless computing: one step forward, two steps back. In: CIDR (2019). www.cidrdb.org

19.

Hendrickson, S., et al.: Serverless computation with OpenLambda. In: USENIX. USENIX Association (2016)

20.

Hüttel, H., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3:1–3:36 (2016)CrossRef

21.

IBM: Cloud Functions. https://www.ibm.com/cloud/functions. Accessed Feb 2019

22.

Iron.io: IronFunctions. https://open.iron.io. Accessed Feb 2019

23.

Jangda, A., et al.: Formal foundations of serverless computing. CoRR abs/1902.05870 (2019). arXiv:1902.05870

24.

Jonas, E., et al.: Cloud programming simplified: a berkeley view on serverless computing. Technical report, EECS Department, University of California, Berkeley, Feburary 2019

25.

K-Optional Software: serverless out of Control. https://koptional.com/2019/01/22/serverless-out-of-control/. Accessed Feb 2019

26.

Kavantzas, N., Burdett, D., Ritzinger, G., Lafon, Y.: Web services choreography description language version 1.0, W3C candidate recommendation. Technical report, W3C (2005). http://www.w3.org/TR/ws-cdl-10

27.

Kevin Vandenborne: serverless: a lesson learned. The hard way. https://sourcebox.be/blog/2017/08/07/serverless-a-lesson-learned-the-hard-way/. Accessed Feb 2019

28.

Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690–691 (1979)CrossRef

29.

Microsoft: Azure Functions. https://azure.microsoft.com/services/functions. Accessed Feb 2019

30.

Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). https://doi.org/10.1007/3-540-10235-3CrossRefMATH

31.

Montesi, F.: Kickstarting choreographic programming. In: Hildebrandt, T., Ravara, A., van der Werf, J.M., Weidlich, M. (eds.) WS-FM 2014-2015. LNCS, vol. 9421, pp. 3–10. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33612-1_1CrossRef

32.

Niehren, J., Schwinghammer, J., Smolka, G.: A concurrent lambda calculus with futures. Theor. Comput. Sci. 364(3), 338–356 (2006)MathSciNetCrossRef

33.

Papadimitriou, C.H.: The serializability of concurrent database updates. J. ACM 26(4), 631–653 (1979)MathSciNetCrossRef

34.

Sangiorgi, D., Walker, D.: The Pi-Calculus - A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)MATH

35.

Summerfield, M.: Python in Practice: Create Better Programs Using Concurrency, Libraries, and Patterns. Addison-Wesley, Reading (2013)

36.

Wright, T.: Beware “RunOnStartup” in Azure Functions – a serverless horror story. http://blog.tdwright.co.uk/2018/09/06/beware-runonstartup-in-azure-functions-a-serverless-horror-story/. Accessed Feb 2019

37.

Williams, A.: C++ Concurrency in Action. Manning, New York (2017)

Title: No More, No Less
Authors: Maurizio Gabbrielli
Saverio Giallorenzo
Ivan Lanese
Fabrizio Montesi
Marco Peressotti
Stefano Pio Zingaro
Publisher: Springer International Publishing
Book: Coordination Models and Languages
Print ISBN: 978-3-030-22396-0

Electronic ISBN: 978-3-030-22397-7

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-22397-7_9

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner