Reasoning About Choreographic Programs

Luís Cruz-Filipe, Eva Graversen, Fabrizio Montesi, Marco Peressotti [2023].
In proceedings of COORDINATION 2023, pp. 144-162.

Abstract

Choreographic programming is a paradigm where a concurrent or distributed system is developed in a top-down fashion. Programs, called choreographies, detail the desired interactions between processes, and can be compiled to distributed implementations based on message passing. Choreographic languages usually guarantee deadlock-freedom and provide an operational correspondence between choreographies and their compiled implementations, but until now little work has been done on verifying other properties.

This paper presents a Hoare-style logic for reasoning about the behaviour of choreographies, and illustrate its usage in representative examples. We show that this logic is sound and complete, and discuss decidability of its judgements. Using existing results from choreographic programming, we show that any functional correctness property proven for a choreography also holds for its compiled implementation.

Links

doi.org

Additional notes

None

Cite (BibTeX)

Click to expand

@inproceedings{DBLP:conf/coordination/Cruz-FilipeGMP23,
  author       = {Lu{\'{\i}}s Cruz{-}Filipe and
                  Eva Graversen and
                  Fabrizio Montesi and
                  Marco Peressotti},
  editor       = {Sung{-}Shik Jongmans and
                  Ant{\'{o}}nia Lopes},
  title        = {Reasoning About Choreographic Programs},
  booktitle    = {Coordination Models and Languages - 25th {IFIP} {WG} 6.1 International
                  Conference, {COORDINATION} 2023, Held as Part of the 18th International
                  Federated Conference on Distributed Computing Techniques, DisCoTec
                  2023, Lisbon, Portugal, June 19-23, 2023, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {13908},
  pages        = {144--162},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-35361-1\_8},
  doi          = {10.1007/978-3-031-35361-1\_8},
  timestamp    = {Fri, 07 Jul 2023 23:30:43 +0200},
  biburl       = {https://dblp.org/rec/conf/coordination/Cruz-FilipeGMP23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

A PDF is available (possibly a preprint):

Some data from DBLP and Crossref.