Formally Verifying Function Scheduling Properties in Serverless Applications

Giuseppe De Palma*, Saverio Giallorenzo, Jacopo Mauro, Matteo Trentin, Gianluigi Zavattaro

*Corresponding author for this work

Research output: Contribution to journalJournal articleResearchpeer-review

11 Downloads (Pure)

Abstract

Function as a service (FaaS) is a serverless cloud execution model offering cost-efficiency, scalability, and simplified development by enabling developers to focus on code and delegate server management and application scaling to the serverless platform. Early FaaS implementations provided no control to users over function placement, but raising data locality-bound scenarios motivated new implementations with user-defined constraints over function allocations, e.g., to keep functions accessing a database close to the latter, with the aim of reducing latency, enhancing security, or complying with regulations. In this article, we show how, by leveraging the Allocation Priority Policies language—used for controlling function scheduling—and state-of-the-art planning tools, it is possible to enforce security properties and data-locality constraints, thereby guiding the definition of fine-grained serverless scheduling policies.
Original languageEnglish
JournalIT Professional
Volume25
Issue number6
Pages (from-to)94-99
ISSN1520-9202
DOIs
Publication statusPublished - 2023

Cite this