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.

翻译：Lamport图是一种普遍且直观的工具，用于并发系统中关于"发生在之前"关系的非形式化推理。然而，Lamport图的传统公理化形式化在Agda等机械化环境中难以处理。我们提出一种替代性的归纳形式化——因果分离图（CSD）——其灵感来自弦图与并发分离逻辑，但保持了类似Lamport图的图形语法。关键在于，CSD基于这样的思想：事件之间的因果关系由信息在它们之间传递的路径来见证。为此，我们将"发生在之前"建模为事件间路径的依赖类型。CSD的归纳公式使其能够被解释到多种语义域中。我们通过一个关于逻辑时钟属性的案例研究来展示CSD的可解释性——逻辑时钟被广泛用于将因果关系具象化为数据。我们通过实现一系列CSD的解释器来开展这项研究，最终得到并证明了一个参数化于时钟选择的Lamport时钟条件通用定理。我们将该定理实例化于Lamport标量时钟、Mattern向量时钟以及Raynal等人与Wuu和Bernstein的矩阵时钟，并分别获得了经过验证的实现。CSD形式化及我们的案例研究已在Agda证明助手中机械化实现。