# Towards a verified compiler for Distributed PlusCal

Ghilain Bergeron, Horatiu Cirstea, Stephan Merz

► To cite this version:

Ghilain Bergeron, Horatiu Cirstea, Stephan Merz. Towards a verified compiler for Distributed PlusCal. 11th International Workshop on Rewriting Techniques for Program Transformations and Evaluation, Jul 2025, Birmingham, United Kingdom. hal-05329156

HAL Id: hal-05329156

https://hal.science/hal-05329156v1

Submitted on 24 Oct 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Towards a verified compiler for Distributed PlusCal

Ghilain Bergeron

Horatiu Cirstea

Stephan Merz

Université de Lorraine, CNRS, Inria, LORIA,
F-54000 Nancy, France

Formal verification techniques are frequently used to ensure correctness properties of distributed systems and algorithms. However, languages used for formal modeling and verification are often substantially different from languages used in software development, and verifying an abstract representation of an algorithm does not ensure that its handwritten implementation will be correct. This paper presents work in progress on a verified compiler for an extension of Lamport's PlusCal with threads and communication channels. Its syntax and semantics are formalized in the Lean 4 proof assistant and the passes compiling PlusCal algorithms into Go code are implemented in the underlying Lean 4 programming language. This paper gives formal semantics for the first pass of the compiler and outlines its mechanically verified correctness proof.

## 1 Introduction

Distributed systems and the distributed algorithms that these systems implement are notoriously difficult to design and to verify. This is due to the high number of potential executions that interleave steps of system components (distributed nodes, threads, messaging subsystem) executing independently, leading to bugs that are difficult to reproduce. Formal verification techniques such as model checking or theorem proving help ensure correctness properties of algorithms and of programs. They can be applied at different levels of abstraction. In particular, verifying formal specifications of distributed algorithms at high levels of abstraction allows designers to identify errors that would be very costly to correct during later development stages. However, languages used for formal modeling and verification are often substantially different from languages used in software development. Moreover, verifying an abstract representation of an algorithm does not ensure that its implementation will be correct if the translation from a verified specification to a concrete implementation is manual and thus, error-prone and potentially introducing subtle bugs.

Whereas the translation of sequential programs, including formal compiler verification, is nowadays a well-understood problem [Ler09], similar techniques for concurrent and distributed programs have been studied to a much lesser extent. Preliminary work exists for Erlang [ZBF20, HB24], Dist-Algo [LSL17] (a domain-specific language extension of Python), Modular PlusCal [HHC+23] (a superset of PlusCal), but the full formal verification of such translations has not been one of the primary goals. The verification aspect is more significant in Verdi [WWP+15], a framework for implementing distributed systems using OCaml and formally verifying their properties in Coq.

A step towards bridging the gap between the formal specification and the corresponding implementation is the use of modeling languages that are closer to programming languages. In the context of TLA⁺ [Lam02], a specification formalism that is based on mathematical set theory and temporal logic, PlusCal [Lam09] was proposed as an algorithmic language intended for the description of concurrent and distributed algorithms and systems. PlusCal combines the “look and feel” of imperative pseudo-code with the full power of mathematical set theory, used for modeling the data structures manipulated by the algorithm. It is therefore well suited to modeling systems at an intermediate level between abstract TLA⁺
<figure><img src="image_2.png" /><figcaption>Figure 1: Outline of the compilation.</figcaption></figure>

specifications and executable code. PlusCal algorithms are translated to TLA⁺ specifications and can be verified using the TLA⁺ model checkers [YML99, KKT19] or the proof assistant TLAPS [CDL⁺¹²], thus allowing a system designer to obtain high confidence in the correctness of the algorithm.

This work specifically targets Distributed PlusCal [CM23], an extension of PlusCal for describing distributed algorithms. The overall objective is to design a verified compiler from Distributed PlusCal to Go. Following standard practice, our compiler is structured as a sequence of transformation passes. Each pass introduces more concrete intermediate representations, systematically bridging the semantic gap between the high-level input and the target executable language by introducing refinements of the semantics of the original specification. The compiler is developed in the Lean 4 proof assistant [MU21], which serves both as a functional programming language and as a proof environment. Figure 1 illustrates the compilation phases. As we will explain in Section 3, the compiler takes as input programs in the Guarded PlusCal fragment of Distributed PlusCal. The downward (blue) arrows in the diagram represent transformations that have been programmed in Lean. The main contribution of this paper are the formal definition of the semantics of Guarded PlusCal and thus of Network PlusCal, which is a fragment of Guarded PlusCal, and a mechanized correctness proof of the first phase of compilation, represented by the upward (red) arrow in the diagram. We expect to apply the same overall methodology for the remaining phases.

**Outline.** We introduce in Section 2 Distributed PlusCal and present in Section 3 the formal syntax and semantics of Guarded PlusCal. Section 4 describes the first pass of the compiler and its correctness proof. We finally discuss the next steps in the development of the compiler.

## 2 Distributed PlusCal

TLA⁺ [Lam02] is a formalism for describing algorithms and systems at a high level of abstraction. It is based on mathematical set theory for representing data structures in terms of sets and functions, and on the Temporal Logic of Actions (TLA) for representing executions of systems. TLA⁺ specifications usually consist of a predicate describing the possible initial states, a predicate that represents the possible state transitions (w.r.t. all state variables appearing in the specification), and some liveness or fairness property expressed as a formula of temporal logic. The formal verification of TLA⁺ specifications is supported by the explicit-state model checker TLC, the SMT-based symbolic model checker Apalache, and the proof assistant TLAPS. Konnov et al. [KKM22] present an overview of the different verification tools applied to a common case study.

PlusCal [Lam09] was designed as a language for describing algorithms, providing a syntax that resembles imperative pseudo-code, including a process abstraction for modeling concurrent programs.
It relies on the rich language of expressions of TLA⁺, which allows for a high level of expressiveness, but also means that PlusCal algorithms are in general not executable. Distributed PlusCal [CM23] extends PlusCal with threads and also with communication channels. Both extensions are relevant for describing distributed algorithms: nodes of distributed systems are modeled by Distributed PlusCal processes and communicate by message passing, and they may contain threads that share access to the node's local memory. For example, a node could have a main thread of execution and a second thread for handling incoming messages in the background. The (Distributed) PlusCal translator generates a TLA⁺ specification from the algorithm and inserts it within the module containing the algorithm. Properties of algorithms are expressed as TLA⁺ formulas and are verified using the standard TLA⁺ tools.

The overall structure of a Distributed PlusCal algorithm consists of sections that declare global variables, operators, macros, and procedures (each of which may be empty) and a final section which contains either process declarations as shown in Listing 2.1 or a single body of statements representing a sequential algorithm.

Distributed PlusCal statements include `skip` (which does nothing), assignments, conditional statements, while loops, procedure calls, and `goto`. Processes and threads may synchronize using the `await` instruction that blocks until a predicate becomes true. Distributed PlusCal also includes two forms of non-deterministic control structures: `either ... or ...` can be used to introduce a choice between a fixed number of alternative branches, whereas the statement `with x ∈ S` expresses a choice among the values in a set `S`. In particular, guarded commands can be expressed by combining `either ... or` and `await` statements. Channels are declared using the keyword `fifo`; messages will be received in the order in which they are sent. The operation `send chan, expr)` sends a message corresponding to the expression `expr` on channel `chan` and the operation `receive chan, var)` receives a message from channel `chan` and stores it in the variable `var`.

An important concern when describing concurrent algorithms is to model the “grain of atomicity”, i.e., which statements are assumed to execute without interleaving with statements of other processes. PlusCal (and Distributed PlusCal) use statement labels to this effect: all statements appearing between two labels are executed atomically.

As an example, Listing 2.1 shows a simple Distributed PlusCal algorithm that implements a ping-pong protocol between two processes. The process `Pong` sends a message `"Ping"` on channel `ping` and waits for a message `"Pong"` on channel `pong` before starting again from the beginning, while process `Ping` proceeds symmetrically. The `await` statements are not really useful for this simple example, and users would typically use `while` loops instead of low-level `goto` statements. The example is written in this way in order to illustrate key aspects in the compilation strategy. The algorithm of Listing 2.1 introduces single instances (with identifiers 0 and 1) of the two process types. Alternatively, a fixed number of instances may be introduced by writing `process` (`p \in S`) where `S` must evaluate to a finite set. For the purpose of compiling towards an executable typed language, we assume that channels and variables are ascribed a type annotation (not shown in this listing) as defined by the Snowcat typechecker [KKT19] and that each process instance is assigned a dedicated channel, referred to as its mailbox, the only one through which it receives messages.

# 3 The Guarded PlusCal fragment

As mentioned in the previous section, the atomicity of statements (in a block) is a central concern when describing concurrent algorithms. Blocking statements like `await` and `receive` are one source of complexity when compiling interleaving blocks towards executable code. For example, an `await` statement
```c
--algorithm PingPong {
    fifos ping, pong;

    (* @ mailbox: ping; *)
    process (Ping = 0)
        variable tmp1 = "";
    {
        rcv1: receive(ping, tmp1);
        await tmp1 = "Ping";
        goto pong;
        pong: send(pong, "Pong");
        goto rcv1;
    }
}

(* @ mailbox: pong; *)
process (Pong = 1)
    variable tmp2 = "";
    {
        ping: send(ping, "Ping");
        goto rcv2;
        rcv2: receive(pong, tmp2);
        await tmp2 = "Pong";
        goto ping;
    }
}
```

<caption>Listing 2.1: Ping-pong algorithm in Distributed PlusCal</caption>

is executed only if the expression it contains evaluates to `TRUE`, in which case the control is passed to the next statement and otherwise, the execution of the containing block is aborted and tried again later. A direct implementation of such a behavior in executable code would require, in case of failure, rolling back all changes performed from the beginning of the block until the `await` statement. Indeed, this is the strategy employed in PGo, the compiler for Modular PlusCal, but provisioning for failure and potential rollback introduces significant overhead at execution.

We restrict here to a fragment of Distributed PlusCal that we call Guarded PlusCal that imposes several restrictions. First, Guarded PlusCal algorithms may contain process-local variables, but no global variables other than channel declarations: processes communicate exclusively by message passing. Second, a process receives messages only from a single channel, its mailbox<fnref n="1" />. Third and most importantly, any `receive` and `await` statements must be placed at the top of their respective blocks. This restriction by itself is not sufficient for avoiding rollbacks: for example, in the case of two `receive` operations, the second one might block, requiring the first one to be undone. However, we will see in Section 4 that it is a stepping stone for allowing us to avoid cancellation mechanisms built into the compiled program. Although the constraints might appear quite restrictive, we believe that Distributed PlusCal algorithms can generally be rewritten to satisfy them. For example, we checked that this is true for the algorithms contained in the TLA⁺ examples repository [LKM⁺]. Our Ping-Pong example is already written in Guarded PlusCal. For simplicity, we further assume that `while` statements are replaced with equivalent `if` and `goto` statements, and that `if` statements are rewritten as guarded commands, using a combination of `either ... or` and `await`.

## 3.1 Syntax of Guarded PlusCal

As for Distributed PlusCal, a Guarded PlusCal algorithm is composed of a section containing declarations (including the declaration of communication channels), and a section containing the different processes. Each process consists of some local variable declarations followed by the definition of the behavior of each of its threads, where each thread corresponds to a list of atomic blocks. Each block groups all the `guard` statements at the beginning and contains a final `goto` statement at the end. Note that there are no global variables in Guarded PlusCal; processes communicate exclusively through channels.

<footnote n="1">¹Observe that channel declarations could therefore be omitted, and the process identity could be used instead of the mailbox channel. We do not do this here so that Guarded PlusCal algorithms remain valid Distributed PlusCal algorithms.</footnote>
<table><tr><td>P</td><td>::=</td><td>p ⋆ (x = e)⋆ ⋆ ({(l : either B<sub>1</sub> or ... or B<sub>n</sub>)<sup>*</sup>}</td><td>Process</td></tr><tr><td>B</td><td>::=</td><td>G<sup>*</sup> ; E<sup>*</sup> ; goto l</td><td>Atomic block</td></tr><tr><td>G</td><td>::=</td><td>await e<br> receive(c,x)<br> with x = e | with x ∈ e</td><td>Precondition<br> Message reception<br> Block-local binding</td></tr><tr><td>E</td><td>::=</td><td>skip<br> x := e<br> print e<br> assert e<br> send(c,e)</td><td>Inaction<br> Local variable assignment<br> Local value output<br> Dynamic assertion<br> Message sending</td></tr></table>

where $l \in Label \uplus \{\text{Done}\}$ denotes labels, $x, c \in Var$ denote (channel) variables and $e$ denotes (non-temporal) TLA<sup>+</sup> expressions. Channels and variables can be indexed.

A process, identified by its identifier $p^2$, consists of a declaration of local variables—each initialized by an expression—and a list of threads, where each thread is defined as a sequence of labeled non-deterministic choices of atomic blocks (as will be discussed in the next section, any of the alternative branches can be selected for execution). For the sake of simplicity, we write $l_i : B_i$ instead of $l_i : \text{either } B_i$ when there is only one block. We denote by $\text{mailbox}_p$ the unique mailbox on which (the threads of) process $p$ can receive messages. For the algorithm in the Listing 2.1, the process identifiers are respectively 0 and 1, and their mailboxes are respectively *ping* and *pong*.

An atomic block $B$ (or simply block) is composed of three kinds of statements:

* guard statements $G$ determine when the block is *enabled*, i.e. has a chance to be executed, and may non-deterministically select values for some of the variables;

* execution statements $E$ define the actual behavior of the block;

* a `goto l` statement indicates the next block to be executed (or none, if $l$ is the reserved `Done`).

We consider $S ::= G | E$ the set of statements (guards or execution statements).

## 3.2 Semantics of Guarded PlusCal

A state is a pair $(M, C)$ where $M$ is a mapping from variables to values and $C$ is a mapping from channels to sequences of values. The execution of a statement on a state produces a new state and the execution of an atomic block results in a *final state* which also indicates the label of the next block to execute. $\mathit{State} = \mathit{State}_{\perp} \uplus \mathit{State}_{\top}$ denotes the indexed family of all the states:

$$ \mathit{State}_{\perp} = (\mathit{Var} \to \mathit{Value}) \times (\mathit{Var} \to \mathit{Value}^*) $$

$$ \mathit{State}_{\top} = \mathit{State}_{\perp} \times \mathit{Label} $$

$\mathit{State}_{\top}$ represents execution states reached after a `goto` terminal statement, while $\mathit{State}_{\perp}$ represents execution states obtained when executing the statements inside an atomic block. For any given $\sigma \in \mathit{State}_{\perp}$, we denote $M_{\sigma}$ and $C_{\sigma}$ its first and second projections respectively. $M(r \leftarrow v)$ denotes the mapping obtained by replacing the value of variable $r$ with $v$ in $M$, and $C(c \leftarrow vs)$ denotes the mapping obtained by replacing the sequence of values of channel $c$ with $vs$ in $C$.

To represent the actions performed by a process that are observable by other processes we consider the set *Trace* of sequences of process events of the form *out v* (process output) or *c!v* (channel sending).

<footnote n="2">²We omit in the syntax the process name.</footnote>
The symbol $\varepsilon$ denotes the empty trace, * the concatenation of two traces and $\le$ the prefix relation on traces.

We follow the approach proposed in [CWWC24], and define the semantics of Guarded PlusCal by two functions $[\cdot]$ and $[\cdot]^{\perp}$ describing respectively all the possible non-erroneous executions and all executions leading to an error. The semantics of atomic blocks (and threads) in case of non-erroneous executions is a set of triples $\langle\sigma, t, \sigma'\rangle$ where $\sigma \in State_{\perp}$ is the initial state, $t \in Trace$ is the trace of events produced by the statements in the block and $\sigma' \in State_{\top}$ is the final state. For statements, the semantics is also a set of triples $\langle\sigma, t, \sigma'\rangle$ but the state $\sigma' \in State_{\perp}$ is not final.

We present below the semantics of the Guarded PlusCal constructs used in the rest of the paper; the semantics of all the constructs is given in the appendix.

**Semantics of (non-temporal) expressions.** The expression language of TLA$^+$ is very rich and expressive, but not all expressions have a defined meaning. For example, the expression $1 \cup TRUE$ is a well-formed expression of TLA$^+$, but its meaning is not specified, and it is rejected by the model checkers TLC and Apalache.

We introduce the two reduction predicates $M \vdash e \Downarrow v$ and $M \vdash e \nparallel v$ that respectively describe when an expression is meaningful (i.e. can be reduced to a normal form $v$, given a memory $M$) and when an expression is meaningless (when $e$ admits no normal form in a given memory $M$). The set *Value* of normal forms consists of numerals, strings, booleans, sets, sequences, tuples, records, and functions. Note that some expressions may not always be meaningful depending on the memory in which they are reduced: for example the TLA$^+$ expression $x \cup \{TRUE\}$ evaluates to $\{TRUE\}$ if $M(x) = \{TRUE\}$ but does not evaluate to a value if $M(x) = 0$.

**Semantics of guards.** For an `await` statement, if the corresponding expression evaluates to `TRUE`, the execution continues with no changes to the state and no impact on the trace. When the expression evaluation fails, the execution is aborted. For a `receive` statement, the first value of the channel (mapping) is removed and assigned to the variable $r$. Such a statement never fails. For a `with` statement, the result of evaluating the expression (or one of the elements if the result is a set) is assigned to the variable in the memory. When the expression evaluation fails, the execution is aborted.

$$ 
\begin{align*}
[\text{await } e] &= \{\langle\sigma, \varepsilon, \sigma\rangle \mid \sigma \in \text{State}_{\perp} \wedge M_{\sigma} \vdash e \Downarrow \text{TRUE}\} \\
[\text{receive}(c,r)] &= \{\langle\sigma, \varepsilon, \langle M_{\sigma}(r \leftarrow v), C_{\sigma}(c \leftarrow vs)\rangle\rangle \mid \sigma \in \text{State}_{\perp} \wedge C_{\sigma}(c) = v \cdot vs\} \\
[\text{with } x = e] &= \{\langle\sigma, \varepsilon, \langle M_{\sigma}(x \leftarrow v), C_{\sigma}\rangle\rangle \mid \sigma \in \text{State}_{\perp} \wedge M_{\sigma} \vdash e \Downarrow v\} \\
[\text{with } x \in e] &= \{\langle\sigma, \varepsilon, \langle M_{\sigma}(x \leftarrow v), C_{\sigma}\rangle\rangle \mid \sigma \in \text{State}_{\perp} \wedge v \in S \wedge M_{\sigma} \vdash e \Downarrow S\} \\
[\text{await } e]^{\perp} &= \{\langle\sigma, \varepsilon\rangle \mid \sigma \in \text{State}_{\perp} \wedge M_{\sigma} \vdash e \nparallel \varepsilon\} \\
[\text{receive}(c,r)]^{\perp} &= \emptyset \\
[\text{with } x = e]^{\perp} &= \{\langle\sigma, \varepsilon\rangle \mid \sigma \in \text{State}_{\perp} \wedge M_{\sigma} \vdash e \nparallel \varepsilon\} \\
[\text{with } x \in e]^{\perp} &= \{\langle\sigma, \varepsilon\rangle \mid \sigma \in \text{State}_{\perp} \wedge M_{\sigma} \vdash e \nparallel \varepsilon\}
\end{align*}
$$

Note that we have a blocking semantics for all the guards: there is no transition when the expression in `await` evaluates to anything else than `TRUE`, when the channel in `receive` is empty, and when the expression in `with` evaluates to an empty set.
**Semantics of execution statements.** An assignment $r := e$ updates the value of the variable $r$ to the value of the expression $e$ and produces no trace event. If the evaluation of $e$ fails so does the assignment.

$$ 
\begin{align*}
\llbracket r := e \rrbracket &= \{ \langle \sigma, \varepsilon, \langle M_\sigma(r \leftarrow v), C_\sigma \rangle \rangle \mid \sigma \in \mathit{State}_\perp \wedge M_\sigma \vdash e \downarrow v \} \\
\llbracket r := e \rrbracket^\perp &= \{ \langle \sigma, \varepsilon \rangle \mid \sigma \in \mathit{State}_\perp \wedge M_\sigma \vdash e \downarrow \} 
\end{align*}
$$

An `assert` statement has no effect on the state and does not produce any trace event if the expression it contains evaluates to `TRUE`, otherwise the execution fails. The statements `print`, `send` and `skip` behave as usually. In particular, successful executions of `print` and `send` produce trace events. The formal semantics of all statements is given in the appendix.

**Semantics of atomic blocks.** Reducing an atomic block simply amounts to checking if it is enabled (i.e. if all its guards are satisfied), and then executing all the statements following the guards as well as the terminal `goto` statement. Given the (forward) composition defined by

$$ R_1 \circ_2 R_2 = \{ \langle s_1, t_1 * t_2, s_3 \rangle \mid \langle s_1, t_1, s_2 \rangle \in R_1 \wedge \langle s_2, t_2, s_3 \rangle \in R_2 \}, $$

the semantics of a block is a set of triples of the form $State_\perp \times Trace \times State_\perp$ defined inductively by:

$$ 
\begin{align*}
\llbracket \text{goto } l \rrbracket &= \{ \langle \sigma, \varepsilon, \langle \sigma, l \rangle \rangle \mid \sigma \in \mathit{State}_\perp \} \\
\llbracket S; B \rrbracket &= \llbracket S \rrbracket \circ_2 \llbracket B \rrbracket
\end{align*}
$$

An atomic block aborts whenever one of its guards or statements aborts (goto never aborts).

**Semantics of threads and processes.** We define the semantics of threads as a set of triples $State_\perp \times Trace \times State_\perp$, where the label in the first state indicates which block is allowed to be reduced, by

$$ 
\begin{align*}
\llbracket T \rrbracket &= \{ \langle \langle M, C, l \rangle, t, \sigma' \rangle \mid \sigma' \in \mathit{State}_\perp \wedge \langle \langle M, C \rangle, t, \sigma' \rangle \in \bigcup_{B \in T(l)} \llbracket B \rrbracket \} \\
\llbracket T \rrbracket^\perp &= \{ \langle \langle M, C, l \rangle, t \rangle \mid \langle \langle M, C \rangle, t \rangle \in \bigcup_{B \in T(l)} \llbracket B \rrbracket^\perp \}
\end{align*}
$$

where $T(l) = \{B_i | 1 \le i \le n \wedge l : \text{either } B_1 \text{ or } \dots \text{ or } B_n \in T\}$ is the collection of blocks at label $l$ in the thread $T$. The semantics of threads is merely defined as the set of all the possible choices between the enabled blocks at the given label $l$ in the thread (in their respective memory), effectively modelling the angelic non-determinism exhibited by an `either` statement in PlusCal.

The semantics of processes is then defined as the iteration of the composition of the semantics of threads (in any order), starting from the initial configuration where the memory is initialized to the initial value of local variables and each thread starts in its first block.

# 4 Towards compiling Guarded PlusCal into executable code

In this section, we describe the first pass of our compiler, from Guarded PlusCal to a restricted language better suitable for compilation into executable code. The other passes have also been implemented but not yet verified.
**4.1 General compiler correctness**

We start by recalling some standard techniques used to prove compiler correctness, which we will then apply in the following subsection. In the following, we consider two arbitrary languages $\mathcal{L}_S$ (the source language) and $\mathcal{L}_t$ (the target language) whose semantics [CWWC24] are defined by the functions $[\cdot]$ and $[\cdot]^{\perp}$ exhibiting all the possible (non-)erroneous executions in terms of tuples $(\sigma, t, \sigma')$, respectively $(\sigma, t)$, with $\sigma, \sigma'$ language specific configurations and $t$ observational traces. In the case of Guarded PlusCal, the configurations are the states of the program and the traces are sequences of events that can be observed, resulting from *print* and *send* statements. We also assume that the semantics of $\mathcal{L}_S$ and $\mathcal{L}_t$ are related by a (matching) relation $\mathcal{R}$ between configurations of the two languages and that the target language $\mathcal{L}_t$ has a well-founded measure $|\cdot|$ on its configurations.

**Definition 4.1 (Behavior refinement [CWWC24])**. Given two programs $S \in \mathcal{L}_S$ and $T \in \mathcal{L}_t$, $T$ refines the behavior of $S$, denoted $[[T]] \sqsubseteq_{\mathcal{R}} [[S]]$, if for all configurations $\sigma_S$ of $\mathcal{L}_S$, $\sigma_t$, $\sigma'_t$ of $\mathcal{L}_t$ and trace $t$ such that $(\sigma_S, \sigma_t) \in \mathcal{R}$ and $(\sigma_t, t, \sigma'_t) \in [[T]]$, either

a. there exists a configuration $\sigma'_S$ of $\mathcal{L}_S$ such that $(\sigma'_S, \sigma'_t) \in \mathcal{R}$ and $(\sigma_S, t, \sigma'_S) \in [[S]]$, or

b. there exists a trace $t_0 \le t$ such that $(\sigma_S, t_0) \in [[S]]^{\perp}$, or

c. $(\sigma_S, \sigma'_t) \in \mathcal{R}$ and $t = \varepsilon$ and $|\sigma'_t| < |\sigma_t|$.

<figure><img src="image_3.png" /></figure>

<figure><img src="image_4.png" /></figure>

<figure><img src="image_5.png" /></figure>

Behavior refinement states that every (non-erroneous) behavior that $T$ can exhibit is either a behavior that can also be exhibited by $S$, or corresponds to a failure of $S$ (perhaps for a shorter trace: $T$ could have performed some additional logging actions), or is an internal action that decreases the measure (and therefore $T$ cannot indefinitely perform such actions). Therefore, any execution of $T$ that does not fail corresponds to a successful execution of $S$ or to an execution of $S$ that fails at some point. Of course, the second case cannot happen if $S$ has been proved to be failure-free. Observe that nothing is required if $T$ fails and therefore the definition does not ensure completeness of the compiler.

**Theorem 4.2 (Refinement of sequential composition).** If both $[[S]] \sqsubseteq_{\mathcal{R}} [[T]]$ and $[[U]] \sqsubseteq_{\mathcal{R}} [[V]]$ hold, then $[[S;U]] \sqsubseteq_{\mathcal{R}} [[T;V]]$ holds as well.

A compiler $\mathcal{C} : \mathcal{L}_S \to \mathcal{L}_t$, i.e. a partial function from $\mathcal{L}_S$ to $\mathcal{L}_t$, is said to be partially correct if every program we obtain as output of $\mathcal{C}$ refines the behavior of the original program:

**Definition 4.3 (Compiler partial correctness).** $\mathcal{C}$ preserves the semantics of $\mathcal{L}_S$ iff for all program $P \in \mathcal{L}_S$ such that $\mathcal{C}(P)$ is defined, $[[\mathcal{C}(P)]] \sqsubseteq_{\mathcal{R}} [[P]]$.

Proving full compiler partial correctness is non-trivial, but is more easily tackled by considering each pass as a separate compiler. Each pass can then be proven partially correct separately, and all the correctness results can be tied back together by simple composition of partial functions and semantics.

**Theorem 4.4 (Composition of partially correct compilers).** Given two compilers $\mathcal{C}_1 : \mathcal{L}_1 \to \mathcal{L}_2$ and $\mathcal{C}_2 : \mathcal{L}_2 \to \mathcal{L}_3$ that respectively preserve the semantics of $\mathcal{L}_1$ and $\mathcal{L}_2$, their functional composition $\mathcal{C}_2 \circ \mathcal{C}_1 : \mathcal{L}_1 \to \mathcal{L}_3$ also preserves the semantics of $\mathcal{L}_1$.
## 4.2 From Guarded PlusCal to Network PlusCal

Compilation of Distributed PlusCal specifications into executable programs is a complex task essentially because of the atomicity of block execution combined with the blocking statements `await` and `receive`. A naive compilation of `receive@mailboxp,x)` into an executable language featuring asynchronous channels (e.g. into Go's `x := <-mailboxp`) can lead to behaviors that are not consistent with the semantics of Distributed PlusCal.

Consider the block `receive@mailboxp,x); await x > 50; goto Done`. When compiled naively by simply replacing the first statement with `x := <-mailboxp`, the corresponding program would receive a value from a channel `mailboxp`, without actually knowing if this value is greater than 50. Note that in Go it is not possible to peek at the channel's content without actually receiving the message. To preserve the intended semantics of PlusCal, we should roll back and replace the received value back as the first value in the channel, which is not possible in Go.

We address this problem by performing a first compilation pass $\mathcal{C}_{G \to N}$ that essentially replaces all receive guards with await statements. We call Network PlusCal the restriction of Guarded PlusCal where all receive guards have been removed. Since every process $p$ receives only from a single mailbox, we can use a new (fresh) variable `inboxp` in the local process state which handles the temporary buffering of a received message, and use it to encode the receive behavior. Continuing the previous example, we replace the first statements of the block by `await Len(inboxp) > 0; x := Head(inboxp); inboxp := Tail(inboxp); await x > 50`. However, this introduces an assignment preceding an await guard, and the statements must be reordered to obtain `await Len(inboxp) > 0; await Head(inboxp) > 50; x := Head(inboxp); inboxp := Tail(inboxp)`. Additionally, we introduce a separate thread to handle the transfer of messages from the mailbox to the local variable `inboxp`. These transformations are performed by rewrite rules, as defined below.

**The compiler $\mathcal{C}_{G \to N}$**. The goal of this compiler pass is to get rid of any potential blocking that may be incurred by receive guards by using an explicitly handled sequence `inboxp`; channel reception then becomes indexing into `inboxp` if that sequence is nonempty.

The compilation of receive statements is done by normalizing w.r.t. the one rule rewrite system $\mathcal{E}$:

$$ 
\begin{align*}
& p \star V^* \star T_1^* \{S_1^*; \text{receive}(\mathit{mailbox}_p, x); S_2^*; \text{goto } l; \} T_2^* \\
& \qquad \implies \mathcal{E} \\
& p \star V^*, \mathit{inbox}_p = \langle \rangle \star T_1^* \{S_1^*; \text{await } \mathit{Len}(\mathit{inbox}_p) > 0; x := \text{Head}(\mathit{inbox}_p); \mathit{inbox}_p := \text{Tail}(\mathit{inbox}_p); \\
& \qquad \qquad S_2^*; \text{goto } l; \} T_2^*
\end{align*}
$$

where $V^*, S^*$ and $T^*$ stand for arbitrary sequences of variables, statements and threads, respectively. The standard operators `Len`, `Head` and `Tail` on TLA$^+$ sequences denote the number of elements in the sequence, the first element of the sequence (provided it is nonempty) and the sequence without its first element, and $\langle \rangle$ denotes the empty sequence.

As explained above, the compilation of receive guards introduces new assignments that need to be reordered in order to produce a valid Network PlusCal block. This reordering is done by replacing the variables involved in the newly introduced assignments with the corresponding expressions. Since these expressions only depend on the freshly generated variables `inboxp`, no special care needs to be taken in the replacement process to avoid possible variable captures. This is done by normalizing w.r.t. the rewrite
system $\mathcal{S}$:

$$
\begin{align*}
S_1^*; x := e_1; & \textcolor{magenta}{await} e_2; S_2^*; \textcolor{magenta}{goto} l; && \implies \mathcal{S} \quad S_1^*; \textcolor{magenta}{await} e_2[e_1/x]; x := e_1; S_2^*; \textcolor{magenta}{goto} l; \\
S_1^*; x := e_1; & \textcolor{magenta}{with} y = e_2; S_2^*; \textcolor{magenta}{goto} l; && \implies \mathcal{S} \quad S_1^*; \textcolor{magenta}{with} y = e_2[e_1/x]; x := e_1; S_2^*; \textcolor{magenta}{goto} l; \\
S_1^*; x := e_1; & \textcolor{magenta}{with} y \in e_2; S_2^*; \textcolor{magenta}{goto} l; && \implies \mathcal{S} \quad S_1^*; \textcolor{magenta}{with} y \in e_2[e_1/x]; x := e_1; S_2^*; \textcolor{magenta}{goto} l;
\end{align*}
$$

Because we are replacing receive guards with indexing into a new local variable `inbox_p`, we also need to insert a separate thread that handles the transfer of messages from `mailbox_p` to that variable. This is accomplished by applying once the following rewrite rule on all processes that have an associated mailbox:

$$
\begin{align*}
& p \star V^* \star T^* \\
& \qquad \implies \mathcal{M} \\
& p \star V^*, \text{tmp} = v \star T^* \{rx_p : \text{receive}(\mathit{ mailbox}_p, \text{tmp}); \mathit{inbox}_p := \text{Append}(\mathit{ inbox}_p, \text{tmp}); \text{goto } rx_p; \}
\end{align*}
$$

where `tmp` is a fresh process-local variable that is initialized to some value `v` of the same type as the type contained in the mailbox, and `Append` is the operator from the TLA⁺ standard library that denotes insertion of a value at the end of a sequence. Note that the choice of the initial value `v` does not matter because `tmp` will always be overwritten before its first use.

We then define the compilation process by $\mathcal{C}_{G \to N} = \downarrow_{\mathcal{E}} \circ \downarrow_{\mathcal{S}} \circ \implies_{\mathcal{M}}$ with $\downarrow_R$ denoting the reduction to normal form w.r.t. a rewrite system $R$. The result of applying our compiler $\mathcal{C}_{G \to N}$ to the example of 2.1 is presented in Listing 4.1.

```c
--algorithm PingPong {
    fifos ping, pong;

    process (Ping = 0)
        variables
            tmp1 = "", rx_inbox_Ping = "",
            inbox_Ping = <<>>;
    {
        rcv1:   await Len(inbox_Ping) > 0;
        await Head(inbox_Ping) = "Ping";
        tmp1 := Head(inbox_Ping);
        inbox_Ping := Tail(inbox_Ping);
        goto pong;
        pong:  send(pong, "Pong");
        goto rcv1;
    }
}
{
    rx1:   receive(ping, rx_inbox_Ping);
        inbox_Ping :=
            Append(inbox_Ping, rx_inbox_Ping);
        goto rx;
}

process (Pong = 1)
    variables
        tmp2 = "", rx_inbox_Pong = "",
        inbox_Pong = <<>>;
    {
        ping:  send(ping, "Ping");
        goto rcv2;
        rcv2:  await Len(inbox_Pong) > 0;
        await Head(inbox_Pong) = "Pong";
        tmp2 := Head(inbox_Pong);
        inbox_Pong := Tail(inbox_Pong);
        goto ping;
    }
}
{
    rx2:   receive(pong, rx_inbox_Pong);
        inbox_Pong :=
            Append(inbox_Pong, rx_inbox_Pong);
        goto rx;
}
}
```

<caption>Listing 4.1: Ping-pong algorithm in Network PlusCal</caption>

**On the partial correctness of $\mathcal{C}_{G \to N}$**. The different languages involved in the compilation (Distributed PlusCal, Guarded PlusCal, Network PlusCal) are specified as types in the Lean proof assistant, and the rewrite rules defining the passes are implemented as Lean functions. Because in Lean, functions must terminate and respect their types, each transformation step is terminating, and the resulting normal forms contain only well-formed Network PlusCal blocks.
**Theorem 4.5 (Termination).** $\mathcal{C}_{G \to N}$ is terminating and the produced normal forms are valid Network PlusCal processes.

Concerning the correctness of this compilation pass, since the semantics of processes and threads does not change between Guarded PlusCal and Network PlusCal, it suffices to show that the compilation of each atomic block is correct. To establish this property, we first define the relation $\langle M_s, C_s \rangle \sim_{\text{mailbox}_p} \langle M_t, C_t \rangle$, which connects configurations of Guarded PlusCal and Network PlusCal in the presence of a mailbox:

$$ \langle M_s, C_s \rangle \sim_{\text{mailbox}_p} \langle M_t, C_t \rangle \iff \bigwedge \left\{ \begin{array}{l} \forall x \neq \text{inbox}_p. M_s(x) = M_t(x), \\ \forall c \neq \text{ mailbox}_p. C_s(c) = C_t(c), \\ C_s(\text{ mailbox}_p) = M_t(\text{ inbox}_p) \color{red}{++} C_t(\text{ mailbox}_p) \end{array} \right. $$

where ++ denotes sequence concatenation in TLA$^+$. In words, the values of variables other than the newly added variable inbox$_p$ and of channels other than mailbox$_p$ must match in the configurations of the source and target programs. Moreover, the content of mailbox$_p$ in the source configuration must correspond to the concatenation of the sequences contained in inbox$_p$ and in mailbox$_p$ in the target configuration, since some messages from the mailbox may already have been transferred to the local variable inbox$_p$. In particular, in the absence of a mailbox, the source and target configurations must match exactly.

The semantics of all languages involved in the compilation process have been defined in Lean and the partial correctness of each transformation step has been mechanically established. The partial correctness of the compilation pass $\mathcal{C}_{G \to N}$ is then obtained by composition of these results.

**Theorem 4.6 (Partial correctness of $\mathcal{C}_{G \to N}$).** For any Guarded PlusCal process P, we have that $[[\mathcal{C}_{G \to N}(P)]] \sqsubseteq_{\sim_{\text{mailbox}_p}} [[P]]$.

# 5 Conclusion

We have formally defined the semantics of the Distributed PlusCal specification language, an extension of PlusCal featuring processes, threads, and message-passing communications, in Lean 4, and we have started the development of a compiler into an executable language.

The first pass of the compiler, which transforms programs written in the Guarded PlusCal fragment of Distributed PlusCal into the Network PlusCal fragment by separating `await` and `receive` statements through the introduction of a helper thread and reordering statements if necessary, has been specified using rewrite rules and implemented in Lean 4. The rigorous description of Guarded PlusCal and Network PlusCal, using the type system of Lean 4, allows us to automatically establish the termination of the translation process and to guarantee that the resulting programs have the expected shape. We have also used the Lean 4 proof assistant to mechanically verify the correctness of the translation process.

The next step concerns the translation into Go programs. The syntax of Go has already been defined in Lean 4, and the translation from Network PlusCal into Go has been implemented. However, we will also need to define a formal semantics of Go in Lean 4 in order to state the correctness of the compilation. The preliminary compilation pass from Guarded PlusCal into Network PlusCal significantly simplifies the compilation into executable code since each block begins with a sequence of (side effect free) guards that must all be satisfied before changing the process-local environment. This allows us to avoid cancellation mechanisms (such as rollbacks in transactions) when compiling a block, because the enabledness of a block is completely determined by its guards. However, we still need to introduce synchronization mechanisms (such as locks) in order to prevent data races between multiple concurrently executing blocks. As before, we obtain for free the termination of the pass as well as the well-formedness of the resulting Go programs, but the correctness of the translation still needs to be established.
References

[CDL<sup>+</sup> 12] Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts & Hernán Vanzetto (2012): *TLA<sup>+</sup> Proofs*. In Dimitra Giannakopoulou & Dominique Méry, editors: *18th Intl. Symp. Formal Methods (FM 2012)*, LNCS 7436, Springer, Paris, France, pp. 147–154.

[CM23] Horatiu Cirstea & Stephan Merz (2023): *Extending PlusCal for Modeling Distributed Algorithms*. In Paula Herber & Anton Wijs, editors: *iFM 2023 - 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13-15, 2023, Proceedings, Lecture Notes in Computer Science* 14300, Springer, pp. 321–340, doi:10.1007/978-3-031-47705-8_17.

[CWWC24] Zhang Cheng, Jiyang Wu, Di Wang & Qinxiang Cao (2024): *Denotation-based Compositional Compiler Verification*. arXiv:2404.17297.

[HB24] Marian Hristov & Annette Bieniusa (2024): *Erla<sup>+</sup>: Translating TLA<sup>+</sup> Models into Executable Actor-Based Implementations*. In: *Proceedings of the 23rd ACM SIGPLAN International Workshop on Erlang*, Erlang 2024, Association for Computing Machinery, New York, NY, USA, p. 13–23, doi:10.1145/3677995.3678190. Available at https://doi.org/10.1145/3677995.3678190.

[HHC<sup>+</sup> 23] Finn Hackett, Shayan Hosseini, Renato Costa, Matthew Do & Ivan Beschastnikh (2023): *Compiling Distributed System Models with PGo*. In: *Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2*, ASPLOS 2023, Association for Computing Machinery, New York, NY, USA, p. 159–175, doi:10.1145/3575693.3575695. Available at https://doi.org/10.1145/3575693.3575695.

[KKM22] Igor Konnov, Markus Kuppe & Stephan Merz (2022): *Specification and Verification with the TLA<sup>+</sup> Trifecta: TLC, Apalache, and TLAPS*. In Tiziana Margaria & Bernhard Steffen, editors: *11th Intl. Symp. Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2022), Lecture Notes in Computer Science* 13701, Springer, Rhodes, Greece, pp. 88–105.

[KKT19] Igor Konnov, Jure Kukovec & Thanh-Hai Tran (2019): *TLA+ model checking made symbolic*. Proc. ACM Program. Lang. 3 (OOPSLA), doi:10.1145/3360549. Available at https://doi.org/10.1145/3360549.

[Lam02] Leslie Lamport (2002): *Specifying Systems: The TLA<sup>+</sup> Language and Tools for Hardware and Software Engineers*. Addison-Wesley, USA.

[Lam09] Leslie Lamport (2009): *The PlusCal Algorithm Language*. In M. Leucker & C. Morgan, editors: *6th Intl. Coll. Theor. Asp. Comp. (ICTAC 2009)*, LNCS 5684, Springer, Kuala Lumpur, Malaysia, pp. 36–60.

[Ler09] Xavier Leroy (2009): *Formal verification of a realistic compiler*. *Communications of the ACM* 52(7), pp. 107–115. Available at http://xavierleroy.org/publi/compcert-CACM.pdf.

[LKM<sup>+</sup>] Leslie Lamport, Markus A. Kuppe, Stephan Merz, Andrew Helwer, William Schultz, Jeff Hemphill, Mariusz Ryndzionek, Igor Konnov, Thanh Hai Tran, Josef Widder, Jim Gray, Murat Demirbas, Guanzhou Hu, Giuliano Losa, Ron Pressler, Younes Akhouayri, Luming Dong, Zhi Niu, Lim Ngian Xin Terry, Gaurav Gandhi, Isaac DeFrain, Martin Harrison, Santhosh Raju, Cherry G. Mathew, Fransisca Andriani & Ludovic Yvoz: *TLA<sup>+</sup> Examples*. https://github.com/tlaplus/examples/.

[LSL17] Yanhong A. Liu, Scott D. Stoller & Bo Lin (2017): *From Clarity to Efficiency for Distributed Algorithms*. *ACM Transactions on Programming Languages and Systems* 39(3), pp. 1–41.

[MU21] Leonardo de Moura & Sebastian Ullrich (2021): *The Lean 4 Theorem Prover and Programming Language*. In: *Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings*, Springer-Verlag, Berlin, Heidelberg, p. 625–635, doi:10.1007/978-3-030-79876-5_37. Available at https://doi.org/10.1007/978-3-030-79876-5_37.
[WWP<sup>+</sup>15] James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst & Thomas Anderson (2015): *Verdi: a framework for implementing and formally verifying distributed systems*. SIGPLAN Not. 50(6), p. 357–368, doi:10.1145/2813885.2737958. Available at https://doi.org/10.1145/2813885.2737958.

[YML99] Yuan Yu, Panagiotis Manolios & Leslie Lamport (1999): *Model Checking TLA<sup>+</sup> Specifications*. In Laurence Pierre & Thomas Kropf, editors: *Correct Hardware Design and Verification Methods*, Springer, Bad Herrenalb, Germany, pp. 54–66.

[ZBF20] Peter Zeller, Annette Bieniusa & Carla Ferreira (2020): *Teaching practical realistic verification of distributed algorithms in Erlang with TLA+. In Annette Bieniusa & Viktória Fördós, editors: *Erlang Workshop*, ACM, pp. 14–23.
# Appendix

## A Normal forms of TLA⁺ expressions

We define the set *Value* of all normal forms v by:

<table><tr><td>v</td><td>::=</td><td>n</td><td>Number literal</td></tr><tr><td></td><td></td><td>"s"</td><td>String literal</td></tr><tr><td></td><td></td><td>TRUE | FALSE</td><td>Boolean literal</td></tr><tr><td></td><td></td><td>{v<sub>1</sub>, ..., v<sub>n</sub>}</td><td>Set literal</td></tr><tr><td></td><td></td><td>&lt;v<sub>1</sub>, ..., v<sub>n</sub>&gt;</td><td>Sequence/tuple literal</td></tr><tr><td></td><td></td><td>[x<sub>1</sub> : v<sub>1</sub>, ..., x<sub>n</sub> : v<sub>n</sub>]</td><td>Record literal</td></tr><tr><td></td><td></td><td>v<sub>1</sub> :&gt; v<sub>2</sub> @@ ... @@ v<sub>n-1</sub> :&gt; v<sub>n</sub></td><td>Function literal</td></tr><tr><td></td><td></td><td>LAMBDA x<sub>1</sub> ... x<sub>n</sub>. e</td><td>Operator literal</td></tr></table>

## B Definition of the semantics of Guarded PlusCal

**Complete semantics of execution statements** A *skip* statement has no effect on the state and does not produce any trace event. A *print* statement produces an output event containing the value of the expression it contains. An *assert* statement has no effect on the state and does not produce any trace event if the expression it contains evaluates to *TRUE*, otherwise it aborts the execution. A *send* statement appends the value of the expression it contains to the sequence of values of the channel it sends to, and produces a sending event. An assignment statement *r* := *e* updates the value of the variable *r* to the value of the expression *e* and produces no trace event. A *skip* could not lead to a failure, all the other statements lead to a failure if the corresponding expression does so and in this case, no trace event is produced.

$$
\begin{align*}
[[skip]] &= \{\langle\sigma, \varepsilon, \sigma\rangle \mid \sigma \in \text{State}_{\perp}\} \\
[[print e]] &= \{\langle\sigma, \text{out } v, \sigma\rangle \mid \sigma \in \text{State}_{\perp} \wedge M_{\sigma} \vdash e \Downarrow v\} \\
[[assert e]] &= \{\langle\sigma, \varepsilon, \sigma\rangle \mid \sigma \in \text{State}_{\perp} \wedge M_{\sigma} \vdash e \Downarrow \text{TRUE}\} \\
[[send(c,e)]] &= \{\langle\sigma, c^{!}v, \langle M_{\sigma}, C_{\sigma}(c \leftarrow vs \cdot v) \rangle\rangle \mid \sigma \in \text{State}_{\perp} \wedge C_{\sigma}(c) = vs \wedge M_{\sigma} \vdash e \Downarrow v\} \\
[[r := e]] &= \{\langle\sigma, \varepsilon, \langle M_{\sigma}(r \leftarrow v), C_{\sigma}\rangle\rangle \mid \sigma \in \text{State}_{\perp} \wedge M_{\sigma} \vdash e \Downarrow v\} \\
[[skip]]^{\perp} &= \emptyset \\
[[print e]]^{\perp} &= \{\langle\sigma, \varepsilon\rangle \mid \sigma \in \text{State}_{\perp} \wedge M_{\sigma} \vdash e^{\perp}\} \\
[[assert e]]^{\perp} &= \{\langle\sigma, \varepsilon\rangle \mid \sigma \in \text{State}_{\perp} \wedge (M_{\sigma} \vdash e^{\perp} \lor M_{\sigma} \vdash e \Downarrow \text{FALSE})\} \\
[[send(c,e)]]^{\perp} &= \{\langle\sigma, \varepsilon\rangle \mid \sigma \in \text{State}_{\perp} \wedge M_{\sigma} \vdash e^{\perp}\} \\
[[r := e]]^{\perp} &= \{\langle\sigma, \varepsilon\rangle \mid \sigma \in \text{State}_{\perp} \wedge M_{\sigma} \vdash e^{\perp}\}
\end{align*}
$$

**Complete semantics of atomic blocks** Let the (forward) composition of semantics sets ($\circ_2$) : (State × Trace × State) × (State × Trace × State) → State × Trace × State defined by

$$R_1 \circ_2 R_2 = \{\langle s_1, t_1 * t_2, s_3 \rangle \mid \langle s_1, t_1, s_2 \rangle \in R_1 \wedge \langle s_2, t_2, s_3 \rangle \in R_2\},$$
the semantics of an atomic block is a set of triples of the form $State_⊥ \times Trace \times State_⊤$ defined inductively
by:

$$[[goto \ l]] = \{\langle\sigma, \varepsilon, \langle\sigma, l\rangle\rangle \mid \sigma \in State_⊥\}$$

$$[[S; B]] = [[S]] \circ_2 [[B]]$$

Let the (forward) composition $(\circ_1) : (State \times Trace \times State) \times (State \times Trace) \to State \times Trace$ defined
by

$$R \circ_1 X = \{\langle s_1, t_1 * t_2 \rangle \mid (s_1, t_1, s_2) \in R \wedge (s_2, t_2) \in X\},$$

the aborting semantics of an atomic block is then defined inductively by:

$$[[goto \ l]]^{\perp} = \emptyset$$

$$[[S; B]]^{\perp} = [[S]]^{\perp} \cup ([S] \circ_1 [[B]]^{\perp})$$

Reducing an atomic block simply amounts to checking if it is enabled (i.e. if all its guards are satisfied), and then executing all the statements following the guards as well as the terminal `goto` statement. An atomic block aborts whenever one of its guards or statements aborts (`goto` never aborts).