Inductive diagrams for causal reasoning

TL;DR

Causal separation diagrams (CSDs) offer an inductive, diagrammatic model of causality in concurrent systems that generalizes Lamport diagrams while enabling mechanized verification. The approach builds interpretations of CSDs into causal paths, clock programs, and proofs, yielding a generic, clock-agnostic proof of Lamport's clock condition across realizable clocks such as scalar, vector, and matrix clocks. By mechanizing the framework in Agda, the authors demonstrate verified logical clocks and instantiate them for several clock families, including first mechanized proofs for matrix clocks. The work harmonizes diagrammatic reasoning with inductive semantics, providing a flexible foundation for verifying causal properties in both shared-memory and message-passing settings and suggesting strong links to string diagrams and separation logic.

Abstract

The Lamport diagram is a pervasive and intuitive tool for informal reasoning about "happens-before" relationships in a concurrent system. However, traditional axiomatic formalizations of Lamport diagrams can be painful to work with in a mechanized setting like Agda. We propose an alternative, inductive formalization -- the causal separation diagram (CSD) -- that takes inspiration from string diagrams and concurrent separation logic, but enjoys a graphical syntax similar to Lamport diagrams. Critically, CSDs are based on the idea that causal relationships between events are witnessed by the paths that information follows between them. To that end, we model happens-before as a dependent type of paths between events. The inductive formulation of CSDs enables their interpretation into a variety of semantic domains. We demonstrate the interpretability of CSDs with a case study on properties of logical clocks, widely-used mechanisms for reifying causal relationships as data. We carry out this study by implementing a series of interpreters for CSDs, culminating in a generic proof of Lamport's clock condition that is parametric in a choice of clock. We instantiate this proof on Lamport's scalar clock, on Mattern's vector clock, and on the matrix clocks of Raynal et al. and of Wuu and Bernstein, yielding verified implementations of each. The CSD formalism and our case study are mechanized in the Agda proof assistant.

Figures (9)

• Figure 1: An assortment of Lamport diagrams from the literature. In these examples, time flows from top to bottom ellis-gibbs-otweil-cephmathur-tree-clocks, from left to right castro-liskov-pbftlesani-chapar, or, rarely, from bottom to top lamport-clocks, and parallel through-lines represent processes, threads, or spatially-separated sites, while arrows represent communication between them.
• Figure 2: An example Lamport diagram.
• Figure 3: Two ways to decompose the Lamport diagram of \ref{['fig:lamport-diagram-example']} into "tiles". On the left (a), we split first along spatial boundaries (dashed red lines), yielding individual processes, and then along temporal boundaries (solid blue lines). On the right (b), we split first along temporal boundaries, yielding consistent cuts, and then along spatial boundaries.
• Figure 4: Global steps in our example diagram, with a site implied everywhere a cut intersects the diagram.
• Figure 5: Atomic steps of a CSD, depicted as graphical tiles. The $\mathbf{noop}$, $\mathbf{swap}$, and $\mathbf{assoc}$ tiles characterize the more general $\mathbf{perm}$ atomic step.

Theorems & Definitions (27)

• definition 1: Lamport execution lamport-clocks
• definition 2: Happens-before lamport-clocks
• definition 3: Site configurations
• definition 4: Sites
• definition 5: Permutations of sites ($\simeq$)
• definition 6: Causal separation diagrams ($\rightrightarrows$)
• definition 7: Global steps ($\multimap$)
• definition 8: The type of ticks
• definition 9: Labeled CSDs
• definition 10: Semantic interpretations