The Lamport diagram is a pervasive and intuitive tool for informal reasoning about causality in a concurrent system. However, traditional axiomatic formalizations of Lamport diagrams can be painful to work with in a mechanized setting like Agda, whereas inductively-defined data would enjoy structural induction and automatic normalization. We propose an alternative, inductive formalization -- the causal separation diagram (CSD) -- that takes inspiration from string diagrams and concurrent separation logic. CSDs enjoy a graphical syntax similar to Lamport diagrams, and can be given compositional semantics in a variety of domains. We demonstrate the utility of CSDs by applying them to logical clocks -- widely-used mechanisms for reifying causal relationships as data -- yielding 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. Our results and general framework are mechanized in the Agda proof assistant.

翻译：Lamport图是并发系统中用于非正式因果推理的一种直观且广泛使用的工具。然而，传统的Lamport图公理化形式化在Agda等机械化环境中难以处理，而归纳定义的数据结构则可以享受结构归纳和自动归一化的优势。我们提出了一种替代性的归纳形式化方法——因果分离图（CSD），其灵感来源于弦图与并发分离逻辑。CSD具有类似于Lamport图的图形语法，并可在多种领域中赋予组合语义。通过将CSD应用于逻辑时钟（一种将因果关系具象化为数据的广泛使用的机制），我们证明了其效用，从而得到了一个参数化于时钟选择的Lamport时钟条件的通用证明。我们在Lamport的标量时钟、Mattern的向量时钟以及Raynal等人和Wuu与Bernstein的矩阵时钟上实例化了该证明，并得到了每种时钟的验证实现。我们的结果与通用框架已在Agda证明助手中机械化实现。