Accompanist: A Runtime for Resilient Choreographic Programming

TL;DR

Accompanist introduces a resilient runtime for choreographic programming that enables reliable, decentralized saga transactions without requiring strong network assumptions or modifications to existing compilers.

Contribution

It presents Accompanist, a runtime that replays computations to mask faults, allowing simple, resilient choreographic programs to be deployed in service-oriented architectures.

Findings

Formal model and correctness proof for Accompanist

Supports decentralized saga transactions in existing systems

Enables fault masking without complex language features

Abstract

In service-oriented architecture, services coordinate in one of two ways: directly, using point-to-point communication, or indirectly, through an intermediary called the orchestrator. Orchestrators tend to be more popular because their local state is a 'single source of truth' for the status of ongoing workflows, which simplifies fault recovery and rollback for distributed transactions that use the 'saga' pattern. But orchestration is not always an option because of hardware constraints and security policies. Without a central orchestrator, resilient saga transactions are hard to implement correctly. A natural idea is to use choreographic programming, a paradigm that brings the 'global view' of orchestrators to a decentralised setting. Unfortunately, choreographic programming relies on strong assumptions about network reliability and service uptime that often do not hold. Recent work weakens some of these assumptions with 'failure-aware' language features, but these features make programs more complex. We propose a complementary approach: to co-design the programming interface with a customizable runtime that can replay computation to mask faults. Our approach keeps programs simple, does not require modifying the compiler, and lends itself to a clean separation of concerns in formal proofs. We present Accompanist, a resilient runtime for the Choral choreographic programming language. With Accompanist, programmers can implement decentralised saga transactions as choreographic programs and deploy the compiled code to 'sidecars' that run alongside services in a pre-existing codebase. Our key assumptions are that choreographic programs should be deterministic, transactions within a saga should be idempotent, and messages should be written to a durable message queue. Based on these assumptions, we present a formal model and prove that target code is correct-by-construction.