Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Ozone: Fully Out-of-Order Choreographies

Dan Plyukhin, Marco Peressotti, Fabrizio Montesi

TL;DR

A model of choreographic programming for out-of-order processes that guarantees absence of CIVs and deadlocks is developed and an API for safe non-blocking communication via futures in the choreographic programming language Choral is introduced.

Abstract

Choreographic programming is a paradigm for writing distributed applications. It allows programmers to write a single program, called a choreography, that can be compiled to generate correct implementations of each process in the application. Although choreographies provide good static guarantees, they can exhibit high latency when messages or processes are delayed. This is because processes in a choreography typically execute in a fixed, deterministic order, and cannot adapt to the order that messages arrive at runtime. In non-choreographic code, programmers can address this problem by allowing processes to execute out of order -- for instance by using futures or reactive programming. However, in choreographic code, out-of-order process execution can lead to serious and subtle bugs, called communication integrity violations (CIVs). In this paper, we develop a model of choreographic programming for out-of-order processes that guarantees absence of CIVs and deadlocks. As an application of our approach, we also introduce an API for safe non-blocking communication via futures in the choreographic programming language Choral. The API allows processes to execute out of order, participate in multiple choreographies concurrently, and to handle unordered data messages. We provide an illustrative evaluation of our API, showing that out-of-order execution can reduce latency and increase throughput by overlapping communication with computation.

Ozone: Fully Out-of-Order Choreographies

TL;DR

A model of choreographic programming for out-of-order processes that guarantees absence of CIVs and deadlocks is developed and an API for safe non-blocking communication via futures in the choreographic programming language Choral is introduced.

Abstract

Choreographic programming is a paradigm for writing distributed applications. It allows programmers to write a single program, called a choreography, that can be compiled to generate correct implementations of each process in the application. Although choreographies provide good static guarantees, they can exhibit high latency when messages or processes are delayed. This is because processes in a choreography typically execute in a fixed, deterministic order, and cannot adapt to the order that messages arrive at runtime. In non-choreographic code, programmers can address this problem by allowing processes to execute out of order -- for instance by using futures or reactive programming. However, in choreographic code, out-of-order process execution can lead to serious and subtle bugs, called communication integrity violations (CIVs). In this paper, we develop a model of choreographic programming for out-of-order processes that guarantees absence of CIVs and deadlocks. As an application of our approach, we also introduce an API for safe non-blocking communication via futures in the choreographic programming language Choral. The API allows processes to execute out of order, participate in multiple choreographies concurrently, and to handle unordered data messages. We provide an illustrative evaluation of our API, showing that out-of-order execution can reduce latency and increase throughput by overlapping communication with computation.
Paper Structure (16 sections, 5 theorems, 26 equations, 14 figures)

This paper contains 16 sections, 5 theorems, 26 equations, 14 figures.

Table of Contents

  1. Introduction
  2. Overview
  3. Intraprocedural Integrity
  4. Procedural Choreographies
  5. Interprocedural Integrity
  6. Choreography Model
  7. Syntax
  8. Semantics
  9. Transition rules
  10. Discussion
  11. Properties
  12. Process Model and Endpoint Projection
  13. Syntax
  14. Semantics
  15. Endpoint Projection
  16. ...and 1 more sections

Key Result

Theorem 1

If $\langle\, C,\ \Sigma,\ K \,\rangle$ is well-formed and $\langle\, C,\ \Sigma,\ K \,\rangle \xrightarrow{\,\mathsf{p}\,} \langle\, C',\ \Sigma',\ K' \,\rangle$, then $\langle\, C',\ \Sigma',\ K' \,\rangle$ is well-formed.

Figures (14)

  • Figure 1: A choreography where out-of-order execution can improve performance.
  • Figure 2: A choreography where naïve out-of-order execution is unsafe. Process $\mathsf{c}$ cannot distinguish whether the first message it receives represents key or txt.
  • Figure 3: Two approaches to prevent CIVs: selections and integrity keys.
  • Figure 4: The challenges of non-FIFO delivery. Part (a) depicts head-of-line blocking when using a FIFO transport protocol: The message containing $k$ arrives first, but it cannot be processed until $t$ arrives. Part (b) depicts a CIV caused by using an unordered transport protocol without integrity keys. Part (c) depicts how the processes can use integrity keys to prevent CIVs.
  • Figure 5: A choreography and two possible executions. In both diagrams, the green lines correspond to $X(\mathsf{p},\mathsf{q},\mathsf{r}_1)$ and the blue lines correspond to $X(\mathsf{p},\mathsf{q},\mathsf{r}_2)$.
  • ...and 9 more figures

Theorems & Definitions (6)

  • Theorem 1: Preservation
  • Theorem 2: Deadlock-Freedom
  • Definition 3: Send/receive transitions
  • Theorem 4: Communication Integrity
  • Lemma 5
  • Theorem 6: EPP Theorem