1

# Optimal SMC for Transactional Programs

Parosh Aziz Abdulla  Uppsala UniversitySweden<EMAIL_ADDRESS>,  Mohamed
Faouzi Atig  Uppsala UniversitySweden<EMAIL_ADDRESS>,  Ashutosh
Gupta  IIT BombayIndia<EMAIL_ADDRESS>,  Shankaranarayanan Krishna  IIT
BombayIndia<EMAIL_ADDRESS>and  Omkar Tuppe  IIT BombayIndia
<EMAIL_ADDRESS>
###### Abstract.

The verification of transactional concurrent programs running over causally
consistent databases is a challenging problem. We present a framework for
efficient stateless model checking (SMC) of concurrent programs with
transactions under two well known models of causal consistency, ${\tt CCv}$
and ${\tt CC}$. Our approach is based on exploring the program order
${\color[rgb]{1,0,0}po}$ and the reads from ${\color[rgb]{0,0,1}\it{rf}}$
relations, avoiding exploration of all possible coherence orders. Our SMC
algorithm is provably optimal in the sense that it explores each
${\color[rgb]{1,0,0}po}$ and ${\color[rgb]{0,0,1}\it{rf}}$ relation exactly
once. We have implemented our framework in a tool called TranChecker.
Experiments show that TranChecker performs well in detecting anomalies in
classical distributed databases benchmarks.

causal consistency, stateless model checking, transactions

††journal: PACMPL††journalvolume: 1††journalnumber: CONF††article:
1††journalyear: 2018††publicationmonth: 1††ccs: Software and its engineering
General programming languages††ccs: Social and professional topics History of
programming languages

##  1\. Introduction

Transactions are a proven abstraction mechanism in database systems for
constructing reusable parallel computations. A transactional program is a
concurrent program, which has _transactions_ in the code of its processes.
Transactional programming (Harris et al., 2010) attempts to adapt the powerful
transaction processing technology originally developed for database
concurrency, to the setting of general purpose concurrent programs. Using
transactions as the main enabling construct for shared memory concurrency
obliviates the programmer from using low level mechanisms like locks, mutexes
and semaphores to prevent two concurrent threads from interfering.

A _transaction_ is a code segment consisting of several instructions which
must be executed _atomically_. Each process in a transactional program is a
sequence of transactions, written as
$\mathtt{t1}[\dots];\mathtt{t2}[\dots];\dots;\mathtt{tn}[\dots]$, where
$\mathtt{t}[\dots]$ represents a transaction, with the brackets [ and ]
demarcating the beginning and end. The general idea is that each process $p$
executes its transactions following the program order, and, when a process $p$
finishes executing a transaction $\mathtt{t}[\dots]$, it “delivers” the
writes/data updates made in $\mathtt{t}[\dots]$ to all processes. The manner
in which the receiving processes make use of this delivery is dependent on the
underlying consistency model of transactional programs.

The strongest consistency model is the one ensuring serializability
(Papadimitriou, 1979), where every execution of a program is equivalent to
another one where the transactions are executed serially one after the other,
with no interference. In the non-transactional setting, this model corresponds
to sequential consistency (SC) (Lamport, 1979). While serializability and SC
are easy to understand for programmers, they are too strong, since they need
global synchronization between all processes, which makes it difficult to
achieve good performance guarantees (Fischer et al., 1985; Gilbert and Lynch,
2002). Thus, modern databases ensure weaker consistency guarantees.

Causal consistency (Lamport, 1978), is a fundamental model implemented in many
leading production databases such as AntidoteDB, CockroachDB and MongoDB.
Unlike serializability, causal consistency allows conflicting transactions
having reads/writes to a common location to be executed in different orders by
different processes as long as they are not causally related. The sets of
updates visible to different processes may differ and read actions may return
values that cannot be obtained in SC executions. There are at least three
variations of causal consistency introduced in the literature, weak causal
consistency (CC) (Perrin et al., 2016; Bouajjani et al., 2017), causal memory
(CM) (Ahamad et al., 1995; Perrin et al., 2016), and causal convergence (CCv)
(Burckhardt, 2014). When one considers transactions to be single instructions,
${\tt CCv}$ is equivalent to SRA (strong release acquire), while ${\tt CC}$ is
equivalent to WRA (weak release acquire) (Lahav, 2019).

Figure 1.  // are assertions to be checked, based on values read.

Causal Consistency. We provide a gentle introduction to the 3 models here, via
the program in Figure 1. Two key notions needed across the models are that of
_causal delivery_ and _transaction isolation_. First, a _transaction log_ is a
sequence of all writes made in order, in a transaction. The log is reset
before a transaction begins, and every write $x:=v$ in the transaction appends
$(x,v)$ to the log. Thus, the log of $t3$ in Figure 1 is $(x,2)(z,2)$. In
causal delivery, if the log of a transaction $t$ is received by a process
before it starts executing a transaction $t^{\prime}$, then the log of $t$ is
received by all processes before receiving the log of $t^{\prime}$. Also, if
$t,t^{\prime}$ are two transactions in program order in a process $p$, with
$t^{\prime}$ coming later than $t$, then the log of $t$ is always
(self)delivered to $p$ before the execution of $t^{\prime}$. Transaction
isolation says that while a process is executing a transaction, it will not
receive any delivery. Thus, deliveries are received only when a process has
finished executing a transaction and not started executing the next
transaction. An execution under any of the 3 models respect causal delivery
and transaction isolation.

Each process has a _local store_ , keeping track of the latest values
delivered to it, per variable. Under ${\tt CM}$, whenever a process receives a
delivery, it updates its local store using the most recent values per variable
from the log received. When executing a read $r=x$ in transaction $t$, the
process first checks if a write to $x$ was made already in $t$, and if so,
reads the latest value written to $x$ in $t$, and if not, takes the value of
$x$ from the local store. The program in Figure 1 has a ${\tt CM}$ consistent
execution as seen in Figure 2.

Figure 2. A ${\tt CM}$-consistent execution for the program in Figure 1. A
configuration consists of the transaction log as well as the local store per
process. The transitions depict how a configuration changes when a transaction
is executed in a process, or when a process receives the delivery of the
transaction log from another process. Figure 3. The program in Figure 1 does
not have a ${\tt CCv}$ consistent execution. A process configuration consists
of the transaction log, the local store, as well as the time stamps of
variables. As in Figure 2, we depict transitions between configurations.

Figure 4. A ${\tt CC}$ consistent execution for the program in Figure 1. A
process configuration consists of the transaction log, the local store as well
as a snapshot of its local store. As for ${\tt CM},{\tt CCv}$, we depict
transitions between configurations.

$t1$ is executed first, then the log $(x,5)(x,1)$ of $t1$ is delivered to
$p1$, resulting in $x\mapsto 1,z\mapsto 0$ as $p1$’s local store. Then $t3$ is
executed in $p2$, and the log $(x,2)(z,2)$ is delivered to $p2$, resulting in
$x\mapsto 2,z\mapsto 2$ as $p2$’s local store. Next, we deliver $t1$’s log to
$p2$. On receiving the delivery, $p2$’s local store becomes $x\mapsto
1,z\mapsto 2$. Next, deliver the log of $t3$ to $p1$. On receiving the log of
$t3$, $p1$’s local store becomes $x\mapsto 2,z\mapsto 2$, and hence $r1$ can
read 2. Next, we deliver $t2$’s log to $p2$. On receiving the delivery, $p2$’s
local store becomes $x\mapsto 1,z\mapsto 1$, and hence $r2,r3$ can read 1,1
respectively.

In ${\tt CCv}$, transactions are totally ordered by unique ids
($\in\mathbb{N}$) associated to transactions. Transactions in program order of
a process have monotonically increasing ids. Each process $p$ maintains per
variable $x$, the timestamp of $x$, $\mathsf{ts}(x)$ which is the largest
transaction id among all transaction logs containing an $(x,v)$, delivered to
$p$. On receiving the delivery of a log from a transaction $t$, the value of
$x$ in the local store of process $p$ is updated with the latest value of $x$
in the log only if $\mathsf{ts}(x)$ in $p$ is smaller than $t.id$. In this
case, $\mathsf{ts}(x)$ is also updated to $t.id$. The program in Figure 1
cannot have a ${\tt CCv}$ consistent execution : we need to deliver the log of
$t1$ to $p2$ after $t3$ has been executed so that the value of $x$ read by
$r3$ can be 1. Likewise the log of $t3$ must be delivered to $p1$ after $t1$
is executed, so that $r1$ can read value 2. Both of these must take effect to
satisfy the assertion. Clearly with time stamps in place, this cannot happen :
either $t1.id>t3.id$ or $t3.id>t1.id$. If $t1.id>t3.id$, then the delivery of
the log of $t1$ to $p2$ after executing $t3$ is useless; likewise if we had
$t3.id>t1.id$, then delivering the log of $t3$ to $p1$ after execution of $t1$
is useless. Figure 3 depicts this.

In ${\tt CC}$, transaction ids are vector clocks. The local store of each
process is a set of triples of the form $(x,v,t.id)$, where $t.id$ is the
transaction id of the transaction which wrote $v$ to $x$. For each process
$p$, on receiving delivery of a log from a transaction $t$, (1) $(x,v,t.id)$
is added to the local store of $p$ if $t.id$ is incomparable with all the
transaction ids of existing triples in the store of $p$, (2) $(x,v,t.id)$
replaces all $(x,v^{\prime},t^{\prime}.id)$ triples in the store of $p$ if
$t.id>t^{\prime}.id$, and (3) $(x,v)$ is the latest write to $x$ in the log of
$t$. Each time a new transaction begins execution in a process $p$, it
maintains a “snapshot” of its local store, which assigns to each variable, the
latest value obtained, from considering a possible linearization of the store.
A read instruction $r=x$ in a transaction $t$ first checks its log for an
$(x,v)$. If that is unavailable ($t$ has not written to $x$), $r$ reads
$snapshot(x)$. The program in Figure 1 has a ${\tt CC}$ consistent execution
as seen below.

Choose incomparable vector clocks for $t1,t3$, say (1,0) and (0,1). Deliver
the log of $t1$ to $p2$ after $t3$ is executed, and the log of $t3$ to $p1$
after $t1$ is executed. The local store of $p2,p1$ will then be
$\\{(x,2,t3.id),(z,2,t3.id),(x,1,t1.id)\\}$. $p1$ can choose $snapshot(x)=2$
since $t1,t3$ is a linearization of the store, enabling the read of 2 in $r1$.
Next, choose $t2.id$ as (2,1), and execute $t2$. Deliver the log of $t2$ to
$p2$. Then $(z,1,t2.id)$ is added to the local store of $p2$. $p2$ can choose
$snapshot(x)=1,snapshot(z)=1$ since $t3,t1,t2$ is a linearization of the
store. This enables $r2,r3=1$.

##  2\. Related Work and Contributions

The main contribution of this paper is a Stateless Model Checking (SMC)
algorithm for transactional programs under causal consistency.

###  2.1. Related Work

We compare our contribution with two lines of work. On one hand, we review
work on the verification of causal consistency models, and on the other hand,
on SMC algorithms.

Figure 5. A non-transactional program and its Shasha-Snir traces.

There has been a spate of recent work on causal consistency models (Ahamad et
al., 1995). The question of verifying automatically, whether a given
transactional program is robust against causal consistency has been explored
in many papers, (Bernardi and Gotsman, 2016), (Brutschy et al., 2017),
(Brutschy et al., 2018), (Cerone and Gotsman, 2018), (Nagar and Jagannathan,
2018) via under and over approximation techniques. Checking robustness amounts
to asking whether the behaviours obtained while executing over a causally
consistent database are serializable. The latest in this direction providing a
precise robustness algorithm is (Beillahi et al., 2021b), which showed that
verifying robustness against causal consistency reduces to the reachability
problem under SC. As a means to analyse the robustness problem for ${\tt CC}$,
(Cerone et al., 2017) provide an algebraic connection between the operational
and axiomatic semantics of ${\tt CC}$. In the non-transactional setting,
(Lahav, 2019) surveys WRA (analogue of ${\tt CC}$), SRA (analogue of ${\tt
CCv}$) and discusses the operational and axiomatic semantics of both models.
(Raad et al., 2019) proposes a lock-based reference implementation for
_snapshot isolation_ (SI), a weak consistency model used in databases such as
Oracle and MS SQL server, while prior work (Raad et al., 2018) did the same
for _parallel snapshot isolation_ (PSI), a model closely related to snapshot
isolation. (Xiong et al., 2020) identify a consistency model _weak snapshot
isolation_ (WSI) that sits in between SI and PSI and propose an operational
semantics for client observable behaviours of atomic transactions. (Chong et
al., 2018) considers the interplay between weak memory and transactional
memory (Herlihy and Moss, 1993) by extending existing axiomatic weak memory
models (x86, Power, ARMv8, and C++) with new rules for transactional memory.
They also synthesize tests for validating these models on existing
implementations. Thus, there has been a lot of work on causal consistency
models in terms of checking robustness, providing operational/axiomatic
semantics as well as exploring the relationship between various models. Given
the widespread application of causal consistency models in distributed
databases, the verification of these models are of utmost importance.

In contrast to our paper, none of the earlier works provide algorithms that
can systematically explore all executions of a concurrent program under causal
consistency and certify them safe against concurrency bugs. We close this gap
here, by providing a stateless model checking (SMC) algorithm for
transactional programs under ${\tt CCv},{\tt CC}$.

SMC is a successful technique for finding concurrency bugs (Godefroid, 1997).
For a terminating program, SMC systematically explores all thread schedulings
that are possible during runs of the program. A runtime scheduler drives the
SMC exploration by making decisions on scheduling whenever such choices affect
interaction between threads. SMC has been implemented in many tools CHESS
(Musuvathi et al., 2008), Concuerror (Christakis et al., 2013), VeriSoft
(Godefroid, 2005), Nidhugg (Abdulla et al., 2015), CDSChecker (Norris and
Demsky, 2016), RCMC(Kokologiannakis et al., 2018), GenMC (Kokologiannakis and
Vafeiadis, 2021), rInspect (Zhang et al., 2015) and Tracer (Abdulla et al.,
2018). The number of possible schedulings grows exponentially with the
execution length in SMC. To counter this and reduce the number of explored
executions, the technique of _partial order reduction_ (Clarke et al., 1999;
Godefroid, 1996) has been proposed. This has been adapted to SMC as DPOR
(dynamic partial order reduction). DPOR was first developed for concurrent
programs under SC (Abdulla et al., 2014; Sen and Agha, 2006). Recent years
have seen DPOR adapted to language induced weak memory models such as RC11
(Kokologiannakis et al., 2018; Norris and Demsky, 2016), the release acquire
fragment of C11(Abdulla et al., 2018), as well as hardware-induced relaxed
memory models (Abdulla et al., 2015; Zhang et al., 2015). DPOR is based on the
observation that two executions are equivalent if they induce the same
ordering between conflicting events, and hence it is sufficient to consider
one such execution from each equivalence class. Under sequential consistency,
these equivalence classes are called _Mazurkiewicz_ traces (Mazurkiewicz,
1987), while for relaxed memory models, the generalization of these are called
_Shasha-Snir_ traces (Shasha and Snir, 1988). A Shasha-Snir trace
characterizes an execution of a concurrent program by three relations between
events : (1) ${\color[rgb]{1,0,0}po}$ program order, totally orders events of
each process, (2), ${\color[rgb]{0,0,1}\it{rf}}$ reads from, connects each
read with the write it reads from, (3) ${\color[rgb]{1,.5,0}co}$ coherence
order, totally orders writes to the same shared variable. Figure 5 gives a
program and its Shasha-Snir traces. Note that traces $\tau_{1}$ and $\tau_{2}$
differ only in ${\color[rgb]{1,.5,0}co}$. These two traces can be considered
equivalent since each process goes through the same local states in both
traces : note that the values read by $a,b$ are the same in both
$\tau_{1},\tau_{2}$, and to check an assertion on the local variables $a,b$,
the ${\color[rgb]{1,.5,0}co}$ relation does not matter. An optimal DPOR should
only explore $\tau_{6}$, ignoring the ${\color[rgb]{1,.5,0}co}$ relation,
rather than exploring both $\tau_{1},\tau_{2}$.

In recent years, there has been much interest in DPOR algorithms : (Abdulla et
al., 2019) for SC, (Kokologiannakis and Vafeiadis, 2021) for the release
acquire semantics, (Silva and Leino, 2021) for C/C++, and (Kokologiannakis et
al., 2022) for TSO, PSO and RC11. However, none of these work for
transactional programs, which is the subject of this paper. As we describe in
Section 2.2, extending these to work in the transactional setting has many non
trivial tasks to be accomplished.

###  2.2. Challenges and Contributions

We now summarize the main challenges in the development of our DPOR algorithm.

Axiomatization and equivalence with operational semantics. The first step to a
DPOR for transactional programs is to have an axiomatization of the causal
consistency semantics. To this end, we provide a generalization of Shasha-Snir
traces to work for transactional programs under causal consistency, by
extending the
${\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}\it{rf}},{\color[rgb]{1,.5,0}co}$
relations to transactions. Then we define the notions of ${\tt CCv},{\tt CC}$
consistent traces. Using this notion of traces, we provide an axiomatic
semantics for ${\tt CCv},{\tt CC}$ and prove their equivalence with their
known operational semantics (Beillahi et al., 2021b).

Exploring weak traces. Building up on the notion of traces, our algorithm
focuses only on exploring so called weak traces. For a trace $\tau$, dropping
the ${\color[rgb]{1,.5,0}co}$ relations gives the corresponding weak trace
$weak(\tau)$ (Abdulla et al., 2018). Mazurkiewicz traces have the disadvantage
of often being too strong. More precisely, they induce an equivalence relation
that is unnecessarily fine for checking typical properties such as program
errors or assertion violations. The equivalence relation includes coherence
order, i.e., the order in which write events on shared variables reach the
memory. Coherence order is irrelevant for checking the above properties, and
hence using Mazurkiewicz traces is a large source of redundancy, inherently
limiting the efficiency that can possibly be achieved in the analysis.

Keeping this in mind, in the non-transactional setting the idea of exploring
only weak traces, that is, those in the equivalence classes induced by
${\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}\it{rf}}$ is preferred as a way to
obtain optimality on the number of explored traces (Abdulla et al., 2018),
(McKinley and Fisher, 2019), (Kokologiannakis et al., 2022). Making this work
in the transactional setting is one of the challenges we overcome here. One of
the main difficulties while working with weak traces is to determine which
continuations of a currently explored trace will allow a coherence order that
makes the trace consistent with ${\tt CCv},{\tt CC}$. Prior work in the non-
transactional setting with weak traces proceeded by adding only those
${\color[rgb]{1,.5,0}co}$ edges which are necessary to check if the trace is
consistent with the model. The difficulty and complexity of this consistency
check differs from one model to another. For instance, it is polynomial for
release acquire (Abdulla et al., 2018), while for SC it is NP-complete
(Chalupa et al., 2017). We need to tackle this in the setting of transactional
programs.

To solve this question for transactional programs under ${\tt CCv}$ and ${\tt
CC}$, we define a notion of _fulfilment_ , which decides which
${\color[rgb]{1,.5,0}co}$ edges must be added while extending a trace so that
the resultant traces preserve ${\tt CCv},{\tt CC}$ consistency. On adding
these necessary ${\color[rgb]{1,.5,0}co}$ edges, the traces become fulfilled
traces. During exploration, DPOR algorithm maintains a fulfilled version of
the currently explored weak trace, and we precisely examine those weak traces
which are ${\tt CCv},{\tt CC}$ consistent. Adding a write event to a fulfilled
trace results in a fulfilled trace, while, adding a read event to a fulfilled
trace requires care in choosing write events it can read from, so that the
resultant trace remains fulfilled after adding the
${\color[rgb]{0,0,1}\it{rf}}$ edge. We identify which transactions can be read
from by computing the _readable sets_ for each read event. After adding the
${\color[rgb]{0,0,1}\it{rf}}$ edge, some ${\color[rgb]{1,.5,0}co}$ edges are
necessary to be added from transactions in the readable set to the remaining
transactions, so that the trace remains fulfilled. In contrast to the non-
transactional case, it is non-trivial to determine, (i) which transaction can
be read from (to add the ${\color[rgb]{0,0,1}\it{rf}}$ edge) and (ii) which
${\color[rgb]{1,.5,0}co}$ edges should be added. We show that computing a
${\tt CCv},{\tt CC}$ consistent successor trace of a given fulfilled trace can
be done in polynomial time, making our trace exploration efficient. For ${\tt
CM}$, this is work in progress.

A sound, complete and optimal DPOR algorithm for ${\tt CCv},{\tt CC}$. We show
that our ${\tt CCv},{\tt CC}$ DPOR algorithms are s.t. (i) each ${\tt
CCv},{\tt CC}$ consistent weak trace is explored exactly once (optimality),
(ii) all the explored traces are ${\tt CCv},{\tt CC}$ consistent (soundness),
(iii) if $\rho$ is a terminating execution corresponding to a total ${\tt
CCv},{\tt CC}$ consistent trace $\tau$, then the algorithm explores a trace
$\tau^{\prime}$ such that $weak(\tau)=weak(\tau^{\prime})$(completeness).

The first SMC tool for ${\tt CCv},{\tt CC}$. We have implemented our fulfilled
semantics and DPOR in a tool TranChecker, by extending Nidhugg, an SMC tool
for multithreaded C/C++ programs based on LLVM. First, as a sanity check we
ran TranChecker on known litmus tests (Alglave et al., 2014) adapting them to
the transactional setting (Section 7.1). Then we proceeded with experimental
evaluation on a wide range of benchmarks from distributed databases. We showed
that (i) TranChecker correctly detects known transaction anamolies (Bernardi
and Gotsman, 2016), (Biswas and Enea, 2019), (Beillahi et al., 2021b) and
(Beillahi et al., 2021a) under ${\tt CCv}$ and ${\tt CC}$ (Section 7.2),
(ii)TranChecker correctly detects known bugs in applications using
transactions (Difallah et al., 2013), (Holt et al., 2016), (Beillahi et al.,
2021b), (Nair et al., 2020) (Section 7.3). To the best of our knowledge,
TranChecker is the first SMC tool for transactional concurrent programs.

##  3\. Causal Consistency

_Program Syntax_. We consider transactional programs $\mathcal{P}$ consisting
of a finite set of _threads_ or _processes_ $p\in\mathbf{P}$ that share a
finite set of shared variables $\mathcal{V}$ over a data domain $\mathcal{D}$.
Each process has a finite set of local registers that store values from
$\mathcal{D}$. Each process runs a deterministic code, built in a standard way
from expressions and atomic commands, using standard control flow constructs
(sequential composition, selection, and bounded loop constructs). We use $x,y$
for shared variables, $r,r1,r2,r3\dots$ for local registers and $e$ for
expressions. Expressions are only over local registers.

Each process is a sequence of _transactions_ and each transaction is a
sequence of _labeled instructions_ $\mathsf{Lab}$. Let $\mathcal{T}$ denote
the set of all transactions in $\mathcal{P}$. A transaction $t\in\mathcal{T}$
in process $p$ starts with a $\mathtt{begin}$$(p,t)$ instruction and ends with
an $\mathtt{end}$$(p,t)$ instruction (in the figures, we simply denote these
by opening and closing braces [ and ]). The instructions between the
$\mathtt{begin}$ and $\mathtt{end}$ instructions can be write/read/assign
instructions. Write instructions $x:=e$ write to the shared variable $x$ while
read instructions $r:=x$ read from the shared variables $x$. Assignments have
the form $r:=e$ involving local registers and expressions. We assume that the
control cannot pass from one transaction to another without going through
$\mathtt{begin}$ and $\mathtt{end}$ instructions.

_Program Semantics_. Each process maintains its own local valuation of the
shared variables, called its _local store_. The local store of each process
consists of pairs $(x,v)$ corresponding to each shared variable $x$, and its
value $v$. During the execution of a transaction, writes made to the shared
variables are stored in a _transaction log_
$\in(\mathcal{V}\times\mathcal{D})^{*}$ which is visible only to the process
executing the transaction, and is broadcast to all processes at the end of the
transaction.

A configuration is defined as the tuple
$\sigma=\langle\mathsf{ls},\mathsf{msgs}\rangle$, where $\mathsf{ls}$ is a
mapping from processes $p\in\mathbf{P}$ to their local states. $\mathsf{msgs}$
is a set of ‘messages in transit’ of the form $m=(t.id,log)$, where $t.id$ is
a transaction identifier and $log\in(\mathcal{V}\times\mathcal{D})^{*}$. The
local state $\mathsf{ls}(p)$ of a process $p$ defined as
$\mathsf{ls}(p)=(\mathsf{pc},\mathsf{log},\mathsf{store},\mathsf{rval})$
consists of (i) the program counter $\mathsf{pc}\in\mathsf{Lab}$ which gives
the label of the next instruction to be executed, (ii) $\mathsf{log}$ is the
transaction log which is a sequence of (shared variable,value) pairs, (iii)
$\mathsf{store}:\mathcal{V}\rightarrow\mathcal{D}$ is the local store of a
process, (iv) $\mathsf{rval}$ is the valuations of local registers. For
$k\in\\{\mathsf{pc},\mathsf{log},\mathsf{store},\mathsf{rval}\\}$,
$\mathsf{ls}(p).k$ represents the respective component of $\mathsf{ls}(p)$. A
$\mathsf{begin}({p},{t})$ instruction affects only the transaction log of $p$
by resetting it (makes $\mathsf{ls}(p).\mathsf{log}=\epsilon$). Each time a
write $x:=v$ is performed in the current transaction of $p$, $(x,v)$ is
appended to $\mathsf{ls}(p).\mathsf{log}$. A read from a shared variable $x$
in a process ${p}$ first accesses $\mathsf{ls}(p).\mathsf{log}$ and takes the
latest written value on $x$, if any. In case the current transaction does not
have any writes on $x$, it takes the value from its local store
$\mathsf{ls}(p).\mathsf{store}$. The last instruction in a transaction $t$ of
process $p$ is $\mathtt{end}$$(p,t)$. On $\mathtt{end}$$(p,t)$, we add
$(t.id,\mathsf{ls}(p).\mathsf{log})$ to $\mathsf{msgs}$.
$(t.id,\mathsf{ls}(p).\mathsf{log})\in\mathsf{msgs}$ is delivered to $p$
(denoted $\mathsf{del}(p,t)$) before $p$ chooses the next transaction to
execute. Apart from the self delivery of $t$, any other message from
$\mathsf{msgs}$ can also be delivered to $p$ before it begins a fresh
transaction. The delivery of
$(t.id,\mathsf{ls}(p).\mathsf{log})\in\mathsf{msgs}$ to a process $p^{\prime}$
is denoted by the event $\mathsf{del}(p^{\prime},t)$. When a process
$p^{\prime}$ receives this delivery, the last write on a variable $x$ from
$\mathsf{ls}(p).\mathsf{log}$ is applied on the local store
$\mathsf{ls}(p^{\prime}).\mathsf{store}$. Delivery of transaction logs respect
causal delivery and transaction isolation, as described below.

Figure 6. The operational semantics for ${\tt CCv}$ (Beillahi et al., 2021b).
We assume that all the events which come from the same transaction use a
unique transaction identifier ${t}$. For a function $f$, we use $f[a\mapsto
b]$ to denote a function $g$ such that $g(c)=f(c)$ for all $c\neq a$ and
$g(a)=b$. The function ${\mathsf{inst}}$ returns the set of instructions
labeled by some given label while $\mathsf{next}$ gives the next instruction
to execute. We use $\cdot$ to denote sequence concatenation. The function
$\mathit{eval}(\mathsf{ls}({p}),x)$ returns the value of $x$ in the local
state $\mathsf{ls}({p})$: (1) if $\mathsf{ls}({p}).\mathsf{log}$ contains a
pair $(x,v)$, for some $v$, then $\mathit{eval}(\mathsf{ls}({p}),x)$ returns
the value of the last such pair in $\mathsf{ls}({p}).\mathsf{log}$, and (2)
$\mathit{eval}(\mathsf{ls}({p}),x)$ returns
$\mathsf{ls}({p}).\mathsf{store}(x)$, otherwise. Also,
$\mathit{last}(\mathit{log},x)$ returns the value $v$ in the last pair $(x,v)$
in $\mathit{log}$, and $\bot$, if such a pair does not exist.

_Events_. The operational semantics (Beillahi et al., 2021b) is defined as a
labeled transition system over configurations. Each transition corresponds
either to a process executing an instruction in its current transaction, or
delivering a transaction log. The transition from configuration $\sigma$ to
configuration $\sigma^{\prime}$ is symbolized by
$\sigma\xrightarrow[]{\ell}\sigma^{\prime}$.

Here configuration $\sigma^{\prime}$ is the successor of configuration
$\sigma$ and $\ell$ is the label of the transition. The labels come from a set
of events $\\{$$\mathtt{begin}$$(p,t)$, $\mathtt{end}$$(p,t)$,
$\mathtt{del}$$(p,t)$, $w(p,t,x,v),r(p,t,x,v)\\}$, where $p\in\mathbf{P}$,
$t\in\mathcal{T}$, $x\in\mathcal{V}$, and $v\in\mathcal{D}$.
$\mathtt{begin}$$(p,t)$, $\mathtt{end}$$(p,t)$ represent the begin, end of
transaction $t$ in process $p$ and $\mathtt{del}$$(p,t)$ represents delivery
of the transaction log (of transaction $t$), to process $p$.
$w(p,t,x,v),r(p,t,x,v)$ respectively represent write and read events of
variable $x$ in transaction $t$ of process $p$, writing or reading value
$v\in\mathcal{D}$. For an event $ev$ of the form $w(p,t,x,v)$ or $r(p,t,x,v)$
we define by $ev.var=x$, $ev.trans=t$, $ev.type=W$ or $ev.type=R$ and
$ev.process=p$. We define a special transaction which has only write events of
the form $init_{x}=w(-,-,x,0)$, called $initializer$, which initializes all
shared variables $x$ with 0.

_The transition relation_. The labeled transition system (LTS) corresponding
to program $\mathcal{P}$ is defined as
$\mathrm{LTS}[\mathcal{P}]=(\mathcal{G},Ev,\mathcal{G}_{0},\rightarrow)$ where
$\mathcal{G}$ is the set of configurations, $Ev$ is the set of events due to
which transitions on configurations occur, $\mathcal{G}_{0}$ denotes initial
configurations, and $\rightarrow$ is the transition relation. In the
$\mathrm{LTS}$, each transition $\rightarrow$ corresponds to a change in
configuration after executing an event from $Ev$. An execution $\rho$ of a
program from a configuration $\sigma\in\mathcal{G}$ is a transition sequence
of configurations where each transition is due to one of the events in $Ev$.

The transitions involving $\mathtt{del}$$(p,t)$ represent the delivery of the
messages in transit. An execution satisfies _transaction isolation_ and
_causal delivery_ as explained below.

  * $\bullet$

$Transaction$ $isolation$. No deliveries to $p$ happen when $p$ is executing a
transaction $t$; there are no events $\mathsf{del}(p,t^{\prime})$ between
$\mathtt{begin}$$(p,t)$ and $\mathtt{end}$$(p,t)$.

  * $\bullet$

An execution $\rho$ satisfies _causal delivery_ if the following hold.

    * (i)

corresponding to any $\mathtt{begin}$$(p,t)$, $\rho$ contains at most one
event $\mathtt{del}$$(p^{\prime},t)$. That is, each transaction $t$ which is
executed in a process $p$ is delivered to a process $p^{\prime}$ at most once.

    * (ii)

For any two events $\mathtt{begin}$$(p,t)$ and
$\mathtt{begin}$$(p,t^{\prime})$ if $\mathtt{begin}$$(p,t)$ occurs in $\rho$
before $\mathtt{begin}$$(p,t^{\prime})$, then $\mathtt{del}$$(p,t)$ occurs
before $\mathtt{begin}$$(p,t^{\prime})$. Thus, $p$ stores the writes of $t$ in
$\mathsf{ls}(p).store$ before issuing another transaction $t^{\prime}$.

    * (iii)

for events $ev_{1}\in\\{$$\mathtt{del}$$(p,t_{1})$,
$\mathtt{end}$$(p,t_{1})\\}$, $ev_{2}$=$\mathtt{begin}$$(p,t_{2})$,
$ev^{\prime}_{2}=$$\mathtt{del}$$(p^{\prime},t_{2})$ with $p\neq p^{\prime}$,
if $ev_{1}$ occurs in execution $\rho$ before $ev_{2}$, then there exists
$ev^{\prime}_{1}=$$\mathtt{del}$$(p^{\prime},t_{1})$ such that
$ev^{\prime}_{1}$ occurs before $ev^{\prime}_{2}$ in $\rho$. That is, if
$t_{1}$ is delivered to $p$ before executing $t_{2}$ in $p$, or if $t_{1}$
finishes in $p$ before starting $t_{2}$, then for any process $p^{\prime}\neq
p$, $t_{1}$ is delivered before $t_{2}$.

Terminal configurations are those from which no transitions are available. An
$execution$ $\rho$ of a program starts from an initial configuration
$\sigma_{0}\in\mathcal{G}_{0}$ and is a sequence of transitions,
$\sigma_{0}\xrightarrow[]{\ell_{1}}\sigma_{1}\xrightarrow[]{\ell_{2}}\sigma_{2}\xrightarrow[]{\ell_{3}}\sigma_{3}\cdots\xrightarrow[]{\ell_{n-1}}\sigma_{n-1}\xrightarrow[]{\ell_{n}}\sigma_{n}$,
where $\sigma_{n}$ is a terminal configuration, and
$\ell_{i}\in\mathsf{Ev}(\rho)$, where
$\mathsf{Ev}(\rho)=\\{$$\mathtt{begin}$$(p,t)$, $\mathtt{end}$$(p,t)$,
$\mathtt{del}$$(p,t)$, $w(p,t,x,v),r(p,t,x,v)\\}$ is the set of all events
from $\rho$. Let $\mathcal{T}(\rho)$ be the set of all transactions
participating in $\rho$. Let $\mathcal{T}({\rho})^{w,x}$
($\mathcal{T}({\rho})^{r,x}$) be all transactions in $\mathcal{T}(\rho)$
having a write (read) instruction on variable $x$, and let
$\mathcal{T}({\rho})^{w}=\bigcup_{x\in\mathcal{V}}\mathcal{T}({\rho})^{w,x}$
($\mathcal{T}({\rho})^{r}=\bigcup_{x\in\mathcal{V}}\mathcal{T}({\rho})^{r,x}$).
Denote by ${\tt ExecFrom}(\sigma)$ all executions starting from configuration
$\sigma$.

Causal Memory Semantics(${\tt CM}$). The set of executions of
$LTS[\mathcal{P}]$ under causal memory, denoted $\mathsf{Exec}_{{\tt
CM}}(\mathcal{P})$ are those executions satisfying transaction isolation and
causal delivery.

###  3.1. Causal Convergence Semantics(${\tt CCv}$)

In ${\tt CCv}$, each transaction $t$ in a process is identified by a unique
_transaction identifier_ $t.id\in\mathbb{N}$, totally ordering all
transactions

The transaction identifiers are totally ordered according to some relation
$<$.

(i) The local state $\mathsf{ls}(p)$ of a process $p$ defined as
$\mathsf{ls}(p)=(\mathsf{pc},\mathsf{log},\mathsf{store},\mathsf{rval},\mathsf{ts})$,
where the first 4 components are as before, and
$\mathsf{ts}\in\mathbb{N}^{|\mathcal{V}|}$ is the tuple of the largest time
stamps the process has seen per variable. Initially, we assume
$\mathsf{ls}(p).\mathsf{ts}(x)=0$ for all variables $x$ and processes $p$.

(ii) A $\mathsf{begin}({p},{t})$ transition will choose a transaction
identifier ${t}.id>\mathsf{ls}(p).\mathsf{ts}(x)$ for all $x\in\mathcal{V}$.
(iii) When a process $p$ receives the delivery of a $log$ corresponding to
transaction $t$, the last write on a variable $x$ from $log$ is applied on the
local store $\mathsf{ls}(p).store$ only if
$\mathsf{ls}(p).\mathsf{ts}(x){<}t.id$, and in this case,
$\mathsf{ls}(p).\mathsf{ts}(x)$ is updated to $t.id$.

_${\tt CCv}$ executions_. The set of executions of $LTS[\mathcal{P}]$ under
causal convergence, denoted $\mathsf{Exec}_{{\tt CCv}}(\mathcal{P})$ are those
executions satisfying transaction isolation, causal delivery, and which
guarantees that each process generates monotonically increasing transaction
identifiers. Figure 6 gives the transition rules under ${\tt CCv}$.

###  3.2. Weak Causal Consistency Semantics(${\tt CC}$)

In ${\tt CC}$, each transaction $t$ is identified by a unique transaction
identifier $t.id$ given as a _vector clock_ (Lamport, 1978), which play the
role of timestamps, and are partially ordered according to some relation $<$.
Define ${t}_{1}.id<{t}_{2}.id$ iff $t_{1}$ is delivered to the process of
$t_{2}$ before $t_{2}$ begins. $t_{1},t_{2}$ are _concurrent_ if $t_{1}.id$ is
incomparable to $t_{2}.id$.

(i)
$\mathsf{store}:\mathcal{V}\rightarrow\mathfrak{p}(\mathcal{D}\times\mathcal{T})$
: the local store of each process $p$ maintains for each variable $x$, a set
of pairs, having the value $v$ written along with the transaction which wrote
it. Thus, the local store of $p$ wrt $x$ is a set of pairs $(v,t.id)$. On
applying the log of a transaction $t$ on the local state of the receiving
process $p$, for each $x$, $\mathsf{ls}(p).\mathsf{store}(x)$ is updated to
contain $(v_{x},t.id)$, where $v_{x}$ is the most recent value for $x$ in the
log, along with all $(v,t^{\prime}.id)$ that were present earlier in it, such
that $t^{\prime},t$ are concurrent.

(ii) The local state $\mathsf{ls}(p)$ of a process $p$ is
$\mathsf{ls}(p)=(\mathsf{pc},\mathsf{log},\mathsf{store},\mathsf{rval},\mathsf{ts},\mathsf{snapshot})$
where $\mathsf{pc},\mathsf{log},\mathsf{rval}$ are as before, $\mathsf{store}$
is as above, $\mathsf{ts}$ is a vector clock which dominates all the $t.id$s
from all pairs $(v,t.id)\in\mathsf{ls}(p).\mathsf{store}(x)$ for all $x$. A
new transaction $t$ which begins in a process $p$ chooses
$t.id>\mathsf{ls}(p).\mathsf{ts}$. Lastly,
$\mathsf{snapshot}:\mathcal{V}\rightarrow(\mathcal{D}\times\mathcal{T})$ maps
each shared variable $x$ to a single pair $(v,t.id)$.
$\mathsf{ls}(p).\mathsf{snapshot}$ is obtained by taking a “consistent”
snapshot from $\mathsf{ls}(p).\mathsf{store}$ when a new transaction begins in
$p$. $\mathsf{ls}(p).\mathsf{snapshot}$ corresponds to a linearization of the
transactions that were delivered to $p$, and consistent with the vector clock
order. The snapshot associates to each $x\in\mathcal{V}$ the last value
written in this linearization. When $p$ does a read from $x\in\mathcal{V}$, it
looks first at $\mathsf{ls}(p).\mathsf{log}$ and then, at
$\mathsf{ls}(p).\mathsf{snapshot}(x)$.

_${\tt CC}$ executions_. The set of executions of $LTS[\mathcal{P}]$ under
${\tt CC}$, denoted $\mathsf{Exec}_{{\tt CC}}(\mathcal{P})$ are those
executions satisfying transaction isolation and causal delivery, apart from
respecting the above mentioned conditions on updating the $\mathsf{store}$ and
$\mathsf{snapshot}$, which decides which values can be read. The formal
operational semantics of ${\tt CC}$ are available in the appendix.‘

### An Example to illustrate ${\tt CCv}$

Figure 7. ${\tt CCv}$ Example

Consider the progam in Figure 7. In the initial configuration
$(\mathsf{ls},\mathsf{msgs})$, we have
$\mathsf{ls}(p_{1}).\mathsf{log},\mathsf{ls}(p_{2}).\mathsf{log}$ are both
$\epsilon$,
$\mathsf{ls}(p_{1}).\mathsf{store},\mathsf{ls}(p_{2}).\mathsf{store}$ are both
$x\mapsto 0,y\mapsto 0,z\mapsto 0$, and
$\mathsf{ls}(p_{1}).\mathsf{rval},\mathsf{ls}(p_{2}).\mathsf{rval}$ assign 0
to all local registers. Finally, $\mathsf{ls}(p_{i}).\mathsf{ts}(\alpha)=0$
for both $i=1,2$ and $\alpha\in\\{x,y,z\\}$. $\mathsf{msgs}$ is empty (and
will be populated whenever a transaction ends).

Consider the ${\tt CCv}$ execution where transaction $t_{1}$ is executed
choosing $t_{1}.id=1$. After the first write,
$\mathsf{ls}(p_{1}).\mathsf{log}=(x,1)$, and after the second write,
$\mathsf{ls}(p_{1}).\mathsf{log}=(x,1)\cdot(y,1)$. At the end of $t_{1}$,
$\mathsf{msgs}=\\{(1,(x,1)\cdot(y,1))\\}$. This is followed by
$\mathsf{del}(p_{1},t_{1})$, updating $\mathsf{ls}(p_{1}).\mathsf{store}$ to
$x\mapsto 1,y\mapsto 1,z\mapsto 0$, and $\mathsf{ls}(p_{1}).\mathsf{ts}(x)$ as
well as $\mathsf{ls}(p_{1}).\mathsf{ts}(y)=1$. Next execute $t_{2}$ choosing
$t_{2}.id=2$, resetting $\mathsf{ls}(p_{1}).\mathsf{log}$. The write $z=1$
results in $\mathsf{ls}(p_{1}).\mathsf{log}=(z,1)$. The read in $t_{2}$ picks
up $(x,1)$ from the local store $\mathsf{ls}(p_{1}).\mathsf{store}$ of $p_{1}$
since the log does not have an $x$ entry. At the end of $t_{2}$, $(2,(z,1))$
is added to $\mathsf{msgs}$, and we have $\mathsf{del}(p_{1},t_{2})$, updating
$\mathsf{ls}(p_{1}).\mathsf{store}$ to $x\mapsto 1,y\mapsto 1,z\mapsto 1$ and
$\mathsf{ls}(p_{1}).\mathsf{ts}(z)=2$.

Next execute $t3$ choosing $t_{3}.id=3$. After the write to $y$ in $t_{3}$,
$\mathsf{ls}(p_{2}).\mathsf{log}=(y,2)$. The read in $t3$ picks $(x,0)$ from
$\mathsf{ls}(p_{2}).\mathsf{store}$. At the end of $t_{3}$, $(3,(y,2))$ is
added to $\mathsf{msgs}$, and we have $\mathsf{del}(p_{2},t_{3})$, updating
$\mathsf{ls}(p_{2}).\mathsf{store}$ to $x\mapsto 0,y\mapsto 2,z\mapsto 0$, and
$\mathsf{ls}(p_{2}).\mathsf{ts}(y)$ to 3. This is followed by
$\mathsf{del}(p_{2},t_{1})$, delivering $(1,(x,1)\cdot(y,1))$ to $p_{2}$.
Since $\mathsf{ls}(p_{2}).\mathsf{ts}(x)=0<1=t_{1}.id$, the value $x\mapsto 1$
is used to replace the local store of $p_{2}$ wrt $x$. However since
$\mathsf{ls}(p_{2}).\mathsf{ts}(y)=3>1=t_{1}.id$, the local store of $p_{2}$
is not changed wrt $y$, and the value $(y,1)$ is not chosen from
$(1,(x,1)\cdot(y,1))$. Thus, $\mathsf{ls}(p_{2}).\mathsf{store}$ is updated to
$x\mapsto 1,y\mapsto 2,z\mapsto 0$. This is followed by
$\mathsf{del}(p_{2},t_{2})$. $z\mapsto 1$ will replace $z\mapsto 0$ in
$\mathsf{ls}(p_{2}).\mathsf{store}$ since
$\mathsf{ls}(p_{2}).\mathsf{ts}(z)=0<2=t_{2}.id$. Last, execute $t_{4}$
choosing $t_{4}.id=4$, and both reads happen from the local store
$\mathsf{ls}(p_{2}).\mathsf{store}$.

### An Example to illustrate ${\tt CC}$

Let us look at the program in Figure 8 for a ${\tt CC}$ execution. The
transactions ids are ordered pairs (since we have 2 processes). The initial
$\mathsf{store}$ for $p_{1}$ and $p_{2}$ is $\\{(x,0,init)$, $(y,0,init)$,
$(z,0,init)\\}$ the last component signifying that the value 0 is the initial
value.

Begin with $t_{1}.id=(1,0)$. At the end of $t_{1}$,
$\mathsf{ls}.\mathsf{log}(p_{1})=(x,5)\cdot(x,1)\cdot(y,1)$. Deliver $t_{1}$
to $p_{1}$, $\mathsf{del}(p_{1},t_{1})$ obtaining
$\\{(x,1,(1,0)),(y,1,(1,0)),(z,0,init)\\}$ as
$\mathsf{ls}.\mathsf{store}(p_{1})$. The only consistent $\mathsf{snapshot}$
from $\mathsf{ls}.\mathsf{store}(p_{1})$ is
$\mathsf{ls}.\mathsf{snapshot}(p_{1})(x)=(1,(1,0))$,
$\mathsf{ls}.\mathsf{snapshot}(p_{1})(y)=(1,(1,0))$ and
$\mathsf{ls}.\mathsf{snapshot}(p_{1})(z)=(0,init)$.

Figure 8. ${\tt CC}$ Example, not ${\tt CCv}$

Next execute $t_{2}$ in $p_{1}$, with $t_{2}.id=(1,1)$ obtaining
$\mathsf{ls}.\mathsf{log}(p_{1})=(z,1)$. The read is taken from the snapshot
$\mathsf{ls}.\mathsf{snapshot}(p_{1})(x)$. This is followed by
$\mathsf{del}(p_{1},t_{2})$. Next, execute $t_{3}$ with $t_{3}.id=(0,1)$. At
the end of $t_{3}$, $\mathsf{ls}.\mathsf{log}(p_{2})=(y,2)$. On
$\mathsf{del}(p_{2},t_{3})$, we obtain $\mathsf{ls}.\mathsf{store}(p_{2})$ as
$\\{(x,0,init)$, $(y,2,(0,1))$, $(z,0,init)\\}$. Next deliver $t_{1}$ to
$p_{2}$, $\mathsf{del}(p_{2},t_{1})$. Then $\\{(x,1,(1,0)),(y,1,(1,0))\\}$
should be added to $\mathsf{ls}.\mathsf{store}(p_{2})$. Since $t_{1},t_{3}$
are concurrent, we obtain $\mathsf{ls}.\mathsf{store}(p_{2})$ as
$\\{(x,1,(1,0)),(y,1,(1,0))$, $(y,2,(0,1)),(z,0,init)\\}$. Next, on
$\mathsf{del}(p_{2},t_{2})$, $(z,1,(1,1))$ replaces $(z,0,init)$ in
$\mathsf{ls}.\mathsf{store}(p_{2})$. A consistent snapshot from
$\mathsf{ls}.\mathsf{store}(p_{2})$ is
$\mathsf{ls}.\mathsf{snapshot}(p_{2})(x)=(1,(1,0))$,
$\mathsf{ls}.\mathsf{snapshot}(p_{2})(y)=(2,(0,1))$ and
$\mathsf{ls}.\mathsf{snapshot}(p_{2})(z)=(1,(1,1))$ considering the
linearization $t_{3},t_{1},t_{2}$. Next execute $t_{4}$ choosing
$t_{4}.id=(1,2)$. To read from $z$ in $t_{4}$, $(z,1)$ is picked up from
$\mathsf{ls}.\mathsf{snapshot}(p_{2})(z)$, likewise for reading $y$. Last,
execute $t_{5}$ choosing $t_{5}.id=(2,2)$. Before executing $t_{5}$, calculate
the snapshot wrt the store of $p_{2}$. Since $t_{3}$ and $t_{1}$ are
concurrent, $\mathsf{ls}.\mathsf{snapshot}(p_{2})(y)=(1,(1,0))$ considering
the linearization $t_{3},t_{1},t_{2}$. Hence, when executing $t_{5}$, $r4$ can
read 1.

Note that the above execution is not ${\tt CCv}$. We need a total order among
all transactions in ${\tt CCv}$. if we choose $t_{1}.id<t_{3}.id$ then $t_{5}$
cannot read 1. Likewise if $t_{1}.id>t_{3}.id$, then $t_{2}.id>t_{3}.id$. This
would imply that when $t_{2}$ is delivered before $t_{4}$ so that r2 can read
1, $t_{1}$ must have been delivered before $t_{2}$ by causal delivery. Indeed
with $t_{1}.id>t_{3}.id$, $t_{4}$ will not be able to read 2 from $y$, but
only 1 from $t_{1}$. So both cases, we cannot read the expected values in
$t_{4},t_{5}$.

Organization of the rest of the paper. In the rest of the paper, to ease
reading, we focus on the technical details needed for the ${\tt CCv}$ DPOR
algorithm. The changes needed for ${\tt CC}$ are minor, and are described in
the supplementary material. We report experimental details for ${\tt CCv},{\tt
CC}$ in Section 7.

##  4\. ${\tt CCv}$ Axiomatic Semantics

As the first step towards the DPOR, we provide an axiomatic semantics for
${\tt CCv}$. The main result of this section is the equivalence (Theorem 4.1)
of the operational semantics for ${\tt CCv}$ (Beillahi et al., 2021b) and our
axiomatic semantics.

(a) A ${\tt CCv}$ execution for the program in Figure 7

$\mathsf{isu}(p1,t1)\cdot\mathsf{del}(p1,t1)\cdot\mathsf{isu}(p1,t2)\cdot\mathsf{del}(p1,t2)\cdot\mathsf{isu}(p2,t3)\cdot\mathsf{del}(p2,t3)\cdot\mathsf{del}(p2,t1)\cdot\mathsf{del}(p2,t2)\cdot\mathsf{isu}(p2,t4)$

(b) Execution summary for above execution

$\mathsf{isu}(p1,t1)\cdot\mathsf{del}(p1,t1)\cdot\mathsf{isu}(p1,t2)\cdot\mathsf{del}(p1,t2)\cdot\mathsf{del}(p2,t1)\cdot\mathsf{del}(p2,t2)\cdot\mathsf{isu}(p2,t3)\cdot\mathsf{del}(p2,t3)\cdot\mathsf{isu}(p2,t4)$

(e) Another execution summary for trace 9(c) Figure 9. Execution summary and
${\tt CCv}$ traces for program given in Figure 7

(c) ${\tt CCv}$ consistent trace

(d) ${\tt CCv}$ inconsistent trace

${\tt CCv}$ Execution Summary. As instructions within a transaction are not
visible to other transactions and processes, we “summarize” the internal
transitions in a transaction and only represent its overall effect. Given a
${\tt CCv}$ execution $\rho$, its execution summary $\mathsf{Sum}(\rho)$ is
obtained by replacing every subsequence in $\rho$ delimited by
$\mathtt{begin}$$(p,t)$ and $\mathtt{end}$$(p,t)$ event labels with a single
operation $\mathtt{isu}$$(p,t)$. $\mathtt{isu}$$(p,t)$ represents _issuing_
the transaction $t$ in process $p$. Thus, the sequence of transitions
$\sigma_{i}\xrightarrow[]{{\tt{begin}}(p,t)}\sigma_{i+1}\dots\xrightarrow[]{{\tt{end}}(p,t)}\sigma_{j}$
is replaced with $\sigma_{i}\xrightarrow[]{{\tt{isu}}(p,t)}\sigma_{j}$. The
execution summary is a sequence of transitions over the events
$\mathsf{EvSum}(\rho)=\\{\mathsf{isu}(p,t),\mathsf{del}(p,t)\mid
p\in\mathbf{P},t\in\mathcal{T}\\}$, and induces a total ordering $<$ on these
events. Let $(\mathsf{EvSum}(\rho),<)$ denote the execution summary
corresponding to execution $\rho$ (see Fig.9(b)(b) for the execution summary
for the execution in Fig.9(a)). We say that a transaction $t$ executed by
process $p$ _writes $x$ at process $p^{\prime}$_ if $t\in\mathcal{T}^{w,x}$
and the execution summary contains the event $\mathsf{del}(p^{\prime},t)$
which is not preceded by $\mathsf{del}(p^{\prime},t^{\prime})$ with
$t.id<t^{\prime}.id$ and $t^{\prime}\in\mathcal{T}^{w,x}$.

An execution summary $S=(\mathsf{EvSum}(\rho),<)$ induces two functions
capturing the _happens-before_ $S.hb$ and _read from the latest write_ $S.lw$
relations.

  * •

$S.hb:\mathcal{T}(\rho)^{r}\rightarrow\mathfrak{p}(\mathcal{T}(\rho)^{w})$
s.t.
$S.hb(t_{1}){=}\\{t^{\prime}\in\mathcal{T}(\rho)^{w}\mid\mathsf{del}(p,t^{\prime})<\mathsf{isu}(p,t_{1})$,
$p\in\mathbf{P}\\}$. Thus, $S.hb(t_{1})$ is the set of all transactions
$t^{\prime}$ which have a write operation, and were delivered before executing
$t_{1}$.

  * •

$S.lw:\mathcal{T}(\rho)^{r}\times\mathcal{V}\rightarrow\mathcal{T}(\rho)^{w}$,
defined by $S.lw(t_{1},x)=\\{t^{\prime}\mid t^{\prime}\in
S.hb(t_{1})\cap\mathcal{T}(\rho)^{w,x},t_{1}\in\mathcal{T}(\rho)^{r,x}$ and
$\forall t^{\prime\prime}\in
S.hb(t_{1})\cap\mathcal{T}(\rho)^{w,x},t^{\prime}.id\geq
t^{\prime\prime}.id\\}$. For a transaction $t_{1}\in\mathcal{T}(\rho)^{r,x}$,
$S.lw(t_{1},x)$ is the last (based on the ordering of transaction ids)
transaction $t^{\prime}$ to have written on $x$ before executing $t_{1}$.

${\tt CCv}$ Legal Summaries. An execution summary $S=\mathsf{Sum}(\rho)$ is
_legal_ under ${\tt CCv}{}$ iff:

  * (1)

Each $t\in\mathcal{T}$ in the domain of $S.lw$ reads from the latest write,
that is, $S.lw(t,x)$ for all $x$;

  * (2)

For all $t\in\mathcal{T}(\rho)^{w}$, if
$\mathsf{del}(p,t)<\mathsf{isu}(p,t^{\prime})$, then
$\mathsf{del}(p^{\prime},t)<\mathsf{del}(p^{\prime},t^{\prime})$ for all
processes $p,p^{\prime}$; and,

  * (3)

For each $t\in\mathcal{T}$ and processes $p,p^{\prime}$,
$\mathsf{isu}(p,t)<\mathsf{del}(p^{\prime},t)$.

Traces. A trace is an abstract representation of an execution summary. For a
concurrent program $\mathcal{P}$ with transactions $\mathcal{T}$, a trace is
defined as a graph
$(\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co})$
where the transactions are the nodes, and the relations
${\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co}$ form
edges between the nodes. For transactions $t\neq t^{\prime}$, define
$(t,t^{\prime})\in{\color[rgb]{1,0,0}po}$ (or
$t[{\color[rgb]{1,0,0}po}]t^{\prime}$) when $t$ and $t^{\prime}$ are in the
same process $p\in\mathbf{P}$ and $t.id<t^{\prime}.id$.
${\color[rgb]{1,0,0}po}$ does not relate the initializer transactions.
($t,t^{\prime})\in{\color[rgb]{0,0,1}\it{rf}}$ (or
$t[{\color[rgb]{0,0,1}\it{rf}}]t^{\prime}$) relates transactions $t\neq
t^{\prime}$ where $t^{\prime}$ reads from $t$ on some variable
$x\in\mathcal{V}$. The variable $x$ can be made explicit by defining
$(t,t^{\prime})\in{\color[rgb]{0,0,1}\it{rf}}^{x}$ (or
$t[{\color[rgb]{0,0,1}\it{rf}}]^{x}t^{\prime}$), with
${\color[rgb]{0,0,1}\it{rf}}=\bigcup_{x\in\mathcal{V}}{\color[rgb]{0,0,1}\it{rf}}^{x}$.
Lastly, ($t,t^{\prime})\in{\color[rgb]{1,.5,0}co}$ (or
$t[{\color[rgb]{1,.5,0}co}]t^{\prime}$) if $t\neq
t^{\prime}\in\mathcal{T}^{w,x}$ for some $x\in\mathcal{V}$, and $t^{\prime}$
writes to $x$ after $t$. The transaction $init_{x}$ is such that
$init_{x}[{\color[rgb]{1,.5,0}co}]t$ for all transitions
$t{\in}\mathcal{T}(\rho)^{w,x}$.

Let
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}]^{+}$
(resp.,
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}]^{*}$)
denote the transitive (reflexive) closure of
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}]$.
If
$t\,[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}]^{+}\,t^{\prime}$,
then $t$ _happens before_ $t^{\prime}$.

Total and Partial Traces for ${\tt CCv}$. A trace
$\tau=(\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co})$
is _total_ (denoted ${\tt total}(\tau)$) iff the relation
${\color[rgb]{1,.5,0}co}^{x}$ for each variable $x$ is a total order on
$\mathcal{T}^{w,x}$. A _partial_ trace is arbitrary, and need not be total.

$\tau$-consistent ${\tt CCv}$ Execution Summaries. Given an execution summary
$\rho=\sigma_{0}\xrightarrow[]{\ell_{1}}\sigma_{1}\xrightarrow[]{\ell_{2}}\sigma_{2}\xrightarrow[]{\ell_{3}}\sigma_{3}\cdots\xrightarrow[]{\ell_{n-1}}\sigma_{n-1}\xrightarrow[]{\ell_{n}}\sigma_{n}$,
and a trace
$\tau=(\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co})$,
$\rho$ is $\tau$-consistent (denoted $\rho\models\tau$) if the following
holds:

  * •

Each transaction $t\in\mathcal{T}$ corresponds to exactly one label
$\mathsf{isu}(-,t)$ in $\rho$.

  * •

For $t,t^{\prime}\in\mathcal{T}$, if $t[{\color[rgb]{1,0,0}po}]t^{\prime}$,
then $\exists$
$\ell_{i}=\mathsf{isu}(p,t),\ell_{j}=\mathsf{isu}(p,t^{\prime})$ with $i<j$ in
$\rho$.

  * •

For $t,t^{\prime}\in\mathcal{T}$, if $t[{\color[rgb]{1,.5,0}co}]t^{\prime}$,
then there exist
$\ell_{i}=\mathsf{isu}(p,t),\ell_{j}=\mathsf{isu}(p^{\prime},t^{\prime})$,
with $i<j$ such that $t,t^{\prime}\in\mathcal{T}^{w,x}$ for some
$x\in\mathcal{V}$.

  * •

For $t\neq t^{\prime}\in\mathcal{T}$, if
$t[{\color[rgb]{0,0,1}\it{rf}}]t^{\prime}$, then $\exists$
$\ell_{i}=\mathsf{isu}(p^{\prime},t),\ell_{j}=\mathsf{del}(p,t)$,
$\ell_{k}=\mathsf{isu}(p,t^{\prime})$, $i<j<k$, such that (i)
$t\in\mathcal{T}^{w,x}$, $t^{\prime}\in\mathcal{T}^{r,x}$ for some
$x\in\mathcal{V}$, and $p^{\prime}$ writes $x$ at process $p$, (ii)
$\neg(\exists\ell_{m}=\mathsf{del}(p,t^{\prime\prime}),j<m<k\wedge
t^{\prime\prime}\in\mathcal{T}^{w,x}\wedge
t^{\prime}[{\color[rgb]{1,.5,0}co}^{x}]t^{\prime\prime})$.

Partially Good, ${\tt CCv}$ consistent Traces. For a trace
$\tau=(\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co})$,
define $\tau\models{\tt CCv}$ iff (i) $\forall x\in\mathcal{V}$,
$t_{1},t_{3}\in\mathcal{T}^{w,x}$, $t_{2}\in\mathcal{T}^{r,x}$, if
$(t_{1},t_{2})\in{\color[rgb]{0,0,1}rf}^{x}$,
$(t_{3},t_{2})\in[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}]^{+}$, then
$(t_{3},t_{1})\in{\color[rgb]{1,.5,0}co}^{x}$, and (ii)
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}]^{+}$
is irreflexive. A partial trace $\tau$ satisfying $\tau\models{\tt CCv}$ is a
partially good trace. A partial trace $\tau$ is ${\tt CCv}$ consistent iff it
can be extended to a total trace s.t. $\tau\models{\tt CCv}$.

For a configuration $\sigma$, let $\big{[}[\sigma]\big{]}_{{\tt
CCv}}=\\{\tau\mid\exists\rho\in{\tt ExecFrom}(\sigma),\rho\models\tau$ and
$\tau$ is ${\tt CCv}$ consistent$\\}$ denote the set of all ${\tt CCv}$
consistent traces from a configuration $\sigma$. The trace shown in figure
9(d) is not ${\tt CCv}$ consistent for program execution given in Figure 9(a)
since $t3[{\color[rgb]{0,0,1}\it{rf}}]^{y}t4$ and
$t1[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t4$, we can not
have $t3[{\color[rgb]{1,.5,0}co}]^{y}t1$.

###### Theorem 4.1.

A (partial) trace $\tau$ is ${\tt CCv}$-consistent iff there is a legal and
$\tau$-consistent execution summary $S$ corresponding to $\tau$.

As seen in Figure 9(b), a single ${\tt CCv}{}$ consistent trace can represent
different executions : the ${\tt CCv}$ consistent trace in Figure 9(c)
represents executions with summaries as in Figure 9(b) and 9(e). Exploring all
executions of transactional programs under ${\tt CCv}{}$ can be achieved by
generating all traces in $\big{[}[\sigma]\big{]}_{{\tt CCv}}$ exactly once. We
can do better than exploring all traces, by observing that the outcome of
assert statements on local states only depend on ${\color[rgb]{1,0,0}po}$ and
${\color[rgb]{0,0,1}\it{rf}}$ relations irrespective of the
${\color[rgb]{1,.5,0}co}$ relation. Hence two execution (summaries) whose
traces have the same ${\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}\it{rf}}$
relations are regarded equivalent. We propose a DPOR algorithm that explores
traces by considering only the
${\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}\it{rf}}$ relations and such traces
are called _weak traces_.

_Weak traces_. A trace is called a $weak$ $trace$, if its
${\color[rgb]{1,.5,0}co}$ relation is empty. A weak trace is obtained by
removing all ${\color[rgb]{1,.5,0}co}$ edges from a trace
$\tau=\langle\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co}\rangle$
and this trace is denoted as $weak(\tau)$. We define
$\big{[}[\sigma]\big{]}_{{\tt
CCv}}^{weak}=\\{weak(\tau)|\tau\in\big{[}[\sigma]\big{]}_{{\tt CCv}}\\}$ as
the set obtained by weakening traces in $\big{[}[\sigma]\big{]}_{{\tt CCv}}$.
A trace
$\tau=\langle\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co}\rangle$
is _weaker than_ a trace
$\tau^{\prime}=\langle\mathcal{T}^{\prime},{\color[rgb]{1,0,0}po}^{\prime},{\color[rgb]{0,0,1}rf}^{\prime},{\color[rgb]{1,.5,0}co}^{\prime}\rangle$,
denoted by $\tau\sqsubseteq\tau^{\prime}$, if
$\mathcal{T}=\mathcal{T}^{\prime}$,
${\color[rgb]{1,0,0}po}={\color[rgb]{1,0,0}po}^{\prime}$,
${\color[rgb]{0,0,1}rf}={\color[rgb]{0,0,1}rf}^{\prime}$ and
${\color[rgb]{1,.5,0}co}\subseteq{\color[rgb]{1,.5,0}co}^{\prime}$.

Section 6 presents our DPOR algorithm where executions are explored until all
weak traces in $\big{[}[\sigma]\big{]}_{{\tt CCv}}^{weak}$ have been
generated. Towards the optimality of our algorithm in terms of the number of
traces explored, in Section 5, we show how to ensure that each trace in
$\big{[}[\sigma]\big{]}_{{\tt CCv}}^{weak}$ is explored exactly once. While
extending these weak traces, the ${\tt CCv}$ consistency is guaranteed by
defining a fulfilled semantics (Section 5) equivalent with the ${\tt CCv}$
semantics. In the fulfilled semantics, executions are associated to partial
traces that contain only those ${\color[rgb]{1,.5,0}co}$ edges which must be
necessarily present in any corresponding ${\tt CCv}$ consistent total trace.

##  5\. Fulfilled Semantics for ${\tt CCv}$

The main contribution of this section is a notion of _fulfilled semantics_ ,
which enables us to explore only weak traces $\big{[}[\sigma]\big{]}_{{\tt
CCv}}^{weak}$ which are ${\tt CCv}$ consistent, from a configuration $\sigma$.
To achieve this, we first define _fulfilled traces_.

Fulfilled Traces. A fulfilled trace is a partial trace which extends a weak
trace $\zeta$, and carefully selects which ${\color[rgb]{1,.5,0}co}$ edges are
to be added in each step, as we go towards a total trace.

Formally, a trace
$\tau=\langle\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co}\rangle$
is called _fulfilled_ if, for all transactions
$t,t^{\prime}\in\mathcal{T}^{w}$, $t\neq t^{\prime}$, and all variables
$x\in\mathcal{V}$, whenever $t$
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}]^{+}t^{\prime\prime}$ and
$t^{\prime}[{\color[rgb]{0,0,1}rf}^{x}]t^{\prime\prime}$, then $t$
$[{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime}$ : note that allowing
$t^{\prime}$ $[{\color[rgb]{1,.5,0}co}^{x}]^{+}t$ results in a cycle violating
${\tt CCv}$. Note that any trace $\tau$ s.t. $\tau\models{\tt CCv}$ is
fulfilled, but the converse is not true. One can have $\tau$ s.t. (1) for all
$t,t^{\prime}{\in}\mathcal{T}^{w},x{\in}\mathcal{V}$
[$t[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}]^{+}t^{\prime\prime}\wedge
t^{\prime}[{\color[rgb]{0,0,1}rf}^{x}]t^{\prime\prime}\Rightarrow t$
$[{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime}$, and (2)
$t^{\prime}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]^{+}t$.
By (1) $\tau$ is fulfilled, but (2) creates a
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]^{+}$
cycle violating ${\tt CCv}$.

###### Theorem 5.1.

A partial trace is ${\tt CCv}$-consistent if, it is fulfilled and partially
good.

Theorem 5.1 shows that partially good traces $\tau$ can be extended to total
${\tt CCv}$ consistent traces. The challenge is to add _only_ those
${\color[rgb]{1,.5,0}co}$ edges to ensure ${\tt CCv}$ is not violated.

###  5.1. Fulfilled Semantics : Extending Partially Good, Fulfilled Traces

Our DPOR algorithm (section 6) proceeds by extending partially good fulfilled
traces, to obtain ${\tt CCv}$ consistent total traces. For this, we work on a
transition system whose states are pairs $(\sigma,\tau)$ where $\sigma$ is a
configuration of the concurrent program $\mathcal{P}$ and $\tau$ is a
(partial) trace. The _fulfilled semantics_ is given as the transition relation
$\xrightarrow[]{}_{{\tt ful}}$, defined as
$(\sigma,\tau)\xrightarrow[]{\alpha}_{{\tt
ful}}(\sigma^{\prime},\tau^{\prime})$. The label $\alpha$ is one of
$(begin,t),(end,t),(read,t,t^{\prime}),(write,t)$. An important property of
$(\sigma,\tau)\xrightarrow[]{\alpha}_{{\tt
ful}}(\sigma^{\prime},\tau^{\prime})$ is that if $\tau$ is fulfilled and ${\tt
CCv}$-consistent so is $\tau^{\prime}$. By Theorem 5.1, all traces generated
by the fulfilled semantics are ${\tt CCv}$-consistent.

For
$\tau=\langle\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co}\rangle$,
$\tau^{\prime}=\langle\mathcal{T}^{\prime},{\color[rgb]{1,0,0}po}^{\prime},{\color[rgb]{0,0,1}rf}^{\prime},{\color[rgb]{1,.5,0}co}^{\prime}\rangle$,
we describe the transitions $(\sigma,\tau)\xrightarrow[]{\alpha}_{{\tt
ful}}(\sigma^{\prime},\tau^{\prime})$.

  * •

From a state $(\sigma,\tau)$, assume that we observe the $\mathsf{begin}(p,t)$
event. Then, the label $\alpha$ is $(begin,t)$, and we have
$\mathcal{T}^{\prime}=\mathcal{T}\cup\\{t\\}$,
${\color[rgb]{0,0,1}\it{rf}}^{\prime}={\color[rgb]{0,0,1}\it{rf}},{\color[rgb]{1,.5,0}co}^{\prime}={\color[rgb]{1,.5,0}co}$
and ${\color[rgb]{1,0,0}po}^{\prime}={\color[rgb]{1,0,0}po}\cup
t^{\prime}[{\color[rgb]{1,0,0}po}]t$ where $t^{\prime},t$ are transactions in
the same process $p$, $t^{\prime}$ is the last transaction executed in $p$,
and $t$ is the next transaction in ${\color[rgb]{1,0,0}po}$ order of $p$.
Fig.11 illustrates the effect of observing a $\mathsf{begin}(p,t7)$ event,
where $t7$ is the new transaction added to the trace. In Fig.11, assuming $t1$
is the last transaction execution from process $p$, we add
${\color[rgb]{1,0,0}po}$ edge from $t1$ to $t7$.

  * •

On events $w(p,t,x,v),\mathsf{end}(p,t)$, the state does not change.

  * •

From a state $(\sigma,\tau)$, assume that we observe the $ev=r(p,t,x,v)$ event
in transaction $t$. In this case, the label $\alpha$ is $(read,t,t^{\prime})$,
where $t^{\prime}$ is the transaction from which $t$ reads from, so that the
trace $\tau^{\prime}$ in the target state $(\sigma^{\prime},\tau^{\prime})$,
remains _fulfilled_ and ${\tt CCv}$ consistent. The transactions $t^{\prime}$
which qualify to be read from are prescribed using the _readable_ sets
${\tt{readable}}(\tau,t,x)$.

Readable sets to respect ${\tt CCv}$ consistency. A readable set
${\tt{readable}}(\tau,t,x)$ contains all those transactions $t^{\prime}$ from
which a read event on $x$ of transaction $t$ can read from, so that, on adding
the edge $(t^{\prime},t)$ to ${\color[rgb]{0,0,1}rf}^{\prime}$, the resultant
trace $\tau^{\prime}$ is partially good and fulfilled. To allow
$t^{\prime}\in{\tt{readable}}(\tau,t,x)$, we check a condition
$\neg\tt{cond1}\wedge\neg\tt{cond2}\wedge\neg\tt{cond3}\wedge\neg\tt{cond4}$
where $\tt{cond1},\tt{cond2},\tt{cond3}$ and $\tt{cond4}$ are described below.
These 4 conditions are sufficient to ensure that $\tau^{\prime}$ is fulfilled
and partially good (Lemma 5.2). Checking for each of
$\tt{cond1},\tt{cond2},\tt{cond3},\tt{cond4}$ takes time $\leq
O(|\mathcal{T}|^{2})$.

(a) $\tt{cond1}$

(b) $\tt{cond2}$

(c) $\tt{cond3}$

(d) $\tt{cond4}$

Figure 10. ${\tt CCv}$ violating reads.

For transactions $t\in\mathcal{T}^{r,x}$, $t^{\prime}\in\mathcal{T}^{w,x}$,
$x\in\mathcal{V}$, to allow
$t^{\prime}[{\color[rgb]{0,0,1}rf^{\prime}}^{x}]t$, we check the following :

  * (1)

Let ${\tt{cond1}}=\exists t_{3}\in\mathcal{T}^{w,x}$ such that $t^{\prime}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}$]+
$t_{3}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}$]+ $t$. We then check
$\neg{\tt{cond1}}$ to ensure $t$ reads from the transaction which wrote last
to $x$. If we allow $t^{\prime}[{\color[rgb]{0,0,1}rf^{\prime}}^{x}]t$, then
$t_{3}{\in}\mathcal{T}^{w,x}$ induces
$t_{3}[{\color[rgb]{1,.5,0}co^{\prime}}]^{x}t^{\prime}$, resulting in a ${\tt
CCv}$ violating cycle
$t^{\prime}[{\color[rgb]{1,.5,0}co}]t_{3}[{\color[rgb]{1,.5,0}co^{\prime}}]t^{\prime}$.
Thus, To allow $t^{\prime}[{\color[rgb]{0,0,1}rf^{\prime}}^{x}]t$, we check
$\neg{\tt{cond1}}$, see Figure 10(a).

  * (2)

Let ${\tt{cond2}}=\exists t_{4},\exists
y\in\mathcal{V}[t^{\prime},t_{4}\in\mathcal{T}^{w,y}\cap\mathcal{T}^{w,x}\wedge
t_{4}[{\color[rgb]{0,0,1}\it{rf}}^{y}]t]$. $\tt{cond2}$ considers the case
when $t$ has read from a transaction $t_{4}$ wrt $y\neq x$, and both
transactions $t^{\prime},t_{4}$ write on both $x,y$.
$t_{4}[{\color[rgb]{0,0,1}\it{rf}}^{y}]t$ and
$t^{\prime}{\in}\mathcal{T}^{w,y}$ induces
$t^{\prime}[{\color[rgb]{1,.5,0}co^{\prime}}]^{y}t_{4}$ for ${\tt CCv}$
consistency of $\tau^{\prime}$. If we allow
$t^{\prime}[{\color[rgb]{0,0,1}rf^{\prime}}^{x}]t$, then
$t_{4}{\in}\mathcal{T}^{w,x}$ induces
$t_{4}[{\color[rgb]{1,.5,0}co^{\prime}}]^{x}t^{\prime}$, resulting in a ${\tt
CCv}$ violating cycle
$t^{\prime}[{\color[rgb]{1,.5,0}co}]t_{4}[{\color[rgb]{1,.5,0}co^{\prime}}]t^{\prime}$.
Thus, to allow $t^{\prime}[{\color[rgb]{0,0,1}rf^{\prime}}^{x}]t$, we check
$\neg\tt{cond2}$, see Figure 10(b).

  * (3)

Assume $t^{\prime}\in\mathcal{T}^{w,x}\cap\mathcal{T}^{w,y}$. To allow
$t^{\prime}[{\color[rgb]{0,0,1}rf^{\prime}}^{x}]t$, we check the following
conditions $\neg\tt{cond3}$ and $\neg\tt{cond4}$ are true. Intuitively,
${\tt{cond3}}$ (3(a)) and ${\tt{cond4}}$ (3(b)) check that allowing
$t^{\prime}[{\color[rgb]{0,0,1}rf^{\prime}}^{x}]t$ will not induce a ${\tt
CCv}$ violating cycle, by considering existing ${\color[rgb]{0,0,1}rf}^{y}$
relations $t$ has wrt $y\neq x$ and a transaction $t_{4}$ (say $t_{4}$
$[{\color[rgb]{0,0,1}rf}$]y $t$). We analyze the
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}$]+
paths from $t_{4}$ to $t^{\prime},t$.

    * (a)

Assume we have a $t_{4}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}$]∗
$t^{\prime}$ path s.t. there is $t_{3}\in\mathcal{T}^{w,y}$ in this path.
Here, $t_{3}$ can coincide with $t^{\prime}$ or can be
${\color[rgb]{1,.5,0}co}$-after $t_{4}$.

${\tt{cond3}}=[\exists t_{3},t_{4}$ s.t. $t_{4}$[${\color[rgb]{0,0,1}rf}$]y
$t$, $t_{4}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}$]+
$t_{3}$ [${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}$]∗ $t^{\prime}$]
with $t_{3}{\in}\mathcal{T}^{w,y}$.

If $\tt{cond3}$ is true, then allowing
$t^{\prime}[{\color[rgb]{0,0,1}rf^{\prime}}^{x}]t$, creates a ${\tt CCv}$
violation, as shown below.

$\bullet$ Case 1: If $t_{3}=t^{\prime}$,
$t_{4}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]^{+}t^{\prime}$
and
$t^{\prime}[{\color[rgb]{1,0,0}po}^{\prime}\cup{\color[rgb]{0,0,1}\it{rf}}^{\prime}]^{+}t$
imply $t^{\prime}[{\color[rgb]{1,.5,0}co}^{y}]t_{4}$ (to respect
$\tau^{\prime}\models{\tt CCv}$). This results in a cycle
$t_{4}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]^{+}t^{\prime}[{\color[rgb]{1,.5,0}co}]t_{4}$,
violating ${\tt CCv}$.

$\bullet$ Case 2 : If $t_{3}\neq t^{\prime}$, then $t_{3}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}$]∗ $t^{\prime}$ along with
$t^{\prime}[{\color[rgb]{0,0,1}rf^{\prime}}^{x}]t$ will give
$t_{3}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf^{\prime}}$]${}^{+}t$.
Along with $t_{4}$[${\color[rgb]{0,0,1}rf}$]${}^{y}t$, we obtain
$t_{3}[{\color[rgb]{1,.5,0}co^{\prime}}^{y}]t_{4}$ by ${\tt CCv}$ consistency.
This results in the cycle
$t_{4}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}$]${}^{+}t_{3}$
$[{\color[rgb]{1,.5,0}co^{\prime}}^{y}]t_{4}$, violating ${\tt CCv}$
consistency. See Figure 10(c).

    * (b)

Assume we have a $t_{4}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}]^{+}$
$t$ path s.t. (i) there is a transaction $t_{3}\in\mathcal{T}^{w,x}$ in this
path, and (ii) $t_{3}$ is the last transaction writing to $x$ in this path.

${\tt{cond4}}=[\exists t_{3},t_{4}$ s.t. $t_{4}$[${\color[rgb]{0,0,1}rf}$]y
$t$, $t_{4}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}$]+
$t_{3}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}$]+ $t$], with
$t_{3}\in\mathcal{T}^{w,x}$ and, there is no transaction
$t^{\prime\prime}\in\mathcal{T}^{w,x}$ such that $t_{3}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}$]+
$t^{\prime\prime}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}$]+ $t$.

If $\tt{cond4}$ is true, then allowing
$t^{\prime}[{\color[rgb]{0,0,1}rf^{\prime}}^{x}]t$ creates a ${\tt CCv}$
violation as shown below. $t^{\prime}[{\color[rgb]{0,0,1}rf^{\prime}}^{x}]t$
and $t_{3}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}$]+ $t$ gives us
$t_{3}[{\color[rgb]{1,.5,0}co}^{x}]t^{\prime}$, while
$t_{4}[{\color[rgb]{0,0,1}rf}^{y}]t$ and
$t^{\prime}[{\color[rgb]{0,0,1}rf^{\prime}}^{x}]t$ gives us
$t^{\prime}[{\color[rgb]{1,.5,0}co}^{y}]t_{4}$, and thus the cycle
$t_{3}t^{\prime}t_{4}t_{3}$ violating ${\tt CCv}$ consistency. See Figure
10(d).

Figure 11. Transition for (a) $begin$ event and (b) $read$ event.

Once we select a readable transaction
$t^{\prime}\in{\tt{readable}}(\tau,t,x)$, and add
$t^{\prime}[{\color[rgb]{0,0,1}\it{rf}}^{x}]t$ obtaining a trace
$\tau^{\prime}$, in order to keep $\tau^{\prime}$ fulfilled, we should add
some ${\color[rgb]{1,.5,0}co}$ edges to $t^{\prime}$. Next, we find out which
${\color[rgb]{1,.5,0}co}$ edges are necessary to be added.

Necessary ${\color[rgb]{1,.5,0}co}$ edges to maintain fulfilled traces. A
visible set ${\tt{visible}}(\tau,t,x)$ consists of all
$t^{\prime\prime}\in{\tt{readable}}(\tau,t,x)$ which can reach $t$ via
${\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}\it{rf}}$ edges. If we have
$(\sigma,\tau)\xrightarrow[]{(read,t,t^{\prime})}_{{\tt
ful}}(\sigma^{\prime},\tau^{\prime})$, then to maintain fulfilled-ness of
$\tau^{\prime}$, (1) we must add new ${\color[rgb]{1,.5,0}co}$ edges from all
$t^{\prime\prime}\in{\tt{visible}}(\tau,t,x)$ to $t^{\prime}$, (2) if
$\exists$ $t^{\prime\prime\prime}\in\mathcal{T}^{w,y}$ s.t.
$t^{\prime\prime\prime}[{\color[rgb]{0,0,1}\it{rf}}$]y $t$, and
$t^{\prime}\in\mathcal{T}^{w,y}$, for $y\neq x$, then we must add
${\color[rgb]{1,.5,0}co}$ edges from $t^{\prime}$ to $t^{\prime\prime\prime}$.

Thus,
$\tau^{\prime}=(\mathcal{T}^{\prime},{\color[rgb]{1,0,0}po}^{\prime},{\color[rgb]{0,0,1}\it{rf}}^{\prime},{\color[rgb]{1,.5,0}co}^{\prime})$
is given by $\mathcal{T}^{\prime}=\mathcal{T}$,
${\color[rgb]{1,0,0}po}^{\prime}={\color[rgb]{1,0,0}po}$,
${\color[rgb]{0,0,1}rf}^{\prime}={\color[rgb]{0,0,1}rf}\cup(t^{\prime},t)$,
and
${\color[rgb]{1,.5,0}co}^{\prime}={\color[rgb]{1,.5,0}co}\cup\\{(t^{\prime\prime},t^{\prime})\mid
t^{\prime\prime}\in{\tt{visible}}(\tau,t,x)\\}$
$\cup\\{(t^{\prime},t^{\prime\prime\prime})\mid
t^{\prime\prime\prime}[{\color[rgb]{0,0,1}\it{rf}}^{y}]t,t^{\prime}\in\mathcal{T}^{w,y}\\}$.
Lemma 5.2 shows that if $\tau$ is fulfilled and ${\tt CCv}$ consistent, then
the new trace $\tau^{\prime}$ obtained using $\xrightarrow[]{}_{{\tt ful}}$ is
also fulfilled and ${\tt CCv}$ consistent.

###### Lemma 5.2.

If $\tau$ is fulfilled and partially good, and
$\tau\xrightarrow[]{\alpha}_{{\tt ful}}\tau^{\prime}$ then $\tau^{\prime}$ is
fulfilled and ${\tt CCv}$ consistent.

###### Example 5.3.

Consider a trace given in figure 11, suppose we are currently executing
transaction $t7$ and the next event in $t7$ is a read event $e_{R}$ on
variable $y$ and $t7\notin\mathcal{T}^{w,y}$. Assume that
$t_{2},t_{3},t_{4},t_{5},t_{8},t_{9}\in\mathcal{T}^{w,y}$ and
$t_{2},t_{9}\in\mathcal{T}^{w,x}$. The readable set for $e_{R}$ is
${\tt{readable}}(\tau,t_{7},y)=\\{t_{2},t_{4},t_{5},t_{8}\\}$. Transaction
$t_{3}\notin{\tt{readable}}(\tau,t_{7},y)$ because $t_{3}$
[${\color[rgb]{1,0,0}po}$] $t_{4}$ and $t_{4}$ [${\color[rgb]{0,0,1}\it{rf}}$]
$t_{7}$. Since $t_{2},t_{9}\in\mathcal{T}^{w,x},\mathcal{T}^{w,y}$, and
$t_{2}[{\color[rgb]{0,0,1}\it{rf}}]^{x}t_{7}$, if allow $t_{7}$ read $y$ from
$t_{9}$, then we will get ${\tt CCv}$ violating cycle
$t_{2}[{\color[rgb]{1,.5,0}co}^{y}]t_{9}[{\color[rgb]{1,.5,0}co}^{x}]t_{2}$.
Hence $t_{9}\notin{\tt{readable}}(\tau,t_{7},y)$. Only
$t_{2},t_{4}\in{\tt{readable}}(\tau,t_{7},y)$ are such that there is a
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}$ path to $t_{7}$;
hence, the visible set for $e_{R}$ is
${\tt{visible}}(\tau,t_{7},y)=\\{t_{2},t_{4}\\}$. If we let $t_{7}$ read from
$t_{8}$, then we add ${\color[rgb]{0,0,1}\it{rf}}$ and
${\color[rgb]{1,.5,0}co}$ relations (dotted arrows in figure 11) to make the
trace fulfilled.

###  5.2. Weakenings of Traces under ${\tt CCv}$ = Weakenings of Traces under
Fulfilled Semantics

The main result of this section is that when one works with weak traces, the
fulfilled semantics suffices : all weakenings of ${\tt CCv}$-consistent traces
are also weakenings of traces generated by the fulfilled semantics. First, we
show that computing the readable and visible sets according to the fulfilled
semantics is poly time.

Efficiency. Given trace $\tau$ and transaction $t$,
${\tt{readable}}(\tau,t,x)$ and ${\tt{visible}}(\tau,t,x)$ are both computable
in polynomial time. Computing ${\tt{readable}}(\tau,t,x)$ involves (i)
computing the transitive closure of
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]$
which takes $O(|\mathcal{T}|^{3})$ time, (ii) computing the set of
transactions $t^{\prime}$ s.t.
$t^{\prime}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{*}t$,
which takes $O(|\mathcal{T}|^{2})$ time, (iii) for each
$t^{\prime}\in\mathcal{T}^{w,x}$ check if
$t^{\prime}\in{\tt{readable}}(\tau,t,x)$ by checking each of
$\tt{cond1},\tt{cond2},\tt{cond3},\tt{cond4}$, which takes time $\leq
O(|\mathcal{T}|^{3})$. Lemma 5.4 states this result which is also true for
${\tt CC}$.

###### Lemma 5.4.

Given trace $\tau$, a transaction $t$ and a variable $x$, we can construct the
sets ${\tt{readable}}(\tau,t,x)$ and ${\tt{visible}}(\tau,t,x)$ in polynomial
time.

Define $\big{[}[\sigma]\big{]}^{{\tt ful}}_{{\tt CCv}}$ as the set of traces
generated using $\xrightarrow[]{}_{{\tt ful}}$ transitions, starting from a
configuration $\sigma$ with an empty trace $\tau_{\emptyset}$.
$\big{[}[\sigma]\big{]}_{{\tt CCv}}^{{\tt
ful}}=\\{\tau\,|\,(\sigma,\tau_{\emptyset})\xrightarrow[]{*}_{{\tt
ful}}(\sigma^{\prime},\tau)\\}$. Theorem 5.5 shows that ${\tt CCv}$ semantics
and the fulfilled semantics coincide on weak traces. Thus, it suffices to
explore traces according to the fulfilled semantics, where
${\color[rgb]{1,.5,0}co}$ edges are added only when necessary. As seen
already, the fulfilled semantics results in new traces which are not only
fulfilled but also partially good, leading to ${\tt CCv}$ consistent traces.
This constitutes the core of the soundness of our DPOR algorithm.

###### Theorem 5.5.

For any configuration $\sigma$,
$\\{weak(\tau)|\tau\in\big{[}[\sigma]\big{]}^{{\tt ful}}_{{\tt
CCv}}\\}=\big{[}[\sigma]\big{]}_{{\tt CCv}}^{weak}$.

##  6\. ${\tt CCv}$ DPOR Algorithm

We present our DPOR algorithm, which systematically explores, for any
terminating program, all weak traces which can be generated by the fulfilled
semantics. The main procedure is Algorithm 1.

Procedure - ExploreTraces. This procedure takes as input, a _configuration_
$\sigma$, a _fulfilled trace_ $\tau$ and an _observation sequence_ $\pi$.
$\pi$ is a sequence of events $ev\in\\{(begin,t)$,$(end,t)$,$(write,t),$
$(read,t,t^{\prime})\\}$. Events from the same transaction appear contiguously
in $\pi$. For read events $ev=(read,t,t^{\prime})$, the value of the Boolean
flag $localread(ev)$ checks if $t=t^{\prime}$, that is, $ev$ reads from a
write $e_{W}$ of the same transaction. A Boolean array $locally[~{}]$ of size
$|\mathcal{V}|$ is reset to FALSE for all variables at the start of any
transaction; when a write event on $x$ takes place in the current transaction,
then $locally[x]$ is set to TRUE. This signifies the local availability of an
$(x,v)$ in the log. We also maintain a map $currentreads$ from variables to
transactions : $currentreads[x]=t^{\prime}$ means that $x$ read from
transaction $t^{\prime}$; hence, all later read events of $x$ in the current
transaction $t$ must read from $t^{\prime}$, unless $t$ writes to $x$ between
an earlier read (from $t^{\prime}$) and the next read. Initially,
ExploreTraces is invoked with initial configuration $\sigma_{0}$, empty trace
$\tau_{0}$ and observation sequence $\pi=\epsilon$. From the initial
$(\sigma_{0},\tau_{0})$, we choose according to the fulfilled semantics, a
transaction $t^{\prime}$ by adding $\mathsf{begin}(t^{\prime})$ to $\pi$, and
call on $ExploreTraces$ to continue (lines 4-8, Algorithm 1). Let $e$ be the
last event of $\pi$ (line 2, Algorithm 1). If $e\neq\mathsf{end}(t^{\prime})$
then add the next event $e^{\prime}$ (read, write or $\mathsf{end}$) from
transaction $t=e.trans$ to the observation sequence $\pi$, updating it to
$\pi.e^{\prime}$.

$\bullet$ If $e^{\prime}$ writes on $x$, set $locally[x]$ TRUE, update
$\pi{\leftarrow}\pi.e^{\prime}$ and recursively call on $ExploreTraces$ (lines
11-12). Subsequent reads on $x$ from transaction $t$ will hence read from $t$.

$\bullet$ Let $e^{\prime}=r(p,t,x,v)$ be a read event on $x$ in transaction
$t$.

  * •

If $e^{\prime}$ can read from its transaction log due to an earlier write on
$x$ in $t$, then the trace is not updated (lines 14-16).

  * •

If $e^{\prime}$ cannot read from its transaction log it checks if
$currentreads[x]$ is assigned some transaction $t^{\prime}$, and in that case,
reads from $t^{\prime}$ (lines 17-19). In this case, $Swappable(e^{\prime})$
is FALSE, indicating that there is no need to look for a source transaction to
read from.

  * •

If $e^{\prime}$ cannot read from its transaction log and $currentreads[x]$ is
empty, then the set $schedules(e^{\prime})$ is initialized and the Boolean
flag $Swappable(e^{\prime})$ is set to TRUE (lines 20-22).
$Swappable(e^{\prime})$ being TRUE indicates that we must find according to
the fulfilled semantics, readable transactions
$t^{\prime}\in\mathcal{T}^{w,x}$ where $e^{\prime}$ can read from, leading to
$(\sigma^{\prime},\tau^{\prime})$. For each such $t^{\prime}$, let
$\pi=\zeta\cdot(begin,t)\dots(read,t,t^{\prime})$ be the observation sequence
obtained on choosing to read from $t^{\prime}$. $currentreads[x]$ is set to
$t^{\prime}$ and ExploreTraces($\sigma^{\prime},\tau^{\prime},\pi)$ is called
recursively (line 24). If transaction $t^{\prime}$ has not yet appeared in
$\pi$, the write in $t^{\prime}$ is called a _postponed write_.

$\bullet$ If $e^{\prime}$ is $(\mathsf{end},t)$, then we recursively call on
$ExploreTraces$ after appending $(\mathsf{end},t)$ to $\pi$, exploring other
transactions. When the recursive calls return to this point when the last
event of $\pi$ is $(\mathsf{end},t)$, we do the following. Corresponding to
the last write for each variable in transaction $t$, we call CreateSchedule.
This call enables us to pair these write events as potential sources to be
read from, for the read operations of transactions which are dependent on
postponed write operations. This call also creates schedules for such read
operations which are identified in CreateSchedule. These schedules are then
explored when the recursive call to $ExploreTraces$ returns at line 25. For a
read event $e^{\prime}$ in a transaction $t$, each schedule $\beta\in
schedules(e^{\prime})$ explores a new source transaction $t^{\prime}$ to read
from, and extends the trace.

Algorithm 2 CreateSchedule. CreateSchedule is called when we are at an
$e=(end,t_{2})$ event of a transaction $t_{2}\in\mathcal{T}^{w}$ in an
observation sequence $\pi$. The inputs are a fulfilled trace $\tau$, and
observation sequence $\pi$. CreateSchedule enables a read event occurring in a
transaction $t_{1}$ which precedes a transaction $t_{2}$ in $\pi$, to read
from a write event in $t_{2}$. We start from $(end,t_{2})$ in $\pi$, and
traverse $\pi$ backwards, until we cross $\pi[k]=(begin,t_{2})$ (line 2,
Algorithm 2). We continue going back in $\pi$ and find a read event
$e^{\prime}=\pi[i]$, $1\leq i<k-1$ on a variable $x$ in a transaction
$t_{1}\neq t_{2}$ which has appeared before $\pi[k]$, such that

  * •

$swappable(e^{\prime})$ is true, and $localread(e^{\prime})$ is false (line
4). The latter condition ensures that there are no writes in $t_{1}$ on the
variable of interest for $e^{\prime}$, which precedes the read $e^{\prime}$,
while the former ensures that the read is pending.

  * •

$t_{1}=e^{\prime}.trans$, should not happen before $t_{2}$, that is, ($\neg
t_{1}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}]^{+}$ $t_{2}$), (line
6)

  * •

There is no ${\color[rgb]{1,.5,0}co}$-cycle$(t_{1},t_{2})$ (line 8): that is,
there is no $y\in\mathcal{V}$ and transaction $t^{\prime\prime}$ s.t.
$[t^{\prime\prime}[{\color[rgb]{0,0,1}rf}]^{y}t_{1}\wedge
t_{2}\in\mathcal{T}^{w,y}\wedge t^{\prime\prime}\in\mathcal{T}^{w,x}]$.

  * •

$t_{2}$ does not overwrite reads made by $t_{1}$ wrt $x$ (line 8). Let
${\tt{overwrite}}(t_{2},t_{1})$ be the formula $\exists
t^{\prime\prime}\in\mathcal{T}\cdot\exists
y\in\mathcal{V}\cdot[t^{\prime\prime}[{\color[rgb]{0,0,1}rf}]^{y}t_{1}\wedge
t_{2}\in\mathcal{T}^{w,y}\wedge t^{\prime\prime}[{\color[rgb]{1,0,0}po}$
$\cup$ ${\color[rgb]{0,0,1}rf}]^{+}t_{2}]$ which says that $t_{2}$ overwrites
some variable $y$ which has been read by $t_{1}$ from some $t^{\prime\prime}$.

When lines 4,6,8 hold, we create a schedule $\beta$ for $e^{\prime}$ by
swapping $t_{2}$ with $t_{1}$ in $\pi$. First, initialize the schedule $\beta$
(line 10). To populate the schedule appropriately, we move forward in $\pi$
from $e^{\prime}=\pi[i]$ till $(end,t_{1})=\pi[j]$ in $\pi$ (lines 12,13).
Then we inspect the transactions $t^{\prime\prime}$ appearing in $\pi$ between
$\pi[j]$ (the end of $t_{1}$) and $\pi[k]$ (start of $t_{2}$), to see if these
can be retained before $t_{2}$ in the schedule.

Create schedule for $e^{\prime}$. We create a schedule for $e^{\prime}$ by
inspecting all transactions $t^{\prime\prime}$ which appear between
$\pi[j]=(end,t_{1})$ and $\pi[k]=(begin,t_{2})$ (while loop in line 14). We
check whether

  * (1)

$t^{\prime\prime}$ happens before $t_{2}$ (line 16).

  * (2)

$t_{1}$ does not happen before $t^{\prime\prime}$, and

  * (3)

$t^{\prime\prime}$ does not overwrite reads made by $t_{1}$ (line 18).

If (2) or (3) is violated (line 18), it means $t_{1}$ happens before
$t^{\prime\prime}$ or, $t^{\prime\prime}$ overwrites a read made by $t_{1}$.
Then, we cannot choose $t^{\prime\prime}$ in the schedule, and exit the
function. If (1) is violated, then $t^{\prime\prime}$ does not happen before
$t_{2}$, and we need not bother including $t^{\prime\prime}$ in the schedule.
Hence, we move forward beyond $t^{\prime\prime}$ (lines 31-33). If (1),(2),(3)
all hold good, then we proceed to include $t^{\prime\prime}$ in the schedule
(lines 23-26). When we reach $(end,t_{2})$, the loop ends. Then we append the
constructed schedule $\beta$ with events from $t_{2}$, followed by events from
$t_{1}$ till $(read,t_{1},t_{2})$. This schedule is added to
$schedules(e^{\prime})$ if it already does not exist.

Algorithm 3 RunSchedule. $RunSchedule$ is called when the recursive call of
$ExploreTraces$ returns at line 24 in Algorithm 1, at the end of a read event
$e^{\prime}=(read,t,t^{\prime})$ in transaction $t$. Let the observation
sequence be $\pi=\pi^{\prime}.(begin,t)\dots,(read,t,t^{\prime})$, where
$\pi^{\prime}$ denotes the earlier transactions which have been executed.
Assuming the configuration $\sigma$ and trace $\tau$ before adding the
${\color[rgb]{0,0,1}\it{rf}}$ edge from $t$ to $t^{\prime}$, $RunSchedule$ is
called on $\sigma$, $\tau$, $\pi^{\prime}$ and a schedule $\beta\in
Schedules(e^{\prime})$ (line 26, Algorithm 1). Note that $\beta$ ends with the
suffix $(begin,t)\dots(read,t,t^{\prime})$. All read events $e^{\prime}$
having $Swappable(e^{\prime})$ as TRUE in $\beta$ are made FALSE. This is an
optimization step, to rule our redundant schedules corresponding to the read
events in $\beta$. We obtain the observation sequence $\pi^{\prime}.\beta$ by
appending transactions from $\beta$ one at a time to $\pi^{\prime}$. The trace
$\tau$ is updated to trace $\tau^{\prime}$ obtained on executing $\beta$. At
the end, we invoke ExploreTraces on $\tau^{\prime},\pi^{\prime}.\beta$.

###  6.1. An Illustrating Example

We illustrate the DPOR algorithm on Figure 12. We have presented all the
traces as well as the recursion tree in Figure 13. The nodes $n_{0}\dots
n_{35}$ represent recursive calls to $ExploreTraces$ and $RunSchedule$.
$n_{0}$ is the first call to $ExploreTraces$ with an empty trace and
observation sequence.

Figure 12. Example for DPOR

From $n_{0}$, consider the case when $ExploreTraces$ selects $t1$, making
recursive calls to itself after each instruction in $t1$. The two reads of
$t1$ each have two sources to read from, $init_{x}$ or $t4$, and $init_{y}$ or
$t2$. The reads from $t4,t2$ will be scheduled later, by a call to
$CreateSchedule$, as indicated by the orange arrows. The last call to
$ExploreTraces$ in $t1$ is made at $(end,t1)$ reaching node $n_{1}$. Next,
$ExploreTraces$ selects $t2$, and the last recursive call in $t2$ leads to
node $n_{5}$, where $t3$ is selected. The read in $t3$ has two choices to read
from : $t1$ and $t2$, and makes two recursive calls after each choice. The
respective last recursive calls to $ExploreTraces$ leading to $n_{9},n_{10}$.
$t5$ is selected next, leading to nodes $n_{16}$ and $n_{17}$. Finally, $t4$
is chosen. $t4$ has two sources to read from, namely, $t5$ and $t3$, leading
to nodes $n_{23}$ to $n_{26}$. This gives traces $\tau_{1},\dots,\tau_{4}$,
and respective observation sequences. For eg., the observation sequence for
$\tau_{3}$ is $(begin,t1),(read,t1,init_{x}),(read,t1,init_{y})$,
$(write,t1),(end,t1),(begin,t2),\dots,(end,t2)$,
$(begin,t3),(read,t3,t1),(write,t3)$, $(end,t3)$, $(begin,t5)$,
$\dots,(end,t5),(begin,t4),(read,t4,t5)$, $(write,t4),(end,t4)$. The recursive
call to $ExploreTraces$ from $n_{23},n_{24},n_{25},n_{26}$ returns as there
are no more transactions, and $CreateSchedule$ is called from these since $t4$
has write instructions.

From $n_{23}$, the recursive call of $ExploreTraces$ returns to the point
after $(end,t4)$, where $CreateSchedule$ is invoked. We traverse back in the
observation sequence till $(begin,t4)$ (line 2 of $CreateSchedule$). We keep
moving back till obtaining the read event $e^{\prime}$ of $r1$ in $t1$, for
which $localread(e^{\prime})$ has been set to FALSE and
$swappable(e^{\prime})$ set to TRUE in $ExploreTraces$. We check if $t1$
happens before $t4$, which it does not and also check that $t4$ does not
overwrite any prior reads of $t1$ and check absence of
${\color[rgb]{1,.5,0}co}$-cycles. Thus, $t4$ and $t1$ can be swapped. The
schedule $\beta_{1}$ is initialized. We then check whether the transactions
$t2,t3,t5$ which happen between $(end,t1)$ and $(begin,t4)$ should be retained
before $t4$ in the schedule for $e^{\prime}$. Since $\neg
t2[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t4,\neg
t3[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t4$, the schedule
need not contain $t2,t3$, and we skip over them. However,
$t5[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t4$ and must be
retained in the schedule. So we obtain
$\beta_{1}=(begin,t5)\dots(end,t5)\cdot$ $(begin,t4)$ $\dots$
$(end,t4)(begin,t1)$ $\dots$ $(read,t1,t4)$ in $Schedules(e^{\prime})$. After
this, the call from $CreateSchedule$ returns, and we trace back to $n_{16}$
and change the source (from the readable set) for $r4$, so $r4=2$ and we get
the new trace $\tau_{2}$.

Figure 13. Traces and recursion tree for the program in Figure 12. The nodes
$n_{0}$ to $n_{35}$ represent recursive calls to Algorithm 1. The black edges
come from Algorithm 1, green edges represent Algorithm 3 running a schedule
created by a call to Algorithm 2. The orange lines denote the pairs of writes
and reads, resulting in schedules. The edges are decorated with the
transactions executed, and register values read.

The call to $ExploreTraces$ at node $n_{24}$ returns to the point after
$(end,t4)$, after which $CreateSchedule$ is invoked. The corresponding read
event is again $e^{\prime}$ of $r1$ in $t1$. As seen above, we check whether
the transactions $t2,t3,t5$ which happen between $(end,t1)$ and $(begin,t4)$
should be retained before $t4$ in the schedule for $e^{\prime}$. Indeed,
$t3[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t4,t2[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t3,t5[{\color[rgb]{1,0,0}po}]t4$.
Hence we obtain another schedule $\beta_{2}$=$(begin,t2)$ $\dots(end,t2)$
$(begin,t3)$ $\dots$ $(end,t3)(begin,t5)$ $\dots$ $(end,t5)(begin,t4)$
$\dots(end,t4)(begin,t1)\dots(read,t1,t4)$ in $Schedules(e^{\prime})$. Then we
backtrack to $n_{16}$ and call $CreateSchedule$ at $(end,t5)$ which returns an
empty schedule since there are no corresponding read events. Then we backtrack
to node $n_{9}$ and then to $n_{5}$ till we can change the source for $r3$,
which reads from $t1$. We continue exploring traces with $ExploreTraces$ and
obtain $\tau_{3},\tau_{4}$. We invoke $CreateSchedule$ from nodes $n_{25}$ and
$n_{26}$, however these do not add any more schedules to $e^{\prime}$, since
they are equivalent to what has been added already in $Schedules(e^{\prime})$.
From $n_{25}$, we backtrack and reach node $n_{5}$ and invoke $CreateSchedule$
at $(end,t2)$ which creates a schedule $\gamma_{1}$ corresponding to the read
event $e^{\prime\prime}$ of $r2$ in $t1$.
$\gamma_{1}$=$(begin,t2)\dots(end,t2)(begin,t1)(read,t1,init_{x})$
$(read,t1,t2)$ is added to $Schedules(e^{\prime\prime})$.

We then backtrack till the point $r2=0$ and find that
$Schedules(e^{\prime\prime})$ is nonempty. $RunSchedule$ runs the schedule
$\gamma_{1}$ (shown in green edges $n_{0}-n_{2}-n_{6}$), followed by recursive
calls to $ExploreTraces$, resulting in traces
$\tau_{5},\tau_{6},\tau_{7},\tau_{8}$. At node $n_{30}$ on return from
$ExploreTraces$, we backtrack till the point $r1=0$ and find two schedules
$\beta_{1},\beta_{2}$ in $Schedules(e^{\prime})$. We invoke $RunSchedule$
first for $\beta_{1}$, obtaining traces $\tau_{9},\tau_{10}$ ending at nodes
$n_{31},n_{32}$. At nodes $n_{31},n_{32}$, we invoke $CreateSchedule$ at
$(end,t3)$ but these will not generate any schedules for the read $r4$ in $t4$
since $swappable$ is FALSE for this read event. Note that $t4[rf]t3$ (along
with $t1[rf]t4,t1[rf]t2$) is covered by trace $\tau_{13}$; thus, we optimize
on redundant traces by keeping $swappable$ FALSE. We backtrack till $(end,t2)$
at $n_{20}$ and invoke $CreateSchedule$ corresponding to the write in $t2$,
which can be a source for the read in $t1$. This adds the schedule
$\gamma_{2}$= $(begin,t2)\dots(end,t2)$ $(begin,t1)(read,t1,t4)(read,t1,t2)$
to $Schedules(e^{\prime\prime})$. On returning from this call, we backtrack
till the read $e^{\prime\prime}$ of $r2=0$ in $t1$ and invoke $RunSchedule$ at
node $n_{7}$ (the green edges $n_{7}-n_{14}-n_{21}$) for $\gamma_{2}$. After
$RunSchedule$ finishes $n_{21}$, we invoke $ExploreTraces$ and obtain traces
$\tau_{11},\tau_{12}$.

At node $n_{34}$ on return from $ExploreTraces$, we backtrack till the read
event $e^{\prime}$ of $r1$ in $t1$ and invoke $RunSchedule$ on the remaining
schedule $\beta_{2}$, obtaining trace $\tau_{13}$.

###  6.2. Complexity, Soundness and Completeness of the DPOR algorithm

Our DPOR algorithm spends polynomial time per explored trace : (1) each
schedule has length bounded by the program length, (2) each schedule we
generate corresponds to a partially good, weak trace which has not been
generated before, and is added to the set of schedules only if it has not been
added. Checking if a new schedule is equal to an existing one can be done in
polynomial time : arrange all created schedules as a tree, and, compare from
the root, with respect to the new schedule, going over the
${\color[rgb]{0,0,1}\it{rf}}$ relations.

###### Theorem 6.1.

The ${\tt CCv}$ DPOR algorithm is sound, complete and optimal.

Soundness. The algorithm is sound in the sense that, if we initiate Algorithm
1 from $(\sigma,\tau_{\emptyset},\epsilon)$, then, all explored traces $\tau$
are s.t. $\tau\in\big{[}[\sigma]\big{]}^{{\tt ful}}_{{\tt CCv}}$. This follows
from the fact that the exploration uses the $\xrightarrow[]{}_{{\tt ful}}$
relation (lines 6, 23 in Algorithm 1 and line 4 in Algorithm 3).

Optimality. The algorithm is optimal in the sense that, for any two different
recursive calls to Algorithm 1 with arguments $(\sigma_{1},\tau_{1},\pi_{1})$
and $(\sigma_{2},\tau_{2},\pi_{2})$, if $\sigma_{1},\sigma_{2}$ are not
terminal, then $weak(\tau_{1})\neq weak(\tau_{2})$. This follows from (i) each
time we run the for loop in line 23, the read event will read from a different
source, (ii) in each schedule $\beta\in schedules(e)$ in line 25 of Algorithm
1, the event $e$ reads from a transaction $t$ which is different from all
transactions it reads from in lines 16, 19, (iii) Any two schedules added to
$schedules(e)$ at line 33 of Algorithm 2 will have a read event reading from
different transactions.

Completeness. The algorithm is complete in the sense that for any input
configuration $\sigma$, it produces all weak traces corresponding to
terminating runs from $\sigma$. That is, for any $\sigma$, terminal run
$\rho\in{\tt ExecFrom}(\sigma)$, and total trace $\tau$ s.t.
$\tau\models\rho$, $ExploreTraces(\sigma,\tau_{\emptyset},\epsilon)$ produces
a recursive call $ExploreTraces(\sigma^{\prime},\tau^{\prime},\pi)$ for some
terminal $\sigma^{\prime},\tau^{\prime}$ and $\pi$ with
$weak(\tau^{\prime})=weak(\tau)$.

##  7\. Experiments

We have implemented our ${\tt CCv},{\tt CC}$-DPOR algorithms as a tool
TranChecker by extending Nidhugg (Abdulla et al., 2015). TranChecker works at
LLVM IR level and accepts a C language program as input. It can detect run-
time errors, user-provided assertion violations by analyzing the generated
weak traces. TranChecker explores each trace from the set of weak traces by
controlling the exploration of the input program. We conduct all experiments
on a Ubuntu 20.04.3 LTS with Intel Core i7-1165G7 and 16 GB RAM. We evaluate
TranChecker on three sets of benchmarks, as seen in Sections 7.1, 7.2 and 7.3.

Table 1. TranChecker on litmus tests. Expected | Observed | Count
---|---|---
Allow | Allow | 94
Forbid | Forbid | 476
Forbid | Allow | 194
Allow | Forbid |  37 [36+1]

Table 2. Evaluating TranChecker on Applications. Applications |  Transactions |  Time
---|---|---
Vote (Difallah et al., 2013) | 3 | 0.11s
Twitter (Holt et al., 2016) | 4 | 0.09s
FusionTicket (Holt et al., 2016) | 8 | 0.51s
Betting (Beillahi et al., 2021a) | 5 | 0.20s
Auction (Nair et al., 2020) | 8 | 0.11s
Auction-2 (Nair et al., 2020) | 8 | 0.27s
Whatsapp | 3 | 0.12s

Table 3.  Evaluating behaviour of TranChecker on classical benchmarks

Program | ${\tt CCv}$ | ${\tt CC}$
---|---|---
Causality Violation (Bernardi and Gotsman, 2016) | SAFE | SAFE
Causal Violation (Biswas and Enea, 2019) | SAFE | SAFE
Co-Read Atomicity | SAFE | UNSAFE
Delivery Order (Beillahi et al., 2021b) | UNSAFE | UNSAFE
Load Buffer | SAFE | SAFE
Long Fork (Bernardi and Gotsman, 2016) | UNSAFE | UNSAFE
Lost Update (Bernardi and Gotsman, 2016) | UNSAFE | UNSAFE
Lost Update-2 (Bernardi and Gotsman, 2016) | UNSAFE | UNSAFE
Modification Order | SAFE | UNSAFE
Message Passing (Beillahi et al., 2021a) | SAFE | SAFE
Conflict violation (Biswas and Enea, 2019) | UNSAFE | UNSAFE
Serializability violation (Biswas and Enea, 2019) | UNSAFE | UNSAFE
Read Atomicity (Biswas and Enea, 2019) | SAFE | SAFE
Read Committed (Biswas and Enea, 2019) | UNSAFE | UNSAFE
Repeated Read (Biswas and Enea, 2019) | SAFE | SAFE
Repeated Read-2 (Biswas and Enea, 2019) | SAFE | UNSAFE
Store Buffer | UNSAFE | UNSAFE
Write-po-Read | SAFE | SAFE
Write-po-Read-2 | SAFE | SAFE
Write Skew (Bernardi and Gotsman, 2016) | UNSAFE | UNSAFE

###  7.1. Evaluation on Litmus Tests

The first set of experiments (Table 1) includes litmus tests from (Alglave et
al., 2014). These litmus tests (Alglave et al., 2014) are non-transactional
programs and are used as a sanity check in tool development. Out of a total of
4000 litmus tests, we selected all litmus tests free of locks and fences, and
where assertions were on local registers. There are 800 such examples. Litmus
tests which had RMW primitives were replaced by a pair of loads and stores and
treated as a single transaction. We instrument these litmus tests into
transactional programs by grouping the instructions in each process
arbitrarily. Given the small number of instructions per process in the litmus
tests of (Alglave et al., 2014), we group all instructions in a process as a
single transaction. In these litmus tests, the processes execute concurrently,
and we check if an assertion is violated or not. Table 3 describes the
outcomes observed on the litmus tests. The column “Expected” represents the
outcomes using Herd-RA (Abdulla et al., 2018) (i.e, the Herd tool together
with the set of RA-axioms provided in (Lahav et al., 2016)). An outcome
$Allow$ in Table 3 means that the program allows an execution that violates
the assertion; otherwise the outcome is $Forbid$. The first and second rows
have litmus tests where the allowed and forbidden behaviours match in Herd-RA

Figure 14.  Program where ${\tt CCv}$ does not have the violating execution of
Herd-RA

as well as for TranChecker, for both ${\tt CCv}$ and ${\tt CC}$. The 3rd row
consists of programs where there is no assertion violation in Herd-RA, but,
under ${\tt CCv}$ and ${\tt CC}$ the violation crops up. ${\tt CCv}$ and ${\tt
CC}$ allows these assertion violations. In the case of ${\tt CC}$, this
follows from the weaker semantics, while for ${\tt CCv}$, this is due to the
replacement of RMW instructions with transactions (as mentioned above). In the
last row we see 37 programs where an assertion violation is expected in Herd-
RA, but is forbidden under ${\tt CCv},{\tt CC}$. We probe further if splitting
the instructions into more transactions will witness the assertion violation
as expected. Doing so, 36 out of the 37 programs witnessed the assertion
violation as expected in Herd-RA. However, one program (Figure 14) under ${\tt
CCv}$ still forbid the assertion violation irrespective of how the
instructions were grouped. This was because executions which were violating
the assertion in Herd-RA were not ${\tt CCv}$ consistent. Under ${\tt CC}$,
after splitting transactions we could witness the violation for this program,
as expected, since the ${\tt CC}$ semantics is weaker than ${\tt CCv}$.

###  7.2. Evaluation on Classical Transactional Anamolies

The second set (Table 3) consists of classical benchmark examples from
databases on well-known transaction related anomalies (Bernardi and Gotsman,
2016), (Biswas and Enea, 2019), (Beillahi et al., 2021b) and (Beillahi et al.,
2021a). We consider twenty examples based on database anomalies. While most of
them are taken from cited sources, the ones without a citation in Table 3 are
created by us, and can be seen in the supplementary material.

For each of these examples, we have made three versions by parameterizing on
the number of processes and transactions. In version 1, we have four processes
per program and two transactions per process. Version 2 is obtained allowing
each process to have four transactions. Version 3 expands version 2 by
allowing each program to have five processes. Versions 2,3 serve as a stress
test for TranChecker as increasing the number of transactions and processes
increases the number of executions to be explored as well as the number of
consistent traces. TranChecker took less than a second to finish running all
version 1 programs, about 15 seconds to finish running all version 2 programs
and about 200 seconds to finish running all version 3 programs. All programs
in Table 3 are classified as SAFE or UNSAFE, depending on whether or not they
have executions violating the assertion. Since programs under ${\tt CC}$
semantics may exhibit more behaviours than ${\tt CCv}$, Co-Read Atomicity,
Modification Order, and Repeated Read-2 are UNSAFE under ${\tt CC}$ semantics
while they are SAFE under the ${\tt CCv}$ semantics.

###  7.3. Evaluation on some Applications

The third set (Table 2) of benchmarks consists of transactional programs
inspired from six distributed systems and database applications (Difallah et
al., 2013), (Holt et al., 2016), (Beillahi et al., 2021b), (Nair et al.,
2020). For each application, TranChecker verifies the assertions given in
these papers on all possible executions. For instance, Auction (Nair et al.,
2020) is a buggy application where the highest bid may not win, while
Auction-2 (Nair et al., 2020) is the non buggy version where only the highest
bid will win. TranChecker detected the execution leading to the bug in Auction
(Nair et al., 2020), and also verified that in all executions of Auction-2,
the highest bid wins. WhatsApp is a synthetic application created by us, where
we verify that a new user can be added to a group only in one execution.

##  8\. Conclusion

We have presented a DPOR algorithm to verify programs running on causally
consistent semantics. We have developed an axiomatic model for such programs
and presented an efficient procedure that allows identifying the set of write
operations that we can read in a given configuration without compromising
causal consistency. While the current paper is a step toward developing a
general DPOR framework that can handle transactions, several exciting
challenges lie ahead. One direction for future work is to consider other
semantics such as serializability. We have to extend the fulfillment procedure
to have an NP-complete complexity rather than polynomial complexity since we
would need techniques similar to those developed in (Abdulla et al., 2019).
Another relevant challenge is to allow abortion and commitment policies, in
which conflicting transactions are rolled back. We would need methods that
allow optimality while at the same avoiding deadlocks in the executions of the
DPOR algorithm (Abdulla et al., 2017).

## References

  * (1)
  * Abdulla et al. (2014) Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014.  Optimal Dynamic Partial Order Reduction. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). Association for Computing Machinery, New York, NY, USA, 373–384.  https://doi.org/10.1145/2535838.2535845
  * Abdulla et al. (2015) Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. 2015.  Stateless Model Checking for TSO and PSO. In Tools and Algorithms for the Construction and Analysis of Systems, Christel Baier and Cesare Tinelli (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 353–367.
  * Abdulla et al. (2017) Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2017.  Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction.  J. ACM 64, 4 (2017), 25:1–25:49.  https://doi.org/10.1145/3073408
  * Abdulla et al. (2019) Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Magnus Lång, Tuan Phong Ngo, and Konstantinos Sagonas. 2019.  Optimal Stateless Model Checking for Reads-from Equivalence under Sequential Consistency.  Proc. ACM Program. Lang. 3, OOPSLA, Article 150 (Oct. 2019), 29 pages.  https://doi.org/10.1145/3360576
  * Abdulla et al. (2018) Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan Phong Ngo. 2018.  Optimal Stateless Model Checking under the Release-Acquire Semantics.  Proc. ACM Program. Lang. 2, OOPSLA, Article 135 (Oct. 2018), 29 pages.  https://doi.org/10.1145/3276505
  * Ahamad et al. (1995) Mustaque Ahamad, Gil Neiger, James E. Burns, Prince Kohli, and Phillip W. Hutto. 1995.  Causal Memory: Definitions, Implementation, and Programming.  Distributed Comput. 9, 1 (1995), 37–49.  https://doi.org/10.1007/BF01784241
  * Alglave et al. (2014) Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014\.  Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory.  ACM Trans. Program. Lang. Syst. 36, 2, Article 7 (jul 2014), 74 pages.  https://doi.org/10.1145/2627752
  * Beillahi et al. (2021a) Sidi Mohamed Beillahi, Ahmed Bouajjani, and Constantin Enea. 2021a.  Checking Robustness Between Weak Transactional Consistency Models.  Programming Languages and Systems 12648 (2021), 87.
  * Beillahi et al. (2021b) Sidi Mohamed Beillahi, Ahmed Bouajjani, and Constantin Enea. 2021b.  Robustness Against Transactional Causal Consistency.  Logical Methods in Computer Science Volume 17, Issue 1 (Feb. 2021).  https://doi.org/10.23638/LMCS-17(1:12)2021
  * Bernardi and Gotsman (2016) Giovanni Bernardi and Alexey Gotsman. 2016.  Robustness against consistency models with atomic visibility. In 27th International Conference on Concurrency Theory (CONCUR 2016). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
  * Biswas and Enea (2019) Ranadeep Biswas and Constantin Enea. 2019.  On the Complexity of Checking Transactional Consistency.  Proc. ACM Program. Lang. 3, OOPSLA, Article 165 (oct 2019), 28 pages.  https://doi.org/10.1145/3360591
  * Bouajjani et al. (2017) Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, and Jad Hamza. 2017.  On Verifying Causal Consistency.  SIGPLAN Not. 52, 1 (Jan. 2017), 626–638.  https://doi.org/10.1145/3093333.3009888
  * Brutschy et al. (2017) Lucas Brutschy, Dimitar K. Dimitrov, Peter Müller, and Martin T. Vechev. 2017.  Serializability for eventual consistency: criterion, analysis, and applications. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. 458–472.  https://doi.org/10.1145/3009837.3009895
  * Brutschy et al. (2018) Lucas Brutschy, Dimitar K. Dimitrov, Peter Müller, and Martin T. Vechev. 2018.  Static serializability analysis for causal consistency, See Foster and Grossman (2018), 90–104.  https://doi.org/10.1145/3192366.3192415
  * Burckhardt (2014) Sebastian Burckhardt. 2014\.  Principles of Eventual Consistency.  Found. Trends Program. Lang. 1, 1-2 (2014), 1–150.  https://doi.org/10.1561/2500000011
  * Cerone and Gotsman (2018) Andrea Cerone and Alexey Gotsman. 2018.  Analysing Snapshot Isolation.  J. ACM 65, 2 (2018), 11:1–11:41.  https://doi.org/10.1145/3152396
  * Cerone et al. (2017) Andrea Cerone, Alexey Gotsman, and Hongseok Yang. 2017\.  Algebraic Laws for Weak Consistency.  CoRR abs/1702.06028 (2017).  arXiv:1702.06028 http://arxiv.org/abs/1702.06028
  * Chalupa et al. (2017) Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. 2017\.  Data-Centric Dynamic Partial Order Reduction.  Proc. ACM Program. Lang. 2, POPL, Article 31 (dec 2017), 30 pages.  https://doi.org/10.1145/3158119
  * Chong et al. (2018) Nathan Chong, Tyler Sorensen, and John Wickerson. 2018\.  The semantics of transactions and weak memory in x86, Power, ARM, and C++, See Foster and Grossman (2018), 211–225.  https://doi.org/10.1145/3192366.3192373
  * Christakis et al. (2013) Maria Christakis, Alkis Gotovos, and Konstantinos Sagonas. 2013\.  Systematic Testing for Detecting Concurrency Errors in Erlang Programs. In Sixth IEEE International Conference on Software Testing, Verification and Validation, ICST 2013, Luxembourg, Luxembourg, March 18-22, 2013. IEEE Computer Society, 154–163.  https://doi.org/10.1109/ICST.2013.50
  * Clarke et al. (1999) Edmund M. Clarke, Orna Grumberg, Marius Minea, and Doron A. Peled. 1999.  State Space Reduction Using Partial Order Techniques.  Int. J. Softw. Tools Technol. Transf. 2, 3 (1999), 279–287.  https://doi.org/10.1007/s100090050035
  * Cormen et al. (2009) Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009.  Introduction to Algorithms, Third Edition (3rd ed.).  The MIT Press.
  * Difallah et al. (2013) Djellel Eddine Difallah, Andrew Pavlo, Carlo Curino, and Philippe Cudre-Mauroux. 2013.  OLTP-Bench: An Extensible Testbed for Benchmarking Relational Databases.  Proc. VLDB Endow. 7, 4 (dec 2013), 277–288.  https://doi.org/10.14778/2732240.2732246
  * Fischer et al. (1985) Michael J. Fischer, Nancy A. Lynch, and Mike Paterson. 1985\.  Impossibility of Distributed Consensus with One Faulty Process.  J. ACM 32, 2 (1985), 374–382.  https://doi.org/10.1145/3149.214121
  * Foster and Grossman (2018) Jeffrey S. Foster and Dan Grossman (Eds.). 2018.  Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018. ACM.  https://doi.org/10.1145/3192366
  * Gilbert and Lynch (2002) Seth Gilbert and Nancy A. Lynch. 2002.  Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services.  SIGACT News 33, 2 (2002), 51–59.  https://doi.org/10.1145/564585.564601
  * Godefroid (1996) Patrice Godefroid. 1996\.  Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. Lecture Notes in Computer Science, Vol. 1032.  Springer.  https://doi.org/10.1007/3-540-60761-7
  * Godefroid (1997) Patrice Godefroid. 1997\.  Model Checking for Programming Languages Using VeriSoft. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’97). Association for Computing Machinery, New York, NY, USA, 174–186.  https://doi.org/10.1145/263699.263717
  * Godefroid (2005) Patrice Godefroid. 2005\.  Software Model Checking: The VeriSoft Approach.  Form. Methods Syst. Des. 26, 2 (March 2005), 77–101.  https://doi.org/10.1007/s10703-005-1489-x
  * Harris et al. (2010) Tim Harris, James R. Larus, and Ravi Rajwar. 2010\.  Transactional Memory, 2nd edition.  Morgan & Claypool Publishers.  https://doi.org/10.2200/S00272ED1V01Y201006CAC011
  * Herlihy and Moss (1993) Maurice Herlihy and J. Eliot B. Moss. 1993.  Transactional Memory: Architectural Support for Lock-Free Data Structures. In Proceedings of the 20th Annual International Symposium on Computer Architecture, San Diego, CA, USA, May 1993, Alan Jay Smith (Ed.). ACM, 289–300.  https://doi.org/10.1145/165123.165164
  * Holt et al. (2016) Brandon Holt, James Bornholt, Irene Zhang, Dan Ports, Mark Oskin, and Luis Ceze. 2016\.  Disciplined Inconsistency with Consistency Types. In Proceedings of the Seventh ACM Symposium on Cloud Computing (SoCC ’16). Association for Computing Machinery, New York, NY, USA, 279–293.  https://doi.org/10.1145/2987550.2987559
  * Kokologiannakis et al. (2018) Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. 2018.  Effective stateless model checking for C/C++ concurrency.  Proc. ACM Program. Lang. 2, POPL (2018), 17:1–17:32.  https://doi.org/10.1145/3158105
  * Kokologiannakis et al. (2022) Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis. 2022.  Truly stateless, optimal dynamic partial order reduction.  Proc. ACM Program. Lang. 6, POPL (2022), 1–28.  https://doi.org/10.1145/3498711
  * Kokologiannakis and Vafeiadis (2021) Michalis Kokologiannakis and Viktor Vafeiadis. 2021.  GenMC: A Model Checker for Weak Memory Models. In Computer Aided Verification, Alexandra Silva and K. Rustan M. Leino (Eds.). Springer International Publishing, Cham, 427–440.
  * Lahav (2019) Ori Lahav. 2019\.  Verification under causally consistent shared memory.  ACM SIGLOG News 6, 2 (2019), 43–56.  https://doi.org/10.1145/3326938.3326942
  * Lahav et al. (2016) Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. 2016\.  Taming Release-Acquire Consistency. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16). Association for Computing Machinery, New York, NY, USA, 649–662.  https://doi.org/10.1145/2837614.2837643
  * Lamport (1978) Leslie Lamport. 1978\.  Time, Clocks, and the Ordering of Events in a Distributed System.  Commun. ACM 21, 7 (1978), 558–565.  https://doi.org/10.1145/359545.359563
  * Lamport (1979) Leslie Lamport. 1979\.  How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs.  IEEE Trans. Computers 28, 9 (1979), 690–691.  https://doi.org/10.1109/TC.1979.1675439
  * Mazurkiewicz (1987) A Mazurkiewicz. 1987\.  Trace Theory. In Advances in Petri Nets 1986, Part II on Petri Nets: Applications and Relationships to Other Models of Concurrency. Springer-Verlag, Berlin, Heidelberg, 279–324.
  * McKinley and Fisher (2019) Kathryn S. McKinley and Kathleen Fisher (Eds.). 2019.  Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019. ACM.  https://doi.org/10.1145/3314221
  * Musuvathi et al. (2008) Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gérard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. 2008.  Finding and Reproducing Heisenbugs in Concurrent Programs. In 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings, Richard Draves and Robbert van Renesse (Eds.). USENIX Association, 267–280.  http://www.usenix.org/events/osdi08/tech/full_papers/musuvathi/musuvathi.pdf
  * Nagar and Jagannathan (2018) Kartik Nagar and Suresh Jagannathan. 2018.  Automated Detection of Serializability Violations Under Weak Consistency. In 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China (LIPIcs), Sven Schewe and Lijun Zhang (Eds.), Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 41:1–41:18.  https://doi.org/10.4230/LIPIcs.CONCUR.2018.41
  * Nair et al. (2020) Sreeja S. Nair, Gustavo Petri, and Marc Shapiro. 2020\.  Proving the Safety of Highly-Available Distributed Objects. In Programming Languages and Systems, Peter Müller (Ed.). Springer International Publishing, Cham, 544–571.
  * Norris and Demsky (2016) Brian Norris and Brian Demsky. 2016.  A Practical Approach for Model Checking C/C++11 Code.  ACM Trans. Program. Lang. Syst. 38, 3, Article 10 (May 2016), 51 pages.  https://doi.org/10.1145/2806886
  * Papadimitriou (1979) Christos H. Papadimitriou. 1979\.  The serializability of concurrent database updates.  J. ACM 26, 4 (1979), 631–653.  https://doi.org/10.1145/322154.322158
  * Perrin et al. (2016) Matthieu Perrin, Achour Mostefaoui, and Claude Jard. 2016\.  Causal Consistency: Beyond Memory.  SIGPLAN Not. 51, 8, Article 26 (feb 2016), 12 pages.  https://doi.org/10.1145/3016078.2851170
  * Raad et al. (2018) Azalea Raad, Ori Lahav, and Viktor Vafeiadis. 2018.  On Parallel Snapshot Isolation and Release/Acquire Consistency. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings (Lecture Notes in Computer Science), Amal Ahmed (Ed.), Vol. 10801. Springer, 940–967.  https://doi.org/10.1007/978-3-319-89884-1_33
  * Raad et al. (2019) Azalea Raad, Ori Lahav, and Viktor Vafeiadis. 2019.  On the Semantics of Snapshot Isolation. In Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13-15, 2019, Proceedings (Lecture Notes in Computer Science), Constantin Enea and Ruzica Piskac (Eds.), Vol. 11388. Springer, 1–23.  https://doi.org/10.1007/978-3-030-11245-5_1
  * Sen and Agha (2006) Koushik Sen and Gul Agha. 2006.  A Race-Detection and Flipping Algorithm for Automated Testing of Multi-Threaded Programs. In Proceedings of the 2nd International Haifa Verification Conference on Hardware and Software, Verification and Testing (HVC’06). Springer-Verlag, Berlin, Heidelberg, 166–182.
  * Shasha and Snir (1988) Dennis E. Shasha and Marc Snir. 1988.  Efficient and Correct Execution of Parallel Programs that Share Memory.  ACM Trans. Program. Lang. Syst. 10, 2 (1988), 282–312.  https://doi.org/10.1145/42190.42277
  * Silva and Leino (2021) Alexandra Silva and K. Rustan M. Leino (Eds.). 2021\.  Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I. Lecture Notes in Computer Science, Vol. 12759. Springer.  https://doi.org/10.1007/978-3-030-81685-8
  * Xiong et al. (2020) Shale Xiong, Andrea Cerone, Azalea Raad, and Philippa Gardner. 2020.  Data Consistency in Transactional Storage Systems: A Centralised Semantics. In 34th European Conference on Object-Oriented Programming, ECOOP 2020, November 15-17, 2020, Berlin, Germany (Virtual Conference) (LIPIcs), Robert Hirschfeld and Tobias Pape (Eds.), Vol. 166. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 21:1–21:31.  https://doi.org/10.4230/LIPIcs.ECOOP.2020.21
  * Zhang et al. (2015) Naling Zhang, Markus Kusano, and Chao Wang. 2015.  Dynamic Partial Order Reduction for Relaxed Memory Models. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). Association for Computing Machinery, New York, NY, USA, 250–259.  https://doi.org/10.1145/2737924.2737956

Appendix

The appendix contains the following sections.

  1. (1)

Programs under ${\tt CCv}$

    1. (a)

The proof of Theorem 4.1 (Appendix A.1)

    2. (b)

The proof of Theorem 5.1 (Appendix B)

    3. (c)

Properties of the fulfilled semantics where we show that all generated traces
are fulfilled and $\models{\tt CCv}$. This proves Lemma 5.2 (Appendix C)

    4. (d)

The proof of Lemma 5.4 (Appendix D.1)

    5. (e)

A new incremental semantics that is equivalent to the total semantics
(Appendix E). The incremental semantics defines the total traces in a step by
step fashion, and simplifies the proof of Theorem 5.5.

    6. (f)

The proof of Theorem 5.5 (Appendix F)

    7. (g)

Proof of the completeness of the DPOR algorithm (Appendix G).

  2. (2)

Programs under ${\tt CC}$

     * (a)

Operational Semantics of ${\tt CC}$ from (Beillahi et al., 2021b) (Appendix H)

     * (b)

Axiomatic Semantics for ${\tt CC}$ (Appendix I.1)

     * (c)

Equivalence of ${\tt CC}$ axiomatic semantics with the operational semantics
(Theorem I.5, Appendix I.1)

     * (d)

${\tt CC}$ Fulfilled Semantics (Appendix J)

     * (e)

DPOR for ${\tt CC}$, soundness, completeness and optimality (Appendix K)

  3. (3)

Experimental Evaluation

     * (a)

The litmus test where the assertion violating execution is not in ${\tt CCv}$,
for any grouping of instructions as transactions (Appendix L.1)

     * (b)

Uncited programs used in Table 6 (Appendix L.2)

     * (c)

Time taken by ${\tt CCv},{\tt CC}$ for all 3 versions of the benchmarks used
in Table 6 (Appendix L.4)

Causal Convergence ${\tt CCv}$

##  Appendix A Equivalence of the Axiomatic and Operational Semantics for
${\tt CCv}$

###  A.1. Proof of Theorem 4.1

###### Proof.

First let us go from traces to legal execution summaries.

###  ${\tt CCv}$-consistent Traces to Legal Execution Summaries

Consider a partial trace
$\tau=(\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},-)$. Assume
that we can extend it to a total, ${\tt CCv}$ consistent trace
$\tau^{\prime}=(\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co})$.
Given $\tau^{\prime}$, we show that we can construct a
$\tau^{\prime}$-consistent, legal execution summary.

Assume that we have processes $p_{1},p_{2},...p_{n}$ in the concurrent program
$\mathcal{P}$ over the set of transactions $\mathcal{T}$. Define for each $i$,

  * •

Let $A_{i}$ be the set of all transactions $t\in\mathcal{T}$ issued in process
$p_{i}$,

  * •

Let $A^{\prime}_{i}=A_{i}\cup\mathcal{T}^{w}$. $A^{\prime}_{i}$ contains all
transactions issued in process $p_{i}$, as well as all transactions in
$\mathcal{T}$ having a write instruction,

  * •

Define the relation $<_{i}=((hb\cap(A^{\prime}_{i}\times
A^{\prime}_{i}))\cup((A_{i}\times(A^{\prime}_{i}\setminus A_{i}))\setminus
hb^{-1})$ where $hb=({\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf})^{+}$.
Relation $<_{i}$ is a strict partial order.

$hb\cap(A^{\prime}_{i}\times A^{\prime}_{i})$ is built on pairs of
transactions $(t,t^{\prime})$ where $t,t^{\prime}$ are issued in $p_{i}$,
representing ${\color[rgb]{1,0,0}po}$, as well as pairs $(t,t^{\prime})$ such
that $t$ is delivered to $p_{i}$ and $t^{\prime}$ is issued in $p_{i}$ after
that, representing a ${\color[rgb]{0,0,1}\it{rf}}$. Likewise,
$((A_{i}\times(A^{\prime}_{i}\setminus A_{i}))\setminus hb^{-1}))$ is built on
pairs (i) $(t,t^{\prime})$ where $t$ is issued in $p_{i}$ and $t^{\prime}$ is
delivered to $p_{i}$ but not issued in $p_{i}$, such that
$(t^{\prime},t)\notin hb$.

Now define two sets of events $T,T^{\prime}$ as follows.

  * •

Let $T=\\{\mathsf{isu}(p_{i},t)\mid 1{\leq}i{\leq}n,t\in
A_{i}\\}\cup\\{\mathsf{del}(p_{i},t)\mid 1{\leq}i{\leq}n,t\in
A^{\prime}_{i}\setminus A_{i}\\}$. Thus, $T$ consists of all transactions $t$
issued in process $p_{i}$, or those transactions $t$ delivered to process
$p_{i}$ (but not issued in $p_{i}$).

  * •

Let $T^{\prime}=\\{\mathsf{isu}(p_{i},t)\mid 1\leq i\leq n,t\in
A_{i}\cap\mathcal{T}^{w}\\}$. $T^{\prime}$ consists of all transactions issued
in process $p_{i}$ which also have a write instruction.

We define the following relations on $T,T^{\prime}$:

  * 1.

$B_{1}=\\{\langle x(p_{i},t),y(p_{i},t^{\prime})\rangle\in T\times T\mid
x,y\in\\{\mathsf{isu},\mathsf{del}\\}\text{ and }t<_{i}t^{\prime}\\}$. $B_{1}$
relates issue and delivery events in the same process $p_{i}$. $B_{1}$ has
pairs $(\mathsf{isu}(p_{i},t),\mathsf{isu}(p_{i},t^{\prime}))$ as well as
$(\mathsf{del}(p_{i},t),\mathsf{isu}(p_{i},t^{\prime}))$ covering
${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}$ relations in each $p_{i}$.
In addition, $B_{1}$ also has the pairs
$(\mathsf{del}(p_{i},t),\mathsf{del}(p_{i},t^{\prime}))$ as well as
$(\mathsf{isu}(p_{i},t),\mathsf{del}(p_{i},t^{\prime}))$. By definition of
${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}$ and $<_{i}$, $B_{1}$ is
irreflexive (or acyclic).

  * 2.

$B_{2}=\\{\langle\mathsf{isu}(p_{i},t),\mathsf{del}(p_{j},t)\rangle\in
T^{\prime}\times T\\}$. $B_{2}$ relates the issue $\mathsf{isu}(p_{i},t)$ of
each transaction $t$ in process $p_{i}$ to its corresponding delivery
$\mathsf{del}(p_{j},t)$ in some process $p_{j}$. Clearly, $B_{2}$ is also
irreflexive.

  * 3.

$B_{3}=\\{\langle\mathsf{isu}(p_{i},t),\mathsf{isu}(p_{j},t^{\prime})\rangle\in
T^{\prime}\times T^{\prime}\mid t[{\color[rgb]{1,.5,0}co}]t^{\prime}\\}$.
$B_{3}$ models the $[{\color[rgb]{1,.5,0}co}]$ relation, and is a total
irreflexive order.

Indeed $B_{1}\cup B_{2}\cup B_{3}$ is irreflexive. We build an execution
summary using $(B_{1}\cup B_{2}\cup B_{3})$, and the relation $<$ induced by
$B_{1},B_{2},B_{3}$. The events in the execution summary are obviously,
$Ev=\\{\mathsf{isu}(p,t),\mathsf{del}(p,t^{\prime})\mid$
$t,t^{\prime}\in\mathcal{T}$ and $p\in\mathbb{P}\\}$, and the ordering $<$ is
defined as $(a,b)\in(B_{1}\cup B_{2}\cup B_{3})^{+}\Rightarrow a<b$.

####  A.1.1. $<$ is a total order

: To show that $(Ev,<)$ is a legal execution summary, one of the things to
show is that $<$ is a total order on the events $Ev$. To this end, we show
that $(B_{1}\cup B_{2}\cup B_{3})^{+}$ is irreflexive.

###### Lemma A.1.

If $\langle x(p_{i},t_{1}),\mathsf{isu}(p_{j},t_{2})\rangle\in(B_{1}\cup
B_{2})^{+}$ then
$t_{1}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{2}$.

###### Proof.

We prove this using induction. If
$(x(p_{i},t_{1}),\mathsf{isu}(p_{j},t_{2}))\in(B_{1}\cup B_{2})^{+}$, then
there is a sequence
$x_{1}(p_{i_{1}},t_{j_{1}})<x_{2}(p_{i_{2}},t_{j_{2}})<\cdot\cdot\cdot
x_{n-1}(p_{i_{n-1}},t_{j_{n-1}})<x_{n}(p_{i_{n}},t_{j_{n}})$, where
$x_{1}(p_{i_{1}},t_{j_{1}})=x(p_{i},t_{1})$ and
$x_{n}(p_{i_{n}},t_{j_{n}})=\mathsf{isu}(p_{j},t_{2})$.

Base Cases. The base cases are $(i)$ $\langle
x(p_{1},t_{1}),\mathsf{isu}(p_{2},t_{2})\rangle\in B_{1}$, this case is
trivial. $(ii)$ $\langle
x_{1}(p_{1},t_{1}),x_{2}(p_{2},t_{2})\rangle\in(B_{1}\cup B_{2})$ and $\langle
x_{2}(p_{2},t_{2}),\mathsf{isu}(p_{3},t_{3})\rangle\in(B_{1}\cup B_{2})$. For
$(ii)$ we consider the following:

  * (1)

$\langle x_{1}(p_{1},t_{1}),x_{2}(p_{2},t_{2})\rangle\in B_{1}$ and $\langle
x_{2}(p_{2},t_{2}),\mathsf{isu}(p_{3},t_{3})\rangle\in B_{1}$. It follows that
$p_{1}=p_{2}=p_{3}$. Hence we have
$t_{1}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{3}$.

  * (2)

$\langle x_{1}(p_{1},t_{1}),x_{2}(p_{2},t_{2})\rangle\in B_{2}$ and $\langle
x_{2}(p_{2},t_{2}),\mathsf{isu}(p_{3},t_{3})\rangle\in B_{1}$.
$\langle x_{1}(p_{1},t_{1}),x_{2}(p_{2},t_{2})\rangle\in B_{2}$ implies that
$t_{1}=t_{2}$ and $x_{2}$ is $\mathsf{del}$ event. Since $\langle
x_{2}(p_{2},t_{2}),\mathsf{isu}(p_{3},t_{3})\rangle\in B_{1}$ we have
$p_{2}=p_{3}$ and
$t_{2}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{3}$. Hence
we have
$t_{1}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{3}$.

Inductive Step. Assume the result for all sequences of length $\leq n-2$, that
is, whenever there is a sequence
$x_{1}(p_{i_{1}},t_{j_{1}})<x_{2}(p_{i_{2}},t_{j_{2}})<\cdots<x_{n-2}(p_{i_{n-2}},t_{j_{n-2}})$
with $x_{n-2}(p_{i_{n-2}},t_{j_{n-2}})=\mathsf{isu}(p_{i_{n-2}},t_{j_{n-2}})$,
we have
$t_{j_{1}}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{j_{n-2}}$.

Consider a sequence of length $n$. Let $\langle
x_{n-2}(p_{i_{n-2}},t_{j_{n-2}}),x_{n-1}(p_{i_{n-1}},t_{j_{n-1}})\rangle\in(B_{1}\cup
B_{2})$
and $\langle
x_{n-1}(p_{i_{n-1}},t_{j_{n-1}}),x_{n}(p_{i_{n}},t_{j_{n}})\rangle\in(B_{1}\cup
B_{2})$, where $x_{n}(p_{i_{n}},t_{j_{n}})=\mathsf{isu}(p_{j},t_{2})$. Here
again we have two cases:

  * (1)

$\langle
x_{n-2}(p_{i_{n-2}},t_{j_{n-2}}),x_{n-1}(p_{i_{n-1}},t_{j_{n-1}})\rangle,\langle
x_{n-1}(p_{i_{n-1}},t_{j_{n-1}}),x_{n}(p_{i_{n}},t_{j_{n}})\rangle\in B_{1}$.
It follows that $p_{i_{n-2}}=p_{i_{n-1}}=p_{i_{n}}=p_{j}$. Hence we have
$t_{j_{n-2}}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{j_{n}}$.
From the inductive hypothesis we have
$t_{1}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{j_{n-2}}$.
Hence we have
$t_{1}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{j_{n}}$,
i.e. $t_{1}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{2}$.

  * (2)

Consider the case when $\langle
x_{n-2}(p_{i_{n-2}},t_{j_{n-2}}),x_{n-1}(p_{i_{n-1}},t_{j_{n-1}})\rangle\in
B_{2}$, and
$\langle x_{n-1}(p_{i_{n-1}},t_{j_{n-1}}),x_{n}(p_{i_{n}},t_{j_{n}})\rangle\in
B_{1}$.

Since $\langle
x_{n-2}(p_{i_{n-2}},t_{j_{n-2}}),x_{n-1}(p_{i_{n-1}},t_{j_{n-1}})\rangle\in
B_{2}$, it follows that $x_{n-1}$ is a $\mathsf{del}$ event and
$t_{j_{n-2}}=t_{j_{n-1}}$. Since $\langle
x_{n-1}(p_{i_{n-1}},t_{j_{n-1}}),x_{n}(p_{i_{n}},t_{j_{n}})\rangle\in B_{1}$,
we have $p_{i_{n-1}}=p_{i_{n}}=p_{j}$ and
$t_{j_{n-1}}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{j_{n}}$,
i.e
$t_{j_{n-2}}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{2}$.
From the inductive hypothesis we have
$t_{1}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{j_{n-2}}$.
Hence we have
$t_{1}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{j_{n}}$,
i.e. $t_{1}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{2}$.

∎

###### Lemma A.2.

$<$ can be extended to a total order .

###### Proof.

We show that $(B_{1}\cup B_{2}\cup B_{3})^{+}$ is irreflexive. This allows us
to extend $<$ to a total order on $Ev$. First of all, notice that $B_{1}\cup
B_{2}\cup B_{3}$ is irreflexive since each of $B_{1},B_{2},B_{3}$ are
irreflexive. We first show that $(B_{1}\cup B_{2})^{+}$ is irreflexive, and
then use this to argue the irreflexivity of $(B_{1}\cup B_{2}\cup B_{3})^{+}$.