Wed 15 Jun 2022 11:00 - 11:20 at Cockatoo - Distributed Systems Chair(s): Adam Chlipala

Serverless, or Functions-as-a-Service (FaaS), is an increasingly popular paradigm for application development, as it provides implicit elastic scaling and load based billing. However, the weak execution guarantees and intrinsic compute-storage separation of FaaS create serious challenges when developing applications that require persistent state, reliable progress, or synchronization. This has motivated a new generation of serverless frameworks that provide stateful abstractions. For instance, Azure’s Durable Functions (DF) programming model enhances FaaS with actors, workflows, and critical sections. As a programming model, DF is interesting because it combines task and actor parallelism, which makes it suitable for a wide range of serverless applications. We describe DF both informally, using examples, and formally, using an idealized high-level model based on the untyped lambda calculus. Next, we demystify how the DF runtime can (1) execute in a distributed unreliable serverless environment with compute-storage separation, yet still conform to the fault-free high-level model, and (2) persist execution progress without requiring checkpointing support by the language runtime. To this end we define two progressively more complex execution models, which contain the compute-storage separation and the record-replay, and prove that they are equivalent to the high-level model.

https://dl.acm.org/doi/10.1145/3485510
this URL might only work when visiting from a https://dl.acm.org/doi/10.1145/3485510 URL.

Wed 15 Jun

Displayed time zone: Pacific Time (US & Canada) change

10:40 - 12:00
Distributed SystemsSIGPLAN Track at Cockatoo
Chair(s): Adam Chlipala MIT CSAIL
10:40
20m
Talk
(ICFP 2020) TLC: Temporal Logic of Distributed Components
SIGPLAN Track
Jeremiah Griffin University of California, Riverside, Mohsen Lesani University of California at Riverside, Narges Shadab University of California at Riverside, Xizhe Yin University of California, Riverside
Link to publication DOI Authorizer link Pre-print
11:00
20m
Talk
(OOPSLA 2021) Durable functions: semantics for stateful serverless
SIGPLAN Track
Sebastian Burckhardt Microsoft Research, Chris Gillum Microsoft Azure, David Justo Microsoft Azure, Konstantinos Kallas University of Pennsylvania, Connor McMahon Microsoft Azure, Christopher Meiklejohn Carnegie Mellon University
Link to publication DOI Authorizer link Pre-print
11:20
20m
Talk
(OOPSLA 2021) ECROs: building global scale systems from sequential code
SIGPLAN Track
Kevin De Porre Vrije Universiteit Brussel, Carla Ferreira NOVA School of Science and Technology, Nuno Preguica , Elisa Gonzalez Boix Vrije Universiteit Brussel, Belgium
Link to publication DOI Authorizer link Pre-print
11:40
20m
Talk
(POPL 2022) Induction Duality: Primal-Dual Search for Invariants
SIGPLAN Track
Oded Padon VMware Research, James R. Wilcox Certora, Jason R. Koenig Stanford University, Kenneth L. McMillan University of Texas at Austin, Alex Aiken Stanford Univeristy