Reachability Analysis of Function-as-a-Service Scheduling Policies
摘要
Functions-as-a-Service (FaaS) is a Serverless Cloud paradigm where a platform manages the execution (e.g., scheduling, runtime environments) of stateless functions. Recently, domain-specific languages like APP and aAPP have been developed 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. Reachability analysis of FaaS scheduling policies is fundamental to check quality-of-service properties, like preventing the scheduling of functions on workers which cannot sustain expected performance levels, or verifying security properties, e.g., that safety-critical functions cannot run on nodes with untrusted ones. We investigate the complexity of reachability analysis for APP and aAPP– the latter extends APP with constraints for placing functions according to the absence/presence of other (anti-)affine functions on workers. We show that reachability analysis has linear time complexity in APP, while the addition of affinities (in aAPP) makes reachability PSPACE. Given the computational complexity correspondence between reachability analysis in aAPP and automatic planning problems (both are in PSPACE), we investigate the exploitability of planners, i.e., tools specialised for solving planning problems for the realisation of static analysers of reachability-like problems for aAPP.