Inductive diagrams for causal reasoning

TL;DR

This paper introduces causal separation diagrams (CSDs), an inductive, graphical formalism inspired by Lamport diagrams, enabling mechanized reasoning about causal relationships in concurrent systems within Agda.

Contribution

It proposes CSDs as an inductive, graphical formalization of Lamport diagrams, facilitating mechanized reasoning and interpretation into various semantic domains.

Findings

Verified properties of logical clocks using CSDs

Implemented interpreters for different clock types in Agda

Proved Lamport's clock condition across multiple clock models

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.