Choreographies meet Communication Failures
summary
A choreography language models three concrete failure modes — send omission, receive omission, and emission failure — by declaring paired frames K/K' with local counters, splitting communication into declare/send/receive steps, and keeping messages in a network set. Separate send and receive primitives enable a library of recovery patterns (example: exponential backoff for send, timeout-based receive) as syntactic sugar. A static robustness analysis proves at-most-once delivery under any failure and exactly-once when omission failures are absent, while counters remain synchronized to avoid mixups.
AI-written summary · about
chapters (10)
- 0:00Choreographies and failures intro
- 1:06Realistic failures in choreographies
- 2:30Choreography language with failures
- 5:25Communication semantics with failures
- 9:00Recovery with conditional strategies
- 10:28Recovery with syntactic sugar
- 13:21Properties of choreographies with failures
- 14:27Robustness analysis for safety
- 18:22Benefits and guarantees
- 19:05Q&A
related talks
32mBalancing Choreography & Orchestration
19mChorCaml: Functional Choreographic Programming in OCaml
20mEfficient, Portable, Census-Polymorphic Choreographic Programming
38mChoreography vs Orchestration in long running asynchronous processes
22mTowards Lightweight and Efficient Choreographic Cloud Services
14mMultiparty Motion Coordination: From Choreographies to Robotics Programs
36mKlor: Choreographic Programming in Clojure
25mRelax! The Semilenient Core of Choreographic Programming (Functional Pearl)