Semantics of
Reversible Concurrency

SPLS @ St Andrews

Vikraman Choudhury

[email protected]

MSP, University of Strathclyde, Glasgow, UK

Feb 11, 2026

Introduction

Programs run forwards.
Sometimes we may want to run them backwards:
- Reversible functions preserve information (Bennett)
- Reversible Boolean circuits in quantum computers (Fredkin, Toffoli)
- Encoders and decoders are partially invertible
- Reversible debugging
- Reversible process calculi (Danos, Krivine)
Models:
- Rig groupoids
- Inverse categories (Cockett)

What does a debugger do?

Reversible debuggers record the trace of a program’s execution
In debugging mode, the user can step forward and backward through the trace
The user can inspect the state of the program at any point in the trace, and look at the events that led to a particular state

$\begin{tikzpicture} [draw=gray, node distance = 10em, on grid, auto, every loop/.style={stealth-}] % States \node (q0) [state, draw=blue!70!black, initial, initial text = {}] {$q_0$}; \node (q1) [state, draw=blue!70!black, right = of q0] {$q_1$}; \node (q2) [state, draw=blue!70!black, right = of q1] {$q_2$}; \node (q3) [state, draw=blue!70!black, right = of q2] {$q_3$}; % Transitions \path [-stealth, thick, cyan!70!black] (q0) edge[bend left] node {$a$} (q1) (q1) edge[bend left] node {$b$} (q2) (q2) edge[bend left] node {$c$} (q3); \path [-stealth, thick, dotted, magenta!70!black] (q1) edge[bend left] node {$\overline{a}$} (q0) (q2) edge[bend left] node {$\overline{b}$} (q1) (q3) edge[bend left] node {$\overline{c}$} (q2); \end{tikzpicture}$

Debugging concurrent programs

What if the program is concurrent?
In a concurrent program, traces are not linear, they are “asynchronous”
To step backwards, the debugger needs to know which events are causally related, and which are independent

$\begin{tikzpicture} [draw=gray, node distance = 5em, on grid, auto, every loop/.style={stealth-}] % States \node (q0) [state, draw=blue!70!black, initial, initial text = {}] {$q_0$}; \node (q1) [state, draw=blue!70!black, above right = of q0] {$q_1$}; \node (q2) [state, draw=blue!70!black, below right = of q0] {$q_2$}; \node (q3) [state, draw=blue!70!black, right = of q1] {$q_3$}; \node (q4) [state, draw=blue!70!black, right = of q2] {$q_4$}; % Transitions \path [-stealth, thick, cyan!70!black] (q0) edge node {$a$} (q1) (q0) edge node {$b$} (q2) (q1) edge node {$c$} (q3) (q2) edge node {$d$} (q4); \path [-stealth, thick, dotted, magenta!70!black] (q1) edge[bend left] node {$\overline{a}$} (q0) (q2) edge[bend left] node {$\overline{b}$} (q0) (q3) edge[bend left] node {$\overline{c}$} (q1) (q4) edge[bend left] node {$\overline{d}$} (q2); \end{tikzpicture}$

Concurrent programs

$\begin{tikzpicture} [draw=gray, node distance =5em, on grid, auto, every loop/.style={stealth-}] % States \node (q0) [state, draw=blue!70!black, initial, initial text = {}] {$q_0$}; \node (q1) [state, draw=blue!70!black, right = of q0] {$q_1$}; \node (q2) [state, draw=blue!70!black, above right = of q1] {$q_2$}; \node (q3) [state, draw=blue!70!black, below right = of q1] {$q_3$}; \node (q4) [state, draw=blue!70!black, above right = of q3] {$q_4$}; \node (q5) [state, draw=blue!70!black, above right = of q2] {$q_5$}; \node (q6) [state, draw=blue!70!black, below right = of q5] {$q_6$}; \node (q7) [state, draw=blue!70!black, below right = of q3] {$q_7$}; \node (q8) [state, draw=blue!70!black, above right = of q7] {$q_8$}; \node (q9) [state, draw=blue!70!black, above right = of q8] {$q_9$}; % Transitions \path [-stealth, thick, cyan!70!black] (q0) edge node {$a$} (q1) (q1) edge node {$b$} (q2) (q1) edge node {$c$} (q3) (q2) edge node {$c$} (q4) (q3) edge node {$b$} (q4) (q2) edge node {$d$} (q5) (q5) edge node {$c$} (q6) (q4) edge node {$d$} (q6) (q4) edge node {$e$} (q8) (q3) edge node {$e$} (q7) (q7) edge node {$b$} (q8) (q8) edge node {$d$} (q9) (q6) edge node {$e$} (q9); \end{tikzpicture}$

Reversible Process Calculi

Event Structures

An event structure is a:

partial order of events $(E, \leq)$, satisfying
- axiom of finite causes: $\downset{e} = \{e' \in E \mid e' \leq e\}$ is finite for all $e \in E$, and
a conflict relation ${\confl} \subseteq E \times E$, that is:
- irreflexive and symmetric, and satisfies
- axiom of hereditary conflict: if $e \confl e'$ and $e' \leq e''$, then $e \confl e''$.

Two events are concurrent if they are not causally related and not in conflict: \[ e_1 \conc e_2 \iff \neg(e_1 \leq e_2 \lor e_2 \leq e_1 \lor e_1 \confl e_2) \]

Configurations

A (finite) configuration of $(E, \leq, \confl)$ is a subset $C \subseteq E$ that is:

downward-closed: if $e \in C$ and $e' \leq e$, then $e' \in C$, and
conflict-free: if $e, e' \in C$, then $\neg(e \confl e')$.

The set of all configurations is denoted $\Conf(E)$, and is ordered by inclusion.

We say $C \enables e$, or $C$ enables $e$, if:

$e \notin C$, and $C \cup \{e\} \in \Conf(E)$.

\[ E = \{a, b, c\}, \quad {\leq} = \{(a, c), (b, c), (a, a), (b, b), (c, c)\}, \quad {\confl} = \{(b, c), (c, b)\} \]

$\begin{tikzpicture} [draw=gray, node distance = 5em, on grid, auto, every loop/.style={stealth-}] % Events \node (z) [state, draw=blue!70!black, initial, initial text = {}] {$\emptyset$}; \node (a) [state, draw=blue!70!black, right = of z] {$\{a\}$}; \node (ab) [state, draw=blue!70!black, above right = of a] {$\{a, b\}$}; \node (ac) [state, draw=blue!70!black, below right = of a] {$\{a, c\}$}; % Transitions \path [-stealth, thick, cyan!70!black] (z) edge node {$a$} (a) (a) edge node {$b$} (ab) (a) edge node {$c$} (ac); \end{tikzpicture}$

Transitions between configurations

The initial configuration is $\emptyset$.

If $C \enables e$:

do a forward transition $C \flts{e} C \cup \{e\}$, and
add a backward transition $C \cup \{e\} \blts{\overline{e}} C$.

An LTS is a $P(L \times \blank)$-coalgebra.

A revLTS is a $P((L + L) \times \blank)$-coalgebra.

Two transitions are independent, $(C \lts{e_1} C_1) \ind (C \lts{e_2} C_2)$, if $e_1 \conc e_2$.

Labelled transition systems with Independence

Loop property: if $C \flts{e} C'$, then $C' \blts{\overline{e}} C$.

Square property:

$\begin{tikzcd}[ampersand replacement=\&] \& C \\ {C_1} \&\& {C_2} \arrow[""{name=0, anchor=center, inner sep=0}, "a"', from=1-2, to=2-1] \arrow[""{name=1, anchor=center, inner sep=0}, "b", from=1-2, to=2-3] \arrow[shift left=5, draw={rgb,255:red,214;green,92;blue,92}, curve={height=12pt}, shorten <=8pt, shorten >=8pt, no head, from=0, to=1] \end{tikzcd} \quad\Rightarrow\quad \begin{tikzcd}[ampersand replacement=\&] \& C \\ {C_1} \&\& {C_2} \\ \& D \arrow[""{name=0, anchor=center, inner sep=0}, "a"', from=1-2, to=2-1] \arrow[""{name=1, anchor=center, inner sep=0}, "b", from=1-2, to=2-3] \arrow["b"', dashed, from=2-1, to=3-2] \arrow["a", dashed, from=2-3, to=3-2] \arrow[shift left=3, draw={rgb,255:red,214;green,92;blue,92}, curve={height=12pt}, shorten <=4pt, shorten >=4pt, no head, from=0, to=1] \end{tikzcd}$

Backward independence property:

$\begin{tikzcd}[ampersand replacement=\&] {C_1} \&\& {C_2} \\ \& C \arrow["{\overline{a}}", from=2-2, to=1-1] \arrow["{\overline{b}}"', from=2-2, to=1-3] \end{tikzcd} \quad\Rightarrow\quad \begin{tikzcd}[ampersand replacement=\&] {C_1} \&\& {C_2} \\ \& C \arrow[""{name=0, anchor=center, inner sep=0}, "{\overline{a}}", from=2-2, to=1-1] \arrow[""{name=1, anchor=center, inner sep=0}, "{\overline{b}}"', from=2-2, to=1-3] \arrow[shift right=3, color={rgb,255:red,214;green,92;blue,92}, curve={height=-12pt}, shorten <=3pt, shorten >=3pt, no head, from=0, to=1] \end{tikzcd}$

Paths and computations

A path between $C_1$ and $C_2$ is either:

an empty path $C \lts{\varepsilon} C$, or
an edge $C \lts{e} C'$, followed by a path from $C'$ to $C_2$.

Configurations and paths form the free category $F(E)$ on the labelled graph generated by the event structure.

The independence relation on transitions generates a relation on paths:

$p \approx p$,
if $e_1 \conc e_2$, then $p \cdot e_1 \cdot e_2 \cdot q \approx q \cdot e_2 \cdot e_1 \cdot p$.

Configurations and paths form the quotient category of $F(E)$ by this equivalence relation.

Rollback

Given a configuration $C$ and an event $e \in C$, the rollback $\rollback{C}{e}$ is:

a maximal configuration $C' \subseteq C$ such that $C' \enables e$, and
$\rollback{C}{e} = C \mathrel{\setminus} \downset{e}$,
hence maximum.

Rollback satisfies the following properties:

Redoability: event $e$ can be executed in $\rollback{C}{e}$,
Causal safety: $\rollback{C}{e}$ contains no consequences of events that were rolled back,
Correctness: $C$ can be reached from $\rollback{C}{e}$, and
Minimality: there is no $C'$ satisfying the above properties such that the path from $C'$ to $C$ is shorter than the path from $\rollback{C}{e}$ to $C$.

Replay

To replay a computation starting at a configuration, we pick a causally-consistent log.

$e_1$ is in minimal conflict with $e_2$, denoted $e_1 \minconfl e_2$, if:

$e_1 \confl e_2$, and
for all $e_1' \leq e_1$ and $e_2' \leq e_2$, if $e_1' \confl e_2'$, then $e_1' = e_1$ and $e_2' = e_2$.

A log of a configuration $C$ is $\alog{C} = \{e \in C \mid \exists e' \not\in C, e \minconfl e'\}$.

Replay (contd.)

A computation $\sigma$ is compatible with a log $l$ if:

for all $e \in l$, $e \in \sigma$,
for all $e \in \sigma$, $e' \in l$, $\neg(e \confl e')$, and
for all $e \in \sigma$, $e' \in E$, if $e \confl e'$ then $e \in l$.

The set of computations compatible with a log $l$ is $\Comp(l)$.

$\Comp(l)$ has a:

minimum element $\minrepl{l} = \bigcup_{e \in l} \downset{e}$, and
maximum element $\maxrepl{l} = \minrepl{l} \cup \{e \in E \mid \forall e_1, e_2,\, e_1 \minconfl e_2 \land e_1 \leq e \implies e_1 \in l\}$.

Epilogue

What has been achieved?
- An abstract understanding of reversible concurrency.
- A notion of rollback and replay.
- Recovers the standard LTS of revCCS (almost).
- Formalisation in Lean: vikraman/event-structures.
Questions:
- Is this an axiomatisation?
- Is there a categorical account?
- Apply this to other models of concurrency?
- Apply this to other concurrent languages?

Semantics of Reversible Concurrency