Reversible process models reveal causality and concurrency patterns
Concurrency, Causality and Conflict via Independence in Reversible Calculi
Logic in Computer Science
Summary
Understanding how events happen together or depend on one another is important in systems where many things occur at the same time. This paper shows that by looking at reversible systems with a way to tell which actions are independent, one can clearly identify how events cause or conflict with each other. The authors prove unique connections between these ideas and verify them with machine-checked proofs in two example calculi. They also show how reversing steps in these systems helps recover information about past events and their relationships.
What this means in practice
- •For concurrent system designers: Identify and formalize event dependencies and conflicts in concurrent systems to improve design clarity and correctness.
- •For programming language engineers: Use reversible calculi with independence relations to develop semantics that precisely capture concurrency and causality in new language features.
A theory result. No direct application yet.
Authors
Clément Aubert, Gabriele Cecilia, Iain C. C. Phillips, Irek Ulidowski
Abstract
Among the different ways of approaching the semantics of process calculi, true-concurrency models stand out for their ability to highlight subtle interplays between events. At their heart lie three crucial relations: concurrency, causality and conflict. This paper shows that reversibility, when endowed with a notion of independence, provides a rich tooling to study and characterise these true-concurrency relations. First, we prove that systems admitting pre-reversibility (i.e., that can be extended with an independence relation satisfying some basic axioms) have a unique notion of independence, events, concurrency, causality and conflict. We then analyse the relationship between independence and the true-concurrency relations, establishing novel independence-based characterisations of causality and conflict. Our second series of contributions revolves around two concrete process calculi and two syntactic notions defined on their transition labels, namely independence and dependence; we prove that they partition connected transitions and characterise elegantly concurrency on adjacent transitions. This part of our development was machine-checked using the proof assistant Beluga. Last, we study how the key mechanism commonly used in reversible process algebra can be used as a proxy to retrieve causality and core independence on past events. We conclude by discussing how our results extend beyond reversible systems.