Skip to main page content
U.S. flag

An official website of the United States government

Dot gov

The .gov means it’s official.
Federal government websites often end in .gov or .mil. Before sharing sensitive information, make sure you’re on a federal government site.

Https

The site is secure.
The https:// ensures that you are connecting to the official website and that any information you provide is encrypted and transmitted securely.

Access keys NCBI Homepage MyNCBI Homepage Main Content Main Navigation
. 2024 Dec 24:10:e1907.
doi: 10.7717/peerj-cs.1907. eCollection 2024.

A model for correlation-based choreographic programming

Saverio Giallorenzo  1   2 , Fabrizio Montesi  3 , Maurizio Gabbrielli  2
Affiliations

A model for correlation-based choreographic programming

Saverio Giallorenzo et al. PeerJ Comput Sci. .

Abstract

Choreographies provide a clear way to specify the intended communication behaviour of concurrent and distributed systems. Previous theoretical work investigated the translation of choreographies into (models of) programs based on message passing. However, existing theories still present a gap between how they model communications-using channel names à la CCS or π -calculus-and implementations-which use lower-level mechanisms for message routing. We start bridging this gap with a new formal framework called Applied Choreographies. In Applied Choreographies, developers write choreographies in a familiar syntax (from previous work) and reason about their behaviour through simple, abstract name-based communication semantics. The framework offers state-of-the-art features of choreographic models, e.g., modular programming supported via choreographic types. To provide its correctness guarantee, Applied Choreographies comes with a compilation procedure that transforms a choreography into a low-level, implementation-adherent calculus of Service-Oriented Computing (SOC). To manage the complexity of the compilation, we divide its formalisation and proof into three stages, respectively dealing with: (a) the translation of name-based communications into their SOC equivalents, namely, using correlation mechanisms based on message data; (b) the projection of the given choreography into a composition of partial, single-participant choreographies (towards their translation into SOC processes); (c) the translation of partial choreographies and the distribution of global, choreography-level state into local SOC processes. We provide behavioural correspondence results for each stage. Thus, given a choreography specification, we guarantee to synthesise its faithful service-oriented implementation.

Keywords: Choreographic programming; Concurrency; Distributed programming; Service-oriented computing.

PubMed Disclaimer

Conflict of interest statement

The authors declare that they have no competing interests.

Figures

Figure 1
Figure 1. Schema of the components of the encompassing contribution of this article: a behaviour-preserving compiler from frontend choreographies to DCC distributed processes.
Figure 2
Figure 2. Symbols and domains of the frontend choreographies calculus.
Figure 3
Figure 3. Frontend choreographies, syntax.
Figure 4
Figure 4. Choreography C1, extension of example 1.
Figure 5
Figure 5. Choreography C2, compliant choreography to Fig. 4.
Figure 6
Figure 6. Frontend choreographies, deployment transitions.
Figure 7
Figure 7. Frontend choreographies, semantics.
Figure 8
Figure 8. Frontend choreographies, structural congruence ≡C.
Figure 9
Figure 9. Frontend choreographies, swap relation ≃C.
Figure 10
Figure 10. Depiction of correlation-based message exchange in SOC.
Figure 11
Figure 11. Backend choreographies, deployment transitions.
Figure 12
Figure 12. Encoding algorithm from frontend to backend deployments.
Figure 13
Figure 13. Dynamic correlation calculus, syntax.
Figure 14
Figure 14. Dynamic correlation calculus, semantics.
Figure 15
Figure 15. Frontend choreographies, process projection.
Figure 16
Figure 16. Endpoint projection of lines 5–9 of example 1.
Figure 17
Figure 17. Compiler from endpoint choreographies to DCC.
See this image and copyright information in PMC

References

    1. Agha GA. Actors: a model of concurrent computation in distributed systems. 1985. Technical report, Massachusetts Inst of Tech Cambridge Artificial Intelligence Lab.
    1. AIOCJ Team AIOCJ framework. 2016. http://www.cs.unibo.it/projects/jolie/aiocj.html http://www.cs.unibo.it/projects/jolie/aiocj.html
    1. Alrahman YA, De Nicola R, Loreti M. A calculus for collective-adaptive systems and its behavioural theory. Information and Computation. 2019;268(7):104457. doi: 10.1016/j.ic.2019.104457. - DOI
    1. Alrahman YA, De Nicola R, Loreti M. Programming interactions in collective adaptive systems by relying on attribute-based communication. Science of Computer Programming. 2020;192(10):102428. doi: 10.1016/j.scico.2020.102428. - DOI
    1. Alur R, Etessami K, Yannakakis M. Inference of message sequence charts. IEEE Transactions on Software Engineering. 2003;29(7):623–633. doi: 10.1109/TSE.2003.1214326. - DOI

LinkOut - more resources