The Paths to Choreography Extraction

TL;DR

This paper introduces a novel methodology for automatically extracting choreographies from existing programs or protocols, enabling verification and synthesis in concurrent systems by analyzing symbolic execution paths.

Contribution

It presents a new choreography extraction method that handles stateful programs, improves efficiency, and captures asynchronous communication behaviors, advancing the automation of choreography generation.

Findings

Handles programs with internal state and computation

Significantly improves extraction time complexity

Captures correct asynchronous communication protocols

Abstract

Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification (e.g., Multiparty Session Types) and synthesis of correct-by-construction software (Choreographic Programming). They require a top-down approach: programmers first write choreographies, and then use them to verify or synthesize their programs. However, most existing software does not come with choreographies yet, which prevents their application. To attack this problem, we propose a novel methodology (called choreography extraction) that, given a set of programs or protocol specifications, automatically constructs a choreography that describes their behavior. The key to our extraction is identifying a set of paths in a graph that represents the symbolic execution of the programs of interest. Our method improves on previous work in several directions: we can now deal with programs that are equipped with a state and internal computation capabilities; time complexity is dramatically better; we capture programs that are correct but not necessarily synchronizable, i.e., they work because they exploit asynchronous communication.