1 toappendix proofof[1]

# Making Weak Memory Models Fair

Ori Lahav  Tel Aviv UniversityIsrael<EMAIL_ADDRESS>,  Egor Namakonov  St.
Petersburg UniversityRussia JetBrains ResearchRussia
<EMAIL_ADDRESS>,  Jonas Oberhauser  Huawei Dresden Research
CenterGermany Huawei OS Kernel LabGermany<EMAIL_ADDRESS>,  Anton
Podkopaev  HSE UniversityRussia JetBrains ResearchRussia<EMAIL_ADDRESS>and
Viktor Vafeiadis  MPI-SWSGermany<EMAIL_ADDRESS>
(2021)

###### Abstract.

Liveness properties, such as termination, of even the simplest shared-memory
concurrent programs under sequential consistency typically require some
fairness assumptions about the scheduler. Under weak memory models, we observe
that the standard notions of _thread fairness_ are insufficient, and an
additional fairness property, which we call _memory fairness_ , is needed.

In this paper, we propose a uniform definition for memory fairness that can be
integrated into any declarative memory model enforcing acyclicity of the union
of the program order and the reads-from relation. For the well-known models,
SC, x86-TSO, RA, and StrongCOH, that have equivalent operational and
declarative presentations, we show that our declarative memory fairness
condition is equivalent to an intuitive model-specific operational notion of
memory fairness, which requires the memory system to fairly execute its
internal propagation steps. Our fairness condition preserves the correctness
of local transformations and the compilation scheme from RC11 to x86-TSO, and
also enables the first formal proofs of termination of mutual exclusion lock
implementations under declarative weak memory models.

Formal semantics, weak memory models, concurrency, verification

††doi: 10.1145/3485475††journalyear: 2021††submissionid:
oopsla21main-p9-p††journal: PACMPL††journalvolume: 5††journalnumber:
OOPSLA††article: 98††publicationmonth: 10††copyright: none††ccs: Theory of
computation Parallel computing models††ccs: Theory of computation Program
semantics††ccs: Theory of computation Logic and verification

##  1\. Proofs of Propositions and Lemmas in the Paper

##  2\. Introduction

Suppose we want to prove termination of a concurrent program under a full-
featured weak memory model, such as RC11 (Lahav et al., 2017). Sadly, this is
not currently possible because RC11 does not support reasoning about liveness.
Extending its formal definition to enable reasoning about liveness properties
is very important because, as shown by Oberhauser et al. (2021a, Table 2),
multiple existing mutual exclusion lock implementations hang if too few fences
are used. This is also the case for the published version of the HMCS
algorithm (Chabbi et al., 2015): it contains such a termination bug, a
simplified version of which we describe in Section 6.3.

Termination of concurrent programs typically relies on some fairness
assumptions about concurrency as illustrated by the following program, whose
variables are initialized with $0$.

(SpinLoop)
$\begin{array}[]{@{}l@{~~}||@{~~}l@{}}\begin{array}[]{@{}l@{}}x:=1\end{array}\hfil~{}~{}\vrule\vrule~{}~{}&\begin{array}[]{@{}l@{}}\textbf{{repeat}}\;\\{\;a:=x\;\\}\;\textbf{{until}}\;(a\neq
0)\end{array}\end{array}$

Under _sequential consistency_ (SC), the program can diverge if, _e.g.,_
thread 2 is always scheduled and thread 1 never gets a chance to run. This run
is considered unfair because although thread 1 is always available to be
scheduled, it is never selected. A standard assumption is _thread fairness_
(which is typically simply called fairness in the literature (Lamport, 1977;
Park, 1979; Lehmann et al., 1981; Francez, 1986)), namely that every
(unblocked) non-terminated thread is eventually scheduled. With a fair
scheduler, SpinLoop is guaranteed to terminate.

Under weak memory consistency, thread fairness alone does not suffice to
ensure termination of SpinLoop because merely executing the $x:=1$ write does
not mean that its effect is propagated to the other threads. Take, for
example, the operational TSO model (Owens et al., 2009), where writes are
appended to a thread-local buffer and are later asynchronously applied to the
shared memory. With such a model, it is possible that the $x:=1$ write is
forever stuck in the first thread’s buffer and so thread 2 never gets a chance
to read $x=1$. To rule out such behaviors, we introduce another property,
_memory fairness_ (MF), that ensures that threads do not indefinitely observe
the same stale memory state.

Operational models can easily be extended to support MF by requiring fairness
of the internal transitions of the model, which correspond to the propagation
of writes to the different threads. For the standard interleaving semantics of
SC (Lamport, 1979), MF holds vacuously (because the model does not have any
internal transitions). For the usual TSO operational model (Owens et al.,
2009), MF requires that every buffered write eventually propagates to the main
memory. For the operational characterization of _release-acquire_ (RA)
following Kang et al. (2017), more adaptations are necessary: (1) we constrain
the timestamp ordering so that no write can overtake infinitely many other
writes; and (2) add a transition that forcefully updates the views of threads
so that all executed writes eventually become globally visible. The same
criteria are required for MF in the model of _strong coherence_ (StrongCOH),
which is essentially a restriction of the promise-free fragment of Kang et al.
(2017)’s model (as well as of RC11) to relaxed accesses.

In contrast, it is quite challenging to support MF in declarative (a.k.a.
axiomatic) models, which have become the norm for hardware architectures
(x86-TSO (Owens et al., 2009), Power (Alglave et al., 2014), Arm (Pulte et
al., 2017)) and programming languages (e.g., RC11 (Lahav et al., 2017), OCaml
(Dolan et al., 2018), JavaAtomics (Bender and Palsberg, 2019), Javascript
(Watt et al., 2020), WebAssembly (Watt et al., 2019)) alike. In these models,
there are no explicit write propagation transitions so that MF could require
them to eventually take place. Further, the memory accesses of different
threads are not even totally ordered, so even the concept of an event
eventually happening is not immediate. We observe, however, neither internal
transitions nor a total order are necessary for defining fairness; what is
important is that every event is preceded by only a finite number of other
events, and this can be defined on the execution graphs used by declarative
models.

Specifically, for declarative models satisfying
$({\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}\mathtt{po}}\cup{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}})$-acyclicity
(_i.e.,_ acyclicity of the union of the program order and the reads-from
relation), such as RC11, SC, TSO, RA, and StrongCOH, we show that MF can be
defined in a uniform fashion as prefix-finiteness of the extended coherence
order. The latter is a relation used in declarative models to order accesses
to the same location for guaranteeing SC-per-location (Alglave et al., 2014).
Requiring this relation to be prefix-finite means that in a fair execution no
write can be preceded by an infinite number of other events in this order
(_e.g.,_ reads that have not yet observed the write).

We justify the uniform declarative definition of memory fairness in three
ways. First, we show that our declarative MF condition is equivalent to
operational MF for models that have equivalent declarative and operational
presentations (_i.e.,_ SC, TSO, RA, and StrongCOH). This requires extending
the existing equivalence results between operational and declarative models to
_infinite_ executions, and involves more advanced constructions that make use
of memory fairness. Second, we show that including our MF condition in the
RC11 declarative language model, which currently lacks any fairness
guarantees, incurs no performance overhead: the correctness of local program
transformations and the compilation scheme to TSO are unaffected. Third, we
show that memory fairness allows lifting robustness theorems about finite
executions to infinite ones.

We finally demonstrate that our declarative MF condition enables verification
of liveness properties of concurrent programs under RC11 by verifying
termination and/or fairness of multiple lock implementations (see Section 6),
including the MCS lock once the fence missing in the presentation of Chabbi et
al. (2015) is added. Key to those proofs is a reduction theorem we show for
the termination of spinloops. Under certain conditions about the program,
which hold for multiple standard implementations, a spinloop terminates under
a fair model if and only if it exits whenever an iteration reads only the
latest writes in the coherence order. For example, the loop in SpinLoop
terminates because reading the latest write ($x:=1$) exits the loop.

#### Outline

In Section 3 we define fairness operationally and incorporate it in the
operational definitions of SC, x86-TSO, RA, and StrongCOH. In Section 4 we
recap the declarative framework for defining memory models. In Section 5 we
present our declarative MF condition; we establish its equivalence to the
operational MF notions and show that it preserves the existing compilation and
optimization results for RC11 and that it allows lifting of robustness
theorems to infinite executions. In Section 6 we show that the declarative
fairness characterization yields an effective method for proving
(non-)termination of spinloops and illustrate it to prove deadlock-freedom
and/or fairness of three lock implementations. We conclude with a discussion
of fairness in other models in Section 7.

#### Supplementary Material

Our technical appendix (Lahav et al., 2021a) contains typeset proofs for the
lemmas and propositions of the article. We also provide a Coq development
(Lahav et al., 2021b) containing:

  * •

a formalization of operational and declarative fairness for $\mathsf{SC}$,
$\mathsf{TSO}$, $\mathsf{RA}$, and $\mathsf{StrongCOH}$;

  * •

proofs of the aforementioned definitions’ equivalence (Theorem 5.5);

  * •

a proof of Theorem 6.3 stating a sufficient loop termination condition;

  * •

proofs of termination of the spinlock client and of progress of the ticket
lock client for all models satisfying ”SC per location” property (which
generalizes Theorems 6.4 and 6.5) and of termination of the MCS lock client
for $\mathsf{SC}$, $\mathsf{TSO}$ and $\mathsf{RA}$ (Theorem 6.6 without the
RC11 part); and

  * •

a proof of infinite robustness property (Corollary 5.16, excluding the RC11
case).

##  3\. What is a Fair Operational Semantics?

###  3.1. Proofs for Section 3

In this section, we define our operational framework and its fairness
constraints. We initially demonstrate our terminology for sequential
consistency (SC). In Sections 3.2, 3.3 and 3.4, we instantiate our framework
to the total store order (TSO), release/acquire (RA), and strong coherence
(StrongCOH) models, and discuss memory fairness in each of these models.

#### Labeled Transition Systems.

Our formal development is based on _labeled transition systems_ (LTSs), which
we use to represent both programs and operational memory models. We assume
that the transition labels of these systems are split between _(externally)
observable transition labels_ and _silent transition labels_. Using transition
labels we define a _trace_ to be a (finite or infinite) sequence of transition
labels (of any kind); whereas an _observable trace_ is a (finite or infinite)
sequence of observable transition labels. Then, LTSs capture sets of traces
and observable traces in the standard way, which is formulated below.

Formally, we define an LTS ${A}$ to be a tuple
${\langle{Q,\Sigma,\Theta,\mathit{init},\xrightarrow{}}\rangle}$, where $Q$ is
a set of _states_ , $\Sigma$ is a set of _observable transition labels_ ,
$\Theta$ is a set of _silent transition labels_ , $\mathit{init}\in Q$ is the
_initial state_ , and ${\xrightarrow{}}\subseteq
Q\times(\Sigma\uplus\Theta)\times Q$ is a set of _transitions_. We denote by
${A}.{\mathtt{Q}}$, ${A}.{\mathbf{\Sigma}}$, ${A}.{\mathbf{\Theta}}$,
${A}.{\mathtt{init}}$, and $\xrightarrow{}_{{A}}$ the components of an LTS
${A}$.

We denote by ${\mathtt{src}}(t)$, ${\mathtt{tlab}}(t)$, and
${\mathtt{tgt}}(t)$ the three components of a transition
$t\in\,\xrightarrow{}$. For $\sigma\in\Sigma\uplus\Theta$, we write
$\mathrel{\raisebox{-0.8pt}{$\xrightarrow{\sigma}$}}$ for the relation
$\\{{{\langle{{\mathtt{src}}(t),{\mathtt{tgt}}(t)}\rangle}\;|\;t\in{}\xrightarrow{},{\mathtt{tlab}}(t)=\sigma}\\}$.
We use $\xrightarrow{}$ for the relation
$\bigcup_{\sigma\in\Sigma\uplus\Theta}\mathrel{\raisebox{-0.8pt}{$\xrightarrow{\sigma}$}}$.
We say that a transition label $\sigma\in\Sigma\uplus\Theta$ is _enabled_ in
some state $q\in Q$ if
$q\mathrel{\raisebox{-0.8pt}{$\xrightarrow{\sigma}$}}q^{\prime}$ for some
$q^{\prime}\in Q$.

A _run_ of ${A}$ is a (finite or infinite) sequence $\mu$ of transitions in
$\xrightarrow{}_{{A}}$ such that ${\mathtt{src}}(\mu(0))={A}.{\mathtt{init}}$
and ${\mathtt{tgt}}(\mu(k-1))={\mathtt{src}}(\mu(k))$ for every $k\geq 1$ in
$\textit{dom}{({\mu})}$. A run $\mu$ of ${A}$ _induces_ the trace $\rho$ if
$\rho(k)={\mathtt{tlab}}(\mu(k))$ for every $k\in\textit{dom}{({\mu})}$. Also,
$\mu$ induces the _observable_ trace $\rho^{\prime}$ if $\rho^{\prime}$ is the
restriction to $\Sigma$ of some trace $\rho$ that is induced by $\mu$.

An (observable) trace $\rho$ is called an (observable) trace of ${A}$ if it is
induced by some run of ${A}$. We write $\mathsf{OTr}({{A}})$ for the set of
all observable traces of ${A}$ and $\mathsf{OTr^{fin}}({{A}})$ for the set of
all finite observable traces of ${A}$.

#### Domains and Event Labels.

To define programs and their semantics, we fix sets $\mathsf{Loc}$,
$\mathsf{Tid}$, and $\mathsf{Val}$ of _(shared) locations_ , _thread
identifiers_ , and _values_ (respectively). We assume that $\mathsf{Val}$
contains a distinguished value $0$, which serves as the initial value for all
locations. In addition, we assume that $\mathsf{Tid}$ is finite, given by
$\mathsf{Tid}=\\{{1,2{,}\ldots{,}N}\\}$ for some $N\geq 1$. (Our main result
below requires $\mathsf{Tid}$ to be finite, see Remark 3.) We use ${x},{y}$ to
range over $\mathsf{Loc}$; ${\tau},{\pi}$ to range over $\mathsf{Tid}$; and
$v$ to range over $\mathsf{Val}$. Programs interact with the memory using
_event labels_ , defined as follows.

###### Definition 3.1.

An _event label_ ${l}$ is one of the following:

  * •

Read event label: ${{\mathtt{R}}}({{x}},{v_{\mathtt{R}}})$ where
${x}\in\mathsf{Loc}$ and $v_{\mathtt{R}}\in\mathsf{Val}$.

  * •

Write event label: ${{\mathtt{W}}}({{x}},{v_{\mathtt{W}}})$ where
${x}\in\mathsf{Loc}$ and $v_{\mathtt{W}}\in\mathsf{Val}$.

  * •

Read-modify-write label:
${{\mathtt{RMW}}}({{x}},{v_{\mathtt{R}}},{v_{\mathtt{W}}})$ where
${x}\in\mathsf{Loc}$ and $v_{\mathtt{R}},v_{\mathtt{W}}\in\mathsf{Val}$.

The functions ${\mathtt{typ}}$, ${\mathtt{loc}}$, ${\mathtt{val_{r}}}$, and
${\mathtt{val_{w}}}$ return (when applicable) the type
(${\mathtt{R}}/{\mathtt{W}}/{\mathtt{RMW}}$), location (${x}$), read value
($v_{\mathtt{R}}$), and written value ($v_{\mathtt{W}}$) of a given event
label ${l}$. We denote by $\mathsf{ELab}$ the set of all event labels.

###### Remark 1.

For conciseness, we have not included _fences_ in the set of event labels. In
TSO (Owens et al., 2009) and RA (Lahav et al., 2016), fences can be modeled as
read-modify-writes to an otherwise-unused distinguished location $f$.

###### Remark 2.

Rich programming languages like C/C++ (Batty et al., 2011) and Java (Bender
and Palsberg, 2019) as well as the Armv8 multiprocessor (Pulte et al., 2017)
have multiple kinds of accesses. This requires us to extend our event labels
with additional modifiers. However, simple event labels as defined above
suffice for the purpose of this paper.

#### Sequential Programs.

To keep the presentation abstract, we do not fix a particular programming
language, but rather represent sequential (thread-local) programs as LTSs with
$\mathsf{ELab}$, the set of all event labels, serving as the set of observable
transition labels. For simplicity, we assume that sequential programs do not
have silent transitions.111This assumption serves us merely to simplify the
presentation, since silent program transitions can be always attached to the
next memory access. For an example of a toy programming language syntax and
its reading as an LTS, see (Podkopaev et al., 2019). In our code snippets
throughout the paper, we implicitly assume such a standard interpretation.

We refer to observable traces of sequential programs (_i.e.,_ sequences over
$\mathsf{ELab}$) as _sequential traces_.

###### Example 3.2.

The simple sequential program
$\textbf{{repeat}}\;\\{\;a:=x\;\\}\;\textbf{{until}}\;(a\neq 0)$ is formally
captured as an LTS with an initial state $\mathit{init}$ and a state
$\mathit{final}$, and transitions
${\langle{\mathit{init},{{\mathtt{R}}}({x},{v}),\mathit{init}}\rangle}$ for
every $v\in\mathsf{Val}\setminus\\{{0}\\}$ and
${\langle{\mathit{init},{{\mathtt{R}}}({x},{0}),\mathit{final}}\rangle}$. The
sequential traces
${{\mathtt{R}}}({x},{0}),{{\mathtt{R}}}({x},{0}),{{\mathtt{R}}}({x},{0}),{{\mathtt{R}}}({x},{42})$
is an (observable) trace of this program. The infinite sequential trace
${{\mathtt{R}}}({x},{0}),{{\mathtt{R}}}({x},{0}),\dots$ is another
(observable) trace of this program.

#### Concurrent Programs.

A _concurrent program_ , which we also simply call a _program_ , is a top-
level parallel composition of sequential programs, defined as a _finite_
mapping assigning a sequential program to each thread ${\tau}\in\mathsf{Tid}$.
A concurrent program ${P}$ induces an LTS with
$\mathsf{Tid}\times\mathsf{ELab}$ serving as the set of observable transition
labels (and no silent transition labels). This LTS follows the interleaving
semantics of ${P}$: its states are tuples in
$\prod_{{\tau}\in\mathsf{Tid}}{P}({\tau}).{\mathtt{Q}}$; the initial state is
$\lambda{\tau}.\;{P}({\tau}).{\mathtt{init}}$; and the transitions are given
by: * ¯p(τ) $\xrightarrow{{l}}$_P(τ) p
¯p $\xrightarrow{{\tau}:{l}}$_P¯p[τ↦p] In the sequel, we identify concurrent
programs with their induced LTSs.

We refer to observable traces of concurrent programs (_i.e.,_ sequences over
$\mathsf{Tid}\times\mathsf{ELab}$) as _concurrent traces_. We denote the two
components of a pair $\sigma\in\mathsf{Tid}\times\mathsf{ELab}$ by
${\mathtt{tid}}(\sigma)$ and ${\mathtt{elab}}(\sigma)$ respectively.

#### Behaviors.

We define a _behavior_ to be a function $\beta$ assigning a sequential trace
to every thread, since the events executed by each thread capture precisely
what it has observed about the memory system.

###### Notation 3.3.

The restriction of a concurrent trace $\rho$ to thread
${\tau}\in\mathsf{Tid}$, denoted by $\rho|_{{\tau}}$, is the sequence obtained
from $\rho$ by keeping only the transition labels of the form ${\tau}:\\_$.

###### Definition 3.4.

The _behavior induced by a concurrent trace_ $\rho$, denoted by $\beta(\rho)$,
is given by

$\beta(\rho)\triangleq\lambda{\tau}\in\mathsf{Tid}.\;\lambda
k\in\textit{dom}{({\rho|_{{\tau}}})}.\;{\mathtt{elab}}(\rho|_{{\tau}}(k)).$

This notation is extended to sets of concurrent traces in the obvious way
($\beta(S)\triangleq\\{{\beta(\rho)\;|\;\rho\in S}\\}$).

###### Notation 3.5.

For an LTS ${A}$ with ${A}.{\mathbf{\Sigma}}=\mathsf{Tid}\times\mathsf{ELab}$,
we denote by $\mathsf{B}({{A}})$ the set of behaviors induced by observable
traces of ${A}$ (_i.e.,_
$\mathsf{B}({{A}})\triangleq\beta(\mathsf{OTr}({{A}}))$) and by
$\mathsf{B^{fin}}({{A}})$ the set of behaviors induced by finite observable
traces of ${A}$ (_i.e.,_
$\mathsf{B^{fin}}({{A}})\triangleq\beta(\mathsf{OTr^{fin}}({{A}}))$).

Since operations of different threads commute in the program semantics, the
following property easily follows from our definitions.

###### Proposition 3.6.

For every program ${P}$, if $\beta(\rho_{1})=\beta(\rho_{2})$, then
$\rho_{1}\in\mathsf{OTr}({{P}})$ iff $\rho_{2}\in\mathsf{OTr}({{P}})$.

prop:prog W.l.o.g. suppose that $\rho_{1}\in\mathsf{OTr}({{P}})$. Note that
there are no silent transition labels in traces of $P$, so $\rho_{1}$ is a
trace of ${P}$. It means that there exists a run $\mu_{1}$ of $P$ inducing
$\rho_{1}$.

Note that transitions of different sequential programs are independent of each
other. That is, they can be reordered in $\mu_{1}$ in such a way that the
resulting run $\mu_{2}$ will induce $\rho_{2}$. Since
$\beta(\rho_{1})=\beta(\rho_{2})$, no same thread’s transitions reordering are
needed to do that.

#### Thread Fairness.

Not all program behaviors are fair.

###### Example 3.7.

Consider the following program:

(Rloop)
$\begin{array}[]{@{}l@{~~}||@{~~}l@{}}\begin{array}[]{@{}l@{}}{x}\;{:=}\;1\end{array}\hfil~{}~{}\vrule\vrule~{}~{}&\begin{array}[]{@{}l@{}}L\colon
a\;{:=}\;{x}\\\
\phantom{L\colon}\textbf{{if}}\;a=0\;\textbf{{goto}}\;L\end{array}\end{array}$

The behaviors of this program include the behavior assigning
${{\mathtt{W}}}({{x}},{1})$ to the first thread and
${{\mathtt{R}}}({{x}},{1})$ to the second, but also the (infinite) behavior
assigning the empty sequence to the first thread and the infinite sequence
${{\mathtt{R}}}({{x}},{0}),{{\mathtt{R}}}({{x}},{0}),\ldots$ to the second.
This behavior occurs if an unfair scheduler only schedules the second thread
to run even though the first thread is always available to execute.222On this
level, without considering a particular memory system (as defined below), the
read values are not restricted whatsoever. Thus, the behaviors of this program
include also any behavior assigning ${{\mathtt{W}}}({{x}},{1})$ to the first
thread and either ${{\mathtt{R}}}({{x}},{v})$ for some
$v\in\mathsf{Val}\setminus\\{{0}\\}$ or the infinite sequence
${{\mathtt{R}}}({{x}},{0}),{{\mathtt{R}}}({{x}},{0}),\ldots$ to the second
thread. Nonsensical behaviors (with $v\not\in\\{{0,1}\\}$) are overruled when
the program is linked with any of the memory systems defined below, with or
without “memory fairness”.

A natural constraint, which in particular excludes the infinite behavior in
the example above, requires a fair scheduler. Since our formalism assumes no
blocking operations (in particular, locks are implemented using spinloops),
such a scheduler has to ensure that every non-terminated thread is eventually
scheduled, which we formally define as follows.

###### Definition 3.8.

Let ${P}$ be a program.

  * •

A thread ${\tau}\in\mathsf{Tid}$ is _enabled_ in
$\overline{p}\in{P}.{\mathtt{Q}}$ if ${\langle{{\tau},{l}}\rangle}$ is enabled
in $\overline{p}$ for some ${l}\in\mathsf{ELab}$.

  * •

A thread ${\tau}\in\mathsf{Tid}$ is _continuously enabled at index $k$_ in an
infinite run $\mu$ of ${P}$ if it is enabled in ${\mathtt{src}}(\mu(j))$ for
every index $j\geq k$. Thread ${\tau}$ is _continuously enabled_ in $\mu$ if
it is continuously enabled in $\mu$ at some index $k$.

  * •

A run $\mu$ of ${P}$ is _thread-fair_ if $\mu$ is finite or for every thread
${\tau}\in\mathsf{Tid}$ and index $k$ such that ${\tau}$ is continuously
enabled in $\mu$ at $k$, there exists $j\geq k$ such that
${\mathtt{tid}}({\mathtt{tlab}}(\mu(j)))={\tau}$.

  * •

A _thread-fair observable trace of ${P}$_ is any concurrent trace induced by a
thread-fair run of ${P}$.

  * •

A _thread-fair behavior of ${P}$_ is any behavior induced by a thread-fair
observable trace of ${P}$. We denote by $\mathsf{B^{tf}}({{P}})$ the set of
all thread-fair behaviors of ${P}$.

Returning to Example 3.7, thread-fair behaviors of Rloop are either finite or
must assign ${{\mathtt{W}}}({{x}},{1})$ to the first thread.

Again, since operations of different threads commute in the program semantics,
the following property easily follows from our definitions.

###### Proposition 3.9.

For every program ${P}$, if $\beta(\rho_{1})=\beta(\rho_{2})$, then $\rho_{1}$
is a thread-fair observable trace of ${P}$ iff $\rho_{2}$ is a thread-fair
observable trace of ${P}$.

prop:prog_tf W.l.o.g. suppose that $\rho_{1}$ is a thread-fair observable
trace of ${P}$ induced by some $\mu_{1}$. By Prop. 3.6 $\rho_{2}$ is an
observable trace of ${P}$ induced by some $\mu_{2}$.

Note that, since $\beta(\rho_{1})=\beta(\rho_{2})$, every thread’s LTS goes
via the same sequence of states. That is, for each thread $\mu_{2}$ has the
same set of continuously enabled states as $\mu_{1}$ does. Also, since
$\beta(\rho_{1})=\beta(\rho_{2})$, every continuously enabled state is
succeeded by the same sequence of labels both in $\mu_{1}$ and $\mu_{2}$.
Thus, if $\rho_{1}$ is thread-fair then $\rho_{2}$ should also be.

#### Memory Systems.

To give operational semantics to programs, we synchronize them with _memory
systems_ , which, like programs, are LTSs with
$\mathsf{Tid}\times\mathsf{ELab}$ serving as the set of observable transition
labels. In addition, memory systems have silent transition labels, which vary
from one system to another. Intuitively, the set of silent transition labels
${\mathcal{M}}.{\mathbf{\Theta}}$ of a memory system ${\mathcal{M}}$ consists
of internal actions that the program cannot observe (_e.g.,_ cache-related
operations).

The most well-known memory system is that of _sequential consistency_
(Lamport, 1979), denoted here by ${\mathcal{M}}_{\mathsf{SC}}$, in which
writes by each thread are made immediately visible to all other threads.
${\mathcal{M}}_{\mathsf{SC}}$ tracks the most recent value written to each
location. Its initial state maps each location to zero. That is,
${\mathcal{M}}_{\mathsf{SC}}.{\mathtt{Q}}\triangleq\mathsf{Loc}\to\mathsf{Val}$
and ${\mathcal{M}}_{\mathsf{SC}}.{\mathtt{init}}\triangleq\lambda{x}.\;0$. The
system ${\mathcal{M}}_{\mathsf{SC}}$ has no silent transitions
(${\mathcal{M}}_{\mathsf{SC}}.{\mathbf{\Theta}}=\emptyset$) and its transition
relation $\xrightarrow{}_{{\mathcal{M}}_{\mathsf{SC}}}$ is defined as follows:
* M’=M[x↦v] M $\xrightarrow{{\tau}:{{\mathtt{W}}}({{x}},{v})}$_M_$\mathsf{SC}$
M’ * M(x)=v M $\xrightarrow{{\tau}:{{\mathtt{R}}}({{x}},{v})}$_M_$\mathsf{SC}$
M * M
$\xrightarrow{{\tau}:{{\mathtt{R}}}({{x}},{v_{\mathtt{R}}})}$_M_$\mathsf{SC}$
$\xrightarrow{{\tau}:{{\mathtt{W}}}({{x}},{v_{\mathtt{W}}})}$_M_$\mathsf{SC}$
M’ M
$\xrightarrow{{\tau}:{{\mathtt{RMW}}}({{x}},{v_{\mathtt{R}}},{v_{\mathtt{W}}})}$_M_$\mathsf{SC}$
M’ Writing $v$ to ${x}$ simply updates the value of ${x}$ stored in ${M}$.
(${M}[{x}\mapsto v]$ is the function that maps ${x}$ to $v$ and all other
locations ${y}$ to ${M}({y})$.) Reading $v$ from ${x}$ succeeds iff the value
stored for ${x}$ in memory is $v$. The atomic read-modify-write
${{\mathtt{RMW}}}({{x}},{v_{\mathtt{R}}},{v_{\mathtt{W}}})$ reads location
${x}$ yielding value $v_{\mathtt{R}}$ and immediately writes $v_{\mathtt{W}}$
to it. Note that ${\mathcal{M}}_{\mathsf{SC}}$ is oblivious to the thread that
takes the action
($\mathrel{\raisebox{-0.8pt}{$\xrightarrow{{\tau}:{l}}$}}_{{\mathcal{M}}_{\mathsf{SC}}}=\mathrel{\raisebox{-0.8pt}{$\xrightarrow{{\pi}:{l}}$}}_{{\mathcal{M}}_{\mathsf{SC}}}$).
The other memory systems below do not have this property.

#### Linking Programs and Memory Systems.

By linking programs and memory systems, we can talk about the behavior of a
program ${P}$ under a memory system ${\mathcal{M}}$. We say that a certain
behavior $\beta$ is a _behavior of a program ${P}$ under a memory system
${\mathcal{M}}$_ if $\beta$ is both a behavior of ${P}$ and a behavior of
${\mathcal{M}}$ (_i.e.,_
$\beta\in\mathsf{B}({{P}})\cap\mathsf{B}({{\mathcal{M}}})$). Similarly,
$\beta$ is called a _thread-fair behavior of ${P}$ under ${\mathcal{M}}$_ if
$\beta\in\mathsf{B^{tf}}({{P}})\cap\mathsf{B}({{\mathcal{M}}})$.

###### Proposition 3.10.

Let ${P}$ be a program, ${\mathcal{M}}$ be a memory system, and $\beta$ be a
behavior.

  * •

$\beta$ is a behavior of ${P}$ under ${\mathcal{M}}$ iff $\beta=\beta(\rho)$
for some $\rho\in\mathsf{OTr}({{P}})\cap\mathsf{OTr}({{\mathcal{M}}})$.

  * •

$\beta$ is a thread-fair behavior of ${P}$ under ${\mathcal{M}}$ iff
$\beta=\beta(\rho)$ for some $\rho\in\mathsf{OTr}({{\mathcal{M}}})$ that is
also a thread-fair observable trace of ${P}$.

prop:beh_tf_op In the right-to-left implications of both claims the trace
$\rho$ belongs both to $\mathsf{B}({{\mathcal{M}}})$ and $\mathsf{B}({{P}})$
($\mathsf{B^{tf}}({{P}})$ correspondingly) thus satisfying needed conditions.

Note that for a (thread-fair) behavior $\beta$ under ${\mathcal{M}}$ there are
two traces: one from $\mathsf{B}({{P}})$ ($\mathsf{B^{tf}}({{P}})$) and
another from $\mathsf{B}({{\mathcal{M}}})$. But since these traces have the
same behavior, left-to-right implications can be proved by applying Prop. 3.6
(Prop. 3.9 correspondingly) to the trace from $\mathsf{B}({{\mathcal{M}}})$.

###### Example 3.11.

Thread-fair behaviors of the program Rloop under ${\mathcal{M}}_{\mathsf{SC}}$
must be finite. Indeed, in observable traces of ${\mathcal{M}}_{\mathsf{SC}}$,
after the first thread performs ${{\mathtt{W}}}({{x}},{1})$, the second thread
will perform ${{\mathtt{R}}}({{x}},{1})$ and terminate its execution. The
behavior $\beta_{\text{inf}}$ that assigns the empty sequence to the first
thread and the infinite sequence consisting of ${{\mathtt{R}}}({{x}},{0})$
event labels to the second thread cannot be obtained from a thread-fair run of
Rloop.

#### Memory Fairness.

As we have already discussed, thread-fairness alone is often insufficient to
reason about termination under weak memory models. For this reason, we
introduce _memory fairness_ (MF), which ensures that a thread cannot be
lagging behind indefinitely because the memory system did not propagate
certain updates to it. We formalize this intuition by having MF require that
the memory silent transitions (responsible for such propagation steps) are
scheduled infinitely often.

###### Definition 3.12.

Let ${\mathcal{M}}$ be a memory system.

  * •

A silent transition label $\theta\in{\mathcal{M}}.{\mathbf{\Theta}}$ is
_continuously enabled at index $k$_ in an infinite run $\mu$ of
${\mathcal{M}}$ if it is enabled in ${\mathtt{src}}(\mu(j))$ for every index
$j\geq k$. The label $\theta$ is _continuously enabled_ in $\mu$ if it is
continuously enabled in $\mu$ at some index $k$.

  * •

A run $\mu$ of ${\mathcal{M}}$ is _memory-fair_ if $\mu$ is finite or for
every silent memory transition label
$\theta\in{\mathcal{M}}.{\mathbf{\Theta}}$ and index $k$ such that $\theta$ is
continuously enabled in $\mu$ at $k$, there exists $j\geq k$ such that
${\mathtt{tlab}}(\mu(j))=\theta$.

  * •

A _memory-fair observable trace of ${\mathcal{M}}$_ is any concurrent trace
induced by a memory-fair run of ${\mathcal{M}}$.

  * •

A _memory-fair behavior of ${\mathcal{M}}$_ is any behavior induced by a
memory-fair observable trace of ${\mathcal{M}}$. We denote by
$\mathsf{B^{mf}}({{\mathcal{M}}})$ the set of all memory-fair behaviors of
${\mathcal{M}}$.

Linking this definition with programs, we say that a certain behavior $\beta$
is a _memory-fair behavior of a program ${P}$ under a memory system
${\mathcal{M}}$_ if
$\beta\in\mathsf{B}({{P}})\cap\mathsf{B^{mf}}({{\mathcal{M}}})$. Similarly,
$\beta$ is called a _thread &memory-fair behavior of ${P}$ under
${\mathcal{M}}$_ if
$\beta\in\mathsf{B^{tf}}({{P}})\cap\mathsf{B^{mf}}({{\mathcal{M}}})$.

###### Proposition 3.13.

Let ${P}$ be a program, ${\mathcal{M}}$ be a memory system, and $\beta$ be a
behavior.

  * •

$\beta$ is a memory-fair behavior of ${P}$ under ${\mathcal{M}}$ iff
$\beta=\beta(\rho)$ for some observable trace $\rho$ of ${P}$ that is also a
memory-fair observable trace of ${\mathcal{M}}$.

  * •

$\beta$ is a thread&memory-fair behavior of ${P}$ under ${\mathcal{M}}$ iff
$\beta=\beta(\rho)$ for some thread-fair observable trace $\rho$ of ${P}$ that
is also a memory-fair observable trace of ${\mathcal{M}}$.

prop:beh_mf_op In the right-to-left implications of both claims the trace
$\rho$ belongs both to $\mathsf{B^{mf}}({{\mathcal{M}}})$ and
$\mathsf{B}({{P}})$ ($\mathsf{B^{tf}}({{P}})$ correspondingly) thus satisfying
needed conditions.

Note that for a memory-fair (thread&memory-fair) behavior $\beta$ under
${\mathcal{M}}$ there are two traces: one from $\mathsf{B}({{P}})$
($\mathsf{B^{tf}}({{P}})$) and another from
$\mathsf{B^{mf}}({{\mathcal{M}}})$. But since these traces have the same
behavior, left-to-right implications can be proved by applying Prop. 3.6
(Prop. 3.9 correspondingly) to the trace from
$\mathsf{B^{mf}}({{\mathcal{M}}})$.

Since ${\mathcal{M}}_{\mathsf{SC}}.{\mathbf{\Theta}}=\emptyset$, every
behavior of a program ${P}$ under ${{\mathcal{M}}_{\mathsf{SC}}}$ is
(vacuously) memory-fair.

###### Example 3.14.

Consider the following program (assuming that ${x}$ is initialized to $0$):

(WWRloop)
$\begin{array}[]{@{}l@{~~}||@{~~}l@{}}\begin{array}[]{@{}l@{}}L_{1}\colon{x}\;{:=}\;1\\\
\phantom{L_{1}\colon}{x}\;{:=}\;0\\\
\phantom{L_{1}\colon}\textbf{{goto}}\;L_{1}\end{array}\hfil~{}~{}\vrule\vrule~{}~{}&\begin{array}[]{@{}l@{}}L_{2}\colon
a\;{:=}\;{x}\\\
\phantom{L_{2}\colon}\textbf{{if}}\;a=0\;\textbf{{goto}}\;L_{2}\\\
{}\end{array}\end{array}$

The infinite behavior that assigns the infinite sequences
${{\mathtt{W}}}({{x}},{1}),{{\mathtt{W}}}({{x}},{0}),{{\mathtt{W}}}({{x}},{1}),{{\mathtt{W}}}({{x}},{0}),\ldots$,
and ${{\mathtt{R}}}({{x}},{0}),{{\mathtt{R}}}({{x}},{0}),\ldots$ to the first
and second threads (respectively) is a thread&memory-fair behavior of this
program under ${{\mathcal{M}}_{\mathsf{SC}}}$: in a corresponding run both
threads are executed infinitely often. In particular, note that our
definitions require that transitions that are _continuously_ enabled are
eventually taken, and while the transition ${{\mathtt{R}}}({{x}},{1})$ is
infinitely often enabled for the second thread, it is not continuously
enabled.

Next, we demonstrate three weaker memory systems with non-empty sets of silent
transitions that have non-memory-fair traces. In these systems, whether a
program terminates or deadlocks may crucially depend on memory fairness.

###  3.2. The Total Store Order Memory System

We instantiate memory fairness to the “Total Store Order” (TSO) model (Sewell
et al., 2010; Owens et al., 2009) of the x86 architecture. This memory system,
denoted by ${\mathcal{M}}_{\mathsf{TSO}}$, is defined by:

  1. (1)

${\mathcal{M}}_{\mathsf{TSO}}.{\mathtt{Q}}\triangleq(\mathsf{Loc}\to\mathsf{Val})\times(\mathsf{Tid}\to(\mathsf{Loc}\times\mathsf{Val})^{*})$
(Each state consists of a memory and a per-thread store buffer.)

  2. (2)

${\mathcal{M}}_{\mathsf{TSO}}.{\mathbf{\Theta}}\triangleq\\{{{\mathtt{prop}}({\tau})\;|\;{\tau}\in\mathsf{Tid}}\\}$
(Silent transitions consist of a propagation label for every thread.)

  3. (3)

${\mathcal{M}}_{\mathsf{TSO}}.{\mathtt{init}}\triangleq{\langle{{M}_{0},{B}_{0}}\rangle}$,
where ${M}_{0}\triangleq\lambda{x}.\;0$ and
${B}_{0}\triangleq\lambda{\tau}.\;\epsilon$ (Initially, all buffers are
empty.)

  4. (4)

$\xrightarrow{}_{{\mathcal{M}}_{\mathsf{TSO}}}$ is given in Fig. 1.

* B’=B[τ↦⟨x,v⟩ ⋅B(τ)] M,B $\xrightarrow{{\tau}:{{\mathtt{W}}}({{x}},{v})}$_M_$\mathsf{TSO}$ M,B’

* B(τ)=⟨x_n,v_n⟩ ⋅…⋅⟨x_1,v_1⟩

M[x_1 ↦v_1] ⋅ ⋅ ⋅ [x_n ↦v_n](x)=vM,B
$\xrightarrow{{\tau}:{{\mathtt{R}}}({{x}},{v})}$_M_$\mathsf{TSO}$ M,B

* B(τ)=ϵ
M(x) = v_RM,B
$\xrightarrow{{\tau}:{{\mathtt{RMW}}}({{x}},{v_{\mathtt{R}}},{v_{\mathtt{W}}})}$_M_$\mathsf{TSO}$
M[x↦v_W],B

* B(τ)= b⋅⟨x,v⟩ M,B $\xrightarrow{{\mathtt{prop}}({\tau})}$_M_$\mathsf{TSO}$ M[x↦v],B[τ↦b]

Figure 1. Transitions of ${\mathcal{M}}_{\mathsf{TSO}}$

In addition to the global memory ${M}$, states of
${\mathcal{M}}_{\mathsf{TSO}}$ include a mapping ${B}$ assigning a FIFO _store
buffer_ to every thread. Writes are first written to the local buffer and
later non-deterministically propagate to memory (in the order in which they
were issued). Reads read the most recent value of the relevant location in the
thread’s buffer and refer to the memory if such value does not exist. RMWs can
only execute when the thread’s buffer is empty and write their result in the
memory directly.

###### Example 3.15 (Store Buffering).

The following annotated behavior is _allowed_ under
${\mathcal{M}}_{\mathsf{TSO}}$ (but not under ${\mathcal{M}}_{\mathsf{SC}}$):

(SB)
$\begin{array}[]{@{}l@{~~}||@{~~}l@{}}\begin{array}[]{@{}l@{}}{x}\;{:=}\;1\\\
a\;{:=}\;{y}\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}{~{}~{}\texttt{/\\!\\!/}\textit{reads
0}}\end{array}\hfil~{}~{}\vrule\vrule~{}~{}&\begin{array}[]{@{}l@{}}{y}\;{:=}\;1\\\
a\;{:=}\;{x}\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}{~{}~{}\texttt{/\\!\\!/}\textit{reads
0}}\end{array}\end{array}$

Indeed, the first thread may run first, but the write of $1$ to ${x}$ may
remain in its store buffer. Then, when the second thread runs, it reads the
initial value ($0$) of ${x}$ from the memory.

###### Example 3.16.

Revisiting the Rloop program from Section 3, unlike under
${{\mathcal{M}}_{\mathsf{SC}}}$, thread-fair behaviors of Rloop under
${{\mathcal{M}}_{\mathsf{TSO}}}$ include the (infinite) behavior assigning the
${{\mathtt{W}}}({{x}},{1})$ to the first thread and the infinite sequence
${{\mathtt{R}}}({{x}},{0}),{{\mathtt{R}}}({{x}},{0}),\ldots$ to the second.
Indeed, the entry ${\langle{{x},1}\rangle}$ may indefinitely remain in the
first thread’s buffer, so that ${{\mathtt{W}}}({{x}},{1})$ is never executed
from the point of view of the second thread. To disqualify this behavior, we
need to further require _memory_ fairness. Indeed, in runs inducing this
infinite behavior, the silent memory transition ${\mathtt{prop}}(1)$ is
necessarily continuously enabled. Memory fairness requires that
${\mathtt{prop}}(1)$ will be eventually executed, and from that point on
${\mathcal{M}}_{\mathsf{TSO}}$ prohibits the second thread from executing
${{\mathtt{R}}}({{x}},{0})$.

We note that the notion of memory fairness is sensitive to the choice of
silent memory transitions. For example, consider an alternative memory system,
denoted by ${\mathcal{M}}_{\mathsf{TSO}}^{\prime}$, with less informative
silent transition labels that do not record the thread identifier of the
propagated write. (Formally ${\mathcal{M}}_{\mathsf{TSO}}^{\prime}$ is defined
just like ${\mathcal{M}}_{\mathsf{TSO}}$ except for
${\mathcal{M}}_{\mathsf{TSO}}^{\prime}.{\mathbf{\Theta}}\triangleq\\{{{\mathtt{prop}}}\\}$,
and the label of the propagation step is ${\mathtt{prop}}$ rather than
${\mathtt{prop}}({\tau})$.) Then, ${\mathcal{M}}_{\mathsf{TSO}}^{\prime}$
induces the same set of behaviors as ${\mathcal{M}}_{\mathsf{TSO}}$, but not
the same set of _memory fair_ behaviors. In particular, we can extend the
Rloop program with an additional thread that constantly writes to some
unrelated location ${y}$, and obtain a memory fair run of
${\mathcal{M}}_{\mathsf{TSO}}^{\prime}$ by infinitely often propagating a
write to ${y}$, but never propagating the ${{\mathtt{W}}}({{x}},{1})$ entry.

###  3.3. The Release/Acquire Memory System

We instantiate our operational framework with a memory system for
Release/Acquire (RA), enriched with silent memory transitions for capturing
fair behaviors. Here we follow an operational formulation of RA from Kaiser et
al. (2017), based on the Promising Semantics of Kang et al. (2017).

The memory of the RA system records a (finite) set of _messages_ , each of
which corresponds to some write that was previously executed. Messages (of the
same location) are ordered using _timestamps_ , and carry a _view_ —a mapping
from locations to timestamps. In turn, the states of this memory system also
keep track of the current view of each thread, and use these views to confine
the set of messages that threads may read and write. In particular, if a
thread has observed (either by reading or by writing itself) a message whose
view $\mathit{V}$ has $\mathit{V}({x})=t$, then it can only read messages of
${x}$ whose timestamp is greater than or equal to $t$.

To formally define this system, we let $\mathsf{Time}\triangleq{\mathbb{N}}$
(using natural numbers as timestamps),
$\mathsf{View}\triangleq\mathsf{Loc}\to\mathsf{Time}$ (the set of views), and
$\mathsf{Msg}\triangleq\mathsf{Loc}\times\mathsf{Val}\times\mathsf{Time}\times\mathsf{View}$
(the set of messages). We denote a message $m$ as a tuple of the form
${\langle{{x}:v@t,\mathit{V}}\rangle}$, where ${x}\in\mathsf{Loc}$,
$v\in\mathsf{Val}$, $t\in\mathsf{Time}$, and $\mathit{V}\in\mathsf{View}$. We
write ${\mathtt{loc}}(m)$, ${\mathtt{val}}(m)$, ${\mathtt{ts}}(m)$, and
${\mathtt{view}}(m)$ to refer to the components of a message $m$. The usual
order $<$ on natural numbers is lifted pointwise to a partial order on views;
$\sqcup$ denotes the pointwise maximum on views; and $\mathit{V}_{0}$ is the
minimum view ($\mathit{V}_{0}\triangleq\lambda{x}.\;0$).

With these definitions and notations, the RA memory system, denoted here by
${\mathcal{M}}_{\mathsf{RA}}$, is defined as follows (additional silent memory
transitions are discussed below):

  1. (1)

${\mathcal{M}}_{\mathsf{RA}}.{\mathtt{Q}}\triangleq\mathcal{P}({\mathsf{Msg}})\times(\mathsf{Tid}\to\mathsf{View})$.

  2. (2)

${\mathcal{M}}_{\mathsf{RA}}.{\mathtt{init}}\triangleq{\langle{{M}_{0},\lambda{\tau}.\;\mathit{V}_{0}}\rangle}$,
where the initial memory is
${M}_{0}\triangleq\\{{{\langle{{x}:0@0,\mathit{V}_{0}}\rangle}\;|\;{x}\in\mathsf{Loc}}\\}$.

  3. (3)

$\xrightarrow{}_{{\mathcal{M}}_{\mathsf{RA}}}$ is given in Fig. 2.

* ∄m∈M. loc(m)=x∧ts(m)=t

T(τ)(x) ¡ t

T’=T[τ↦T(τ)[x↦t]]

M’=M∪{⟨x:v@t,T’(τ)⟩} ⟨M,T⟩
$\xrightarrow{{\tau}:{{\mathtt{W}}}({{x}},{v})}$_M_$\mathsf{RA}$ ⟨M’,T’⟩ *
⟨x:v@t,V⟩ ∈M

T(τ)(x) ≤t

T’=T[τ↦T(τ) ⊔V] ⟨M,T⟩
$\xrightarrow{{\tau}:{{\mathtt{R}}}({{x}},{v})}$_M_$\mathsf{RA}$ ⟨M,T’⟩ *
⟨M,T⟩
$\xrightarrow{{\tau}:{{\mathtt{R}}}({{x}},{v_{\mathtt{R}}})}$_M_$\mathsf{RA}$
⟨M,T’⟩
$\xrightarrow{{\tau}:{{\mathtt{W}}}({{x}},{v_{\mathtt{W}}})}$_M_$\mathsf{RA}$
⟨M’,T”⟩
T”(τ)(x)=T’(τ)(x)+1 ⟨M,T⟩
$\xrightarrow{{\tau}:{{\mathtt{RMW}}}({{x}},{v_{\mathtt{R}}},{v_{\mathtt{W}}})}$_M_$\mathsf{RA}$
⟨M’,T”⟩

Figure 2. Transitions of ${\mathcal{M}}_{\mathsf{RA}}$

The states of ${\mathcal{M}}_{\mathsf{RA}}$ consist of a set ${M}$ of all
messages added to the memory so far and a mapping $\mathit{T}$ assigning a
view to each thread. Write steps of thread ${\tau}$ writing to location ${x}$
pick a timestamp $t$ that is fresh ($\nexists
m\in{M}.\;{\mathtt{loc}}(m)={x}\land{\mathtt{ts}}(m)=t$) and greater than the
latest timestamp that ${\tau}$ has observed for ${x}$
($\mathit{T}({\tau})({x})<t$); update the thread’s view to include this
timestamp
($\mathit{T}^{\prime}=\mathit{T}[{\tau}\mapsto\mathit{T}({\tau})[{x}\mapsto
t]]$); and add a corresponding message to the memory carrying the (updated)
thread view
(${M}^{\prime}={M}\cup\\{{{\langle{{x}:v@t,\mathit{T}^{\prime}({\tau})}\rangle}}\\}$).
Read steps of thread ${\tau}$ reading from location ${x}$ pick a message from
the current memory (${\langle{{x}:v@t,\mathit{V}}\rangle}\in{M}$) whose
timestamp is greater than or equal to the latest timestamp that ${\tau}$ has
observed for ${x}$ ($\mathit{T}({\tau})({x})\leq t$); and incorporate the
message’s view in the thread view
($\mathit{T}^{\prime}=\mathit{T}[{\tau}\mapsto\mathit{T}({\tau})\sqcup\mathit{V}]$).
RMW steps are defined as atomic sequencing of a read step followed by a write
step, with the restriction that the new message’s (fresh) timestamp is the
successor of the timestamp of the read message
($\mathit{T}^{\prime\prime}({\tau})({x})=\mathit{T}^{\prime}({\tau})({x})+1$).
The latter condition is needed to ensure the atomicity of RMWs: no other write
can intervene between the read part and the write part of the RMW (_i.e.,_ no
message can be placed between the read and the written messages in the
timestamp order).

###### Example 3.17 (Message passing).

The following annotated behavior is _disallowed_ under
${\mathcal{M}}_{\mathsf{RA}}$:

(MP)
$\begin{array}[]{@{}l@{~~}||@{~~}l@{}}\begin{array}[]{@{}l@{}}{x}\;{:=}\;1\\\
{y}\;{:=}\;1\end{array}\hfil~{}~{}\vrule\vrule~{}~{}&\begin{array}[]{@{}l@{}}a\;{:=}\;{y}\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}{~{}~{}\texttt{/\\!\\!/}\textit{reads
1}}\\\
b\;{:=}\;{x}\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}{~{}~{}\texttt{/\\!\\!/}\textit{reads
0}}\end{array}\end{array}$

Indeed, the second thread can read $1$ for ${y}$, only after the first thread
added two messages $m_{x}={\langle{{x}:1@t_{x},[{x}\mapsto t_{x}]}\rangle}$
and $m_{y}={\langle{{y}:1@t_{y},[{x}\mapsto t_{x},{y}\mapsto t_{y}]}\rangle}$
to the memory with $t_{x},t_{y}>0$. When reading $m_{y}$, the second thread
increases its view of ${x}$ to be $t_{x}$. Since $t_{x}>0$, it is then unable
to read the initial message of ${x}$, and must read $m_{x}$.

###### Example 3.18.

By forcing RMWs to use the successor of the read message as the timestamp of
the written message, ${\mathcal{M}}_{\mathsf{RA}}$ forbids different RMWs to
read the same message. To see this, consider the following example (where FADD
denotes an atomic fetch-and-add instruction that returns its read value):

(2RMW)
$\begin{array}[]{@{}l@{~~}||@{~~}l@{}}\begin{array}[]{@{}l@{}}a\;{:=}\;\textbf{{FADD}}({{x}},{1})\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}{~{}~{}\texttt{/\\!\\!/}\textit{reads
0}}\end{array}\hfil~{}~{}\vrule\vrule~{}~{}&\begin{array}[]{@{}l@{}}b\;{:=}\;\textbf{{FADD}}({{x}},{1})\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}{~{}~{}\texttt{/\\!\\!/}\textit{reads
0}}\end{array}\end{array}$

W.l.o.g., if the first runs first, it reads from the initialization message
${\langle{{x}:0@0,\mathit{V}_{0}}\rangle}$ (it is the only message of ${x}$ in
${M}_{0}$), and it is forced to add a message _with timestamp $1$_. When the
second thread runs, it may _not_ read from the initialization message: that
would again require adding a message of ${x}$ with timestamp $1$, but that
timestamp is no longer available. Thus, it may only read from the message that
was added by the first thread.

###### Example 3.19.

Fences (modeled as RMWs to an otherwise unused distinguished location $f$) can
be used to recover sequential consistency when needed. The following outcome
is forbidden by $\mathsf{RA}$.

(SB+RMWs)
$\begin{array}[]{@{}l@{~~}||@{~~}l@{}}\begin{array}[]{@{}l@{}}{x}\;{:=}\;1\\\
\textbf{{FADD}}({f},{0})\\\
a\;{:=}\;{y}\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}{~{}~{}\texttt{/\\!\\!/}\textit{reads
0}}\end{array}\hfil~{}~{}\vrule\vrule~{}~{}&\begin{array}[]{@{}l@{}}{y}\;{:=}\;1\\\
\textbf{{FADD}}({f},{0})\\\
b\;{:=}\;{x}\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}{~{}~{}\texttt{/\\!\\!/}\textit{reads
0}}\end{array}\end{array}$

Due to the RMWs in both threads, ${\mathcal{M}}_{\mathsf{RA}}$ forbids the
annotated program behavior. Indeed, suppose, w.l.o.g., that the first thread
executes its $\textbf{{FADD}}({f},{0})$ first, it will read from the
initialization message to $f$ and will add to memory a message of the form
${\langle{f:0@1,\mathit{V}}\rangle}$ with $\mathit{V}({x})>0$. When the second
thread executes its $\textbf{{FADD}}({f},{0})$, it will necessarily read that
message and incorporate the view $\mathit{V}$ in its thread view, so that its
view of ${x}$ will be increased. Then, when it reads ${x}$ it may not pick the
initial message.

The RA memory system defined so far (with no silent transitions) allows non-
fair executions. In particular, it allows messages added by some thread to
never propagate to other threads, so that other threads may forever read a
message with a lower timestamp, and thus, allows, _e.g.,_ a thread-fair
_infinite_ behavior for the Rloop program from Section 3.

To address this problem, we include silent memory transitions in
${\mathcal{M}}_{\mathsf{RA}}$, labeled with tuples of the form
${\mathtt{prop}}({\tau},m)$, where ${\tau}\in\mathsf{Tid}$ and
$m\in\mathsf{Msg}$ (_i.e.,_
${\mathcal{M}}_{\mathsf{RA}}.{\mathbf{\Theta}}\triangleq\\{{{\mathtt{prop}}({\tau},m)\mid{\tau}\in\mathsf{Tid},m\in\mathsf{Msg}}\\}$).
Then, we include in ${\mathcal{M}}_{\mathsf{RA}}$ the following silent memory
step:

$\inferrule[RA-propagate]{m\in{M}\\\
\mathit{T}({\tau})({\mathtt{loc}}(m))<{\mathtt{ts}}(m)}{{\langle{{M},\mathit{T}}\rangle}\mathrel{\raisebox{-0.8pt}{$\xrightarrow{{\mathtt{prop}}({\tau},m)}$}}_{{\mathcal{M}}_{\mathsf{RA}}}{\langle{{M},\mathit{T}[{\tau}\mapsto\mathit{T}({\tau})[{\mathtt{loc}}(m)\mapsto{\mathtt{ts}}(m)]]}\rangle}}$

For a given thread ${\tau}$ and message $m$ that has not been yet observed by
thread ${\tau}$ ($\mathit{T}({\tau})({\mathtt{loc}}(m))<{\mathtt{ts}}(m)$),
this step increases ${\tau}$’s view to include $m$’s timestamp. Intuitively
speaking, it ensures that every thread ${\tau}$ eventually advances its view
so that it cannot keep reading an old message indefinitely.

###### Example 3.20.

While thread-fair behaviors of Rloop under ${{\mathcal{M}}_{\mathsf{RA}}}$
include an infinite behavior (in which the second thread indefinitely read the
initialization message), memory fairness forbids this behavior. Indeed, in
runs inducing this infinite behavior, a silent label
${\mathtt{prop}}(2,{\langle{{x}:1@t,[{x}\mapsto t]}\rangle})$ (where $t$ is a
timestamp of a message added by instruction ${x}\;{:=}\;1$ of Rloop) is
necessarily continuously enabled. Memory fairness ensures that the
corresponding transition is eventually executed, and from that point on,
${\mathcal{M}}_{\mathsf{RA}}$ prohibits the second thread from executing
${{\mathtt{R}}}({{x}},{0})$.

We emphasize again that memory fairness is sensitive to the choice of silent
memory transitions. For instance, the system obtained from
${\mathcal{M}}_{\mathsf{RA}}$ by discarding the message $m$ from the labels of
silent memory steps induces the same set of behaviors as
${\mathcal{M}}_{\mathsf{RA}}$, but not the same set of _memory fair_
behaviors. In the next sections, we present the declarative approach for
defining the semantics of memory systems, which uniformly captures memory
fairness, and does not require the technical ingenuity needed for ensuring
fairness in operational memory systems.

###  3.4. The Strong-Coherence Memory System

We consider a memory system for Strong-Coherence (StrongCOH), _i.e.,_ the
relaxed fragment of RC11. Similar to RA, we follow an operational formulation
of StrongCOH following the relaxed and promise-free fragment of the Promising
Semantics of Kang et al. (2017). Since this operational formulation is very
close to RA’s one discussed above, we describe only the difference between
them.

The states of ${\mathcal{M}}_{\mathsf{StrongCOH}}$ are the same as of
${\mathcal{M}}_{\mathsf{RA}}$, and transitions are similar, where the only
difference is in the read transition (note the crossed out
“$\sqcup\mathit{V}$”):

$\inferrule*{{\langle{{x}:v@t,\mathit{V}}\rangle}\in{M}\\\
\mathit{T}({\tau})({x})\leq t\\\
\mathit{T}^{\prime}=\mathit{T}[{\tau}\mapsto\mathit{T}({\tau})[{x}\mapsto
t]\cancel{\sqcup\mathit{V}}]}{{\langle{{M},\mathit{T}}\rangle}\mathrel{\raisebox{-0.8pt}{$\xrightarrow{{\tau}:{{\mathtt{R}}}({{x}},{v})}$}}_{{\mathcal{M}}_{\mathsf{StrongCOH}}}{\langle{{M},\mathit{T}^{\prime}}\rangle}}$

That is, when a thread reads from a message, it does not update its view by
the message’s view but just by its timestamp.333In this model one may change
messages to not store views at all since they are never used. We keep the
message views only in order to be as close as possible to RA. This change
makes the semantics weaker: StrongCOH allows weak behavior of MP and SB+RMWs
from Examples 3.17 and 3.19.

We include the same silent memory transitions in
${\mathcal{M}}_{\mathsf{StrongCOH}}$ as we do for
${\mathcal{M}}_{\mathsf{RA}}$, which is enough to guarantee termination of
memory-fair executions of Rloop for the same reason as for RA.

##  4\. Preliminaries on Declarative Semantics

In this section, we review the declarative (a.k.a. axiomatic) framework for
assigning semantics to concurrent programs and present the well-known
declarative models for the four operational models presented above. Later, we
will extend the framework and the existing correspondence results with
fairness guarantees that account for infinite behaviors.

#### Relations

Given a binary relation (in particular, a function) $R$, $\textit{dom}{({R})}$
and $\textit{codom}{({R})}$ denote its domain and codomain. We write $R^{?}$,
$R^{+}$, and $R^{*}$ respectively to denote its reflexive, transitive, and
reflexive-transitive closures. The inverse relation is denoted by $R^{-1}$. We
denote by $R_{1}\mathbin{;}R_{2}$ the (left) composition of two relations
$R_{1},R_{2}$, and assume that $\mathbin{;}$ binds tighter than $\cup$ and
$\setminus$. We denote by $[A]$ the identity relation on a set $A$. In
particular, $[A]\mathbin{;}R\mathbin{;}[B]=R\cap(A\times B)$. For $n\geq 0$
and a relation $R$ on a set $A$, $R^{n}$ is recursively defined by
$R^{0}\triangleq[A]$ and $R^{n+1}\triangleq R\mathbin{;}R^{n}$. We write
$R^{\leq n}$ for the union $\bigcup_{1\leq i\leq n}R^{n}$.

#### Events

Events represent individual memory accesses in a run of a program. They
consist of a thread identifier, an event label, and a serial number used to
uniquely identify events and order the events inside each thread.

###### Definition 4.1.

An _event_ $e$ is a tuple ${\langle{k,{\tau}:{l}}\rangle}$ where
$k\in{\mathbb{N}}\cup\\{{\bot}\\}$ is a serial number inside each thread
($\bot$ for initialization events), ${\tau}\in\mathsf{Tid}\uplus\\{{\bot}\\}$
is a thread identifier ($\bot$ for initialization events), and
${l}\in\mathsf{ELab}$ is an event label (as defined in Def. 3.1). The
functions ${\mathtt{sn}}$, ${\mathtt{tid}}$, and ${\mathtt{elab}}$ return the
serial number, thread identifier, and the event label of an event. The
functions ${\mathtt{typ}}$, ${\mathtt{loc}}$, ${\mathtt{val_{r}}}$, and
${\mathtt{val_{w}}}$ are lifted to events in an obvious way. We denote by
$\mathsf{Event}$ the set of all events, and use ${\mathtt{R}},{\mathtt{W}}$,
and ${\mathtt{RMW}}$ to denote the following subsets:

$\displaystyle{\mathtt{R}}$
$\displaystyle\triangleq\\{{e\in\mathsf{Event}\;|\;{\mathtt{typ}}(e)={\mathtt{R}}\lor{\mathtt{typ}}(e)={\mathtt{RMW}}}\\}$
$\displaystyle{\mathtt{W}}$
$\displaystyle\triangleq\\{{e\in\mathsf{Event}\;|\;{\mathtt{typ}}(e)={\mathtt{W}}\lor{\mathtt{typ}}(e)={\mathtt{RMW}}}\\}$
$\displaystyle{\mathtt{RMW}}$
$\displaystyle\triangleq\\{{e\in\mathsf{Event}\;|\;{\mathtt{typ}}(e)={\mathtt{RMW}}}\\}$

We use subscripts and superscripts to restrict sets of events to certain
location and thread (_e.g.,_
${\mathtt{W}}_{x}=\\{{w\in{\mathtt{W}}\;|\;{\mathtt{loc}}(w)={x}}\\}$ and
$E^{\tau}=\\{{e\in E\;|\;{\mathtt{tid}}(e)={\tau}}\\}$). The set of
_initialization events_ is given by
$\mathsf{Init}\triangleq\\{{{\langle{\bot,\bot:{{\mathtt{W}}}({{x}},{0})}\rangle}\;|\;{x}\in\mathsf{Loc}}\\}$.

###### Notation 4.2.

Given a relation $R$ on events, we denote by $R|_{{\mathtt{loc}}}$ the
restriction of $R$ to events of the same location:

$R|_{{\mathtt{loc}}}=\\{{{\langle{e_{1},e_{2}}\rangle}\in
R\;|\;\exists{x}\in\mathsf{Loc}.\;{\mathtt{loc}}(e_{1})={\mathtt{loc}}(e_{2})={x}}\\}$

Our representation of events induces a _sequenced-before_ partial order on
events given by:

$e_{1}<e_{2}\;\mathrel{\stackrel{{\scriptstyle\mathsf{\triangle}}}{{\Leftrightarrow}}}\;\begin{array}[]{@{}l@{}}(e_{1}\in\mathsf{Init}\land
e_{2}\not\in\mathsf{Init})\lor{}({\mathtt{tid}}(e_{1})={\mathtt{tid}}(e_{2})\land{\mathtt{sn}}(e_{1})<{\mathtt{sn}}(e_{2}))\end{array}$

Initialization events precede all non-initialization events, while events of
the same thread are ordered according to their serial numbers.

Behaviors (_i.e.,_ mappings from threads to sequential traces) are associated
with sets of events in an obvious way:

###### Definition 4.3.

The set of events _extracted from a behavior_ $\beta$, denoted by
$\mathsf{Event}(\beta)$, is given by
$\mathsf{Event}(\beta)\triangleq\mathsf{Init}\cup\\{{{\langle{k,{\tau}:\beta({\tau})(k)}\rangle}\;|\;{\tau}\in\mathsf{Tid},k\in\textit{dom}{({\beta({\tau})})}}\\}$.

It is easy to see that for every behavior $\beta$, $\mathsf{Event}(\beta)$
satisfies certain “well-formedness” properties:

###### Definition 4.4.

A set $E\subseteq\mathsf{Event}$ is _well-formed_ if the following hold:

  * •

$\mathsf{Init}\subseteq E$.

  * •

${\mathtt{tid}}(e)\neq\bot$ and ${\mathtt{sn}}(e)\neq\bot$ for every $e\in
E\setminus\mathsf{Init}$.

  * •

If ${\mathtt{tid}}(e_{1})={\mathtt{tid}}(e_{2})$ and
${\mathtt{sn}}(e_{1})={\mathtt{sn}}(e_{2})$, then $e_{1}=e_{2}$ for all
$e_{1},e_{2}\notin\mathsf{Init}$.

  * •

For every $e\in E\setminus\mathsf{Init}$ and $0\leq k<{\mathtt{sn}}(e)$, there
exists ${l}\in\mathsf{ELab}$ such that
${\langle{k,{\mathtt{tid}}(e):{l}}\rangle}\in E$.

#### Execution Graphs

An execution graph consists of a set of events, a _reads-from_ mapping that
determines the write event from which each read reads its value, and a
_modification order_ which totally orders the writes to each location.

###### Definition 4.5.

An _execution graph_ $G$ is a tuple
${\langle{E,{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathit{rf}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathit{mo}}}\rangle}$
where:

  1. (1)

$E$ is a well-formed (possibly, infinite) set of events.

  2. (2)

${\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathit{rf}}$,
called _reads-from_ , is a relation on $E$ satisfying:

     * •

If
${\langle{w,r}\rangle}\in{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathit{rf}}$
then $w\in{\mathtt{W}}$, $r\in{\mathtt{R}}$,
${\mathtt{loc}}(w)={\mathtt{loc}}(r)$, and
${\mathtt{val_{w}}}(w)={\mathtt{val_{r}}}(r)$.

     * •

$w_{1}=w_{2}$ whenever
${\langle{w_{1},r}\rangle},{\langle{w_{2},r}\rangle}\in{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathit{rf}}$
(that is,
${\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathit{rf}}^{-1}$
is functional).

     * •

$E\cap{\mathtt{R}}\subseteq\textit{codom}{({{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathit{rf}}})}$
(every read should read from some write).

  3. (3)

${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathit{mo}}$,
called _modification order_ , is a disjoint union of relations
$\\{{{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathit{mo}}_{x}}\\}_{{x}\in\mathsf{Loc}}$,
such that each
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathit{mo}}_{x}$
is a strict total order on $E\cap{\mathtt{W}}_{x}$.

We denote the components of $G$ by $G.{\mathtt{E}}$,
$G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$,
and
$G.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$,
and write
$G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>(called _program order_) for the restriction of sequenced-before to
$G.{\mathtt{E}}$ (_i.e.,_
$G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}\mathtt{po}}\triangleq[G.{\mathtt{E}}];<;[G.{\mathtt{E}}]$).
For a set $E^{\prime}\subseteq\mathsf{Event}$, we write $G.E^{\prime}$ for
$G.{\mathtt{E}}\cap E^{\prime}$ (_e.g.,_
$G.{\mathtt{W}}=G.{\mathtt{E}}\cap{\mathtt{W}}$). The set of all execution
graphs is denoted by $\mathsf{EGraph}$.

A _declarative memory system_ is simply a set $\mathcal{G}$ of execution
graphs (often formulated using a conjunction of several constraints). We refer
to execution graphs in a declarative memory system $\mathcal{G}$ as
_$\mathcal{G}$ -consistent_ execution graphs.

We can now define the behaviors allowed by a given declarative memory system.

###### Definition 4.6.

A behavior $\beta$ is _allowed by a declarative memory system_ $\mathcal{G}$
if $\mathsf{Event}(\beta)=G.{\mathtt{E}}$ for some execution graph
$G\in\mathcal{G}$. We denote by $\mathsf{B}({\mathcal{G}})$
($\mathsf{B^{fin}}({\mathcal{G}})$) the set of all (finite) behaviors that are
allowed by $\mathcal{G}$.

The linking with programs is defined as follows.

###### Definition 4.7.

Let ${P}$ be a program, $\mathcal{G}$ be a declarative memory system, and
$\beta$ be a behavior.

  * •

$\beta$ is a _behavior of ${P}$ under $\mathcal{G}$_ if
$\beta\in\mathsf{B}({{P}})\cap\mathsf{B}({\mathcal{G}})$.

  * •

$\beta$ is a _thread-fair behavior of ${P}$ under $\mathcal{G}$_ if
$\beta\in\mathsf{B^{tf}}({{P}})\cap\mathsf{B}({\mathcal{G}})$.

###  4.1. A Declarative Memory System for SC

To provide a declarative formulation of $\mathsf{SC}$, following Alglave et
al. (2014), we use the standard “from-read” relation (a.k.a. “reads-before”).
In this relation a read $r$ is ordered before a write $w$ if $r$ reads from a
write $w^{\prime}$ that is earlier than $w$ in the modification order.

###### Definition 4.8.

The _from-read_ relation for an execution graph $G$, denoted by
$G.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$,
is defined by:

$G.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}\triangleq(G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}^{-1}\mathbin{;}G.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}})\setminus[G.{\mathtt{E}}].$

Note that we have to explicitly subtract the identity relation from
$G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}^{-1}\mathbin{;}G.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
for making sure that ${\mathtt{RMW}}$ events are not
$G.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$-ordered
before themselves.

Having defined
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$,
the “$\mathsf{SC}$-happens-before” relation is given by:

$G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{SC}}\triangleq(G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}\cup
G.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}\cup
G.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}})^{+}$

In turn, $\mathsf{SC}$ consistency requires that
$G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{SC}}$
is irreflexive:

$\mathcal{G}_{\mathsf{SC}}\triangleq\\{{G\in\mathsf{EGraph}\;|\;G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{SC}}\text{
is irreflexive}}\\}$

Intuitively speaking, every trace of ${\mathcal{M}}_{\mathsf{SC}}$ induces an
execution graph $G$ with irreflexive
$G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{SC}}$;
and, conversely, every total order on $G.{\mathtt{E}}$ that extends
$G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{SC}}$
is essentially a trace of ${\mathcal{M}}_{\mathsf{SC}}$. The following
standard theorem formalizes these claims for _finite_ executions:

###### Theorem 4.9 ((Alglave et al., 2014)).

$\mathsf{B^{fin}}({{\mathcal{M}}_{\mathsf{SC}}})=\mathsf{B^{fin}}({\mathcal{G}_{\mathsf{SC}}})$.

###### Example 4.10.

$\mathcal{G}_{\mathsf{SC}}$ forbids the annotated outcome of the SB program
from Example 3.15 because the following graph is
$\mathcal{G}_{\mathsf{SC}}$-inconsistent (${{\mathtt{W}}}({{x}},{0})$ and
${{\mathtt{W}}}({{y}},{0})$ are the implicit initialization writes):

${{\mathtt{W}}}({{x}},{0})$${{\mathtt{W}}}({{y}},{0})$${{\mathtt{W}}}({{x}},{1})$
${{\mathtt{R}}}({{y}},{0})$ ${{\mathtt{W}}}({{y}},{1})$
${{\mathtt{R}}}({{x}},{0})$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$${\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$

Indeed, to get the desired behavior, the
${\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$-edges
are forced because of the read values. Since
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
cannot contradict
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>(they are both included in
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{SC}}$),
the
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$-edges
are also forced as depicted above. We obtain
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$-edges
from ${{\mathtt{R}}}({{x}},{0})$ to ${{\mathtt{W}}}({{x}},{1})$ and from
${{\mathtt{R}}}({{y}},{0})$ to ${{\mathtt{W}}}({{y}},{1})$, which, in turn,
imply a
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{SC}}$-cycle
composed of two
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>and two
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
edges.

###  4.2. A Declarative Memory System for TSO

Following Alglave et al. (2014), a declarative formulation for $\mathsf{TSO}$
is easily obtained from the one of $\mathsf{SC}$, by removing from the
transitive closure in
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{SC}}$
the program order edges from writes to reads that are not necessarily
“preserved” in $\mathsf{TSO}$. Indeed, because writes are buffered in
$\mathsf{TSO}$, roughly speaking, the effect of a write in $\mathsf{TSO}$ may
be delayed w.r.t. subsequent reads. By contrast, it cannot be delayed w.r.t.
subsequent writes, since entries in the $\mathsf{TSO}$ buffers propagate in a
FIFO fashion.

When removing the write to read program order edges, we need to explicitly
enforce “$\mathsf{SC}$ per-location” (a.k.a. coherence), which takes care of
intra-thread write-read pairs (a read $r$ from ${x}$ that is later in program
order than a write $w$ to ${x}$ may not read from a write that is
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$-earlier
than $w$). To achieve this, the model employs the following derived relations:

(_external reads-from_) $\displaystyle
G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}\mathtt{e}$
$\displaystyle\triangleq
G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}\setminus
G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>(_preserved program order_) $\displaystyle
G.{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{ppo}}$
$\displaystyle\triangleq
G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}\mathtt{po}}\setminus(({\mathtt{W}}\setminus{\mathtt{RMW}})\times({\mathtt{R}}\setminus{\mathtt{RMW}}))$
(_$\mathsf{TSO}$ -happens-before _) $\displaystyle
G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{TSO}}$
$\displaystyle\triangleq(G.{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{ppo}}\cup
G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}\mathtt{e}\cup
G.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}\cup
G.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}})^{+}$
(_SC-per-location order_) $\displaystyle G.{\mathtt{sc}}_{{\mathtt{loc}}}$
$\displaystyle\triangleq(G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}\cup
G.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}\cup
G.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}})^{+}$

Then, $\mathsf{TSO}$ consistency requires that
$G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{TSO}}$
and $G.{\mathtt{sc}}_{{\mathtt{loc}}}$ are irreflexive:

$\mathcal{G}_{\mathsf{TSO}}\triangleq\\{G\in\mathsf{EGraph}\;|\;G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{TSO}}\text{\
and\ }G.{\mathtt{sc}}_{{\mathtt{loc}}}\text{\ are irreflexive}\\}$

###### Theorem 4.11 ((Alglave et al., 2014)).

$\mathsf{B^{fin}}({{\mathcal{M}}_{\mathsf{TSO}}})=\mathsf{B^{fin}}({\mathcal{G}_{\mathsf{TSO}}})$.

The execution graph for the SB program in Example 4.10 is
$\mathcal{G}_{\mathsf{TSO}}$-consistent. In particular, the two
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>edges that participate in the
$G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{SC}}$
cycle are from a write to a read, so none of them is included in
$G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{TSO}}$.

###  4.3. A Declarative Memory System for RA

The declarative model for $\mathsf{RA}$ is obtained by strengthening the SC
per-location requirement to use $\mathsf{RA}$’s happens-before relation
instead of the program order:

(_$\mathsf{RA}$ -happens-before_) $\displaystyle
G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{RA}}$
$\displaystyle\triangleq(G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}})^{+}$
(_$\mathsf{RA}$ -per-location order_) $\displaystyle
G.{\mathtt{ra}}_{{\mathtt{loc}}}$
$\displaystyle\triangleq(G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{RA}}|_{{\mathtt{loc}}}\cup
G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}\cup
G.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}\cup
G.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}})^{+}$

Then, $\mathsf{RA}$ consistency requires that
$G.{\mathtt{ra}}_{{\mathtt{loc}}}$ is irreflexive:

$\mathcal{G}_{\mathsf{RA}}\triangleq\\{{G\in\mathsf{EGraph}\;|\;G.{\mathtt{ra}}_{{\mathtt{loc}}}\text{\
is irreflexive}}\\}$

###### Example 4.12.

The annotated outcome of the MP program from Example 3.17 is disallowed by
$\mathcal{G}_{\mathsf{RA}}$ because the following (partially depicted)
execution graph is $\mathcal{G}_{\mathsf{RA}}$-inconsistent:

${{\mathtt{W}}}({{x}},{0})$${{\mathtt{W}}}({{y}},{0})$${{\mathtt{W}}}({{x}},{1})$
${{\mathtt{W}}}({{y}},{1})$ ${{\mathtt{R}}}({{y}},{1})$
${{\mathtt{R}}}({{x}},{0})$
${\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}\
$${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$

An execution graph for this outcome must have
${\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$
and
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$-edges
as depicted above. Since
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
goes from ${{\mathtt{W}}}({{x}},{0})$ to ${{\mathtt{W}}}({{x}},{1})$, and
${{\mathtt{R}}}({{x}},{0})$ reads from ${{\mathtt{W}}}({{x}},{0})$, we have an
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
edge from ${{\mathtt{R}}}({{x}},{0})$ to ${{\mathtt{W}}}({{x}},{1})$. Due to
the
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{RA}}$
from ${{\mathtt{W}}}({{x}},{1})$ to ${{\mathtt{R}}}({{x}},{0})$, we obtain a
${\mathtt{ra}}_{{\mathtt{loc}}}$-cycle, rendering this graph
$\mathcal{G}_{\mathsf{RA}}$-inconsistent.

###### Example 4.13.

Similarly, the annotated outcome of 2RMW from Example 3.18 is disallowed by
$\mathcal{G}_{\mathsf{RA}}$ because the following execution graph is
$\mathcal{G}_{\mathsf{RA}}$-inconsistent for any choice of
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$:

${{\mathtt{W}}}({{x}},{0})$${{\mathtt{RMW}}}({{x}},{0},{1})$
${{\mathtt{RMW}}}({{x}},{0},{1})$
${\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$${\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$

To see this, note that in $\mathcal{G}_{\mathsf{RA}}$-consistent executions,
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
cannot contradict
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>Hence, we must have
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
from the initial write to the two RMWs. This implies an
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
edge in both directions between the two RMWs, so that
${\mathtt{ra}}_{{\mathtt{loc}}}$ must be cyclic.

Equivalence to the operational RA model for _finite_ behaviors follows from
(Kang et al., 2017):

###### Theorem 4.14.

$\mathsf{B^{fin}}({{\mathcal{M}}_{\mathsf{RA}}})=\mathsf{B^{fin}}({\mathcal{G}_{\mathsf{RA}}})$.

###  4.4. A Declarative Memory System for StrongCOH

The declarative model for $\mathsf{StrongCOH}$ is obtained by requiring “SC
per-location” and irreflexivity of $\mathsf{RA}$’s happens-before,
$(G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}})^{+}$:

$\mathcal{G}_{\mathsf{StrongCOH}}\triangleq\\{{G\in\mathsf{EGraph}\;|\;G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{RA}}\text{
and }G.{\mathtt{sc}}_{\mathtt{loc}}\text{\ are irreflexive}}\\}$

Similarly to $\mathsf{RA}$, equivalence to the operational
$\mathsf{StrongCOH}$ model for _finite_ behaviors follows from the results of
Kang et al. (2017):

###### Theorem 4.15.

$\mathsf{B^{fin}}({{\mathcal{M}}_{\mathsf{StrongCOH}}})=\mathsf{B^{fin}}({\mathcal{G}_{\mathsf{StrongCOH}}})$.

##  5\. Making Declarative Semantics Fair

###  5.1. Proofs for Section 5

In this section, we introduce memory fairness into declarative models in a
model-agnostic fashion.

To define fairness of execution graphs, we require that the partial ordering
of events in the graph is, like the ordering of natural numbers, _prefix-
finite_. From an operational point of view, an event preceded by an infinite
number of events is never executed.

###### Definition 5.1.

A relation $R$ on a set $A$ is _prefix-finite_ if
$\\{{a\;|\;{\langle{a,b}\rangle}\in R}\\}$ is finite for every $b\in A$.

Concretely, we require the modification order and the from-read relation to be
prefix-finite.444Note that the _program order_ and the _reads-from_ relation
are prefix-finite in a well-formed execution graph. The former–by
construction, the latter–since its reverse relation is functional.

###### Definition 5.2.

An execution graph $G$ is _fair_ if
$G.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
and
$G.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
are prefix-finite. We denote by $\mathcal{G}^{\texttt{fair}}$ the set of all
fair execution graphs, and let
$\mathcal{G}_{X}^{\texttt{fair}}\triangleq\mathcal{G}_{X}\cap\mathcal{G}^{\texttt{fair}}$
for $X\in\\{{\mathsf{SC},\mathsf{TSO},\mathsf{RA},\mathsf{StrongCOH}}\\}$.

###### Example 5.3.

The following program illustrates our definition of fairness:

(SCDeclUnfair)
$\begin{array}[]{@{}l@{~~}||@{~~}l@{}}\begin{array}[]{@{}l@{}}\phantom{L_{1}\colon}{x}\;{:=}\;1\,;\\\
L_{1}\colon
a\;{:=}\;{x}\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}{~{}~{}\texttt{/\\!\\!/}\textit{\text{only}
1}}\\\
\phantom{L_{1}\colon}\textbf{{goto}}\;L1\end{array}\hfil~{}~{}\vrule\vrule~{}~{}&\begin{array}[]{@{}l@{}}L_{2}\colon{x}\;{:=}\;2\,;\\\
\phantom{L_{2}\colon}\textbf{{goto}}\;L_{2}\end{array}\end{array}$

Thread-fair executions of this program cannot produce the annotated outcome
with the $\mathsf{SC}$ memory system. With the declarative $\mathsf{SC}$
memory system, however, there are two ways in which every read can read from
the write of $1$.

First, the write of $1$ to $x$ may have infinitely many
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$-predecessors,
as illustrated below.

${{\mathtt{W}}}({x},{1})$Thread 1:
${{\mathtt{R}}}({x},{1})$${{\mathtt{R}}}({x},{1})$$\cdots$${{\mathtt{W}}}({x},{2})$Thread
2:
${{\mathtt{W}}}({x},{2})$${{\mathtt{W}}}({x},{2})$$\cdots$${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$${\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$${\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$

Otherwise, the write of $1$ may have finitely many
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$-predecessors
but infinitely many
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$-successors.
Then, each of the
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$-successors
will have infinitely many
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$-predecessors.

${{\mathtt{W}}}({x},{1})$Thread 1:
${{\mathtt{R}}}({x},{1})$${{\mathtt{R}}}({x},{1})$$\cdots$${{\mathtt{W}}}({x},{2})$Thread
2:
${{\mathtt{W}}}({x},{2})$${{\mathtt{W}}}({x},{2})$$\cdots$${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$${\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$${\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$

In both cases, the execution graph is unfair. (As we prove below, this is not
a coincidence.)

###### Example 5.4.

On the converse, one should avoid unnecessary prefix-finiteness constraints.
In particular, requiring prefix-finiteness of cyclic relations, such as
$[G.{\mathtt{E}}\setminus\mathsf{Init}]\mathbin{;}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{SC}}$
under $\mathsf{TSO}$, $\mathsf{RA}$, or $\mathsf{StrongCOH}$, is too strong.
Doing so would forbid the annotated behavior of the following example, since
the corresponding execution graph contains an infinite
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}\mathtt{po}}\cup{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
descending chain. Yet, $\mathsf{TSO}$, $\mathsf{RA}$, and $\mathsf{StrongCOH}$
allow the annotated behavior, as every write may be delayed past 1 or 2 reads.

$\displaystyle\begin{array}[]{@{}l@{~~}||@{~~}l@{}}\begin{array}[]{@{}l@{}}L_{1}\colon
k\;{:=}\;k+1\\\ \phantom{L_{1}\colon}x\;{:=}\;k\\\
\phantom{L_{1}\colon}a\;{:=}\;y\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}{~{}~{}\texttt{/\\!\\!/}\textit{0,0,1,2\ldots}}\\\
\phantom{L_{1}\colon}\textbf{{goto}}\;L_{1}\end{array}\hfil~{}~{}\vrule\vrule~{}~{}&\begin{array}[]{@{}l@{}}L_{2}\colon
m\;{:=}\;m+1\\\ \phantom{L_{2}\colon}y\;{:=}\;m\\\
\phantom{L_{2}\colon}b\;{:=}\;x\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}{~{}~{}\texttt{/\\!\\!/}\textit{0,1,2,3\ldots}}\\\
\phantom{L_{2}\colon}\textbf{{goto}}\;L_{2}\end{array}\end{array}$
${{\mathtt{W}}}({x},{1})$Thread 1:
${{\mathtt{R}}}({y},{0})$${{\mathtt{W}}}({x},{2})$${{\mathtt{R}}}({y},{0})$${{\mathtt{W}}}({x},{3})$${{\mathtt{R}}}({y},{1})$${{\mathtt{W}}}({y},{1})$Thread
2:
${{\mathtt{R}}}({x},{0})$${{\mathtt{W}}}({y},{2})$${{\mathtt{R}}}({x},{1})$${{\mathtt{W}}}({y},{3})$${{\mathtt{R}}}({x},{2})$…

Our main result extends Theorems 4.9, 4.11, 4.14 and 4.15 for _infinite_
traces by imposing memory fairness on the operational systems (Def. 3.12) and
execution graph fairness on the declarative systems (Def. 5.2).

###### Theorem 5.5.

For $X\in\\{{\mathsf{SC},\mathsf{TSO},\mathsf{RA},\mathsf{StrongCOH}}\\}$,

$\mathsf{B^{mf}}({{\mathcal{M}}_{X}})=\mathsf{B}({\mathcal{G}_{X}^{\texttt{fair}}}).$

As a corollary, it easily follows from our definitions that the set of
(thread&) memory-fair behaviors of a program ${P}$ under ${\mathcal{M}}_{X}$
coincides with the set of (thread&) memory-fair behaviors of a program ${P}$
under $\mathcal{G}_{X}^{\texttt{fair}}$.

The full proof of Theorem 5.5 is included in appendix ((Lahav et al., 2021a))
and its Coq mechanization in (Lahav et al., 2021b). Here, we outline the proof
starting with the easier direction.

###  5.2.
$\mathsf{B^{mf}}({{\mathcal{M}}_{X}})\subseteq\mathsf{B}({\mathcal{G}_{X}^{\texttt{fair}}})$

Given a memory-fair behavior $\beta$ of ${\mathcal{M}}_{X}$, we let $\rho$ be
a memory-fair observable trace of ${\mathcal{M}}_{X}$ such that
$\beta(\rho)=\beta$. Then, using $\rho$, we construct a fair execution graph
$G\in\mathcal{G}_{X}$. Its events are determined by $\beta$
($G.{\mathtt{E}}=\mathsf{Event}(\beta)$), and its relations are defined
differently for every system:

#### SC

The
${\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$
and
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
relations are determined by the trace order: for each read
${\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$
assigns the latest write of the same location, while
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
corresponds to the trace order restricted to writes to the same location. It
follows that
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
is included in the trace order, and since the trace order is prefix-finite,
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
and
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
are prefix-finite as well.

#### TSO

We define
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
to be the order in which writes to the same location are propagated
(unbuffered) to memory. For each read,
${\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$
maps it either to the
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$-maximal
write to the same location that was propagated before it in $\rho$ (if the
read reads from memory) or to the
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>one by the same thread (if it reads from the buffer). Since every write is
eventually propagated to memory, and once propagated no thread can read from
an
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$-prior
write, it follows that both
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
and
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
are prefix-finite.

#### RA and StrongCOH

The
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
component of $G$ follows the order induced by timestamps of messages in the
operational run. Prefix-finiteness of
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
follows from the facts that a location and a timestamp uniquely identify the
corresponding message (and the write event in $G$ respectively) and that
timestamps are natural numbers—that is, each write event $w$ representing a
message with a timestamp $t$ has at most $t$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$-prior
writes.

The
${\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$
component of $G$ connects an event related to a read/RMW transition of $\rho$
with a write event representing the message read by the transition.

Prefix-finiteness of
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
follows from the fact that in the fair operational run every message is
eventually propagated to every thread. That is, for any given write event $w$
to a location ${x}$ in $G$ representing a message with a timestamp $t$, there
cannot be infinitely many reads from ${x}$ in $G$ reading from write events
that correspond to messages with timestamps smaller than $t$.

###  5.3.
$\mathsf{B}({\mathcal{G}_{X}^{\texttt{fair}}})\subseteq\mathsf{B^{mf}}({{\mathcal{M}}_{X}})$

The converse direction is more challenging. Given a fair
$\mathcal{G}_{X}$-consistent execution graph $G$, we have to find a memory-
fair observable trace $\rho$ of ${\mathcal{M}}_{X}$ such that
$\mathsf{Event}(\beta(\rho))=G.{\mathtt{E}}$.

Put differently, we need a total order over
$G.{\mathtt{E}}\setminus\mathsf{Init}$ that extends
$G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>so that some memory-fair run of ${\mathcal{M}}_{X}$ executes according to this
order. Existing proofs of correspondence between declarative and operational
definitions of SC, RA, and StrongCOH pick an arbitrary total order extending
$G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{SC}}$
(for SC) and
$G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{RA}}$
(for RA and StrongCOH). (Assuming the axiom of choice, any partial order $R$
on a set $A$ can be extended to a total order on $A$.) It is then not
difficult to show that executing the program following that order yields the
labels appearing in the execution graph. For infinite graphs, however, an
arbitrary extension of
$G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{SC}}$
(or
$G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{RA}}$
respectively) does not necessarily correspond to a (memory-fair) run of the
program. For this, we need an _enumeration_ of
$G.{\mathtt{E}}\setminus\mathsf{Init}$, as defined next.

###### Definition 5.6.

An _enumeration_ of a set $A$ is a (finite or infinite) injective (_i.e.,_
without repetitions) sequence $\nu$ covering all the elements in $A$ (_i.e.,_
$A=\\{{\nu(i)\;|\;i\in\textit{dom}{({\nu})}}\\}$). An enumeration $\nu$ of $A$
_respects_ a partial order $R$ on $A$ if $i<j$ whenever
${\langle{\nu(i),\nu(j)}\rangle}\in R$.

Prefix-finiteness of a partial order ensures that a suitable enumeration
exists (our proof employs classical, non-constructive, reasoning):

###### Proposition 5.7.

Let $R$ be a prefix-finite partial order on a countable set $A$. Then, there
exists an enumeration of $A$ that respects $R$.

prop:respect-enum Let $\nu$ be an enumeration on $A$. For $i\in{\mathbb{N}}$,
let $S^{i}=\\{{\nu(i)}\\}\cup\\{{a\;|\;{\langle{a,\nu(i)}\rangle}\in R}\\}$ be
the set containing $\nu(i)$ and all its $R$-predecessors. Note that this set
is finite because $R$ is prefix-finite.

Now let $T^{i}=S^{i}\setminus\bigcup\\{{S^{j}\;|\;j<i}\\}$ be the set of new
elements in $S^{i}$ (_i.e.,_ those not included in the $S$-set for previous
indices). Since $T^{i}$ is a finite set, it can be topologically ordered with
respect to $R$ yielding a sequence $t^{i}_{1}\ldots t^{i}_{|T^{i}|}$
respecting $R$.

We will now define an enumeration $\mu$ on $A$ that respects $R$. Let $\mu(i)$
to be the $i^{\textrm{th}}$ element of the sequence

$t^{1}_{1}\,t^{1}_{2}\ldots t^{1}_{|T^{1}|}\,t^{2}_{1}\,t^{2}_{2}\ldots
t^{2}_{|T^{2}|}\ldots t^{i}_{1}\,t^{i}_{2}\ldots t^{i}_{|T^{i}|}.$

Note that this sequence has at least $i$ elements, so $\mu(i)$ is well
defined. Moreover, by construction, this sequence has no duplicates, respects
$R$, and the sequence for $i$ is a prefix of the sequence for $i+1$. From
these facts, it follows that $\mu$ is an enumeration of $A$ that respects $R$.

However, we do not yet have that the “happens-before” relation of each model
is prefix-finite; we only know that
$G.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
and
$G.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
are prefix-finite. Next, we show that prefix-finiteness of
$G.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
and
$G.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
suffices for prefix-finiteness of the other relations, as long as the program
in question has a bounded number of threads. (Recall that we assume that the
set $\mathsf{Tid}$ is finite.)

First, note that every relation on a finite set is prefix-finite, and prefix-
finiteness is preserved by (finite) composition.

###### Lemma 5.8.

Let $R$ and $R^{\prime}$ be prefix-finite relations and $n\in{\mathbb{N}}$.
Then $R\cup R^{\prime}$, $R\mathbin{;}R^{\prime}$ and $R^{\leq n}$ are also
prefix-finite.

For transitive closures, we need an auxiliary property.

###### Definition 5.9.

A relation $R$ on a set $A$ is _$n$ -total_ if for every $n+1$ distinct
elements $a_{1}{,}\ldots{,}a_{n+1}\in A$, we have
${\langle{a_{i},a_{j}}\rangle}\in R$ for some $1\leq i,j\leq n+1$.

For an execution graph $G$ with $n$ threads,
$G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>is $n$-total (as a relation on $G.{\mathtt{E}}\setminus\mathsf{Init}$). By the
pigeonhole principle, any set of $n+1$ events in
$G.{\mathtt{E}}\setminus\mathsf{Init}$ contain two elements belonging to the
same thread, and those two events are ordered by
$G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>
Now, if a relation $R$ is $n$-total and acyclic, its transitive closure
$R^{+}$ has bounded length, which entails that $R^{+}$ is prefix-finite
provided $R$ is prefix-finite.

###### Lemma 5.10.

Let $R$ be an acyclic, $n$-total, prefix-finite relation. Then, $R^{+}$ is
prefix-finite.

lem:ct-pref-fin It suffices to show that $R^{2n+1}\subseteq R^{\leq 2n}$. The
reason is that then $R^{+}\subseteq R^{\leq 2n}$, and so by Lemma 5.8, $R^{+}$
is prefix-finite. Consider therefore a set of $2n+1$ distinct elements
$a_{1}{,}\ldots{,}a_{2n+1}\in A$ such that ${\langle{a_{k},a_{k+1}}\rangle}\in
R$ for all $1\leq k\leq 2n$. Consider the set of $n+1$ elements
$a_{1},a_{3},a_{2n+1}$. By $n$-totality, there exist $1\leq i,j\leq n+1$ such
that ${\langle{a_{2i+1},a_{2j+1}}\rangle}\in R$. Since $R$ is acyclic, it
follows that $i<j$, and so there is a shorter path from $a_{1}$ to $a_{2n+1}$,
_i.e.,_ ${\langle{a_{1},a_{2n+1}}\rangle}\in R^{\leq 2n}$, as required. (In
more detail, we have ${\langle{a_{1},a_{2i+1}}\rangle}\in R^{2i+1}$,
${\langle{a_{2i+1},a_{2j+1}}\rangle}\in R$,
${\langle{a_{2j+1},a_{2n+1}}\rangle}\in R^{2n-2j}$, and so
${\langle{a_{1},a_{2n+1}}\rangle}\in R^{2i+1+1+2n-2j}=R^{2(n+i+1-j)}\subseteq
R^{\leq 2n}$.)

As a corollary, we obtain that the prefix-finiteness of the “happens-before”
relation in fair execution graphs.

###### Corollary 5.11.

For $X\in\\{{\mathsf{SC},\mathsf{TSO},\mathsf{RA},\mathsf{StrongCOH}}\\}$, let
$G$ be a fair $\mathcal{G}_{X}$-consistent execution graph. Then
$[G.{\mathtt{E}}\setminus\mathsf{Init}]\mathbin{;}G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{X}$
is prefix finite.555We define
$G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{StrongCOH}}$
to be equal to
$G.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{RA}}$.

cor:hb-pf In all cases, by applying Lemma 5.10, it suffices to show that the
non-transitive versions of these relations are acyclic, prefix-finite, and
$n$-total. Acyclicity follows by the consistency conditions, prefix-finiteness
follows by Lemma 5.8 as they are unions of prefix-finite relations.

$n$-totality follows immediately for SC, RA, and StrongCOH, because
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>is $n$-total where $n$ is the number of threads.

In the case of TSO,
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}\mathtt{po}}\setminus(({\mathtt{W}}\setminus{\mathtt{RMW}})\times({\mathtt{R}}\setminus{\mathtt{RMW}}))$
is $2n$-total (where $n$ is the number of threads) because for every three
events in the same thread at least two of them are related by
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}\mathtt{po}}\setminus(({\mathtt{W}}\setminus{\mathtt{RMW}})\times({\mathtt{R}}\setminus{\mathtt{RMW}}))$.
Namely, let the three events be $a$, $b$, and $c$, and without loss of
generality assume that
${\langle{a,b}\rangle}\in{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>and
${\langle{b,c}\rangle}\in{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>If
${\langle{a,b}\rangle}\notin({\mathtt{W}}\setminus{\mathtt{RMW}})\times({\mathtt{R}}\setminus{\mathtt{RMW}})$,
then ${\langle{a,b}\rangle}$ satisfies the required condition. Otherwise,
depending on the type of $c$, either ${\langle{b,c}\rangle}$ or
${\langle{a,c}\rangle}$ satisfy it.

From Prop. 5.7, there is an enumeration $\nu$ that respects
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{X}$.
We use $\nu$ to construct a program trace $\rho$:

#### SC

The trace $\rho$ follows $\nu$ exactly. Since ${\mathcal{M}}_{\mathsf{SC}}$
has no silent memory transitions, $\rho$ is trivially memory fair.

#### TSO

The trace $\rho$ is incrementally constructed by following the order of events
in $\nu$ and appending an appropriate sequence of transitions. If the next
event in $\nu$ is a read, we append to $\rho$ all unexecuted
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>writes and then the read. If the next event in $\nu$ is a write, we append the
write to the trace if it has not already been included in the trace. In
addition, when the next event is a write, we append its propagation action to
memory. By construction, every write in $\rho$ is eventually propagated to
memory.

#### RA and StrongCOH

The trace $\rho$ is the enumeration $\nu$ interleaved with silent
$\mathsf{RA}$/$\mathsf{StrongCOH}$ transition labels. Namely, for each write
$w$ and thread ${\tau}$, we compute an index $i$ in the enumeration such that
it is _safe_ to propagate $w$ to ${\tau}$ at that index: for each event in
${\tau}$ with index greater than $i$, there is no $\mathtt{X}$-following
(where
$\mathtt{X}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{RA}}$
for $\mathsf{RA}$ and
$\mathtt{X}={\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}^{?}\mathbin{;}{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}\mathtt{po}}^{?}$
for $\mathsf{StrongCOH}$) (i) write that
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$-precedes
$w$ and (ii) read that reads from a write
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$-preceding
$w$. Since $G$ is fair, such an index is defined for all (non-initialization)
writes. Then, after the event with an index corresponding to some write has
been enumerated, we execute a propagation transition for the write. In that
way, every write is eventually propagated to every thread, so the resulting
trace is memory fair.

###### Remark 3.

Corollary 5.11 relies on having a bounded number of threads. With infinite
number of threads, generated, _e.g.,_ by thread spawning, prefix-finiteness of
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
and
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
is not enough to rule out unfair behaviors. To see this, consider the
annotated behavior of the following program and the corresponding execution
graph:

$\displaystyle{\begin{array}[]{@{}l@{}}L\colon i\;{:=}\;i+1\\\
\phantom{L\colon}\textbf{{spawn}}\left\\{\;\begin{array}[]{@{}l@{}}x_{i+1}:=1\\\
a:=x_{i}\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}{~{}~{}\texttt{/\\!\\!/}\textit{only
0}}\\\ \end{array}\;\right\\}\\\
\phantom{L\colon}\textbf{{goto}}\;L\end{array}}\qquad\begin{array}[]{@{}l@{}}\leavevmode\hbox
to198.37pt{\vbox to39.43pt{\pgfpicture\makeatletter\hbox{\hskip
66.03192pt\lower 14.42928pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-62.69891pt}{43.02458pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${{\mathtt{W}}}({x_{2}},{1})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-61.24057pt}{20.26228pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${{\mathtt{R}}}({x_{1}},{0})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-17.17433pt}{43.02458pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${{\mathtt{W}}}({x_{3}},{1})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-15.71599pt}{20.26228pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${{\mathtt{R}}}({x_{2}},{0})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{28.35025pt}{43.02458pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${{\mathtt{W}}}({x_{4}},{1})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{29.8086pt}{20.26228pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${{\mathtt{R}}}({x_{3}},{0})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{98.61705pt}{27.5212pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\Huge$\cdot\\!\cdot\\!\cdot$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{75.33318pt}{20.26228pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${{\mathtt{R}}}({x_{4}},{0})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{tikz@color}{rgb}{0.3,0.3,0.3}\definecolor[named]{.}{rgb}{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-45.52473pt}{38.41435pt}\pgfsys@lineto{-45.52473pt}{31.87273pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{-45.52473pt}{31.87273pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{tikz@color}{rgb}{0.3,0.3,0.3}\definecolor[named]{.}{rgb}{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{0.0pt}{38.41435pt}\pgfsys@lineto{0.0pt}{31.87273pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{0.0pt}{31.87273pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{tikz@color}{rgb}{0.3,0.3,0.3}\definecolor[named]{.}{rgb}{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{45.52473pt}{38.41435pt}\pgfsys@lineto{45.52473pt}{31.87273pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{45.52473pt}{31.87273pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{tikz@color}{rgb}{.75,0,.25}\definecolor[named]{.}{rgb}{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\pgfsys@color@rgb@stroke{.75}{0}{.25}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{.75}{0}{.25}\pgfsys@invoke{
}\pgfsys@setdash{0.8pt,2.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-15.79147pt}{30.65932pt}\pgfsys@lineto{-27.40652pt}{36.46533pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.89447}{0.44711}{-0.44711}{-0.89447}{-27.40651pt}{36.46533pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-19.02878pt}{33.85422pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\pgfsys@color@rgb@stroke{.75}{0}{.25}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{.75}{0}{.25}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{.75,0,.25}\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\smaller${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{tikz@color}{rgb}{.75,0,.25}\definecolor[named]{.}{rgb}{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\pgfsys@color@rgb@stroke{.75}{0}{.25}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{.75}{0}{.25}\pgfsys@invoke{
}\pgfsys@setdash{0.8pt,2.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{29.73341pt}{30.65932pt}\pgfsys@lineto{18.11821pt}{36.46533pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.89449}{0.44711}{-0.44711}{-0.89449}{18.11823pt}{36.46533pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{26.49602pt}{33.85422pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\pgfsys@color@rgb@stroke{.75}{0}{.25}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{.75}{0}{.25}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{.75,0,.25}\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\smaller${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{tikz@color}{rgb}{.75,0,.25}\definecolor[named]{.}{rgb}{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\pgfsys@color@rgb@stroke{.75}{0}{.25}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{.75}{0}{.25}\pgfsys@invoke{
}\pgfsys@setdash{0.8pt,2.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{75.2583pt}{30.65932pt}\pgfsys@lineto{63.6431pt}{36.46533pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.89449}{0.44711}{-0.44711}{-0.89449}{63.64311pt}{36.46533pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{72.0209pt}{33.85422pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\pgfsys@color@rgb@stroke{.75}{0}{.25}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{.75}{0}{.25}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{.75,0,.25}\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\smaller${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\end{array}$

While
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
and
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
are trivially prefix-finite,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{hb}}_{\mathsf{SC}}$
has an infinite descending chain, and indeed there is no $\mathsf{SC}$
execution of the program leading to the annotated behavior (where spawn adds a
thread to the current pool, and a thread from the pool is non-
deterministically chosen at each step).

###  5.4. Making RC11 Fair

Having established evidence for the adequacy of the declarative fairness
condition, we may apply this condition in other (and richer) declarative
models. In particular, we propose to adopt this condition into the C/C++
memory model. Next, we discuss this proposal in the context of the RC11 model
(Lahav et al., 2017), a repaired version of the C/C++11 specification (Batty
et al., 2012) that fixes certain issues involving sequentially consistent
accesses and works around the “thin-air” problem by completely forbidding
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}\mathtt{po}}\cup{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$
cycles. A full definition of RC11 is obtained by carefully combining the key
concepts of $\mathsf{SC}$, $\mathsf{RA}$, and $\mathsf{StrongCOH}$. It
requires us to include in the declarative framework access modes (a.k.a.
“memory orderings”—the consistency level required from every memory access),
and several types of fences. For simplicity, we elide these definitions and
keep the discussion more abstract. Indeed, there is nothing special about RC11
in this context—the declarative fairness condition could be added to any model
requiring
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}\mathtt{po}}\cup{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$
acyclicity.

Generally speaking, when proposing a strengthening of a programming language
memory model, one has to make sure that the mapping schemes to multicore
architectures are not broken, and that source-to-source compiler
transformations are still validated. In our case, the mapping of RC11 to
x86-TSO trivially remains sound. Indeed, as we saw in Theorem 5.5, the natural
operational characterization of liveness in TSO corresponds to the declarative
condition requiring that the
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
and
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
relations are prefix-finite. Since the same condition is applied both in the
source level (RC11) and in the target level (x86-TSO), and mappings of source
graphs to target ones keep
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
and
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
intact, we maintain the soundness of the known mappings.666See
http://www.cl.cam.ac.uk/~pes20/cpp/cpp0xmappings.html [accessed July-2021]. We
note that for establishing the soundness of the mappings to other
architectures, one first needs a formal fairness condition of the
architecture. While this may be more difficult in architectures weaker than
x86-TSO (see Section 7), it is likely that no hardware will allow that a write
is placed after infinitely many other writes in the coherence order (non-
prefix-finite
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$),
or that infinitely many reads do not observe a later write (non-prefix-finite
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$).

Considering compiler transformations, one has to show that every behavior of
the target program explained by a consistent graph $G_{\text{tgt}}$ is also
obtained by a consistent graph $G_{\text{src}}$ of the source program. It is
not hard to see that the constructions of Vafeiadis et al. (2015) and Lahav et
al. (2017) work as-is for the RC11 model strengthened with fairness. First,
the constructions of $G_{\text{src}}$ for _reordering transformations_ , which
reorder two memory accesses under certain conditions, keep the same
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
and
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
relations of $G_{\text{tgt}}$; so their prefix-finiteness trivially follows.

Second, we consider _elimination transformations_ that eliminate a redundant
memory access. In this case, $G_{\text{src}}$ is obtained from
$G_{\text{tgt}}$ by adding one additional event $e_{\text{new}}$ that
corresponds to the eliminated instruction. For read elimination (read-after-
read or read-after-write), $e_{\text{new}}$ is a read event, and the
construction of ensures that
$G_{\text{src}}.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}=G_{\text{tgt}}.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$.
In turn,
$G_{\text{tgt}}.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}\subseteq
G_{\text{src}}.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$,
but since only one event is added to $G_{\text{src}}$, prefix-finiteness of
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
is again trivially preserved.

Finally, we consider write-after-write elimination. Let $w_{0}$ denote the
immediate
$G_{\text{src}}.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>of $e_{\text{new}}$. Then, to construct
$G_{\text{src}}.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$,
one places $e_{\text{new}}$ as the immediate predecessor of $w_{0}$. Then,
consistency of $G_{\text{src}}$ follows the argument of (Lahav et al., 2017),
and it remains to show that fairness of $G_{\text{src}}$ follows from the
fairness of $G_{\text{tgt}}$. The latter is easy: write events in
$G_{\text{src}}$ other than $e_{\text{new}}$ all have at most one more
incoming
$G_{\text{src}}.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}$
edge (from $e_{\text{new}}$), and the same set of incoming
$G_{\text{src}}.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
edges. In turn, For $e_{\text{new}}$ itself, we have: $\\{{e\in
G_{\text{src}}.{\mathtt{E}}\;|\;{\langle{e,e_{\text{new}}}\rangle}\in
G_{\text{src}}.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}\cup
G_{\text{src}}.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}}\\}\subseteq\\{{e\in
G_{\text{tgt}}.{\mathtt{E}}\;|\;{\langle{e,w_{0}}\rangle}\in
G_{\text{tgt}}.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}\cup
G_{\text{tgt}}.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}}\\}.$

In the next section, we demonstrate that adding fairness to RC11 as proposed
above provides the necessary underpinnings allowing one to formally reason
about termination under RC11.

###  5.5. From Finite to Infinite Robustness

Common advice given to programmers of multi-threaded software is to follow a
programming discipline that hides the effects of that weak memory model,
_e.g.,_ to use exclusively sequentially consistent accesses. Programs that
follow such a discipline are _robust_ , meaning that they have only
sequentially consistent behaviors on the underlying weak memory model. While
there is a rich literature on programming disciplines that imply robustness
and verification techniques for robustness (Bouajjani et al., 2013, 2011;
Derevenetc and Meyer, 2014; Bouajjani et al., 2018; Margalit and Lahav, 2021;
Lahav and Margalit, 2019; Oberhauser, 2018), most work only considers _finite_
behaviors, i.e., they leave open whether programs following the discipline
have only sequentially consistent _infinite_ behaviors. This means that any
correctness properties that only concern infinite behaviors, such as
starvation-freedom, might be lost on the weak memory model despite its
(finite) robustness. In this section, we show that this cannot happen as long
as the weak memory model satisfies our declarative memory fairness condition
and its consistency predicate is
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}\mathtt{po}}\cup{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$-prefix
closed. This is the case for all models studied in this paper. Thus our
unified definition of memory fairness lifts all existing robustness results
for these models from the literature to infinite behaviors.

First, we observe that the consistency predicates based on acyclicity
($\mathsf{SC}$-consisterncy, in particular) enjoy a “compactness property”—if
they hold for all finite prefixes of a graph, then they also hold for the full
graph. Below, by _finite_ execution graph, we mean a graph $G$ with
$G.{\mathtt{E}}\setminus\mathsf{Init}$ being finite (the set $\mathsf{Init}$
of initialization events may be infinite if $\mathsf{Loc}$ is infinite).

###### Definition 5.12.

An execution graph $G^{\prime}$ is a
_${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}\mathtt{po}}\cup{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$
-prefix_ of an execution graph $G$ if we have
$\textit{dom}{({(G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}})\mathbin{;}[G^{\prime}.{\mathtt{E}}]})}\subseteq
G^{\prime}.{\mathtt{E}}$,
$G^{\prime}.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}=[G^{\prime}.{\mathtt{E}}]\mathbin{;}G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}\mathbin{;}[G^{\prime}.{\mathtt{E}}]$,
and
$G^{\prime}.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}=[G^{\prime}.{\mathtt{E}}]\mathbin{;}G.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}\mathbin{;}[G^{\prime}.{\mathtt{E}}]$.

###### Proposition 5.13 ($\mathcal{G}_{\mathsf{SC}}$ compactness).

Let $G$ be an execution graph with prefix-finite
$([G.{\mathtt{E}}\setminus\mathsf{Init}]\mathbin{;}G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}})^{+}$.
If every finite
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}\mathtt{po}}\cup{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$-prefix
of $G$ is $\mathcal{G}_{\mathsf{SC}}$-consistent, then so is $G$.

###### Proof.

Suppose that $G$ is $\mathcal{G}_{\mathsf{SC}}$-inconsistent, and let
$a_{1}{,}\ldots{,}a_{n}\in G.{\mathtt{E}}$ such that
${\langle{a_{i},a_{i+1}}\rangle}\in
G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}\cup
G.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}\cup
G.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
for every $1\leq i\leq n-1$, and ${\langle{a_{n},a_{1}}\rangle}\in
G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}\cup
G.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}\cup
G.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$.
Let
$E^{\prime}=\mathsf{Init}\cup\textit{dom}{({(G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}})^{*}\mathbin{;}[\\{{a_{1}{,}\ldots{,}a_{n}}\\}]})}$,
and let
$G^{\prime}={\langle{E^{\prime},[E^{\prime}]\mathbin{;}G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}\mathbin{;}[E^{\prime}],[E^{\prime}]\mathbin{;}G.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}\mathbin{;}[E^{\prime}]}\rangle}$.
Since
$([G.{\mathtt{E}}\setminus\mathsf{Init}]\mathbin{;}G.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>G.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}})^{+}$
is prefix-finite, $G^{\prime}$ is a finite
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}\mathtt{po}}\cup{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}$-prefix
of $G$. However, we have ${\langle{a_{i},a_{i+1}}\rangle}\in
G^{\prime}.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>G^{\prime}.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}\cup
G^{\prime}.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}\cup
G^{\prime}.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$
for every $1\leq i\leq n-1$, and ${\langle{a_{n},a_{1}}\rangle}\in
G^{\prime}.{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>G^{\prime}.{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\mathtt{rf}}\cup
G^{\prime}.{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathtt{mo}}\cup
G^{\prime}.{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathtt{fr}}$,
so $G^{\prime}$ is $\mathcal{G}_{\mathsf{SC}}$-inconsistent. ∎

###### Definition 5.14 (Robustness).

Let ${P}$ be a program and $\mathcal{G}$ be a declarative memory system.

  * •

${P}$ is _finitely execution-graph robust_ against $\mathcal{G}$ if for every
finite behavior $\beta\in\mathsf{B}({{P}})$ and $G\in\mathcal{G}$ with
$\mathsf{Event}(\beta)=G.{\mathtt{E}}$, we have
$G\in\mathcal{G}_{\mathsf{SC}}$.

  * •

${P}$ is _strongly execution-graph robust_ against $\mathcal{G}$ if for every
(finite or infinite) behavior $\beta\in\mathsf{B}({{P}})$ and