We Know I Know You Know; Choreographic Programming With Multicast and Multiply Located Values

TL;DR

The paper tackles the Knowledge of Choice and deadlock-freedom challenges in choreographic programming by introducing multiply-located values and a multicast-based KoC approach in the He-Lambda-Small language. It defines a rigorous type system, centralized and local semantics, and an endpoint projection that preserves safety while eliminating the need for explicit bashselect constructs. The authors prove deadlock-freedom, provide correctness with respect to EPP, and demonstrate through case studies that the approach yields concise encodings of complex communication patterns with competitive efficiency. This work broadens the practical applicability of choreographic programming by simplifying KoC management and enabling scalable, distributed reasoning with multicast data distributions.

Abstract

Concurrent distributed systems are notoriously difficult to construct and reason about. Choreographic programming is a recent paradigm that describes a distributed system in a single global program called a choreography. Choreographies simplify reasoning about distributed systems and can ensure deadlock freedom by static analysis. In previous choreographic programming languages, each value is located at a single party, and the programmer is expected to insert special untyped "select" operations to ensure that all parties follow the same communication pattern. We present He-Lambda-Small, a new choreographic programming language with Multiply Located Values. He-Lambda-Small allows multicasting to a set of parties, and the resulting value will be located at all of them. This approach enables a simple and elegant alternative to "select": He-Lambda-Small requires that the guard for a conditional be located at all of the relevant parties. In He-Lambda-Small, checking that a choreography is well-typed suffices to show that it is deadlock-free. We present several case studies that demonstrate the use of multiply-located values to concisely encode tricky communication patterns described in previous work without the use of "select" or redundant communication.

Figures (26)

• Figure 1: A simple choreography between a buyer and seller.
• Figure 2: Endpoint projection of the example from Figure \ref{['fig:simple-choreography']}.
• Figure 3: A simple choreography between a buyer and seller, made projectable using bashselect (top), and its projection (bottom). This example adapts Figure \ref{['fig:simple-choreography']} to the syntax of Chor$\lambda$; bash<- becomes bashcom, bashif becomes bashcase, and added calls to bashselect for KoC project as bashoffer and bashchoose.
• Figure 4: The buyer and seller example from Figure \ref{['fig:epp2']}, written in $𐤄_{λ\mathrm{small}}$ without bashselect. In line 3, the bashcom function multicasts the conditional's guard to both parties, ensuring KoC for the conditional. The multicast bashcom operator is transformed into a multicast bashsend during endpoint projection.
• Figure 5: The complete syntax of the $𐤄_{λ\mathrm{small}}$ language.

Theorems & Definitions (23)

• Theorem 1: Substitution
• Theorem 2: Preservation
• Theorem 3: Progress
• Theorem 4: Soundness
• Theorem 5: Completeness
• Corollary 1: Deadlock Freedom
• Lemma 1: Enclave
• Lemma 2: Quorum
• Lemma 3: Unused
• Lemma 4: Sub-Mask