Write a Blog >>
SPLASH 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
Wed 23 Oct 2019 16:00 - 16:22 at Attica - Formalization Chair(s): Eric Koskinen

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.

Wed 23 Oct

Displayed time zone: Beirut change

16:00 - 17:30
FormalizationOOPSLA at Attica
Chair(s): Eric Koskinen Stevens Institute of Technology
16:00
22m
Talk
Formal Foundations of Serverless ComputingACM SIGPLAN Distinguished Paper Award
OOPSLA
Abhinav Jangda University of Massachusetts Amherst, Donald Pinckney University of Massachusetts Amherst, Yuriy Brun University of Massachusetts Amherst, Arjun Guha University of Massachusetts, Amherst
Link to publication DOI Pre-print
16:22
22m
Talk
A Formalization of Java’s Concurrent Access Modes
OOPSLA
John Bender University of California, Los Angeles, Jens Palsberg University of California, Los Angeles
DOI
16:45
22m
Talk
A Path to DOT: Formalizing Fully Path-Dependent Types
OOPSLA
Marianna Rapoport University of Waterloo, Ondřej Lhoták University of Waterloo
DOI Pre-print Media Attached
17:07
22m
Talk
Qubit Allocation as a Combination of Subgraph Isomorphism and Token Swapping
OOPSLA
DOI Pre-print