research-article

Open access

Formal foundations of serverless computing

Authors:

Abhinav Jangda,

Donald Pinckney,

Arjun GuhaAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue OOPSLA

Article No.: 149, Pages 1 - 26

https://doi.org/10.1145/3360575

Published: 10 October 2019 Publication History

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, which are programs that respond to external events. When demand for the serverless function spikes, the platform automatically allocates additional hardware 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 λ_λ, an operational semantics of the essence of serverless computing. Despite being a small (half a page) core calculus, λ_λ models all the low-level details that serverless functions can observe. To show that λ_λ is useful, we present three applications. First, to ease reasoning about code, we present a simplified naive semantics of serverless execution and precisely characterize when the naive semantics and λ_λ coincide. Second, we augment λ_λ 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 λ_λ with a composition language and show that our implementation can outperform prior work.

Supplementary Material

a149-jangda (a149-jangda.webm)

Presentation at OOPSLA '19

Download
87.85 MB

References

[1]

Istemi Ekin Akkus, Ruichuan Chen, Ivica Rimac, Manuel Stein, Klaus Satzke, Andre Beck, Paarijaat Aditya, and Volker Hilt. 2018. SAND: Towards High-Performance Serverless Computing. In USENIX Annual Technical Conference (ATC).

[2]

Kalev Alpernas, Cormac Flanagan, Sadjad Fouladi, Leonid Ryzhyk, Mooly Sagiv, Thomas Schmitz, and Keith Winstein. 2018. Secure Serverless Computing Using Dynamic Information Flow Control. Proceedings of the ACM on Programming Languages 2, OOPSLA (Oct. 2018).

Digital Library

[3]

Amazon 2018. AWS Lambda Developer Guide: Invoke. https://docs.aws.amazon.com/lambda/latest/dg/API_Invoke.html . Accessed Jul 5 2018.

[4]

Lixiang Ao, Liz Izhikevich, Geoffrey M. Voelker, and George Porter. 2018. Sprocket: A Serverless Video Processing Framework. In ACM Symposium on Cloud Computing (SOCC).

Digital Library

[5]

Austin Aske and Xinghui Zhao. 2018. Supporting Multi-Provider Serverless Computing on the Edge. In International Conference on Parallel Processing (ICPP) .

[6]

Alexander Bakst, Klaus v. Gleissenthall, Rami Gökhan K, and Ranjit Jhala. 2017. Verifying Distributed Programs via Canonical Sequentialization. In ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages and Applications (OOPSLA) .

Digital Library

[7]

Ioana Baldini, Perry Cheng, Stephen J. Fink, Nick Mitchell, Vinod Muthusamy, Rodric Rabbah, Philippe Suter, and Olivier Tardieu. 2017. The Serverless Trilemma: Function Composition for Serverless Computing. In ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!) .

[8]

Guillaume Baudart, Julian Dolby, Evelyn Duesterwald, Martin Hirzel, and Avraham Shinnar. 2018. Protecting Chatbots from Toxic Content. In ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software .

Digital Library

[9]

Phil Bernstein, Sergey Bykov, Alan Geller, and Jorgen Thelin. 2014. Orleans: Distributed Virtual Actors for Programmability and Scalability . Technical Report. https://www.microsoft.com/en-us/research/publication/orleans-distributed-virtualactors-for-programmability-and-scalability/

[10]

Mathias Björkqvist, Robert Birke, and Walter Binder. 2016. Resource management of replicated service systems provisioned in the cloud. In Network Operations and Management Symposium (NOMS).

Digital Library

[11]

Oliver Bračevac, Sebastian Erdweg, Guido Salvaneschi, and Mira Mezini. 2016. CPL: A Core Language for Cloud Computing. In Proceedings of the 15th International Conference on Modularity.

Digital Library

[12]

Tej Chajed, Frans Kaashoek, Butler Lampson, and Nickolai Zeldovich. 2018. Verifying concurrent software using movers in CSPEC. In USENIX Symposium on Operating Systems Design and Implementation (OSDI).

[13]

Sarah Conway. 2017. Cloud Native Technologies Are Scaling Production Applications. https://www.cncf.io/blog/2017/12/ 06/cloud-native-technologies-scaling-production-applications/ . Accessed Jul 12 2018.

[14]

Ankush Desai, Amar Phanishayee, Shaz Qadeer, and Sanjit A. Seshia. 2018. Compositional Programming and Testing of Dynamic Distributed Systems. In ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages and Applications (OOPSLA) .

[15]

Cezara Drăgoi, Thomas A. Henzinger, and Damien Zufferey. 2016. PSync: A Partially Synchronous Language for Faulttolerant Distributed Algorithms. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).

[16]

Alex Ellis. 2018. OpenFaaS. https://www.openfaas.com . Accessed Jul 5 2018.

[17]

Matthias Felleisen and Daniel P. Friedman. 1986. Control Operators, the SECD-Machine, and the λ-Calculus. In Proceedings of the IFIP TC 2/WG 2.2 Working Conference on Formal Description of Programming Concepts .

[18]

Jeffery Fischer, Rupak Majumdar, and Shahram Esmaeilsabzali. 2012. Engage: A Deployment Management System. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) .

Digital Library

[19]

Sadjad Fouladi, Francisco Romero, Dan Iter, Qian Li, Shuvo Chatterjee, Christos Kozyrakis, Matei Zaharia, and Keith Winstein. 2019. From Laptop to Lambda: Outsourcing Everyday Jobs to Thousands of Transient Functional Containers.

[20]

Sadjad Fouladi, Riad S. Wahby, Brennan Shacklett, Karthikeyan Vasuki Balasubramaniam, William Zeng, Rahul Bhalerao, Anirudh Sivaraman, George Porter, and Keith Winstein. 2017. Encoding, Fast and Slow: Low-Latency Video Processing Using Thousands of Tiny Threads. In USENIX Symposium on Networked System Design and Implementation (NSDI).

[21]

José Fragoso Santos, Petar Maksimović, Daiva Naudži¯unien˙e, Thomas Wood, and Philippa Gardner. 2018. JaVerT: JavaScript verification toolchain. Proceedings of the ACM on Programming Languages 2, POPL (2018), 50:1–50:33.

[22]

Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Marco Peressotti, and Stefano Pio Zingaro. 2019. No More, No Less - A Formal Model for Serverless Computing. In Coordination Models and Languages (COORDINATION). 148–157.

[23]

Yu Gan and Christina Delimitrou. 2018. The Architectural Implications of Cloud Microservices. In Computer Architecture Letters (CAL) .

[24]

Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford. 2017. Verifying Strong Eventual Consistency in Distributed Systems. In ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages and Applications (OOPSLA) .

[25]

Google 2018a. Cloud Functions Execution Environment. https://cloud.google.com/functions/docs/concepts/exec . Accessed Jul 5 2018.

[26]

Google 2018b. Google Cloud Functions. https://cloud.google.com/functions/ . Accessed Jul 5 2018.

[27]

Arjun Guha, Mark Reitblatt, and Nate Foster. 2013. Machine Verified Network Controllers. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) .

[28]

Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. 2015. IronFleet: Proving Practical Distributed Systems Correct. In ACM Symposium on Operating Systems Principles (SOSP) .

Digital Library

[29]

Scott Hendrickson, Stephen Sturdevant, Tyler Harter, Venkateshwaran Venkataramani, Andrea C. Arpaci-Dusseau, and Remzi H. Arpaci-Dusseau. 2016. Serverless computation with OpenLambda. In USENIX Workshop on Hot Topics in Cloud Computing (HotCloud) .

[30]

John Hughes. 2000. Generalising Monads to Arrows. Science of Computer Programming 37, 1–3 (May 2000), 67–111.

Digital Library

[31]

Abhinav Jangda, Donald Pinckney, Yuriy Brun, and Arjun Guha. 2019. Formal Foundations of Serverless Computing. https://arxiv.org/abs/1902.05870 .

[32]

Eric Jonas, Qifan Pu, Shivaram Venkataraman, Ion Stoica, and Benjamin Recht. 2017. Occupy the Cloud: Distributed Computing for the 99%. In Symposium on Cloud Computing.

Digital Library

[33]

Microsoft 2018a. Choose between Azure services that deliver messages. https://docs.microsoft.com/en-us/azure/eventgrid/compare-messaging-services . Accessed Jul 5 2018.

[34]

Microsoft 2018b. Microsoft Azure Functions. https://azure.microsoft.com/en-us/services/functions/ . Accessed Jul 5 2018.

[35]

OpenWhisk 2018a. Apache OpenWhisk. https://openwhisk.apache.org . Accessed Jul 5 2018.

[36]

OpenWhisk 2018b. OpenWhisk Actions. https://github.com/apache/incubator-openwhisk/blob/master/docs/actions.md . Accessed Jul 5 2018.

[37]

Aurojit Panda, Mooly Sagiv, and Scott Shenker. 2017. Verification in the Age of Microservices. In Workshop on Hot Topics in Operating Systems .

[38]

Daejun Park, Andrei Stefănescu, and Grigore Roşu. 2015. KJS: A Complete Formal Semantics of JavaScript. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) .

[39]

Ross Paterson. 2001. A New Notation for Arrows. In ACM International Conference on Functional Programming (ICFP).

Digital Library

[40]

Pulumi 2018. Pulumi. Cloud Native Infrastructure as Code. https://www.pulumi.com/ . Accessed Jul 5 2018.

[41]

Rodric Rabbah. 2017. Composing Functions into Applications the Serverless Way. https://medium.com/openwhisk/ composing-functions-into-applications-70d3200d0fac . Accessed Jul 5 2018.

[42]

Ganesan Ramalingam and Kapil Vaswani. 2013. Fault Tolerance via Idempotence. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) .

Digital Library

[43]

Ilya Sergey, James R. Wilcox, and Zachary Tatlock. 2017. Programming and Proving with Distributed Protocols. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) .

[44]

Zhiming Shen, Zhen Sun, Gur-Eyal Sela, Eugene Bagdasaryan, Christina Delimitrou, Van Robbert Renesse, and Hakin Weatherspoon. 2019. X-Containers: Breaking Down Barriers to Improve Performance and Isolation of Cloud-Native Containers. In ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) .

Digital Library

[45]

Arjun Singhvi, Sujata Banerjee, Yotam Harchol, Aditya Akella, Mark Peek, and Pontus Rydin. 2017. Granular Computing and Network Intensive Applications: Friends or Foes?. In ACM SIGCOMM Workshop on Hot Topics in Networks (HotNets).

Digital Library

[46]

David Walker, Lester Mackey, Jay Ligatti, George A. Reis, and David I. August. 2006. Static Typing for a Faulty Lambda Calculus. In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming.

[47]

Lucas Waye, Stephen Chong, and Christos Dimoulas. 2017. Whip: Higher-Order Contracts for Modern Services. In ACM International Conference on Functional Programming (ICFP) .

[48]

Sanjiva Weerawarana, Chathura Ekanayake, Srinath Perera, and Frank Leymann. 2018. Bringing Middleware to Everyday Programmers with Ballerina. In Business Process Management.

[49]

James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. 2015. Verdi: A framework for implementing and formally verifying distributed systems. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) .

Digital Library

Cited By

Mughele EOkuyade SOyem I(2024)A REVIEW OF THE IMPACT OF COVID-19 ON SERVERLESS COMPUTING TECHNOLOGYFUDMA JOURNAL OF SCIENCES10.33003/fjs-2024-0803-24788:3(111-118)Online publication date: 30-Jun-2024
https://doi.org/10.33003/fjs-2024-0803-2478
Hong ZLin JGuo SLuo SChen WWattenhofer RYu Y(2024)Optimus: Warming Serverless ML Inference via Inter-Function Model TransformationProceedings of the Nineteenth European Conference on Computer Systems10.1145/3627703.3629567(1039-1053)Online publication date: 22-Apr-2024
https://dl.acm.org/doi/10.1145/3627703.3629567
Basu Roy RPatel TGarg RTiwari DTsafrir DMUSUVATHI MGupta RAbu-Ghazaleh N(2024)CodeCrunch: Improving Serverless Performance via Function Compression and Cost-Aware Warmup Location OptimizationProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3617232.3624866(85-101)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3617232.3624866
Show More Cited By

Index Terms

Formal foundations of serverless computing
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Distributed programming languages

Recommendations

Supporting Multi-Provider Serverless Computing on the Edge
ICPP Workshops '18: Workshop Proceedings of the 47th International Conference on Parallel Processing

Serverless computing has recently emerged as a new execution model for cloud computing, in which service providers offer compute runtimes, also known as Function-as-a-Service (FaaS) platforms, allowing users to develop, execute and manage application ...
FLY: A Domain-Specific Language for Scientific Computing on FaaS
Euro-Par 2019: Parallel Processing Workshops
Abstract
Cloud Computing is widely recognized as distributed computing paradigm for the next generation of dynamically scalable applications. Recently a novel service model, called Function-as-a-Service (FaaS), has been proposed, that enables users to ...
Survey on serverless computing
Abstract
Serverless computing has gained importance over the last decade as an exciting new field, owing to its large influence in reducing costs, decreasing latency, improving scalability, and eliminating server-side management, to name a few. However, to ...

Comments

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue OOPSLA

October 2019

2077 pages

EISSN:2475-1421

DOI:10.1145/3366395

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 October 2019

Published in PACMPL Volume 3, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

64
Total Citations
View Citations
3,278
Total Downloads

Downloads (Last 12 months)648
Downloads (Last 6 weeks)58

Reflects downloads up to 19 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Mughele EOkuyade SOyem I(2024)A REVIEW OF THE IMPACT OF COVID-19 ON SERVERLESS COMPUTING TECHNOLOGYFUDMA JOURNAL OF SCIENCES10.33003/fjs-2024-0803-24788:3(111-118)Online publication date: 30-Jun-2024
https://doi.org/10.33003/fjs-2024-0803-2478
Hong ZLin JGuo SLuo SChen WWattenhofer RYu Y(2024)Optimus: Warming Serverless ML Inference via Inter-Function Model TransformationProceedings of the Nineteenth European Conference on Computer Systems10.1145/3627703.3629567(1039-1053)Online publication date: 22-Apr-2024
https://dl.acm.org/doi/10.1145/3627703.3629567
Basu Roy RPatel TGarg RTiwari DTsafrir DMUSUVATHI MGupta RAbu-Ghazaleh N(2024)CodeCrunch: Improving Serverless Performance via Function Compression and Cost-Aware Warmup Location OptimizationProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3617232.3624866(85-101)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3617232.3624866
Pandey MKwon YHong JPark J(2024)FuncMem: Reducing Cold Start Latency in Serverless Computing Through Memory Prediction and Adaptive Task ExecutionProceedings of the 39th ACM/SIGAPP Symposium on Applied Computing10.1145/3605098.3636033(131-138)Online publication date: 8-Apr-2024
https://dl.acm.org/doi/10.1145/3605098.3636033
De Palma GGiallorenzo SMauro JTrentin MZavattaro G(2024)FunLess: Functions-as-a-Service for Private Edge Cloud Systems2024 IEEE International Conference on Web Services (ICWS)10.1109/ICWS62655.2024.00114(961-967)Online publication date: 7-Jul-2024
https://doi.org/10.1109/ICWS62655.2024.00114
Mathew AAndrikopoulos VBlaauw FKarastoyanova D(2024)Pattern-based serverless data processing pipelines for Function-as-a-Service orchestration systemsFuture Generation Computer Systems10.1016/j.future.2023.12.026154(87-100)Online publication date: May-2024
https://doi.org/10.1016/j.future.2023.12.026
Palma GGiallorenzo SMauro JTrentin MZavattaro G(2024)Function-as-a-Service Allocation Policies Made FormalLeveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola10.1007/978-3-031-73709-1_19(306-321)Online publication date: 9-Oct-2024
https://doi.org/10.1007/978-3-031-73709-1_19
Li ZXu CChen QZhao JChen CGuo MAamodt TSwift MJerger N(2023)DataFlower: Exploiting the Data-flow Paradigm for Serverless Workflow OrchestrationProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 410.1145/3623278.3624755(57-72)Online publication date: 25-Mar-2023
https://dl.acm.org/doi/10.1145/3623278.3624755
Joosen AHassan AAsenov MSingh RDarlow LWang JBarker A(2023)How Does It Function? Characterizing Long-term Trends in Production Serverless WorkloadsProceedings of the 2023 ACM Symposium on Cloud Computing10.1145/3620678.3624783(443-458)Online publication date: 30-Oct-2023
https://dl.acm.org/doi/10.1145/3620678.3624783
Goodwin TQuinn AKuper LUstiugov DBruno RFonseca PGrot BBarbalace A(2023)What goes wrong in serverless runtimes? A survey of bugs in Knative ServingProceedings of the 1st Workshop on SErverless Systems, Applications and MEthodologies10.1145/3592533.3592806(12-18)Online publication date: 8-May-2023
https://dl.acm.org/doi/10.1145/3592533.3592806
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents