Introduction to Choreographies

Where to get it

You can get the book from various libraries and websites, including:

• Cambridge University Press
• Cambridge Core (for institutional access)
• Amazon (.com, .co.uk, .de, .it)

If you are a student or work in academia, you can probably ask your local library to get a copy for you.

Reviews

Distributed Systems have a large number and variety of Computing infrastructure parts. One of the main challenges lies in the solid definition of concurrency and protocols. This excellent and timely book addresses these issues in a convincing way by taking the reader on a journey of dealing with and reasoning on choreographies by providing many examples.

Schahram Dustdar, TU Wien, Austria

A mass of dancers dance individually and concurrently following a choreography, creating a masterpiece collaboratively. Choreographies are a framework to promote a protocol-guided programming for no single point of failure. Montesi's book starts from a friendly introduction to formal methods for beginners and covers comprehensive choreography theories—from the simple choreographies to the advanced extensions. Highly recommended for the undergraduate and graduate computer science students as well as developers of web services.

Nobuko Yoshida, Christopher Strachey Chair of Computing, University of Oxford

Distributed systems are the norm today. Choreographies govern how autonomous parts of distributed systems that operate concurrently may communicate with each other. However, it is not always clear whether all communication participants comply with a given choreography design. This book comes to the remedy. Fabrizio Montesi, pioneer of choreographic programming with the Jolie language and microservices community leader, establishes a uniform theory and a notation for choreographies – not only to specify their protocols, but also to check participant conformance and prove desired properties including communication safety and freedom from starvation. Read this book if you want to learn or teach these concepts en route to more robust and more understandable Distributed Systems, and apply its concepts in practice if you want to prove that your language, middleware, and tool creations work as designed.

Olaf Zimmermann, Eastern Switzerland University of Applied Sciences, School of Computer Science, Author of Patterns for API Design - Simplifying Integration with Loosely Coupled Message Exchanges

Book description

In concurrent and distributed systems, processes can complete tasks together by playing their parts in a joint plan. The plan, or protocol, can be written as a choreography: a formal description of overall behaviour that processes should collaborate to implement, like authenticating a user or purchasing an item online. Formality brings clarity, but not only that. Choreographies can contribute to important safety and liveness properties. This book is an ideal introduction to theory of choreographies for students, researchers, and professionals in computer science and applied mathematics. It covers languages for writing choreographies and their semantics, and principles for implementing choreographies correctly. The text treats the study of choreographies as a discipline in its own right, following a systematic approach that starts from simple foundations and proceeds to more advanced features in incremental steps. Each chapter includes examples and exercises aimed at helping with understanding the theory and its relation to practice.

Additional Resources

• Notes on the experience of teaching with this book.
• Wanna chat about choreographies? Join the Discord discussion server on multiparty languages!
• Choral, an object-oriented choreographic programming language that extends Java.
• Choreographic Programming on Wikipedia.
• Mermaid, a tool for writing and drawing sequence diagrams (among other things). Useful for documenting choreographies as text and visualising them. A live editor is available online.
• sequencediagram.com, a website for writing and displaying sequence diagrams.

Errata

Preface

• In the sentence right before (0.1), 'Charlie' should be 'Carol'.

Chapter 1

• On page 26, in the conclusion of the application of rule COMP in the middle of the page, Rome should be Sydney. Thanks to Thomas Wulff Heissel for pointing it out!

Chapter 2

• On page 53, figure 2.5, the transitions that appear in the middle and at the top-right should have a horizontal line labelled by COM above. Thanks to Thomas Wulff Heissel for pointing it out!

Chapter 6

• The extension to nondeterministic local functions in Section 6.1.2, page 111, requires a small modification to the transition labels of conditionals for Lemma 8.20 to hold (in particular, in order to deal with the case of DELAY-COND). Here are the updated COND-THEN and COND-ELSE rules. The transition rules for conditionals in the process language(s) need to be updated in the same way in order to match (the transition labels are the same). Thanks to Marco Peressotti and Dan Plyukhin for notifying me of the initial issue!

Chapter 7

• In Exercise 7.2, there should be only one initial transition of the form 𝜏@p, not two. (And the C mentioned in the text is not used.) Thanks to Thomas Wulff Heissel for noticing!
• In Exercise 7.12, Ring3 is incorrectly reported from Example 7.12: the last communication should be from r to p (as in the referenced example). Thanks to Thomas Wulff Heissel for noticing!

Chapter 10

• The semantics of choreographic choice requires a similar fix to the semantics of nondeterministic conditionals for Chapter 6:

Chapter 11

• Page 192 misses an equation about message sequences, which allows for exchanging messages from different receivers. This equation is necessary to deal with situations where the same sender communicates multiple messages to the same receiver one right after the other. Here is the equation: Having this kind of exchange rules is quite standard in the literature of choreographic programming and session types, but looking back a simpler approach might have been to model messaging states like choreographic stores (a map of maps of type PName -> PName -> Value | Label, mapping each process to another function that maps each process to the values or selection labels received from this latter process). This would eliminate the need for such exchanges.
• Rule SEND-VAL in Figure 11.2 should not update the store in the derivative: the Σ component should (obviously) be the same before and after the transition. Here is the fixed rule: Thanks to Lovro Lugović for spotting this issue!
• In 11.3, the rules for projecting asynchronous terms should look like this: Sadly, this mistake was introduced in the publishing process and I missed it when reading the proofs. :-( Thanks to Luc Edixhoven for the report!