Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards a Function-as-a-Service Choreographic Programming Language: Examples and Applications

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

TL;DR

This work presents FaaSChal, a Choreographic Programming (CP) language tailored to Function-as-a-Service (FaaS) environments, enabling correctness-by-construction for serverless workflows. It demonstrates core CP concepts like projection and applies them to a serverless AI training example, where a choreography orchestrates stateless functions and imports library operations. A key contribution is showing how to extract locality principles from choreographies and synthesize Allocation Priority Policies (APP) to minimize latency while honoring user-defined constraints. The paper also develops a pipeline from choreography to local code (Projection) and from locality analysis to APP script generation, outlining future formal analyses and mechanisation efforts for broader FaaS architectures.

Abstract

Choreographic Programming (CP) is a language paradigm whereby software artefacts, called choreographies, specify the behaviour of communicating participants. CP is famous for its correctness-by-construction approach to the development of concurrent, distributed systems. In this paper, we illustrate FaaSChal, a proposal for a CP language tailored for the case of serverless Function-as-a-Service (FaaS). In FaaS, developers define a distributed architecture as a collection of stateless functions, leaving to the serverless platform the management of deployment and scaling. We provide a first account of a CP language tailored for the FaaS case via examples that present some of its relevant features, including projection. In addition, we showcase a novel application of CP. We use the choreography as a source to extract information on the infrastructural relations among functions so that we can synthesise policies that strive to minimise their latency while guaranteeing the respect of user-defined constraints.

Towards a Function-as-a-Service Choreographic Programming Language: Examples and Applications

TL;DR

This work presents FaaSChal, a Choreographic Programming (CP) language tailored to Function-as-a-Service (FaaS) environments, enabling correctness-by-construction for serverless workflows. It demonstrates core CP concepts like projection and applies them to a serverless AI training example, where a choreography orchestrates stateless functions and imports library operations. A key contribution is showing how to extract locality principles from choreographies and synthesize Allocation Priority Policies (APP) to minimize latency while honoring user-defined constraints. The paper also develops a pipeline from choreography to local code (Projection) and from locality analysis to APP script generation, outlining future formal analyses and mechanisation efforts for broader FaaS architectures.

Abstract

Choreographic Programming (CP) is a language paradigm whereby software artefacts, called choreographies, specify the behaviour of communicating participants. CP is famous for its correctness-by-construction approach to the development of concurrent, distributed systems. In this paper, we illustrate FaaSChal, a proposal for a CP language tailored for the case of serverless Function-as-a-Service (FaaS). In FaaS, developers define a distributed architecture as a collection of stateless functions, leaving to the serverless platform the management of deployment and scaling. We provide a first account of a CP language tailored for the FaaS case via examples that present some of its relevant features, including projection. In addition, we showcase a novel application of CP. We use the choreography as a source to extract information on the infrastructural relations among functions so that we can synthesise policies that strive to minimise their latency while guaranteeing the respect of user-defined constraints.
Paper Structure (8 sections, 5 figures)

This paper contains 8 sections, 5 figures.

Table of Contents

  1. Introduction
  2. Background on Serverless
  3. FaaSChal by Example
  4. Projection
  5. Applications: The Case of Function Scheduling Policies
  6. The APP Language
  7. Extraction of Locality Principles and Generation of APP Scripts
  8. Conclusion

Figures (5)

  • Figure 1: A typical serverless platform architecture.
  • Figure 2: The choreography of the serverless AI training program.
  • Figure 3: Projections of the example from \ref{['lst:choreo']}.
  • Figure 4: Left: locality principles extracted from the example from \ref{['lst:choreo']}. Right: infrastructure topology and user-defined function scheduling constraints.
  • Figure 5: APP script generated from the localities, topology, and user-defined constraints from \ref{['fig:localities']}