Formalizing Event-Driven Behavior of Serverless Applications

TL;DR

This paper introduces formal operational semantics for serverless computing to model event-driven interactions and constructs service call graphs for real applications, enhancing understanding of serverless workflows.

Contribution

It provides a formal framework for modeling serverless event-driven behavior and a method to construct and evaluate service call graphs from real applications.

Findings

Successfully modeled control transfer between functions

Constructed accurate service call graphs for twelve applications

Validated the semantics and graph construction algorithm

Abstract

We present new operational semantics for serverless computing that model the event-driven relationships between serverless functions, as well as their interaction with platforms services such as databases and object stores. These semantics precisely encapsulate how control transfers between functions, both directly and through reads and writes to platform services. We use these semantics to define the notion of the service call graph for serverless applications that captures program flows through functions and services. Finally, we construct service call graphs for twelve serverless JavaScript applications, using a prototype of our call graph construction algorithm, and we evaluate their accuracy.