TY - GEN
T1 - Function-as-a-Service Allocation Policies Made Formal
AU - Palma, Giuseppe De
AU - Giallorenzo, Saverio
AU - Mauro, Jacopo
AU - Trentin, Matteo
AU - Zavattaro, Gianluigi
PY - 2025
Y1 - 2025
N2 - Function-as-a-Service (FaaS) is a Serverless Cloud paradigm where a platform manages the execution scheduling (e.g., resource allocation, runtime environments) of stateless functions. Recent developments demonstrate the benefits of using domain-specific languages to express per-function scheduling policies, e.g., enforcing the allocation of functions on nodes that enjoy low data-access latencies thanks to proximity and connection pooling. In this paper, we consider APP, one of the languages proposed to specify Allocation Priority Policies in FaaS implemented on top of the popular OpenWhisk serverless platform. The aim of our operational semantics is twofold: on the one hand, it represents the underlying substrate necessary for the application of formal analysis techniques, on the other hand, it can drive consistent implementations of APP on top of the numerous serverless platforms recently proposed.
AB - Function-as-a-Service (FaaS) is a Serverless Cloud paradigm where a platform manages the execution scheduling (e.g., resource allocation, runtime environments) of stateless functions. Recent developments demonstrate the benefits of using domain-specific languages to express per-function scheduling policies, e.g., enforcing the allocation of functions on nodes that enjoy low data-access latencies thanks to proximity and connection pooling. In this paper, we consider APP, one of the languages proposed to specify Allocation Priority Policies in FaaS implemented on top of the popular OpenWhisk serverless platform. The aim of our operational semantics is twofold: on the one hand, it represents the underlying substrate necessary for the application of formal analysis techniques, on the other hand, it can drive consistent implementations of APP on top of the numerous serverless platforms recently proposed.
U2 - 10.1007/978-3-031-73709-1_19
DO - 10.1007/978-3-031-73709-1_19
M3 - Article in proceedings
AN - SCOPUS:85206993585
SN - 9783031737084
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 306
EP - 321
BT - Leveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola - 12th International Symposium, ISoLA 2024, Proceedings
A2 - Margaria, Tiziana
A2 - Steffen, Bernhard
PB - Springer Science+Business Media
T2 - 12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2024
Y2 - 27 October 2024 through 31 October 2024
ER -