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.

翻译：在面向服务的架构中，服务通过两种方式进行协调：直接使用点对点通信，或通过称为编排器的中介间接进行。编排器更受欢迎，因为其本地状态是持续工作流状态的“单一事实来源”，这简化了使用“saga”模式的分布式事务的故障恢复和回滚。但由于硬件约束和安全策略，编排并不总是可行的。在没有中央编排器的情况下，弹性saga事务难以正确实现。一个自然的想法是使用编舞化编程，这一范式将编排器的“全局视图”引入去中心化环境。不幸的是，编舞化编程依赖于对网络可靠性和服务可用性的强假设，而这些假设往往不成立。近期工作通过“故障感知”语言特性削弱了部分假设，但这些特性使程序更加复杂。我们提出一种补充方法：将编程接口与可定制的运行时协同设计，该运行时能重放计算以掩盖故障。我们的方法保持程序简洁，无需修改编译器，并在形式化证明中实现了清晰的关注点分离。我们提出Accompanist，一种面向Choral编舞化编程语言的弹性运行时。借助Accompanist，程序员可将去中心化saga事务实现为编舞化程序，并将编译后的代码部署到与现有代码库中服务并存的“边车”中。我们的关键假设是：编舞化程序应为确定性的，saga内的事务应为幂等的，消息应写入持久化消息队列。基于这些假设，我们提出了形式化模型，并证明了目标代码的构造正确性。