Executing Microservice Applications on Serverless, Correctly
While serverless platforms substantially simplify the provisioning, configuration, and management of cloud applications, implementing correct services on top of these platforms can present significant challenges to programmers.
For example, serverless infrastructures introduce a host of failure modes that are not present in traditional deployments.
Individual serverless instances can fail while others continue to make progress, correct but slow instances can be killed by the cloud provider as part of resource management, and providers will often respond to such failures by re-executing requests.
For functions with side-effects, these scenarios can create behaviors that are not observable in serverful deployments.
In this paper, we propose mu2sls, a framework for implementing microservice applications on serverless using standard Python code with two extra primitives: transactions and asynchronous calls.
Our framework orchestrates user-written services to address several challenges,
such as failures and re-executions,
and provides formal guarantees that the generated serverless implementations are correct.
To that end, we present a novel service specification abstraction and formalization of serverless implementations that facilitate reasoning about the correctness of a given application's serverless implementation.
This formalization forms the basis of the mu2sls prototype, which we then use to develop a few real-world microservice applications and show that the performance of the generated serverless implementations achieves significant scalability (3-5$\times$ the throughput of a sequential implementation) while providing correctness guarantees in the context of faults, re-execution, and concurrency.
Fri 20 JanDisplayed time zone: Eastern Time (US & Canada) change
13:30 - 14:45
Formal Methods in Compilation & ImplementationPOPL at Avenue34
Chair(s): Lindsey Kuper University of California at Santa Cruz
|Tail Recursion Modulo Context: An Equational Approach|
Daan Leijen Microsoft Research, Anton Lorenzen University of EdinburghDOI
|Taking Back Control in an Intermediate Representation for GPU Computing|
Vasileios Klimis Imperial College London, Jack Clark Imperial College London, Alan Baker Google, David Neto Google, John Wickerson Imperial College London, Alastair F. Donaldson Imperial College London; GoogleDOI
|Executing Microservice Applications on Serverless, Correctly|
Konstantinos Kallas University of Pennsylvania, Haoran Zhang University of Pennsylvania, Rajeev Alur University of Pennsylvania, Sebastian Angel University of Pennsylvania; Microsoft Research, Vincent Liu University of PennsylvaniaDOI