Just Verification of Mutual Exclusion Algorithms

The mutual exclusion problem is a fundamental problem in concurrent programming. Given $N\ge 2$ threads,²²2What we call threads are in the literature frequently referred to as processes or computers. We use threads to distinguish between the real systems and our models of them, expressed in a process algebra. each of which may occasionally wish to access a critical section, a mutual exclusion algorithm seeks to ensure that at most one thread accesses its critical section at any given time. Ideally, this is done in such a way that whenever a thread wishes to access its critical section, it eventually succeeds in doing so. Many mutual exclusion algorithms have been proposed in the literature, and in general their correctness depends on assumptions one can make on the environment in which these algorithms will be running. The present paper aims to make these assumptions explicit, and to verify the correctness of some of the most popular mutual exclusion algorithms as a function of these assumptions.

A labelled transition system (LTS) is a tuple $(𝒮,\mathrm{𝐴𝑐𝑡},\mathrm{𝑖𝑛𝑖𝑡},\mathrm{𝑇𝑟𝑎𝑛𝑠})$ in which $𝒮$ is a finite set of states, $\mathrm{𝐴𝑐𝑡}$ is a finite set of actions, $\mathrm{𝑖𝑛𝑖𝑡}\in 𝒮$ is the initial state, and $\mathrm{𝑇𝑟𝑎𝑛𝑠}\subseteq 𝒮\times \mathrm{𝐴𝑐𝑡}\times 𝒮$ is a transition relation. We write $s\stackrel{𝑎}{\to }{s}^{\prime }$ for $(s,a,s^{\prime })\in \mathrm{𝑇𝑟𝑎𝑛𝑠}$. We say an action $a$ is enabled in a state $s$ if there exists a state $s^{\prime }$ such that $(s,a,s^{\prime })\in \mathrm{𝑇𝑟𝑎𝑛𝑠}$.

A path $\pi$ is a non-empty, potentially infinite alternating sequence of states and actions $s_0{a}_1{s}_1{a}_2\mathrm{\dots }$, with $s_0,s_1,\mathrm{\dots }\in 𝒮$ and $a_1,a_2,\mathrm{\dots }\in \mathrm{𝐴𝑐𝑡}$, such that if $\pi$ is finite, then its last element is a state, and for all $i\in \mathbb{N}$, $s_i\stackrel{a_{i+1}}{\to }{s}_{i+1}$. The first state of $\pi$ is its initial state. The length of $\pi$ is the number of transitions in it.

We use a notion of parallel composition that is taken from Hoare’s CSP [33], where synchronisation between components is enforced on all shared actions. It is defined as follows: For some $k\ge 1$, let $P_1,\mathrm{\dots },P_k$ be LTSs, where $P_i=({𝒮}_i,{\mathrm{𝐴𝑐𝑡}}_i,{\mathrm{𝑖𝑛𝑖𝑡}}_i,{\mathrm{𝑇𝑟𝑎𝑛𝑠}}_i)$ for all $1\le i\le k$. The parallel composition $P_1\Vert \mathrm{\dots }\Vert P_k$ of $P_1,\mathrm{\dots },P_k$ is the LTS $P=(𝒮,\mathrm{𝐴𝑐𝑡},\mathrm{𝑖𝑛𝑖𝑡},\mathrm{𝑇𝑟𝑎𝑛𝑠})$ in which $𝒮={𝒮}_1\times \mathrm{\dots }\times {𝒮}_k$, $\mathrm{𝐴𝑐𝑡}={\bigcup }_{1\le i\le k}{\mathrm{𝐴𝑐𝑡}}_i$, $\mathrm{𝑖𝑛𝑖𝑡}=({\mathrm{𝑖𝑛𝑖𝑡}}_1,\mathrm{\dots },{\mathrm{𝑖𝑛𝑖𝑡}}_k)$, and a transition $((s_1,\mathrm{\dots },s_k),a,(s_1^{\prime },\mathrm{\dots },s_k^{\prime }))$ is in $\mathrm{𝑇𝑟𝑎𝑛𝑠}$ if, and only if, $a\in \mathrm{𝐴𝑐𝑡}$ and the following are true for all $1\le i\le k$: if $a\notin {\mathrm{𝐴𝑐𝑡}}_i$, then $s_i=s_i^{\prime }$, and if $a\in {\mathrm{𝐴𝑐𝑡}}_i$, then $(s_i,a,s_i^{\prime })\in {\mathrm{𝑇𝑟𝑎𝑛𝑠}}_i$.
Note that by this definition of $\mathrm{𝑇𝑟𝑎𝑛𝑠}$, if an action is in the action set of a component but not enabled by that component in a particular state of the parallel composition, then the composition cannot perform a transition labelled with that action.

As mentioned in the introduction, the completeness criterion we use for our liveness verification is a variant of justness [24, 27]. Specifically, while justness is originally defined on transitions, we here define it on action labels, an adaption we take from [14]. As stated earlier, the definition of justness relies on the notion of a concurrency relation.

A concurrency relation may be asymmetric. We often reason about the complement of ${⌣}^{\bullet }$, ${\mathrm{／}⌣}^{\bullet }$. Read $a{⌣}^{\bullet }b$ as “$a$ is independent from $b$” and $a{\mathrm{／}⌣}^{\bullet }b$ as “$b$ interferes with/postpones $a$”.

Informally, justness says that a path is complete if whenever an action $a$ is enabled along the path, there is eventually an occurrence of an action (possibly $a$ itself) that interferes with it. This can be weakened by defining a set of blockable actions, for which this restriction does not hold; a blockable action may be enabled on a complete path without there being a subsequent occurrence of an interfering action. In this paper, the action of a thread to leave its non-critical section will be blockable. This way we model that a thread may choose to never take that option. We give the formal definition of justness, incorporating the blockable actions. We represent the set of blockable actions as $ℬ$. Its complement, $\overline{ℬ}$, is defined as $\mathrm{𝐴𝑐𝑡}\setminus ℬ$, given a set of actions $\mathrm{𝐴𝑐𝑡}$.

We say that a property is satisfied on a model under ${\mathrm{𝐽𝐴}}_{ℬ}^{{⌣}^{\bullet }}$ if it is satisfied on every path of that model, starting from the model’s initial state, that satisfies ${\mathrm{𝐽𝐴}}_{ℬ}^{{⌣}^{\bullet }}$. If $ℬ$ and ${⌣}^{\bullet }$ are clear from the context, we simply say that a path that satisfies ${\mathrm{𝐽𝐴}}_{ℬ}^{{⌣}^{\bullet }}$ is just.

In [50], we presented process-algebraic models of MWMR safe, regular and atomic registers. Through the semantics of the process algebra, this determines an LTS for each register of a given kind. In this paper, we use the same definitions for the three register types, but we have altered the process-algebraic models to be more compact and better facilitate the definition of the concurrency relations. The process-algebraic models can be found in Appendix A; here we merely summarise the key design decisions.

A register model represents a multi-reader multi-writer read-write register that allows every thread to read from and write to it. However, every thread may only perform a single operation on the register at a time. The register model specifies the behaviour of the register in response to operations performed by threads. Here we presuppose two disjoint finite sets: $𝕋$ of thread identifiers (thread id’s) and $ℝ$ of register identifiers (register id’s). Additionally, for every $r\in ℝ$ we reference the set ${𝔻}_r$ of all data values that the register $r$ can hold.

Recall that read and write operations take time, and may hence be concurrent. Therefore we represent a single operation with two actions: an invocation to indicate the start of the operation, and a response to indicate its end. Two operations are concurrent if the interval between their respective invocations and responses overlaps. The interface of a register is represented by the following actions: a read by thread $t\in 𝕋$ of register $r\in ℝ$ that returns value $d\in {𝔻}_r$ is a start read action ${\mathrm{𝑠𝑟}}_{t,r}$ followed by a finish read action ${\mathrm{𝑓𝑟}}_{t,r}(d)$; a write of value $d\in {𝔻}_r$ by a thread $t\in 𝕋$ to register $r\in ℝ$ is a start write action ${\mathrm{𝑠𝑤}}_{t,r}(d)$ followed by a finish write action ${\mathrm{𝑓𝑤}}_{t,r}$. In addition to this interface, which the threads can use to perform operations on the register, the regular and atomic models also use register local actions; these are internal actions by the register that are used to model the correct behaviour.

A register model requires some finite amount of memory to store a representation of relevant past events. We store this in what we call the status object, which features a finite set $𝕊$ of possible states. We abstract away from the exact implementation; for this presentation, all that is relevant is which information can be retrieved from it. Amongst others, we use the following access functions, which are local to any given register $r$:

• $\mathrm{■}$

  $\mathrm{𝑠𝑡𝑜𝑟}:𝕊\to {𝔻}_r$, the value that is currently stored in the register.

• $\mathrm{■}$

  $\mathrm{𝑤𝑟𝑡𝑠}:𝕊\to 2^{𝕋}$, the set of thread id’s of threads that have invoked a write operation on this register that has not yet had its response.

Any occurrence of a register action $a$ induces a state change $s\stackrel{𝑎}{\to }{s}^{\prime }$, resulting in an update to these access functions. For instance, the actions ${\mathrm{𝑠𝑤}}_{t,r}(d)$ and ${\mathrm{𝑓𝑤}}_{t,r}$ cause the updates $\mathrm{𝑤𝑟𝑡𝑠}(s^{\prime })=\mathrm{𝑤𝑟𝑡𝑠}(s)\cup \{t\}$ and $\mathrm{𝑤𝑟𝑡𝑠}(s^{\prime })=\mathrm{𝑤𝑟𝑡𝑠}(s)\setminus \{t\}$, respectively.

In our models, we combine processes representing both threads and registers. Similar to how register processes may contain register local actions, threads may contain thread local actions. Crucially, the local actions of both registers and threads are not involved in any communication, meaning that the only way for two threads to communicate is by writing to and reading from registers using the register interface actions.

The register models are mostly independent of the algorithm that we analyse with them; the algorithm merely dictates a register’s identifier, domain, and initial value. However, the thread models are fully dependent on the modelled algorithm, which dictates their behaviour. Therefore, we cannot present an algorithm-independent thread process. Instead, we presuppose the existence of an LTS $T_t=({𝒮}_t,{\mathrm{𝐴𝑐𝑡}}_t,{\mathrm{𝑖𝑛𝑖𝑡}}_t,{\mathrm{𝑇𝑟𝑎𝑛𝑠}}_t)$ and a set of thread local actions ${\mathrm{𝑇𝐿𝑜𝑐}}_t$ for every $t\in 𝕋$ such that ${\mathrm{𝐴𝑐𝑡}}_t=\{{\mathrm{𝑠𝑟}}_{t,r},{\mathrm{𝑓𝑟}}_{t,r}(d),{\mathrm{𝑠𝑤}}_{t,r}(d),{\mathrm{𝑓𝑤}}_{t,r}\mid r\in ℝ,d\in {𝔻}_r\}\cup {\mathrm{𝑇𝐿𝑜𝑐}}_t$. We assume that all sets of thread local actions are pairwise disjoint and that all thread LTSs $T_t$ satisfy two properties, representing the reasonable implementation of read and write operations. Firstly, on all paths from ${\mathrm{𝑖𝑛𝑖𝑡}}_t$, each transition labelled ${\mathrm{𝑠𝑟}}_{t,r}$ for some $r\in ℝ$ must go to a state where exactly the actions ${\mathrm{𝑓𝑟}}_{t,r}(d)$ for all $d\in {𝔻}_r$ are enabled. Similarly, all transitions labelled ${\mathrm{𝑠𝑤}}_{t,r}(d)$ for some $r\in ℝ,d\in {𝔻}_r$ must go to states where only ${\mathrm{𝑓𝑤}}_{t,r}$ is enabled. Secondly, transitions labelled ${\mathrm{𝑓𝑟}}_{t,r}(d)$ or ${\mathrm{𝑓𝑤}}_{t,r}$ are only enabled in these states.

We combine thread and register LTSs into thread-register models. For the following definition, we let $R_r=({𝒮}_r,{\mathrm{𝐴𝑐𝑡}}_r,{\mathrm{𝑖𝑛𝑖𝑡}}_r,{\mathrm{𝑇𝑟𝑎𝑛𝑠}}_r)$ be the LTS associated with each $r\in ℝ$.

Note that by our construction of the thread and register LTSs, every action in $\mathrm{𝐴𝑐𝑡}$ appears in at most two components of the parallel composition. Specifically, for all $t\in 𝕋$ and $a_t\in {\mathrm{𝑇𝐿𝑜𝑐}}_t$, $a_t$ appears only in $T_t$; for all $t\in 𝕋,r\in ℝ$, ${\mathrm{𝑜𝑟}}_{t,r}$ and ${\mathrm{𝑜𝑤}}_{t,r}$ appear only in $R_r$; and for all $t\in 𝕋,r\in ℝ$ and $d\in {𝔻}_r$, ${\mathrm{𝑠𝑟}}_{t,r},{\mathrm{𝑓𝑟}}_{t,r}(d),{\mathrm{𝑠𝑤}}_{t,r}(d)$ and ${\mathrm{𝑓𝑤}}_{t,r}$ appear exactly in $T_t$ and $R_r$.

In order to obtain a suitable notion of justness for our thread-register models, we need to choose both $ℬ$ and ${⌣}^{\bullet }$. Only thread local actions will be blockable; we define $ℬ$ in Section 6.

The concurrency relation, on the other hand, should relate the register interface actions. This is how we represent whether it is reasonable for one thread’s operations on a register to interfere with (and thereby postpone) another thread’s operations on that register. We use four different concurrency relations in our verifications, representing the four different models of blocking described in Section 1. These concurrency relations do not reference the thread local actions outside of the $\mathrm{𝑡ℎ𝑟}$ mapping, so we can already present these relations before giving more details on the precise models. To establish that the relations we present are indeed concurrency relations, we first establish a property of our models. We call this property thread consistency.

The correctness of our concurrency relations (cf. Definition 1) relies on our thread-register models being thread-consistent. The proof of this fact is given in Appendix B.

For the definitions of our four concurrency relations, we fix a thread-register model $M=(𝒮,\mathrm{𝐴𝑐𝑡},\mathrm{𝑖𝑛𝑖𝑡},\mathrm{𝑇𝑟𝑎𝑛𝑠},\mathrm{𝑡ℎ𝑟},\mathrm{𝑟𝑒𝑔})$. We also introduce two predicates on $\mathrm{𝐴𝑐𝑡}$: $\mathrm{𝑠𝑟}\mathrm{?}$ and $\mathrm{𝑠𝑤}\mathrm{?}$. For an action $a\in \mathrm{𝐴𝑐𝑡}$, these are defined as:

The thread interference relation, $⌣_{}^{\bullet }{}_T{}^{}$, expresses that every action is independent from every other action unless the two actions belong to the same thread; every two actions by the same thread interfere with each other. It captures the memory model with non-blocking reads and writes. This is the coarsest concurrency relation we will use.

This follows by a straightforward application of Lemma 6. The details are in [28, Appendix D].

The model with blocking writes and non-blocking reads is captured by the signalling reads relation, $⌣_{}^{\bullet }{}_S{}^{}$.

Intuitively, this is the same as $⌣_{}^{\bullet }{}_T{}^{}$ except that one thread starting a write to a register can interfere with a write to or a read from that same register by another thread. However, a read cannot interfere with another thread’s read or write. This concurrency relation has a precedent in [21, 14]. There, reads are modelled as signals, which differ from standard actions in that they do not block any other actions. Hence the name of this relation.

The blocking model with concurrent reads is captured by the interfering reads relation, $⌣_{}^{\bullet }{}_I{}^{}$. This is a further refinement from $⌣_{}^{\bullet }{}_S{}^{}$, where a start read can interfere with a start write on the same register, but cannot interfere with a start read.

This goes with the idea that performing a write on a memory location can only be done when the memory is reserved: repeated reads can prevent the memory from being reserved for a write, but as long as there is no write all the reads can take place concurrently.

Finally, the model of blocking reads and writes is captured by the all interfering relation, $⌣_{}^{\bullet }{}_A{}^{}$, a refinement of $⌣_{}^{\bullet }{}_I{}^{}$ where a start read can also interfere with another start read.

In this model, every operation on a register fully reserves that register for only that operation, and hence can prevent any other operation from taking place at the same time.

Below, we collect over a dozen mutual exclusion algorithms from the literature. We also present altered versions of several algorithms, incorporating fixes we propose. All these algorithms, and the registers themselves, have been translated to the process algebra mCRL2 [30]. The mCRL2 files are available as supplementary material. We give the most important design decisions regarding this translation here; further details can be found in [28, Appendix G]. The only operations on registers we allow are reading and writing. Hence, more complicated statements that may have been present in the original presentation of an algorithm, such as compare-and-swap instructions, are converted into these primitive operations. A statement like “await ${\forall }_{i\in 𝕋}:x(i)$”, where $x$ is some condition on a thread id $i$, is modelled as a recursive process that checks each thread id from smallest to largest, waiting for each until $x(i)$ is satisfied. Where an algorithm does not specify the initial value of a register, we take the lowest value from the given domain.

We use $c_t$ and ${\mathrm{𝑛𝑐}}_t$, with $t\in 𝕋$, as thread local actions. These actions represent a thread entering its critical section and leaving its non-critical section, respectively. We define $ℬ=\{{\mathrm{𝑛𝑐}}_t\mid t\in 𝕋\}$ to capture that a thread may always choose to remain in its non-critical section indefinitely; this is an important assumption underlying the correctness of mutual exclusion protocols.

We did our verification with the mCRL2 toolset [16]. To this end, we encoded mutual exclusion, deadlock freedom, and starvation freedom in the modal $\mu$-calculus, the logic used to represent properties in the mCRL2 toolset. We used the patterns from [51] to incorporate the justness assumption into our formulae for deadlock freedom and starvation freedom. The full modal $\mu$-calculus formulae appear in [28, Appendix H] (and also as supplementary material). Besides the correctness properties discussed in Section 1, Dijkstra [20] requires that the correctness of the algorithms may not depend on the relative speeds of the threads. This requirement is automatically satisfied in our approach, since we allow all possible interleavings of thread actions in our models.

We checked mutual exclusion, deadlock freedom, and starvation freedom. If mutual exclusion is not satisfied, we do not care about the other two properties. Additionally, if deadlock freedom is not satisfied, we know that starvation freedom is not satisfied either. We can therefore summarise our results in a single table: $\mathrm{X}$ if none of the three properties are satisfied, $\mathrm{M}$ if only mutual exclusion is satisfied, $\mathrm{D}$ if only mutual exclusion and deadlock freedom hold, and $\mathrm{S}$ if all three are satisfied. See Table 1. As stated previously, we verify liveness properties under justness, where we employ $⌣_{}^{\bullet }{}_T{}^{}$ for safe and regular registers and all four concurrency relations $⌣_{}^{\bullet }{}_T{}^{}$, $⌣_{}^{\bullet }{}_S{}^{}$, $⌣_{}^{\bullet }{}_I{}^{}$ and $⌣_{}^{\bullet }{}_A{}^{}$ for atomic registers. We checked with 2 threads for algorithms designed for 2 threads, and with 3 for all others. We restrict ourselves to at most 3 threads because, due to the state-space explosion problem, even models with only 3 threads frequently take hours or even days to check these properties on.

We list the origin of each algorithm in the table; the results of verifying our proposed alternate versions are indicated by “alt.”. For the algorithms we discuss in detail, we include their pseudocode. Therein we merely present the entry and exit protocols of an algorithm, separated by the instruction critical section. Implicitly these instructions alternate with the non-critical section, and may be repeated indefinitely. We use $N$ for the number of threads. As identifiers for threads, we use the integers $0\mathrm{\dots }N-1$. So $𝕋=\{0,\mathrm{\dots },N-1\}$. When presenting pseudocode, we give the algorithm for an arbitrary thread $i$. When $N=2$, we use the shorthand notation $j=1-i$.

In the subsequent sections, we discuss the most interesting results. Pseudocode and further discussion of the algorithms not covered here appear in [28, Appendix I].

To the best of our knowledge, we are the first to do automatic verification of mutual exclusion algorithms while incorporating both which operations can block each other and the effects of overlapping write operations. The two elements have been considered separately previously.

In [14], starvation-freedom of Peterson’s algorithm with atomic registers is checked using mCRL2 under the justness assumption. Two different concurrency relations are considered, which are similar to our $⌣_{}^{\bullet }{}_S{}^{}$ and $⌣_{}^{\bullet }{}_A{}^{}$.

There have been many formal verifications of mutual exclusion algorithms with atomic registers [11, 43, 29]. Non-atomic registers have been covered less frequently, and their verification is often restricted to single-writer registers [41, 15]. The safety properties of mutual exclusion algorithms with MWMR non-atomic registers were verified using mCRL2 in [50]. In several papers by Nigro, including [44, 45], safety and liveness verification with MWMR non-atomic registers has been done using UPPAAL.

A major drawback of our approach is that we only consider a small number of parallel threads. There has been much work in the literature on parametrised verification, where the correctness of an algorithm is established for an arbitrary number of threads [13, 22, 55, 12]. Where these techniques handle liveness, it is under forms of weak or strong fairness, not justness. To our knowledge, these techniques have not yet been applied in the context of non-atomic registers. While several papers on parametrised verification, such as [2, 1], mention dropping the atomicity assumption, this refers to evaluating existential and universal conditions on all threads in a single atomic operation, rather than atomicity of the registers.

In [7, 31, 32] and other work by Hesselink, interactive theorem proving with the proof assistant PVS is used to check safety and liveness properties (under fairness) of mutual exclusion algorithms for an arbitrary number of threads with non-atomic registers. To our knowledge, the case of writes overlapping each other has not been covered with this technique.

When it comes to analysing the correctness of algorithms, particularly when considering non-atomic registers, behavioural reasoning is often insufficient. Mistakes can be subtle, and may depend on edge-cases that are easily overlooked. Model checking is a solution here; we formally model the threads executing the algorithm, as well as the registers through which they communicate, and the entire state-space is searched for possibly violations of correctness properties. In this work, we verify a large number of mutual exclusion algorithms using the model checking toolset mCRL2. We expand on previous work by checking liveness properties – deadlock freedom and starvation freedom – in addition to the main safety property. To circumvent spurious violating paths in our models, we incorporate the completeness criterion justness into our verifications. We checked algorithms under six different memory models, where a memory model is a combination of a register model (safe, regular, or atomic) and a model of which register access operations can block each other. The former dimension we capture in the models themselves, by modelling the behaviour of the three types of register. The latter, we capture in the concurrency relations employed as part of justness. We found a number of interesting violations of correctness properties, and in some cases could suggest improvements to algorithms to fix these violations. We find that there are several algorithms that satisfy all three properties for four out of six memory models. For three threads, this is accomplished by the fixed version of Aravind’s BLRU algorithm and Lamport’s 3-bit algorithm. If we also consider algorithms for just two threads, then Anderson’s algorithm and the fixed version of Szymanski’s 3-bit linear wait algorithm also meet this bar. We also considered an algorithm to turn deadlock-free algorithms into starvation-free ones, and experimentally confirmed that it indeed works for Dekker’s algorithm made RW-safe and Lamport’s 1-bit algorithm.