Information and Computer Sciences Researchers Receive Award for Work on Serverless Computing

Abhinav Jangda (left) and Donald Pinckney (right)
Abhinav Jangda (left) and Donald Pinckney (right)

College of Information and Computer Sciences (CICS) doctoral students Abhinav Jangda and Donald Pinckney, along with professors Arjun Guha and Yuriy Brun, have received an Association for Computing Machinery (ACM) Special Interest Group on Programming Languages (SIGPLAN) 2019 Distinguished Paper Award for their paper, “Formal Foundations of Serverless Computing,” presented today at the Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) conference, held in Athens, Greece.

Serverless computing represents a step forward in cloud abstraction technology, making it easier to write robust, large-scale web services. In serverless computing, programmers write what are called serverless functions, or 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.

Unfortunately, serverless computing abstraction exposes several low-level operational details that make it hard for programmers to write and reason about their code. The paper “Formal Foundations of Serverless Computing” sheds light on this problem by presenting λλ (“Lambda Lambda”), 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 ease reasoning about code, the researchers present a simplified naive semantics of serverless execution and precisely characterize when the naive semantics and λλ coincide. In essence, λλ allows programmers to reason about their code without having to worry about the low-level complexities of the serverless framework deployment but get guarantees that their code will work properly even when faced with those complexities.

Read the full paper.