ordered. This can be done trivially by introducing auxiliary events with an
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$
relation between them, while
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$
remains of size $O(n)$. In particular, every
$(e_{1},e_{2})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
edge can be simulated using fresh events $\mathtt{r},\mathtt{w}$ such that (i)
$(\mathtt{w},\mathtt{r})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$
(ii)
$(e_{1},\mathtt{w})\in\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color<EMAIL_ADDRESS>and (iii)
$(\mathtt{r},e_{2})\in\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color<EMAIL_ADDRESS>For simplicity of presentation, we do not mention these events explicitly, but
rather directly the
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
relation they result in. For every edge $(\alpha,\beta)\in E_{G}$ with
$\alpha<\beta$, we have the following relations:

$(\mathtt{w}_{\beta},\mathtt{r}^{\alpha}_{\beta})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}\qquad\qquad\quad\quad(\mathtt{w}_{\alpha},\mathtt{w}^{\beta}_{\alpha})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\qquad\qquad\quad\quad(\mathtt{w}^{\beta}_{\alpha},\sf\mathtt{w}Jxn_{\beta})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
$(\sf\mathtt{w}Jxn_{\beta},e_{(\alpha,\beta)})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\qquad\qquad(e_{(\alpha,\beta)},\sf\mathtt{r}Jxn_{\alpha})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\qquad\qquad(\sf\mathtt{r}Jxn_{\alpha},\mathtt{r}^{\alpha}_{\beta})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$

$1$$2$$3$$e_{(1,3)}$$\sf\mathtt{r}Jxn_{1}$$\sf\mathtt{w}Jxn_{3}$$\mathtt{w}_{2}$$\mathtt{r}^{1}_{2}$$\mathtt{w}^{3}_{2}$$\mathtt{w}^{3}_{1}$$e_{(2,3)}$$\mathtt{r}^{1}_{3}$$e_{(1,2)}$$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$

Figure 10.  _Left:_ A graph $G$ with three nodes $V_{G}=\\{1,2,3\\}$
containing a triangle. _Right:_ A slice of the partial execution
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$
for $G$. We have
$(\mathtt{w}_{2},\mathtt{w}^{3}_{2})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
and
$(\mathtt{w}^{3}_{2},\mathtt{r}^{1}_{2})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$,
thus violating weak read coherence in
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$.

Fig. 10 illustrates the above construction for a slice of the constructed
partial execution
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$.
We conclude with a proof sketch of Theorem 1.7, and refer to Section A.7
(arxiv) for the full proof.

Correctness and time complexity. If there is a triangle
$(\alpha,\beta,\gamma)$ in $G$ with $\alpha<\beta,\gamma$, then
$(\mathtt{w}^{\gamma}_{\beta},\mathtt{r}^{\alpha}_{\beta})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
because of the sequence of
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
edges: $(\mathtt{w}^{\gamma}_{\beta},\sf\mathtt{w}Jxn_{\gamma})$,
$(\sf\mathtt{w}Jxn_{\gamma},e_{(\alpha,\gamma)})$,
$(e_{(\alpha,\gamma)},\sf\mathtt{r}Jxn_{\alpha})$,
$(\sf\mathtt{r}Jxn_{\alpha},\mathtt{r}^{\alpha}_{\beta})$. Together with
$(\mathtt{w}_{\beta},\mathtt{r}^{\alpha}_{\beta})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$
and
$(\mathtt{w}_{\beta},\mathtt{w}^{\gamma}_{\beta})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
by construction, we obtain a weak-read-coherence violation. In the other
direction, if there are no triangles in $G$, then the modification order
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}=\bigcup_{\alpha\in
V_{G}}\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{y_{\alpha}}$
where
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{y_{\alpha}}$
orders $\mathtt{w}_{\alpha}$ before every other write
$\mathtt{w}^{\beta}_{\alpha}$ on $y_{\alpha}$, makes
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}=\langle\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}.\mathsf{E},\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}.\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po},\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}.\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf},\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}\rangle$
$\mathsf{SRA}$\- (and thus also $\mathsf{RA}$\- and $\mathsf{WRA}$-)
consistent. Such an
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
ensures that
$(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo})$
is acyclic. Triangle-freeness ensures read-coherence — a violation of read
coherence implies that there are three events
$e_{1}=\mathtt{w}_{\beta},e_{2}=\mathtt{w}^{\gamma}_{\beta},e_{3}=\mathtt{r}^{\alpha}_{\beta}$
such that
$(e_{1},e_{3})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$,
$(e_{1},e_{2})\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
and
$(e_{2},e_{3})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$,
implying a triangle $(\alpha,\beta,\gamma)$ in $G$. The total time to
construct
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$
is $O(|V_{G}|+|E_{G}|)$. Further, our reduction is completely combinatorial.
We thus arrive at the following theorem.

See 1.7

##  5\. Experimental Evaluation

We implemented our consistency-checking algorithms for
$\mathsf{RA}$/$\mathsf{RC20}$ and evaluated their performance on two standard
settings of program analysis, namely, (i)  _stateless model checking_ , using
TruSt (Kokologiannakis et al., 2022), and (ii)  _online testing_ , using
C11Tester (Luo and Demsky, 2021). These tools are designed to handle variants
of C11 including SC accesses, and performing race-detection, which are beyond
the scope of this work. Here, we focus on the consistency-checking component
for the $\mathsf{RA}$/$\mathsf{RC20}$ fragment, which is common in these tools
and our work. We conducted our experiments on a machine running Ubuntu 22.04
with 2.4GHz CPU and 64GB of memory.

Benchmarks. We used standard benchmark programs from prior state-of-the-art
verification and testing papers (Norris and Demsky, 2013; Abdulla et al.,
2018; Luo and Demsky, 2021; Kokologiannakis and Vafeiadis, 2021), as well as
the applications Silo, GDAX, Mabain, and Iris (Luo and Demsky, 2021) for
online testing. These benchmarks use C11 concurrency primitives extensively.
For thorough evaluation, we have scaled up some of them, when their baseline
versions were too small, by increasing the number of threads or loop counters.
Some benchmarks also contain accesses outside our scope; we converted those
accesses to access modes applicable for our experiments, in line with the
evaluation in prior works (Abdulla et al., 2018; Lahav and Margalit, 2019).

###  5.1. Stateless Model Checking

The TruSt model checker explores all behaviors of a bounded program by
enumerating executions, making use of different strategies to avoid redundant
exploration. One such strategy is to enumerate partial executions
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$
and perform a consistency check for the maximal ones, to verify that they
represent valid program behavior. As the number of explored executions is
typically large, it is imperative that consistency checks are performed as
fast as possible.

Consistency checking inside TruSt. The algorithm for consistency checking in
TruSt constructs a writes-before order
$\mathsf{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{.5}\pgfsys@color<EMAIL_ADDRESS>(Lahav and Vafeiadis, 2015), which is a partial modification order that serves
as a witness of consistency. The time taken to construct
$\mathsf{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{.5}\pgfsys@color<EMAIL_ADDRESS>is $O(n^{3})$, which has been identified as a bottleneck in the model checking
task (Kokologiannakis et al., 2019, 2022). We replaced TruSt’s
$\mathsf{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{.5}\pgfsys@color<EMAIL_ADDRESS>algorithm for consistency checking with the
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
computation of Algorithm 3, and measured (i) the speedup realized for
consistency checking, and (ii) the effect of this speedup on the overall
model-checking task. We executed TruSt on several benchmarks, each with a time
budget of $2$ hours, measuring the average time for consistency checking (for
evaluating (i)) as well as the total number of executions explored (for
evaluating (ii)). Finally, we note that TruSt employs a number of simpler
consistency checks during the exploration. Although we expect that our new
algorithm can improve those as well, we have left them intact as it was
unclear to us how they interact with the rest of the tool, and in order to
maintain soundness of the obtained results.

Experimental results. Our results are shown in Table 1. We mark with $\dagger$
benchmarks on which the model checker found an error and halted early. We
observe that Algorithm 3 is always faster, typically by a significant margin.
The maximum speedup for consistency checking is $162\times$, and the geometric
mean of speedups is $36\times$. Regarding the number of executions, the model
checker explores $4.3\times$ more on (geometric) average, and as high as
$71.6\times$ more, when using Algorithm 3. In some benchmarks, the two
approaches observe a similar number of executions. This is due to consistency
checking being only part of the overall model-checking procedure, which also
consists of other computationally intensive tasks such as backtracking. As
consistency checking appears now to not be a bottleneck, it is meaningful to
focus further optimization efforts on these other tasks. For ttaslock, we
noticed a livelock that blocks the model checker. Overall, our experiments
highlight that the benefit of the new, nearly linear time property of
consistency checking leads to a measurable speedup that positively impacts the
overall efficiency of model checking. We refer to Section B.1 (arxiv) for
experiments on $\mathsf{RC20}$, which lead to the same qualitative
conclusions.

Table 1.  Impact on model checking. Columns $2$ and $3$ denote the average
time (in seconds) spent in consistency checking by resp. TruSt and our
algorithm. Columns $5$ and $6$ denote the total number of executions explored
by resp. TruSt and our algorithm. Columns $4$ and $7$ denote the respective
speedups and ratios.

1 | 2 | 3 | 4 | 5 | 6 | 7 | 1 | 2 | 3 | 4 | 5 | 6 | 7
---|---|---|---|---|---|---|---|---|---|---|---|---|---
Benchmark |  Avg. Time |  Executions | Benchmark |  Avg. Time |  Executions
TruSt | Our Alg. | S | TruSt | Our Alg. | R | TruSt | Our Alg. | S | TruSt | Our Alg. | R
barrier | 0.5 | 0.01 | 45.0 | 14K | 81K | 5.98 |  ms-queue$\dagger$ | 0.07 | 0.01 | 7.0 | 208 | 208 | 1
buf-ring | 1.6 | 0.02 | 79.5 | 3K | 6K | 2.52 | mutex | 0.8 | 0.01 | 78.0 | 7K | 218K | 29.67
chase-lev$\dagger$ | 0.0 | 0.0 | - | 2 | 2 | 1 | peterson | 0.3 | 0.01 | 26.0 | 4K | 5K | 1.16
control-flow | 0.08 | 0.01 | 8.0 | 88K | 1M | 16.56 | qu | 0.1 | 0.01 | 12.0 | 2K | 2K | 1.04
dekker | 0.2 | 0.01 | 24.0 | 26K | 64K | 2.45 | seqlock | 0.2 | 0.01 | 24.0 | 24K | 171K | 7.02
dq | 0.1 | 0.01 | 13.0 | 40K | 163K | 4.11 | sigma | 0.2 | 0.01 | 22.0 | 4K | 62K | 5.97
exp-bug | 0.1 | 0.01 | 13.0 | 55K | 2M | 29.98 | spinlock | 1.0 | 0.01 | 98.0 | 5K | 31K | 6.04
fib-bench | 1.6 | 0.01 | 162.0 | 4K | 315K | 71.63 | szymanski | 0.4 | 0.01 | 44.0 | 2K | 2K | 1.16
gcd | 0.3 | 0.01 | 31.0 | 18K | 80K | 4.46 | ticketlock | 0.9 | 0.02 | 45.5 | 7K | 89K | 12.47
lamport | 0.4 | 0.01 | 36.0 | 17K | 93K | 5.54 | treiber | 0.6 | 0.01 | 58.0 | 403 | 403 | 1
linuxrwlocks | 0.4 | 0.01 | 40.0 | 12K | 32K | 2.75 | ttaslock | 1.0 | 0.01 | 97.0 | 401 | 401 | 1
mcs-spinlock | 1.1 | 0.01 | 108.0 | 5K | 38K | 7.19 | twalock | 0.5 | 0.01 | 52.0 | 8K | 30K | 3.58
mpmc | 0.7 | 0.01 | 66.0 | 10K | 77K | 8.01 |  |  |  |  |  |  |
Totals | - | - | - | - | - | - | - | 14.5 | 0.26 | - | 356K | 4.6M | -

###  5.2. Online Testing

We now turn our attention to the online testing setting using C11Tester’s
framework. In C11Tester’s setting, a partial execution
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$
is constructed incrementally, by iteratively (i) revealing a randomly chosen
new read/RMW event $\mathtt{r}$, (ii) choosing a valid writer
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}(\mathtt{r})$,
and (iii) continuing the execution of the program until the next read/RMW
events. Hence, every iteration requires a consistency check. Although we could
use Algorithm 3 from scratch at each step, this would result in unnecessary
recomputations of
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$.
Instead, we follow a different approach here — we maintain
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
on-the-fly, in a way that incremental consistency checks can be done more
efficiently.

Incremental consistency checking. Our incremental algorithm constructs a
similar minimally coherent partial modification order
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
as our offline algorithm (Algorithm 3). However, unlike the offline setting,
we need efficient incremental consistency checks. For this, we maintain a per-
location order
$\mathsf{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}hbmo}_{x}$
on write/RMW events that satisfies following invariants: (i)
$\mathsf{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}hbmo}_{x}\subseteq(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x})^{+}$
and (ii)
$(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup(\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x};\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}_{x}^{?}))\subseteq\mathsf{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}hbmo}_{x}$.
In order to decide whether a new read/RMW event $\mathtt{r}(x)$ can observe a
write/RMW event $\mathtt{w}(x)$, we must determine if there exists another
write/RMW event $\mathtt{w}^{\prime}(x)$ such that
$(\mathtt{w}^{\prime},\mathtt{r})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}$
and
$(\mathtt{w}^{\prime},\mathtt{w})\in(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x})^{+}$,
as this would lead to a consistency violation. Using
$\mathsf{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}hbmo}_{x}$,
this check is performed as follows: (a) for each thread $u$, we identify the
$\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color<EMAIL_ADDRESS>write/RMW event $\mathtt{w}^{\prime}(u,x)$ for which
$(\mathtt{w}^{\prime},\mathtt{r})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$,
and (b) we update
$\mathsf{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}hbmo}_{x}\leftarrow\mathsf{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}hbmo}_{x}\cup\\{(\mathtt{w}^{\prime\prime},\mathtt{w}^{\prime})\,|\,(\mathtt{w}^{\prime\prime},\mathtt{w}^{\prime})\in\mathsf{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}hbmo}_{x}^{+}\\}$.
Due to invariant (ii), at this point we are guaranteed that, for all write
events $\mathtt{w}^{\prime\prime}$, we have
$(\mathtt{w}^{\prime\prime},\mathtt{w}^{\prime})\in\mathsf{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}hbmo}_{x}$
iff
$(\mathtt{w}^{\prime\prime},\mathtt{w}^{\prime})\in(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x})^{+}$.
We can now test whether $\mathtt{w}$ is a valid writer for $\mathtt{r}$ by
checking whether
$(\mathtt{w},\mathtt{w}^{\prime})\in\mathsf{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}hbmo}_{x}$,
for one of the aforementioned write/RMW events $\mathtt{w}^{\prime}$. We refer
to Section B.2 (arxiv) for implementation details.

Main differences with C11Tester. The consistency-checking algorithm
implemented inside C11Tester also infers
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
orderings as implied by read and write coherence. The two key differences
between that approach and our incremental algorithm described above are the
following: (i) C11Tester’s
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
is stronger than our minimally coherent
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
that is contained in
$\mathsf{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}hbmo}$,
and (ii) this
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
is always maintained transitively-closed. These two differences are expected
to make
$\mathsf{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}hbmo}$
computationally cheaper to maintain than C11Tester’s
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$.
Although we also have to compute transitive paths
$\mathsf{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}hbmo}^{+}$
when encountering read/RMW operations (step (b) above), in our experience,
these paths typically touch a small part of the input, leading to an efficient
computation.

Table 2.  Impact on online testing. Columns $2$, $3$ and $4$ give the average
number of events, threads and locations in each benchmark. Columns $5$ and $6$
denote the average times in seconds to check for consistency by resp.
C11Tester and our algorithm. Column 6 denotes the speedup.

1 | 2 | 3 | 4 | 5 | 6 | 7 | 1 | 2 | 3 | 4 | 5 | 6 | 7
---|---|---|---|---|---|---|---|---|---|---|---|---|---
Benchmark | $\mathbf{n}$ | $\mathbf{k}$ | $\mathbf{d}$ | C11Test. | Our Alg. | SpeedUp | Benchmark | $\mathbf{n}$ | $\mathbf{k}$ | $\mathbf{d}$ | C11Test. | Our Alg. | SpeedUp
control-flow | 52K | 25 | 3 | 4.2 | 0.04 | 104.25 | mutex | 15M | 11 | 11 | 20.9 | 16.8 | 1.24
sigma | 36K | 10 | 9 | 2.4 | 0.03 | 80 | gdax | 11M | 5 | 46K | 7.0 | 5.7 | 1.23
dq | 599K | 4 | 2 | 22.1 | 0.5 | 46.78 | spinlock | 5M | 11 | 10 | 7.0 | 5.9 | 1.18
iris-1 | 1M | 12 | 45 | 28.4 | 1.8 | 16.25 | ticketlock | 14M | 6 | 20 | 15.7 | 13.2 | 1.18
seqlock | 478K | 17 | 20 | 14.4 | 1.4 | 10.38 | ttaslock | 5M | 11 | 10 | 7.8 | 6.6 | 1.18
exp-bug | 2M | 4 | 2 | 1.6 | 0.7 | 2.35 | fib-bench | 6M | 3 | 2 | 3.3 | 2.8 | 1.18
chase-lev | 7M | 5 | 2 | 12.4 | 5.4 | 2.3 | qu | 1M | 10 | 29 | 1.6 | 1.3 | 1.18
linuxrwlocks | 7M | 6 | 10 | 10.9 | 5.9 | 1.84 | treiber | 1M | 6 | 11 | 1.1 | 1.0 | 1.12
mabain | 5M | 6 | 18 | 7.3 | 4.0 | 1.82 | silo | 8M | 4 | 4K | 5.3 | 4.8 | 1.1
iris-2 | 12M | 3 | 12 | 9.9 | 5.7 | 1.72 | barrier | 8M | 5 | 20 | 7.8 | 7.4 | 1.04
mcs-lock | 10M | 11 | 30 | 17.8 | 12.2 | 1.45 | mpmc | 9M | 10 | 3 | 12.9 | 12.5 | 1.03
lamport | 6M | 3 | 5 | 3.4 | 2.5 | 1.36 | indexer | 2M | 17 | 128 | 1.6 | 1.5 | 1.03
peterson | 5M | 3 | 4 | 2.9 | 2.2 | 1.29 | buf-ring | 5M | 9 | 12 | 7.0 | 6.8 | 1.02
spsc | 10M | 3 | 699 | 6.4 | 5.0 | 1.28 | ms-queue | 4M | 11 | 13 | 8.2 | 8.2 | 0.99
dekker | 16M | 3 | 3 | 9.2 | 7.2 | 1.27 | gcd | 5M | 3 | 2 | 2.2 | 2.5 | 0.89
twalock | 4M | 11 | 4K | 8.9 | 7.0 | 1.26 | szymanski | 4M | 3 | 3 | 1.8 | 2.3 | 0.81
Totals | - | - | - | - | - | - | - | 196M | - | - | 286.4 | 170.8 | -

Experimental results. Our results are shown in Table 2. For robust
measurements, we report averages over $10$ executions per benchmark, focusing
on benchmarks for which at least one algorithm took $\geq 1$s. Our approach
achieves a maximum speedup of $104.2\times$ and a geometric speed-up of
$2\times$. In more detail, we observe significant improvement in the first $5$
benchmarks, and consistent speedups of at least $1.2\times$ on $18$
benchmarks. We have encountered only 2 benchmarks, gcd and szymanski, on which
the new algorithm is arguably slower. These benchmarks contain no RMWs and
only a small number of write events. This results in the computation of very
small modification orders, diminishing the benefit of our algorithm and
results in a marginal slowdown.

##  6\. Conclusion

Checking the reads-from consistency of concurrent executions is a fundamental
computational task in the development of formal concurrency semantics, program
verification and testing. In this paper we have addressed this problem in the
context of C11-style weak memory models, for which this problem is both highly
meaningful, and intricate. We have developed a collection of algorithms and
complexity results that are either optimal or nearly-optimal, and thus
accurately characterize the complexity of the problem in this setting.
Further, our experimental evaluation indicates that the new algorithms have a
measurable, and often significant, impact on the consistency-checking tasks
that arise in practice. Thus our algorithms enable the development of more
performant and scalable program analysis tools in this domain. This work is
focused on non-SC fragments of C11, as otherwise, consistency checking
inherits the $\mathcal{NP}$-hardness of $\mathsf{SC}$ consistency checking.
For applications having an abundance of SC accesses, however, a meaningful
direction for future work is to combine our techniques with heuristics
developed for checking $\mathsf{SC}$ consistency (e.g., (Abdulla et al., 2018;
Pavlogiannis, 2019)), and apply them on programs that mix all types of C11
accesses.

###### Acknowledgements.

Andreas Pavlogiannis was partially supported by a research grant (VIL42117)
from VILLUM FONDEN. Umang Mathur was partially supported by the Simons
Institute for the Theory of Computing, and by a Singapore Ministry of
Education (MoE) Academic Research Fund (AcRF) Tier 1 grant. Shankaranarayanan
Krishna was partially supported by the SERB MATRICS grant MTR/2019/000095.
Parosh Aziz Abdulla was partially supported by the Swedish Research Council.

## Data and Software Availability Statement

The artifact developed for this work is available (Tunç et al., 2023), which
contains all source codes and experimental data necessary to reproduce our
evaluation in Section 5.

## References

  * (1)
  * Abdulla et al. (2019) Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Magnus Lång, Tuan Phong Ngo, and Konstantinos Sagonas. 2019.  Optimal stateless model checking for reads-from equivalence under sequential consistency.  _Proc. ACM Program. Lang._ 3, OOPSLA (2019), 150:1–150:29.  https://doi.org/10.1145/3360576
  * Abdulla et al. (2018) Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan Phong Ngo. 2018.  Optimal Stateless Model Checking under the Release-Acquire Semantics.  _Proc. ACM Program. Lang._ 2, OOPSLA, Article 135 (2018), 29 pages.  https://doi.org/10.1145/3276505
  * Agarwal et al. (2021) Pratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, and Viktor Toman. 2021.  Stateless Model Checking Under a Reads-Value-From Equivalence. In _Computer Aided Verification_ , Alexandra Silva and K. Rustan M. Leino (Eds.). Springer International Publishing, Cham, 341–366.  https://doi.org/10.1007/978-3-030-81685-8_16
  * Alglave (2010) Jade Alglave. 2010\.  _A Shared Memory Poetics_.  Ph. D. Dissertation. l’Université Paris 7 - Denis Diderot.
  * Alglave et al. (2011) Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2011.  Litmus: Running Tests against Hardware. In _Tools and Algorithms for the Construction and Analysis of Systems_ , Parosh Aziz Abdulla and K. Rustan M. Leino (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 41–44.  https://doi.org/10.1007/978-3-642-19835-9_5
  * Alglave et al. (2014) Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014\.  Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory.  _ACM Trans. Program. Lang. Syst._ 36, 2, Article 7 (2014), 74 pages.  https://doi.org/10.1145/2627752
  * Batty et al. (2016) Mark Batty, Alastair F. Donaldson, and John Wickerson. 2016\.  Overhauling SC Atomics in C11 and OpenCL. In _Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (St. Petersburg, FL, USA) _(POPL ’16)_. Association for Computing Machinery, New York, NY, USA, 634–648.  https://doi.org/10.1145/2837614.2837637
  * Batty et al. (2011) Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011.  Mathematizing C++ Concurrency. In _Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Austin, Texas, USA) _(POPL ’11)_. Association for Computing Machinery, New York, NY, USA, 55–66.  https://doi.org/10.1145/1926385.1926394
  * Bender and Palsberg (2019) John Bender and Jens Palsberg. 2019.  A Formalization of Java’s Concurrent Access Modes.  _Proc. ACM Program. Lang._ 3, OOPSLA, Article 142 (2019), 28 pages.  https://doi.org/10.1145/3360568
  * Boehm and Adve (2008) Hans-J. Boehm and Sarita V. Adve. 2008.  Foundations of the C++ Concurrency Memory Model. In _Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Tucson, AZ, USA) _(PLDI ’08)_. Association for Computing Machinery, New York, NY, USA, 68–78.  https://doi.org/10.1145/1375581.1375591
  * Bornholt et al. (2021) James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, and Andrew Warfield. 2021\.  Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3. In _Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles_ (Virtual Event, Germany) _(SOSP ’21)_. Association for Computing Machinery, New York, NY, USA, 836–850.  https://doi.org/10.1145/3477132.3483540
  * Bouajjani et al. (2017) Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, and Jad Hamza. 2017.  On Verifying Causal Consistency. In _Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages_ (Paris, France) _(POPL ’17)_. Association for Computing Machinery, New York, NY, USA, 626–638.  https://doi.org/10.1145/3009837.3009888
  * Bui et al. (2021) Truc Lam Bui, Krishnendu Chatterjee, Tushar Gautam, Andreas Pavlogiannis, and Viktor Toman. 2021\.  The Reads-from Equivalence for the TSO and PSO Memory Models.  _Proc. ACM Program. Lang._ 5, OOPSLA, Article 164 (2021), 30 pages.  https://doi.org/10.1145/3485541
  * Burckhardt (2014) Sebastian Burckhardt. 2014\.  Principles of Eventual Consistency.  _Foundations and Trends® in Programming Languages_ 1, 1-2 (2014), 1–150.  https://doi.org/10.1561/2500000011
  * Chakraborty and Vafeiadis (2019) Soham Chakraborty and Viktor Vafeiadis. 2019.  Grounding Thin-Air Reads with Event Structures.  _Proc. ACM Program. Lang._ 3, POPL, Article 70 (2019), 28 pages.  https://doi.org/10.1145/3290383
  * Chalupa et al. (2017) Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. 2017\.  Data-Centric Dynamic Partial Order Reduction.  _Proc. ACM Program. Lang._ 2, POPL, Article 31 (2017), 30 pages.  https://doi.org/10.1145/3158119
  * Chatterjee et al. (2019) Krishnendu Chatterjee, Andreas Pavlogiannis, and Viktor Toman. 2019.  Value-Centric Dynamic Partial Order Reduction.  _Proc. ACM Program. Lang._ 3, OOPSLA, Article 124 (2019), 29 pages.  https://doi.org/10.1145/3360550
  * Chen et al. (2004) Jianer Chen, Xiuzhen Huang, Iyad A. Kanj, and Ge Xia. 2004\.  Linear FPT Reductions and Computational Lower Bounds. In _Proceedings of the Thirty-Sixth Annual ACM Symposium on Theory of Computing_ (Chicago, IL, USA) _(STOC ’04)_. Association for Computing Machinery, New York, NY, USA, 212–221.  https://doi.org/10.1145/1007352.1007391
  * Chen et al. (2009) Yunji Chen, Yi Lv, Weiwu Hu, Tianshi Chen, Haihua Shen, Pengyu Wang, and Hong Pan. 2009.  Fast complete memory consistency verification. In _2009 IEEE 15th International Symposium on High Performance Computer Architecture_. 381–392.  https://doi.org/10.1109/HPCA.2009.4798276
  * Chini and Saivasan (2020) Peter Chini and Prakash Saivasan. 2020.  A Framework for Consistency Algorithms. In _40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 182)_ , Nitin Saxena and Sunil Simon (Eds.). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 42:1–42:17.  https://doi.org/10.4230/LIPIcs.FSTTCS.2020.42
  * Dang et al. (2019) Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Derek Dreyer. 2019.  RustBelt Meets Relaxed Memory.  _Proc. ACM Program. Lang._ 4, POPL, Article 34 (2019), 29 pages.  https://doi.org/10.1145/3371102
  * Desnoyers et al. (2011) Mathieu Desnoyers, Paul E McKenney, Alan S Stern, Michel R Dagenais, and Jonathan Walpole. 2011\.  User-level implementations of read-copy update.  _IEEE Transactions on Parallel and Distributed Systems_ 23, 2 (2011), 375–382.  https://doi.org/10.1109/TPDS.2011.159
  * Furbach et al. (2015) Florian Furbach, Roland Meyer, Klaus Schneider, and Maximilian Senftleben. 2015.  Memory-Model-Aware Testing: A Unified Complexity Analysis.  _ACM Trans. Embed. Comput. Syst._ 14, 4 (2015).  https://doi.org/10.1145/2753761
  * Gibbons and Korach (1997) Phillip B. Gibbons and Ephraim Korach. 1997.  Testing Shared Memories.  _SIAM J. Comput._ 26, 4 (1997), 1208–1244.  https://doi.org/10.1137/S0097539794279614
  * Huang et al. (2014) Jeff Huang, Patrick O’Neil Meredith, and Grigore Rosu. 2014\.  Maximal Sound Predictive Race Detection with Control Flow Abstraction. In _Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Edinburgh, United Kingdom) _(PLDI ’14)_. ACM, New York, NY, USA, 337–348.  https://doi.org/10.1145/2594291.2594315
  * ISO/IEC 14882 (2011) ISO/IEC 14882. 2011\.  Programming Language C++.
  * ISO/IEC 9899 (2011) ISO/IEC 9899. 2011\.  Programming Language C.
  * Kalhauge and Palsberg (2018) Christian Gram Kalhauge and Jens Palsberg. 2018.  Sound Deadlock Prediction.  _Proc. ACM Program. Lang._ 2, OOPSLA, Article 146 (2018), 29 pages.  https://doi.org/10.1145/3276516
  * Kini et al. (2017) Dileep Kini, Umang Mathur, and Mahesh Viswanathan. 2017\.  Dynamic Race Prediction in Linear Time. In _Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Barcelona, Spain) _(PLDI 2017)_. ACM, New York, NY, USA, 157–170.  https://doi.org/10.1145/3062341.3062374
  * Kokologiannakis et al. (2023) Michalis Kokologiannakis, Ori Lahav, and Viktor Vafeiadis. 2023\.  Kater: Automating Weak Memory Model Metatheory and Consistency Checking.  _Proc. ACM Program. Lang._ 7, POPL, Article 19 (2023), 29 pages.  https://doi.org/10.1145/3571212
  * Kokologiannakis et al. (2022) Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis. 2022.  Truly Stateless, Optimal Dynamic Partial Order Reduction.  _Proc. ACM Program. Lang._ 6, POPL (2022).  https://doi.org/10.1145/3498711
  * Kokologiannakis et al. (2019) Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis. 2019\.  Model Checking for Weakly Consistent Libraries. In _Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Phoenix, AZ, USA) _(PLDI 2019)_. Association for Computing Machinery, New York, NY, USA, 96–110.  https://doi.org/10.1145/3314221.3314609
  * Kokologiannakis and Vafeiadis (2021) Michalis Kokologiannakis and Viktor Vafeiadis. 2021.  GenMC: A Model Checker for Weak Memory Models. In _Computer Aided Verification_. Springer-Verlag, Berlin, Heidelberg, 427–440.  https://doi.org/10.1007/978-3-030-81685-8_20
  * Lahav and Boker (2022) Ori Lahav and Udi Boker. 2022.  What’s Decidable About Causally Consistent Shared Memory?  _ACM Trans. Program. Lang. Syst._ 44, 2, Article 8 (2022), 55 pages.  https://doi.org/10.1145/3505273
  * Lahav et al. (2016) Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. 2016\.  Taming Release-Acquire Consistency. In _Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (St. Petersburg, FL, USA) _(POPL ’16)_. Association for Computing Machinery, New York, NY, USA, 649–662.  https://doi.org/10.1145/2837614.2837643
  * Lahav and Margalit (2019) Ori Lahav and Roy Margalit. 2019.  Robustness against Release/Acquire Semantics. In _Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Phoenix, AZ, USA) _(PLDI 2019)_. Association for Computing Machinery, New York, NY, USA, 126–141.  https://doi.org/10.1145/3314221.3314604
  * Lahav and Vafeiadis (2015) Ori Lahav and Viktor Vafeiadis. 2015.  Owicki-Gries Reasoning for Weak Memory Models. In _Automata, Languages, and Programming_ , Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 311–323.  https://doi.org/10.1007/978-3-662-47666-6_25
  * Lahav et al. (2017) Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. 2017.  Repairing Sequential Consistency in C/C++11. In _Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Barcelona, Spain) _(PLDI 2017)_. Association for Computing Machinery, New York, NY, USA, 618–632.  https://doi.org/10.1145/3062341.3062352
  * Lee et al. (2020) Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, and Viktor Vafeiadis. 2020.  Promising 2.0: Global Optimizations in Relaxed Memory Concurrency. In _Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation_ (London, UK) _(PLDI 2020)_. Association for Computing Machinery, New York, NY, USA, 362–376.  https://doi.org/10.1145/3385412.3386010
  * Lerche (2020) Carl Lerche. 2020\.  Loom.  Available at https://github.com/tokio-rs/loom.
  * Lloyd et al. (2011) Wyatt Lloyd, Michael J. Freedman, Michael Kaminsky, and David G. Andersen. 2011.  Don’t Settle for Eventual: Scalable Causal Consistency for Wide-Area Storage with COPS. In _Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles_ (Cascais, Portugal) _(SOSP ’11)_. Association for Computing Machinery, New York, NY, USA, 401–416.  https://doi.org/10.1145/2043556.2043593
  * Luo and Demsky (2021) Weiyu Luo and Brian Demsky. 2021.  C11Tester: A Race Detector for C/C++ Atomics. In _Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems_ (Virtual, USA) _(ASPLOS ’21)_. Association for Computing Machinery, New York, NY, USA, 630–646.  https://doi.org/10.1145/3445814.3446711
  * Manovit and Hangal (2006) C. Manovit and S. Hangal. 2006.  Completely verifying memory consistency of test program executions. In _The Twelfth International Symposium on High-Performance Computer Architecture, 2006._ 166–175.  https://doi.org/10.1109/HPCA.2006.1598123
  * Margalit and Lahav (2021) Roy Margalit and Ori Lahav. 2021.  Verifying Observational Robustness against a C11-Style Memory Model.  _Proc. ACM Program. Lang._ 5, POPL, Article 4 (2021), 33 pages.  https://doi.org/10.1145/3434285
  * Mathur et al. (2018) Umang Mathur, Dileep Kini, and Mahesh Viswanathan. 2018\.  What Happens-after the First Race? Enhancing the Predictive Power of Happens-before Based Dynamic Race Detection.  _Proc. ACM Program. Lang._ 2, OOPSLA, Article 145 (2018), 29 pages.  https://doi.org/10.1145/3276515
  * Mathur et al. (2020) Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan. 2020\.  The Complexity of Dynamic Data Race Prediction. In _Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science_ (Saarbrücken, Germany) _(LICS ’20)_. Association for Computing Machinery, New York, NY, USA, 713–727.  https://doi.org/10.1145/3373718.3394783
  * Mathur et al. (2021) Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan. 2021\.  Optimal Prediction of Synchronization-Preserving Races.  _Proc. ACM Program. Lang._ 5, POPL, Article 36 (2021), 29 pages.  https://doi.org/10.1145/3434317
  * Norris and Demsky (2013) Brian Norris and Brian Demsky. 2013.  CDSchecker: Checking Concurrent Data Structures Written with C/C++ Atomics. In _Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications_ (Indianapolis, Indiana, USA) _(OOPSLA ’13)_. Association for Computing Machinery, New York, NY, USA, 131–150.  https://doi.org/10.1145/2509136.2509514
  * Oberhauser et al. (2021) Jonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu, Antonio Paolillo, Lilith Oberhauser, Koustubha Bhat, Yuzhong Wen, Haibo Chen, Jaeho Kim, and Viktor Vafeiadis. 2021\.  VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models. In _Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems_ (Virtual, USA) _(ASPLOS ’21)_. Association for Computing Machinery, New York, NY, USA, 530–545.  https://doi.org/10.1145/3445814.3446748
  * Pavlogiannis (2019) Andreas Pavlogiannis. 2019\.  Fast, Sound, and Effectively Complete Dynamic Race Prediction.  _Proc. ACM Program. Lang._ 4, POPL, Article 17 (2019), 29 pages.  https://doi.org/10.1145/3371085
  * Qadeer (2003) S. Qadeer. 2003\.  Verifying sequential consistency on shared-memory multiprocessors by model checking.  _IEEE Transactions on Parallel and Distributed Systems_ 14, 8 (2003), 730–741.  https://doi.org/10.1109/TPDS.2003.1225053
  * Tunç et al. (2023) Hünkar Can Tunç, Parosh Aziz Abdulla, Soham Chakraborty, Shankaranarayanan Krishna, Umang Mathur, and Andreas Pavlogiannis. 2023\.  _Optimal Reads-From Consistency Checking for C11-Style Memory Models_.  https://doi.org/10.5281/zenodo.7816526 Artifact.
  * Vafeiadis et al. (2015) Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, and Francesco Zappa Nardelli. 2015\.  Common Compiler Optimisations Are Invalid in the C11 Memory Model and What We Can Do about It. In _Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Mumbai, India) _(POPL ’15)_. Association for Computing Machinery, New York, NY, USA, 209–220.  https://doi.org/10.1145/2676726.2676995
  * Wickerson et al. (2017) John Wickerson, Mark Batty, Tyler Sorensen, and George A. Constantinides. 2017.  Automatically Comparing Memory Consistency Models. In _Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages_ (Paris, France) _(POPL ’17)_. Association for Computing Machinery, New York, NY, USA, 190–204.  https://doi.org/10.1145/3009837.3009838
  * Williams (2019) Virginia Vassilevska Williams. 2019\.  On some fine-grained questions in algorithms and complexity. In _Proceedings of the International Congress of Mathematicians_. 3447–3487.  https://doi.org/10.1142/9789813272880_0188
  * Williams and Williams (2018) Virginia Vassilevska Williams and R. Ryan Williams. 2018.  Subcubic Equivalences Between Path, Matrix, and Triangle Problems.  _J. ACM_ 65, 5, Article 27 (2018), 38 pages.  https://doi.org/10.1145/3186893
  * Windsor et al. (2022) Matt Windsor, Alastair F. Donaldson, and John Wickerson. 2022\.  High-coverage metamorphic testing of concurrency support in C compilers.  _Software Testing, Verification and Reliability_ 32, 4 (2022).  https://doi.org/10.1002/stvr.1812
  * Zennou et al. (2019) Rachid Zennou, Ahmed Bouajjani, Constantin Enea, and Mohammed Erradi. 2019.  Gradual Consistency Checking. In _Computer Aided Verification_ , Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing, Cham, 267–285.  https://doi.org/10.1007/978-3-030-25543-5_16

##  Appendix A Proofs

###  A.1. Proofs from Section 3

See 3.2

###### Proof.

First we have
$(\mathtt{w}^{\prime},\mathtt{w})\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$,
due to read-coherence. Since
$(\mathtt{w}^{\prime},\mathtt{w})\not\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{+}$,
we have that $\mathtt{w}^{\prime}$ is not in the
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$-chain
of $\mathtt{w}$, otherwise we would have
$(\mathtt{w},\mathtt{w}^{\prime})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{+}$,
which together with
$(\mathtt{w}^{\prime},\mathtt{w})\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$,
would violate write-coherence. Due to atomicity, we then have
$(\mathtt{w}^{\prime},\mathtt{w}_{1})\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$,
where
$\mathtt{w}_{1}=\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{-1}(\mathtt{w})$.
The final statement follows by applying atomicity inductively on the
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$-chain,
i.e., for each
$\mathtt{w}_{i}=\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{-1}(\mathtt{w}_{i-1})$,
we have
$(\mathtt{w}^{\prime},\mathtt{w}_{i})\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$.
∎

###  A.2. Proofs from Section 4.1

See 1.5

###### Proof.

We argue about both correctness and running time.

Correctness of Algorithm 1. We first argue that whenever the algorithm reports
a violation, the input
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$
is not WRA consistent. If
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
is acyclic or
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$
violates weak-atomicity (Algorithm 1), then clearly
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$
violates one of irrHB or weak-atomicity and thus violates $\mathsf{WRA}$
consistency. Next, suppose a violation is reported on Algorithm 1 when
processing event $e$. Observe that
$e.\mathsf{op}\in\\{\mathtt{r},\mathtt{rmw}\\}$, and let $x=e.\mathsf{loc}$,
as well as
$w=\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{-1}(e)$,
with $t^{\prime}=w.\mathsf{tid}$. There must be a thread $u$ and another event
$w_{u}$ such that $w_{u}\not\in\\{w,e\\}$ and further,
$(w,w_{u})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
and
$(w_{u},e)\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$.
This clearly violates weak-read-coherence since
$(w,w_{u})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hbloc}$,
$(w_{u},e)\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
and
$(e,w)\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{-1}$
and thus
$(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hbloc};[\mathsf{W}\cup\mathsf{RMW}];\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb};\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{-1})$
is reflexive.

Now, let’s assume that no violation was reported. Then clearly
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
is irreflexive and
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$
satisfies weak-atomicity. Now assume on the contrary that weak-read-coherence
was violated by some triplet $(w_{u},w,r)$ where
$w_{u}.\mathsf{loc}=w.\mathsf{loc}=r.\mathsf{loc}=x$,
$(w,r)\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$,
$w_{u}\not\in\\{w_{u},w\\}$, $w_{u}.\mathsf{tid}=u$,
$w.\mathsf{tid}=t^{\prime}$ and
$\\{(w,w_{u}),(w_{u},r)\\}\subseteq\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$.
Then, when processing event $r$, we will consider the event
$w_{u}^{\textsf{last}}$ such that $w_{u}^{\textsf{last}}$ is the last event
that is both
$\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}^{?}$-after
$w_{u}$ and is
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$-before
$r$, yielding
$\\{(w,w_{u}^{\textsf{last}}),(w_{u}^{\textsf{last}},r)\\}\subseteq\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$.
This means the algorithm will report a violation, which is a contradiction.

Complexity. First, checking for reflexivity of
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
takes $O(n)$ time — this can be done using a cycle detection algorithm on a
graph with $|\mathsf{E}|=n$ nodes and with $O(n)$ edges (corresponding to
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$
and
$\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color<EMAIL_ADDRESS>orderings). Next, checking for weak-atomicity of
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$
also takes $O(n)$ — scan over all write events and check if there are more
than one RMW events that read from any given write. Next, the computation of
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
timestamps takes $O(n\cdot k)$ time (Proposition 3.1) and the computation
involved in initializing and accessing the lists
$\\{{\mathbb{WList}}_{t,x}^{u}\\}_{t,x,u}$ takes $O(n\cdot k)$ time. Finally,
at each read event, the algorithm spends $O(k)$ time. This gives a total
running time of $O(n\cdot k)$. ∎

###  A.3. Proofs from Section 4.2

####  A.3.1. Proof of Theorem 1.2

We first present the proof of the lower bound.

See 4.1

###### Proof.

Consider two partial executions
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}_{1}=(\mathsf{E}_{1},\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}_{1},\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{1})$,
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}_{2}=(\mathsf{E}_{2},\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}_{2},\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{2})$,
where $\mathsf{E}_{1}$ consists of only read/write events,
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{1}$
is bijective, and
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}_{2}$
is identical to
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}_{1}$
except that every read event of $\mathsf{E}_{1}$ is replaced by an RMW event
in $\mathsf{E}_{2}$. We argue that
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}_{1}\models\mathsf{SC}$
iff
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}_{2}\models\mathsf{SC}$.
First, consider an
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{2}$
witnessing the consistency of
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}_{2}$.
Take
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{1}$
be identical to
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{2}$,
restricted on the write events of $\mathsf{E}$. Since the write events of
$\mathsf{E}_{1}$ are a subset of the write/RMW events of $\mathsf{E}_{2}$, we
have
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{1}\subseteq\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{2}$
and
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}fr}_{1}\subseteq\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}fr}_{2}$,
where
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}fr}_{i}$
is the corresponding from-reads relation derived from
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{i}$.
Since
$(\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}_{2}\cup\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{2}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{2}\cup\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}fr}_{2})$
is acyclic we have that
$(\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}_{1}\cup\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{1}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{1}\cup\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}fr}_{1})$
is also acyclic, thus
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{1}$
witnesses the $\mathsf{SC}$ consistency of
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}_{1}$.

For the inverse direction, consider an
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{1}$
witnessing the consistency of
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}_{1}$,
and let
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{2}=\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{1}\cup\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}fr}_{1}$.
Since there are no read events in $\mathsf{E}_{2}$, we have
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}fr}_{2}\subseteq\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{2}$.
Since
$(\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}_{1}\cup\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{1}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{1}\cup\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}fr}_{1})$
is acyclic, we have that
$(\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}_{2}\cup\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{2}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{2})=(\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}_{2}\cup\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{2}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{2}\cup\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}fr}_{2})$
is also acyclic. Thus
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{2}$
witnesses the $\mathsf{SC}$ consistency of
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}_{2}$.
∎

See 1.2

###### Proof.

Let
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}=(\mathsf{E},\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po},\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf})$
be an instance of the consistency problem for $\mathsf{SC}$. In light of Lemma
4.1, we assume that $\mathsf{E}$ consists of only write/RMW events. Since
$\mathsf{SC}\sqsubseteq\mathsf{SRA}$, if
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\models\mathsf{SC}$
then
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\models\mathsf{SRA}$.
For the inverse direction, assume that
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\models\mathsf{SRA}$
and let
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}=(\mathsf{E},\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po},\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf},\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo})$
be a witness execution, i.e.,
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}\models\mathsf{SRA}$.
Consider the derived relation
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}fr}$.
Since there are no read events in $\mathsf{E}$, we have
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}fr}\subseteq\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$.
Thus
$(\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}\cup\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo})=(\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}\cup\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}\cup\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}fr})$,
and since the former is acyclic, due to strong-write-coherence, so is the
latter. Hence
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}\models\mathsf{SC}$,
thereby serving as a witness for
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\models\mathsf{SC}$.
∎

####  A.3.2. Proof of Theorem 1.3

We now turn our attention to Theorem 1.3. We argue separately about soundness
(Lemma A.1) and completeness (Lemma A.2).

###### Lemma A.1.

If node $\mathsf{E}$ is reachable in
$\mathcal{G}_{\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}}$,
then
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\models\mathsf{SRA}$.

###### Proof.

Consider a path $\rho$ in
$\mathcal{G}_{\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}}$
from the root node $\varnothing$ to the terminal node $\mathsf{E}$. We
represent $\rho$ as a sequence of events, which are the ones executed along
the corresponding edges traversed by $\rho$. We construct a modification order
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
such that, for any two write/RMW events $\mathtt{w}_{1},\mathtt{w}_{2}$ on the
same location, we have
$(\mathtt{w}_{1},\mathtt{w}_{2})\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
iff $\mathtt{w}_{1}$ is executed before $\mathtt{w}_{2}$ in $\rho$. We argue
that the resulting execution
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}=(\mathsf{E},\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po},\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf},\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo})$
satisfies the $\mathsf{SRA}$ axioms.

  1. (1)

_Strong-write-coherence:_ Due to Item (1) of the executability conditions, no
event $e$ of $\rho$ is
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$-ordered
before any event appearing before $e$ in $\rho$. Moreover, by construction, no
event $e$ of $\rho$ is
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$-ordered
before any event appearing before $e$ in $\rho$. Thus $\rho$ represents a
linear extension of
$(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo})$,
and hence write-coherence is satisfied.

  2. (2)

_Read-coherence:_ Consider any triplet
$(\mathtt{w},\mathtt{r},\mathtt{w}^{\prime})$ such that
$(\mathtt{w}^{\prime},\mathtt{r})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$.
It suffices to argue that $\mathtt{w}^{\prime}$ appears in $\rho$ before
$\mathtt{w}$, implying that
$(\mathtt{w}^{\prime},\mathtt{w})\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$,
and thus read-coherence is not violated for $\mathtt{r}$. Indeed, Item (a) of
the enabledness condition makes $\mathtt{w}$ not enabled in any node $S$ for
which $\mathtt{w}^{\prime}\not\in S$. Thus any path from the root
$\varnothing$ to a node that contains both $\mathtt{w}$ and
$\mathtt{w}^{\prime}$ must execute $\mathtt{w}^{\prime}$ before $\mathtt{w}$.

  3. (3)

_Atomicity:_ Consider any trilpet
$(\mathtt{w},\mathtt{rmw},\mathtt{w}^{\prime})$, where
$\mathtt{rmw}\in\mathsf{RMW}$ is an RMW event. We have to argue that
$\mathtt{w}^{\prime}$ does not appear between $\mathtt{w}$ and $\mathtt{rmw}$
in $\rho$. Indeed, Item (b) of the enabledness condition makes
$\mathtt{w}^{\prime}$ not enabled in any node $S$ for which $\mathtt{w}\in S$
and $\mathtt{rmw}\not\in S$. Thus, any path from the root $\varnothing$ to a
node that contains both $\mathtt{w}$ and $\mathtt{w}^{\prime}$ must execute
$\mathtt{w}^{\prime}$ before $\mathtt{w}$.

The desired result follows. ∎

###### Lemma A.2.

If
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\models\mathsf{SRA}$,
then node $\mathsf{E}$ is reachable in
$\mathcal{G}_{\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}}$.

###### Proof.

Consider any witness complete execution
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}=(\mathsf{E},\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po},\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf},\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo})$
with
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}\models\mathsf{SRA}$.
We show the existence of a path $\rho$ from the root $\varnothing$ to the
terminal $\mathsf{E}$ incrementally, with the property that every node $S$ in
$\rho$ is downward-closed wrt
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$.
The statement clearly holds for the root $\varnothing$. Now assume that the
statement holds for some $S$, and we argue that there is an executable event
that takes us to $S^{\prime}$, with the statement holding in $S^{\prime}$.

If there is a read event $\mathtt{r}$ such that $S\cup\\{\mathtt{r}\\}$ is
downward-closed wrt to
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$,
then $\mathtt{r}$ is enabled in $S$, and we execute it to arrive at
$S^{\prime}=S\cup\\{\mathtt{r}\\}$. Since
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
does not relate read events, we have that $S^{\prime}$ is also downward-closed
wrt
$(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo})$.

Otherwise, all
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$-minimal
events in $\mathsf{E}\setminus S$ are write/RMW events. Consider any such
event $\mathtt{w}$ that is also
$(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo})$-minimal,
and we argue that $\mathtt{w}$ is executable in $S$.

First, consider any triplet $(\mathtt{w},\mathtt{r},\mathtt{w}^{\prime})$ with
$(\mathtt{w}^{\prime},\mathtt{r})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$.
Read-coherence on
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}$
implies that
$(\mathtt{w}^{\prime},\mathtt{w})\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$.
Since $\mathtt{w}$ is
$(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo})$-minimal
in $\mathsf{E}\setminus S$ , we have that $\mathtt{w}^{\prime}\in S$. Thus the
enabledness condition in Item (a) holds.

Second, consider any triplet
$(\mathtt{w}^{\prime\prime},\mathtt{rmw},\mathtt{w})$, where
$\mathtt{rmw}\in\mathsf{RMW}$ is an RMW event, and such that
$\mathtt{w}^{\prime\prime}\in S$. Since $S$ is downward-closed wrt
$(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo})$,
we have that
$(\mathtt{w}^{\prime\prime},\mathtt{w})\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$.
Note that $\mathtt{rmw}\in S$ as well, as otherwise, by the minimality of
$\mathtt{w}$, we would have
$(\mathtt{w},\mathtt{rmw})\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$,
which would violate atomicity. Thus the enabledness condition in Item (b) also
holds, thereby making $\mathtt{w}$ executable in $S$. Finally, observe that,
by construction, the set $S^{\prime}=S\cup\\{\mathtt{w}\\}$ is downward-closed
wrt
$(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo})$.

The desired result follows. ∎

###  A.4. Proof of Section 4.3

See 4.3

###### Proof.

Since
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
is minimally coherent for
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$,
we have that
$(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\cup\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}})$
is acyclic. Let
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
be any linear extension of
$(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\cup\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}})^{+}$
projected on $\mathsf{W}$, and
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}=(\mathsf{E},\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po},\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf},\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo})$
the resulting execution. Clearly
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}$
satisfies strong-write-coherence. Now consider any triplet
$(\mathtt{w},\mathtt{r},\mathtt{w}^{\prime})$ with
$(\mathtt{w}^{\prime},\mathtt{r})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$.
As
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
is minimally coherent for
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}$,
we have
$(\mathtt{w}^{\prime},\mathtt{w})\in(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\cup\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}})^{+}$.
Thus
$(\mathtt{w}^{\prime},\mathtt{w})\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$,
and
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}$
also satisfies read-coherence. Hence
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}\models\mathsf{SRA}$,
witnessing that
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\models\mathsf{SRA}$,
as desired. ∎

See 1.4

###### Proof.

We start with soundness. First, the algorithm verifies that
$\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}\cup\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$
is acyclic (Algorithm 2). At the end of the algorithm, for every triplet
$(\mathtt{w},\mathtt{r},\mathtt{w}^{\prime})$ such that
$(\mathtt{w}^{\prime},\mathtt{r})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
and $\mathtt{w}^{\prime}$ is
$\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color<EMAIL_ADDRESS>among all such write/RMW events, we have
$(\mathtt{w}^{\prime},\mathtt{w})\in\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$.
It follows that, at the end of the loop of Algorithm 2, for every triplet
$(\mathtt{w},\mathtt{r},\mathtt{w}^{\prime})$ with
$(\mathtt{w}^{\prime},\mathtt{r})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$,
we have
$(\mathtt{w}^{\prime},\mathtt{w})\in(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\cup\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}})$,
thus
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
satisfies Item (1) of minimal coherence. Finally, the algorithm verifies that
$(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\cup\bigcup_{x\in\mathsf{E}.locs}\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x})$
is acyclic, thus
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
satisfies Item (2) of minimal coherence. In turn, Lemma 4.3 guarantees that
indeed
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\models\mathsf{SRA}$.

We now turn our attention to completeness. Clearly, if the algorithm returns
“Inconsistent” due to
$(\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}\cup\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf})$
being cyclic (Algorithm 2), we have
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\not\models\mathsf{SRA}$.
Otherwise, observe that, whenever the algorithm inserts an ordering
$(\mathtt{w}_{u},\mathtt{w}_{\mathsf{rf}})\in\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$,
we have a triplet $(\mathtt{w}_{\mathsf{rf}},\mathtt{r},\mathtt{w}_{u})$ and
$(\mathtt{w}_{u},\mathtt{r})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$.
But then Corollary 4.2 guarantees that, for any
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
witnessing the consistency of
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$,
we have
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}\subseteq\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$.
Hence if the algorithm returns “Inconsistent” in Algorithm 2, we have that
$(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\cup\bigcup_{x\in\mathsf{E}.locs}\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})$
is cyclic, contradicting
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
as a consistency witness. Thus
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\not\models\mathsf{SRA}$.
∎

###  A.5. Proofs from Section 4.4

We begin with the proof of Lemma 4.4. Consider any location
$x\in\mathsf{E}.locs$, and we extend
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x}$
to a total modification order
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$
that satisfies read-coherence, write-coherence and atomicity. We build
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$
in three phases, as follows.

  1. (1)

Initially, we set
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}=\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x}$.

  2. (2)

While there exist two (distinct, maximal)
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$-chains
$\mathtt{w}^{1}_{1},\mathtt{w}^{1}_{2},\dots,\mathtt{w}^{1}_{i_{1}}$ and
$\mathtt{w}^{2}_{1},\mathtt{w}^{2}_{2},\dots,\mathtt{w}^{2}_{i_{2}}$ such that
$(\mathtt{w}^{2}_{1},\mathtt{w}^{1}_{i_{1}})\not\in(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})^{+}$,
we insert an ordering $(\mathtt{w}^{1}_{i_{1}},\mathtt{w}^{2}_{1})$ in
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$.

  3. (3)

Finally we set
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$
to be
$(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})^{+}$
projected on $(\mathsf{W}\cup\mathsf{RMW})$.

Towards Lemma 4.4, we establish three intermediate lemmas.

###### Lemma A.3.

We have that
$(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})$
is acyclic at the end of phase 2.

###### Proof.

Since
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
is minimally coherent, the statement holds for
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$
at the beginning of phase 2. Moreover, in every step of phase 2 inserting an
ordering $(\mathtt{w}^{1}_{i_{1}},\mathtt{w}^{2}_{1})$ in
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$,
we have
$(\mathtt{w}^{2}_{1},\mathtt{w}^{1}_{i_{1}})\not\in(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})^{+}$.
Hence
$(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})$
remains acyclic after the ordering has been inserted in
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$.
∎

###### Lemma A.4.

At all times, for every
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$-chain
$\mathtt{w}_{1},\mathtt{w}_{2},\dots,\mathtt{w}_{i}$ and write/RMW event
$\mathtt{w}$, all accessing the same location $x$, if
$\mathbb{TC}[\mathtt{w}]\neq\mathtt{w}_{1}$ and
$(\mathtt{w},\mathtt{w}_{j})\in(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})^{+}$
for some $j\in\\{1,\dots,i\\}$, then
$(\mathtt{w},\mathtt{w}_{1})\in(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})^{+}$.

###### Proof.

We first prove that the statement holds at the end of phase 1, i.e., it holds
for
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x}$
instead of
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$.
Consider a path $\mathtt{w}\rightsquigarrow\mathtt{w}_{j}$ in
$(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x})^{+}$,
and let $\mathtt{w}^{\prime}$ be the first event in this path that belongs to
the
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$-chain
(i.e., $\mathbb{TC}[\mathtt{w}^{\prime}]=\mathtt{w}_{1}$). Hence
$\mathtt{w}^{\prime}\neq\mathtt{w}$. If $\mathtt{w}^{\prime}=\mathtt{w}_{1}$,
we are done. Otherwise, let $\mathtt{w}^{\prime\prime}$ be the immediate
predecessor of $\mathtt{w}^{\prime}$ in this path. We distinguish cases for
the edge connecting $\mathtt{w}^{\prime\prime}$ and $\mathtt{w}^{\prime}$ in
the path.

  1. (1)

$(\mathtt{w}^{\prime\prime},\mathtt{w}^{\prime})\in\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x}$.
Since
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
is minimally coherent, Item (2) implies that
$(\mathtt{w}^{\prime\prime},\mathtt{w}_{1})\in\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x}$.

  2. (2)

$(\mathtt{w}^{\prime\prime},\mathtt{w}^{\prime})\in(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x})$.
Then
$(\mathtt{w}^{\prime\prime},\mathtt{w}^{\prime})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{?};\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$.
Since
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
is minimally coherent, Item (1) implies that
$(\mathtt{w}^{\prime\prime},\mathtt{w}_{1})\in(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x})^{+}$.

Thus in both cases
$(\mathtt{w},\mathtt{w}_{1})\in(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x})^{+}$,
as desired. Second, observe that in every step of phase 2, we insert an
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$
ordering towards the top of an
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$-chain.
Hence the statement holds along every step of phase 2. ∎

###### Lemma A.5.

At the end of phase 2,
$(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})^{+}$
projected on $({{\mathsf{W}}_{x}}\cup{{\mathsf{RMW}}_{x}})$ is total.

###### Proof.

Consider any two (distinct, maximal)
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$-chains
$\mathtt{w}^{1}_{1},\mathtt{w}^{1}_{2},\dots,\mathtt{w}^{1}_{i_{2}}$ and
$\mathtt{w}^{2}_{1},\mathtt{w}^{2}_{2},\dots,\mathtt{w}^{2}_{i_{2}}$ accessing
the same location $x$, and such that
$(\mathtt{w}^{1}_{i_{1}},\mathtt{w}^{2}_{1})\not\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$
at the end of phase 2. Since that phase completed, we have
$(\mathtt{w}^{2}_{1},\mathtt{w}^{1}_{i_{1}})\in(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})^{+}$,
and thus
$(\mathtt{w}^{2}_{1},\mathtt{w}^{1}_{1})\in(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})^{+}$
by Lemma A.4. If also
$(\mathtt{w}^{2}_{i_{2}},\mathtt{w}^{1}_{1})\not\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$,
we similarly have
$(\mathtt{w}^{1}_{1},\mathtt{w}^{2}_{1})\in(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})^{+}$.
But then
$(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})^{+}$
would be cyclic, violating Lemma A.3. Thus
$(\mathtt{w}^{2}_{i_{2}},\mathtt{w}^{1}_{2})\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$.
It follows that
$(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})^{+}$
projected on $({{\mathsf{W}}_{x}}\cup{{\mathsf{RMW}}_{x}})$ is total. ∎

We are now ready to prove Lemma 4.4.

See 4.4

###### Proof.

Consider the modification order
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
constructed above, and we argue that
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
witnesses the consistency of
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$.
Write-coherence follows from Lemma A.3. For read-coherence, consider any
triplet $(\mathtt{w},\mathtt{r},\mathtt{w}^{\prime})$ such that
$(\mathtt{w}^{\prime},\mathtt{r})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{?};\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$.
If
$(\mathtt{w}^{\prime},\mathtt{w})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{+}$,
we have
$(\mathtt{w},\mathtt{w}^{\prime})\not\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$
due to write-coherence. Otherwise, since
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
is minimally coherent, we have
$(\mathtt{w}^{\prime},\mathbb{TC}[\mathtt{w}])\in\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$,
and due to write-coherence, we also have
$(\mathtt{w},\mathtt{w}^{\prime})\not\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$.
Hence
$(\mathtt{r},\mathtt{r})\not\in\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}fr};\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{?};\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$,
satisfying read-coherence. Finally, we argue about atomicity. Consider any RMW
event $\mathtt{rmw}$, and any triplet
$(\mathtt{w},\mathtt{rmw},\mathtt{w}^{\prime})$ with
$(\mathtt{w}^{\prime},\mathtt{rmw})\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$.
If $\mathbb{TC}[\mathtt{w}^{\prime}]=\mathbb{TC}[\mathtt{rmw}]$, due to
read/write-coherence, we have that
$\mathbb{PC}[\mathtt{w}^{\prime}]<\mathbb{PC}[\mathtt{w}]$. Thus
$(\mathtt{w}^{\prime},\mathtt{w})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}^{+}$,
and hence
$(\mathtt{w},\mathtt{w}^{\prime})\not\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$.
Otherwise, due to Lemma A.4, we have that
$(\mathtt{w}^{\prime},\mathbb{TC}[\mathtt{rmw}])\in(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})^{+}$,
and by write-coherence, we again have
$(\mathtt{w},\mathtt{w}^{\prime})\not\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x}$.
Thus, in both cases,
$(\mathtt{rmw},\mathtt{w}^{\prime})\not\in\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}fr}$.
The desired result follows. ∎

See 1.1

###### Proof.

We start with soundness. First, the algorithm verifies that
$(\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}\cup\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf})$
is acyclic (Algorithm 3). At the end of the algorithm, for every triplet
$(\mathtt{w},\mathtt{r},\mathtt{w}^{\prime})$ such that
$(\mathtt{w}^{\prime},\mathtt{r})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{?};\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
and $\mathtt{w}^{\prime}$ is
$\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color<EMAIL_ADDRESS>among all such write/RMW events, if
$(\mathtt{w}^{\prime},\mathtt{w})\not\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{+}$,
we have
$(\mathtt{w}^{\prime},\mathtt{w})\in\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x}$.
It follows that, at the end of loop of Algorithm 3, for every triplet
$(\mathtt{w},\mathtt{r},\mathtt{w}^{\prime})$ such that
$\mathtt{w}^{\prime}\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{?};\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$,
if
$(\mathtt{w}^{\prime},\mathtt{w})\not\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{+}$,
then
$(\mathtt{w}^{\prime},\mathtt{w})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}^{?};\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$.
Thus
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
trivially satisfies Item (1) of minimal coherence. Moreover, since every
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
ordering goes to the top of an
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$-chain,
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
also satisfies Item (2) of minimal coherence. Finally, the algorithm verifies
that
$(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x})$
is acyclic for every location $x$, hence
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
satisfies Item (3) of minimal coherence. Thus, Lemma 4.4 guarantees that
indeed
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\models\mathsf{RC20}$.

We now turn our attention to completeness. Clearly, if the algorithm returns
“Inconsistent” due to
$(\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}\cup\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf})$
being cyclic (Algorithm 3), we have
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\not\models\mathsf{RC20}$.
Otherwise, observe that, whenever the algorithm inserts an ordering
$(\mathtt{w}_{u},\mathtt{w})$ in
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
in the loop of Algorithm 3, we have
$(\mathtt{w}_{u},\mathtt{r})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{?};\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$,
where $\mathtt{r}$ is a read/RMW event such that there exists a triplet
$(\mathtt{w}_{\mathsf{rf}},\mathtt{r},\mathtt{w}_{u})$ and
$(\mathtt{w}_{u},\mathtt{w}_{\mathsf{rf}})\not\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{+}$.
But then Lemma 3.2 guarantees that, for any
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
witnessing the consistency of
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$,
we have
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}\subseteq\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$.
Hence if the algorithm returns “Inconsistent” in Algorithm 3, we have that
$(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})$
is cyclic for some location $x$, contradicting
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
as a consistency witness. Thus
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\not\models\mathsf{RC20}$.
∎

###  A.6. Proofs from Section 4.5

Towards Theorem 1.6, we first prove the following intermediate lemma

###### Lemma A.6.

Before Algorithm 4 processes a read/RMW event $e(t,x)$, for every triplet
$(\mathtt{w}_{\mathsf{rf}},e,\mathtt{w}^{\prime})$, if
$(\mathtt{w}^{\prime},e)\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{?};\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color<EMAIL_ADDRESS>then $\mathtt{w}^{\prime}=\mathsf{LW}_{t,x}$ or
$(\mathtt{w}^{\prime},\mathsf{LW}_{t,x})\in(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}\cup\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}\cup\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}})^{+}$.

###### Proof.

The proof is by induction on the events of thread $t$ and location $x$
processed by the algorithm. The statement clearly holds for $e$ being the
first event of thread $t$, as there is no $\mathtt{w}^{\prime}$ with
$(\mathtt{w}^{\prime},e)\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{?};\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color<EMAIL_ADDRESS>while $\mathsf{LW}_{t,x}=\bot$.

Now consider that the algorithm processes an event $e$, and the statement
holds for the event $e^{\prime}$ that is an immediate
$\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color<EMAIL_ADDRESS>of $e$ in $t$. We split cases based on the type of $e^{\prime}$.

  1. (1)

$e^{\prime}\in({{\mathsf{W}}_{x}}\cup{{\mathsf{RMW}}_{x}})$. Then
$\mathsf{LW}_{t,x}=e^{\prime}$, while clearly, either
$\mathtt{w}^{\prime}=e^{\prime}$, or
$(\mathtt{w}^{\prime},e^{\prime})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{?};\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color<EMAIL_ADDRESS>
  2. (2)

$e^{\prime}\in{{\mathsf{R}}_{x}}$. Then
$\mathsf{LW}_{t,x}=\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{-1}(e^{\prime})$,
while clearly, either
$\mathtt{w}^{\prime}=\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{-1}(e^{\prime})$,
or
$(\mathtt{w}^{\prime},e^{\prime})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{?};\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color<EMAIL_ADDRESS>But for every event $\mathtt{w}^{\prime}$ with
$\mathtt{w}^{\prime}\neq\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{-1}(e^{\prime})$
and
$(\mathtt{w}^{\prime},e^{\prime})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{?};\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color<EMAIL_ADDRESS>the algorithm has either inserted an ordering
$(\mathtt{w}^{\prime},\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{-1}(e^{\prime}))\in\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x}$,
or infered that
$(\mathtt{w}^{\prime},\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{-1}(e))\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{+}$.
Thus the statement holds for $e$.

∎

See 1.6

###### Proof.

We start with soundness. First, the algorithm verifies that
$(\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}\cup\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf})$
is acyclic (Algorithm 4). Due to Lemma A.6, at the end of the algorithm, for
every triplet $(\mathtt{w},\mathtt{r},\mathtt{w}^{\prime})$ such that
$(\mathtt{w}^{\prime},\mathtt{r})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{?};\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color<EMAIL_ADDRESS>if
$(\mathtt{w}^{\prime},\mathtt{w})\not\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{+}$,
we have
$(\mathtt{w}^{\prime},\mathtt{w})\in\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x}$.
Thus
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
satisfies Item (1′) of minimal coherence. Moreover, since every
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
ordering goes to the top of an
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$-chain,
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
also satisfies Item (2) of minimal coherence. Finally, the algorithm verifies
that
$(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x})$
is acyclic for every location $x$ in Algorithm 4, hence
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
satisfies Item (3′) of minimal coherence. Thus, Lemma 4.4 guarantees that
indeed
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\models\mathsf{Relaxed}$.

We now turn our attention to completeness. Clearly, if the algorithm returns
“Inconsistent” due to
$(\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}\cup\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf})$
being cyclic (Algorithm 4), we have
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\not\models\mathsf{Relaxed}$.
Otherwise, observe that, whenever the algorithm inserts an ordering
$(\mathtt{w}_{u},\mathtt{w})$ in
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$
in the loop of Algorithm 4, we have
$(\mathsf{LW}_{t,x},\mathtt{r})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{?};\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color<EMAIL_ADDRESS>where $\mathtt{r}$ is a read/RMW event such that there exists a triplet
$(\mathtt{w}_{\mathsf{rf}},\mathtt{r},\mathsf{LW}_{t,x})$, and
$(\mathsf{LW}_{t,x},\mathtt{w}_{\mathsf{rf}})\not\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{+}$.
But then Lemma 3.2 guarantees that, for any
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
witnessing the consistency of
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$,
we have
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}\subseteq\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$.
Hence if the algorithm returns “Inconsistent” in Algorithm 4, we have that
$(\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}_{x}\cup\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}_{x}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{x})$
is cyclic for some location $x$, contradicting
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
as a consistency witness. Thus
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\not\models\mathsf{Relaxed}$.

Finally, we turn our attention to complexity. The computation of
$(\mathbb{TC},\mathbb{PC})$ in Algorithm 4 takes $O(n)$ time (Section 3). For
every location $x$, the loop in Algorithm 4 takes $O({{n}_{x}})$ time, where
${{n}_{x}}=|{{\mathsf{E}}_{x}}|$. The acyclicity check in Algorithm 4 can also
easily performed in $O(n_{x})$ time, viewed as a cycle detection problem on a
graph of $O({{n}_{x}})$ edges. Summing over all locations $x$, we obtain total
time $\sum_{x}O({{n}_{x}})=O(n)$. ∎

###  A.7. Proofs of Section 4.6

Correctness. Let us now argue about the correctness of the construction i.e.,
$G$ has a triangle iff
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$
is not consistent under $\mathsf{WRA}$, $\mathsf{RA}$ or $\mathsf{SRA}$. The
precise statements we prove are as follows. First, if $G$ has a triangle then
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\not\models\mathsf{WRA}$,
implying
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\not\models\mathsf{RA}$
and
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\not\models\mathsf{SRA}$.
Second, we show that if $G$ does not have a triangle then
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\models\mathsf{SRA}$,
implying
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\not\models\mathsf{RA}$
and
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\not\models\mathsf{WRA}$.

We first observe that
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
is indeed acyclic. This is because the event set $\mathsf{E}$ can be
partitioned into $6$ classes
$\mathsf{E}_{1},\mathsf{E}_{2},\ldots,\mathsf{E}_{6}$, and the
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
edges only go from $\mathsf{E}_{i}$ to $\mathsf{E}_{j}$ for $i<j$.
Specifically, $\mathsf{E}_{1}=\\{\mathtt{w}_{\alpha}\,|\,\alpha\in V_{G}\\}$,
$\mathsf{E}_{2}=\\{\mathtt{w}^{\beta}_{\alpha}\,|\,\\{\alpha,\beta\\}\in
E_{G},\alpha<\beta\\}$,
$\mathsf{E}_{3}=\\{\sf\mathtt{w}Jxn_{\alpha}\,|\,\alpha\in V_{G}\\}$,
$\mathsf{E}_{4}=\\{e_{(\alpha,\beta)}\,|\,\\{\alpha,\beta\\}\in
E_{G},\alpha<\beta\\}$,
$\mathsf{E}_{5}=\\{\sf\mathtt{w}Jxn_{\alpha}\,|\,\alpha\in V_{G}\\}$, and
$\mathsf{E}_{6}=\\{\mathtt{r}^{\alpha}_{\beta}\,|\,\\{\alpha,\beta\\}\in
E_{G},\alpha<\beta\\}$. Observe that the
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
edges only go from $\mathsf{E}_{1}$ to $\mathsf{E}_{2}$, $\mathsf{E}_{2}$ to
$\mathsf{E}_{3}$, $\mathsf{E}_{3}$ to $\mathsf{E}_{4}$, $\mathsf{E}_{4}$ to
$\mathsf{E}_{5}$, $\mathsf{E}_{5}$ to $\mathsf{E}_{6}$ and also from
$\mathsf{E}_{1}$ to $\mathsf{E}_{6}$.

($\Rightarrow$) Assume that there is a triangle in $G$, and we show that there
is a violation of weak-read-coherence. Consider the triangle
$(\alpha,\beta,\gamma)$ in $G$, with $\alpha<\beta<\gamma$. Consider the
events $\mathtt{w}_{\beta}$, $\mathtt{w}^{\gamma}_{\beta}$ and
$\mathtt{r}^{\alpha}_{\beta}$, which access the same memory location
$y_{\beta}$. The construction ensures that
$(\mathtt{w}_{\beta},\mathtt{r}^{\alpha}_{\beta})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$,
and
also$(\mathtt{w}_{\beta},\mathtt{w}^{\gamma}_{\beta})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$.
Now observe the sequence of
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
edges: $(\mathtt{w}^{\gamma}_{\beta},\sf\mathtt{w}Jxn_{\gamma})$,
$(\sf\mathtt{w}Jxn_{\gamma},e_{(\alpha,\gamma)})$,
$(e_{(\alpha,\gamma)},\sf\mathtt{r}Jxn_{\alpha})$,
$(\sf\mathtt{r}Jxn_{\alpha},\mathtt{r}^{\alpha}_{\beta})$. Clearly, all of
these together imply that
$(\mathtt{w}^{\gamma}_{\beta},\mathtt{r}^{\alpha}_{\beta})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$.
This is a violation of weak-read-coherence. See Fig. 10 for illustration.

($\Leftarrow$) Assume that $G$ is triangle-free, and we show that
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}\models\mathsf{SRA}$.
Consider the per-location
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}=\bigcup_{\alpha\in
V_{G}}\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{y_{\alpha}}$
such that
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}_{\alpha}$
is the total order
$\mathtt{w}_{\alpha}<\mathtt{w}^{\beta_{1}}_{\alpha}<\mathtt{w}^{\beta_{2}}_{\alpha}\ldots<\mathtt{w}^{\beta_{k}}_{\alpha}$,
where $\beta_{1}<\beta_{2}<\ldots<\beta_{k}$ are all the neighbors of $\alpha$
(recall that each write event accesses location $y_{a}$). We will show that
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}=\langle\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}.\mathsf{E},\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}.\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po},\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}.\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf},\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}\rangle$
is $\mathsf{SRA}$-consistent. First, we argue that
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}$
satisfies strong-write-coherence. Assume on the contrary that there is a
$(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo})^{+}$
cycle $\mathcal{C}$. Since
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
and
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
are both acyclic, there must be at least one
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
edge and at least one
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
edge in $\mathcal{C}$. Thus, there must be three distinct events
$e_{1},e_{2},e_{3}$ in the cycle such that
$(e_{1},e_{2})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
and
$(e_{2},e_{3})\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$,
and let $y_{\alpha}=e_{2}.\mathsf{loc}=e_{3}.\mathsf{loc}$. Our construction
ensures that the only
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
edge incident to a write event of $y_{\alpha}$ emanates from
$\mathtt{w}_{\alpha}$, and thus $e_{1}=\mathtt{w}_{\alpha}$. Our construction
further ensures that there is no incoming
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
edge into $\mathtt{w}_{\alpha}$, while our
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
also does not have incoming edges into $\mathtt{w}_{\alpha}$, which is a
contradiction as $e_{1}$ cannot participate in a
$(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}\cup\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo})^{+}$
cycle. Let us now argue that
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}$
satisfies read-coherence. Assume on the contrary that it does not. Then, there
are distinct events $e_{1},e_{2},e_{3}$ such that
$(e_{1},e_{3})\in\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$,
$(e_{1},e_{2})\in\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
and
$(e_{2},e_{3})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$.
The only memory locations with $>1$ read accesses are those on the locations
associated with a node in the graph. Thus, there is a node $\beta\in V_{G}$
such that $e_{1}=\mathtt{w}_{\beta}$ and two nodes $\alpha$ and $\gamma$ such
that $e_{3}=\mathtt{r}^{\alpha}_{\beta}$ and
$e_{2}=\mathtt{w}^{\gamma}_{\beta}$. It follows that $\alpha<\beta<\gamma$,
and that $(\alpha,\beta)\in E_{G}$ and $(beta,\gamma)\in E_{G}$. Now consider
the
$\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$
path from $e_{2}$ to $e_{3}$. The only edge emanating from
$e_{2}=\mathtt{w}^{\gamma}_{\beta}$ is
$(\mathtt{w}^{\gamma}_{\beta},\sf\mathtt{w}Jxn_{\gamma})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$.
Similarly, the only
non-$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$
edge incident onto $e_{3}=\mathtt{r}^{\alpha}_{\beta}$ is the edge
$(\sf\mathtt{r}Jxn_{\alpha},\mathtt{r}^{\alpha}_{\beta})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$.
Thus, it must be that
$(\sf\mathtt{w}Jxn_{\gamma},\sf\mathtt{r}Jxn_{\alpha})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}^{+}$.
This is possible only when the event $e_{(\alpha,\gamma)}$ exists as the only
edges that are incident onto $\sf\mathtt{r}Jxn_{\alpha}$ emanate from an event
of the form $e_{(\alpha,*)}$, and the only edges that emanate from
$\sf\mathtt{w}Jxn_{\gamma}$ are incident on events of the form
$e_{(*,\gamma)}$. Thus, $(\alpha,\gamma)\in E_{G}$ by the construction,
resulting to a triangle $(\alpha,\beta,\gamma)$, which is a contradiction.
Thus
$\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}$
satisfies all the axioms of $\mathsf{SRA}$.

Time Complexity. The total time to construct
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$
is proportional to $O(|V_{G}|+|E_{G}|)$. Also, the size of
$\overline{\mathsf{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}X}}$
is $O(|V_{G}|+|E_{G}|)$. Thus, if there is an algorithm that solves
consistency under any of $\mathsf{SRA}$, $\mathsf{RA}$ or $\mathsf{WRA}$ in
time $O(n^{\omega/2-\epsilon})$, then there is an algorithm that checks for
triangle-freeness in time $O(n^{\omega/2-\epsilon})$ on graphs of $n$ nodes.
Moreover, since our reduction is completely combinatorial, if there is a
combinatorial algorithm that solves consistency in $O(n^{3/2-\epsilon})$ time,
then there is an algorithm that checks for triangle-freeness in time
$O(n^{3/2-\epsilon})$ on graphs of $O(n)$ edges.

##  Appendix B Experimental Details

###  B.1. Further Experiments with TruSt

Here we report further experiments inside the TruSt model checker on
benchmarks that contain rlx accesses. TruSt follows the RC11 semantics (Lahav
et al., 2017) which has subtle difference from the RC20 model (Lahav and
Boker, 2022) in the definition of release-sequence as it uses rlx accesses.
The experimental results are shown in Table 3.

Table 3.  Performance comparison. Columns $2$ and $3$ denote the total number
of executions explored by resp. TruSt and our algorithm. Columns $5$ and $6$
denote the average time (in seconds) spent in consistency checking by resp.
TruSt and our algorithm. Columns $4$ and $7$ denote the respective ratios and
speedups.

1 | 2 | 3 | 4 | 5 | 6 | 7 | 1 | 2 | 3 | 4 | 5 | 6 | 7
---|---|---|---|---|---|---|---|---|---|---|---|---|---
Benchmark |  Avg. Time |  Executions | Benchmark |  Avg. Time |  Executions
TruSt | Our Alg. | R | TruSt | Our Alg. | S | TruSt | Our Alg. | R | TruSt | Our Alg. | S
barrier | 0.5 | 0.01 | 45.0 | 14K | 76K | 5.65 | mutex | 0.8 | 0.01 | 76.0 | 8K | 55K | 7.17
buf-ring | 1.6 | 0.05 | 31.6 | 3K | 5K | 1.83 | peterson | 0.3 | 0.01 | 26.0 | 4K | 5K | 1.16
chase-lev$\dagger$ | 0.0 | 0.0 | - | 2 | 2 | 1 | qu | 0.2 | 0.02 | 9.5 | 34 | 2K | 71.62
dekker | 0.3 | 0.1 | 2.7 | 24K | 234K | 9.88 | seqlock | 0.2 | 0.01 | 24.0 | 26K | 118K | 4.58
dq | 0.1 | 0.01 | 13.0 | 43K | 117K | 2.72 | spinlock | 1.0 | 0.02 | 49.0 | 6K | 17K | 2.91
fib-bench | 1.6 | 0.02 | 80.5 | 4K | 194K | 43.94 | szymanski | 0.5 | 0.01 | 50.0 | 2K | 2K | 1.17
lamport | 0.4 | 0.01 | 36.0 | 17K | 91K | 5.41 | ticketlock | 0.9 | 0.03 | 30.3 | 7K | 62K | 8.52
linuxrwlocks | 0.4 | 0.02 | 20.0 | 12K | 21K | 1.8 | treiber | 0.6 | 0.03 | 19.3 | 403 | 403 | 1
mcs-spinlock | 1.1 | 0.02 | 54.0 | 6K | 23K | 4.12 | ttaslock | 1.0 | 0.02 | 48.5 | 401 | 401 | 1
mpmc | 0.7 | 0.03 | 22.0 | 10K | 65K | 6.68 | twalock | 0.6 | 0.02 | 29.0 | 8K | 13K | 1.7
ms-queue$\dagger$ | 0.07 | 0.01 | 7.0 | 210 | 210 | 1 |  |  |  |  |  |  |
Totals | - | - | - | - | - | - | - |  | 12.58 | 0.46 | 192K | 1.1M | -

###  B.2. Incremental Algorithm for Consistency Checking

In this section we present in detail our increlemental algorithm for
consistency checking that is evaluated in Section 5.2. Overall, Algorithm 5
has a similar working mechanism as Algorithm 3, i.e., it computes the same
minimally coherent partial modification order
$\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}$.
In contrast to that algorithm however, as we need efficient, on-the-fly
consistency checks, this algorithm maintains a per-location order
$\mathsf{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}hbmo}_{x}$
on write/RMW events that satisfies following invariants: (i)
$\mathsf{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}hbmo}_{x}\subseteq(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x})^{+}$
and (ii)
$(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup(\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x};\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}_{x}^{?}))\subseteq\mathsf{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}hbmo}_{x}$.

The algorithm is given in pseudocode in Algorithm 5. Its main data structure
is $\mathsf{HBMO}\colon\mathsf{E}\to\mathbb{N}_{\geq 0}$, that is used to
store the
$\mathsf{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}hbmo}$
relation. When a new read or write event is observed, the functions
readHandler and writeHandler are called, respectively. RMW events are handled
by first calling readHandler followed by writeHandler. The algorithm does not
precompute the array $\mathbb{HB}$
($\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}$-timestamps)
or the data structures $\\{{\mathbb{WList}}_{t,x}^{u}\\}_{t,x,u}$ (for
implementing $\textsf{lastWriteBefore}(\cdot,\cdot,\cdot)$) and
$\\{{\mathbb{RList}}_{t,x}^{u}\\}_{t,x,u}$ (for implementing
$\textsf{lastReadBefore}(\cdot,\cdot,\cdot)$). Instead, it maintains the same
information on-the-fly (Lines 5, 5, 5, 5-5).

In more detail, read and write events are handled as follows.

  * •

For a new read event $e=\mathtt{r}(x)$ (or $e=\mathtt{rmw}(x)$) with
$w_{\mathsf{rf}}=\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}^{-1}(e)$,
in the first part of the procedure (Algorithms 5-5) the algorithm performs
certain checks (Lines 5, 5, 5) to ensure that extending the execution with $e$
results in a consistent execution. These checks are performed by means of an
acyclicity check and they ensure that the write coherence and atomicity axioms
are not violated.

A core component of the algorithm is the $\mathsf{HBMO}$ clocks, which are
essential for performing efficient consistency checks incrementally. Each
write event in the execution has an associated $\mathsf{HBMO}$ vector clock.
RMW events in the same chain are represented with a single $\mathsf{HBMO}$
clock. Intuitively, $\mathsf{HBMO}$ clock of a write event $\mathtt{w}$
captures the incoming
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
edges to $\mathtt{w}$ from the writes in the other threads.

In order to decide whether the new read/RMW event $\mathtt{r}(x)$ can observe
a write/RMW event $\mathtt{w}(x)$, we must determine if there exists another
write/RMW event $\mathtt{w}^{\prime}(x)$ such that
$(\mathtt{w}^{\prime},\mathtt{r})\in\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}$
and
$(\mathtt{w}^{\prime},\mathtt{w})\in(\mathsf{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}hb}_{x}\cup\overline{\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}}_{x})^{+}$,
as this would lead to a consistency violation (Algorithms 5-5).

An important feature of Algorithm 5 is that to optimize for performance, it
does not keep the $\mathsf{HBMO}$ clocks transitively closed. Due to this
reason, the algorithm may fail to reject an inconsistent execution in these
first checks. To aleviate this, in Algorithms 5-5, a transitive closure
procedure is conducted and the above condition is checked again (Algorithm 5).
If this step is passed, then the algorithm updates the state of the execution
(Algorithms 5-5) and declares that the execution is consistent. While the
algorithm is updating the state of the execution, it propagates the new
inferred
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
edges on $\mathtt{w}_{\mathsf{rf}}$ into the writes that are
$\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color<EMAIL_ADDRESS>ordered after $\mathbb{TC}[\mathtt{w}_{\mathsf{rf}}]$ (Algorithm 5).

  * •

For a new write event $e=\mathtt{w}(t,x)$ (or $e=\mathtt{rmw}(t,x)$), the main
goal of the procedure is to initialize or update the $\mathsf{HBMO}$ clock of
$e$. In particular, the algorithm first fetches the write event $\mathtt{w}$
which corresponds to the last executed write event in thread $t$ on location
$x$. The algorithm then joins $\mathsf{HBMO}[\mathbb{TC}[e]]$ with
$\mathsf{HBMO}[\mathtt{w}]$ and $\mathbb{HB}[e]$ (Algorithm 5) and propagates
the new inferred
$\mathsf{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}mo}$
edges into the writes that are
$\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color<EMAIL_ADDRESS>ordered after $\mathbb{TC}[e]$. The latter step is only relevant for the write
events that are associated with an
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$-chain.

1

2function  _readHandler(_$e,w_{\mathsf{rf}}$_)_

3 $\mathbb{HB}[e]\leftarrow\mathbb{H}_{t}[t]+1$ ;
$\mathsf{PredHBMO}\leftarrow[]$

4

5 foreach  _$t^{\prime}\in tids$_ do

6 let $w=$ lastWriteBefore($t^{\prime},x,\mathbb{H}_{t}[t^{\prime}]$)

7 if  _$w\neq w_{\mathsf{rf}}$_ then

8 if  _$\mathbb{TC}[w]=\mathbb{TC}[w_{\mathsf{rf}}]$_ then

9 if  _$\mathbb{PC}[w_{\mathsf{rf}}] <\mathbb{PC}[w]$_ then

10 declare ‘Inconsistent’

11 else

12 if
_$\mathsf{HBMO}[\mathbb{TC}[w]][\mathbb{TC}[w_{\mathsf{rf}}].\mathsf{tid}]\geq\mathbb{HB}[\mathbb{TC}[w_{\mathsf{rf}}]][\mathbb{TC}[w_{\mathsf{rf}}].\mathsf{tid}]$_
then

13 declare ‘Inconsistent’

14 $\mathsf{PredHBMO}\leftarrow\mathsf{PredHBMO}\sqcup\mathsf{HBMO}[w]$

15 let $L=tids$; let $changedThreads=\varnothing$

16 while  _$L\neq\varnothing$_ do

17 foreach  _$t^{\prime}\in L$_ do

18 if  _$\mathbb{HB}[e][t^{\prime}] <\mathsf{PredHBMO}[t^{\prime}]$_ then

19 let $w^{\prime}=$
lastWriteBefore($t^{\prime},x,\mathsf{PredHBMO}[t^{\prime}]$)

20 if
_$\mathsf{HBMO}[\mathbb{TC}[w^{\prime}]][\mathbb{TC}[w_{\mathsf{rf}}].\mathsf{tid}]\geq\mathsf{HBMO}[\mathbb{TC}[w_{\mathsf{rf}}]][\mathbb{TC}[w_{\mathsf{rf}}].\mathsf{tid}]$_
then

21 declare ‘Inconsistent’

22
$\mathsf{PredHBMO}\leftarrow\textnormal{{pairwiseMaxIndexes(}}\textnormal{\emph{$\mathsf{PredHBMO},\mathsf{HBMO}[w^{\prime}]$}}\textnormal{{)}}$

23 $changedThreads\leftarrow
changedThreads\cup\mathsf{PredHBMO}.\mathsf{changedIndexes}$

24 $L\leftarrow changedThreads$; $changedThreads\leftarrow\varnothing$

25
$\mathsf{HBMO}[\mathbb{TC}[w_{\mathsf{rf}}]]\leftarrow\mathsf{HBMO}[\mathbb{TC}[w_{\mathsf{rf}}]]\sqcup\mathsf{PredHBMO}$

26 $\mathbb{HB}[e]\leftarrow\mathbb{HB}[e]\sqcup\mathbb{HB}[w_{\mathsf{rf}}]$;
$\mathbb{H}_{t}[t]\leftarrow\mathbb{H}_{t}[t]+1$

27 $\textnormal{{poPropagate}}(\mathbb{TC}[w_{\mathsf{rf}}])$

28 declare ‘Consistent’

29function  _writeHandler(_$e$_)_

30 if  _$e.\mathsf{op}\not=\mathtt{rmw}$_ then

31 $\mathbb{H}_{t}[t]\leftarrow\mathbb{H}_{t}[t]+1$;
$\mathbb{HB}[e]\leftarrow\mathbb{H}_{t}[t]$; $\mathsf{HBMO}[e]\leftarrow[]$

32

33 let $w=$ lastWriteBefore($e.\mathsf{tid},e.\mathsf{loc},\mathbb{HB}[e]-1$)

34
$\mathsf{HBMO}[\mathbb{TC}[e]]\leftarrow\mathsf{HBMO}[\mathbb{TC}[e]]\sqcup\mathbb{HB}[e]\sqcup\mathsf{HBMO}[w]$

35 $\textnormal{{poPropagate}}(\mathbb{TC}[e])$

36 declare ‘Consistent’

Algorithm 5 Incremental consistency checking for $\mathsf{RA}$.

Scalablity experiments. We complement our experimental results of Table 2 with
some controlled scalability experiments that better illustrate differences in
consistency checking between Algorithm 5 and the algorithm implemented inside
C11Tester.

The benchmarks consists of patterns shown in Fig. 11. They are created to
exhibit certain behaviors which exploit contrasting aspects of the algorithms.
These benchmarks provide a better understanding of the algorithm by
demonstrating when and why Algorithm 5 ensues a better performance.

$e_{1}=\mathtt{w}(t,x)$$e_{6}=\mathtt{rmw}(t,x)$$\vdots$$e_{7}=\mathtt{rmw}(t,x)$$e_{2}=\mathtt{r}(t_{1},x)$$e_{3}=\mathtt{w}(t_{1},x)$$\ldots$$e_{4}=\mathtt{r}(t_{k},x)$$e_{5}=\mathtt{w}(t_{k},x)$$\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}$$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$
(a) Fixed
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$-Chain
Read-Write

$e_{1}=\mathtt{w}(t,x)$$e_{2}=\mathtt{rmw}(t,x)$$\vdots$$e_{3}=\mathtt{rmw}(t,x)$$e_{4}=\mathtt{w}(t_{1},x)$$e_{5}=\mathtt{r}(t_{1},x)$$\ldots$$e_{6}=\mathtt{w}(t_{k},x)$$e_{7}=\mathtt{r}(t_{k},x)$$\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}$$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$
(b) Fixed
$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$-chain
Write-Read.

$e_{3}=\mathtt{r}(t,y)$$e_{4}=\mathtt{w}(t,x)$$e_{5}=\mathtt{w}(t,x)$$e_{6}=\mathtt{w}(t,x)$$\vdots$$e_{1}=\mathtt{w}(t^{\prime},x)$$e_{2}=\mathtt{w}(t^{\prime},y)$$e_{7}=\mathtt{w}(t_{1},x)$$e_{8}=\mathtt{r}(t_{1},x)$$\ldots$$e_{9}=\mathtt{w}(t_{k},x)$$e_{10}=\mathtt{r}(t_{k},x)$$\mathsf{\color[rgb]{0.2,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.2}\pgfsys@color@gray@stroke{0.2}\pgfsys@color@gray@fill{0.2}po}$$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$$\mathsf{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}rf}$
(c) New read events.