一句话：提出归纳式因果分离图（CSD），用路径依赖类型形式化 happens-before，并在 Agda 中验证逻辑时钟条件。
Lamport 图是并发系统中非形式化推理 happens-before 关系的直观工具，但其传统公理化形式在 Agda 等机械化环境中难以使用。本文提出归纳式的因果分离图（CSD），借鉴 string diagram 与并发分离逻辑，同时保留类似 Lamport 图的图形语法。CSD 将事件间因果关系视为信息沿路径传播的证据，并用事件间路径的依赖类型建模 happens-before，从而可解释到多种语义域。作者在 Agda 中机械化 CSD，并以逻辑时钟为案例实现一系列解释器，最终给出参数化于时钟选择的 Lamport clock condition 通用证明，实例化到标量、向量及矩阵时钟，得到经验证的实现。
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.
@article{paperbot2550,
title = {Inductive Diagrams for Causal Reasoning},
author = {Jonathan Castello and Patrick Redmond and Lindsey Kuper},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649830}
}