From Global Choreographies to Provably Correct and Efficient Distributed Implementations

TL;DR

This paper presents a method to automatically generate correct and efficient distributed systems from high-level choreographies, ensuring behavior preservation and enabling verification, demonstrated through a micro-services case study.

Contribution

It introduces a novel approach for synthesizing conflict-free, controller-free distributed implementations from global choreographies with automatic verification capabilities.

Findings

Synthesized implementations are conflict-free and controller-free.

The approach reduces runtime communication overhead.

Verification of behavioral properties is enabled through translation to Promela.

Abstract

We define a method to automatically synthesize provably-correct efficient distributed implementations from high-level global choreographies. A global choreography describes the execution and communication logic between a set of provided processes which are described by their interfaces. The operations at the level of choreographies include multiparty communications, choice, loop, and branching. Choreographies are master-triggered, that is each choreography has one master to trigger its execution. This allows to automatically generate conflict free distributed implementations without controllers. The behavior of the synthesized implementations follows the behavior of choreographies. In addition, the absence of controllers ensures the efficiency of the implementation and reduces the communication needed at runtime. Moreover, we define a translation of the distributed implementations to equivalent Promela versions. The translation allows verifying the distributed system against behavioral properties. We implemented a Java prototype to validate the approach and applied it to automatically synthesize micro-services architectures. We illustrate our method on the automatic synthesis of a verified distributed buying system.