# Complexity of Consistency Testing for the Release-Acquire Semantics

R Govind, S Krishna, Sanchari Sil, B Srivathsan

► To cite this version:

R Govind, S Krishna, Sanchari Sil, B Srivathsan. Complexity of Consistency Testing for the Release-Acquire Semantics. 2026. hal-05534072

HAL Id: hal-05534072

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

Preprint submitted on 3 Mar 2026

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

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

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

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
Complexity of Consistency Testing for the
Release-Acquire Semantics

R. Govind$^{1,2,5}$, S. Krishna$^3$, Sanchari Sil$^4$, and B. Srivathsan$^{4,5}$

¹ The Institute of Mathematical Sciences, Chennai, India, govind@imsc.res.in

² Homi Bhabha National Institute, Anushaktinagar, Mumbai, India

³ IIT Bombay, India, krishnas@cse.iitb.ac.in

⁴ Chennai Mathematical Institute, India, {sanchari, sri} @ cmi.ac.in

⁵ CNRS, ReLaX, IRL 2000, Chennai, India

**Abstract.** In a seminal work, Gibbons and Korach [10] studied the complexity of deciding whether an observed sequence of reads and writes of a multi-threaded program admits a sequentially consistent interleaving. They showed the problem to be NP-hard even under strong syntactic restrictions. More recently, Chakraborty et al. [7] considered the problem for weak memory models and proved that NP-hardness remains even when the number of threads, the number of memory locations, and the value domain are all bounded.

In this paper we revisit the problem for the release-acquire variants of the C11 memory model. Our main positive result is that consistency testing can be done in polynomial-time when each memory location is written by at most one thread (multiple readers are allowed). Notably, this restriction is already NP-hard for sequential consistency. We complement this upper bound with tight hardness results: the problem is NP-hard when two threads may write to the same location, and allowing three writers per location rules out $2^{o(k)} \cdot n^{O(1)}$ algorithms under the exponential Time Hypothesis, where *k* denotes the number of threads, and *n* the number of memory operations.

# 1 Introduction

Multi-threaded programs, in which threads interact through shared memory operations, are prevalent across software systems. Modern hardware and compilers apply various optimizations (like instruction reordering, store buffering, etc.) to enhance performance. These optimizations can cause threads to observe writes to a shared memory location in an order that differs from the program order. *Memory models* formalize the rules to constrain which values reads may observe, and allow the programmer to be aware of the memory behaviour. These models are implemented via hardware or software protocols. As the correctness of concurrent programs depends on the chosen memory model, a faithful implementation of memory models is essential.

One of the fundamental results in this subject is the work of Gibbons and Korach [10] on *testing shared memories*, which presents a way to test whether an
observed execution of a multi-threaded program is consistent with the (rules of the) underlying memory model. In their work [10], Gibbons and Korach consider sequential consistency (SC) [18], the most common and simple-to-understand memory model. SC uses an interleaving semantics to explain memory operations: any observed execution across the threads is identical to that of some global interleaving of the threads' operations that preserves the program order of each thread, and each read observes the value of the last write (in this interleaving) made to the memory location. Deciding whether an observed execution can be justified by such an interleaving is the classical consistency testing problem for SC.

## VERIFYING SEQUENTIAL CONSISTENCY (The VSC-problem [10])

**Instance:** A variable set $\mathcal{X}$, a value set $\mathcal{V}$, a finite collection of nonempty sequences $S_1, S_2, \dots, S_k$, each consisting of a finite set of memory operations of the form "$read(x, d)$" or "$write(x, d)$" with $x \in \mathcal{X}$ and $d \in \mathcal{V}$.

**Question:** Is there a sequence $S$, an interleaving of $S_1, S_2, \dots, S_k$ such that for each "$read(x, d)$" there is a preceding "$write(x, d)$" in $S$ with no other "$write(x, d')$" in between.

The set of sequences $S_1, \dots, S_k$ forms our observed execution. A "Yes" answer to the question above indicates that the observed execution admits an SC behaviour, while a "No" answer shows the memory implementation can violate sequential consistency.

Gibbons and Korach [10] established that the VSC problem is NP-complete, even under a number of natural syntactic restrictions (see Table 1 of [10]). Subsequent work has extended these complexity results along two complementary directions: (i) to weaker memory models that arise in programming languages, hardware, and distributed systems [21,25,8,23,9,5,4]; and (ii) to algorithmic techniques for stateless model-checking of multi-threaded programs under sequential consistency [1]. Consistency testing also appears in the context of comparing memory models [14].

In this work, we revisit this consistency testing problem for the Release-Acquire semantics (RA), which form the core of the memory model adopted by the C11 programming language. We also investigate its variants, the strong release acquire (SRA) [15] and the weak release acquire (WRA) [13]. For all these models, we make use of an axiomatic semantics that help reason about the observed executions as graphs and the rules of the model as constraints over special kinds of edges [16,15]. Closely related to these memory models are Relaxed [22,24] and causal consistency models [4,6] which employ axioms which differ mildly from the release-acquire variants. From [7] we know that the analogous consistency testing problem is NP-complete for all these models even when the number of threads, the number of memory locations and the domain of values are kept bounded. In this paper, we consider a different dimension to bound.
**Contributions.** We prove that the consistency testing problem under the release-acquire model and its variants can be solved in $O(n^3)$ (where $n$ is the total number of memory operations in the instance) for 1-WRITER systems: these are programs where almost one thread writes to a shared variable, but multiple threads can read from it. To the best of our knowledge, this is the first known polynomial-time algorithm for the consistency testing problem under the release-acquire semantics. Single-writer systems appear in several contexts, for instance, in producer-consumer models or CREW (concurrent-read-exclusive-write) distributed systems [12]. Notably, for sequential consistency, the problem for single-writer systems is known to be NP-hard [10], and from [1] it is known to have a polynomial-time procedure when the number of threads is kept bounded. Here, we show polynomial-time under no restriction, for the release-acquire semantics. As our second contribution, we present new lower bounds for the consistency testing problem under the release-acquire model and its variants:

- For 1-WRITER programs, we prove that there is no $O(n^{\frac{3}{2}-\epsilon})$-time algorithm, under the Boolean Matrix Multiplication (BMM) hypothesis, for any $\epsilon > 0$.

- When we consider 2-WRITER programs (those where each variable is written into by at most two threads), the problem continues to be NP-complete.

- Furthermore, when we consider 3-WRITER programs, the problem admits a conditional lower bound under the Exponential Time Hypothesis (ETH): there is no $2^{o(k)} \cdot n^{O(1)}$ algorithm, where $k$ is the number of threads, and $n$ is the total number of operations.

The results provide a tight complexity picture while bounding the number of writer threads per memory location, with 1-WRITER giving polynomial-time, 2-WRITER being NP-hard and 3-WRITER allowing a stronger conditional lower bound.

**Structure of the paper.** In Section 2, we present the axiomatic definitions for the release-acquire semantics and its variants. In Section 3, we present the polynomial-time procedure for single-writer systems and in Section 4, the hardness results. In the paper, we talk about the models RA, SRA and WRA. The corresponding results for the closely related memory models Relaxed and the models for causal consistency are presented in Appendices C and D. Finally, in Section 5, we conclude the paper with some directions for future work. Missing proofs can be found in clearly marked appendices.

## 2 Preliminaries

Unlike SC, where consistency is checked via an interleaving, release-acquire semantics requires reasoning with two special types of relations on the reads and writes: a reads-from relation rf (mapping each read to the write it observes) and a per-location modification order mo (ordering writes to the same variable). The verification question becomes: does there exist rf and mo on the observed events
that satisfy the axioms for the release-acquire memory model? The presentation in this section follows [16,7] and introduces these preliminaries.

An *event* is a memory operation: either a read $\mathbf{r}(x, v)$ or write $\mathbf{w}(x, v)$, where $x \in \mathcal{X}$ is a shared memory location and $v \in \mathcal{V}$ is a value that is either read-from or written-to the memory location. These are the analogues of “$read(x, v)$” and “$write(x, v)$” that were used in [10] and recalled in the Introduction. We sometimes use the term *variable* for a memory location. For an event $e$, we write $e.op$, $e.var$ and $e.val$ respectively for the memory operation ($\mathbf{r}$ or $\mathbf{w}$), the shared memory location and the value associated with the event. Events are spread across a set of *threads*. For a set of events $E$, we write $E.R$ and $E.W$ for the set of all read and write events in $E$ respectively, and $E.R_x$, $E.W_x$ for the read and write events involving variable $x$. When the set of events $E$ is clear from the context, we simply write $R_x$ and $W_x$.

**Execution graph.** An *execution graph* [17] (also known as candidate execution [3]) is a tuple $X = (E, \mathit{po}, \mathit{rf}, \mathit{mo})$ where $E$ is a set of events and $\mathit{po}, \mathit{rf}, \mathit{mo}$ are binary relations over $E$. The *program order* $\mathit{po}$ is a partial order that enforces a total order on events of the same thread. The *reads-from relation* $\mathit{rf} \subseteq (E.W \times E.R)$ associates write events $e_1$ to read events $e_2$. It can be seen as an edge $e_1 \xrightarrow{\mathit{rf}} e_2$ from (the node corresponding to) $e_1$ to (the node corresponding to) $e_2$ in the execution graph $X$. Indeed, it must be that $e_1$.var = e_2.var$, $e_1$.val = e_2.val$ and every read event has a unique writer ($\mathit{rf}^{-1}$ is a function). The *modification order* $\mathit{mo} \subseteq (E.W \times E.W)$ is the union of modification orders $\mathit{mo}_x$ for $x \in \mathcal{X}$, where each $\mathit{mo}_x$ is a total order over the set $W_x$ of write events that involve variable $x$. For a read $r$, let $\mathit{rf}^{-1}(r)$ denote the write associated by $\mathit{rf}$ to $r$, in other words, it is the write from which $r$ reads from according to $\mathit{rf}$.

Consistency of an observed execution graph with respect to a weak memory model can be characterized using certain properties of the combination consisting of the $\mathit{po}$, $\mathit{rf}$ and $\mathit{mo}$ relations – these properties are called *consistency axioms*. In this work, we focus on the release-acquire memory model (RA) and its close variants strong release-acquire (SRA) and weak release-acquire (WRA). In Section 2.1, we formally define the consistency axioms. Before that, we state our problem of interest, the analogue of the VSC problem [10] for release-acquire semantics. The problem statement uses the notion of a *partial execution graph* $\bar{X} = (E, \mathit{po})$, which is an abstraction of execution graphs without the modification order and reads-from relation.

VERIFYING WEAK MEMORY CONSISTENCY (The $V\mathcal{M}$-problem)

**Instance:** A partial execution graph $\bar{X} = (E, \mathit{po})$ and a memory model $\mathcal{M} \in \{\text{RA, SRA, WRA}\}$

**Question:** Do there exist $\mathit{rf}$ and $\mathit{mo}$ relations on $E$ such that the complete execution graph $X = (E, \mathit{po}, \mathit{rf}, \mathit{mo})$ satisfies the consistency axioms of the memory model $\mathcal{M}$?
<figure><img src="image_2.png" /><figcaption>Fig. 1: Violations of coherence and causality. Values in the **r** and **w** operations suppressed for clarity. Black edge denotes po: (a) porf-acyclicity is violated (b) write-coherence is violated: w₁(x) **hb** w₂(x) while w₂(x) **mo** w₁(x), (c) read-coherence is violated : w₁(x) **rf** r(x) with w₁(x) **mo** w₂(x) and w₂(x) **hb** r(x), (d) weak-read-coherence is violated : w₁(x) **rf** r(x) with w₁(x) **hb** w₂(x) and w₂(x) **hb** r(x), (e) strong-write-coherence is violated : **hb** ∪ **mo** cycle.</figcaption></figure>

**Notations for Relations.** Let $S$ be a binary relation over the set of events $E$. The reflexive, transitive, reflexive-transitive closures, and inverse relations of $S$ are denoted as $S^?$, $S^+$, $S^*$, $S^{-1}$ respectively. The relation $S$ is *acyclic* if $S^+$ is *irreflexive*. We write $\text{irr}(S)$ and $\text{acy}(S)$ to denote that relation $S$ is *irreflexive* and *acyclic* respectively. The identity relation on a set $B$ is denoted as $[B] : [B](x, y) \triangleq x = y \land x \in B$. The composition of two relations $S_1$ and $S_2$, is denoted by $S_1; S_2$. For a shared variable $x$, we let $S_x = [E_x]; S; [E_x]$ be the restriction of $S$ to all events of $E$ on $x$, with $E_x = \{e \in E | e. \text{var} = x\}$.

**Derived relations.** The *happens-before* relation **hb** is the transitive closure of po and rf. In our descriptions, we view **hb** as a path consisting of $\xrightarrow{po}$ and $\xrightarrow{rf}$ edges. Happens-before (**hb**) projected to an individual variable $x$ is denoted as **hb$_x$**: this will be a path where all the **rf** edges are over the variable $x$. More precisely: **hb** $\triangleq (\text{po} \cup \text{rf})^+$, and **hb$_x$** $\triangleq (\text{po} \cup \text{rf$_x$})^+$. We write **rf$_x$** for the projection of **rf** to variable $x$.

## 2.1 Consistency Axioms

The axioms are broadly classified as *coherence* and *causality cycles*. Table 1 states the axioms and indicates the axioms for each memory model. Figure 1 gives scenarios for violation of the various axioms described below.

**Coherence.** The modification order **mo** enforces an 'SC-per-variable' constraint in any execution $X$, that is, memory accesses per shared variable are totally ordered. Coherence axioms essentially describe rules on the **mo**.

*Write-coherence* enforces that **mo** agrees with **hb** for each variable (denoted as $\text{irr}(\text{mo}_x; \text{hb})$ in Table 1 and a violation of it is shown in Figure 1(b)): intuitively, if a write $w(x, v_1)$ happens-before $w(x, v_2)$, then $x$ is updated to $v_1$ first, and then $v_2$. As the order of updates to $x$ is encoded by the modification order $\text{mo}_x$, the axiom requires $\text{mo}_x$ to align with **hb**. A stronger version of it, called *strong-write-coherence*, requires the entire **mo** (and not just $\text{mo}_x$) to align with **hb**, in other words, it requires the acyclicity of $\text{po} \cup \text{rf} \cup \text{mo}$ – again, notice that this requirement
<table><caption>Table 1: Models WRA, RA, SRA.</caption><tbody><tr><td rowspan="3">WRA</td><td>porf-acyclicity</td><td>irr(<b>mo</b><sub>x</sub>; <b>hb</b>) (write-coherence)</td></tr><tr><td>weak-read-coherence</td><td>irr(<b>rf</b><sup>-1</sup>; <b>mo</b><sub>x</sub>; <b>hb</b>) (read-coherence)</td></tr><tr><td></td><td>acy(<b>hb</b> ∪ <b>mo</b>) (strong-write-coherence)</td></tr><tr><td rowspan="3">RA</td><td>porf-acyclicity</td><td>irr(<b>hb</b>; [<b>W</b><sub>x</sub>]; <b>hb</b>; <b>rf</b><sub>x</sub><sup>-1</sup>) (weak-read-coherence)</td></tr><tr><td>write-coherence</td><td>porf-acyclicity</td></tr><tr><td>read-coherence</td><td>strong-write-coherence</td></tr><tr><td></td><td></td><td>read-coherence</td></tr><tr><td></td><td></td><td></td></tr></tbody></table>

is across variables, as $mo = \bigcup_{x \in X} mo_x$. Execution graph in Figure 1(e) violates strong-write-coherence, while it does not violate write-coherence.

Read coherence enforces that a read $\mathbf{r}(x)$ cannot read from a write $\mathbf{w}_1(x)$ if there is an intermediate write $\mathbf{w}_2(x)$ that happens-before $\mathbf{r}(x)$, i.e. $(\mathbf{w}_2(x), \mathbf{r}(x)) \in \textcolor{blue}{\text{hb}}$ (denoted as $\mathbf{w}_2(x) \xrightarrow{\textcolor{blue}{\text{hb}}} \mathbf{r}(x)$), and “intermediate” refers to mo, i.e., $(\mathbf{w}_1(x), \mathbf{w}_2(x)) \in \textcolor{green}{\text{mo}}$ (denoted as $\mathbf{w}_1(x) \xrightarrow{\textcolor{green}{\text{mo}}} \mathbf{w}_2(x)$). Said differently, if $\mathbf{w}_1(x)$ and $\mathbf{w}_2(x)$ happen-before a read $\mathbf{r}(x)$, then $\mathbf{w}_1 \xrightarrow{\textcolor{green}{\text{mo}}} \mathbf{w}_2$, implies $\mathbf{r}(x)$ cannot read from $\mathbf{w}_1(x)$. The mo relation makes $\mathbf{w}_1$ stale for $\mathbf{r}$. Figure 1(c) shows a violation of read-coherence. In a weaker form of read-coherence called weak-read-coherence [15] (Figure 1(d)), “intermediate” relates to hb (and not mo), i.e., we have $\mathbf{w}_1(x) \xrightarrow{\textcolor{blue}{\text{hb}}} \mathbf{w}_2(x)$: in other words, if two writes $\mathbf{w}_1 \xrightarrow{\textcolor{blue}{\text{hb}}} \mathbf{w}_2 \xrightarrow{\textcolor{blue}{\text{hb}}} \mathbf{r}$, then $\mathbf{r}$ cannot read from $\mathbf{w}_1$.

**Causality cycles.** A causality cycle consists of po and rf orderings. The C11 models explicitly mandate porf-acyclicity [15,20], that is, acy po ∪ rf ) (Figure 1(a)).

An execution graph $X = (E, po, rf, mo)$ is consistent with memory model $\mathcal{M}$ if it satisfies all the axioms corresponding to $\mathcal{M}$ as shown in Table 1. We write $X \models \mathcal{M}$ if $X$ is consistent with $\mathcal{M}$. For a partial execution graph $\bar{X} = (\bar{E}, po)$, we write $\bar{X} \models \mathcal{M}$ if there exists an rf and mo such that $X \models \mathcal{M}$ for the complete execution graph $X = (\bar{E}, po, rf, mo)$. Hence, the VM problem can be stated as: given a partial execution graph $\bar{X}$ and a memory model $\mathcal{M}$, does $\bar{X} \models \mathcal{M}$?

We conclude this section with a useful lemma describing the relationship between these three models.

**Lemma 1.** Let $X = (E, po, rf, mo)$ be an execution graph. Then: $X \models \text{SRA implies } X \models \text{RA}$, and $X \models \text{RA implies } X \models \text{WRA}$.

*Proof.* It is easy to see that if $X$ satisfies strong-write-coherence, then it satisfies write-coherence also. Hence $X \models \text{SRA}$ implies $X \models \text{RA}$. For RA to WRA, we show that if weak-read-coherence is violated, then either read-coherence or write-coherence is violated: suppose weak-read-coherence is violated, there is a cycle
$\mathbf{r}(x) \xrightarrow{\mathrm{rf}^{-1}} \mathbf{w}_1(x) \xrightarrow{\mathrm{hb}} \mathbf{w}_2(x) \xrightarrow{\mathrm{hb}} \mathbf{r}(x)$. The `mo` relation can order $\mathbf{w}_1$ and $\mathbf{w}_2$ in either way. If $\mathbf{w}_1(x) \xrightarrow{\mathrm{mo}} \mathbf{w}_2(x)$, then read-coherence is violated, and if $\mathbf{w}_2(x) \xrightarrow{\mathrm{mo}} \mathbf{w}_1(x)$, then write-coherence is violated. $\square$

### 3 Polynomial-time algorithm for 1-WRITER systems

We now consider programs where, for every variable, there is a single thread which writes to it. Any number of threads can read from a variable. An execution graph $X = (E, \mathrm{po}, \mathrm{rf}, \mathrm{mo})$ is said to be a 1-WRITER execution graph if in the set of events $E$, there is at most one thread writing to every memory location.

**Overview of this section.** The fact that we work with 1-WRITER execution graphs simplifies several axioms of Table 1, allowing for a polynomial-time procedure. Recall however that for sequential consistency, the 1-WRITER assumption offers no specific advantage and still yields a NP-hard complexity [10].

SRA and RA *reduce to WRA*. Firstly, we note that consistency checking for the SRA and RA memory models reduce to checking for WRA in 1-WRITER execution graphs (Lemma 2). Moreover, since all writes of a memory location lie in a single thread, the `mo` relation on writes gets fixed to the unique order that agrees with `po`. Therefore, the problem boils down to detecting if there is an `rf` that satisfies *porf-acyclicity* and *weak-read-coherence*, the two axioms needed for WRA consistency. So we focus on these two axioms for the rest of the section.

A *partial order on rf*. Secondly, since all writes to a memory location $x$ are totally ordered by `po`, there is a natural partial order induced on the `rf` relations. A *reads-from relation* $rf_1$ is said to be smaller than $rf_2$, written as $rf_1 \subseteq rf_2$, if for every read $r$, the write event $w_2 = rf_2^{-1}(r)$ appears *po*-later than $w_1 = rf_1^{-1}(r)$ (we say $w_2$ is *po*-later than $w_1$ if $w_1 \text{ po}^* w_2$). In other words, $rf_2$ associates each read $r$ to a write that appears later in the program order compared to the write that $rf_1$ associates it to. We observe two useful properties of this partial order: (1) if an `rf` violates *porf-acyclicity*, then every $rf^\dagger$ larger than it also violates *porf-acyclicity*, and (2) among all the `rf` that satisfy *weak-read-coherence*, there is a unique minimum element $rf_{\min}$.

*Algorithm*. Using these two properties, we design an algorithm that starts with the smallest `rf` and iteratively computes larger reads-from relations until a WRA-consistent `rf` is found, or concludes that no such `rf` exists.

The first two ideas appear in Section 3.1 and the algorithm is described in Section 3.2.

#### 3.1 Structural properties of 1-WRITER execution graphs

Our first observation is that for 1-WRITER systems, checking SRA and RA reduces to checking WRA. For WRA the only axioms are *porf-acyclicity* and
weak-read-coherence. For RA one must also ensure write-coherence and read-coherence, in addition to porf-acyclicity. In a 1-WRITER setting, write-coherence is enforced by choosing mo to agree with po (so all writes to a location are ordered by the program order of their single writer).

A violating cycle for read-coherence has the form

$$r_x \xrightarrow{rf^{-1}} w_x \xrightarrow{mo_x} w'_x \xrightarrow{hb} r_x.$$

When mo agrees with po, the $mo_x$ edge is simply $po^+$, since both $w_x$ and $w'_x$ are in the same thread. Now, a violating cycle for weak-read-coherence has the form

$$r_x \xrightarrow{rf^{-1}} w_x \xrightarrow{hb} w'_x \xrightarrow{hb} r_x,$$

and, since $w_x$ and $w'_x$ come from the same thread, the $hb$ step between $w_x$ and $w'_x$ can likewise be instantiated by $po^+$. Hence read-coherence coincides with weak-read-coherence in the 1-WRITER setting. Moreover, having an mo agreeing with po reduces strong-write-coherence to porf-acyclicity, culminating in this lemma.

**Lemma 2.** Let $X = \langle E, po, rf, mo \rangle$ be a 1-WRITER execution graph. Then, for $M \in \{SRA, RA\}$, we have $X \models M$ iff mo agrees with po and $X \models WRA$.

As a consequence, the consistency checking of 1-WRITER under SRA, RA and WRA boils down to checking porf-acyclicity and weak-read-coherence violation. Secondly, the problem of synthesizing both rf and mo boils down to just synthesizing rf, since mo is fixed to the order that respects po. Nevertheless, there are still exponentially many rf functions possible. The next lemma entails that there is a “smallest” rf among all WRA-consistent rfs in the $\sqsubseteq$ order on rfs defined in the overview of this section. Given $rf_1, rf_2$, we write $\min(rf_1, rf_2)$ for the reads-from relation which associates every read $r$ to the po-smaller write between $rf_1^{-1}(r)$ and $rf_2^{-1}(r)$.

**Lemma 3.** Let $rf_1$ and $rf_2$ be two reads-from relations over a partial 1-WRITER execution graph $X = \langle E, po, mo \rangle$ s.t. mo agrees with po.

- Suppose $rf_1 \sqsubseteq rf_2$. Then, if $rf_1$ induces a $po \cup rf_1$ cycle, then $rf_2$ induces a $po \cup rf_2$ cycle.

- Suppose both $rf_1$ and $rf_2$ satisfy weak-read-coherence. Then, the rf function $\min(rf_1, rf_2)$ also satisfies weak-read-coherence.

Suppose $S$ is the set of all rf that satisfy weak-read-coherence. The second item of Lemma 3 implies that $S$ contains a unique minimum element, which we denote by $rf_{min}$. By the first item of Lemma 3, if $rf_{min}$ violates porf-acyclicity then every rf in $S$ also violates it. Therefore, WRA-consistency checking reduces to computing $rf_{min}$ and testing it for porf-acyclicity. The algorithm in the next section performs exactly this construction and test.
<figure><img src="image_3.png" /><figcaption>Fig. 2: From left: $rf_0 \sqsubseteq rf_1 \sqsubseteq rf_2$. $rf_0$ has a violation of weak-read-coherence: $r_3 \xrightarrow{rf_0^{-1}} w_1 \xrightarrow{po} w_2 \xrightarrow{hb_0} r_3$. $rf_1$ has a violation of weak-read-coherence: $r_4 \xrightarrow{rf_1^{-1}} w_2 \xrightarrow{po} w_3 \xrightarrow{hb_1} r_4$. $rf_2$ does not have any more violations of weak-read-coherence. porf-acyclicity is also satisfied by $rf_2$. The underlying partial execution graph is WRA-consistent.</figcaption></figure>

## 3.2 Algorithm

Our algorithm starts from an $rf_0$ which maps every read $r$ to the po-smallest write in its writer thread, such that the value of the chosen write matches with that of $r$, and in case the writer thread is the same as the one where $r$ is present, the mapped write lies above $r$. This relation $rf_0$ may not satisfy weak-read-coherence. In that case, a violating cycle is identified and $rf_0$ is modified to $rf_1$ as explained below. Assume we have iteratively constructed upto $rf_i$, and $rf_i$ does not satisfy weak-read-coherence.

From $rf_i$ to $rf_{i+1}$. Pick a violating cycle for weak-read-coherence:

$$r_i \xrightarrow{rf_i^{-1}} w_i \xrightarrow{hb_i} w'_i \xrightarrow{hb_i} r_i$$

where all three events $r_i$, $w_i$, $w'_i$ are over the same variable, say $x_i$, and $hb_i$ is $(po \cup rf_i)^+$. Recall that since we are in the 1-WRITER case, the intermediate $hb_i$ can be replaced with $po^+$. Modify $rf_i$ to eliminate the violating cycle: choose a write for $r_i$ which appears on or after $w'_i$, that is, pick $w''_i$ such that $w'_i \text{ po}^* w''_i$ and $w''_i$ is a write on the same variable $x_i$, writing the same value as the read event $r_i$. If no such write exists, conclude that there is no rf for $\bar{X}$ that satisfies weak-read-coherence. Else, let the resulting rf be called $rf_{i+1}$. If $rf_{i+1}$ does not satisfy weak-read-coherence, we update $rf_{i+1}$ as above. Else, $rf_{i+1}$ satisfies weak-read-coherence. We declare $rf_{\min} = rf_{i+1}$.

<figure><img src="image_4.png" /><figcaption>Fig. 3: From left: $rf_0 \sqsubseteq rf_1$. $rf_0$ has a violation of weak-read-coherence: $r_3 \xrightarrow{rf_0^{-1}} w_1 \xrightarrow{po} w_2 \xrightarrow{hb} r_3$. $rf_1$ has no weak-read-coherence violation but does not satisfy porf-acyclicity: $w_5 \xrightarrow{rf_1} r_3 \xrightarrow{po} w_4 \xrightarrow{rf} r_2 \xrightarrow{po} w_5$. The partial execution graph is not WRA-consistent.</figcaption></figure>
Finally, we test whether $rf_{\min}$ satisfies porf-acyclicity. If it does, we have a witness for WRA-consistency. Else, we conclude (due to Lemma 3) that $\bar{X}$ is not WRA-consistent. We formalize this discussion in Algorithm 1 in Appendix A.2. Here is the key invariant maintained by the algorithm: at each step $i$ where the update function is called on $rf_i$, we can show that $rf_i \subseteq rf^\dagger$ for every $rf^\dagger$ that satisfies weak-read-coherence. Examples 2 and 3 illustrate the running of the algorithm on two different partial execution graphs.

**Theorem 4.** A partial execution graph $\bar{X} = \langle E, \text{po} \rangle$ of a one-writer system is consistent for WRA iff the final rf computed by the procedure discussed above satisfies weak-read-coherence and porf-acyclicity. Moreover, the algorithm runs in time $O(n^3)$ where $n = |E|$ and returns the smallest rf that is WRA-consistent, if one exists.

The major contributor to the complexity of Algorithm 1 is verification of whether a given rf satisfies weak-read-coherence. This can be posed as a graph problem: there are $n$ nodes corresponding to the events, and there are three kinds of edges $\text{po}$, $\text{rf}$ and $\text{rf}^{-1}$; does there exist a cycle of the form $r \xrightarrow{\text{rf}^{-1}} w \xrightarrow{\text{po}^+} w' \xrightarrow{(\text{po}\cup\text{rf})^*} r$? For each read event $r$ and its corresponding write event $w$, we need to check if there exist a $w'$ such that (1) there is a path of $\text{po}$ edges from $w$ to $w'$, and (2) there is a path from $w'$ to $r$ over a combination of $\text{po}$ and $\text{rf}$ edges. For each read, this can be achieved by in $O(n)$ time by a graph search. Hence, overall, across all possible reads, this algorithm takes $O(n^2)$ time. Therefore, each update to an rf costs $O(n^2)$ and there can be at most $n$ updates (as each update moves the write of a read to a po-later write). This gives a complexity of $O(n^3)$. As our next observation, we prove a conditional lower bound of $O(n^{\frac{3}{2}-\epsilon})$ on the time to check for weak-read-coherence in a one-writer program with $n$ events. This also transfers as a lower bound for the WRA-consistency checking. Due to Lemma 2, it also gives a lower bound on the consistency checking for SRA and RA as well. To show the lower bound, we make use of the Boolean Matrix Multiplication hypothesis and a lower bound result on finding triangles in graphs.

*Boolean Matrix Multiplication (BMM) hypothesis.* There is no $O(n^{3-\epsilon})$ algorithm for Boolean Matrix Multiplication, for any $\epsilon > 0$.

**Theorem 5 (Theorem 1.3 of [27]).** Under BMM hypothesis, there is no $O(n^{3-\epsilon})$ algorithm for detecting a triangle in an (undirected) graph with $n$ vertices, for any $\epsilon > 0$.

We reduce triangle detection in a graph with $n$ vertices to weak-read-coherence checking in a 1-WRITER execution graph with $n^2$ events. This results in the following proposition.

**Proposition 6.** Under BMM, for any $\epsilon > 0$, there is no $O(n^{\frac{3}{2}-\epsilon})$ algorithm for deciding if a given 1-WRITER execution graph $X = \langle E, \text{po}, \text{rf}, \text{mo} \rangle$ satisfies the weak-read-coherence axiom.
Given graph $G = (V_G, E_G)$ with $n$ vertices, we build an execution graph $\bar{X}_G = \langle \mathbf{E}, \mathbf{po} \rangle$ of a single-writer program with $n^2$ events, such that $\bar{X}$ is consistent w.r.t. $\mathcal{M}$ for iff $G$ has no triangles. Therefore, if the consistency problem can be solved in $O(n^{\frac{3}{2}-\epsilon})$ for some $\epsilon$, we can solve triangle detection on $n$-node graphs in $O((n^2)^{\frac{3}{2}-\epsilon}) = O(n^{3-\frac{5}{2}})$, contradicting the BMM hypothesis.

Our idea for the reduction is as follows. We will construct $\bar{X}$ in such a way that for every $\mathbf{r}(x, v)$ there is a unique $\mathbf{w}(x, v)$ present in the entire program. Therefore, the rf relation is fixed. If $G$ has a triangle, we will have a shared variable $a$ and a cycle of the form: $\mathbf{w}(a, 0) \xrightarrow{\text{po}} \mathbf{w}(a, 1) \xrightarrow{\text{hb}} \mathbf{r}(a, 0) \xrightarrow{\text{rf}^{-1}} \mathbf{w}(a, 0)$. This cycle violates weak-read-coherence. If $\bar{X}$ with the fixed rf violates weak-read-coherence, then $G$ has a triangle. The hb path $\mathbf{w}(a, 1) \xrightarrow{\text{hb}} \mathbf{r}(a, 0)$ should reflect the presence of a triangle in $G$.

<figure><img src="image_5.png" /><figcaption>Fig. 4: From triangles to violations of weak-read-coherence</figcaption></figure>

The key aspect of the construction is depicted in Figure 4. Suppose $G$ contains a triangle over vertices $x, y, z$. We consider a variable $a_x$ for which we extract an **hb** path as above. To force the **hb** path to have length 3, we consider four copies $t_{a_x}, t_{b_x}, t_{c_x}, t_{d_x}$ for each vertex $x$. When there is edge $(x, y)$, thread $t_{a_x}$ writes to $t_{b_y}$. Similarly, $(y, z)$ makes $t_{b_y}$ write to $t_{c_x}$ and finally the edge $(z, x)$ makes $t_{c_x}$ write to $t_{d_x}$ which contains $\mathbf{r}(a_x, 0)$. The full construction is explained in Appendix A.3.

# 4 Hardness in the presence of multiple writers

While having a single writer per location induced a polynomial-time algorithm for the consistency check, we show that having two writers per thread makes the problem NP-complete. The NP upper bound follows by guessing an rf and mo and then checking whether the complete execution graph $X = \langle \mathbf{E}, \mathbf{po}, \mathbf{rf}, \mathbf{mo} \rangle$ satisfies the consistency axioms. When rf and mo are already given, this test can be done in polynomial-time [26]. Hence the NP upper bound follows. The hardness for our $\mathcal{V}\mathcal{M}$ problem comes from the fact that we need to * synthesize* suitable rf and mo (the analogue in the sequential consistency setting would be the synthesis of an interleaving). For proving hardness, we provide a reduction from 3-CNF-SAT: given a boolean formula $\varphi$ over $k$ variables and $m$ clauses, with each clause being a disjunction of three literals, is there a satisfying assignment for $\varphi$? We provide two reductions.

1. Formula $\varphi$ to a partial execution graph $\bar{X}_{\varphi}$ with $O(k)$ threads, and containing at most three threads writing to a location (3-WRITER).
2. Formula $\varphi$ to a partial execution graph $\bar{Y}_{\varphi}$ with $O(k+m)$ threads, and containing at most two threads writing to a location (2-WRITER).

In both the reductions, we achieve the property that $\varphi$ is satisfiable iff $\bar{X}_{\varphi}$ and $\bar{Y}_{\varphi}$ are $M$-consistent, for $M \in \{\text{SRA}, \text{RA}, \text{WRA}\}$. This shows that the consistency checking problem is NP-complete with a bounded number of writers per location, in fact, even with two writers. The reason we present the first reduction to 3-WRITER is because we get a stronger conditional bound: since the number of threads in $\bar{X}_{\varphi}$ is linearly related to the number of variables in $\varphi$, we get a parameterized reduction that helps proving a conditional lower bound under the Exponential Time Hypothesis (ETH). In the reduction to 2-WRITER systems, the number of threads depends both on $k$ (number of variables in the formula) and $m$ (the number of clauses). Hence this reduction cannot be used for the conditional lower bound. We will first describe the reduction to three writers and its implications, and then follow up with the second reduction.

*Notation.* Let the variables used by $\varphi$ be $x_1, \dots, x_k$. The clauses are $C_1, \dots, C_m$. Each clause $C_j$ consists of three literals ($\ell_j^1, \ell_j^2, \ell_j^3$), where each literal is either a variable $x_i$ or its negation $\neg x_i$. We define $S_{x_i} := \{j \mid C_j \text{ contains } x_i\}$ and $S_{\neg x_i} := \{j \mid C_j \text{ contains } \neg x_i\}$ as the set of (indices of) clauses containing the literals $x_i$ and $\neg x_i$ respectively.

## 4.1 Reduction to 3-WRITER systems

We consider execution graphs where for each variable $x$ there are at most three threads writing to $x$, that is, at most three threads can have statements of the form $w(x, d)$. We will call them 3-WRITER execution graphs. Our objective is to show a hardness result stronger than NP-hardness, for the $VM$ problem under the assumption stated below.

**Exponential Time Hypothesis (ETH).** There is no $2^{o(k)} \cdot (k+m)^{O(1)}$ algorithm for 3-CNF-SAT, where $k$ is the number of variables, $m$ is the number of clauses [11,19].

We prove the following theorem in this section.

**Theorem 7.** *Under ETH, there is no $2^{o(k)} \cdot n^{O(1)}$ algorithm for the $VM$-problem with $M \in \{\text{SRA}, \text{RA}, \text{WRA}\}$, $k$ being the number of threads, and $n$ the number of events. The result holds even while restricting the input instance to 3-WRITER execution graphs.*

*Proof strategy.* Given a 3-CNF formula $\varphi$ with $k$ threads and $m$ clauses, we construct a partial execution graph $\bar{X}_{\varphi} = \langle E, \rho_0 \rangle$ that satisfies the following properties:

- $\bar{X}_{\varphi}$ is 3-WRITER,

- the number of threads in $\bar{X}_{\varphi}$ is $O(k)$,
- the number of events in $\bar{X}_{\varphi}$ is $O(k+m)$,

- $\bar{X}_{\varphi} \models \mathcal{M}$ iff $\varphi$ is satisfiable, for $\mathcal{M} \in \{\text{SRA}, \text{RA}, \text{WRA}\}$.

Thus, if there was a $2^{o(k)} \cdot n^{O(1)}$ algorithm for the $\mathcal{V}\mathcal{M}$ problem, we could solve 3-CNF-SAT in $2^{o(k)} \cdot (k+m)^{O(1)}$ time: from $\varphi$, construct the $\mathcal{V}\mathcal{M}$ instance in $O(k+m)$ time, and then use the $2^{o(k)} \cdot (k+m)^{O(1)}$ procedure for $\mathcal{V}\mathcal{M}$, thereby contradicting ETH. To show the last item above, we make use of what is known in the literature as a *range reduction* [7]: using Lemma 1, it is enough to show that if $\varphi$ has a satisfying assignment, then $\bar{X} \models \text{SRA}$, and if $\varphi$ does not have a satisfying assignment, then $\bar{X} \not\models \text{WRA}$.

**The reduction.** For every variable $x_i$, we introduce four threads $T_i^1$, $T_i^0$, $T_{x_i}$ and $T_{\neg x_i}$, as shown in Figure 5. Apart from these, there is a special thread $T_f$. A concrete example of the reduction is presented in Appendix B.1.

$$ \begin{array}{c|c} T_i^1 & T_i^0 \\ \mathbf{w}(s_i, 1) & \mathbf{w}(s_i, 1) \\ \mathbf{w}(s_i, 2) & \mathbf{w}(s_i, 2) \\ \mathbf{w}(v_i, 1) & \mathbf{w}(v_i, 0) \end{array} $$

$$ \begin{array}{c|c|c} T_{x_i} & T_{\neg x_i} & T_f \\ \mathbf{r}(v_i, 1) & \mathbf{r}(v_i, 0) & \mathbf{r}(c_1, 1) \\ \mathbf{w}(c_j, 1) & \mathbf{w}(c_j, 1) & \mathbf{r}(c_m, 1) \\ \forall j \in S_{x_i} & \forall j \in S_{\neg x_i} & \mathbf{r}(s_1, 2) \\ & & \mathbf{r}(s_1, 1) \\ & & \mathbf{r}(s_k, 2) \\ & & \mathbf{r}(s_k, 1) \end{array} $$

<caption>Fig. 5: Threads in the reduction, for $i \in \{1, 2, \dots, k\}$</caption>

Here is an intuitive description of the reduction. The statements $\mathbf{w}(v_i, 1)$ and $\mathbf{w}(v_i, 0)$ in $T_i^1$ and $T_i^0$ encode variable $x_i$ being set to true and false respectively. Thread $T_{x_i}$ has a read statement $\mathbf{r}(v_i, 1)$ (reading true for $x_i$) and sets all clauses containing $x_i$ to true, using the statement $\mathbf{w}(c_j, 1)$ for all $j \in S_{x_i}$. Similarly, thread $T_{\neg x_i}$ reads $\mathbf{r}(v_i, 0)$ (false for $x_i$) and sets all clauses containing $\neg x_i$ to true. Finally the thread $T_f$ needs to make sure that all clauses are set to true, hence the read statements $\mathbf{r}(c_1, 1), \dots, \mathbf{r}(c_m, 1)$. The main challenge is to encode a valid assignment, where every variable is assigned a unique truth value: to do this, we need to ensure that there are no two distinct reads $\mathbf{r}(c_j, 1)$ and $\mathbf{r}(c_l, 1)$ in $T_f$ which read from some $T_{x_i}$ and its negation $T_{\neg x_i}$. This is where the rest of the statements, using $s_i$ become useful, as we elaborate in the proofs below.

**Lemma 8.** If $\bar{X}_{\varphi} \models \text{WRA}$, then $\varphi$ has a satisfying assignment.

*Proof.* If $\bar{X}_{\varphi} \models \text{WRA}$ there is an rf function which satisfies porf-acyclicity and weak-read-coherence. We need to prove that this rf encodes a valid satisfying assignment. This can be shown by proving that there are no two distinct reads $\mathbf{r}(c_j, 1)$ and $\mathbf{r}(c_l, 1)$ which read from $T_{x_i}$ and $T_{\neg x_i}$ for some variable $x_i$, since it gives the following assignment: $A(x_i) = \text{true}$ if some read event $\mathbf{r}(c_j, 1)$ reads
from the write in $T_{x_i}$; $A(x_i) = \text{false}$ otherwise. Moreover, the assignment $A$ is
satisfying since every clause is made true by this assignment.

Let us now prove the property. Suppose $\mathbf{r}(c_j, 1)$ and $\mathbf{r}(c_\ell, 1)$ read from $T_{x_i}$ and $T_{\neg x_i}$ respectively. Since $\mathbf{r}(c_j, 1)$ reads from $T_{x_i}$, there is an **hb** path from $T_i^1$ to $\mathbf{r}(c_j, 1)$ due to the **rf** edges: $\mathbf{w}(v_i, 1) \xrightarrow{\mathrm{rf}} \mathbf{r}(v_i, 1)$ and $T_{x_i} : \mathbf{w}(c_j, 1) \xrightarrow{\mathrm{rf}} \mathbf{r}(c_j, 1)$. Similarly, there is an **hb** path from $T_i^0$ to $\mathbf{r}(c_\ell, 1)$. Hence there is an **hb** path from both $T_i^1$ and $T_i^0$ to the event $\mathbf{r}(s_i, 1)$ in $T_f$. Since the only matching write $\mathbf{w}(s_i, 1)$ appears above $\mathbf{w}(s_i, 2)$ in these threads, any assignment to $\mathbf{r}(s_i, 1)$ violates weak-read-coherence, a contradiction to the hypothesis that **rf** satisfies weak-read-coherence. $\square$

**Lemma 9.** If $\varphi$ has a satisfying assignment, then $\bar{X}_{\varphi} \models \text{SRA}$.

*Proof.* Suppose $\varphi$ has a satisfying assignment $A$. We need to synthesize **rf** and **mo** such that the resulting execution graph satisfies porf-acyclicity, strong-write-coherence and strong-read-coherence. Since $A$ is a satisfying assignment, for every clause $C_j$ there is a literal $\ell_j$ that is made true. Let $\mathrm{rf}^{-1}(\mathbf{r}(c_j, 1))$ be the write event $\mathbf{w}(c_j, 1)$ in $T_{\ell_j}$. Assigning writes this way introduces an **hb** path from $T_i^{\neg A(x_i)}$ to $T_f$ for all variables that are indeed being utilized to make the clauses true. Importantly, there is no **hb** path created from $T_i^{\neg A(x_i)}$ to the thread $T_f$. Therefore, the read event $\mathbf{r}(s_i, 2)$ can read from the write in $T_i^{\neg A(x_i)}$ and $\mathbf{r}(s_i, 1)$ can read from the unused thread $T_i^{\neg A(x_i)}$. This gives an **rf** which satisfies weak-read-coherence. By design of the execution graph, the **rf** also satisfies porf-acyclicity. For the lemma, we require to prove strong-write-coherence and read-coherence. For this we need to also synthesize an **mo**. Consider any **mo** relation that respects the following orders:

$$- T_i^{\neg A(x_i)} : \mathbf{w}(s_i, 1) \xrightarrow{\text{mo}} T_i^{\neg A(x_i)} : \mathbf{w}(s_i, 1) \xrightarrow{\text{mo}} T_i^{\neg A(x_i)} : \mathbf{w}(s_i, 2) \xrightarrow{\text{mo}} T_i^{\neg A(x_i)} : \mathbf{w}(s_i, 2),$$

- For each clause $j$ there are three threads writing $\mathbf{w}(c_j, 1)$. For each clause $C_j$ choose a specific literal $\ell_j$ that is made true by the satisfying assignment $A$. The **mo** relation orders the other write statements $\mathbf{w}(c_j, 1)$ before $T_{\ell_j} : \mathbf{w}(c_j, 1)$.

It can be shown that the constructed **rf** and **mo** satisfy strong-write-coherence and read-coherence (see Appendix B for the full proof). $\square$

## 4.2 Reduction to 2-WRITER systems

The reduction in Section 4.1 involved 3-WRITER systems. Mainly, each clause variable $c_j$ was written by three threads corresponding to its three literals. Here, our objective is to prove hardness even when there are atmost two threads writing to each variable. We will now reduce 3-CNF-SAT to the consistency testing problem for 2-WRITER systems. However, in this reduction, a formula $\varphi$ with $k$ threads and $m$ clauses yields an execution graph with $\mathcal{O}(k+m)$ threads. While
this still proves NP-hardness, it does not give the stronger hardness under ETH,
parameterized by the number of threads.

**Theorem 10.** The VM problem is NP-complete for $\mathcal{M} \in \{\text{SRA}, \text{RA}, \text{WRA}\}$, even when restricted to 2-WRITER execution graphs.

The key challenge in proving the hardness is to reduce the number of threads writing to each clause variable $c_j$ from three (one for each literal in the clause) to at most two, while still encoding the satisfiability of the 3-CNF formula. This can be achieved by introducing one auxiliary variable $d_j$ per clause. Suppose $C_j = (\ell_j^1 \lor \ell_j^2 \lor \ell_j^3)$. In all the reductions of Section 4.1, there are three threads $T_{\ell_j^1}, T_{\ell_j^2}$ and $T_{\ell_j^3}$. We make the following changes to constructions of $\bar{X}_{\varphi}$ in Section 4.1.

- Replace $w(c_j, 1)$ in $T_{\ell_j^3}$ with $w(d_j, 1)$, i.e., in the third literal, the write is on $d_j$.

- Add a new thread $T_j$ with two events as follows: $\mathbf{r}(c_j, 1)$; $w(d_j, 1)$

- Finally, in $T_f$, replace all $\mathbf{r}(c_j, 1)$ with $\mathbf{r}(d_j, 1)$

Notice that due to the introduction of the new threads $T_j$, the total number of threads also depends on the number of clauses $m$. Let the resulting partial execution graph be called $\bar{Y}_{\varphi}$. In Appendix B.3 we prove the correctness of the reduction.

# 5 Conclusion

Testing shared memory implementations is a key problem in concurrency, whose computational foundations have been laid by the work of [10] for sequential consistency. Ever since, the work has been applied to various other memory models and also used in stateless model-checking algorithms for concurrent programs. We have contributed to the study of this problem under the release-acquire semantics. We have presented a trichotomy of the landscape, with 1-WRITER solved in polynomial-time, 2-WRITER being NP-complete, and 3-WRITER having a stronger lower bound under the Exponential-Time-Hypothesis (ETH). Our presentation works for RA and its close variants SRA and WRA.

A milder variant of the problem studies the complexity when the reads-from relation *rf* is also given. Then the question is to synthesize an *mo* such that the axioms can be satisfied. This “rf-given” problem can be solved in polynomial-time [26], under no restrictions on the execution graphs. When *rf* is not provided apriori, while the general problem is known to be NP-hard [7], no subclass or bounded variant with a polynomial-time algorithm is known in the literature (to the best of our knowledge). We have shown that the 1-WRITER subclass lends itself to a polynomial-time algorithm.

Our results can also be extended to the memory model called Relaxed, whose consistency axioms are a relaxed version of write-coherence and read-coherence,
where essentially *hb* is replaced with *po*. This makes the consistency check easier for the 1-WRITER algorithm. For the hardness, we need to make small changes, but we still obtain the same trichotomy of results. Appendix C provides the details. Another set of memory models that are closely related w.r.t the analysis techniques are the models CC, CM and CCv coming from distributed databases. It is known that CC coincides with WRA while CCv coincides with SRA [15]. Some care needs to be taken for CM, but yet again, we get the same trichotomy of results. Appendix D has the details.

Adapting these complexity theoretic insights to improve algorithmics for the
verification of concurrent programs under the release-acquire semantics, is one
direction for future work.

References

1. Agarwal, P., Chatterjee, K., Pathak, S., Pavlogiannis, A., Toman, V.: Stateless model checking under a reads-value-from equivalence. In: CAV (1). Lecture Notes in Computer Science, vol. 12759, pp. 341–366. Springer (2021)

2. Ahamad, M., Neiger, G., Burns, J.E., Kohli, P., Hutto, P.W.: Causal memory: Definitions, implementation, and programming. Distrib. Comput. 9(1), 37–49 (mar 1995). https://doi.org/10.1007/BF01784241, https://doi.org/10.1007/BF01784241

3. Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: POPL'11. pp. 55–66. ACM (2011). https://doi.org/10.1145/1926385.1926394

4. Bouajjani, A., Enea, C., Guerraoui, R., Hamza, J.: On verifying causal consistency. In: POPL. pp. 626–638. ACM (2017)

5. Bui, T.L., Chatterjee, K., Gautam, T., Pavlogiannis, A., Toman, V.: The reads-from equivalence for the tso and pso memory models. Proceedings of the ACM on Programming Languages 5 (OOPSLA), 1–30 (2021)

6. Burckhardt, S.: Principles of Eventual Consistency. Foundations and Trends in Programming Languages 1(1-2), 1–150 (2014). https://doi.org/10.1561/2500000011

7. Chakraborty, S., Krishna, S.N., Mathur, U., Pavlogiannis, A.: How hard is weak-memory testing? Proc. ACM Program. Lang. 8 (POPL), 1978–2009 (2024)

8. Chen, Y., Lv, Y., Hu, W., Chen, T., Shen, H., Wang, P., Pan, H.: Fast complete memory consistency verification. In: HPCA. pp. 381–392. IEEE Computer Society (2009)

9. Chini, P., Saivasan, P.: A framework for consistency algorithms. In: Saxena, N., Simon, S. (eds.) 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2020, December 14-18, 2020, BITS Pilani, K K Birla Goa Campus, Goa, India (Virtual Conference). LIPIcs, vol. 182, pp. 42:1–42:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020). https://doi.org/10.4230/LIPICS.FSTTCS.2020.42, https://doi.org/10.4230/LIPICS.FSTTCS.2020.42

10. Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comput. 26(4), 1208–1244 (1997)

11. Impagliazzo, R., Paturi, R., Zane, F.: Which problems have strongly exponential complexity? J. Comput. Syst. Sci. 63(4), 512–530 (2001)
12. JáJá, J.: An Introduction to Parallel Algorithms. Addison-Wesley (1992)

13. Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for c/c++ concurrency. Proc. ACM Program. Lang. 2(POPL) (Dec 2017). https://doi.org/10.1145/3158105, https://doi.org/10.1145/3158105

14. Kokologiannakis, M., Lahav, O., Vafeiadis, V.: Kater: Automating weak memory model metatheory and consistency checking. Proc. ACM Program. Lang. 7(POPL) (Jan 2023). https://doi.org/10.1145/3571212, https://doi.org/10.1145/3571212

15. Lahav, O., Boker, U.: What's decidable about causally consistent shared memory? ACM Trans. Program. Lang. Syst. 44(2) (apr 2022). https://doi.org/10.1145/3505273

16. Lahav, O., Boker, U.: What's decidable about causally consistent shared memory? ACM Trans. Program. Lang. Syst. 44(2), 8:1-8:55 (2022). https://doi.org/10.1145/3505273, https://doi.org/10.1145/3505273

17. Lahav, O., Vafeiadis, V., Kang, J., Hur, C.K., Dreyer, D.: Repairing sequential consistency in C/C++11. In: PLDI 2017. pp. 618-632 (2017). https://doi.org/10.1145/3062341.3062352, technical Appendix Available at https://plv.mpi-sws.org/scfix/full.pdf

18. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558-565 (1978)

19. Lokshtanov, D., Marx, D., Saurabh, S.: Lower bounds based on the exponential time hypothesis. Bull. EATCS 105, 41-72 (2011), http://eatcs.org/beatcs/index.php/beatcs/article/view/92

20. Luo, W., Demsky, B.: C11Tester: A Race Detector for C/C++ Atomics, pp. 630-646. Association for Computing Machinery, New York, NY, USA (2021). https://doi.org/10.1145/3445814.3446711

21. Manovit, C., Hangal, S.: Completely verifying memory consistency of test program executions. In: HPCA. pp. 166-175. IEEE Computer Society (2006)

22. Margalit, R., Lahav, O.: Verifying observational robustness against a c11-style memory model. Proc. ACM Program. Lang. 5(POPL) (Jan 2021). https://doi.org/10.1145/3434285, https://doi.org/10.1145/3434285

23. Mathur, U., Pavlogiannis, A., Viswanathan, M.: The complexity of dynamic data race prediction. In: LICS. pp. 713-727. ACM (2020)

24. Norris, B., Demsky, B.: 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. p. 131-150. OOPSLA '13, Association for Computing Machinery, New York, NY, USA (2013). https://doi.org/10.1145/2509136.2509514, https://doi.org/10.1145/2509136.2509514

25. Qadeer, S.: Verifying sequential consistency on shared-memory multiprocessors by model checking. IEEE Trans. Parallel Distributed Syst. 14(8), 730-741 (2003)

26. Tunç, H.C., Abdulla, P.A., Chakraborty, S., Krishna, S., Mathur, U., Pavlogiannis, A.: Optimal reads-from consistency checking for c11-style memory models. Proc. ACM Program. Lang. 7(PLDI) (jun 2023). https://doi.org/10.1145/3591251, https://doi.org/10.1145/3591251

27. Vassilevska Williams, V., Williams, R.R.: Subcubic equivalences between path, matrix, and triangle problems. J. ACM 65(5), 27:1-27:38 (2018)
# A Appendix for Section 3

## A.1 Proofs of Section 3.1

**Lemma 2.** Let $X = \langle E, \text{po}, \text{rf}, \text{mo} \rangle$ be a 1-WRITER execution graph. Then, for $M \in \{\text{SRA}, \text{RA}\}$, we have $X \models M$ iff `mo` agrees with `po` and $X \models WRA$.

*Proof.* Let us begin with $M = \text{RA}$. For $X$ to be consistent with $\text{RA}$, it has to satisfy the three axioms: porf-acyclicity, write-coherence and read-coherence (see Table 1). In a 1-WRITER system, for `mo` edges, both its source and target are in the same thread. Therefore, to satisfy write-coherence, `mo` should agree with `po`: in other words, if $w_1 \text{mo}_x w_2$, then $w_1 \text{po}^+ w_2$. Hence, notice that to prove the lemma, it is sufficient to show that the read-coherence axiom and weak-read-coherence axiom coincide for 1-WRITER. A violating cycle for read-coherence is of the form

$$r \xrightarrow{\text{rf}} w_1 \xrightarrow{\text{mo}_x} w_2 \xrightarrow{\text{hb}} r$$

As seen above the `mo_x` edge is simply `po^+`, hence $w_1 \xrightarrow{\text{mo}_x} w_2$ can be replaced with $w_1 \xrightarrow{\text{po}^+} w_2$. A violating cycle for weak-read-coherence is of the form

$$r \xrightarrow{\text{rf}} w_1 \xrightarrow{\text{hb}} w_2 \xrightarrow{\text{hb}} r$$

with $w_1$ and $w_2$ being writes on the same variable $x$. Since the writes are on the same variable, $w_1 \xrightarrow{\text{hb}} w_2$ can be replaced with $w_1 \xrightarrow{\text{po}^+} w_2$. This proves that the violating cycles for both the axioms coincide for 1-WRITER systems.

Now, let $M = \text{SRA}$. For strong-write-coherence to be true, we require `mo` to agree with `po`. If $X \models \text{SRA}$, then the axioms porf-acyclicity, strong-write-coherence and read-coherence are true. Since strong-write-coherence holds, `mo` needs to agree with `po`. We have shown above that read-coherence coincides with weak-read-coherence, when `mo` agrees with `po`. Hence $X \models WRA$. Now, for the other direction. Suppose `mo` agrees with `po` and weak-read-coherence are true. From above, we deduce read-coherence holds. If strong-write-coherence is violated, then there will be a porf-cycle, a contradiction. Hence, the lemma follows for $M = \text{SRA}$. $\square$

**Lemma 3.** Let $\text{rf}_1$ and $\text{rf}_2$ be two reads-from relations over a partial 1-WRITER execution graph $X = \langle E, \text{po}, \text{mo} \rangle$ s.t. `mo` agrees with `po`.

- Suppose $\text{rf}_1 \sqsubseteq \text{rf}_2$. Then, if $\text{rf}_1$ induces a $\text{po} \cup \text{rf}_1$ cycle, then $\text{rf}_2$ induces a $\text{po} \cup \text{rf}_2$ cycle.

- Suppose both $\text{rf}_1$ and $\text{rf}_2$ satisfy weak-read-coherence. Then, the $\text{rf}$ function $\min(\text{rf}_1, \text{rf}_2)$ also satisfies weak-read-coherence.

*Proof.* For the first item, suppose $\text{rf}_1$ induces a porf-cycle of the form:

$$e_1 \xrightarrow{\text{rf}_1} f_1 \xrightarrow{\text{po}} e_2 \xrightarrow{\text{rf}_1} f_2 \cdots e_m \xrightarrow{\text{rf}_1} f_m \xrightarrow{\text{po}} e_1$$
Notice that each $e_i$ is a write event and $f_i$ is a read event such that $e_i = rf_1(f_i)$. Since $rf_1 \sqsubseteq rf_2$, we know $rf_1(f_i) \xrightarrow{po^*} rf_2(f_i)$. Hence: $e_i \xrightarrow{po^*} e'_i$ where $e'_i = rf_2(f_i)$. This gives the following $po \cup rf_2$ cycle:

$$e_1 \xrightarrow{po^*} e'_1 \xrightarrow{rf_2} f_1 \xrightarrow{po} e_2 \xrightarrow{po^*} e'_2 \xrightarrow{rf_2} f_2 \cdots e_m \xrightarrow{po^*} e'_m \xrightarrow{rf_2} f_m \xrightarrow{po} e_1$$

This proves the first item.

For the second item, denote $rf_0 = \min(rf_1, rf_2)$. We will show that if $rf_0$ violates weak-read-coherence, then either $rf_1$ or $rf_2$ violates it. Suppose $rf_0$ induces a violation of weak-read-coherence. There is a cycle of the form:

$$r \xrightarrow{rf_0^{-1}} w \xrightarrow{po^+} w' \xrightarrow{hb_0} r$$

where both $w$ and $w'$ are on the same variable, and hence the edge between them is $po^+$. By definition, either $rf_1$ or $rf_2$ associates $r$ to $w$. Let us say $rf_1(r) = w$. If we show $w'hb_0r$ then we are done. Since $w'hb_0r$, there is a path with $po$ and $rf_0$ edges from $w'$ to $r$:

$$w' \xrightarrow{po^*} e_1 \xrightarrow{rf_0} f_1 \xrightarrow{po^*} e_2 \xrightarrow{rf_0} f_2 \cdots e_m \xrightarrow{rf_0} f_m \xrightarrow{po^*} r$$

We will now form a $po \cup rf_1$ path from $w'$ to $r$. For each $e_i \xrightarrow{rf_0} f_i$, either $e_i \xrightarrow{rf_1} f_i$ too, in which case we retain that edge. If not, by construction of $rf_0$, we know that $e_i \xrightarrow{rf_2} f_i$ and $e_i po^* rf_1(f_i)$. Replace $e_i \xrightarrow{rf_0} f_i$ by the sequene $e_i po^* rf_1(f_i) \xrightarrow{rf_1} f_i$ as in the proof of the first item, to deduce an $hb_1$ path from $w'$ to $r$. This shows that there is a violating cycle for weak-read-coherence induced by $rf_1$ too, thereby proving the second item. $\square$

## A.2 Algorithm

**Theorem 4.** A partial execution graph $\bar{X} = \langle E, po \rangle$ of a one-writer system is consistent for WRA iff the final rf computed by the procedure discussed above satisfies weak-read-coherence and porf-acyclicity. Moreover, the algorithm runs in time $O(n^3)$ where $n = |E|$ and returns the smallest rf that is WRA-consistent, if one exists.

*Proof.* Let $rf_0$ be the initial rf function assigned by Line 2 of the algorithm. Notice that if `Initialize` executes either Line 16 or 20, then there is a read for which no write can be assigned, and hence there is no rf function at all, and there is nothing more to prove. Let us assume `Initialize` returns an rf function $rf_0$.

Let $rf_i$ be the rf function assigned by the $i^{th}$ call to the `Update` function in Line 4. Let us assume that in the call to `Update`($\bar{X}$, $rf_i$), a read event $r_i$'s write changes from $w_i$ to $w_i''$, to result in $rf_{i+1}$. By construction, $rf_{i+1}$ differs from $rf_i$ only at $r_i$. Furthermore, the `Update` function ensures that $w_i po^+ w_i''$ (Lines 28 and 32).
<table><caption>**Algorithm 1:** WRA-consistency checking in 1-WRITER systems</caption><thead><tr><th></th><th></th></tr></thead><tbody><tr><td>1</td><td>Function CheckConsistency(X&#773;):</td></tr><tr><td>2</td><td>rf &larr; Initialize(X&#773;)</td></tr><tr><td>3</td><td>while rf violates weak-read-coherence do</td></tr><tr><td>4</td><td>&nbsp;&nbsp;&nbsp;&nbsp;rf &larr; Update(X&#773;, rf)</td></tr><tr><td>5</td><td>&nbsp;&nbsp;&nbsp;&nbsp;/* Now rf = rf<sub>min</sub> */</td></tr><tr><td>6</td><td>if rf satisfies porf-acyclicity then</td></tr><tr><td>6</td><td>&nbsp;&nbsp;&nbsp;&nbsp;return X&#773; is WRA-consistent</td></tr><tr><td>7</td><td>else</td></tr><tr><td>8</td><td>&nbsp;&nbsp;&nbsp;&nbsp;return X&#773; is not WRA-consistent</td></tr><tr><td>9</td><td>Function Initialize(X&#773;):</td></tr><tr><td>10</td><td>&nbsp;&nbsp;&nbsp;&nbsp;for each read r = r(x, v) do</td></tr><tr><td>11</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;t &larr; thread containing r</td></tr><tr><td>12</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;t<sub>x</sub> &larr; writer thread for x</td></tr><tr><td>13</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if t &ne; t<sub>x</sub> then</td></tr><tr><td>14</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;rf<sub>0</sub><sup>-1</sup>(r) &larr; po-smallest write w of the form w(x, v) in t<sub>x</sub></td></tr><tr><td>15</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if there is no such write then</td></tr><tr><td>16</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return X&#773; is not WRA-consistent</td></tr><tr><td>17</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if t = t<sub>x</sub> then</td></tr><tr><td>18</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;rf<sub>0</sub><sup>-1</sup>(r) &larr; po-smallest write w of the form w(x, v) in t<sub>x</sub> s.t. w po<sup>+</sup>r</td></tr><tr><td>19</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if there is no such write then</td></tr><tr><td>20</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return X&#773; is not WRA-consistent</td></tr><tr><td>21</td><td>&nbsp;&nbsp;&nbsp;&nbsp;return rf<sub>0</sub></td></tr><tr><td>22</td><td>Function Update(X&#773;, rf<sub>i</sub>):</td></tr><tr><td>23</td><td>&nbsp;&nbsp;&nbsp;&nbsp;Pick a cycle violating weak-read-coherence: r<sub>i</sub> &rarr; w<sub>i</sub> &rarr; w'<sub>i</sub> &rarr; r<sub>i</sub></td></tr><tr><td>24</td><td>Let r<sub>i</sub> = r(x, v), w<sub>i</sub> = w(x, v), w'<sub>i</sub> = w(x, v')</td></tr><tr><td>25</td><td>t &larr; thread of r<sub>i</sub></td></tr><tr><td>26</td><td>t<sub>x</sub> &larr; writer thread of variable x</td></tr><tr><td>27</td><td>if t &ne; t<sub>x</sub> then</td></tr><tr><td>28</td><td>&nbsp;&nbsp;&nbsp;&nbsp;rf<sub>i+1</sub><sup>-1</sup>(r<sub>i</sub>) &larr; po-smallest write w''<sub>i</sub> of the form w(x, v) in t<sub>x</sub> s.t.<br/>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;w'<sub>i</sub> po * w''<sub>i</sub></td></tr><tr><td>29</td><td>&nbsp;&nbsp;&nbsp;&nbsp;if there is no such write then</td></tr><tr><td>30</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return X&#773; is not WRA-consistent</td></tr><tr><td>31</td><td>if t = t<sub>x</sub> then</td></tr><tr><td>32</td><td>&nbsp;&nbsp;&nbsp;&nbsp;rf<sub>i+1</sub><sup>-1</sup>(r<sub>i</sub>) &larr; po-smallest write w''<sub>i</sub> of the form w(x, v) in t<sub>x</sub> s.t.<br/>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;w'<sub>i</sub> po * w''<sub>i</sub> po<sup>+</sup>r<sub>i</sub></td></tr><tr><td>33</td><td>&nbsp;&nbsp;&nbsp;&nbsp;if there is no such write then</td></tr><tr><td>34</td><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return X&#773; is not WRA-consistent</td></tr><tr><td>35</td><td>rf<sub>i+1</sub><sup>-1</sup>(r') &larr; rf<sub>i</sub>(r') for all r' &ne; r<sub>i</sub></td></tr><tr><td>36</td><td>return rf<sub>i+1</sub></td></tr></tbody></table>

The algorithm terminates. At each call to the Update procedure, a read event $r_i$ is picked and is associated with a new write event $w''_i$ which is po-later than the current write event $w_i$. Therefore, there cannot be more than $n$ calls to the Update function.
The algorithm is correct. Suppose the algorithm stops after $m$ calls to Update function in Line 4. We will now inductively prove that $rf_i \subseteq rf^\dagger$ for every rf function $rf^\dagger$ that satisfies weak-read-coherence. The property is trivially true for $rf_0$. Assume the property to be true for $rf_i$, that is $rf_i \subseteq rf^\dagger$. We will show that the call to the update function preserves the property. Since Update has been called, there is a cycle violating weak-read-coherence: $r_i \xrightarrow{rf_i} w_i \xrightarrow{hb_i} w'_i \xrightarrow{hb_i} r_i$.

Let $hb^\dagger$ be the happens-before relation induced by $rf^\dagger$. Since $rf_i \subseteq rf^\dagger$, by an argument similar to the proof of the second item of Lemma 3, we deduce $w'_i \xrightarrow{hb^\dagger} r_i$. As $rf^\dagger$ satisfies weak-read-coherence, this would mean $w'_i \text{ po}^* rf^\dagger(r_i)$: since $w'_i$ happens before $r_i$, the event $rf^\dagger(r_i)$ that writes to $r_i$ should be po-later to $w'_i$. In Lines 28 and 32 of the algorithm, we pick the earliest matching write event $w''_i$ that appears po-after $w'_i$. Therefore, this would imply $w''_i \text{ po}^* rf^\dagger(r_i)$. For the other events $r'$, there is no change in the Update function. Hence, we deduce $rf_{i+1} \subseteq rf^\dagger$ for every rf function $rf^\dagger$ that satisfies weak-read-coherence.

When the Algorithm stops at Lines 30 or 34, it has not found a matching write that is po-later than $w'_i$. From the above invariant that $rf_i \subseteq rf^\dagger$, this means there is no consistent $rf^\dagger$ for this partial execution graph $\bar{X}$. The algorithm correctly returns the verdict of inconsistency in Lines 30 or 34. When the algorithm reaches 5, an rf function $rf_m$ satisfying weak-read-coherence is found. By the above invariant, $rf_m = rf_{min}$, the smallest rf that satisfies weak-read-coherence. Then, we test for porf-acyclicity. From the first item of Lemma 3, if it does not satisfy porf-acyclicity, no bigger rf function satisfies it, and we can conclude that both weak-read-coherence and porf-acyclicity cannot be simultaneously satisfied. Hence the algorithm correctly returns that the partial execution graph is no WRA-consistent in Line 8.

*Complexity.* As discussed before, there are atmost $n$ calls to Update. Before each call, weak-read-coherence needs to be checked. This can be posed as a graph problem: there are $n$ nodes corresponding to the events, and there are three kinds of edges po, rf and $rf^{-1}$; does there exist a cycle of the form $r \xrightarrow{rf^{-1}} w_x \xrightarrow{\text{po}^*} w'_x \xrightarrow{(\text{po} \cup \text{rf})^*} r$? For each read event $r$ and its corresponding write event $w$, we need to check if there exist a $w'$ such that (1) there is a path of po edges from $w$ to $w'$, and (2) there is a path from $w'$ to $r$ over a combination of po and rf edges. For each read, this can be achieved by in $O(n)$ time by a graph search. Hence, overall, across all possible reads, this algorithm takes $O(n^2)$ time. Now, once inside the Update procedure, finding the next write takes $O(n)$ time. Therefore, each call to update costs $O(n^2)$ and there are $n$ calls. This gives a complexity of $O(n^3)$. Furthermore, the Initialize procedure takes at most $O(n^2)$: for each read, there is atmost $O(n)$ time spent on finding the matching write. The final check for $\text{po} \cup \text{rf}$ cycle can be done in $(n)$. Hence we get an overall complexity of $O(n^3)$. $\square$
### A.3 Super linear lower bound for checking weak-read-coherence

This section is devoted to the proof of Proposition 6.

**Reduction.** Given an undirected graph $G = (V_G, E_G)$ with $n$ vertices, we construct a partial execution graph $\bar{X} = \langle E, \rho_0 \rangle$ with $|E| = O(V_G + E_G)$ such that $\bar{X}$ satisfies weak-read-coherence iff $G$ is triangle-free. For simplicity, we let $V_G = \{1, \dots, n\}$. As the graph is undirected, we assume that if $(u, v) \in E$ then $(v, u) \in E$.

*Events, threads and memory locations.* For each vertex $v \in V_G$, we have threads $t_{a_v}, t_{b_v}, t_{c_v}$ and $t_{d_v}$. For each edge $(u, v) \in E_G$, we have locations $a_{uv}, b_{uv}, c_{uv}$. We also have locations $a_v, b_v, c_v$ for $v \in V_G$. The events are $\mathbf{w}(a_v, 0), \mathbf{w}(a_v, 1), \mathbf{r}(a_v, 0)$, as well as $\{\mathbf{w}(x_{uv}, 0), \mathbf{r}(x_{uv}, 0) | x \in \{a, b, c\}\}$. We also have events $\mathbf{w}(b_v), \mathbf{w}(c_v)$ (the values do not matter). This gives us $4|V_G|$ threads, $3(|E_G| + |V_G|)$ locations and $5|V_G| + 2|E_G|$ events.

We now describe the threads. Let $v \in V_G$ and $x \in \{a, b, c\}$. Let $N_v = \{\alpha | (v, \alpha) \in E_G\}$. Let $W(x_{vw}, 0), R(x_{vw}, 0)$ be macros representing respectively, the sequence of events $\mathbf{w}(x_{v\alpha_1}, 0) \dots \mathbf{w}(x_{v\alpha_m}, 0)$ and $\mathbf{r}(x_{v\alpha_1}, 0) \dots \mathbf{r}(x_{v\alpha_m}, 0)$ such that $\alpha_1, \dots, \alpha_n \in N_v$.

$$ 
\begin{align*}
t_{a_v} & : \mathbf{w}(a_v, 0)\mathbf{w}(a_v, 1)W(a_{vw}, 0) \\
t_{b_v} & : R(a_{vw}, 0) w(b_v) W(b_{vw}, 0) \\
t_{c_v} & : R(b_{vw}, 0) w(c_v) W(c_{vw}, 0) \\
t_{d_v} & : R(c_{vw}, 0)\mathbf{r}(a_v, 0)
\end{align*}
$$

The construction is such that each location is written into by a unique thread. Further, each location is accessed only by at most two threads. Each location (barring $a_v$) is written into exactly once by its writer thread and the *rf* is trivially determined. Thus, the constructed $\bar{X}$ qualifies as a single writer. The construction has the following properties.

1. $(x, y) \in E_G$ iff $\mathbf{w}(a_x, 0) \rho_0 \mathbf{w}(a_x, 1) \textcolor{green}{\mathbf{w}(b_y)}$

2. $(x, y) \in E_G$ iff $\mathbf{w}(b_x) \textcolor{green}{\mathbf{w}(c_y)}$

3. $(x, y) \in E_G$ iff $\mathbf{w}(c_x) \textcolor{green}{\mathbf{r}(a_y, 0)}$

Thus, a path $x-y-z$ of length 2 results in $\mathbf{w}(a_x, 1) \rho_0 \mathbf{w}(a_x, 0) \textcolor{green}{\mathbf{w}(b_y)} \textcolor{green}{\mathbf{w}(c_z)}$, and a path $x-y-z-w$ of length 3 results in

$$ \mathbf{w}(a_x, 1) \rho_0 \mathbf{w}(a_x, 0) \textcolor{green}{\mathbf{w}(b_y)} \textcolor{green}{\mathbf{w}(c_z)} \textcolor{green}{\mathbf{r}(a_w, 0)} $$

The key invariant behind the reduction is that for any $v \in V_G$, $\mathbf{w}(a_v, 1) \textcolor{green}{\mathbf{r}(a_v, 0)}$ iff $G$ contains a triangle. The former violates weak-read-coherence. Figure 6
<figure><img src="image_6.png" /><figcaption>Fig. 6: A partial execution $\bar{X}$ for a graph $G = (\{1, 2, 3\}, \{(1, 2), (2, 1), (1, 3), (3, 1), (2, 3), (3, 2)\})$. We have $(\mathbf{w}(a_1, 0), \mathbf{r}(a_1, 0)) \in \text{hb}$ violating weak read coherence in $\bar{X}$.</figcaption></figure>

shows the reduction on a graph with 3 vertices $\{1, 2, 3\}$, having edges between every distinct pair of vertices.

**Correctness and Time Complexity.** Assume that $G$ has a triangle $(x, y, z)$. Wlg, let $x < y < z$. Then $\mathbf{w}(a_x, 1)$ **hb** $\mathbf{r}(a_x, 0)$ as follows: $\mathbf{w}(a_x, 1)$ po $\mathbf{w}(a_{xy}, 0)$ **rf** $\mathbf{r}(a_{xy}, 0)$ po $\mathbf{w}(b_{yz}, 0)$ **rf** $\mathbf{r}(b_{yz}, 0)$ po $\mathbf{w}(c_{zx}, 0)$ **rf** $\mathbf{r}(c_{zx}, 0)$ po $\mathbf{r}(a_x, 0)$. Together with $\mathbf{w}(a_x, 0)$ po $\mathbf{w}(a_x, 1)$, we obtain a weak-read-coherence violation. Triangle-freeness in the input graph $G$ ensures satisfying weak-read-coherence. In the construction, the only way to violate weak-read-coherence is to have $\mathbf{w}(a_v, 0)$ po $\mathbf{w}(a_v, 1)$ **hb** $\mathbf{r}(a_v, 0)$ for some $v \in V_G$. This is achieved by:

$$ \mathbf{w}(a_v, 1) \text{ po } \mathbf{w}(a_{vu}, 0) \text{ hb } \mathbf{w}(b_{uw}, 0) \text{ hb } \mathbf{w}(c_{wv}, 0) \text{ rf } \mathbf{r}(c_{wv}, 0) \text{ po } \mathbf{r}(a_v, 0) $$

This points to a triangle $vuw$ in $G$. The total time to construct $\bar{X}$ is $O(V_G + E_G)$.

# B Appendix for Section 4

## B.1 An example to illustrate the reduction

Table 2 gives an instance of the fine-grained hardness reduction for 3-WRITER. A satisfying assignment for $\varphi$ is $x_1 = 1, x_2 = 0, x_3 = 0$. The rf synthesis would be as follows:

$$ - \langle T_{x_1} : \mathbf{w}(c_1, 1) \rangle \text{ rf } \langle T_f : \mathbf{r}(c_1, 1) \rangle, \langle T_{x_1} : \mathbf{w}(c_2, 1) \rangle \text{ rf } \langle T_f : \mathbf{r}(c_2, 1) \rangle $$

$$ - \langle T_1^1 : \mathbf{w}(s_1, 2) \rangle \text{ rf } \langle T_f : \mathbf{r}(s_1, 2) \rangle, \langle T_1^0 : \mathbf{w}(s_1, 1) \rangle \text{ rf } \langle T_f : \mathbf{r}(s_1, 1) \rangle $$

$$ - \langle T_2^0 : \mathbf{w}(s_2, 2) \rangle \text{ rf } \langle T_f : \mathbf{r}(s_2, 2) \rangle, \langle T_2^1 : \mathbf{w}(s_2, 1) \rangle \text{ rf } \langle T_f : \mathbf{r}(s_2, 1) \rangle $$

$$ - \langle T_3^0 : \mathbf{w}(s_3, 2) \rangle \text{ rf } \langle T_f : \mathbf{r}(s_3, 2) \rangle, \langle T_3^1 : \mathbf{w}(s_3, 1) \rangle \text{ rf } \langle T_f : \mathbf{r}(s_3, 1) \rangle $$

All other rf-edges are trivial. Note that the resulting execution graph satisfies all the weak memory axioms of SRA (Refer Table 1).
<table><caption>Table 2: $\varphi = (x_1 \lor x_2 \lor x_3) \land (x_1 \lor \neg x_2 \lor \neg x_3)$</caption><thead><tr><th>T<sub>1</sub><sup>1</sup></th><th>T<sub>1</sub><sup>0</sup></th><th>T<sub>x<sub>1</sub></sub></th><th>T<sub>x<sub>1</sub></sub></th><th>T<sub>f</sub></th></tr></thead><tbody><tr><td>w(s<sub>1</sub>, 1)</td><td>w(s<sub>1</sub>, 1)</td><td>r(v<sub>1</sub>, 1)</td><td>r(v<sub>1</sub>, 0)</td><td>r(c<sub>1</sub>, 1)</td></tr><tr><td>w(s<sub>1</sub>, 2)</td><td>w(s<sub>1</sub>, 2)</td><td>w(c<sub>1</sub>, 1)</td><td></td><td>r(c<sub>2</sub>, 1)</td></tr><tr><td>w(v<sub>1</sub>, 1)</td><td>w(v<sub>1</sub>, 0)</td><td>w(c<sub>2</sub>, 1)</td><td></td><td>r(s<sub>1</sub>, 2)</td></tr><tr><th>T<sub>2</sub><sup>1</sup></th><th>T<sub>2</sub><sup>0</sup></th><th>T<sub>x<sub>2</sub></sub></th><th>T<sub>x<sub>2</sub></sub></th><th>r(s<sub>1</sub>, 1)</th></tr><tr><td>w(s<sub>2</sub>, 1)</td><td>w(s<sub>2</sub>, 1)</td><td>r(v<sub>2</sub>, 1)</td><td>r(v<sub>2</sub>, 0)</td><td>r(s<sub>2</sub>, 2)</td></tr><tr><td>w(s<sub>2</sub>, 2)</td><td>w(s<sub>2</sub>, 2)</td><td>w(c<sub>1</sub>, 1)</td><td>w(c<sub>2</sub>, 1)</td><td>r(s<sub>2</sub>, 1)</td></tr><tr><td>w(v<sub>2</sub>, 1)</td><td>w(v<sub>2</sub>, 0)</td><td></td><td></td><td>r(s<sub>3</sub>, 2)</td></tr><tr><th>T<sub>3</sub><sup>1</sup></th><th>T<sub>3</sub><sup>0</sup></th><th>T<sub>x<sub>3</sub></sub></th><th>T<sub>x<sub>3</sub></sub></th><th>r(s<sub>3</sub>, 1)</th></tr><tr><td>w(s<sub>3</sub>, 1)</td><td>w(s<sub>3</sub>, 1)</td><td>r(v<sub>3</sub>, 1)</td><td>r(v<sub>3</sub>, 0)</td><td></td></tr><tr><td>w(s<sub>3</sub>, 2)</td><td>w(s<sub>3</sub>, 2)</td><td>w(c<sub>1</sub>, 1)</td><td>w(c<sub>2</sub>, 1)</td><td></td></tr><tr><td>w(v<sub>3</sub>, 1)</td><td>w(v<sub>3</sub>, 0)</td><td></td><td></td><td></td></tr></tbody></table>

## B.2 Missing proofs of Section 4.1

**Lemma 9.** If $\varphi$ has a satisfying assignment, then $\bar{X}_{\varphi} \models \text{SRA}$.

*Proof.* Suppose $\varphi$ has a satisfying assignment $A$. We need to synthesize rf and mo such that the resulting execution graph satisfies porf-acyclicity, strong-write-coherence and strong-read-coherence. Since $A$ is a satisfying assignment, for every clause $C_j$ there is a literal $\ell_j$ that is made true. Let rf($r(c_j, 1)$) be the write event $w(c_j, 1)$ in $T_{\ell_j}$. Assigning writes this way introduces an hh path from $T_i^{A(x_i)}$ for all variables that are indeed being utilized to make the clauses true. Importantly, there is no hh path created from $T_i^{\neg A(x_i)}$ to the thread $T_f$. Therefore, the read event $r(s_i, 2)$ can read from the write in $T_i^{A(x_i)}$ and $r(s_i, 1)$ can read from the unused thread $T_i^{\neg A(x_i)}$. This gives an rf which satisfies weak-read-coherence. By design of the execution graph, the rf also satisfies porf-acyclicity. However, for the lemma, we need to show consistency for SRA, hence we require to prove strong-write-coherence and read-coherence. For this we need to also synthesize an mo. Consider any mo relation that respects the following orders:

- $T_i^{A(x_i)} : w(s_i, 1) \xrightarrow{\text{mo}} T_i^{\neg A(x_i)} : w(s_i, 1) \xrightarrow{\text{mo}} T_i^{\neg A(x_i)} : w(s_i, 2) \xrightarrow{\text{mo}} T_i^{A(x_i)} : w(s_i, 2)$,

- For each clause $j$ there are three threads writing $w(c_j, 1)$. For each clause $C_j$ choose a specific literal $\ell_j$ that is made true by the satisfying assignment $A$. The mo relation orders the other write statements $w(c_j, 1)$ before $T_{\ell_j} : w(c_j, 1)$.

It can be shown that the constructed rf and mo satisfy strong-write-coherence and read-coherence.

*Strong-write-coherence.* We will show that the constructed rf and mo satisfy strong-write-coherence, that is acyclicity of hh $\cup$ mo. Suppose not. There is a cycle $C$ consisting of po, rf and mo edges (thereby violating strong-write-coherence).
Since we have seen that there is no po ∪ rf cycle, cycle C should contain an mo edge. An edge $\langle T_i^1 : \mathbf{w}(s_i, 1) \rangle$ mo $\langle T_i^1 : \mathbf{w}(s_i, 1) \rangle$ cannot be present in C since there can be no incoming po or rf edge to $\langle T_i^1 : \mathbf{w}(s_i, 1) \rangle$. Now, consider an edge $\langle T_i^0 : \mathbf{w}(s_i, 2) \rangle$ mo $\langle T_i^1 : \mathbf{w}(s_i, 2) \rangle$. The only incoming edge to $\langle T_i^0 : \mathbf{w}(s_i, 2) \rangle$ is a po edge from $\langle T_i^0 : \mathbf{w}(s_i, 1) \rangle$, and there can be no po or rf edges into the latter event. Hence, even the second type of mo edges cannot be present in C. This leaves us with mo edges of the form $\langle T_{\ell'} : \mathbf{w}(c_j, 1) \rangle$ mo $\langle T_{\ell_j} : \mathbf{w}(c_j, 1) \rangle$. Notice that from the latter event, $\langle T_{\ell_j} : \mathbf{w}(c_j, 1) \rangle$ the only outgoing edges are to $T_f$, and from $T_f$, there are no outgoing edges, hence there is no path from an event in $T_f$ to $\langle T_{\ell'} : \mathbf{w}(c_j, 1) \rangle$. This proves that such an mo edge cannot be part of an hb ∪ po cycle too. We conclude that there are no hb ∪ mo cycles.

**Read-coherence.** Finally, we need to prove read-coherence, i.e., $\text{irr}(\text{rf}^{-1}; \text{mo}_x; \text{hb})$. If read coherence is violated, there is a read event $r$, and two write events $w, w'$ such that $w \text{ rf } r$, $w$ mo $w'$ and $w'$ hb $r$. Such a violation can potentially happen on variables which have multiple write events: in our case $s_i$ and $c_j$. To do this, let us collect the view of each read event on these variables and note that no read observes a value that is mo-overwritten in its happens-before past.

- By construction $\langle T_f : \mathbf{r}(s_i, 2) \rangle$ contains $T_i^{A(x_i)}$ and does not contain $T_i^{\neg A(x_i)}$. Therefore there is no write event mo-later than $T_i^{A(x_i):w(s_i, 2)}$ in this view.

- For the read event $\langle T_f : \mathbf{r}(s_i, 1) \rangle$, all writes to $s_i$ except $\langle T_i^{\neg A(x_i)} : \mathbf{w}(s_i, 2) \rangle$ are visible to it. Moreover, the event $\langle T_i^{A(x_i)} : \mathbf{w}(s_i, 1) \rangle$ that writes to it is the mo-latest in the view.

- For the variable $c_j$, the view of $\langle T_f : \mathbf{r}(c_j, 1) \rangle$ contains only the write $w(c_j, 1)$ from the thread $T_{\ell_j}$ corresponding to the literal $\ell_j$ that satisfies $C_j$ under A. All other writes to $c_j$ occur before this write in mo.

This shows that the constructed rf and mo are consistent with SRA. □

## B.3 Missing proofs from Section 4.2

**Lemma 11.** If $\overline{Y}_{\phi} \models WRA$, then $\phi$ has a satisfying assignment.

*Proof.* The proof proceeds similar to Lemma 8. We need to argue that if there is an rf that satisfies weak-read-coherence, then there cannot be two distinct reads $\mathbf{r}(d_j, 1)$ and $\mathbf{r}(d_p, 1)$ in $T_f$ that (directly or indirectly) read from threads corresponding to both a literal and its negation for some variable $x_i$. The $\mathbf{r}(d_j, 1)$ event in $T_f$ can either read from $T_{\ell_j}$ or from $T_j$. Similarly, $\mathbf{r}(d_p, 1)$ can read from $T_{\ell_p}$ or $T_p$. If it so happens that the two threads from which $\mathbf{r}(d_j, 1)$ and $\mathbf{r}(d_p, 1)$ read from are of the form $T_{x_i}$ and $T_{\neg x_i}$, then both $\langle T_i^0 : \mathbf{w}(s_i, 2) \rangle$ and $\langle T_i^1 : \mathbf{w}(s_i, 2) \rangle$ are in the view of $\langle T_f : \mathbf{r}(s_i, 2) \rangle$. Then, since the execution satisfies weak-read-coherence, there is no write event available for $\langle T_f : \mathbf{r}(s_i, 1) \rangle$. A
contradiction. Hence the set of literals making the clauses true in $T_f$ encode a
satisfying assignment. $\square$

**Lemma 12.** If $\varphi$ has a satisfying assignment, then $\bar{Y}_{\varphi}^{RA} \models$ SRA.

*Proof.* Let $A$ be a satisfying assignment. The *rf* and *mo* relations on events with variables $s_i$ remains the same as in the proof of Lemma 9. There are changes for $c_j$ and $d_j$. Consider a clause $C_j$.

- If $A$ makes $\ell_j^3$ true then:

• $\langle T_{\ell_j^3} : w(d_j, 1) \rangle$ rf $\langle T_f : r(d_j, 1) \rangle$,

• Choose an arbitrary $w(c_j, 1)$ for $\langle T_j : r(c_j, 1) \rangle$

- Else, $A$ makes one of the first two literals of $C_j$ true. Arbitrarily pick one $\ell_j^i$, for $i \in \{1, 2\}$:

• $\langle T_{\ell_j^i} : w(c_j, 1) \rangle$ rf $\langle T_j : r(c_j, 1) \rangle$,

• $\langle T_j : w(d_j, 1) \rangle$ rf $\langle T_f : r(d_j, 1) \rangle$

For every variable-value pair, there are atmost two writes. With the rf picked as above, the mo relation gets fixed: the unused write is mo-before the used write.

Clearly, the rf relation agrees with po and hence does not violate porf-acyclicity. We need to prove strong-write-coherence and read-coherence as in the proof of Lemma 9.

*Strong-write-coherence.* Suppose, for contradiction, that there is a cycle in *hb* ∪ *mo*. As in Lemma 9, the only possible *mo* edges are between the two writes to $s_i$, $c_j$, or $d_j$. For $s_i$, the argument is identical to before: the only incoming edges to the earlier write are from po, and there are no cycles. For $c_j$ and $d_j$, each has at most two writers, and the *mo*-later event leads to $T_f$ from which there is no path back to the *mo*-earlier event. Thus, no cycle can be formed. Therefore, strong-write-coherence holds.

*Read-coherence.* Suppose, for contradiction, that there is a violation of read-coherence: there exists a read $r$ and two writes $w, w'$ to the same variable such that $w$ rf $r$, $w$ mo $w'$, and $w'$ hb $r$. As before, this can only occur for variables $s_i$, $c_j$, or $d_j$. For $s_i$, the argument is unchanged from Lemma 9. For $c_j$ and $d_j$, the view of each read contains only the rf-used write, and the other write (if any) is mo-before and not visible to the read. Thus, no such violation can occur.

Therefore, the constructed rf and mo are consistent with SRA. $\square$
<figure><img src="image_7.png" /><figcaption>Fig. 7: Violation of (a) relaxed-write-coherence: $w_2(x)$ mo $w_1(x)$, $w_1(x)$ po $w_2(x)$ (b) relaxed-read-coherence: $w_1(x)$ mo $w_2(x)$, $r_2(x)$ po $r_1(x)$ with $w_2(x)$ rf $r_2(x)$ and $w_1(x)$ rf $r_1(x)$.</figcaption></figure>

## C Relaxed Memory Model

In this appendix we study the complexity of the VM problem for the 'relaxed' fragment of C-11. Relaxed model satisfy the coherence axioms: relaxed-read-coherence and relaxed-write-coherence (Table 3). Essentially all hb's in weak-read-coherence and write-coherence are replaced by po. For better understanding, Figure 7 shows instances for violation of the relaxed axioms. For the stronger variation of the relaxed model, Relaxed-A cyclic we have the extra requirement of porf-acyclicity. The overview of this section is as follows:

- Appendix C.1 gives a polynomial time algorithm for the VM-problem restricted to 1-WRITER under Relaxed-A cyclic memory model.

- Appendix C.2 gives a conditional lower bound for the VM-problem under ETH for 3-WRITER.

- Appendix C.3 shows that the VM-problem restricted to 2-WRITER is NP-hard

<table><caption>Table 3: Coherence Axioms for Relaxed-A cyclic variant of C11</caption><thead><tr><th></th><th>Relaxed-A cyclic</th></tr></thead><tbody><tr><td>irr po ∪ rf</td><td>(porf-acyclicity)</td></tr><tr><td>irr mo<sub>x</sub>; po</td><td>(relaxed-write-coherence)</td></tr><tr><td>irr rf<sup>-1</sup>; mo<sub>x</sub>; rf<sup>?</sup>; po</td><td>(relaxed-read-coherence)</td></tr></tbody></table>

### C.1 Polynomial Time for 1-WRITER systems

Here we give a polynomial time algorithm for solving the VM-problem for 1-WRITER under Relaxed-A cyclic memory model. Note that as Relaxed-A cyclic is stronger than Relaxed. So any polynomial time result for Relaxed-A cyclic would also hold for Relaxed. As for 1-WRITER systems we have mo = po, relaxed-write-coherence would always hold. Hence to show that an execution graph X is Relaxed-A cyclic-consistent, we need to verify porf-acyclicity and relaxed-read-coherence. We can state the following lemma for Relaxed similar to Lemma 3.
**Lemma 13.** Let $rf_1$ and $rf_2$ be two reads-from functions over a partial 1-WRITER execution graph $\mathcal{X} = (E, \mathit{po}, \mathit{mo})$ s.t. $\mathit{mo}$ agrees with $\mathit{po}$.

- Suppose $rf_1 \sqsubseteq rf_2$. Then, if $rf_1$ induces a $\mathit{po} \cup rf_1$ cycle, then $rf_2$ induces a $\mathit{po} \cup rf_2$ cycle.

- Suppose both $rf_1$ and $rf_2$ satisfy relaxed-read-coherence. Then, the rf function $\min(rf_1, rf_2)$ also satisfies relaxed-read-coherence.

*Proof.* The proof for the first part is same as that of WRA in lemma 3 and hence we skip it.

For the second part, we denote $rf_0 = \min(rf_1, rf_2)$. We shall show that that if $rf_0$ violates relaxed-read-coherence, then either $rf_1$ or $rf_2$ violates it. Suppose $rf_0$ induces a violation of relaxed-read-coherence. There is a cycle of the form:

$$r \xrightarrow{rf_0^{-1}} w \xrightarrow{\mathit{po}^+} w' \xrightarrow{rf_0} r' \xrightarrow{\mathit{po}^+} r$$

, where all of $w, w', r$ and $r'$ are in the same variable. By definition, either $rf_1$ or $rf_2$ associates $r$ to $w$. WLOG, say $rf_1(r) = w$. Then either $w' rf_1 r'$ or $w' rf_2 r'$. For the former case, $rf_1$ is not Relaxed-consistent. For the later case, there is a write event $w''$ on $x$ such that $w' \mathit{po}^* w'' rf_1 r'$ as $rf_0$ maps $r'$ to the po-earlier read between $rf_1(r')$ and $rf_2(r')$. Again relaxed-read-coherence of $rf_1$ fails thereby proving the second item. $\square$

**Finding the smallest Relaxed-consistent rf** To show that an execution graph, $\bar{\mathcal{X}}$ satisfies Relaxed consistency, we check for porf-acyclicity, relaxed-read-coherence and relaxed-write-coherence.

Algorithm 1 can be modified to obtain a PTIME algorithm for Relaxed. The modifications are as follows:

- Any appearance of weak-read-coherence would be replaced by relaxed-read-coherence.

- Any appearance of WRA-consistency would be replaced by Relaxed-consistency.

- Line 20 would be replaced by 'Pick a cycle violating relaxed-read-coherence:

$$r_i \xrightarrow{rf_i^{-1}} w_i \xrightarrow{\mathit{po}} w'_i \xrightarrow{rf} r'_i \xrightarrow{\mathit{po}} r_i.$$

- We use check for porf-acyclicity in line 5 of Algorithm 1 only if the underlying memory model is Relaxed-A cyclic.

Note that, by construction of the algorithm, relaxed-write-coherence is never violated. The correctness of the algorithm uses Lemma 13 and is analogous to that of Algorithm 1. Theorem 14 can be restated in terms of Relaxed as follows.

**Theorem 14.** A partial execution graph $\bar{\mathcal{X}} = (E, \mathit{po})$ of a one-writer system is consistent for Relaxed iff the modified version of Algorithm 1 for Relaxed memory
model, executes Line 6. Moreover, the algorithm runs in time $O(n^3)$ where $n = |E|$ and returns the smallest rf function that is Relaxed-consistent, if one exists.

The calculation of complexity of the algorithm is similar to that of WRA (Section 3.2). We want to check for a cycle of the form $r \xrightarrow{rf_0^{-1}} w \xrightarrow{po^+} w' \xrightarrow{rf_0} r' \xrightarrow{po^+} r$. For each read event $r$ and its corresponding write event $w$, we need to check if there exist a $w'$ such that (1) there is a path of $po$ edges from $w$ to $w'$, (2) $w' \text{ rf } r'$ and (3) $r' \text{ po}^+ r$. For each read, this can be achieved in $O(n)$ time by a graph search. Hence, overall, across all possible reads, this algorithm takes $O(n^2)$ time. Therefore, each call to update costs $O(n^2)$ and there can be at most $n$ calls. This gives a complexity of $O(n^3)$.

## C.2 Fine-grained hardness under ETH for 3-WRITER systems

**Lemma 15.** Under ETH, there is no $2^{o(k)} \cdot n^{O(1)}$ algorithm for the consistency testing problem for Relaxed where $k$ is the number of threads, and $n$ the number of events, even when the executions graphs are 3-WRITER and the number of writes per variable is four.

Let $\varphi = \{C_i\}_{i \in [m]}$ be a Boolean formula over $k$ variables $\{x_j\}_{j \in [k]}$ and $m$ clauses of the form $C_j = (\ell_j^1, \ell_j^2, \ell_j^3)$ with where each literal is either a variable $x_i$ or its negation $\neg x_i$. Given a 3-CNF-SAT formula $\varphi$ with $k$ variables and $m$ clauses, we construct an abstract execution $\bar{X} = (E, po)$ with $2k+3$ threads, accessing $k+m$ memory locations $v_1, v_2, \dots, v_k, c_1, \dots, c_m$ and 2 values 1, 0 such that $\varphi$ is satisfiable iff $\bar{X}_\varphi \models \text{Relaxed}$. $\bar{X}_\varphi$ follows the general scheme depicted in Table 8.

We remark that an **mo** edge from $w(v_i, 0)$ to $w(v_i, 1)$ encode variable $x_i$ being set to **true**, and an **mo** edge in the opposite direction $x_i$ being set to **false**.

The threads `Init1` and `Init0` initialize the valuation used to evaluate the formula. For each variable $x_i$ corresponding to the Boolean variables of $\varphi$, `Init1` writes 1 and `Init0` writes 0. $T_{x_i}$ has a read statement $\mathbf{r}(v_i, 0)$ followed by $\mathbf{r}(v_i, 1)$ (which denotes reading **true** for $x_i$) and sets all clauses containing $x_i$ to true, using the statement $w(c_j, 1)$ for all $j \in S_{x_i}$.

Similarly, thread $T_{\neg x_i}$ reads $\mathbf{r}(v_i, 1)$ followed by $\mathbf{r}(v_i, 0)$ (denoting the value **false** for $x_i$) and sets all clauses containing $\neg x_i$ to true. Finally the thread $T_f$ needs to make sure that all clauses are set to true, accomplished by the read statements

<figure><img src="image_8.png" /><figcaption>Fig. 8: Threads in the reduction for Relaxed</figcaption></figure>
r(c<sub>1</sub>, 1), . . . , r(c<sub>m</sub>, 1). Then, T<sub>f</sub> proceeds through the following steps (1) all the variables v<sub>i</sub>s are set to 0, followed by (2) setting all the variables v<sub>i</sub>s to 1, and finally (3) setting all the variables v<sub>i</sub>s to 0 again. This sequence ensures that any threads T<sub>x<sub>i</sub></sub>, T<sub>¬x<sub>i</sub></sub> which were not executed in Phase 2 now have their conditions satisfied and can complete their execution.

**Lemma 16.** $\varphi$ is satisfiable iff $\bar{X}_{\varphi} \models \text{Relaxed}$.

*Proof.* Suppose A is a satisfying assignment for $\varphi$. We explicitly describe the **rf** relation and **mo** relation as follows.

If $A(x_i) = true$:

- $\langle \text{Init}_0 : \mathbf{w}(v_i, 0) \rangle \text{ rf } \langle T_{x_i} : \mathbf{r}(v_i, 0) \rangle$ and $\langle \text{Init}_1 : \mathbf{w}(v_i, 1) \rangle \text{ rf } \langle T_{x_i} : \mathbf{r}(v_i, 1) \rangle$,

- $\langle T_f : \mathbf{w}(v_i, 1) \rangle \text{ rf } \langle T_{\neg x_i} : \mathbf{r}(v_i, 1) \rangle$, and $\langle T_f : \mathbf{w}(v_i, 0) \rangle \text{ rf } \langle T_{\neg x_i} : \mathbf{r}(v_i, 0) \rangle$.

Else, when $A(x_i) = false$,

- $\langle \text{Init}_1 : \mathbf{w}(v_i, 1) \rangle \text{ rf } \langle T_{\neg x_i} : \mathbf{r}(v_i, 1) \rangle$, and $\langle \text{Init}_0 : \mathbf{w}(v_i, 0) \rangle \text{ rf } \langle T_{\neg x_i} : \mathbf{r}(v_i, 0) \rangle$,

- $\langle T_f : \mathbf{w}(v_i, 0) \rangle \text{ rf } \langle T_{x_i} : \mathbf{r}(v_i, 0) \rangle$, and $\langle T_f : \mathbf{w}(v_i, 1) \rangle \text{ rf } \langle T_{x_i} : \mathbf{r}(v_i, 1) \rangle$.

Coming to variables $c_i$s, for each $T_f : \mathbf{r}(c_j, 1)$ there is a literal $\ell_j$ in clause $C_j$ that is true. Let $\langle T_{\ell_j} : \mathbf{w}(c_j, 1) \rangle \text{ rf } \langle T_f : \mathbf{r}(c_j, 1) \rangle$. Observe that the constructed **rf** satisfies po – **rf**-acyclicity.

The **rf** induces the following **mo** relation. If $A(x_i) = true$:

- $\langle \text{Init}_0 : \mathbf{w}(v_i, 0) \rangle \text{ mo } \langle \text{Init}_1 : \mathbf{w}(v_i, 1) \rangle \text{ mo } \langle T_f : \mathbf{w}(v_i, 1) \rangle \text{ mo } \langle T_f : \mathbf{w}(v_i, 0) \rangle \text{ mo } \langle T_f : \mathbf{w}(v_i, 1) \rangle$

- For each clause $C_j$ there are three threads writing $\mathbf{w}(c_j, 1)$. For $C_j$, choose a specific literal $\ell_j$ that is made true by the satisfying assignment A. The **mo** relation orders the write statements $\mathbf{w}(c_j, 1)$ in literals that are set to true before $T_{\ell_j} : \mathbf{w}(c_j, 1)$, and those in literals that set to false after $T_{\ell_j} : \mathbf{w}(c_j, 1)$.

When $A(x_i) = false$, an **mo** order can be defined analogously.

**Relaxed Write-coherence.** From our construction, it is easy to see $\text{irr}(\text{mo}_x; \text{po})$.

**Relaxed Read-coherence.** We need to prove $\text{irr}(\text{rf}^{-1}; \text{mo}_x; \text{rf}^?; \text{po})$. If relaxed read coherence is violated, the violating pattern is of the following form there are read events $r_1$ and $r_2$, and two write events $w_1, w_2$ such that $w_1 \text{ rf } r_1, w_2 \text{ rf } r_2, w_1 \text{ mo } w_2$ and $r_2 \text{ po } r_1$. Such a violation can potentially happen on variables which have multiple read events in the same thread, which is only the case for $v_i$. We consider the various possibilities below. We consider the case $A(x_i) = true$ below.

- $\langle T_{x_i} : \mathbf{r}(v_i, 0) \rangle \text{ po } \langle T_{x_i} : \mathbf{r}(v_i, 1) \rangle$, reads-from $\text{Init}_0$ and $\text{Init}_1$ respectively, where **mo** agrees with the **po**.
- $\langle T_{\neg x_i} : \mathbf{r}(v_i, 1) \rangle \text{ po } \langle T_{\neg x_i} : \mathbf{r}(v_i, 0) \rangle$, reads-from the first two writes on $v_i$ in $T_f$ respectively, where, once again **mo** agrees with the po, and irreflexivity is ensured.

A similar argument can be made for the case the case $A(x_i) = \text{false}$.

This shows that the constructed **rf** and **mo** are consistent with **Relaxed**.

Conversely, suppose $\bar{\mathbf{X}}_{\varphi} \models \text{Relaxed}$. We need to show that there are no two $\mathbf{r}(c_j, 1)$ and $\mathbf{r}(c_{\ell}, 1)$ reading from some $T_{x_i}$ and $T_{\neg x_i}$. Suppose not. Let $\mathbf{r}(c_j, 1)$ read from $T_{x_i} : \mathbf{w}(c_j, 1)$ and $\mathbf{r}(c_{\ell}, 1)$ read from $T_{\neg x_i} : \mathbf{w}(c_{\ell}, 1)$. Consider the thread $T_{x_i}$. Since $T_{x_i} : \mathbf{w}(c_j, 1)$ has been read from, this means that the preceding read instructions of $T_{x_i}$ have been executed, and the only possible read from relation is as follows: $\langle \text{Init}_0 : \mathbf{w}(v_i, 0) \rangle \text{ rf } \langle T_{x_i} : \mathbf{r}(v_i, 0) \rangle$, and $\langle \text{Init}_1 : \mathbf{w}(v_i, 1) \rangle \text{ rf } \langle T_{x_i} : \mathbf{r}(v_i, 1) \rangle$. By relaxed read coherence axiom, this implies $\langle \text{Init}_0 : \mathbf{w}(v_i, 0) \rangle \text{ mo } \langle \text{Init}_1 : \mathbf{w}(v_i, 1) \rangle$

Now, consider the thread $T_{\neg x_i}$. As argued from $T_{x_i}$, since the last instruction has been read from, the preceding read instructions of $T_{x_i}$ have been executed with the only reads-from relation being $\langle \text{Init}_1 : \mathbf{w}(v_i, 1) \rangle \text{ rf } \langle T_{\neg x_i} : \mathbf{r}(v_i, 1) \rangle$ and $\langle \text{Init}_0 : \mathbf{w}(v_i, 0) \rangle \text{ rf } \langle T_{\neg x_i} : \mathbf{r}(v_i, 0) \rangle$. However, this violates relaxed read coherence axiom, as $\langle \text{Init}_0 : \mathbf{w}(v_i, 0) \rangle \text{ mo } \langle \text{Init}_1 : \mathbf{w}(v_i, 1) \rangle$ but $\langle T_{\neg x_i} : \mathbf{r}(v_i, 1) \rangle \text{ po } \langle T_{\neg x_i} : \mathbf{r}(v_i, 0) \rangle$. This contradicts our assumption that there are two $\mathbf{r}(c_j, 1)$ and $\mathbf{r}(c_{\ell}, 1)$ reading from some $T_{x_i}$ and $T_{\neg x_i}$. Thus, the assignment induced by the $T_i^b$ threads executed before $T_f$ satisfies $\varphi$. $\square$

### C.3 NP-hardness for 2-WRITER systems

Given a 3-CNF-SAT formula $\varphi$ with $k$ variables and $m$ clauses, we construct an abstract execution $\bar{\mathbf{X}} = (\mathbf{E}, \text{po})$ with $2k + m + 3$ threads, accessing $k + 2m + 1$ memory locations $v_1, v_2, \dots, v_k, c_1, \dots, c_m, d_1, \dots, d_m, s$ and 2 values 0, 1 such that $\varphi$ is satisfiable iff $\bar{\mathbf{Y}}_{\varphi}^{\text{Relaxed}} \models \text{Relaxed}$. $\bar{\mathbf{Y}}_{\varphi}^{\text{Relaxed}}$ follows the general scheme depicted in Table 4.

<table><caption>Table 4: Threads in the reduction for Relaxed</caption><thead><tr><th>Init<sub>0</sub></th><th>Init<sub>1</sub></th><th></th><th></th><th></th></tr></thead><tbody><tr><td>w(v<sub>1</sub>, 0)</td><td>w(v<sub>1</sub>, 1)</td><td></td><td></td><td></td></tr><tr><td>w(v<sub>2</sub>, 0)</td><td>w(v<sub>2</sub>, 1)</td><td></td><td></td><td></td></tr><tr><td>...</td><td></td><td></td><td></td><td></td></tr><tr><td>w(v<sub>k</sub>, 0)</td><td>w(v<sub>k</sub>, 1)</td><td>T<sub>x<sub>i</sub></sub></td><td>T<sub>¬x<sub>i</sub></sub></td><td>T<sub>f</sub></td></tr><tr><td></td><td>r(s, 1)</td><td>r(v<sub>i</sub>, 0)</td><td>r(v<sub>i</sub>, 1)</td><td></td></tr><tr><td></td><td>w(v<sub>1</sub>, 0)</td><td></td><td></td><td>T<sub>j</sub></td></tr><tr><td></td><td>w(v<sub>2</sub>, 0)</td><td>w(c<sub>j</sub>/d<sub>j</sub>, 1)</td><td>w(c<sub>j</sub>/d<sub>j</sub>, 1)</td><td>r(d<sub>1</sub>, 1)</td></tr><tr><td></td><td>...</td><td>∀j ∈ S<sub>x<sub>i</sub></sub></td><td>∀j ∈ S<sub>¬x<sub>i</sub></sub></td><td>r(d<sub>2</sub>, 1)</td></tr><tr><td></td><td>w(v<sub>k</sub>, 0)</td><td>d<sub>j</sub> if x<sub>i</sub> is</td><td></td><td>...</td></tr><tr><td></td><td>w(v<sub>1</sub>, 1)</td><td>c<sub>j</sub></td><td>the third literal</td><td>w(s, 1)</td></tr><tr><td></td><td>w(v<sub>2</sub>, 1)</td><td></td><td>otherwise</td><td></td></tr><tr><td></td><td>...</td><td></td><td></td><td></td></tr><tr><td></td><td>w(v<sub>k</sub>, 1)</td><td></td><td></td><td></td></tr></tbody></table>
**Lemma 17.** $\varphi$ is satisfiable iff $\overline{\mathbb{Y}}_{\varphi}^{\text{Relaxed}} \models \text{Relaxed}$.

*Proof.* Suppose $A$ is a satisfying assignment for $\varphi$. Then, the execution proceeds as follows. The **rf** relation and **mo** relation are exactly as in Lemma 15, except the following. If $A(x_i) = \text{true}$:

$$- \langle T_f : \mathbf{w}(s, 1) \rangle \text{rf} \langle \text{Init}_1 : \mathbf{r}(s, 1) \rangle,$$

$$- \langle \text{Init}_1 : \mathbf{w}(v_i, 1) \rangle \text{rf} \langle T_{\neg x_i} : \mathbf{r}(v_i, 1) \rangle, \text{ and } \langle \text{Init}_1 : \mathbf{w}(v_i, 0) \rangle \text{rf} \langle T_{\neg x_i} : \mathbf{r}(v_i, 0) \rangle.$$

For clause variables $c_j$ and $d_j$, the **rf** (and consequently **mo**) relation depends on the literals set to true by $A$. For each clause $C_j$ there are two threads writing $\mathbf{w}(c_j, 1)$, and two threads writing $\mathbf{w}(d_j, 1)$.

If $A$ makes $\ell_j^3$ true then $\langle T_{\ell_j^3} : \mathbf{w}(d_j, 1) \rangle$ **rf** $\langle T_f : \mathbf{r}(d_j, 1) \rangle$. Otherwise $A$ makes $\ell_j^1$ or $\ell_j^2$ true. Let $\ell_j^k$ be the literal that is made true by the satisfying assignment $A$. Then, we have $\langle T_{\ell_j^k} : \mathbf{w}(c_j, 1) \rangle$ **rf** $\langle T_j : \mathbf{r}(c_j, 1) \rangle$ and $\langle T_j : \mathbf{w}(d_j, 1) \rangle$ **rf** $\langle T_f : \mathbf{r}(d_j, 1) \rangle$.

For every variable-value pair for $c_j$ and $d_j$, there are atmost two writes. With the **rf** picked as above, the **mo** relation gets fixed: the unused write in $T_x/T_{\neg x}$ that is set to true by $A$ is **mo**-before the used write, while if the unused write is in $T_x/T_{\neg x}$ that is set to false by $A$, then it is **mo**-after the used write.

**Relaxed Write-coherence.** From our construction, it is easy to see $\text{irr}(\text{mo}_x; \text{po})$.

**Relaxed Read-coherence.** We need to prove $\text{irr}(\text{rf}^{-1}; \text{mo}_x; \text{rf}^?; \text{po})$. The possible violating patterns and the arguments follow as in Lemma 15.

This yields an **rf** where all $\mathbf{r}(d_j, 1)$ in $T_f$ read from a thread corresponding to a true literal in $A$, so $\overline{\mathbb{Y}}_{\varphi}^{\text{Relaxed}} \models \text{Relaxed}$.

Conversely, suppose $\overline{\mathbb{Y}}_{\varphi}^{\text{Relaxed}} \models \text{Relaxed}$. The proof proceeds as in Lemma 15, where we show that if there are two clauses $C_j$ and $C_\ell$ such that $\mathbf{r}(d_j, 1)$ and $\mathbf{r}(c_\ell, 1)$ reading from some $T_{x_i}$ and $T_{\neg x_i}$, then relaxed read coherence is violated. $\square$

# D Causal Consistency Models

In this appendix, we study the consistency checking problem under the *causal consistency models* namely, CC, CM and CCv which come from distributed databases. We begin with a brief overview of the operational and axiomatic semantics of these models, and then show that the complexity landscape observed for the Release - Acquire (RA) variants extends to these models as well. Recall that for RA, we established a tight characterization of complexity with respect to the number of writer threads per memory location: 1-WRITER admits polynomial-time solutions, 2-WRITER is NP-hard, and 3-WRITER yields a stronger conditional lower bound. Our goal in this section is to establish analogous results for causal
consistency models, thereby showing that the same complexity results extend to CC, CM and CCv. Next, we provide an overview of these causal consistency models.

## D.1 Overview of Causal Consistency Models

In the domain of distributed systems, causality is the key concept for consistency. There are three popular causal models, namely, Causal Consistency (CC), Causal Convergence (CCv), and Causal Memory (CM) [4]. It is known that CC coincides with WRA while CCv coincides with SRA [15]. CM is stronger than CC and incomparable to CCv and RA.

In Causal Memory, each thread has a locally-consistent view of the order that different writes have been executed [2,4]. This is formalised by introducing an additional relation for each thread, called the “happened-before” relation in the literature. To avoid confusion with the “happens before” *hb*, we call this the *observed relation* *ob*.

To enhance understanding we define the notion of conflicting triplets first.

**Definition 18.** (Conflicting Triplet) Given an execution graph $\bar{X} = (E, \rho_0)$, two events in $E$ are called conflicting if both are on the same variable and at least one of them is a write. If also the reads-from function $rf$ is given, a Conflicting Triplet is defined as a tuple $(w, r, w')$ of pairwise conflicting events in $E$ such that $w \text{ rf } r$.

The observed relation *ob*. Given an event *e*, the *observed relation* for *e* is the smallest transitive relation $ob_e \subseteq E \times E$ with the following properties.

1. For every $(e_1, e_2) \in \text{hb}$ such that $(e_i, e) \in \text{hb}$ for each $i \in [2]$, we have $(e_1, e_2) \in \text{ob}_e$.

2. For every conflicting triplets $(w, r, w')$ such that: (ii) $(w', r) \in \text{ob}_e$ and (iii) $(r, e) \in \text{po}^?$, we have $(w', w) \in \text{ob}_e$.

The idea is that any thread which executes the read *r* must observe *w* after it has observed *w'* so that it does not read an obsolete value. For any event *e*, $ob_e$ contains *hb*, and *ob* grows monotonically as we move down a thread in *po*-order. That is, for any $(e_1, e_2) \in \text{po}$, we have $ob_{e_1} \subseteq ob_{e_2}$. For a thread *t*, the observed relation is defined as $ob_t = ob_{e_{max}}$, where $e_{max}$ is the po-maximal event of *t*. CM requires all the axioms of WRA, and in addition, requires that $ob_t$ is irreflexive [4]. Figure 9 depicts some examples.

$$ \text{PORF} \wedge (\text{weak-Rcoh}) \wedge (\text{ob-acyclicity}) \qquad [\text{CM}] $$

Thus, WRA $\leq$ CM. However, CM is incomparable with RA/SRA, i.e., CM allows executions that are inconsistent in RA/SRA and vice versa.

Since WRA = CC and SRA = CCv, both the fine-grained-hardness and NP-hardness result for WRA, SRA implies the same for CC and CCv. So we only need
<figure><img src="image_9.png" /><figcaption>Fig. 9: (a) is CM consistent as $ob_{t_1}, ob_{t_2}$ are acyclic. (b) is also CM consistent : the $w_1(x)ob_{t_2}w_2(x)$ is induced by $w_1(x)$ and $w_2(x)$ are both seen by $r(x)$. (c) is obtained from (b) by adding $w_1(z)$ and $r(z)$, and is CM inconsistent, since we have $w_1(z)$ positive with $w_2(z)$, $ob_{t_2}w_1(z)$. $w_2(z)$ positive with $w_1(z), r(z), w_2(z)$) with $w_2(z)$ positive with $r(z)$.</figcaption></figure>

to prove the hardness results for CM. In Section D.2, we discuss the polynomial-time algorithm for 1-WRITER programs and in Section D.3, we discuss the complexity results for 3-WRITER programs under CM. Note that the NP-hardness for 2-WRITER programs under CM follows from arguments analogous to those made in Section 4.2 for RA models, and therefore we do not discuss it separately.

For a CM-consistent execution graph the following should be satisfied: (PORF) ∧ (weak-Rcoh) ∧ (ob-acyclicity)

## D.2 1-WRITER programs under Causal Consistency

Recall that CM is essentially WRA with the extra axiom of *ob* acyclicity. We argue that the algorithm in Section 3.2 can be used for CM also. It is easy to see that any execution graph X which is CM-consistent is also WRA-consistent.

The other direction follows for the 1-WRITER case. Suppose X is WRA-consistent but violates *ob*<sub>t</sub> acyclicity for some thread *t*. Then we have both $w' ob_t w$ and $w ob_t w'$ for writes $w, w'$ on some location *x*.

By definition of $ob_t, w' ob_t w$ implies the existence of a conflicting triplet $(w, r, w')$ such that $w rf r, w' ob_t r, r po^? e_{max}$ where $e_{max}$ is the po-maximal element of *t*. Likewise, $w ob_t w'$ implies the existence of a conflicting triplet $(w', r', w)$ such that $w' rf r', w ob_t r', r' po^? e_{max}$ where $e_{max}$ is the po-maximal element of *t*. Since $w, w'$ are in the same thread, either $w po w'$ or $w' po w$. Either way, we observe one violation for weak-read-coherence wrt $r$ or $r'$. Thus, inconsistency wrt CM results in WRA inconsistency as well. Therefore, the algorithm for WRA can be employed for CM as well. Thus in case of 1-WRITER the time complexity of consistency testing will be same as that of WRA, $O(n^3)$.

Since $CC_v = SRA$ and $CC = WRA$, the lower bound result under BMM hypothesis in Section 3 holds for both $CC_v$ and $CC$. Finally, as mentioned previously, for
the single writer case, obtaining a cyclic $ob_t$ for a thread $t$ results in violation of weak-read-coherence. In the reduction given in Section 3, weak-read-coherence is violated in the presence of a triangle, hence, the result also holds for CM.

### D.3 Fine-grained Hardness under ETH for 3-WRITER systems

We will now discuss the fine-grained hardness of 3-WRITER-system under CM. Since CM is stronger than WRA, the soundness part of the reduction in Lemma 8 follows : Assume $\bar{X}_{\phi}^{RA} \models CM$. Then we know $\bar{X}_{\phi}^{RA} \models WRA$. Our soundness argument shows that $\phi$ is satisfiable.

For the completeness part, assume that $\phi$ is satisfiable. We have already synthesized an **rf**, **mo** which respect SRA(and hence WRA). We have to now show that, ob-acyclicity is preserved by the synthesized **rf**.

**Lemma 19.** If $\phi$ has a satisfying assignment, then $\bar{X}_{\phi}^{RA} \models CM$.

*Proof.* Let $A$ be the satisfying assignment for $\phi$. Say $A(x_i) = true$:

(i) For all pair of events in E, e **hb** e' we have e $ob_{T_f}$ e'

(ii) For the conflicting triplet ($(T_i^0 : w(s_i, 1))$, $(T_f : r(s_i, 1))$, $(T_i^1 : r(s_i, 2))$), we have $(T_i^1 : w(s_i, 2)) \ ob_{T_f} (T_f : r(s_i, 1))$ and $(T_f : r(s_i, 1)) \ po^? e_{max}^{T_f}$ where $e_{max}^{T_f}$ is the po-maximal event in $T_f$. This implies $(T_i^1 : w(s_i, 2)) \ ob_{T_f} (T_i^0 : w(s_i, 1))$.

As there are no **hb**-cycle and no members of $ob_{T_f}$ directed from $T_i^0$ to $T_i^1$, $ob_{T_f}$ is irreflexive.

If we consider the relation $ob_{T_{-x_i}}$, for the conflicting triplet ($(T_i^0 : w(v_i, 0))$, $(T_{x_i} : r(v_i, 0))$, $(T_i^1 : w(v_i, 1))$) we have $(T_i^1 : w(v_i, 1)) \ ob_{T_{-x_i}} (T_i^0 : w(v_i, 0))$.

Again no members of $ob_{T_{-x_i}}$ are directed from $T_i^0$ to $T_i^1$. As there is no **hb**-cycle, $ob_{T_{-x_i}}$ is also irreflexive.

It is easy to see that **ob** is irreflexive for all remaining threads. Hence ob-acyclicity is preserved by the synthesized **rf**

□

### D.4 NP-hardness for 2-WRITER systems

For 2-WRITER systems the reduction from 3-SAT instance has similar construction as that of WRA and the proof of the reduction will be on similar argument as the proof of the reduction for 3-WRITER.