1 Introduction

Safety and liveness properties are the cornerstones of concurrent program verification. While safety and liveness are complementary, verification methodologies for the latter tend to be more complicated for two reasons. First, checking safety properties, in many cases, can be reduced to the (simple) reachability problem, while checking liveness properties usually amounts to checking repeated reachability of states [47]. Second, concurrency comes with an inherent scheduling non-determinism, i.e., at each step, the scheduler may non-deterministically select the next process to run. Therefore, liveness properties need to be accompanied by appropriate fairness conditions on the scheduling policies to prohibit trivial blocking behaviors [42]. In the example of two processes trying to acquire a lock, demonic non-determinism [20] may always favour one process over the other, leading to starvation.

Despite the gap in complexity, the verification of liveness properties has attracted much research in the context of programs running under the classical Sequential Consistency (SC) [40]. An execution of a program under SC is a non-deterministically chosen interleaving of its processes’ atomic operations. A write by any given process is immediately visible to all other processes, and reads are made from the most recent write to the memory location in question. SC is (relatively) simple since the only non-determinism comes from interleaving.

Weak memory models forego the fundamental SC guarantee of immediate visibility of writes to optimize for performance. More precisely, a write operation by a process may asynchronously be propagated to the other processes. The delay could be owed to physical buffers or caches, or could simply be a virtual one thanks to instruction reorderings allowed by the semantics of the programming language. Hence we have to contend with a (potentially unbounded) number of write operations that are “in transit”, i.e., they have been issued by a process but they have yet to reach the other processes. In this manner, weak memory introduces a second source of non-determinism, namely memory non-determinism, reflecting the fact that write operations are non-deterministically (asynchronously) propagated to the different processes. Formal models for weak memory, ranging from declarative models [8, 21, 35, 39, 41] to operational ones [15, 30, 43, 46] make copious use of non-determinism (non-determinism over entire executions in the case of declarative models and non-deterministic transitions in the case of operational models). While we have seen extensive work on verifying safety properties for program running under weak memory models, the literature on liveness for programs running under weak memory models is relatively sparse, and it is only recently we have seen efforts in that direction [5, loop.

Fig. 1.
figure 1

Does this program always terminate? Only if we can guarantee that the process to the right will eventually be scheduled to read when \(\textsf{x}= 1\).

Full size image

Stronger fairness conditions such as transition fairness, and probabilistic fairness [11, 27] can help avoid this problem. They imply that any transition enabled infinitely often is also taken infinitely often (with probability one in the case of probabilistic fairness). Transition fairness eliminates demonic scheduler non-determinism, and hence it is an appropriate notion of fairness in the case o  SC. However, it is unable to eliminate demonic memory non-determinism. The reason is that transition fairness allows runs of the programs where write events occur at a higher frequency than the frequency in which they are propagated to the processes. This means that, in the long run, a process may only see its own writes, potentially preventing its progress and, therefore, the system’s progress as a whole. This scenario is illustrated in Fig. 2.

Fig. 2.
figure 2

This program is guaranteed to terminate under any model only if pending propagation is guaranteed to not accumulate unboundedly: e.g. in TSO, each process may never see the other’s writes due to an overflowing buffer.

Full size image

To deal with memory non-determinism, we exploit the fact that the sizes of physical buffers or caches are bounded, and instruction reorderings are bounded in scope. Therefore, in any practical setting, the number of writes in transit at a given moment cannot be unbounded indefinitely. This is what we seek to capture in our formalism. Based on this observation, we propose three new notions of fairness that (surprisingly) all turn out to be equivalent in the context of liveness. First, we introduce boundedness fairness which only considers runs of the system for which there is a bound b on the number of events in transit, in each configuration of the run. Note that the value of b is arbitrary (but fixed for a given run). Bounded fairness is apposite: (i) it is sufficiently strong to eliminate demonic memory non-determinism, and (ii) it is sufficiently weak to allow all reasonable behaviors (as mentioned above, practical systems will bound the number of transient messages). Since we do not fix the value of the bound, this allows parameterized reasoning, e.g., about buffers of any size: our framework does not depend on the actual value of the bound, only on its mere existence. Furthermore, we define two additional related notions of fairness for memory non-determinism. The two new notions rely on plain configurations: configurations in which there are no transient operations (all the writes operations have reached all the processes). First, we consider plain fairness: along each infinite run, the set of plain configurations is visited infinitely often, and then define the probabilistic version: each run almost surely visits the set of plain configurations. We show that the three notions of fairness are equivalent (in Sect. 4, we make precise the notion of equivalence we use).

After we have defined our fairness conditions, we turn our attention to the verification problem. We show that verifying the repeated reachability under the three fairness conditions, for a given memory model m, is reducible to the simple reachability under m. Since our framework does not perform program transformations we can prove liveness properties for program P through proving simple reachability on the same program P. As a result we obtain two important sets of corollaries: if the simple reachability problem is decidable for m, then the repeated reachability problem under the three fairness conditions are also decidable. This is the case when the memory model m is TSO, PSO, SRA, etc. Even when the simple reachability problem is not decidable for m, e.g., when m is RA, RMO, we have still succeeded to reduce the verification of liveness properties under fairness conditions to the verification of simple probability. This allows leveraging proof methodologies developed for the verification of safety properties under these weak memory models (e.g., [22, 29]).

Having identified the fairness conditions and the verification problem, there are two potential approaches, each with its advantages and disadvantages. We either instantiate a framework for individual memory models one after one or define a general framework in which we can specify multiple memory models and apply the framework “once for all”. The first approach has the benefit of making each instantiation more straightforward, however, we always need to translate our notion of fairness into the specific formulation. In the second approach, although we incur the cost of heavier machinery, we can subsequently take for granted the fact that the notion of fairness is uniform across all models, and coincides with our intuition. This allows us to be more systematic in our quest to verify liveness. In this paper, we have thus chosen to adopt the second approach. We define a general model of weak memory models in which we represent write events as sequences of messages ordered per variable and process. We augment the message set with additional conditions describing which messages have reached which processes. We use this data structure to specify our fairness conditions and solve our verification problems. We instantiate our framework to apply our results to a wide variety of memory models, such as RMO [12], FIFO consistency, RA, SRA, WRA [34, 35], TSO [13], PSO, StrongCOH (the relaxed fragment of RC11) [30], and SC [40].

In summary, we make the following contributions

  • Define new fairness conditions that eliminate demonic memory non-determinism.

  • Reduce checking the repeated reachability problem under these fairness conditions to the simple reachability problem.

  • Introduce a general formalism for weak memory models that allows applying our results uniformly to a broad class of memory models.

  • Prove the decidability of liveness properties for models such as TSO, PSO, SRA, WRA, StrongCOH, and opening the door for leveraging existing proof frameworks for simple reachability for other models such as RA.

We give an overview of a wide landscape of memory models in Sect. 3.3, and provide a high level explanation of the versatility of our framework.

Structure of the Paper. We begin by casting concurrent programs as transition systems in Sect. 2. In Sect. 3, we develop our framework for the memory such that the desired fairness properties can be meaningfully defined across several models. In Sect. 4, we define useful fairness notions and prove their equivalence. Finally, in Sect. 5 we show how the liveness problems of repeated control state reachability reduce to the safety problem of control state reachability, and obtain decidability results. A full version of this paper is available at [6].

2 Modelling Concurrent Programs

We consider concurrent programs as systems where a set of processes run in parallel, computing on a set of process-local variables termed as registers and communicating through a set of shared variables. This inter-process communication, which consists of reads from, writes to, and atomic compare-and-swap operations on shared variables, is mediated by the memory subsystem. The overall system can be visualized as a composition of the process and memory subsystems working in tandem. In this section we explain how concurrent programs naturally induce labelled transition systems.

2.1 Labelled Transition Systems

A labelled transition system is a tuple \(\mathcal {T}= \langle \Gamma , \rightarrow , \Lambda \rangle \) where \(\Gamma \) is a (possibly-infinite) set of configurations, \(\rightarrow \subseteq \Gamma \times \Lambda \times \Gamma \) is a transition relation, and \(\Lambda \) is the set of labels that annotate transitions. We also refer to them as annotations to disambiguate from instruction labels. We write \(\gamma \xrightarrow {l} \gamma '\) to denote that \((\gamma , l, \gamma ') \in \rightarrow \), in words that there is a transition from \(\gamma \) to \(\gamma '\) with label l. We denote the transitive closure of \(\rightarrow \) by \(\xrightarrow {*}\), and the k-fold self-composition (for \(k \in {\mathbb N}\)) as \(\xrightarrow {k}\).

Runs and Paths. A (possibly infinite) sequence of valid transitions \(\rho = \gamma _1 \rightarrow \gamma _2 \rightarrow \gamma _3 \cdots \) is called a run. We say that a run is a \(\gamma \)-run if the initial configuration in the run is \(\gamma \), and denote the set of \(\gamma \)-runs as \(\textsf{Runs}(\gamma )\). We call a (finite) prefix of a run as a path. In some cases transition systems are initialized, i.e. an initial set \(\Gamma _\textsf{init}\subseteq \Gamma \) is specified. In such cases, we call runs starting from some initial configuration (\(\gamma _1 \rightarrow \gamma _2 \rightarrow \gamma _3 \dots \) with \(\gamma _1 \in \Gamma _\textsf{init}\)) as initialized runs.

2.2 Concurrent Programs

The sequence of instructions executed by each process is dictated by a concurrent program, which induces a process subsystem. We begin by formulating the notion of a program. We assume a finite set \(\mathbb {P}\) of processes that operate over a (finite) set \(\mathbb {X}\) of shared variables. Figure 3 gives the grammar for a small but general assembly-like language that we use for defining the syntax of concurrent programs. A program instance, \(\textsf{prog}\) is described by a set of shared variables, , followed by the codes of the processes, . Each process \(p\in \mathbb {P}\) has a finite set \(\textsf{Regs}(p)\) of (local) registers. We assume w.l.o.g. that the sets of registers of the different processes are disjoint, and define \(\textsf{Regs}(\textsf{prog}):=\cup _{p\in \mathbb {P}}\textsf{Regs}(p)\). We assume that the data domain of both the shared variables and registers is a finite set \(\mathbb {D}\), with a special element \(\textsf{0}\in \mathbb {D}\). The code of a process starts by declaring its set of registers, , followed by a sequence of instructions.

Fig. 3.
figure 3

A simple programming language.

Full size image

An instruction \(\textsf{i}\) is of the form \(\textsf{l}: \texttt {stmt}\) where \(\textsf{l}\) is a unique (across all processes) instruction label that identifies the instruction, and \(\texttt {stmt}\) is a statement. The labels comprise the set of values the program counters of the processes may take. The problems of (repeated) instruction label reachability, which ask whether a section of code is accessed (infinitely often), are of importance to us.

Read () and write () statements read the value of a shared variable into a register, and write the value of a register to a shared variable respectively. The \(\textsf{CAS}\) statement is the compare-and-swap operation which atomically executes a read followed by a write. We consider a non-blocking version of the \(\textsf{CAS}\) operation which returns a boolean indicating whether the operation was successful (the expected value was read and atomically updated to the new value). The write is performed only if the read matches the expected value.

We assume a set of expressions containing a set of operators applied to constants and registers without referring to the shared variables. The statement updates the value of register by evaluating expression . We exact set of expressions is orthogonal to our treatment, and hence left uninterpreted. The -statement has its usual interpretation, and control flow commands such as , , and -statements, can be encoded with branching and -statements as usual.

2.3 Concurrent Programs as Labelled Transition Systems

We briefly explain the abstraction of a concurrent program as a labelled transition system. The details for the process component, i.e. evolution of the program counter and register contents, follow naturally. The key utility of this approach lies in the modelling of the memory subsystem, which we devote §3 to.

Configurations. A configuration \(\gamma \) is expressed as a tuple \(\langle (L, R), \gamma _\texttt{m}\rangle \), where L maps processes to their current program counter values, R maps registers to their current values, and \(\gamma _\texttt{m}\) captures the current state of the (weak) memory.

Transitions. In our model, a step in our system is either: (a) a silent memory update, or (b) a process executing its current instruction. In case (a), only the memory component \(\gamma _\texttt{m}\) of \(\gamma \) changes. The relation is governed by the definition of the memory subsystem. In case (b), if the instruction is the terminal one, or assigns an expression to a register, or a conditional, then only the process component (L, R) of \(\gamma \) changes. Here, the relation is obvious. Otherwise, the two components interact via a read, write or \(\textsf{CAS}\), and both undergo changes. Here again, the relation is governed by what the memory subsystem permits.

Annotations. Silent memory update steps are annotated with \(\texttt{m}: \texttt{Upd}\). Transitions involving process \(p\) executing an instruction that does not involve memory are annotated with \(p: \bot \). On the other hand, \(p:\texttt{R}(\textsf{x},\textsf{d})\), \(p:\texttt{W}(\textsf{x},\textsf{d})\), \(p:\texttt{CAS}(\textsf{x},\textsf{d},\textsf{d}',\textsf{b})\) represent reads, writes and CAS operations by \(p\) respectively. The annotations indicate the variable and the associated values.

To study this transition system, one must understand which transitions, annotated thus, are enabled. For this, it is clear that we must delve into the details of the memory subsystem.

3 A Unified Framework for Weak Memory Models

In this section, we present our unified framework for representing weak memory models. We begin by describing the modelling aspects of our framework at a high level.

We use a message-based framework, where each write event generates a message. A process can use a write event to justify its read only if the corresponding message has been propagated to it by the memory subsystem. The total chronological order in which a process p writes to variable \(\textsf{x}\) is given by (per-location program order). We work with models where the order of propagation is consistent with . This holds for several models of varying strengths. This requirement allows us to organise messages into per-variable, per-process channels. We discuss these aspects of the framework in Sect. 3.1. Weak memory models define additional causal dependencies over . Reading a message may cause other messages it is dependent on to become illegible. We discuss our mechanism to capture these dependencies in Sect. 3.2. The strength of the constraints levied by causal dependencies varies according to memory model. In Sect. 3.3, we briefly explain how our framework allows us to express causality constraints of varying strength, by considering a wide landscape of weak memory models. We refer the reader to [6] for the technical details of the instantiations.

3.1 Message Structures

Message. A write by a process to a variable leads to the formation of a message, which, first and foremost records the value being written. In order to ensure atomicity, a message also records a boolean denoting whether the message can be used to justify the read of an atomic read-write operation, i.e. \(\textsf{CAS}\). Finally, to help with the tracking of causal dependencies generated by read events, a message records a set of processes that have sourced a read from it. Thus, a message is a triple and we define the set of messages as: \(\textsf{Msgs}= \mathbb {D}\times \mathbb {B} \times 2^{\mathbb {P}}\).

Channels. A channel \(\textsf{e}(\textsf{x}, p)\) is the sequence of messages corresponding to writes to \(\textsf{x}\) by process \(p\). The total order of these writes naturally induces the channel order. By design, we will ensure that the configuration holds finitely many messages in each channels. We model each channel as a word over the message set: \(\textsf{e}(\textsf{x}, p) \in \textsf{Msgs}^*\). A message structure is a collection of these channels: \(\textsf{e}: \mathbb {X}\times \mathbb {P}\rightarrow \textsf{Msgs}^*\).

3.2 Ensuring Consistency of Executions

Memory models impose constraints restricting the set of message that can be read by a process. The framework uses state elements that help enforce these constraints. These elements reference positions within each channel which is something that we now discuss.

Channel Positions. The channel order provides the order of propagation of write messages to any process (which in turn is aligned with ). Thus, for any process \(p'\), channel \(\textsf{e}(\textsf{x}, p)\) is partitioned into a prefix of messages that are outdated, a null or singleton set of messages that can be used to justify a read, and a suffix of messages that are yet to be propagated. In order to express these partitions, we need to identify not only nodal positions, but also to internodes (space between nodes). To this end, we index channels using the set \(\mathbb {W}= {\mathbb N}\cup {\mathbb N}^+\). Positions indexed by \({\mathbb N}\) denote nodal positions (with a message), while positions indexed with \({\mathbb N}^+\) denote internodes. For a channel of length n, the positions are ordered as: \(\top = 0^+< 1< 1^+< 2 \cdots< n < n^+ = \bot \). A process can read from the message located at \(\textsf{e}(\cdot , \cdot )[i]\) for \(i \in {\mathbb N}\).

Frontier. With respect to a given process, a message can either have been propagated but not readable, propagated and readable, or none. Since the propagation order of messages follows channel order, the propagated set of messages forms a prefix of the channel. This prefix-partitioning is achieved by a map . If is an internode (of form \(i^+\)) then the message \(\textsf{v}= \textsf{e}[i]\) has been propagated to \(p\), but cannot be read because it is outdated. On the other hand, if , then the message \(\textsf{e}[i]\) can be read by the process. In Fig. 4, equal \(\textsf{v}_1^+/\textsf{v}_2/\textsf{v}_3\) respectively (the colored nodes). Consequently, the message at index \(\textsf{v}\) (or the ones before it) are unreadable (denoted by the pattern). On the other hand the messages at \(\textsf{v}_2, \textsf{v}_3\) are readable.

Fig. 4.
figure 4

Frontier and source.

Full size image
Fig. 5.
figure 5

Constraint.

Full size image

Source. Given process \(p\) and variable \(\textsf{x}\), the process potentially can source the read from any of the \(|\mathbb {P}|\) channels on \(\textsf{x}\). The second state element, performs arbitration over this choice of read sources: \(p\) can read \(\textsf{v}\) only if . In Fig. 4, while both nodes \(\textsf{v}_2, \textsf{v}_3\) are not outdated, , making \(\textsf{v}_3\) the (checkered) node which \(p_1\) reads from.

Constraint. The element tracks causal dependencies between messages. For each message m, and channel, it identifies the last message on the channel that is a causal predecessor of m. It is defined as a map . Figure 5 illustrates possible pointers for message node \(\textsf{v}_3\) in the context of the channel configuration in Fig. 4.

Garbage Collection. The state marks the last messages in each channel that can be read by a process. Messages that are earlier than the of all processes can be effectively eliminated from the system since they are illegible. We call this garbage collection (denoted as \(\textsf{GC}\)).

The overall memory configuration,

figure ai

consists of the message structure along with the consistency enforcing state.

Read Transition. Our framework allows a unified read transition relation which is independent of the memory model that we work with. We now discuss this transition rule which is given in Fig. 6. Suppose process \(p\) is reading from variable \(\textsf{x}\). First, we identify the arbitrated process \(p_s\) which is read from using the state. Then we pick the message on the \((\textsf{x}, p_s)\) channel which the of \(p\) points to. Note that this must be a node of form \({\mathbb N}\). The read value is the value in this message. Finally, we update the to reflect the fact that all messages in the causal prefix of the read message have propagated to \(p\).

Fig. 6.
figure 6

The read transition, common to all models across the framework. For \(\gamma \in \Gamma _\texttt{m}\), represent the respective components of \(\gamma \). For a node \(\textsf{v}\in \textsf{Msgs}\), \(\textsf{v}.\textsf{value}\in \mathbb {D}\) represents the written value in the message node \(\textsf{v}\).

Full size image
Fig. 7.
figure 7

SB

Full size image

Example 1 (Store Buffer (SB))

Fig. 7 shows the Store Buffer (SB) litmus test. The annotated outcome of store buffering is possible in all WRA/RA/SRA/TSO models. Right after \(p_1\) (resp. \(p_2\)) has performed both its writes to \(\textsf{x}\) (resp. \(\textsf{y}\)), we have \(\textsf{e}(\textsf{y}, p_2) = \top \textsf{v}^0_\textsf{y}\textsf{v}^1_\textsf{y}\bot \), and \(\textsf{e}(\textsf{x}, p_1) = \top \textsf{v}^0_\textsf{x}\textsf{v}^1_\textsf{x}\bot \).

This example illustrates how weak memory models allow non-deterministic delays the propagation of messages. In this example, , and , both processes see non-recent messages. On the other hand, the annotated outcomes are observed if and .

We now turn to a toy example (Fig. 8) to illustrate the dependency enforcing and book-kee** mechanisms we have introduced.

Example 2

Consider an program with two shared variables, \(\textsf{x}, \textsf{y}\), and two processes, \(p_1\), \(p_2\). We omit the channel \(\textsf{e}(p_2, \textsf{y})\) for space. Process \(p_1\)’s frontiers are shown in violet, \(p_2\)’s frontiers are shown in orange. We begin with the first memory configuration. The arrow depicts . This situation can arise in a causally consistent model where the writer of \(\textsf{v}_1\) was aware of \(\textsf{v}_2\) before writing \(\textsf{v}_1\). The first transition shows \(p_2\) updating and moving its (to \(\textsf{v}_1\)). This results in a redundant node (\(\textsf{v}_3\) in hashed texture) since the of both \(p_1\) and \(p_2\) has crossed it. This is cleaned up by \(\textsf{GC}\). Now, \(p_2\) begins its read from \(\textsf{v}_1\). Reading \(\textsf{v}_1\), albeit on \(\textsf{x}\), makes all writes by \(p_1\) to \(\textsf{y}\) prior to \(\textsf{v}_2\) redundant. When \(p_2\) reads \(\textsf{v}_1\), its frontier on \(\textsf{e}(\textsf{y}, p_1)\) advances as prescribed by , as shown in the fourth memory configuration. Note that this makes another message (\(\textsf{v}_4\)) redundant: all frontiers are past it. Once again, \(\textsf{GC}\) discards the message obtaining the last configuration.

Fig. 8.
figure 8

Update, in action during a read, and garbage collection

Full size image

3.3 Instantiating the Framework

Versatility of the Framework. The framework we introduce can be instantiated to RMO [12], FIFO consistency, RA, SRA, WRA [34, 35], TSO [13], PSO, StrongCOH (the relaxed fragment of RC11) [30], and SC [40].

This claim is established by constructing semantics for each of these models using the components that we have discussed. We provide a summary of the insights, and defer the technical details to the full version [6].

Fig. 9.
figure 9

Memory models, arranged by their strength. An arrow from A to B denotes that B is strictly more restrictive than A. A green check (resp. red cross) denotes the control state reachability is decidable (resp. undecidable). (Color figure online)

Full size image

We briefly explain how our framework accounts for the increasing restrictive strength of these memory models. The weakest of these is RMO, which only enforces . There are no other causal dependencies, and thus for any message the on other channels is \(\top \). RMO can be strengthened in two ways: StrongCOH does it by requiring a total order on writes to the same variable, i.e. . Here the is nontrivial only on channels of the same variable. On the other hand, FIFO enforces consistency with respect to the program order. Here, the is nontrivial only on channels of the same process. WRA strengthens FIFO by enabling reads to enforce causal dependencies between write messages. This is captured by the non-trivial , and we note that (the set of processes to have sourced a read from a message) plays a crucial role here. RA enforces the of StrongCOH as well as the causal dependencies of WRA. PSO strengthens StrongCOH by requiring a stronger precondition on the execution of an atomic read-write. More precisely, in any given configuration, for every variable, there is at most one write message that can be used to source a \(\textsf{CAS}\) operation, i.e. with the \(\textsf{CAS}\) flag set to true. SRA and TSO respectively strengthen RA and PSO by doing away with write races. Here, the Boolean \(\textsf{CAS}\) flag in messages is all-important as an enforcer of atomicity. TSO strengthens SRA in the same way as PSO strengthens StrongCOH. Finally, when we get to SC, the model is so strong that all messages are instantly propagated. Here, for any message, the pointer on other channels is \(\bot \).

4 Fairness Properties

Towards the goal of verifying liveness, we use the framework we developed to introduce fairness properties in the the classical and probabilistic settings in Sect. 4.1 and Sect. 4.2 respectively. Our approach thus has the advantage of generalising over weak memory. In Sect. 4.3 we relate these fairness properties in the context of repeated control state reachability: a key liveness problem.

4.1 Transition and Memory Fairness

In this section, we consider fairness in the classical (non-probabilistic) case. We begin by defining transition fairness, which [11] is a standard notion of fairness that disallows executions which neglect certain transitions while only taking others. For utility in weak memory liveness, we then augment transition fairness to meet practical assumptions on the memory subsystem. Transition fairness and probabilistic fairness are intrinsically linked [27, Section 11]. Our augmentations are designed to carry over to the probabilistic domain in the same spirit.

Definition 1

(Transition fairness, [11]). We say that a program execution is transition fair if for every configuration that is reached infinitely often, each transition enabled from it is also taken infinitely often.

We argued the necessity of transition fairness in the introduction; however, it is vacuously satisfied by an execution that visits any configuration only finitely often. This could certainly be the case in weak memory, where there are infinitely many configurations. To make a case for the implausibility of this scenario, we begin by characterising classes of weak memory configurations.

Definition 2

(Configuration size). Let \(\gamma \) be a program configuration with memory component . We denote the configuration size by \(\textsf{size}(\gamma )\) and it is defined as \(\sum _\textsf{x}\sum _p\textsf{len}(\textsf{e}(\textsf{x}, p))\), i.e. the total number of messages in the message structure.

Intuitively, the size of the configuration is the number of messages “in transit”, and hence a measure of the weakness of the behaviour of the execution. We note that overly weak behaviour is rarely observed in practice [23, 45]. For instance, instruction reorderings that could be observed as weak behaviour are limited in scope. Another source of weak behaviour is the actual reading of stale values at runtime. However, the hardware (i.e. caches, buffers, etc.) that stores these values is finite, and is typically flushed regularly. Informally, the finite footprint of the system architecture (eg. micro-architecture) implies a bound, albeit hard to compute, on the size of the memory subsystem. Thus, we use the notion of configuration size to define:

Definition 3

(Size Bounded Executions). An execution \(\gamma _0, \gamma _1, \dots \) is said to be size bounded, if there exists an N such that for all \(n \in \mathbb {N}\), \(\textsf{size}(\gamma _n) \le N\). If this N is specified, we refer to the execution as N-bounded.

Already, the requirement of size-boundedness enables our system to refine our practical heuristics. However, if the bound N is unknown, it isn’t immediately clear how this translates into a technique for liveness verification. We will now use the same rationale to motivate and develop an alternate augmentation which lends itself more naturally to algorithmic techniques. Recall that we intuitively relate the size of the configuration to the extent of weak behaviour. Now, consider Sequential Consistency, the strongest of the models. All messages are propagated immediately, and hence, the configuration has minimal size throughout. We call minimally sized configurations plain, and they are of particular interest to us:

Definition 4

(Plain message structure). A message structure \((\textsf{V}, \textsf{msgmap}, \textsf{e})\) is called plain, if for each variable \(\textsf{x}\), \(\sum _p\textsf{len}(\textsf{e}(\textsf{x}, p)) = 1\).

Drawing a parallel with SC, one could reason that the recurrence of plain configurations is a hallmark of a system that doesn’t exhibit overly weak behaviour. This is captured with the following fairness condition.

Definition 5

(Repeatedly Plain Executions). An execution \(\gamma _0, \gamma _1, \dots \) is said to be repeatedly plain, if \(\gamma _i\) is a plain configuration for infinitely many i.

Following the memory transition system introduced in Sect. 2 and Sect. 3, we observe that every configuration has a (finite) path to some plain configuration (by performing a sequence of update steps). Hence, if a configuration is visited infinitely often in a fair execution, a plain configuration will also be visited infinitely often. Consequently, size bounded transition fair runs are also repeatedly plain transition fair.

4.2 Probabilistic Memory Fairness

Problems considered in a purely logical setting ask whether all executions satisfying a fairness condition fulfill a liveness requirement. However, if the answer is negative, one might be interested in quantifying the fair executions which do not repeatedly reach the control state. We perform this quantification by considering the probabilistic variant of the model proposed earlier, and defining fairness analogously as a property of Markov Chains.

Markov chains A Markov chain is a pair \(\mathcal {C}= \langle {\Gamma , \texttt{M}\rangle }\) where \(\Gamma \) is a (possibly-infinite) set of configurations and \(\texttt{M}\) is the transition matrix which assigns to each possible transition, a transition probability: \(\texttt{M}: \Gamma \times \Gamma \rightarrow [0, 1]\). Indeed, this matrix needs to be stochastic, i.e., \(\sum _{\gamma ' \in \Gamma } \texttt{M}(\gamma , \gamma ') = 1\) should hold for all configurations.

We can convert our concurrent program transition (Sect. 2) into a Markov chain \(\texttt{M}\) by adding probabilities to the transitions. We assign \(\texttt{M}(\gamma , \gamma ')\) to a nonzero value if and only if the transition \(\gamma \rightarrow \gamma '\) is allowed in the underlying transition system. Markov Chain executions are, by construction, transition fair with probability 1. We now present the analog of the repeatedly plain condition.Footnote 1

Definition 6

(Probabilistic Memory Fairness. A Markov chain is considered to satisfy probabilistic memory fairness if a plain configuration is reached infinitely often with probability one.

This parallel has immense utility because verifying liveness properties for a class of Markov Chains called Decisive Markov Chains is well studied. [7] establishes that the existence of a finite attractor, i.e. a finite set of states F that is repeatedly reached with probability 1, is sufficient for decisiveness. The above definition asserts that the set of plain configurations is a finite attractor.

4.3 Relating Fairness Notions

Although repeatedly plain transition fairness is weaker than size bounded transition fairness and probabilistic memory fairness, these three notions are equivalent with respect to canonical liveness problems, i.e. repeated control state reachability and termination. The proof we present for repeated reachability can be adapted for termination.

Theorem 1

There exists \(N_0 \in \mathbb {N}\) such that for all \(N \ge N_0\), the following are equivalent for any control state (program counters and register values) c:

  1. 1.

    All repeatedly plain transition fair runs visit c infinitely often.

  2. 2.

    All N-bounded transition fair runs visit c infinitely often.

  3. 3.

    c is visited infinitely often under probabilistic memory fairness with probability 1.

Proof

For each \(N \in \mathbb {N}\), we construct a connectivity graph \(\mathcal {G}_N\). The vertices are the finitely many plain configurations \(\gamma \), along with the finitely many control states c. We draw a directed edge from \(\gamma _i\) to \(\gamma _j\), if \(\gamma _j\) is reachable from \(\gamma _i\) via configurations of size at most N. We additionally draw an edge from a plain configuration \(\gamma \) to control state c iff c is reachable from \(\gamma \) via configurations of size at most N. We similarly construct a connectivity graph \(\mathcal {G}\) without bounds on intermediate configuration sizes. We note:

  1. 1.

    There are only finitely many possibilities for \(\mathcal {G}_N\)

  2. 2.

    As N increases, edges can only be added to \(\mathcal {G}_N\). This guarantees saturation.

  3. 3.

    Any witness of reachability is necessarily finite, hence the saturated graph is the same as \(\mathcal {G}\), i.e. for all sufficiently large N, \(\mathcal {G}_N = \mathcal {G}\)

Since plain configurations are attractors, the graph \(\mathcal {G}\) is instrumental in deciding repeated control state reachability. Consider the restriction of \(\mathcal {G}\) to plain configurations, i.e. \(\mathcal {G}_\Gamma \). Transition fairness (resp. Markov fairness) implies that \(\gamma \) is visited infinitely often (resp. with probability 1) only if it is in a bottom strongly connected component (scc). In turn any control state c will be guaranteed to be reached infinitely often if and only if it is reachable from every bottom scc of \(\mathcal {G}_\Gamma \). The if direction follows using the transition fairness and attractor property, while the converse follows by simply identifying a finite path to a bottom scc from which c isn’t reachable. The equivalence follows because the underlying graph is canonical for all three notions of fairness.

5 Applying Fairness Properties to Decision Problems

In this section, we show how to decide liveness as a corollary of the proof of Theorem 1. We begin by noting that techniques for termination are subsumed by those for repeated control state reachability. This is because termination is not guaranteed iff one can reach a plain configuration from which a terminal control state is inaccessible. Hence, in the sequel, we focus on repeated control state reachability.

5.1 Deciding Repeated Control State Reachability

We observe that under the fairness conditions we defined, liveness, i.e. repeated control state reachability reduces to a safety query.

Problem 1 (Repeated control state reachability)

Given a control state (program counters and register values) c, do all infinite executions (in the probabilistic case, a set of measure 1) satisfying fairness condition \(\mathcal {A}\) reach c infinitely often?

Problem 2 (Control state reachability)

Given a control state c and a configuration \(\gamma \), is \((c, \gamma _\texttt{m})\) reachable from \(\gamma \) for some \(\gamma _\texttt{m}\)?

Theorem 2

Problem 1 for repeatedly fair transition fairness and probabilistic memory fairness reduces to Problem 2. Moreover, the reduction can compute the \(N_0\) from Theorem 1 such that it further applies to size bounded transition fairness.

Proof

This follows by using Problem 2 to compute the underlying connectivity graph \(\mathcal {G}\) from the proof of Theorem 1. A small technical hurdle is that plain configuration reachability is not the same as control state reachability. However, the key to encode this problem as a control state query is to use the following property: for a configuration \(\gamma \) and a message m (\(\in \textsf{e}(\textsf{x}, p)\)), if for every process \(p'\), m is not redundant (formally, ), then there exists a plain configuration \(\gamma '\) containing m such that \(\gamma '\) is reachable from \(\gamma \) via a sequence of update steps. The plan, therefore, is to read and verify whether the messages desired in the plain configuration are, and remain accessible to all processes. Finally, the computation of \(N_0\) follows by enumerating \(\mathcal {G}_N\).

5.2 Quantitative Control State Repeated Reachability

We set the context of a Markov chain \(\mathcal {C}= \left\langle \Gamma , \texttt{M}\right\rangle \) that refines the underlying the transition system induced by the program. We consider is the quantitative variant of repeated reachability, where instead of just knowing whether the probability is one or not, we are interested in computing it.

Problem 3 (Quantitative control state repeated reachability)

Given a control state c and an error margin \(\epsilon \in \mathbb {R}\), find a \(\delta \) such that for Markov chain \(\mathcal {C}\),

 

We refer the reader to [6] for details on the standard reduction, from which the following result follows:

Theorem 3

If Problem 2 is decidable for a memory model, then Problem 3 is computable for Markov chains that satsify probabilistic memory fairness.

5.3 Adapting Subroutines to Our Memory Framework

We now briefly sketch how to adapt known solutions to Problem 2 for PSO, TSO, StrongCOH, WRA and SRA to our framework.

PSO and TSO. Reachability between plain configurations (a special case of Problem 2) under these models has already been proven decidable [12]. The store buffer framework is similar to the one we describe, and hence the results go through. Moreover, [5, Lemmas 3, 4] shows the decidability of our Problem 2 for TSO. The same construction, which uses an augmented program to reduce to ex-plain configuration reachability, works for PSO as well.

StrongCOH. Decidability of reachability under StrongCOH is shown in [1]. The framework used, although quite different in notation, is roughly isomorphic to the one we propose. The relaxed semantics of StrongCOH allow the framework to be set up as a WSTS [2, 26], which supports backward reachability analysis, yielding decidability. Backward reachability gives an upward closed set of states that can reach a target label. Checking whether an arbitrary state is in this upward closed set requires a comparison with only the finitely many elements in the basis. This solves Problems 2.

WRA and SRA. Decidability of reachability under WRA and SRA has recently been shown in [34]. The proof follows the WSTS approach, however, the model used in the proof has different syntax and semantics from the one we present here. However, a reconciliation is possible, and we briefly sketch it here. A state in the proof model is a map from processes to potentials. A potential is a finite set of finite traces that a process may execute. These proof-model states are well-quasi-ordered and operating on them sets up a WSTS. Backward reachability gives us a set of maps from processes to potentials that allow us to reach the target label. The key is to view a process-potential map as a requirement on our message based configuration. Higher a map in the wqo, stronger the requirement it enforces. In this sense, the basis of states returned by backward reachability constitute the minimal requirements our configuration may meet in order for the target label to be reachable. Formally, let \(\gamma \) be a configuration of our framework. The target label is reachable from \(\gamma \) if and only if: there exists a process-potential map \(\mathcal {B}\) is in the backward reachable set, such that every trace in every process’ potential in \(\mathcal {B}\) is enabled in \(\gamma \). It suffices to check the existence of \(\mathcal {B}\) over the finite basis of the backward reachable set. Note that \(\gamma \) is completely arbitrary: this solves our Problem 2.

6 Related Work

Fairness. Only recently has fairness for weak memory started receiving increasing attention. The work closest to ours is by [4], who formulate a probabilistic extension for the Total Store Order (TSO) memory model and show decidability results for associated verification problems. Our treatment of fairness is richer, as we relate same probabilistic fairness with two alternate logical fairness definitions. Similar proof techniques notwithstanding, our verification results are also more general, thanks to the development of a uniform framework that applies to a landscape of models. [37] develop a novel formulation of fairness as a declarative property of event structures. This notion informally translates to “Each message is eventually propagated.” We forego axiomatic elegance to motivate and develop stronger practical notions of fairness in our quest to verify liveness.

Probabilistic Verification. There are several works on verification of finite-state Markov chains (e.g. [14, 33]). However, since the messages in our memory systems are unbounded, these techniques do not apply. There is also substantive literature on the verification of infinite state probabilistic system, which have often been modelled as infinite Markov chains [17,18,19, 24, 25]. However their results cannot be directly leveraged to imply ours. The machinery we use for showing decidability is relies on decisive Markov chains, a concept formulated in [7] and used in [4].

Framework. On the modelling front, the ability to specify memory model semantics as first-order constraints over the program-order (), reads-from (), and modification-order () have led to elegant declarative frameworks based on event structures [9, 10, 21, 28]. There are also approaches that, instead of natively characterizing semantics, prescribe constraints on their ISA-level behaviours in terms of program transformations [38]. On the operational front, there have been works that model individual memory models [43, 46] and clusters of similar model [30, 35], however we are not aware of any operational modelling framework that encompasses as wide a range of models as we do. The operationalization in [16] uses write buffers which resemble our channels, however, their operationalization too focuses on a specific semantics.

7 Conclusion, Future Work, and Perspective

Conclusion. The ideas developed in Sect. 4 lie at the heart of our contribution: we motivate and define transition fairness augmented with memory size boundedness or the recurrence of plain configurations, as well as the analogous probabilistic memory fairness. These are equivalent for the purpose of verifying repeated control state reachability, i.e. liveness, and lie at the core of the techniques we discuss in Sect. 5. These techniques owe their generality to the versatile framework we describe in Sect. 3.

Future Work. There are several interesting directions for future work. We believe that our framework can be extended to handle weak memory models that allow speculation, such as ARM and POWER. In such a case, we would need to extend our fairness conditions to limit the amount of allowed speculation. It is also interesting to mix transition fairness with probabilistic fairness, i.e., use the former to solve scheduler non-determinism and the latter to resolve memory non-determinism, leading to (infinite-state) Markov Decision Process model. Along these lines, we can also consider synthesis problems based on \(2\frac{1}{2}\)-games. To solve such game problems, we could extend the framework of Decisive Markov chains that have been developed for probabilistic and game theoretic problems over infinite-state systems [7] A natural next step is develo** efficient algorithms for proving liveness properties for programs running on weak memory models. In particular, since we reduce the verification of liveness properties to simple reachability, there is high hope one can develop CEGAR frameworks relying both on over-approximations, such as predicate abstraction, and under-approximations such as bounded context-switching [44] and stateless model checking [3, 32].

Perspective. Leveraging techniques developed over the years by the program verification community, and using them to solve research problems in programming languages, architectures, databases, etc., has substantial potential added value. Although it requires a deep understanding of program behaviors running on such platforms, we believe it is about finding the right concepts, combining them correctly, and then applying the existing rich set of program verification techniques, albeit in a non-trivial manner. The current paper is a case in point. Here, we have used a combination of techniques developed for reactive systems [31], methods for the analysis of infinite-state systems [7], and semantical models developed for weak memory models [12, 30, 34, 35] to obtain, for the first time, a framework for the systematic analysis of liveness properties under weak memory models.