Expand ↗
Page list (1404)
zetl

A Core Model for Choreographic Programming

Reference: Luís Cruz-Filipe & Fabrizio Montesi (2020). A Core Model for Choreographic Programming. Theoretical Computer Science (Elsevier). Extended version of the FoSSaCS 2017 paper of the same title. University of Southern Denmark, Department of Mathematics and Computer Science. URL. Keywords: Choreography, Computability, Process Calculi.

Summary

Choreographic Programming is a paradigm for writing concurrent programs that are deadlock-free by construction: a programmer declaratively writes the communications they want as a global program (a choreography), and an Endpoint Projection (EPP) mechanically synthesises the per-process implementations that faithfully realise those communications. Despite sustained interest, the field lacked a foundational model explaining which computations the hallmark constructs of choreographies can actually perform. This paper supplies one: Core Choreographies (CC), a calculus containing only the core primitives common to most choreography languages, restricted to the minimum needed for Turing power.

In CC, processes run in parallel and each stores a single value (a string built from a successor over a base symbol) in a local cell; a process may read its own memory but never another’s (no data sharing). The syntax offers just value communication (p.e -> q), label selection (p -> q[l]), conditionals, recursive procedure definitions, and a terminated choreography 0; local computation is deliberately crippled to constant and successor only, so any nontrivial computation must be expressed through communication. The central technical result is that the set of projectable choreographies in CC — those EPP can compile — is Turing complete; hence the resulting choreography projections (the executable process terms) are Turing complete too, characterising a Turing-complete, deadlock-free fragment of a process calculus (the authors’ Stateful Processes, and, relatedly, a fragment of value-passing CCS). The Turing-completeness proof is constructive: it gives an algorithm that builds a choreography implementing any given computable function.

Beyond expressivity, CC is offered as a canonical common setting for foundational questions about choreographies, analogous to the λ-calculus for functional programming and the π-calculus for mobile processes. As an illustration, the authors show label selection can be removed from CC without changing its computational power, yielding Minimal Choreographies (MC) — but at the cost of the clean separation between data and control, making programs hard to read. This motivates treating selections as a source-level convenience: the paper gives an amendment strategy encoding selections into ordinary communications, and shows the EPP for MC avoids the Merge Operator — usually one of the most intricate steps in projection.

Key Ideas

  • Core Choreographies (CC): a minimal choreographic calculus — value communication, label selection, conditional, recursive procedures, and termination 0 — with processes holding a single string cell and successor-only local computation.
  • Communication-forced computation: because local computation is restricted, any nontrivial function must be realised through inter-process communication, keeping the model both representative and analysable.
  • Turing completeness of projectable choreographies: the projectable fragment of CC (and therefore its EPP-produced process terms) is Turing complete; the proof constructs a choreography for any computable function.
  • Deadlock-free by construction: EPP yields processes guaranteed deadlock-free even under arbitrary protocol composition; only projectable choreographies can be projected, and their projections form the deadlock-free processes.
  • Expressivity of choreographies ≠ expressivity of projections: since EPP is an incomplete procedure guarding deadlock-freedom, the two must be studied separately.
  • Amendment: every unprojectable choreography can be made projectable by adding label selections.
  • Minimal Choreographies (MC): dropping label selection keeps Turing power but destroys the data/control separation; selections are better seen as syntactic sugar, encodable into communications — and MC’s EPP needs no merge operator.
  • Parallelism: CC gives a clean notion of parallelism in choreographies that translates directly to parallel execution of the projected processes.
  • Foundational stance: CC is argued to be a canonical model for choreographic programming, akin to λ-calculus / π-calculus, and also exposes a Turing-complete, deadlock-free fragment of value-passing CCS.

Connections

Conceptual Contribution

Tags

#choreographic-programming #process-calculi #computability #deadlock-freedom #endpoint-projection #foundations

Backlinks