Introduction to Choreographies

The first rigorous and systematic treatment of choreographies: formal coordination plans for concurrent and distributed systems.

Fabrizio Montesi (Author)

9781108833769, Cambridge University Press

Hardback, published 25 May 2023

253 pages
26.2 x 18.4 x 1.9 cm, 0.63 kg

'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

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.

Introduction: Alice, Bob, concurrency, and distribution
This book
Part I. Foundations: Introduction to Part I
1. Inference systems
2. Simple choreographies
3. Simple processes
4. Endpoint projection
Part II. Computation: Introduction to Part II
5. Memory and local computation
6. Conditionals and knowledge of choice
7. Recursion
8. Properties of choreographies and endpoint projection
Part III. Extensions and Variations: Introduction to Part III
9. Conservative extensions
10. Choreographic choice
11. Asynchronous communication
12. Discussion and further reading
Solutions to selected exercises
Bibliography
Index.

Subject Areas: Computer science [UY], Software Engineering [UMZ], Information theory [GPF]