Chorex: Restartable, Language-Integrated Choreographies
Ashton Wiersdorf (University of Utah, USA), Ben Greenman (University of Utah, USA)

TL;DR
Chorex is a novel choreographic programming language for Elixir that enables robust distributed applications by supporting actor failure recovery, static error detection, and tight language integration.
Contribution
It introduces failure-tolerant choreographies in Elixir, demonstrating implementation via metaprogramming and providing static error reporting within the host language.
Findings
Chorex effectively recovers from actor crashes using checkpoints.
It integrates choreographies tightly with Elixir, enabling static error detection.
Overhead of checkpointing is measured and analyzed.
Abstract
We built Chorex, a language that brings choreographic programming to Elixir as a path toward robust distributed applications. Chorex is unique among choreographic languages because it tolerates failure among actors: when an actor crashes, Chorex spawns a new process, restores state using a checkpoint, and updates the network configuration for all actors. Chorex also proves that full-featured choreographies can be implemented via metaprogramming, and that doing so achieves tight integration with the host language. For example, mismatches between choreography requirements and an actor implementation are reported statically and in terms of source code rather than macro-expanded code. This paper illustrates Chorex on several examples, ranging from a higher-order bookseller to a secure remote password protocol, details its implementation, and measures the overhead of checkpointing. We…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsModular Robots and Swarm Intelligence · Security and Verification in Computing · Logic, programming, and type systems
