Wed 23 Oct 2024 16:40 - 17:00 at San Gabriel - Formal Methods 2 Chair(s): Bor-Yuh Evan Chang

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.

Wed 23 Oct

Displayed time zone: Pacific Time (US & Canada) change

16:00 - 17:40
Formal Methods 2OOPSLA 2024 at San Gabriel
Chair(s): Bor-Yuh Evan Chang University of Colorado Boulder & Amazon
16:00
20m
Talk
A Constraint Solving Approach to Parikh Images of Regular Languages
OOPSLA 2024
Amanda Stjerna Uppsala university, Philipp Rümmer University of Regensburg and Uppsala University
DOI
16:20
20m
Talk
Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping with References via Bidirectional Typing
OOPSLA 2024
Wenjia Ye National University of Singapore, Yaozhu Sun University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI
16:40
20m
Talk
Inductive diagrams for causal reasoning
OOPSLA 2024
Jonathan Castello University of California, Santa Cruz, Patrick Redmond University of California at Santa Cruz, Lindsey Kuper University of California, Santa Cruz
DOI Pre-print
17:00
20m
Talk
Message-Observing Sessions
OOPSLA 2024
Ryan Kavanagh Université du Québec à Montréal (UQAM), Brigitte Pientka McGill University
DOI
17:20
20m
Talk
Plume: Efficient and Complete Black-box Checking of Weak Isolation Levels
OOPSLA 2024
Si Liu ETH Zurich, Long Gu State Key Laboratory for Novel Software Technology, Nanjing University, Hengfeng Wei State Key Laboratory for Novel Software Technology, Nanjing University, David Basin ETH Zurich
DOI