Choreographies in Practice
Lu\'is Cruz-Filipe, Fabrizio Montesi

TL;DR
This paper evaluates the practical application of choreographic programming, specifically Procedural Choreographies, to implement and analyze distributed algorithms like Quicksort, Gaussian elimination, and FFT, highlighting its potential and future directions.
Contribution
It demonstrates the use of Procedural Choreographies to implement complex distributed algorithms, providing insights into their applicability and future development.
Findings
Choreographies can be applied to real distributed algorithms.
Procedural Choreographies facilitate correct-by-construction implementations.
Lessons learned suggest directions for improving choreography languages.
Abstract
Choreographic Programming is a development methodology for concurrent software that guarantees correctness by construction. The key to this paradigm is to disallow mismatched I/O operations in programs, called choreographies, and then mechanically synthesise distributed implementations in terms of standard process models via a mechanism known as EndPoint Projection (EPP). Despite the promise of choreographic programming, there is still a lack of practical evaluations that illustrate the applicability of choreographies to concrete computational problems with standard concurrent solutions. In this work, we explore the potential of choreographies by using Procedural Choreographies (PC), a model that we recently proposed, to write distributed algorithms for sorting (Quicksort), solving linear equations (Gaussian elimination), and computing Fast Fourier Transform. We discuss the lessons…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
