Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Complexity of Reachability Properties in Serverless Function Scheduling

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

TL;DR

This work analyzes the complexity of static reachability properties in serverless function scheduling by formalizing APP and its affinity-extended variant. It defines and studies Reach and CoOccur, showing linear-time results for APP without affinity but PSPACE-completeness when affinity is introduced, with NP-hardness emerging for affinity-only fragments. The results highlight a trade-off between expressiveness and tractability, informing the design of affinity-aware scheduling languages and verification tools for FaaS platforms. The formal framework and complexity results have practical implications for verifying security and locality properties in serverless environments while guiding future work on dynamic configurations and timed analyses.

Abstract

Functions-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. We present aAPP, an affinity-aware extension of a platform-agnostic function scheduling language. We formalise its scheduling semantics and then study the complexity of statically checking reachability properties, e.g., useful to verify that trusted and untrusted functions cannot be co-located. Analysing different fragments of aAPP, we show that checking reachability of policies without affinity has linear complexity, while affinity makes the problem PSpace.

On the Complexity of Reachability Properties in Serverless Function Scheduling

TL;DR

This work analyzes the complexity of static reachability properties in serverless function scheduling by formalizing APP and its affinity-extended variant. It defines and studies Reach and CoOccur, showing linear-time results for APP without affinity but PSPACE-completeness when affinity is introduced, with NP-hardness emerging for affinity-only fragments. The results highlight a trade-off between expressiveness and tractability, informing the design of affinity-aware scheduling languages and verification tools for FaaS platforms. The formal framework and complexity results have practical implications for verifying security and locality properties in serverless environments while guiding future work on dynamic configurations and timed analyses.

Abstract

Functions-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. We present aAPP, an affinity-aware extension of a platform-agnostic function scheduling language. We formalise its scheduling semantics and then study the complexity of statically checking reachability properties, e.g., useful to verify that trusted and untrusted functions cannot be co-located. Analysing different fragments of aAPP, we show that checking reachability of policies without affinity has linear complexity, while affinity makes the problem PSpace.
Paper Structure (14 sections, 8 theorems, 16 equations, 6 figures)

This paper contains 14 sections, 8 theorems, 16 equations, 6 figures.

Table of Contents

  1. Introduction
  2. language
  3. Reachability and Co-Occurrence in APP
  4. On the Support for Affinity-awareness of APP
  5. Reachability and Co-Occurence in
  6. Reachability and Co-Occurence with Polarised Affinities
  7. Related Work and Discussion
  8. Conclusion and Future Work
  9. Semantics
  10. APP semantics
  11. From YAML to APP Semantics' Structures
  12. Semantics
  13. LTS rules
  14. \ref{['theo:PSPACE_pp']}

Key Result

lemma 1

Let $C$ be an empty configuration, i.e., $\forall\ w \in \mathop{\mathrm{dom}}\nolimits(C)\ . C(w)=(\sigma,\cdot,\cdot)\ \wedge\ |\sigma| = 0$. Let $p$ be a scheduling policy, $\textit{reg}$ a function registry, $f$ a function, and $w$ a worker s.t. $w \in \mathop{\mathrm{dom}}\nolimits(C)$ and $\

Figures (6)

  • Figure 1: syntax.
  • Figure 2: Example script.
  • Figure 3: APP Syntax Encoding.
  • Figure 4: $\textbf{strategy}$ and $\textbf{valid}$ functions.
  • Figure 5: encoding.
  • ...and 1 more figures

Theorems & Definitions (17)

  • definition 1: Reachability
  • definition 2: Co-occurrence
  • lemma 1
  • proof
  • theorem 1
  • proof
  • theorem 2
  • proof
  • theorem 3
  • proof
  • ...and 7 more