Irreflexivity of $(B_{1}\cup B_{2})^{+}$. Assume otherwise. To obtain a
$(x,x)\in(B_{1}\cup B_{2})^{+}$, we must compose $B_{1},B_{2}$, as
individually both $B_{1},B_{2}$ are reflexive.

  1. (1)

Consider the case when we have $\langle
x(p_{i},t_{1}),\mathsf{isu}(p_{j},t_{2})\rangle,\langle\mathsf{isu}(p_{j},t_{2}),y(p_{k},t_{3})\rangle\in
B_{1}\cup B_{2}$, and $\langle
y(p_{k},t_{3}),x(p_{i},t_{1})\rangle\in(B_{1}\cup B_{2})^{+}$. Since $\langle
x(p_{i},t_{1}),\mathsf{isu}(p_{j},t_{2})\rangle\in B_{1}$ and $\langle
y(p_{k},t_{3}),x(p_{i},t_{1})\rangle\in(B_{1}\cup B_{2})^{+}$, we have
$\langle y(p_{k},t_{3}),\mathsf{isu}(p_{j},t_{2})\rangle\in(B_{1}\cup
B_{2})^{+}$.

By Lemma A.1, it follows that
$t_{3}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{2}$.

     * •

If $y(p_{k},t_{3})=\mathsf{isu}(p_{k},t_{3})$.

Then
$\langle\mathsf{isu}(p_{j},t_{2}),y(p_{k},t_{3})\rangle=\langle\mathsf{isu}(p_{j},t_{2}),\mathsf{isu}(p_{k},t_{3})\rangle\in
B_{1}$. Hence $p_{j}=p_{k}$ and $t_{2}[{\color[rgb]{1,0,0}po}]t_{3}$. Thus we
get a cycle
$t_{3}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{2}[{\color[rgb]{1,0,0}po}]t_{3}$.
This contradicts the fact that
$({\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}})^{+}$ is irreflexive.

     * •

If $y(p_{k},t_{3})=\mathsf{del}(p_{k},t_{3})$.

Then $\langle\mathsf{isu}(p_{j},t_{2}),$
$y(p_{k},t_{3})\rangle=\langle\mathsf{isu}(p_{j},t_{2}),\mathsf{del}(p_{k},t_{3})\rangle\in
B_{2}$ and $t_{2}=t_{3}$, i.e we get
$t_{3}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{3}$. This
contradicts the fact that
$({\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}})^{+}$ is irreflexive.

  2. (2)

Another possibility is
$\langle\mathsf{isu}(p_{i},t_{1}),\mathsf{del}(p_{j},t_{2})\rangle\in B_{2}$,
$\langle\mathsf{del}(p_{j},t_{2}),y(p_{k},t_{3})\rangle\in B_{1}\cup B_{2}$,
and $\langle y(p_{k},t_{3}),\mathsf{isu}(p_{i},t_{1})\rangle\in(B_{1}\cup
B_{2})^{+}$. Combining $\langle
y(p_{k},t_{3}),\mathsf{isu}(p_{i},t_{1})\rangle\in(B_{1}\cup B_{2})^{+}$ and
$\langle\mathsf{isu}(p_{i},t_{1}),\mathsf{del}(p_{j},t_{2})\rangle\in B_{2}$,
we get $\langle y(p_{k},t_{3}),\mathsf{del}(p_{j},t_{2})\rangle\in(B_{1}\cup
B_{2})^{+}$.

     * •

If $y(p_{k},t_{3})=\mathsf{isu}(p_{k},t_{3})$.

Then
$\langle\mathsf{del}(p_{j},t_{2}),y(p_{k},t_{3})\rangle=\langle\mathsf{del}(p_{j},t_{2}),\mathsf{isu}(p_{k},t_{3})\rangle\in
B_{1}$. Then $p_{j}=p_{k}$ and $t_{2}[{\color[rgb]{1,0,0}po}]t_{3}$. Then we
get the cycle
$t_{3}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{2}[{\color[rgb]{1,0,0}po}]t_{3}$.

     * •

If $y(p_{k},t_{3})=\mathsf{del}(p_{k},t_{3})$.

Then
$\langle\mathsf{del}(p_{j},t_{2}),y(p_{k},t_{3})\rangle=\langle\mathsf{del}(p_{j},t_{2}),\mathsf{del}(p_{k},t_{3})\rangle\in
B_{1}$. Then $p_{j}=p_{k}$ and $t_{2}[{\color[rgb]{1,0,0}po}]t_{3}$. Then we
get the cycle
$t_{3}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{2}[{\color[rgb]{1,0,0}po}]t_{3}$.

Thus, $(B_{1}\cup B_{2})^{+}$ is irreflexive.

Irreflexivity of $(B_{1}\cup B_{2}\cup B_{3})^{+}$. Assume otherwise. To
obtain $(x,x)\in(B_{1}\cup B_{2}\cup B_{3})^{+}$, we must compose $(B_{1}\cup
B_{2})^{+}$ and $B_{3}$ since, individually, $(B_{1}\cup B_{2})^{+}$ and
$B_{3}$ are irreflexive. To this end, consider $\langle
x(p_{i},t_{1}),\mathsf{isu}(p_{j},t_{2})\rangle\in(B_{1}\cup B_{2})^{+}$ and
$\langle\mathsf{isu}(p_{k},t_{3}),\mathsf{isu}(p_{l},t_{4})\rangle\in B_{3}$.
Then we have
$t_{1}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{2}$ and
$t_{3}[{\color[rgb]{1,.5,0}co}]t_{4}$. Assume a cycle in $(B_{1}\cup B_{2}\cup
B_{3})^{+}$ involving $t_{1},t_{2},t_{3},t_{4}$, of the form
$t_{0}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t^{\prime}_{0}[{\color[rgb]{1,.5,0}co}]t_{1}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t^{\prime}_{1}[{\color[rgb]{1,.5,0}co}]\cdot\cdot\cdot[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t^{\prime}_{n-1}[{\color[rgb]{1,.5,0}co}]t_{n}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t^{\prime}_{n}$
where $t_{0}=t^{\prime}_{n}$. This contradicts the fact that
$({\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co})$
is acyclic.

The irreflexivity of $(B_{1}\cup B_{2}\cup B_{3})^{+}$ shows that we can
extend $<$ to a total order.

∎

We now show how to build an execution summary $S=(Ev,<)$ using the events
$Ev$, and the total order $<$ which is legal and $\tau^{\prime}$-consistent.
Let the execution summary be
$S=\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}$.

$S=(Ev,<)$ is $\tau^{\prime}$-consistent. We show that $S$ satisfies all the
conditions to be $\tau^{\prime}$-consistent below.

  * $\star$

First, each transaction $t\in\mathcal{T}$ is issued in some unique process
$p_{i}$. This is ensured by the total order $<$.

  * $\star$

For $t,t^{\prime}\in\mathcal{T}$, if $t[{\color[rgb]{1,0,0}po}]t^{\prime}$ in
$\tau^{\prime}$, we have $t<_{i}t^{\prime}$ by definition. This gives us
$(\mathsf{isu}(p,t),\mathsf{isu}(p,t^{\prime}))\in B_{1}$, giving
$\ell_{i}=\mathsf{isu}(p,t),\ell_{j}=\mathsf{isu}(p,t^{\prime})$ in $S$ with
$i<j$.

  * $\star$

For $t,t^{\prime}\in\mathcal{T}^{w}$, if
$t[{\color[rgb]{1,.5,0}co}]t^{\prime}$ in $\tau^{\prime}$, then
$(\mathsf{isu}(p_{i},t),\mathsf{isu}(p_{j},t^{\prime}))\in B_{3}$. Then we
have $\ell_{i}=\mathsf{isu}(p_{i},t),\ell_{j}=\mathsf{isu}(p_{j},t^{\prime})$
with $i<j$.

  * $\star$

For $t,t^{\prime}\in\mathcal{T}$, if
$t^{\prime}[{\color[rgb]{0,0,1}\it{rf}}^{x}]t$, then we have
$t^{\prime}<_{i}t$ by definition of $<_{i}$. This gives us
$(\mathsf{del}(p,t^{\prime}),\mathsf{isu}(p,t))\in B_{1}$, giving
$\ell_{i}=\mathsf{del}(p,t^{\prime}),\ell_{j}=\mathsf{isu}(p,t)$ with $i<j$ in
$S$, $t^{\prime}\in\mathcal{T}^{w,x},t\in\mathcal{T}^{r,x}$. It remains to
argue that $t$ reads from the latest transaction which has written on $x$ and
delivered to it, and that is $t^{\prime}$. We show this below in (1).

$S=(Ev,<)$ is a legal execution summary. To show this, we must show the three
conditions of legality hold good.

Recall the function
$S.hb:\mathcal{T}^{r}\rightarrow\mathfrak{p}(\mathcal{T}^{w})$ which
associates a transaction $t$ having a read event, with the set of transactions
$t^{\prime}$ it can read from, defined as
$S.hb(t)=\\{t^{\prime}\in\mathcal{T}^{w}\mid\mathsf{del}(p,t^{\prime})<\mathsf{isu}(p,t)\\}$.
Recall also, the function
$S.lw:\mathcal{T}^{r}\times\mathcal{V}\rightarrow\mathcal{T}^{w}$, which
associates to each transaction $t\in\mathcal{T}^{r}$, the latest transaction
in $[{\color[rgb]{1,.5,0}co}]^{x}$ order it can read $x\in\mathcal{V}$ from.
This is defined as $S.lw(t,x)=\\{t^{\prime}\mid t^{\prime}\in
S.hb(t)\cap\mathcal{T}^{w,x},t\in\mathcal{T}^{r,x}$ and $\forall
t^{\prime\prime}\in S.hb(t)\cap\mathcal{T}^{w,x},t^{\prime\prime}.id\leq
t^{\prime}.id\\}$

  * (1)

The first condition is to show that, each transaction $t$ in process $p_{i}$
reads from the latest write, i.e. $(S.lw(t,x)=t^{\prime})$ when
$t^{\prime}[{\color[rgb]{0,0,1}\it{rf}}^{x}]t$. Let
$(\mathsf{del}(p_{i},t^{\prime}),\mathsf{isu}(p_{i},t))\in B_{1}$ with
$t^{\prime}\in\mathcal{T}^{w,x},t\in\mathcal{T}^{r,x}$, $t^{\prime}\in
S.hb(t)$, and $t^{\prime}[{\color[rgb]{0,0,1}\it{rf}}^{x}]t$. We show that
$S.lw(t,x)=t^{\prime}$.

Assume otherwise, that is, there exists a transaction
$t^{\prime\prime}\in\mathcal{T}^{w,x}$ such that
$(\mathsf{del}(p_{i},t^{\prime\prime}),\mathsf{isu}(p_{i},t)){\in}B_{1}$ and
$S.lw(t,x)=t^{\prime\prime}$. By Lemma A.1,
$t^{\prime\prime}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t$.
Since $t^{\prime}\in S.hb(t)$ and $S.lw(t,x)=t^{\prime\prime}$, we have
$t^{\prime}.id\leq t^{\prime\prime}.id$. Using
$t^{\prime}[{\color[rgb]{0,0,1}\it{rf}}^{x}]t$,
$t^{\prime\prime}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t$
and the fact that $\tau^{\prime}\models{\tt CCv}$, we obtain
$t^{\prime\prime}[{\color[rgb]{1,.5,0}co}^{x}]t^{\prime}$. This implies that
$t^{\prime\prime}.id<t^{\prime}.id$ since we can have
$\mathsf{del}(p,t^{\prime\prime})<\mathsf{isu}(p,t^{\prime})$ but not the
other way around, since
$t^{\prime\prime}[{\color[rgb]{1,.5,0}co}^{x}]t^{\prime}$ implies
$\mathsf{isu}(-,t^{\prime\prime})<\mathsf{isu}(-,t^{\prime})$. This however
contradicts $t^{\prime}.id\leq t^{\prime\prime}.id$, and therefore contradicts
$S.lw(t,x)=t^{\prime\prime}$. Thus, $S.lw(t,x)=t^{\prime}$.

  * (2)

The second condition to prove is this : For transactions
$t,t^{\prime}\in\mathcal{T}^{w}$, if
$\mathsf{del}(p,t)<\mathsf{isu}(p,t^{\prime})$, then
$\mathsf{del}(p^{\prime},t)<\mathsf{del}(p^{\prime},t^{\prime})$ for any
$p^{\prime}\neq p$. If we have $\mathsf{del}(p,t)<\mathsf{isu}(p,t^{\prime})$,
then $(\mathsf{del}(p,t),\mathsf{isu}(p,t^{\prime}))\in B_{1}$. By definition
of $B_{1}$, then we have $t<_{p}t^{\prime}$. By Lemma A.1, we have
$(t,t^{\prime})\in$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}$]+. By definition of
$<_{p^{\prime}}=hb\cap A^{\prime}_{p^{\prime}}\times A^{\prime}_{p^{\prime}}$,
we obtain $t<_{p^{\prime}}t^{\prime}$ since $t,t^{\prime}\in\mathcal{T}^{w}$.
By $B_{1}$, $t<_{p^{\prime}}t^{\prime}$ gives
$\mathsf{del}(p^{\prime},t)<\mathsf{del}(p^{\prime},t^{\prime})$.

  * (3)

The third condition is to show this : for each transaction $t$ and processes
$p,p^{\prime}$, $\mathsf{isu}(p,t)<\mathsf{del}(p^{\prime},t)$. This is given
to us by $B_{2}$ already.

Thus, we have shown that we can construct a $\tau^{\prime}$-consistent, legal
execution summary from the ${\tt CCv}$ consistent trace $\tau^{\prime}$.

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

For the converse direction, assume that we begin with a legal execution
summary $\mathsf{Sum}(\rho)$ corresponding to an execution $\rho$. First, we
define the trace corresponding to $\rho$, denoted $\tau=\mathsf{tr}(\rho)$
following what we did in the main paper. To recall, given
$\mathsf{Sum}(\rho)=(\mathsf{EvSum},<)$,

  * •

For transactions $t,t^{\prime}$, define $t$ [po] $t^{\prime}$ when we have
$ev_{1}=\mathsf{isu}(p,t)$ and $ev_{2}=\mathsf{isu}(p,t^{\prime})$ such that
$ev_{1}<ev_{2}$ in $\tau$. This corresponds to the order of transactions
issued in process $p$. ${\color[rgb]{1,0,0}po}$ does not relate the
initializer transactions.

  * •

$t$ [rf] $t^{\prime}$ relates transactions with delivery and issue events. If
there exists $ev_{1}=\mathsf{del}(p,t)$ and
$ev_{2}=\mathsf{isu}(p,t^{\prime})$ such that $ev_{1}<ev_{2}$ in $\tau$ such
that $t^{\prime}$ performs an _external read_ of some variable $x$ and
$ev_{1}$ is the last event in $\tau$ before $ev_{2}$ that writes to $x$,
$t=S.lw(t^{\prime},x)$. We say that $t^{\prime}$ performs an _external read_
on a variable $x$ in the run $\rho$ if $\rho$ has the read event
$r(p,t^{\prime},x,v)$ which is not preceded by a $w(p,t^{\prime},x,v)$.

The variable $x$ can be made explicit by defining
$t[{\color[rgb]{0,0,1}rf}^{x}]t^{\prime}$.

  * •

$t$ [co] $t^{\prime}$ relates transactions writing on common variables. If
there are events $ev_{1}=\mathsf{isu}(p,t)$ and
$ev_{2}=\mathsf{isu}(q,t^{\prime})$ such that $ev_{1}<ev_{2}$ in $\tau$, such
that $t_{1},t_{2}$ both write on $x$, then $t$ [co] $t^{\prime}$. Note that
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}$.

We now show that the trace $\tau$ as defined above is ${\tt CCv}$ consistent.
For this, we have to show the following.

  1. (1)

For each variable $x$, ${\color[rgb]{1,.5,0}co}^{x}$ respects
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}^{x}]^{+}$. Assume
$t[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}^{x}]^{+}t^{\prime}$ for
$t,t^{\prime}\in\mathcal{T}(\rho)^{w,x}$. Then we have a sequence
$\mathsf{isu}(p,t)<\mathsf{isu}(p,t^{1}_{p})<\dots<\mathsf{isu}(p,t^{n}_{p})<\mathsf{del}(p,t^{n}_{p})<\mathsf{del}(p^{\prime},t^{n}_{p})<\mathsf{isu}(p^{\prime},t^{1}_{p^{\prime}})<\dots\mathsf{isu}(q,t^{\prime})$.
This gives $\mathsf{isu}(p,t)<\mathsf{isu}(q,t^{\prime})$. By definition,
$t[{\color[rgb]{1,.5,0}co}]^{x}t^{\prime}$.

  2. (2)

Assume $t_{1}[{\color[rgb]{0,0,1}rf}^{x}]t_{2}$ and
$t_{3}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}]^{+}t_{2}$. We show
that $t_{3}[{\color[rgb]{1,.5,0}co}^{x}]t_{1}$.

Assume otherwise, that is, $t_{1}[{\color[rgb]{1,.5,0}co}]t_{3}$. Since
$t_{3}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{2}$, we
have $\mathsf{del}(p_{i},t_{3})<\mathsf{isu}(p_{i},t_{2})$, i.e. $t_{3}\in
S.hb(t_{2})$. Since $t_{1}[{\color[rgb]{1,.5,0}co}]t_{3}$, we have
$\mathsf{isu}(p_{j},t_{1})<\mathsf{isu}(p_{k},t_{3})$. Together with
$t_{1},t_{3}\in S.hb(t_{2})$, we have $t_{1}\neq S.lw(t_{2},x)$. Since
$t_{1}[{\color[rgb]{0,0,1}\it{rf}}^{x}]t_{2}$, we have $t_{1}\in S.hb(t_{2})$
and $S.lw(t_{2},x)=t_{1}$. This is a contradiction.

  3. (3)

Now we have to show that
$({\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co})^{+}$
is acyclic.

It is clear that ${\color[rgb]{1,0,0}po}$ cannot generate cycles, since it
picks transactions in increasing order of their identifiers. Likewise,
${\color[rgb]{1,.5,0}co}$ is a total order, which is acyclic.

Assume we have a cycle in
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}]^{+}$. This corresponds to
a sequence
$\mathsf{isu}(p,t)<\dots<\mathsf{del}(q,t)<\mathsf{isu}(q,t_{1})<\dots<\mathsf{del}(r,t_{1})<\mathsf{isu}(p,t)$.
However this gives us $\mathsf{del}(q,t)<\mathsf{isu}(q,t_{1})$ as well as
$\mathsf{del}(r,t_{1})<\mathsf{isu}(p,t)<\mathsf{del}(r,t)$. The last
inequality comes from the third condition of a legal execution. However, this
gives us $\mathsf{del}(q,t)<\mathsf{isu}(q,t_{1})$ and
$\mathsf{del}(r,t_{1})<\mathsf{del}(r,t)$ contradicting the second condition
of legal execution summaries.

Hence,
$({\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co})^{+}$
is acyclic.

∎

##  Appendix B ${\tt CCv}$ Consistency of Partial Traces

###  B.1. Adding Coherence Edges

For 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$,
a variable $x\in\mathcal{X}$, and a pair
$(t,t^{\prime})\in\mathcal{T}^{w,x}\times\mathcal{T}^{w,x}$, we define
$\tau\odot(t_{1},t_{2}):=(\mathcal{T},{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}^{\prime})$,
where
${\color[rgb]{1,.5,0}co}^{\prime}:={\color[rgb]{1,.5,0}co}\cup\\{(t_{1},t_{2})\\}$.

We first give an alternative definition for fulfilled traces.

###### Lemma B.1.

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 _fulfilled_ iff, for all transactions $t,t^{\prime}\in\mathcal{T}^{w,x}$,
$t\neq t^{\prime}$, whenever $t$
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime\prime}$
and $t^{\prime}[{\color[rgb]{0,0,1}rf}^{x}]t^{\prime\prime}$, then $t$
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime}$.

###### Proof.

Recall that we have defined a trace as fulfilled, if for all transactions
$t,t^{\prime}\in\mathcal{T}^{w,x}$, $t\neq t^{\prime}$, 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}$. Now we show that the new
condition in the lemma statement above implies this condition.

Show that the condition

$t$
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime\prime}$
and $t^{\prime}[{\color[rgb]{0,0,1}rf}^{x}]t^{\prime\prime}\Rightarrow t$
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime}$

implies the condition

$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}\Rightarrow t$
$[{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime}$.

Assume $t$
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime\prime}$.
This means either

  * (1)

$t$ $[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}]^{+}t^{\prime\prime}$
(we do not have ${\color[rgb]{1,.5,0}co}^{x}$ edges from $t$ to
$t^{\prime\prime}$), or

  * (2)

$t$
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}^{x}]^{+}s[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}]^{+}t^{\prime\prime}$.

  * (a)

Assume(1). Then we have $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}$. From the given
condition we know $t$
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime}$.
By assumption,
$\neg[t[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime\prime}]$.

Note that if we conclude $t$
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime}$,
then, with $t^{\prime}[{\color[rgb]{0,0,1}rf}^{x}]t^{\prime\prime}$, we will
also get $t$
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime\prime}$,
which by assumption (1) we do not. Thus, we have only $t$
$[{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime}$.

Thus we obtain $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}$ gives $t$
$[{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime}$.

  * (b)

Now consider condition (2), where we have $t$
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}^{x}]^{+}s[{\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}$. From (1) above,
using
$s[{\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}$ we obtain $s$
$[{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime}$. Again, as in (1), if we allow
only $t$
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}]^{+}t^{\prime\prime}$, then
we need to have $t[{\color[rgb]{1,.5,0}co}^{x}]^{+}s$; otherwise we will have
$t$
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}^{x}]^{+}s[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}]^{+}t^{\prime\prime}$.
Hence, $t[{\color[rgb]{1,.5,0}co}^{x}]^{+}s$ and $s$
$[{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime}$ gives
$t[{\color[rgb]{1,.5,0}co}^{x}]^{+}t^{\prime}$.

∎

###### Lemma B.2.

If $\tau_{1}$ is fulfilled, $t_{1}$, $t_{2}\in\mathcal{T}^{w,x}$, $t_{1}\neq
t_{2}$ , and $\tau_{2}=\tau_{1}\odot(t_{1},t_{2})$ then $\tau_{2}$ is
fulfilled.

###### Proof.

Let
$\tau_{1}=(\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co}_{1})$,
and
$\tau_{2}=(\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co}_{2})$.
Suppose that there are transactions $t_{3}$, $t_{4}$, and $t_{5}$ such that
$t_{3}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]+
$t_{5}$ and $t_{4}$ [${\color[rgb]{0,0,1}rf}^{x}$] $t_{5}$. We show that
$t_{3}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]+
$t_{4}$. We consider two cases.

  * (i)

$t_{3}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]+
$t_{5}$. Since $\tau_{1}$ is fulfilled, we will have $t_{3}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]+
$t_{4}$. Since $\tau_{1}\sqsubseteq\tau_{2}$ it follows that $t_{3}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]+
$t_{4}$.

  * (ii)

$t_{3}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}^{x}_{1}$
]+ $t_{1}$ and $t_{2}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]+
$t_{5}$. Note that we added $(t_{1},t_{2})$ as a new $co$ edge to obtain
$\tau_{2}$.

Since $\tau_{1}$ is fulfilled, $t_{2}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]+
$t_{4}$. Moreover, $t_{3}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]+
$t_{1}$ and $\tau_{1}\sqsubseteq\tau_{2}$, so we have $t_{3}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]+
$t_{1}$. Hence, we have $t_{3}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]+
$t_{1}$ [${\color[rgb]{1,.5,0}co}_{2}^{x}$] $t_{2}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]+
$t_{4}$, i.e., we have $t_{3}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]+
$t_{4}$.

∎

###### Lemma B.3.

Assume
$\tau_{1}=\langle\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co}_{1}\rangle$
is fulfilled, $\tau_{1}\models{\tt CCv}$, and there exists $t_{1}$, $t_{2}$
$\in\mathcal{T}^{w,x}$, such that
$\neg[t_{2}({\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{1})^{+}t_{1}]$.
Then $\tau_{2}=\tau_{1}\odot(t_{1},t_{2})$ is such that $\tau_{2}\models{\tt
CCv}$.

###### Proof.

Let
$\tau_{1}=\langle\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co}_{1}\rangle$.
Assume we have a
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}]$
cycle in $\tau_{2}$ : $t$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{2}$]+
$t$. Since $\tau_{1}$ is fulfilled, it follows from Lemma B.2 that $\tau_{2}$
is fulfilled. We consider two possible cases.

  * (i)

$t$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{1}$]+
$t$. This contradicts the premise that
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{1}$]+
is acyclic.

  * (ii)

$t$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{1}]^{+}t_{1}[{\color[rgb]{1,.5,0}co}_{2}^{x}$]
$t_{2}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{1}]^{+}t$.
This means that $t_{2}$
[${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{1}]^{+}t_{1}$
which contradicts the premise that
$\neg[t_{2}({\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{1})^{+}t_{1}]$.

Thus,
$({\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}_{2})^{+}$
is acyclic. Now for the rest of the conditions to show that $\tau_{2}$
respects ${\tt CCv}$.

Assume that $\tau_{2}\nvDash{\tt CCv}$. Since $\tau_{2}$ is fulfilled by Lemma
B.2, the second condition for $\models{\tt CCv}$ holds good. Assume that
${\color[rgb]{1,.5,0}co}_{2}^{x};[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}]^{+}$
is reflexive. Then we have $(t_{1},t_{2})\in{\color[rgb]{1,.5,0}co}_{2}^{x}$,
and $t_{2}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}]^{+}t_{1}$. This
however contradicts our assumption that
$\neg[t_{2}({\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{1})^{+}t_{1}]$.
Hence $\tau_{2}\models{\tt CCv}$.

∎

###  B.2. Proof of Theorem 5.1

###### Proof.

Assume we have a fulfilled, partially good trace
$\tau=\langle\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co}\rangle$.
By definition of partially good traces, we know that $\tau\models{\tt CCv}$
and
$({\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co})^{+}$
is acyclic. To show that $\tau$ is ${\tt CCv}$ consistent, we have to show
that we can extend $\tau$ to a total, ${\tt CCv}$ consistent trace
$\tau^{\prime}$.

For extending $\tau$, we construct a sequence of traces
$\tau=\tau_{0}\sqsubseteq\tau_{1}\sqsubseteq\tau_{2},...$, such that

  1. (1)

Each
$\tau_{i}=\langle\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co}_{i}\rangle$
is fulfilled,

  2. (2)

$\tau_{i}\models{\tt CCv}$

If $\tau_{i}$ is not total, then we generate trace
$\tau_{i+1}=\langle\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}rf},{\color[rgb]{1,.5,0}co}_{i+1}\rangle$,
by adding $t$ $[{\color[rgb]{1,.5,0}co}]$ $t^{\prime}$ to
${\color[rgb]{1,.5,0}co}_{i+1}$ for transactions $t$ and $t^{\prime}$ which
write on some same variable, such that
$\neg(t^{\prime}\,[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}rf}\cup{\color[rgb]{1,.5,0}co}_{i}]^{+}\,t)$
and $\neg(t^{\prime}\,[{\color[rgb]{1,.5,0}co}_{i}]\,t)$. As $\tau_{i}$ is
fulfilled, $\tau_{i+1}$ is also fulfilled (Lemma B.2). Also,
$\tau_{i+1}\models{\tt CCv}$ (Lemma B.3). If $\tau_{i+1}$ is not total, then
we generate trace $\tau_{i+2}$. We continue generating these new traces until
we get a total trace $\tau_{n}$. We obtain $\tau_{n}$ which is total and
$\tau_{n}\models{\tt CCv}$. Hence, $\tau_{n}$ is ${\tt CCv}$-consistent.

So, we successfully extended $\tau$ to a ${\tt CCv}$ consistent total trace
$\tau_{n}$. Hence, $\tau$ is ${\tt CCv}$ consistent. ∎

##  Appendix C Properties of the Fulfilled Semantics

We show that all traces $\tau$ generated in the fulfilled semantics are (i)
fulfilled, and (ii) $\tau\models{\tt CCv}$, and therefore, by Theorem 5.5 are
${\tt CCv}$ consistent. In particular, Lemma C.1, C.2, C.3 and C.4 imply Lemma
5.2.

###### Lemma C.1.

For traces $\tau_{1}$ and $\tau_{2}$ if $\tau_{1}$
$\xrightarrow[]{(begin,t)}_{{\tt ful}}$ $\tau_{2}$, and $\tau_{1}$ is
fulfilled then $\tau_{2}$ is fulfilled.

###### Proof.

Let
$\tau_{1}=\langle\mathcal{T}_{1},{\color[rgb]{1,0,0}po}_{1},{\color[rgb]{0,0,1}rf}_{1},{\color[rgb]{1,.5,0}co}_{1}\rangle$
and
$\tau_{2}=\langle\mathcal{T}_{2},{\color[rgb]{1,0,0}po}_{2},{\color[rgb]{0,0,1}rf}_{2},{\color[rgb]{1,.5,0}co}_{2}\rangle$.
Assume $\tau_{1}$ is fulfilled. By definition of
$\xrightarrow[]{(begin,t)}_{{\tt ful}}$ it follows that
$\mathcal{T}_{1}\subseteq\mathcal{T}_{2},{\color[rgb]{1,0,0}po}_{1}\subseteq{\color[rgb]{1,0,0}po}_{2}$,
${\color[rgb]{0,0,1}\it{rf}}_{1}\subseteq{\color[rgb]{0,0,1}\it{rf}}_{2}$, and
${\color[rgb]{1,.5,0}co}_{1}\subseteq{\color[rgb]{1,.5,0}co}_{2}$. Assume that
$t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}$]+
$t_{2}$, and $t^{\prime}$ [${\color[rgb]{0,0,1}\it{rf}}^{y}_{2}$]$t_{2}$. The
newly added transaction $t\in\mathcal{T}_{2}$ has no successors in
${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}$,
hence it follows that $t_{1}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}$]+
$t_{2}$ and $t^{\prime}$ [${\color[rgb]{0,0,1}\it{rf}}^{y}_{1}$]$t_{2}$. As
$\tau_{1}$ is fulfilled, we have $t_{1}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}$]+
$t^{\prime}$, and hence $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}$]+
$t^{\prime}$. Thus, $\tau_{2}$ is fulfilled whenever $\tau_{1}$ is.

∎

###### Lemma C.2.

For traces $\tau_{1}$ and $\tau_{2}$ if $\tau_{1}$
$\xrightarrow[]{(read,t,t^{\prime})}_{{\tt ful}}$ $\tau_{2}$, and $\tau_{1}$
is fulfilled then $\tau_{2}$ is fulfilled.

###### Proof.

Let
$\tau_{1}=\langle\mathcal{T}_{1},{\color[rgb]{1,0,0}po}_{1},{\color[rgb]{0,0,1}rf}_{1},{\color[rgb]{1,.5,0}co}_{1}\rangle$,
$\tau_{2}=\langle\mathcal{T}_{2},{\color[rgb]{1,0,0}po}_{2},{\color[rgb]{0,0,1}rf}_{2},{\color[rgb]{1,.5,0}co}_{2}\rangle$.
Let $ev=r(p,t,x,v)$ be the read event in $t$, and let
$t^{\prime}\in{\tt{readable}}(\tau,t,x)$ be the chosen transaction that $t$
reads from, while $\tau_{1}$ $\xrightarrow[]{(read,t,t^{\prime})}_{{\tt ful}}$
$\tau_{2}$. Then $\mathcal{T}_{2}=\mathcal{T}_{1}$,
${\color[rgb]{0,0,1}rf}_{2}={\color[rgb]{0,0,1}rf}_{1}\cup(t^{\prime},t)$,
${\color[rgb]{1,.5,0}co}_{2}={\color[rgb]{1,.5,0}co}_{1}\cup\\{(t^{\prime\prime},t^{\prime})\mid
t^{\prime\prime}\in{\tt{visible}}(\tau,t,x)\\}\cup\\{(t^{\prime},t_{2})\mid
t^{\prime}\in\mathcal{T}_{1}^{w,y}$, and
$t_{2}[{\color[rgb]{0,0,1}rf}]^{y}_{2}t\\}$. Assume for any two transactions
$t_{1},t_{2}$ and any variable $y$, $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{y}$]+
$t_{3}$ and $t_{2}$ [${\color[rgb]{0,0,1}\it{rf}}_{2}^{y}$] $t_{3}$. We show
that $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{y}$]+
$t_{2}$. Since $t$ has no successors in
${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}$,
we only need to consider the following cases.

  * $\bullet$

$y$ = $x$, $t_{3}=t$, $t_{2}=t^{\prime}$ and there is a transaction
$t_{4}\in{\tt{visible}}(\tau,t,x)$ such that $t_{1}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]∗
$t_{4}$. From the definition of $\xrightarrow[]{(read,t,t^{\prime})}_{{\tt
ful}}$, we have $t_{4}$ [${\color[rgb]{1,.5,0}co}_{2}^{x}$] $t_{2}$. Since
$t_{1}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]∗
$t_{4}$, we also have $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]∗
$t_{4}$. So we have $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]+
$t_{4}$ [${\color[rgb]{1,.5,0}co}_{2}^{x}$] $t_{2}$.

  * $\bullet$

$y=x$ and there is a transaction $t_{4}\in{\tt{visible}}(\tau,t,x)$. By
definition of $\xrightarrow[]{(read,t,t^{\prime})}_{{\tt ful}}$ we have
$t_{4}$ [${\color[rgb]{1,.5,0}co}_{2}^{x}$] $t^{\prime}$.

By assumption we have $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]+
$t_{3}$ and $t_{2}$ [${\color[rgb]{0,0,1}\it{rf}}_{2}^{x}$] $t_{3}$. Indeed
$t_{2}$ [${\color[rgb]{0,0,1}\it{rf}}_{1}^{x}$] $t_{3}$, since the only new
${\color[rgb]{0,0,1}\it{rf}}$ added to $\tau_{2}$ is $(t^{\prime},t)$. We do
not have $t_{1}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]+
$t_{3}$, since otherwise along with $t_{2}$
[${\color[rgb]{0,0,1}\it{rf}}_{1}^{x}$] $t_{3}$ and the fulfilledness of
$\tau_{1}$ will result in $t_{1}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]+
$t_{2}$ and hence $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]+
$t_{2}$.

Thus, $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]+
$t_{3}$ is obtained using the new
$t_{4}[{\color[rgb]{1,.5,0}co}_{2}^{x}]t^{\prime}$ edge as $t_{1}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]∗
$t_{4}[{\color[rgb]{1,.5,0}co}_{2}^{x}]t^{\prime}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]+
$t_{3}$.

We know that $\tau_{1}$ is fulfilled, and we also have $t_{2}$
[${\color[rgb]{0,0,1}\it{rf}}_{2}^{y}$] $t_{3}$. Together with $t^{\prime}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]+
$t_{3}$, this gives the following.

    1. (1)

either $t_{2}$ [${\color[rgb]{0,0,1}\it{rf}}_{1}^{y}$] $t_{3}$ assuming
$\neg(t_{2}=t^{\prime}\wedge t_{3}=t)$, in which case the fulfilled status of
$\tau_{1}$ gives $t^{\prime}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]+
$t_{2}$ i.e. $t^{\prime}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]+
$t_{2}$,

    2. (2)

$\neg$($t_{2}$ [${\color[rgb]{0,0,1}\it{rf}}_{1}^{y}$] $t_{3}$). Then $t_{2}$
[${\color[rgb]{0,0,1}\it{rf}}_{2}^{y}$] $t_{3}$ is the new reads from
introduced, which means $t_{2}=t^{\prime},t_{3}=t$. This is already handled by
the above bullet. So we again have $t^{\prime}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]+
$t_{2}$ and hence $t^{\prime}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]+
$t_{2}$.

Since $t_{1}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]∗
$t_{4}$ and $t^{\prime}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]+
$t_{3}$, it follows that $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]∗
$t_{4}$ and
$t^{\prime}[{\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]+
$t_{3}$. That is, we have $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]∗
$t_{4}$ [${\color[rgb]{1,.5,0}co}_{2}^{x}$] $t^{\prime}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]+
$t_{2}$. Hence $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]+
$t_{2}$.

  * $\bullet$

$y\neq x$. By assumption, we have $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{y}$]+
$t_{3}$ and $t_{2}$ [${\color[rgb]{0,0,1}\it{rf}}_{2}^{y}$] $t_{3}$. We show
that $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{y}$]+
$t_{2}$. Note that the only new ${\color[rgb]{0,0,1}\it{rf}}_{2}$ added to
$\tau_{2}$ is $(t^{\prime},t)$, hence we also have $t_{2}$
[${\color[rgb]{0,0,1}\it{rf}}_{1}^{y}$] $t_{3}$. Indeed we do not have $t_{1}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{y}$]+
$t_{3}$ : else the fulfilled status of $\tau_{1}$ will already give us $t_{1}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{y}$]+
$t_{2}$ and hence $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{y}$]+
$t_{2}$.

Assume there is a transaction $t_{4}$ such that $t_{4}$
[${\color[rgb]{0,0,1}\it{rf}}_{1}^{y}$] $t$, $y\neq x$, and let
$t^{\prime}\in{\tt{readable}}(\tau,t,x)$ be such that
$t^{\prime}\in\mathcal{T}_{1}^{w,y}\cap\mathcal{T}^{w,x}$. Now by the
definition of $\xrightarrow[]{(read,t,t^{\prime})}_{{\tt ful}}$,
$t^{\prime}\in\mathcal{T}_{1}^{w,y}$ and $t_{4}$
$[{\color[rgb]{0,0,1}rf}_{1}]^{y}t$ gives
$(t^{\prime},t_{4})\in[{\color[rgb]{1,.5,0}co}_{2}]^{y}$.

By assumption, we have $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{y}$]+
$t_{3}$. Since we did not have $t_{1}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{y}$]+
$t_{3}$, using $t^{\prime}[{\color[rgb]{1,.5,0}co}_{2}]^{y}t_{4}$, we can
obtain $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{y}$]+
$t_{3}$ as follows : $t_{1}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{y}$]∗
$t^{\prime}[{\color[rgb]{1,.5,0}co}_{2}]^{y}t_{4}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{y}$]+
$t_{3}$. We have $t_{2}$ [${\color[rgb]{0,0,1}\it{rf}}_{2}^{y}$] $t_{3}$,
which gives $t_{2}$ [${\color[rgb]{0,0,1}\it{rf}}_{1}^{y}$] $t_{3}$, since the
only new ${\color[rgb]{0,0,1}\it{rf}}_{2}$ added is $(t^{\prime},t)$.

The fulfilled status of $\tau_{1}$ along with $t_{4}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{y}$]+
$t_{3}$ and $t_{2}$ [${\color[rgb]{0,0,1}\it{rf}}_{1}^{y}$] $t_{3}$ gives
$t_{4}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{y}$]+
$t_{2}$. Then we have $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{y}$]∗
$t^{\prime}$ [${\color[rgb]{1,.5,0}co}_{2}^{y}$] $t_{4}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{y}$]+
$t_{2}$. This gives us $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{y}$]+
$t_{2}$.

∎

###### Lemma C.3.

If $\tau_{1}\models{\tt CCv}$ and $\tau_{1}$ $\xrightarrow[]{(begin,t)}_{{\tt
ful}}$ $\tau_{2}$ then $\tau_{2}\models{\tt CCv}$.

###### Proof.

The proof follows trivially since we do not change the reads from and
coherence order relations, and the transaction $t$ added to the partial order
has no successors. Thus, if $\tau_{1}\models{\tt CCv}$, so does $\tau_{2}$. ∎

###### Lemma C.4.

If $\tau_{1}\models{\tt CCv}$ and $\tau_{1}$
$\xrightarrow[]{(read,t,t^{\prime})}_{{\tt ful}}$ $\tau_{2}$ then
$\tau_{2}\models{\tt CCv}$.

###### Proof.

Let
$\tau_{1}=\langle\mathcal{T}_{1},{\color[rgb]{1,0,0}po}_{1},{\color[rgb]{0,0,1}rf}_{1},{\color[rgb]{1,.5,0}co}_{1}\rangle$,
$\tau_{2}=\langle\mathcal{T}_{2},{\color[rgb]{1,0,0}po}_{2},{\color[rgb]{0,0,1}rf}_{2},{\color[rgb]{1,.5,0}co}_{2}\rangle$,
and $ev$ = $r(p,t,x,v)$ be a read event in transaction $t\in\mathcal{T}_{1}$.
Suppose $\tau_{2}\nvDash{\tt CCv}$, and that
${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}$
is cyclic. Since $\tau_{1}\models{\tt CCv}$, and $t$ has no outgoing edges, on
adding $(t^{\prime},t)\in{\color[rgb]{0,0,1}rf}_{2}$, it follows that the
cycle in $\tau_{2}$ is as a result of the newly added
${\color[rgb]{1,.5,0}co}_{2}$ edges.

We prove that on adding $(t^{\prime},t)\in{\color[rgb]{0,0,1}rf}_{2}$, such
cycles are possible iff at least one of
${\tt{cond}_{1}},\dots,{\tt{cond}_{4}}$ are true.

###  ${\tt{cond1}}\vee\dots\vee{\tt{cond4}}$ induces
${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}$
cyclicity

This direction is easy to see : assume one of
${\tt{cond1}},\dots,{\tt{cond4}}$ are true; then, as already argued in the
main paper, we will get a
${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}$
cycle on adding the ${\color[rgb]{0,0,1}rf}_{2}$ edge from $t^{\prime}$ to $t$
and we are done.

###
${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}$
cyclicity implies ${\tt{cond1}}\vee\dots\vee{\tt{cond4}}$

For the converse direction, assume that we add the
${\color[rgb]{0,0,1}rf}_{2}$ edge from $t^{\prime}$ to $t$ and obtain a
${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}$
cycle in $\tau_{2}$. We now argue that this cycle has been formed because one
of ${\tt{cond}_{1}},\dots,{\tt{cond}_{4}}$ are true.

First of all, note that $t$ has no outgoing edges in $\tau_{2}$, since it is
the current transaction being executed. Also, we know that $\tau_{1}$ has no
${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}$
cycles. Thus, the cyclicity of
${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}$
is induced by the newly added ${\color[rgb]{0,0,1}\it{rf}}_{2}$ edge as well
as the newly added ${\color[rgb]{1,.5,0}co}_{2}$ edges. Note that adding the
${\color[rgb]{0,0,1}\it{rf}}_{2}$ edge to $\tau_{1}$ does not induce any cycle
since $t$ has no outgoing edges. Lets analyze the
${\color[rgb]{1,.5,0}co}_{2}$ edges added which induce cycles, and argue that
one of ${\tt{cond1}},\dots,{\tt{cond4}}$ will be true.

  1. (1)

We add ${\color[rgb]{1,.5,0}co}_{2}$ edges from
$t^{\prime\prime}\in{\tt{readable}}(\tau_{1},t,x)$ to $t^{\prime}$. For these
edges to induce a cycle, we should have a path from $t^{\prime}$ to
$t^{\prime\prime}$ in $\tau_{1}$. That is, we have
$t^{\prime}[{\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}]^{+}t^{\prime\prime}$.
This is captured by ${\tt{cond1}}$.

  2. (2)

Consider $y\neq x$. If $t^{\prime}\in\mathcal{T}^{w,x}\cap\mathcal{T}^{w,y}$,
and we have $t^{\prime\prime\prime}{\color[rgb]{0,0,1}rf}_{1}^{y}t$. Then we
add $(t^{\prime},t^{\prime\prime\prime})\in{\color[rgb]{1,.5,0}co}^{y}_{2}$.
To get a cycle, we need a path from $t^{\prime\prime\prime}$ to $t^{\prime}$.

     * •

If $t^{\prime\prime\prime}\in\mathcal{T}^{w,x}\cap\mathcal{T}^{w,y}$, then we
add $(t^{\prime\prime\prime},t^{\prime})\in{\color[rgb]{1,.5,0}co}^{x}_{2}$,
resulting in a cycle. This is handled by ${\tt{cond2}}$.

     * •

If we have a path
$t^{\prime\prime\prime}[{\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}]^{+}t^{\prime}$,
then we get a cycle again. This is handled by ${\tt{cond3}}$.

     * •

As a last case, to obtain a path from $t^{\prime\prime\prime}$ to
$t^{\prime}$, assume there is a path from $t^{\prime\prime\prime}$ to $t$ in
$\tau_{1}$, and let $t^{\prime\prime}\in\mathcal{T}^{w,x}$ be the last
transaction writing to $x$ in this path. Note that this will induce a path
from $t^{\prime\prime\prime}$ to $t^{\prime\prime}$ to $t^{\prime}$ : the path
from $t^{\prime\prime}$ to $t^{\prime}$ comes by the
${\color[rgb]{1,.5,0}co}^{x}_{2}$ edge added from $t^{\prime\prime}$ to
$t^{\prime}$ since we have
$(t^{\prime},t)\in{\color[rgb]{0,0,1}\it{rf}}_{2}^{x}$. Once we get this path
from $t^{\prime\prime\prime}$ to $t^{\prime}$, we again have the path we were
looking for to get the cycle. This is handled by ${\tt{cond4}}$.

Thus, we have shown that obtaining a path from $t^{\prime\prime\prime}$ to
$t^{\prime}$ is covered by the conditions
${\tt{cond}_{1}},\dots,{\tt{cond}_{4}}$, and hence, a
${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}$
cycle.

Thus, we can think of
${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}$
cycles as a result of the forbidden patterns described in ${\tt{cond}_{i}}$
$1\leq i\leq 4$. By construction of $\tau_{1}$
$\xrightarrow[]{(read,t,t^{\prime})}_{{\tt ful}}$ $\tau_{2}$, we ensure
$\neg{\tt{cond}_{1}},\dots,\neg{\tt{cond}_{4}}$. Hence, $\tau_{2}\models{\tt
CCv}$.

∎

##  Appendix D Efficiency of Computing Readable and Visible Sets

###  D.1. Proof of Lemma 5.4

###### Proof.

We prove that set ${\tt{readable}}(\tau,t,x)$ can be computed in polynomial
time, by designing an algorithm to generate set ${\tt{readable}}(\tau,t,x)$.
The algorithm consists of the following steps:

  * (i)

First we compute the transitive closure of the relation
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]$,
i.e, we compute
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]^{+}$.
We can use the Floyd-Warshall algorithm (Cormen et al., 2009) to compute the
transitive closure. This will take $O(|\mathcal{T}|^{3})$ time.

  * (ii)

We compute the set $\mathcal{T}^{\prime}=\\{t^{\prime}\mid
t^{\prime}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{*}t\\}$.
This takes $O(|\mathcal{T}|^{2})$ time.

  * (iii)

We compute the set $\mathcal{T}^{\prime\prime}=\\{t^{\prime}\mid
t^{\prime}\in\mathcal{T}^{\prime}\wedge\neg(\exists
t^{\prime\prime}.(t^{\prime}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]^{*}t^{\prime\prime}))\\}$.
It takes $O(|\mathcal{T}|^{2})$ time.

  * (iv)

For each transaction $t^{\prime}\in\mathcal{T}^{w,x}$, we perform following
checks:

    * –

Check $\mathtt{cond1:}$ Check whether there exists a transaction
$t^{\prime\prime}\in\mathcal{T}^{\prime}\cap\mathcal{T}^{w,x}$ with
$t^{\prime}$
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]^{+}$
$t^{\prime\prime}$. If there is no such $t^{\prime\prime}$ then proceed to
$\mathtt{cond2}$. If we find such $t^{\prime\prime}$, then
$t^{\prime}\notin{\tt{readable}}(\tau,t,x)$. This step will take
$O(|\mathcal{T}|^{2})$ time.

    * –

Check $\mathtt{cond2:}$ Check whether there exists a transaction
$t^{\prime\prime}$ such that
$t^{\prime\prime}[{\color[rgb]{0,0,1}\it{rf}}^{y}]t$ and
$t^{\prime},t^{\prime\prime}\in\mathcal{T}^{w,x}\cap\mathcal{T}^{w,y}$. If
there is no such $t^{\prime\prime}$ then proceed to $\mathtt{cond3}$. If we
find such $t^{\prime\prime}$, then
$t^{\prime}\notin{\tt{readable}}(\tau,t,x)$. This step will take
$O(|\mathcal{T}|)$ time.

    * –

Check $\mathtt{cond3:}$

We first check case 1 of $\mathtt{cond3}$. Check whether there exists a
transaction $t^{\prime\prime}$ such that
$t^{\prime\prime}[{\color[rgb]{0,0,1}\it{rf}}^{y}]t$ ,
$t^{\prime}\in\mathcal{T}^{w,y}$, and
$t^{\prime\prime}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]^{+}t^{\prime}$.
If there is no such $t^{\prime\prime}$ then proceed to case two of
$\mathtt{cond3}$. If we find such $t^{\prime\prime}$, then
$t^{\prime}\notin{\tt{readable}}(\tau,t,x)$. This step will take
$O(|\mathcal{T}|)$ time.

Next, we check case 2 of $\mathtt{cond3}$. Check whether there are
transactions $t^{\prime\prime}$ and $t^{\prime\prime\prime}$ such that
$t^{\prime\prime}[{\color[rgb]{0,0,1}\it{rf}}^{y}]t$,
$t^{\prime\prime\prime}\in\mathcal{T}^{w,y}$,
$t^{\prime\prime\prime}[{\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\prime}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]^{+}t^{\prime\prime\prime}$.
If there are no such $t^{\prime\prime}$ and $t^{\prime\prime\prime}$ then
proceed to $\mathtt{cond4}$. If we find such $t^{\prime\prime}$ and
$t^{\prime\prime\prime}$, then $t^{\prime}\notin{\tt{readable}}(\tau,t,x)$.
This step will take $O(|\mathcal{T}|^{2})$ time.

    * –

Check $\mathtt{cond4:}$ Check whether there are transactions
$t^{\prime\prime}$ and $t^{\prime\prime\prime}$ such that
$t^{\prime\prime}[{\color[rgb]{0,0,1}\it{rf}}^{y}]t$,
$t^{\prime\prime\prime}\in\mathcal{T}^{\prime\prime}$ and
$t^{\prime\prime}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]^{+}t^{\prime\prime\prime}$.
If we find such $t^{\prime\prime}$ and $t^{\prime\prime\prime}$, then
$t^{\prime}\notin$ ${\tt{readable}}(\tau,t,x)$. If there are no such
$t^{\prime\prime}$ and $t^{\prime\prime\prime}$ then add $t^{\prime}$ to
${\tt{readable}}(\tau,t,x)$. This step will take $O(|\mathcal{T}|^{2})$ time.

Similarly, we can compute ${\tt{visible}}(\tau,t,x)$ in polynomial time. This
completes the proof. ∎

##  Appendix E Incremental Total Semantics

In this section, we show that the weakenings of traces generated by the
fulfilled semantics coincide with the weakenings of ${\tt CCv}$ consistent
traces. To this end, we introduce a new _incremental_ semantics that is
equivalent to the total ${\tt CCv}$ semantics. The incremental semantics
derives the total, ${\tt CCv}$ consistent traces in an incremental fashion,
step by step, and is used in the proof of Theorem 5.5.

The incremental semantics is given as the transition relation
$\xrightarrow[]{}_{\tt{Inc}}$ on pairs of configurations and traces, defined
as
$(\sigma,\tau)\xrightarrow[]{\alpha}_{\tt{Inc}}(\sigma^{\prime},\tau^{\prime})$.
The label $\alpha$ is one of the following (i) a begin transaction
$(begin,t)$, (ii) a $(write,t)$ corresponding to a write event $w(p,t,x,v)$ in
$t$, (iii) a triple $(read,t,t^{\prime})$ corresponding to a read event
$r(p,t,x,v)$ in transaction $t$, and transaction $t^{\prime}$ which $t$ reads
from, and (iv) an end transaction $(end,t)$. The transitions are described
below.

  * $\bullet$

Transition
$(\sigma,\tau)\xrightarrow[]{(begin,t)}_{\tt{Inc}}(\sigma^{\prime},\tau^{\prime})$
represents extending a total trace after visiting a $\mathsf{begin}(p,t)$
event. Here,
$\tau=\langle\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}\it{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}\it{rf}}^{\prime},{\color[rgb]{1,.5,0}co}^{\prime}\rangle$,
$\mathcal{T}^{\prime}=\mathcal{T}\cup\\{t\\}$ and
${\color[rgb]{1,0,0}po}^{\prime}={\color[rgb]{1,0,0}po}\cup\\{(t^{\prime},t)\mid
t^{\prime}$ is the last transaction from $p$ which has been executed$\\}$.

  * $\bullet$

Transition
$(\sigma,\tau)\xrightarrow[]{(write,t)}_{\tt{Inc}}(\sigma^{\prime},\tau^{\prime})$,
where $ev=w(p,t,x,v)$,
$\tau=\langle\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}\it{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}\it{rf}}^{\prime},{\color[rgb]{1,.5,0}co}^{\prime}\rangle$,
$\mathcal{T}^{\prime}=\mathcal{T}$,
${\color[rgb]{1,0,0}po}^{\prime}={\color[rgb]{1,0,0}po}$,
${\color[rgb]{0,0,1}\it{rf}}^{\prime}={\color[rgb]{0,0,1}\it{rf}}$,
${\color[rgb]{1,.5,0}co}\subseteq{\color[rgb]{1,.5,0}co}^{\prime}$ and
${\color[rgb]{1,.5,0}co}^{\prime}$ is a total order, describing how to extend
the total trace $\tau$ after visiting the write event $ev$ in transaction $t$,
on variable $x$.

  * $\bullet$

Transition
$(\sigma,\tau)\xrightarrow[]{(read,t,t^{\prime})}_{\tt{Inc}}(\sigma^{\prime},\tau^{\prime})$
represents extending the total trace $\tau$ after visiting a read event
$ev=r(p,t,x,v)$ in transaction $t$, and $t$ reads from transaction
$t^{\prime}$. Here,
$\tau=\langle\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}\it{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}\it{rf}}^{\prime},{\color[rgb]{1,.5,0}co}^{\prime}\rangle$,
$\mathcal{T}^{\prime}=\mathcal{T}$,
${\color[rgb]{1,0,0}po}^{\prime}={\color[rgb]{1,0,0}po}$,
${\color[rgb]{0,0,1}\it{rf}}^{\prime}={\color[rgb]{0,0,1}\it{rf}}\cup\\{(t^{\prime},t)\\}$,
${\color[rgb]{1,.5,0}co}^{\prime}={\color[rgb]{1,.5,0}co}$.

  * $\bullet$

Transition
$(\sigma,\tau)\xrightarrow[]{(end,t)}_{\tt{Inc}}(\sigma^{\prime},\tau^{\prime})$,
where $\sigma^{\prime}=\sigma$, and $\tau^{\prime}=\tau$ describes extendind
trace after visiting end event.

We define $\big{[}[\sigma]\big{]}^{\tt{Inc}}$ =
$\\{\tau\mid\exists\sigma^{\prime}.\langle\sigma,\tau_{\emptyset}\rangle\xrightarrow[]{*}_{\tt{Inc}}\langle\sigma^{\prime},\tau\rangle\\}$as
the set of traces generated according to the incremental semantics starting
from configuration $\sigma$ and the empty trace $\tau_{\emptyset}$. We define
$\big{[}[\sigma]\big{]}_{{\tt CCv}}^{\tt{Inc}}$ =
$\big{[}[\sigma]\big{]}^{\tt{Inc}}$ $\cap$ $\\{\tau|\tau$ is ${\tt CCv}$
consistent$\\}$. That is, it is the set of total traces $\tau$ such that
$\tau\models{\tt CCv}$, generated by runs according to the incremental
semantics starting from configuration $\sigma$ and the empty trace.

Starting from a configuration $\sigma$, for each run in the total ${\tt CCv}$
semantics leading to a trace
$\tau=(\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}\it{rf}},{\color[rgb]{1,.5,0}co})$
there is a corresponding run $\big{[}[\sigma]\big{]}_{{\tt CCv}}^{\tt{Inc}}$
in the incremental semantics where the events are scheduled according to the
relations
${\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}\it{rf}},{\color[rgb]{1,.5,0}co}$,
and conversely. Hence we obtain

###### Lemma E.1.

$\big{[}[\sigma]\big{]}_{{\tt CCv}}^{\tt{Inc}}$ =
$\big{[}[\sigma]\big{]}_{{\tt CCv}}$.

##  Appendix F Soundness of the DPOR Algorithm

We prove Theorem 5.5 below.

###  F.1. Proof of Theorem 5.5

We prove the two directions in the coming two subsections. First, in section
F.2, we show that all the weakenings of fulfilled traces are also the
weakenings of ${\tt CCv}$ consistent traces. Then, in section F.3, we show the
converse direction, namely, weakenings of ${\tt CCv}$ consistent traces are
also weakenings of fulfilled traces.

###  F.2. $\\{weak(\tau)|\tau\in\big{[}[\sigma]\big{]}_{{\tt CCv}}^{{\tt
ful}}\\}\subseteq\\{weak(\tau)|\tau\in\big{[}[\sigma]\big{]}_{{\tt CCv}}\\}$

###### Lemma F.1.

If $(\sigma,\tau_{1})\xrightarrow[]{(begin,t)}_{{\tt
ful}}(\sigma^{\prime},\tau_{2})$, $\tau_{2}\sqsubseteq\tau_{4}$, and
$\tau_{4}$ is total then there exists a $\tau_{3}$ such that
$(\sigma,\tau_{3})\xrightarrow[]{(begin,t)}_{\tt{Inc}}(\sigma^{\prime},\tau_{4})$
and $\tau_{1}\sqsubseteq\tau_{3}$.

###### Proof.

Let
$\tau_{1}=\langle\mathcal{T}_{1},{\color[rgb]{1,0,0}po}_{1},{\color[rgb]{0,0,1}\it{rf}}_{1},{\color[rgb]{1,.5,0}co}_{1}\rangle$,
$\tau_{2}=\langle\mathcal{T}_{2},{\color[rgb]{1,0,0}po}_{2},{\color[rgb]{0,0,1}\it{rf}}_{2},{\color[rgb]{1,.5,0}co}_{2}\rangle$,
and
$\tau_{4}=\langle\mathcal{T}_{4},{\color[rgb]{1,0,0}po}_{4},{\color[rgb]{0,0,1}\it{rf}}_{4},{\color[rgb]{1,.5,0}co}_{4}\rangle$.
By definition of $\xrightarrow[]{(begin,t)}_{{\tt ful}}$, we have
$\mathcal{T}_{2}=\mathcal{T}_{1}$,
${\color[rgb]{1,0,0}po}_{2}={\color[rgb]{1,0,0}po}_{1}\cup\\{(t^{\prime},t)\mid$
$t^{\prime}$ is the last transaction executed in process $p\\}$,
${\color[rgb]{0,0,1}\it{rf}}_{2}={\color[rgb]{0,0,1}\it{rf}}_{1}$, and
${\color[rgb]{1,.5,0}co}_{2}={\color[rgb]{1,.5,0}co}_{1}$. Since
$\tau_{2}\sqsubseteq\tau_{4}$ it follows that
$\mathcal{T}_{4}=\mathcal{T}_{2}$,
${\color[rgb]{1,0,0}po}_{4}={\color[rgb]{1,0,0}po}_{2}$,
${\color[rgb]{0,0,1}\it{rf}}_{4}={\color[rgb]{0,0,1}\it{rf}}_{2}$, and
${\color[rgb]{1,.5,0}co}_{2}\subseteq{\color[rgb]{1,.5,0}co}_{4}$.
Define
$\tau_{3}=\langle\mathcal{T}_{3},{\color[rgb]{1,0,0}po}_{3},{\color[rgb]{0,0,1}\it{rf}}_{3},{\color[rgb]{1,.5,0}co}_{3}\rangle$
such that $\mathcal{T}_{3}=\mathcal{T}_{1}$,
${\color[rgb]{1,0,0}po}_{3}={\color[rgb]{1,0,0}po}_{1}$,
${\color[rgb]{0,0,1}\it{rf}}_{3}={\color[rgb]{0,0,1}\it{rf}}_{1}$, and
${\color[rgb]{1,.5,0}co}_{3}={\color[rgb]{1,.5,0}co}_{4}|_{\mathcal{T}_{3}}$,
is the order ${\color[rgb]{1,.5,0}co}_{4}$ restricted to $\mathcal{T}_{3}$. It
follows that
$(\sigma,\tau_{3})\xrightarrow[]{(begin,t)}_{\tt{Inc}}(\sigma^{\prime},\tau_{4})$.
We need to show that
${\color[rgb]{1,.5,0}co}_{1}\subseteq{\color[rgb]{1,.5,0}co}_{3}$. Consider
$t$ [${\color[rgb]{1,.5,0}co}_{1}$] $t^{\prime}$. It follows that $t$
[${\color[rgb]{1,.5,0}co}_{2}$] $t^{\prime}$ and hence $t$
[${\color[rgb]{1,.5,0}co}_{4}$] $t^{\prime}$. Since
$t,t^{\prime}\in\mathcal{T}_{1}$,
${\color[rgb]{1,.5,0}co}_{3}={\color[rgb]{1,.5,0}co}_{4}|_{\mathcal{T}_{3}}$,
and $\mathcal{T}_{3}=\mathcal{T}_{1}$, we have $t$
[${\color[rgb]{1,.5,0}co}_{3}$] $t^{\prime}$. ∎

###### Lemma F.2.

If $(\sigma,\tau_{1})\xrightarrow[]{(write,t)}_{{\tt
ful}}(\sigma^{\prime},\tau_{2})$, $\tau_{2}\sqsubseteq\tau_{4}$, and
$\tau_{4}$ is total then there exists a $\tau_{3}$ such that
$(\sigma,\tau_{3})\xrightarrow[]{(write,t)}_{\tt{Inc}}(\sigma^{\prime},\tau_{4})$
and $\tau_{1}\sqsubseteq\tau_{3}$.

###### Proof.

This follows trivially by the definition of the fulfilled semantics
$\xrightarrow[]{(write,t)}_{{\tt ful}}$. Note that $\sigma=\sigma^{\prime}$,
and $\tau_{1}=\tau_{2}$. Hence, one can choose $\tau_{3}=\tau_{4}$ obtaining
$(\sigma,\tau_{3})\xrightarrow[]{(write,t)}_{\tt{Inc}}(\sigma^{\prime},\tau_{4})$.
∎

###### Lemma F.3.

If $(\sigma,\tau_{1})\xrightarrow[]{(end,t)}_{{\tt
ful}}(\sigma^{\prime},\tau_{2})$, $\tau_{2}\sqsubseteq\tau_{4}$, and
$\tau_{4}$ is total then there exists a $\tau_{3}$ such that
$(\sigma,\tau_{3})\xrightarrow[]{(end,t)}_{\tt{Inc}}(\sigma^{\prime},\tau_{4})$
and $\tau_{1}\sqsubseteq\tau_{3}$.

###### Proof.

This follows in the same lines as Lemma F.2. ∎

###### Lemma F.4.

If $(\sigma,\tau_{1})\xrightarrow[]{(read,t,t^{\prime})}_{{\tt
ful}}(\sigma^{\prime},\tau_{2})$, $\tau_{2}\sqsubseteq\tau_{4}$, and
$\tau_{4}$ is total then there exists a $\tau_{3}$ such that
$(\sigma,\tau_{3})\xrightarrow[]{(read,t,,t^{\prime})}_{\tt{Inc}}(\sigma^{\prime},\tau_{4})$
and $\tau_{1}\sqsubseteq\tau_{3}$.

###### Proof.

Let
$\tau_{1}=\langle\mathcal{T}_{1},{\color[rgb]{1,0,0}po}_{1},{\color[rgb]{0,0,1}\it{rf}}_{1},{\color[rgb]{1,.5,0}co}_{1}\rangle$,
$\tau_{2}=\langle\mathcal{T}_{2},{\color[rgb]{1,0,0}po}_{2},{\color[rgb]{0,0,1}\it{rf}}_{2},{\color[rgb]{1,.5,0}co}_{2}\rangle$,
and
$\tau_{4}=\langle\mathcal{T}_{4},{\color[rgb]{1,0,0}po}_{4},{\color[rgb]{0,0,1}\it{rf}}_{4},{\color[rgb]{1,.5,0}co}_{4}\rangle$.
By definition of $\xrightarrow[]{(read,t,t^{\prime})}_{{\tt ful}}$, we have
$ev=r(p,t,x,v)$, $\mathcal{T}_{2}=\mathcal{T}_{1}$,
${\color[rgb]{1,0,0}po}_{2}={\color[rgb]{1,0,0}po}_{1}$,
${\color[rgb]{0,0,1}\it{rf}}_{2}={\color[rgb]{0,0,1}\it{rf}}_{1}\cup
t^{\prime}[{\color[rgb]{0,0,1}\it{rf}}]t$, and
${\color[rgb]{1,.5,0}co}_{2}={\color[rgb]{1,.5,0}co}_{1}\cup{\color[rgb]{1,.5,0}co}_{2}^{\prime}$,
where
${\color[rgb]{1,.5,0}co}_{2}^{\prime}={\color[rgb]{1,.5,0}co}_{1}\cup\\{t^{\prime\prime}[{\color[rgb]{1,.5,0}co}]t^{\prime}\mid
t^{\prime\prime}\in{\tt{visible}}(\tau_{1},t,x)\\}$, and, if there exists
$t_{2}$ [${\color[rgb]{0,0,1}\it{rf}}_{1}$]y $t$, and
$t^{\prime}\in\mathcal{T}_{1}^{w,y}$, then
${\color[rgb]{1,.5,0}co}_{2}^{\prime}={\color[rgb]{1,.5,0}co}_{2}^{\prime}\cup
t^{\prime}$ [${\color[rgb]{1,.5,0}co}$] $t_{2}$. Since
$\tau_{2}\sqsubseteq\tau_{4}$ it follows that
$\mathcal{T}_{4}=\mathcal{T}_{2}$,
${\color[rgb]{1,0,0}po}_{4}={\color[rgb]{1,0,0}po}_{2}$,
${\color[rgb]{0,0,1}\it{rf}}_{4}={\color[rgb]{0,0,1}\it{rf}}_{2}$, and
${\color[rgb]{1,.5,0}co}_{2}\subseteq{\color[rgb]{1,.5,0}co}_{4}$.

Define
$\tau_{3}=\langle\mathcal{T}_{3},{\color[rgb]{1,0,0}po}_{3},{\color[rgb]{0,0,1}\it{rf}}_{3},{\color[rgb]{1,.5,0}co}_{3}\rangle$
such that $\mathcal{T}_{3}=\mathcal{T}_{1}$,
${\color[rgb]{1,0,0}po}_{3}={\color[rgb]{1,0,0}po}_{1}$,
${\color[rgb]{0,0,1}\it{rf}}_{3}={\color[rgb]{0,0,1}\it{rf}}_{1}={\color[rgb]{0,0,1}\it{rf}}_{4}|_{\mathcal{T}_{3}}$,
${\color[rgb]{1,.5,0}co}_{3}={\color[rgb]{1,.5,0}co}_{4}|_{\mathcal{T}_{3}}$.
It follows that
$\tau_{3}\xrightarrow[]{(read,t,t^{\prime})}_{\tt{Inc}}\tau_{4}$.

We show that
${\color[rgb]{1,.5,0}co}_{1}\subseteq{\color[rgb]{1,.5,0}co}_{3}$. Consider
$t_{1}$ [${\color[rgb]{1,.5,0}co}_{1}$] $t_{2}$. It follows that $t_{1}$
[${\color[rgb]{1,.5,0}co}_{2}$] $t_{2}$ and hence $t_{1}$
[${\color[rgb]{1,.5,0}co}_{4}$] $t_{2}$. Since $t_{1},t_{2}\in\mathcal{T}_{1}$
and
${\color[rgb]{1,.5,0}co}_{3}={\color[rgb]{1,.5,0}co}_{4}|_{\mathcal{T}_{3}}$,
we obtain $t_{1}$ [${\color[rgb]{1,.5,0}co}_{3}$] $t_{2}$. ∎

###### Lemma F.5.

If $(\sigma,\tau_{1})\xrightarrow[]{*}_{{\tt ful}}(\sigma^{\prime},\tau_{2})$,
$\tau_{2}\sqsubseteq\tau_{4}$, and $\tau_{4}$ is total then there exists a
$\tau_{3}$ such that
$(\sigma,\tau_{3})\xrightarrow[]{*}_{\tt{Inc}}(\sigma^{\prime},\tau_{4})$ and
$\tau_{1}\sqsubseteq\tau_{3}$.

###### Proof.

Follows from Lemmas F.1 to F.4. ∎

###### Lemma F.6.

$\\{weak(\tau)|\tau\in\big{[}[\sigma]\big{]}_{{\tt CCv}}^{{\tt
ful}}\\}\subseteq\\{weak(\tau)|\tau\in\big{[}[\sigma]\big{]}^{\tt{Inc}}_{{\tt
CCv}}\\}$ for any configuration $\sigma$.

###### Proof.

Assume $\tau\in\big{[}[\sigma]\big{]}_{{\tt CCv}}^{{\tt ful}}$. We show that
there is a trace $\tau^{\prime}$ s.t.
$\tau^{\prime}\in\big{[}[\sigma]\big{]}_{{\tt CCv}}^{\tt{Inc}}$ s.t.
$\tau\subseteq\tau^{\prime}$. Then we obtain the result.

Since $\tau\in\big{[}[\sigma]\big{]}_{{\tt CCv}}^{{\tt ful}}$, we know that
$(\sigma,\tau_{\emptyset})\xrightarrow[]{*}_{{\tt ful}}(\sigma^{\prime},\tau)$
for some configuration $\sigma^{\prime}$. That is, there is a sequence
$(\sigma_{0},\tau_{0})\xrightarrow[]{}_{{\tt
ful}}(\sigma_{1},\tau_{1})\xrightarrow[]{}_{{\tt
ful}}(\sigma_{2},\tau_{2})\xrightarrow[]{}_{{\tt
ful}}\dots\xrightarrow[]{}_{{\tt ful}}(\sigma_{n},\tau_{n})$ with
$\sigma_{0}=\sigma$, $\tau_{0}=\tau_{\emptyset}$, $\sigma_{n}=\sigma^{\prime}$
and $\tau_{n}=\tau$. Since $\tau_{\emptyset}$ is a fulfilled trace, and
$\tau_{\emptyset}\models{\tt CCv}$, it follows by Lemmas C.1, C.2, C.3 and C.4
that $\tau$ is fulfilled and $\tau\models{\tt CCv}$. By Theorem 5.1 it follows
that $\tau$ is ${\tt CCv}$ consistent, that is, there is a total trace
$\tau^{\prime}$ s.t. $\tau\sqsubseteq\tau^{\prime}$ and
$\tau^{\prime}\models{\tt CCv}$. By Lemma F.5, there is a sequence
$(\sigma_{0},\tau^{\prime}_{0})\xrightarrow[]{}_{\tt{Inc}}(\sigma_{1},\tau^{\prime}_{1})\xrightarrow[]{}_{\tt{Inc}}(\sigma_{2},\tau^{\prime}_{2})\xrightarrow[]{}_{\tt{Inc}}\dots\xrightarrow[]{}_{\tt{Inc}}(\sigma_{n},\tau^{\prime}_{n})$
such that $\tau^{\prime}_{n}=\tau^{\prime}$ and
$\tau_{\emptyset}\sqsubseteq\tau^{\prime}_{0}$.

Note that if we have $\tau_{\emptyset}\sqsubset\tau^{\prime}_{0}$, and have
the run above in the incremental semantics, then we also have a run
$(\sigma_{0},\tau_{\emptyset})\xrightarrow[]{*}_{\tt{Inc}}(\sigma_{n},\tau^{\prime}_{n})$.
This can be seen as follows. If there is no transaction having a write event
in the run from $(\sigma_{0},\tau^{\prime}_{0})$, then no
${\color[rgb]{1,.5,0}co}$ edges get added in the sequence, so in this case we
can assume $\tau^{\prime}_{0}=\tau_{0}$ and $\tau^{\prime}_{n}=\tau_{n}$, and
they are total vacuously. If we encounter write transitions in some
transactions in the sequence, then, even if we begin with
$\tau^{\prime}_{0}=\tau_{\emptyset}$, we can make total, the
${\color[rgb]{1,.5,0}co}$ edges whenever write transitions happen, and reach
$\tau^{\prime}_{n}$. Since $\tau^{\prime}_{0}$ and $\tau_{\emptyset}$ differ
only in the ${\color[rgb]{1,.5,0}co}$ edges, the run starting with
$(\sigma_{0},\tau_{\emptyset})$ can “catch up” with the run starting from
$(\sigma_{0},\tau^{\prime}_{0})$ and reach $\tau^{\prime}_{n}$.

Thus, we obtain the run
$(\sigma_{0},\tau_{\emptyset})\xrightarrow[]{*}_{\tt{Inc}}(\sigma_{n},\tau^{\prime})$,
and hence, $\tau^{\prime}\in\big{[}[\sigma]\big{]}_{{\tt CCv}}^{\tt{Inc}}$.

∎

From Lemma E.1 and Lemma F.6, we obtain

###### Lemma F.7.

$\\{weak(\tau)|\tau\in\big{[}[\sigma]\big{]}_{{\tt CCv}}^{{\tt
ful}}\\}\subseteq\\{weak(\tau)|\tau\in\big{[}[\sigma]\big{]}_{{\tt CCv}}\\}$

###  F.3. $\\{weak(\tau)|\tau\in\big{[}[\sigma]\big{]}^{{\tt ful}}_{{\tt
CCv}}\\}\supseteq\\{weak(\tau)|\tau\in\big{[}[\sigma]\big{]}_{{\tt CCv}}\\}$

###### Lemma F.8.

Given
$\tau_{1}=\langle\mathcal{T}_{1},{\color[rgb]{1,0,0}po}_{1},{\color[rgb]{0,0,1}\it{rf}}_{1},{\color[rgb]{1,.5,0}co}_{1}\rangle$,
$\tau_{2}=\langle\mathcal{T}_{2},{\color[rgb]{1,0,0}po}_{2},{\color[rgb]{0,0,1}\it{rf}}_{2},{\color[rgb]{1,.5,0}co}_{2}\rangle$,
with $(\sigma,\tau_{1})\xrightarrow[]{}_{\tt{Inc}}(\sigma^{\prime},\tau_{2})$
and $\tau_{2}\models{\tt CCv}$, then $\tau_{1}\models{\tt CCv}$.

###### Proof.

By definition of $\xrightarrow[]{}_{\tt{Inc}}$, we know
$\mathcal{T}_{1}\subseteq\mathcal{T}_{2}$,
${\color[rgb]{1,0,0}po}_{1}\subseteq{\color[rgb]{1,0,0}po}_{2}$,
${\color[rgb]{0,0,1}\it{rf}}_{1}\subseteq{\color[rgb]{0,0,1}\it{rf}}_{2}$, and
${\color[rgb]{1,.5,0}co}_{1}\subseteq{\color[rgb]{1,.5,0}co}_{2}$. Since
$\tau_{2}\models{\tt CCv}$, it follows that
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}$]+
is acyclic and the other two conditions are also true for $\tau_{1}$.

∎

###### Lemma F.9.

Given
$\tau_{1}=\langle\mathcal{T}_{1},{\color[rgb]{1,0,0}po}_{1},{\color[rgb]{0,0,1}\it{rf}}_{1},{\color[rgb]{1,.5,0}co}_{1}\rangle$,
$\tau_{2}=\langle\mathcal{T}_{2},{\color[rgb]{1,0,0}po}_{2},{\color[rgb]{0,0,1}\it{rf}}_{2},{\color[rgb]{1,.5,0}co}_{2}\rangle$,
with
$(\sigma,\tau_{1})\xrightarrow[]{(read,t,t^{\prime})}_{\tt{Inc}}(\sigma^{\prime},\tau_{2})$,
reading an event $ev=r(p,t,x,v)$, and $\tau_{2}\models{\tt CCv}$, then
$t^{\prime}\in{\tt{readable}}(\tau_{1},t,x)$.

###### Proof.

From the definition of $\xrightarrow[]{(read,t,t^{\prime})}_{\tt{Inc}}$, we
know $\mathcal{T}_{1}=\mathcal{T}_{2}$,
${\color[rgb]{1,0,0}po}_{2}={\color[rgb]{1,0,0}po}_{1}$,
${\color[rgb]{0,0,1}\it{rf}}_{2}={\color[rgb]{0,0,1}\it{rf}}_{1}\cup
t^{\prime}[{\color[rgb]{0,0,1}\it{rf}}]t$,
${\color[rgb]{1,.5,0}co}_{2}\supseteq{\color[rgb]{1,.5,0}co}_{1}$. $\tau_{1}$
and $\tau_{2}$ are total. Assume
$t^{\prime}\notin{\tt{readable}}(\tau_{1},t,x)$. By the definition of readable
sets, $t^{\prime}\notin{\tt{readable}}(\tau_{1},t,x)$ implies
${\tt{cond1}}\vee{\tt{cond2}}\vee{\tt{cond3}}\vee{\tt{cond4}}$. Using lemmas
from section C, we know that
${\tt{cond1}}\vee{\tt{cond2}}\vee{\tt{cond3}}\vee{\tt{cond4}}$ iff
$[{\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}rf}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}]^{+}$
is cyclic, contradicting $\tau_{2}\models{\tt CCv}$.

∎

###### Lemma F.10.

If $\tau\sqsubseteq\tau^{\prime}$ then
${\tt{readable}}(\tau^{\prime},t,x)\subseteq{\tt{readable}}(\tau,t,x)$.

###### Proof.

If $t^{\prime}\in{\tt{readable}}(\tau^{\prime},t,x)$, then by lemmas from
section C, we know that
$\neg{\tt{cond1}}\wedge\neg{\tt{cond2}}\wedge\neg{\tt{cond3}}\wedge\neg{\tt{cond4}}$.
Since each ${\tt{cond}}$ represents a
$[{\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}rf}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}]^{+}$
cycle, and $\tau\sqsubseteq\tau^{\prime}$, the acyclicity of
$\tau\sqsubseteq\tau^{\prime}$ implies that of
$[{\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}rf}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}]^{+}$.
Thus,
$\neg{\tt{cond1}}\wedge\neg{\tt{cond2}}\wedge\neg{\tt{cond3}}\wedge\neg{\tt{cond4}}$
also hold good for $\tau$ and hence $t^{\prime}\in{\tt{readable}}(\tau,t,x)$.

∎

###### Lemma F.11.

If
$(\sigma,\tau_{1})\xrightarrow[]{(begin,t)}_{\tt{Inc}}(\sigma^{\prime},\tau_{2})$,
and $\tau_{3}\sqsubseteq\tau_{1}$, then there exists a $\tau_{4}$ such that
$(\sigma,\tau_{3})\xrightarrow[]{(begin,t)}_{{\tt
ful}}(\sigma^{\prime},\tau_{4})$ and $\tau_{4}\sqsubseteq\tau_{2}$.

###### Proof.

Let
$\tau_{1}=\langle\mathcal{T}_{1},{\color[rgb]{1,0,0}po}_{1},{\color[rgb]{0,0,1}\it{rf}}_{1},{\color[rgb]{1,.5,0}co}_{1}\rangle$,
$\tau_{2}=\langle\mathcal{T}_{2},{\color[rgb]{1,0,0}po}_{2},{\color[rgb]{0,0,1}\it{rf}}_{2},{\color[rgb]{1,.5,0}co}_{2}\rangle$,
and
$\tau_{3}=\langle\mathcal{T}_{3},{\color[rgb]{1,0,0}po}_{3},{\color[rgb]{0,0,1}\it{rf}}_{3},{\color[rgb]{1,.5,0}co}_{3}\rangle$.
By definition of $\xrightarrow[]{(begin,t)}_{\tt{Inc}}$, we have
$\mathcal{T}_{2}=\mathcal{T}_{1}\cup\\{t\\}$,
${\color[rgb]{1,0,0}po}_{2}={\color[rgb]{1,0,0}po}_{1}\cup\\{(t^{\prime},t)\mid
t^{\prime}$ is the last transaction executed before $t$ in some process
$p\\}$, ${\color[rgb]{0,0,1}\it{rf}}_{2}={\color[rgb]{0,0,1}\it{rf}}_{1}$, and
${\color[rgb]{1,.5,0}co}_{2}={\color[rgb]{1,.5,0}co}_{1}$, and
${\color[rgb]{1,.5,0}co}_{2}$ is total. Since $\tau_{3}\sqsubseteq\tau_{1}$ it
follows that $\mathcal{T}_{3}=\mathcal{T}_{1}$,
${\color[rgb]{1,0,0}po}_{3}={\color[rgb]{1,0,0}po}_{1}$,
${\color[rgb]{0,0,1}\it{rf}}_{3}={\color[rgb]{0,0,1}\it{rf}}_{1}$, and
${\color[rgb]{1,.5,0}co}_{3}\subseteq{\color[rgb]{1,.5,0}co}_{1}$.

Define
$\tau_{4}=\langle\mathcal{T}_{4},{\color[rgb]{1,0,0}po}_{4},{\color[rgb]{0,0,1}\it{rf}}_{4},{\color[rgb]{1,.5,0}co}_{4}\rangle$
such that $\mathcal{T}_{4}=\mathcal{T}_{3}\cup\\{t\\}$,
${\color[rgb]{1,0,0}po}_{4}={\color[rgb]{1,0,0}po}_{3}\cup\\{(t^{\prime},t)\mid
t^{\prime}$ is the last transaction executed before $t$ in some process
$p\\}$, ${\color[rgb]{0,0,1}\it{rf}}_{4}={\color[rgb]{0,0,1}\it{rf}}_{3}$,
${\color[rgb]{1,.5,0}co}_{4}={\color[rgb]{1,.5,0}co}_{3}$. It follows that
$\tau_{3}\xrightarrow[]{t}_{{\tt ful}}\tau_{4}$. We need to show that
${\color[rgb]{1,.5,0}co}_{4}\subseteq{\color[rgb]{1,.5,0}co}_{2}$. Since
${\color[rgb]{1,.5,0}co}_{1}={\color[rgb]{1,.5,0}co}_{2}$,
${\color[rgb]{1,.5,0}co}_{3}\subseteq{\color[rgb]{1,.5,0}co}_{1}$ and
${\color[rgb]{1,.5,0}co}_{4}={\color[rgb]{1,.5,0}co}_{3}$, we get
${\color[rgb]{1,.5,0}co}_{4}\subseteq{\color[rgb]{1,.5,0}co}_{2}$. ∎

###### Lemma F.12.

If
$(\sigma,\tau_{1})\xrightarrow[]{(write,t)}_{\tt{Inc}}(\sigma^{\prime},\tau_{2})$,
and $\tau_{3}\sqsubseteq\tau_{1}$, then there exists a $\tau_{4}$ such that
$(\sigma,\tau_{3})\xrightarrow[]{(write,t)}_{{\tt
ful}}(\sigma^{\prime},\tau_{4})$ and $\tau_{4}\sqsubseteq\tau_{2}$.

###### Proof.

Let
$\tau_{1}=\langle\mathcal{T}_{1},{\color[rgb]{1,0,0}po}_{1},{\color[rgb]{0,0,1}\it{rf}}_{1},{\color[rgb]{1,.5,0}co}_{1}\rangle$,
$\tau_{2}=\langle\mathcal{T}_{2},{\color[rgb]{1,0,0}po}_{2},{\color[rgb]{0,0,1}\it{rf}}_{2},{\color[rgb]{1,.5,0}co}_{2}\rangle$,
and
$\tau_{3}=\langle\mathcal{T}_{3},{\color[rgb]{1,0,0}po}_{3},{\color[rgb]{0,0,1}\it{rf}}_{3},{\color[rgb]{1,.5,0}co}_{3}\rangle$.
By definition of $\xrightarrow[]{(write,t)}_{\tt{Inc}}$, we have
$\mathcal{T}_{2}=\mathcal{T}_{1}$,
${\color[rgb]{1,0,0}po}_{2}={\color[rgb]{1,0,0}po}_{1}$,
${\color[rgb]{0,0,1}\it{rf}}_{2}={\color[rgb]{0,0,1}\it{rf}}_{1}$, and
${\color[rgb]{1,.5,0}co}_{2}\supseteq{\color[rgb]{1,.5,0}co}_{1}$, and
${\color[rgb]{1,.5,0}co}_{2}$ is total. Since $\tau_{3}\sqsubseteq\tau_{1}$ it
follows that $\mathcal{T}_{3}=\mathcal{T}_{1}$,
${\color[rgb]{1,0,0}po}_{3}={\color[rgb]{1,0,0}po}_{1}$,
${\color[rgb]{0,0,1}\it{rf}}_{3}={\color[rgb]{0,0,1}\it{rf}}_{1}$, and
${\color[rgb]{1,.5,0}co}_{3}\subseteq{\color[rgb]{1,.5,0}co}_{1}$.

Define
$\tau_{4}=\langle\mathcal{T}_{4},{\color[rgb]{1,0,0}po}_{4},{\color[rgb]{0,0,1}\it{rf}}_{4},{\color[rgb]{1,.5,0}co}_{4}\rangle$
such that $\mathcal{T}_{4}=\mathcal{T}_{3}$,
${\color[rgb]{1,0,0}po}_{4}={\color[rgb]{1,0,0}po}_{3}$,
${\color[rgb]{0,0,1}\it{rf}}_{4}={\color[rgb]{0,0,1}\it{rf}}_{3}$,
${\color[rgb]{1,.5,0}co}_{4}={\color[rgb]{1,.5,0}co}_{3}$. It follows that
$\tau_{3}\xrightarrow[]{(write,t)}_{{\tt ful}}\tau_{4}$. Since
${\color[rgb]{1,.5,0}co}_{1}\subseteq{\color[rgb]{1,.5,0}co}_{2}$,
${\color[rgb]{1,.5,0}co}_{3}\subseteq{\color[rgb]{1,.5,0}co}_{1}$ and
${\color[rgb]{1,.5,0}co}_{4}={\color[rgb]{1,.5,0}co}_{3}$, we get
${\color[rgb]{1,.5,0}co}_{4}\subseteq{\color[rgb]{1,.5,0}co}_{2}$. ∎

###### Lemma F.13.

If
$(\sigma,\tau_{1})\xrightarrow[]{(end,t)}_{\tt{Inc}}(\sigma^{\prime},\tau_{2})$,
and $\tau_{3}\sqsubseteq\tau_{1}$, then there exists a $\tau_{4}$ such that
$(\sigma,\tau_{3})\xrightarrow[]{(end,t)}_{{\tt
ful}}(\sigma^{\prime},\tau_{4})$ and $\tau_{4}\sqsubseteq\tau_{2}$.

###### Proof.

The proof follows trivially since $\sigma=\sigma^{\prime}$ and
$\tau_{1}=\tau_{2}$. Choosing $\tau_{3}=\tau_{1}$ and $\tau_{4}=\tau_{2}$, we
have the result. ∎

###### Lemma F.14.

If
$(\sigma,\tau_{1})\xrightarrow[]{(read,t,t^{\prime})}_{\tt{Inc}}(\sigma^{\prime},\tau_{2})$,
$\tau_{3}\sqsubseteq\tau_{1}$, and $\tau_{2}\models{\tt CCv}$ then there
exists a $\tau_{4}$ such that
$(\sigma,\tau_{3})\xrightarrow[]{(read,t,t^{\prime})}_{{\tt
ful}}(\sigma^{\prime},\tau_{4})$ and $\tau_{4}\sqsubseteq\tau_{2}$.

###### Proof.

Let
$\tau_{1}=\langle\mathcal{T}_{1},{\color[rgb]{1,0,0}po}_{1},{\color[rgb]{0,0,1}\it{rf}}_{1},{\color[rgb]{1,.5,0}co}_{1}\rangle$,
$\tau_{2}=\langle\mathcal{T}_{2},{\color[rgb]{1,0,0}po}_{2},{\color[rgb]{0,0,1}\it{rf}}_{2},{\color[rgb]{1,.5,0}co}_{2}\rangle$,
and
$\tau_{3}=\langle\mathcal{T}_{3},{\color[rgb]{1,0,0}po}_{3},{\color[rgb]{0,0,1}\it{rf}}_{3},{\color[rgb]{1,.5,0}co}_{3}\rangle$.
By definition of $\xrightarrow[]{(read,t,t^{\prime})}_{\tt{Inc}}$, we have a
read event $ev=r(p,t,x,v)$. Also, $\mathcal{T}_{2}=\mathcal{T}_{1}$,
${\color[rgb]{1,0,0}po}_{2}={\color[rgb]{1,0,0}po}_{1}$,
${\color[rgb]{0,0,1}\it{rf}}_{2}={\color[rgb]{0,0,1}\it{rf}}_{1}\cup
t^{\prime}[{\color[rgb]{0,0,1}\it{rf}}]t$,
${\color[rgb]{1,.5,0}co}_{2}\supseteq{\color[rgb]{1,.5,0}co}_{1}$, and
$\tau_{2}$ is total. Since $\tau_{3}\sqsubseteq\tau_{1}$ it follows that
$\mathcal{T}_{3}=\mathcal{T}_{1}$,
${\color[rgb]{1,0,0}po}_{3}={\color[rgb]{1,0,0}po}_{1}$,
${\color[rgb]{0,0,1}\it{rf}}_{3}={\color[rgb]{0,0,1}\it{rf}}_{1}$, and
${\color[rgb]{1,.5,0}co}_{3}\subseteq{\color[rgb]{1,.5,0}co}_{1}$.

Define
$\tau_{4}=\langle\mathcal{T}_{4},{\color[rgb]{1,0,0}po}_{4},{\color[rgb]{0,0,1}\it{rf}}_{4},{\color[rgb]{1,.5,0}co}_{4}\rangle$
such that $\mathcal{T}_{4}=\mathcal{T}_{3}$,
${\color[rgb]{1,0,0}po}_{4}={\color[rgb]{1,0,0}po}_{3}$,
${\color[rgb]{0,0,1}\it{rf}}_{4}={\color[rgb]{0,0,1}\it{rf}}_{3}\cup
t^{\prime}[{\color[rgb]{0,0,1}\it{rf}}]t$,
${\color[rgb]{1,.5,0}co}_{4}={\color[rgb]{1,.5,0}co}_{3}\cup{\color[rgb]{1,.5,0}co}_{3}^{\prime}$,
where
${\color[rgb]{1,.5,0}co}_{3}^{\prime}={\color[rgb]{1,.5,0}co}_{3}\cup\\{t^{\prime\prime}[{\color[rgb]{1,.5,0}co}]t^{\prime}\mid
t^{\prime\prime}\in{\tt{visible}}(\tau_{3},t,x)\\}$, and if $\exists t_{2}$
[${\color[rgb]{0,0,1}\it{rf}}_{1}$]y $t$, and
$t^{\prime}\in\mathcal{T}^{w,y}$, then
${\color[rgb]{1,.5,0}co}_{3}^{\prime}={\color[rgb]{1,.5,0}co}_{3}^{\prime}\cup
t^{\prime}$ [${\color[rgb]{1,.5,0}co}$] $t_{2}$. From Lemmas F.9, F.10 it
follows that $t^{\prime}\in{\tt{readable}}(\tau_{3},t,x)$, since
$t^{\prime}\in{\tt{readable}}(\tau_{1},t,x)$ and
$\tau_{3}\sqsubseteq\tau_{1}$. Hence we have
$\tau_{3}\xrightarrow[]{(read,t,t^{\prime})}_{\tt{Inc}}\tau_{4}$. We need to
show that ${\color[rgb]{1,.5,0}co}_{4}\subseteq{\color[rgb]{1,.5,0}co}_{2}$.
Assume $t_{1}{\color[rgb]{1,.5,0}co}_{4}t_{2}$. We consider the following
cases:

  * $\bullet$

$t_{1}{\color[rgb]{1,.5,0}co}_{3}t_{2}$. Since
${\color[rgb]{1,.5,0}co}_{3}\subseteq{\color[rgb]{1,.5,0}co}_{1}$, it follows
that $t_{1}{\color[rgb]{1,.5,0}co}_{1}t_{2}$. It follows that
$t_{1}{\color[rgb]{1,.5,0}co}_{2}t_{2}$.

  * $\bullet$

$t_{2}=t^{\prime}$ and $t_{1}\in{\tt{visible}}(\tau_{3},t,x)$. Since
$t_{1}\in{\tt{visible}}(\tau_{3},t,x)$, we have
$t_{1}[{\color[rgb]{1,0,0}po}_{3}\cup{\color[rgb]{0,0,1}\it{rf}}_{3}]^{+}t$,
and hence
$t_{1}[{\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}]^{+}t$.
It follows that
$t_{1}[{\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}]^{+}t$.
Since $\tau_{2}\models{\tt CCv}$ and
$t^{\prime}[{\color[rgb]{0,0,1}\it{rf}}_{2}^{x}]t$, we get
$t_{1}[{\color[rgb]{1,.5,0}co}_{2}]t^{\prime}$.

  * $\bullet$

$t_{1}=t^{\prime}$ and $t_{2}[{\color[rgb]{0,0,1}\it{rf}}_{3}^{y}]t$ and
$t^{\prime}\in\mathcal{T}^{w,y}$. Since $\tau_{3}\subseteq\tau_{1}$ and
$(\sigma,\tau_{1})\xrightarrow[]{(read,t,t^{\prime})}_{\tt{Inc}}(\sigma^{\prime},\tau_{2})$,
it follows that $t_{2}[{\color[rgb]{0,0,1}\it{rf}}_{1}^{y}]t$ and
$t_{2}[{\color[rgb]{0,0,1}\it{rf}}_{2}^{y}]t$. Since
$t_{2}[{\color[rgb]{0,0,1}\it{rf}}_{2}^{y}]t$, and $t$ reads from $t^{\prime}$
(hence
$t^{\prime}[{\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}]^{+}t$),
and $\tau_{2}\models{\tt CCv}$, we get
$t^{\prime}[{\color[rgb]{1,.5,0}co}_{2}]t_{2}$, i.e.
$t_{1}[{\color[rgb]{1,.5,0}co}_{2}]t_{2}$.

∎

###### Lemma F.15.

$\\{weak(\tau)|\tau\in\big{[}[\sigma]\big{]}_{{\tt
CCv}}^{\tt{Inc}}\\}\subseteq\\{weak(\tau)|\tau\in\big{[}[\sigma]\big{]}_{{\tt
CCv}}^{{\tt ful}}\\}$ for any configuration $\sigma$.

###### Proof.

Suppose $\tau\in\big{[}[\sigma]\big{]}_{{\tt CCv}}^{\tt{Inc}}$. We show that
there is a trace $\tau^{\prime}\in\big{[}[\sigma]\big{]}_{{\tt CCv}}^{{\tt
ful}}$ s.t. $\tau^{\prime}\sqsubseteq\tau$. Then the result follows
immediately.

Since $\tau\in\big{[}[\sigma]\big{]}_{{\tt CCv}}^{\tt{Inc}}$, it follows that
$\tau\models{\tt CCv}$ and that
$(\sigma,\tau_{\emptyset})\xrightarrow[]{*}_{\tt{Inc}}(\sigma^{\prime},\tau)$
for some configuration $\sigma^{\prime}$. That is, there is a sequence
$(\sigma_{0},\tau_{0}\xrightarrow[]{}_{\tt{Inc}}(\sigma_{1},\tau_{1})\xrightarrow[]{}_{\tt{Inc}}\dots\xrightarrow[]{}_{\tt{Inc}}(\sigma_{n},\tau_{n})$
where
$\sigma_{0}=\sigma,\tau_{0}=\tau_{\emptyset},\sigma_{n}=\sigma,\tau_{n}=\tau$.
By Lemma F.8, we know that $\tau_{i}\models{\tt CCv}$ for all $1\leq i\leq n$.
By Lemmas F.11, F.12, F.13, F.14, it follows that there is a sequence
$(\sigma_{0},\tau^{\prime}_{0})\xrightarrow[]{}_{{\tt
ful}}(\sigma_{1},\tau^{\prime}_{1})\xrightarrow[]{}_{{\tt
ful}}\dots\xrightarrow[]{}_{{\tt ful}}(\sigma_{n},\tau^{\prime}_{n})$ with
$\tau^{\prime}_{0}=\tau_{\emptyset}$ and
$\tau^{\prime}_{i}\sqsubseteq\tau_{i}$ for $1\leq i\leq n$. Define
$\tau^{\prime}=\tau^{\prime}_{n}$.

∎

From Lemma E.1 and Lemma F.15 we obtain

###### Lemma F.16.

$\\{weak(\tau)|\tau\in\big{[}[\sigma]\big{]}^{{\tt ful}}_{{\tt
CCv}}\\}\supseteq\\{weak(\tau)|\tau\in\big{[}[\sigma]\big{]}_{{\tt CCv}}\\}$.

##  Appendix G Completeness

In this section, we show the completeness of the DPOR algorithm. More
precisely, for any configuration $\sigma$, terminating run $\rho\in{\tt
ExecFrom}(\sigma)$ and total trace $\tau$ s.t. $\tau\models\rho$, we show that
$ExploreTraces(\sigma,\tau_{\emptyset},\epsilon)$ will produce a recursive
visit $ExploreTraces(\sigma^{\prime},\tau^{\prime},\pi)$ for some terminal
$\sigma^{\prime}$, $\tau^{\prime}$, and $\pi$ where
$weak(\tau^{\prime})=weak(\tau)$. First we give some definitions and auxiliary
lemmas.

Let $\pi=\alpha_{t_{1}}\alpha_{t_{2}}\dots\alpha_{t_{n}}$ be an observation
sequence where $\alpha_{t}=\mathsf{begin}(p,t)\dots$ $\mathtt{end}$$(p,t)$.
$\alpha_{t}$ is called an _observable_ , and is a sequence of events from
transaction $t$. Given $\pi$, a configuration $\sigma$, and a trace $\tau$, we
define $\langle\sigma,\tau\rangle\vdash_{\tt{G}}\pi$ to represent a sequence
$\langle\sigma_{0},\tau_{0}\rangle\xrightarrow[]{\alpha_{t_{1}}}_{{\tt
ful}}\langle\sigma_{1},\tau_{1}\rangle\xrightarrow[]{\alpha_{t_{2}}}_{{\tt
ful}}\cdot\cdot\cdot\xrightarrow[]{\alpha_{t_{n}}}_{{\tt
ful}}\langle\sigma_{n},\tau_{n}\rangle$, where $\sigma_{0}=\sigma$,
$\tau_{0}=\tau$ and $\pi=\alpha_{t_{1}}\alpha_{t_{2}}\dots\alpha_{t_{n}}$.
Moreover, we define $\pi(\sigma,\tau):=\langle\sigma_{n},\tau_{n}\rangle$. We
define $\tau\vdash_{\tt{G}}\pi$ in similar manner, when there exists some
$\sigma$ s.t. $(\sigma,\tau)\vdash_{\tt{G}}\pi$.

$\langle\sigma,\tau\rangle$ is $terminal$ if $\sigma$ is terminal. We define
$\langle\sigma,\tau\rangle\vdash_{\tt{G_{T}}}\pi$ to say that $(i)$
$\langle\sigma,\tau\rangle\vdash_{\tt{G}}\pi$ and $(ii)$ $\pi(\sigma,\tau)$ is
terminal.

###### Definition G.1.

($p$-free and $t$-free observation sequences) For a process $p\in\mathbf{P}$,
we say that an observation sequence $\pi$ is $p$-free if all observables
$\alpha_{t}$ in $\pi$ pertain to transactions $t$ not in $p$. For a
transaction $t$ issued in $p$ we say that $\pi$ is $t$-free if $\pi$ is
$p$-free.

###### Definition G.2.

(Independent Observables) For observables $\alpha_{t_{1}}$ and
$\alpha_{t_{2}}$, we write $\alpha_{t_{1}}\sim\alpha_{t_{2}}$ to represent
they are independent. This means $(i)$ $t_{1},t_{2}$ are transactions issued
in different processes, that is, $t_{1}$ is issed in $p_{1}$, $t_{2}$ is
issued in $p_{2}$, with $p_{1}\neq p_{2}$, $(ii)$ no read event
$r(p_{2},t_{2},x,v)$ of transaction $t_{2}$ reads from $t_{1}$, and $(iii)$ no
read event $r(p_{1},t_{1},x,v)$ of transaction $t_{1}$ reads from $t_{2}$.
Thus, $\neg(\alpha_{t_{1}}\sim\alpha_{t_{2}})$ if either $t_{1},t_{2}$ are
issued in the same process, or there is a ${\color[rgb]{0,0,1}\it{rf}}$
relation between $t_{1},t_{2}$. That is,
$\neg(\alpha_{t_{1}}\sim\alpha_{t_{2}})$ iff
$t_{1}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{2}$ or
$t_{2}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t_{1}$.

###### Definition G.3.

(Independent Observation Sequences) Observation sequences $\pi^{1},\pi^{2}$
are called independent written $\pi^{1}\sim\pi^{2}$ if there are observables
$\alpha_{t_{1}}$, $\alpha_{t_{2}}$, and observation sequences $\pi^{\prime}$
and $\pi^{\prime\prime}$ such that
$\pi^{1}=\pi^{\prime}\cdot\alpha_{t_{1}}\cdot\alpha_{t_{2}}\cdot\pi^{\prime\prime}$,
$\pi^{2}=\pi^{\prime}\cdot\alpha_{t_{2}}\cdot\alpha_{t_{1}}\cdot\pi^{\prime\prime}$,
and $\alpha_{t_{1}}\sim\alpha_{t_{2}}$. In other words, we get $\pi^{2}$ from
$\pi^{1}$ by swapping neighbouring independent observables corresponding to
transactions $t_{1}$ and $t_{2}$.

We use $\approx$ to denote reflexive transitive closure of $\sim$.

###### Definition G.4.

(Equivalent Traces) For traces
$\tau_{1}=\langle\mathcal{T}_{1},{\color[rgb]{1,0,0}po}_{1},{\color[rgb]{0,0,1}rf}_{1},{\color[rgb]{1,.5,0}co}_{1}\rangle$
and
$\tau_{2}=\langle\mathcal{T}_{2},{\color[rgb]{1,0,0}po}_{2},{\color[rgb]{0,0,1}rf}_{2},{\color[rgb]{1,.5,0}co}_{2}\rangle$,
we say $\tau_{1},\tau_{2}$ are equivalent denoted $\tau_{1}\equiv\tau_{2}$ if
$\mathcal{T}_{1}=\mathcal{T}_{2}$,
${\color[rgb]{1,0,0}po}_{1}={\color[rgb]{1,0,0}po}_{2}$,
${\color[rgb]{0,0,1}\it{rf}}_{1}={\color[rgb]{0,0,1}\it{rf}}_{2}$ and for all
$t_{1}$,$t_{2}\in\mathcal{T}_{1}^{w,x}$ for all variables $x$, we have $t_{1}$
[${\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}$]
$t_{2}$ iff $t_{1}$
[${\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}$]
$t_{2}$.

###### Lemma G.5.

$((\tau_{1}\equiv\tau_{2})\wedge\tau_{1}\vdash_{\tt{G}}\alpha_{t})\Rightarrow(\tau_{2}\vdash_{\tt{G}}\alpha_{t}\wedge(\alpha_{t}(\tau_{1})\equiv\alpha_{t}(\tau_{2})))$.

###### Proof.

Assume $\tau_{1}\vdash_{\tt{G}}\alpha_{t}$ for an observable $\alpha_{t}$, and
$\tau_{1}=(\mathcal{T}_{1},{\color[rgb]{1,0,0}po}_{1},{\color[rgb]{0,0,1}\it{rf}}_{1},{\color[rgb]{1,.5,0}co}_{1})$,
$\tau_{2}=(\mathcal{T}_{2},{\color[rgb]{1,0,0}po}_{2},{\color[rgb]{0,0,1}\it{rf}}_{2},{\color[rgb]{1,.5,0}co}_{2})$
with $\tau_{1}\equiv\tau_{2}$. Then we know that
$\mathcal{T}_{1}=\mathcal{T}_{2},{\color[rgb]{1,0,0}po}_{1}={\color[rgb]{1,0,0}po}_{2},{\color[rgb]{0,0,1}\it{rf}}_{2}={\color[rgb]{0,0,1}\it{rf}}_{1}$.

Since $\tau_{1}\vdash_{\tt{G}}\alpha_{t}$, let
$\tau_{1}\xrightarrow[]{\alpha_{t}}_{{\tt ful}}\tau^{\prime}$.
$\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})$
where $\mathcal{T}^{\prime}=\mathcal{T}_{1}\cup\\{t\\}$,
${\color[rgb]{1,0,0}po}^{\prime}={\color[rgb]{1,0,0}po}_{1}\cup\\{(t_{1},t)\mid
t_{1}\in\mathcal{T}_{1}$ is in the same process as $t\\}$,
${\color[rgb]{1,.5,0}co}_{1}\subseteq{\color[rgb]{1,.5,0}co}^{\prime}$ and
${\color[rgb]{0,0,1}\it{rf}}_{1}\subseteq{\color[rgb]{0,0,1}\it{rf}}^{\prime}$.
${\color[rgb]{1,.5,0}co}^{\prime}$ can contain $(t^{\prime},t)$ for some
$t^{\prime}\in\mathcal{T}_{1}$, when
$t^{\prime},t\in{\mathcal{T}^{\prime}}^{w,x}$ for some variable $x$, based on
the fulfilled semantics. In particular if we have
$t_{1}{{\color[rgb]{0,0,1}\it{rf}}^{\prime}}^{x}t_{2}$ and
$t_{3}({\color[rgb]{0,0,1}\it{rf}}^{\prime}\cup{\color[rgb]{1,0,0}po}^{\prime}\cup{{\color[rgb]{1,.5,0}co}^{\prime}}^{x})^{+}t_{2}$,
then $t_{3}{{\color[rgb]{1,.5,0}co}^{\prime}}^{x}t_{1}$.

Since $\tau_{1}\equiv\tau_{2}$, for any transactions
$t^{\prime},t^{\prime\prime}$ in $\mathcal{T}_{1}=\mathcal{T}_{2}$,
$t^{\prime}[{\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}]t^{\prime\prime}$
iff
$t^{\prime}[{\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}]t^{\prime\prime}$
for all variables $x$. In particular,
$t^{\prime}{\color[rgb]{1,.5,0}co}_{1}^{x}t^{\prime\prime}$ iff
$t^{\prime}{\color[rgb]{1,.5,0}co}_{2}^{x}t^{\prime\prime}$ for all $x$. Now,
let us construct a trace
$\tau^{\prime\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\prime})$,
where ${\color[rgb]{1,.5,0}co}^{\prime\prime}$ is the smallest set such that
${\color[rgb]{1,.5,0}co}_{2}\subseteq{\color[rgb]{1,.5,0}co}^{\prime\prime}$
and whenever $t_{1}{{\color[rgb]{0,0,1}\it{rf}}^{\prime}}^{x}t_{2}$ and
$t_{3}({\color[rgb]{0,0,1}\it{rf}}^{\prime}\cup{\color[rgb]{1,0,0}po}^{\prime}\cup{{\color[rgb]{1,.5,0}co}^{\prime\prime}}^{x})^{+}t_{2}$,
then $t_{3}{{\color[rgb]{1,.5,0}co}^{\prime\prime}}^{x}t_{1}$.

Since
$t^{\prime}[{\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}^{x}]t^{\prime\prime}$
iff
$t^{\prime}[{\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}^{x}]t^{\prime\prime}$
for all $x$, and all
$t^{\prime},t^{\prime\prime}\in\mathcal{T}_{1}=\mathcal{T}_{2}$, and
${\color[rgb]{1,.5,0}co}^{\prime\prime}$ is the smallest extension of
${\color[rgb]{1,.5,0}co}_{2}$ based on the fulfilled semantics, along with the
fact that
${\color[rgb]{1,0,0}po}^{\prime}={\color[rgb]{1,0,0}po}^{\prime\prime},{\color[rgb]{0,0,1}\it{rf}}^{\prime}={\color[rgb]{0,0,1}\it{rf}}^{\prime\prime}$,
we obtain for any two transactions
$t_{1},t_{2}\in\mathcal{T}^{\prime}=\mathcal{T}^{\prime\prime}$,
$t_{1}[{\color[rgb]{1,0,0}po}^{\prime}\cup{\color[rgb]{0,0,1}\it{rf}}^{\prime}\cup{\color[rgb]{1,.5,0}co}^{\prime}]t_{2}$
iff
$t_{1}[{\color[rgb]{1,0,0}po}^{\prime\prime}\cup{\color[rgb]{0,0,1}\it{rf}}^{\prime\prime}\cup{\color[rgb]{1,.5,0}co}^{\prime\prime}]t_{2}$.
This gives $\tau^{\prime}\equiv\tau^{\prime\prime}$.

This also gives $\tau_{2}\xrightarrow[]{\alpha_{t}}_{{\tt
ful}}\tau^{\prime\prime}$, that is, $\tau_{2}\vdash_{\tt{G}}\alpha_{t}$ and
indeed
$\alpha_{t}(\tau_{1})=\tau^{\prime}\equiv\tau^{\prime\prime}=\alpha_{t}(\tau_{2})$.

∎

###### Lemma G.6.

If $\tau\vdash_{\tt{G}}\alpha_{t_{1}}\cdot\alpha_{t_{2}}$ and
$\alpha_{t_{1}}{\sim}\alpha_{t_{2}}$ then
$\tau\vdash_{\tt{G}}\alpha_{t_{2}}{\cdot}\alpha_{t_{1}}$ and
$(\alpha_{t_{1}}{\cdot}\alpha_{t_{2}})(\tau)\equiv(\alpha_{t_{2}}{\cdot}\alpha_{t_{1}})(\tau)$.

###### Proof.

Let
$\tau=\langle\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}\it{rf}},{\color[rgb]{1,.5,0}co}\rangle$
be a trace and let $t_{1}$ be a transaction issued in process $p_{1}$, and
$t_{2}$ be a transaction issued in process $p_{2}$, with $p_{1}\neq p_{2}$.
Assume $\tau\vdash_{\tt{G}}\alpha_{t_{1}}\cdot\alpha_{t_{2}}$, with
$\alpha_{t_{1}}{\sim}\alpha_{t_{2}}$.

We consider the following cases.

  * $\bullet$

$t_{1},t_{2}\notin\mathcal{T}^{r}$. In this case
$\tau\vdash_{\tt{G}}\alpha_{t_{2}}\cdot\alpha_{t_{1}}$ holds trivially.

$(\alpha_{t_{1}}\cdot\alpha_{t_{2}})(\tau)=(\alpha_{t_{2}}\cdot\alpha_{t_{1}})(\tau)=\langle\mathcal{T}^{\prime},{\color[rgb]{1,0,0}po}^{\prime},{\color[rgb]{0,0,1}\it{rf}},{\color[rgb]{1,.5,0}co}\rangle$,
where $\mathcal{T}^{\prime}=\mathcal{T}\cup\\{t_{1},t_{2}\\}$ and
${\color[rgb]{1,0,0}po}^{\prime}={\color[rgb]{1,0,0}po}\cup\\{(t,t_{1})|t\in
p_{1}\\}\cup\\{(t^{\prime},t_{2})|t^{\prime}\in p_{2}\\}$.

  * $\bullet$

$t_{1}\in\mathcal{T}^{w}$, $t_{1}\notin\mathcal{T}^{r}$ and
$t_{2}\in\mathcal{T}^{r}\cap\mathcal{T}^{w}$. Let
$\tau_{1}=\alpha_{t_{1}}(\tau)$. We know that
$\tau_{1}=\langle\mathcal{T}_{1},{\color[rgb]{1,0,0}po}_{1},{\color[rgb]{0,0,1}\it{rf}}_{1},{\color[rgb]{1,.5,0}co}_{1}\rangle$,
where $\mathcal{T}_{1}=\mathcal{T}\cup\\{t_{1}\\}$, and
${\color[rgb]{1,0,0}po}_{1}={\color[rgb]{1,0,0}po}\cup\\{(t,t_{1})|t\in
p_{1}\\}$, with ${\color[rgb]{0,0,1}\it{rf}}_{1}={\color[rgb]{0,0,1}\it{rf}}$
since there are no read events in $t_{1}$, and
${\color[rgb]{1,.5,0}co}_{1}={\color[rgb]{1,.5,0}co}$ since by the fulfilled
semantics, when ${\color[rgb]{0,0,1}\it{rf}}$ remain same, there are no
${\color[rgb]{1,.5,0}co}$ edges to be added.

Consider
$\tau_{2}=\alpha_{t_{2}}(\tau_{1})=\langle\mathcal{T}_{2},{\color[rgb]{1,0,0}po}_{2},{\color[rgb]{0,0,1}\it{rf}}_{2},{\color[rgb]{1,.5,0}co}_{2}\rangle$.
Since $t_{2}\in\mathcal{T}^{r}$, we know that $t_{2}$ has read events.

Let there be $n$ read events $ev_{1}\dots ev_{n}$ in transaction $t_{2}$,
reading from transactions $t^{\prime}_{1},\dots,t^{\prime}_{n}$ on variables
$x_{1},\dots,x_{n}$. Hence we get a sequence
$\tau_{1}\xrightarrow[]{(begin,t_{2})}_{{\tt
ful}}\dots\tau^{\prime}_{i_{1}}\xrightarrow[]{(read,t_{2},t^{\prime}_{1})}_{{\tt
ful}}\tau_{i_{1}}\xrightarrow[]{}_{{\tt
ful}}\dots\tau^{\prime}_{i_{n}}\xrightarrow[]{(read,t_{2},t^{\prime}_{n})}_{{\tt
ful}}\tau_{i_{n}}\dots\xrightarrow[]{(end,t_{2})}_{{\tt ful}}\tau_{2}$. Hence
$\mathcal{T}_{2}=\mathcal{T}_{1}\cup\\{t_{2}\\}$,
${\color[rgb]{1,0,0}po}_{2}={\color[rgb]{1,0,0}po}_{1}\cup\\{(t^{\prime},t_{2})|t^{\prime}\in
p_{2}\\}$,
${\color[rgb]{0,0,1}\it{rf}}_{2}={\color[rgb]{0,0,1}\it{rf}}_{1}\cup({\color[rgb]{0,0,1}\it{rf}}_{i_{1}}\cup{\color[rgb]{0,0,1}\it{rf}}_{i_{2}}\dots\cup{\color[rgb]{0,0,1}\it{rf}}_{i_{n}})$,
and
${\color[rgb]{1,.5,0}co}_{2}={\color[rgb]{1,.5,0}co}_{1}\cup({\color[rgb]{1,.5,0}co}_{i_{1}}\cup{\color[rgb]{1,.5,0}co}_{i_{2}}\dots\cup{\color[rgb]{1,.5,0}co}_{i_{n}})$.
Since $\tau_{1}\vdash_{\tt{G}}\alpha_{t_{2}}$, for all $ev_{i}:1\leq i\leq n$,
we have $t^{\prime}_{i}\in{\tt{readable}}(\tau_{1},t_{2},x_{i})$.

Since $\alpha_{t_{1}}\sim\alpha_{t_{2}}$, we know that for all $ev_{i}:1\leq
i\leq n$, we have $t^{\prime}_{i}\in{\tt{readable}}(\tau,t_{2},x_{i})$. It
follows that $\tau\vdash_{\tt{G}}\alpha_{t_{2}}$. Define
$\tau_{3}=\langle\mathcal{T}_{3},{\color[rgb]{1,0,0}po}_{3},{\color[rgb]{0,0,1}\it{rf}}_{2},{\color[rgb]{1,.5,0}co}_{2}\rangle$,
where $\mathcal{T}_{3}=\mathcal{T}\cup\\{t_{2}\\}$ and
${\color[rgb]{1,0,0}po}_{3}={\color[rgb]{1,0,0}po}\cup\\{(t^{\prime},t_{2})|t^{\prime}\in
p_{2}\\}$. It follows that $\alpha_{t_{2}}(\tau)=\tau_{3}$,
$\tau_{3}\vdash_{\tt{G}}\alpha_{t_{1}}$ and
$\tau_{2}=\alpha_{t_{1}}(\tau_{3})=\alpha_{t_{2}}(\alpha_{t_{1}}(\tau))$.

  * $\bullet$

$t_{2}\in\mathcal{T}^{w}$ and $t_{1}\in\mathcal{T}^{r}\cap\mathcal{T}^{w}$.
Similar to previous case.

  * $\bullet$

$t_{1},t_{2}\in\mathcal{T}^{r}\cap\mathcal{T}^{w}$. Let
$\tau_{1}=\alpha_{t_{1}}(\tau)=\langle\mathcal{T}_{1},{\color[rgb]{1,0,0}po}_{1},{\color[rgb]{0,0,1}\it{rf}}_{1},{\color[rgb]{1,.5,0}co}_{1}\rangle$
and $\tau_{2}=\alpha_{t_{2}}(\tau_{1})$. Since $t_{1}\in\mathcal{T}^{r}$, we
know that $t_{1}$ has read events. Let there be $n$ read events $ev_{1}\dots
ev_{n}$ in transaction $t_{1}$, reading from transactions
$t^{\prime}_{1},\dots,t^{\prime}_{n}$ on variables $x_{1},\dots,x_{n}$. Hence
we get the sequence $\tau\xrightarrow[]{(begin,t_{1})}_{{\tt
ful}}\dots\tau^{\prime}_{i_{1}}\xrightarrow[]{(read,t_{1},t^{\prime}_{1})}_{{\tt
ful}}\tau_{i_{1}}\xrightarrow[]{}_{{\tt
ful}}\dots\tau^{\prime}_{i_{n}}\xrightarrow[]{(read,t_{1},t^{\prime}_{n})}_{{\tt
ful}}\tau_{i_{n}}\dots\xrightarrow[]{(end,t_{1})}_{{\tt ful}}\tau_{1}$. Since
$t_{2}\in\mathcal{T}^{r}$, we know that $t_{2}$ has read events. Let there be
$m$ read events $ev^{\prime}_{1}\dots ev^{\prime}_{m}$ in transaction $t_{2}$,
reading from transactions $t^{\prime\prime}_{1},\dots,t^{\prime\prime}_{m}$ on
variables $y_{1},\dots,y_{m}$. Then we get the sequence
$\tau_{1}\xrightarrow[]{(begin,t_{2})}_{{\tt
ful}}\dots\tau^{\prime}_{j_{1}}\xrightarrow[]{(read,t_{2},t^{\prime\prime}_{1})}_{{\tt
ful}}\tau_{j_{1}}\xrightarrow[]{}_{{\tt
ful}}\dots\tau^{\prime}_{j_{n}}\xrightarrow[]{(read,t_{2},t^{\prime\prime}_{m})}_{{\tt
ful}}\tau_{j_{n}}\dots\xrightarrow[]{(end,t_{2})}_{{\tt ful}}\tau_{2}$.

$\mathbf{Proving}$
$\mathtt{\tau\vdash_{\tt{G}}\alpha_{t_{2}}{\cdot}\alpha_{t_{1}}}$

Since $\tau_{1}=\alpha_{t_{1}}(\tau)$, for all read events $ev_{i}$ such that
$ev_{i}.trans=t_{1}$, we have
$t^{\prime}_{i}\in{\tt{readable}}(\tau,t_{1},x_{i})$. Since
$\tau_{2}=\alpha_{t_{2}}(\tau_{1})$, for all read events $ev^{\prime}_{j}$
such that $ev^{\prime}_{j}.trans=t_{2}$, we have
$t^{\prime\prime}_{j}\in{\tt{readable}}(\tau_{1},t_{2},y_{j})$. Since
$\alpha_{t_{1}}\sim\alpha_{t_{2}}$, it follows that, we have
$t^{\prime\prime}_{j}\in{\tt{readable}}(\tau,t_{2},y_{j})$ for all read events
$ev^{\prime}_{j}$ such that $ev^{\prime}_{j}.trans=t_{2}$. Hence
$\tau\vdash_{\tt{G}}\alpha_{t_{2}}$.

Consider
$\tau_{3}=\alpha_{t_{2}}(\tau)=\langle\mathcal{T}_{3},{\color[rgb]{1,0,0}po}_{3},{\color[rgb]{0,0,1}\it{rf}}_{3},{\color[rgb]{1,.5,0}co}_{3}\rangle$.
To show that $\tau\vdash_{\tt{G}}\alpha_{t_{2}}\alpha_{t_{1}}$, we show that
for all read events $ev_{i}$ such that $ev_{i}.trans=t_{1}$,
$t^{\prime}_{i}\in{\tt{readable}}(\tau_{3},t_{1},x_{i})$. We prove this using
contradiction. Assume that $\exists t^{\prime}_{i}$ s.t.
$t^{\prime}_{i}\notin{\tt{readable}}(\tau_{3},t_{1},x_{i})$.

If $t^{\prime}_{i}\notin{\tt{readable}}(\tau_{3},t_{1},x_{i})$, then there is
a $t^{\prime}_{k}$ such that (i)
$t^{\prime}_{k}\in{\tt{visible}}(\tau_{3},t_{1},x_{i})$ and (ii)
$t^{\prime}_{i}[{\color[rgb]{1,0,0}po}_{3}\cup{\color[rgb]{0,0,1}\it{rf}}_{3}\cup{\color[rgb]{1,.5,0}co}_{3}]^{+}t^{\prime}_{k}$.

If (i) is true, that is,
$t^{\prime}_{k}\in{\tt{visible}}(\tau_{3},t_{1},x_{i})$, since
$\alpha_{t_{1}}\sim\alpha_{t_{2}}$, we also have
$t^{\prime}_{k}\in{\tt{visible}}(\tau,t_{1},x_{i})$. This, combined with
$t^{\prime}_{i}\in{\tt{readable}}(\tau,t_{1},x_{i})$, gives according to the
fulfilled semantics,
$t^{\prime}_{k}[{\color[rgb]{1,.5,0}co}_{1}]t^{\prime}_{i}$. Going back to
(ii), we can have
$t^{\prime}_{i}[{\color[rgb]{1,0,0}po}_{3}\cup{\color[rgb]{0,0,1}\it{rf}}_{3}\cup{\color[rgb]{1,.5,0}co}_{3}]^{+}t^{\prime}_{k}$
only if we observed one of the following:

    * (a)

There is a path from $t^{\prime}_{i}$ to $t^{\prime}_{k}$ in $\tau$; that is,
$t^{\prime}_{i}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]^{+}t^{\prime}_{k}$.
This implies that $t^{\prime}_{i}\notin{\tt{readable}}(\tau,t_{1},x_{i})$
which is a contradiction.

    * (b)

There is no direct path from $t^{\prime}_{i}$ to $t^{\prime}_{k}$, however,
there are transactions $t^{\prime\prime}_{j},t^{\prime\prime}_{l}$ such that,
in $\tau$ we had
$t^{\prime\prime}_{j}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]^{*}t^{\prime}_{k}$
and
$t^{\prime}_{i}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]^{*}t^{\prime\prime}_{l}$,
along with $t^{\prime\prime}_{j}\in{\tt{readable}}(\tau,t_{2},y_{j})$,
$t^{\prime\prime}_{l}\in{\tt{visible}}(\tau,t_{2},y_{j})$. Let
$ev^{\prime}_{j}=r(p_{2},t_{2},y_{j},v)$ be the read event which reads from
$t^{\prime\prime}_{j}$, justifying
$t^{\prime\prime}_{j}\in{\tt{readable}}(\tau,t_{2},y_{j})$.

Since
$t^{\prime\prime}_{j}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]^{*}t^{\prime}_{k}$
and
$t^{\prime}_{i}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]^{*}t^{\prime\prime}_{l}$
it follows that
$t^{\prime\prime}_{j}[{\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}]^{*}t^{\prime}_{k}$,
$t^{\prime}_{i}[{\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}]^{*}t^{\prime\prime}_{l}$.
By our assumption, we have
$t^{\prime}_{i}\in{\tt{readable}}(\tau,t_{1},x_{i})$ and
$t^{\prime}_{k}\in{\tt{visible}}(\tau,t_{1},x_{i})$, which gives us
$t^{\prime}_{k}[{\color[rgb]{1,.5,0}co}_{1}^{x_{i}}]t^{\prime}_{i}$ (already
observed in the para before (i)).

Thus we get
$t^{\prime\prime}_{j}[{\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}]^{*}t^{\prime}_{k}[{\color[rgb]{1,.5,0}co}_{1}^{x_{i}}]t^{\prime}_{i}[{\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}]^{*}t^{\prime\prime}_{l}$,
which gives
$t^{\prime\prime}_{j}[{\color[rgb]{1,0,0}po}_{1}\cup{\color[rgb]{0,0,1}\it{rf}}_{1}\cup{\color[rgb]{1,.5,0}co}_{1}]^{+}t^{\prime\prime}_{l}$.
Hence $t^{\prime\prime}_{j}\notin{\tt{readable}}(\tau_{1},t_{2},y_{j})$, a
contradiction.

Thus, we have
$\neg(t^{\prime}_{i}[{\color[rgb]{1,0,0}po}_{3}\cup{\color[rgb]{0,0,1}\it{rf}}_{3}\cup{\color[rgb]{1,.5,0}co}_{3}]^{+}t^{\prime}_{k})$.
This, for all $1\leq i\leq n$,
$t^{\prime}_{i}\in{\tt{readable}}(\tau_{3},t_{1},x_{i})$. Thus, we now have
$\tau\vdash_{\tt{G}}\alpha_{t_{2}}\alpha_{t_{1}}$. It remains to show that
$(\alpha_{t_{1}}{\cdot}\alpha_{t_{2}})(\tau)\equiv(\alpha_{t_{2}}{\cdot}\alpha_{t_{1}})(\tau)$.

$\mathbf{Proving}$
$\mathtt{(\alpha_{t_{1}}{\cdot}\alpha_{t_{2}})(\tau)\equiv(\alpha_{t_{2}}{\cdot}\alpha_{t_{1}})(\tau)}$

Define
$\tau_{4}{=}\alpha_{t_{1}}(\tau_{3}){=}\alpha_{t_{1}}.\alpha_{t_{2}}(\tau){=}\langle\mathcal{T}_{4},{\color[rgb]{1,0,0}po}_{4},{\color[rgb]{0,0,1}\it{rf}}_{4},{\color[rgb]{1,.5,0}co}_{4}\rangle$.
Recall that $\tau_{2}{=}$$\alpha_{t_{2}}.\alpha_{t_{1}}(\tau)$
=$\langle\mathcal{T}_{2},{\color[rgb]{1,0,0}po}_{2},{\color[rgb]{0,0,1}\it{rf}}_{2},{\color[rgb]{1,.5,0}co}_{2}\rangle$.

To show that
$(\alpha_{t_{1}}\cdot\alpha_{t_{2}})(\tau)\equiv(\alpha_{t_{2}}\cdot\alpha_{t_{1}})(\tau)$,
we show that
$\mathcal{T}_{2}=\mathcal{T}_{4},{\color[rgb]{1,0,0}po}_{2}={\color[rgb]{1,0,0}po}_{4},{\color[rgb]{0,0,1}\it{rf}}_{2}={\color[rgb]{0,0,1}\it{rf}}_{4}$,
and, for any two transactions
$t^{\prime}_{k},t^{\prime}_{i}\in\mathcal{T}_{2}=\mathcal{T}_{4}$,
$t^{\prime}_{k}[{\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}]^{+}t^{\prime}_{i}$
iff
$t^{\prime}_{k}[{\color[rgb]{1,0,0}po}_{4}\cup{\color[rgb]{0,0,1}\it{rf}}_{4}\cup{\color[rgb]{1,.5,0}co}_{4}]^{+}t^{\prime}_{i}$.
Of these, trivially,
$\mathcal{T}_{2}=\mathcal{T}_{4},{\color[rgb]{1,0,0}po}_{2}={\color[rgb]{1,0,0}po}_{4}$
follow. Since $\alpha_{t_{2}}\sim\alpha_{t_{1}}$, we have
${\color[rgb]{0,0,1}\it{rf}}_{2}={\color[rgb]{0,0,1}\it{rf}}_{4}$. It remains
to prove the last condition.

Assume that
$t^{\prime}_{i}[{\color[rgb]{0,0,1}\it{rf}}^{x_{i}}_{1}]t_{1}\wedge
t^{\prime}_{k}\in{\tt{visible}}(\tau_{1},t_{1},x_{i})$, where
$\tau_{1}=\alpha_{t_{1}}(\tau)$. Then we have
$t^{\prime}_{i}[{\color[rgb]{0,0,1}\it{rf}}^{x_{i}}_{1}]t_{1}\wedge
t^{\prime}_{k}\in{\tt{visible}}(\tau,t_{1},x_{i})$, and by the fulfilled
semantics, we have
$t^{\prime}_{k}[{\color[rgb]{1,.5,0}co}_{1}]t^{\prime}_{i}$, and hence
$t^{\prime}_{k}[{\color[rgb]{1,.5,0}co}_{2}]t^{\prime}_{i}$. To obtain
$\tau_{4}$, we execute $t_{2}$ first obtaining $\tau_{3}$ from $\tau$, and
then $t_{1}$. We show that
$t^{\prime}_{k}[{\color[rgb]{1,0,0}po}_{4}\cup{\color[rgb]{0,0,1}\it{rf}}_{4}\cup{\color[rgb]{1,.5,0}co}_{4}]^{+}t^{\prime}_{i}$,
proving
$t^{\prime}_{k}[{\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}]^{+}t^{\prime}_{i}\Rightarrow
t^{\prime}_{k}[{\color[rgb]{1,0,0}po}_{4}\cup{\color[rgb]{0,0,1}\it{rf}}_{4}\cup{\color[rgb]{1,.5,0}co}_{4}]^{+}t^{\prime}_{i}$.

If we have $t^{\prime}_{k}\in{\tt{visible}}(\tau_{3},t_{1},x_{i})$, then we
are done since we have $t^{\prime}_{i}\in{\tt{readable}}(\tau,t_{1},x_{i})$,
hence $t^{\prime}_{i}\in{\tt{readable}}(\tau_{3},t_{1},x_{i})$, thereby
obtaining $t^{\prime}_{k}{\color[rgb]{1,.5,0}co}_{3}t^{\prime}_{i}$, and hence
$t^{\prime}_{k}{\color[rgb]{1,.5,0}co}_{4}t^{\prime}_{i}$.

Assume $t^{\prime}_{k}\notin{\tt{visible}}(\tau_{3},t_{1},x_{i})$. Assume that
on executing $t_{2}$ from $\tau$, we have
$t^{\prime\prime}_{l}\in{\tt{visible}}(\tau,t_{2},y_{j})$, and let
$t^{\prime\prime}_{j}[{\color[rgb]{0,0,1}\it{rf}}^{y_{j}}_{3}]t_{2}$. Then by
the fulfilled semantics,
$t^{\prime\prime}_{l}[{\color[rgb]{1,.5,0}co}_{3}]t^{\prime\prime}_{j}$ is a
new edge which gets added. When we execute $t_{1}$ next, assume
$t^{\prime\prime}_{m}\in{\tt{visible}}(\tau_{3},t_{1},x_{i})$. Since we have
$t^{\prime}_{i}\in{\tt{readable}}(\tau_{3},t_{1},x_{i})$, we obtain
$t^{\prime\prime}_{m}{\color[rgb]{1,.5,0}co}_{4}t^{\prime}_{i}$.

By assumption, $t^{\prime}_{k}\neq t^{\prime\prime}_{m}$. However,
$t^{\prime}_{k}\in{\tt{visible}}(\tau,t_{1},x_{i})$.
$t^{\prime}_{k}\notin{\tt{visible}}(\tau_{3},t_{1},x_{i})$ points to some
transaction that blocked the visibility of $t^{\prime}_{k}$ in $\tau_{3}$, by
happening after $t^{\prime}_{k}$, and which is in
${\tt{visible}}(\tau_{3},t_{1},x_{i})$.

    1. (1)

This blocking transaction could be $t^{\prime\prime}_{m}$. If this is the
case, we have
$t^{\prime}_{k}[{\color[rgb]{1,0,0}po}_{3}\cup{\color[rgb]{0,0,1}\it{rf}}_{3}\cup{\color[rgb]{1,.5,0}co}_{3}]^{+}t^{\prime\prime}_{m}[{\color[rgb]{1,.5,0}co}_{4}]t^{\prime}_{i}$,
and hence
$t^{\prime}_{k}[{\color[rgb]{1,0,0}po}_{4}\cup{\color[rgb]{0,0,1}\it{rf}}_{4}\cup{\color[rgb]{1,.5,0}co}_{4}]^{+}t^{\prime\prime}_{m}[{\color[rgb]{1,.5,0}co}_{4}]t^{\prime}_{i}$.

    2. (2)

The other possibility is that we have $t^{\prime\prime}_{j}$ happens before
$t^{\prime\prime}_{m}$, and $t^{\prime\prime}_{l}$ happens after
$t^{\prime}_{k}$ blocking $t^{\prime}_{k}$ from being in
${\tt{visible}}(\tau_{3},t_{1},x_{i})$. That is,
$t^{\prime}_{k}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}\cup{\color[rgb]{1,.5,0}co}]^{*}t^{\prime\prime}_{l}$
and
$t^{\prime\prime}_{j}[{\color[rgb]{1,0,0}po}_{4}\cup{\color[rgb]{0,0,1}\it{rf}}_{4}\cup{\color[rgb]{1,.5,0}co}_{4}]^{*}t^{\prime\prime}_{m}$.
Then we obtain
$t^{\prime}_{k}[{\color[rgb]{1,0,0}po}_{4}\cup{\color[rgb]{0,0,1}\it{rf}}_{4}\cup{\color[rgb]{1,.5,0}co}_{4}]^{*}t^{\prime\prime}_{l}[{\color[rgb]{1,.5,0}co}^{x_{j}}_{4}]t^{\prime\prime}_{j}[{\color[rgb]{1,0,0}po}_{4}\cup{\color[rgb]{0,0,1}\it{rf}}_{4}\cup{\color[rgb]{1,.5,0}co}_{4}]^{*}t^{\prime\prime}_{m}[{\color[rgb]{1,.5,0}co}_{4}]t^{\prime}_{i}$.

Thus, we obtain
$t^{\prime}_{k}[{\color[rgb]{1,0,0}po}_{4}\cup{\color[rgb]{0,0,1}\it{rf}}_{4}\cup{\color[rgb]{1,.5,0}co}_{4}]^{+}t^{\prime}_{i}$
as desired.

The converse direction, that is, whenever
$t^{\prime}_{k}[{\color[rgb]{1,0,0}po}_{4}\cup{\color[rgb]{0,0,1}\it{rf}}_{4}\cup{\color[rgb]{1,.5,0}co}_{4}]^{+}t^{\prime}_{i}$,
we also have
$t^{\prime}_{k}[{\color[rgb]{1,0,0}po}_{2}\cup{\color[rgb]{0,0,1}\it{rf}}_{2}\cup{\color[rgb]{1,.5,0}co}_{2}]^{+}t^{\prime}_{i}$
is proved on similar lines.

∎

###### Lemma G.7.

If $\tau_{1}\equiv\tau_{2}$, $\alpha_{t_{1}}\sim\alpha_{t_{2}}$, and
$\tau_{1}\vdash_{\tt{G}}(\alpha_{t_{1}}\cdot\alpha_{t_{2}})$, then (i)
$\tau_{2}\vdash_{\tt{G}}(\alpha_{t_{2}}\cdot\alpha_{t_{1}})$ and (ii)
$(\alpha_{t_{1}}\cdot\alpha_{t_{2}})(\tau_{1})\equiv(\alpha_{t_{2}}\cdot\alpha_{t_{1}})(\tau_{2})$.

###### Proof.

Follows from Lemma G.5 and Lemma G.6. ∎

From Lemma G.7, we get following lemma.

###### Lemma G.8.

If $\tau_{1}\equiv\tau_{2}$, $\pi_{\tt{T^{1}}}\sim\pi_{\tt{T^{2}}}$, and
$\tau_{1}\vdash_{\tt{G}}\pi_{\tt{T^{1}}}$ then
$\tau_{2}\vdash_{\tt{G}}\pi_{\tt{T^{2}}}$ and
$\pi_{\tt{T^{1}}}(\tau_{1})\equiv\pi_{\tt{T^{2}}}(\tau_{2})$.

###### Lemma G.9.

If $\langle\sigma,\tau\rangle\vdash_{\tt{G_{T}}}\pi_{\tt{T}}$,
$\langle\sigma,\tau\rangle\vdash_{\tt{G}}\alpha_{t}$ then
$\pi_{\tt{T}}=\pi_{\tt{T^{1}}}\cdot\alpha_{t}\cdot\pi_{\tt{T^{2}}}$ for some
$\pi_{\tt{T^{1}}}$ and $\pi_{\tt{T^{2}}}$ where $\pi_{\tt{T^{1}}}$ is
$t$-free.

Consider observables
$\pi_{\tt{T}}=\alpha_{t_{1}},\alpha_{t_{2}}\dots\alpha_{t_{n}}$. We write
$\pi_{\tt{T}}\lessapprox\pi^{\prime}_{\tt{T}}$ to represent that
$\pi^{\prime}_{\tt{T}}=\pi_{\tt{T^{0}}}\cdot\alpha_{t_{1}}\cdot\pi_{\tt{T^{1}}}\cdot\alpha_{t_{2}}\cdot\pi_{\tt{T^{2}}}\dots\alpha_{t_{n}}\cdot\pi_{\tt{T^{n}}}$.
In other words, $\pi_{\tt{T}}$ occurs as a non-contiguous subsequence in
$\pi^{\prime}_{\tt{T}}$. For such a $\pi_{\tt{T}},\pi^{\prime}_{\tt{T}}$, we
define
$\pi^{\prime}_{\tt{T}}\oslash\pi_{\tt{T}}:=\pi_{\tt{T^{0}}}\cdot\pi_{\tt{T^{1}}}\dots\pi_{\tt{T^{n}}}$.
Since elements of $\pi_{\tt{T}}$ and $\pi^{\prime}_{\tt{T}}$ are distinct,
operation $\oslash$ is well defined. Let $\pi_{\tt{T}}[i]$ denote the $i$th
observable in the observation sequence $\pi_{\tt{T}}$, and let
$|\pi_{\tt{T}}|$ denote the number of observables in $\pi_{\tt{T}}$.

Let $\alpha_{t}=\pi_{\tt{T}}[i]$ for some $i:1\leq i\leq|\pi_{\tt{T}}|$. We
define $\tt{Pre(\pi_{\tt{T}},\alpha_{t})}$ as a subsequence
$\pi^{\prime}_{\tt{T}}$ of $\pi_{\tt{T}}$ such that (i)
$\alpha_{t}\in\pi^{\prime}_{\tt{T}}$, (ii)
$\alpha_{t_{j}}=\pi_{\tt{T}}[j]\in\pi^{\prime}_{\tt{T}}$ for some $j:1\leq
j<i$ iff there exists $k:j<k\leq i$ such that
$\alpha_{t_{k}}=\pi_{\tt{T}}[k]\in\pi^{\prime}_{\tt{T}}$ and
$\neg(\alpha_{t_{j}}\sim\alpha_{t_{k}})$. Thus,
$\tt{Pre(\pi_{\tt{T}},\alpha_{t})}$ consists of $\alpha_{t}$ and all
$\alpha_{t^{\prime}}$ appearing before $\alpha_{t}$ in $\pi_{\tt{T}}$ such
that $t^{\prime}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t$.

###### Lemma G.10.

If $\pi_{\tt{T^{1}}}=\tt{Pre(\pi_{\tt{T}},\alpha_{t})}$ and
$\pi_{\tt{T^{2}}}=\pi_{\tt{T}}\oslash\pi_{\tt{T^{1}}}$ then
$\pi_{\tt{T}}\approx\pi_{\tt{T^{1}}}\cdot\pi_{\tt{T^{2}}}$.

###### Proof.

The proof is trivial since we can always execute in order, the
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}$ predecessors of
$\alpha_{t}$ from $\tt{Pre(\pi_{\tt{T}},\alpha_{t})}$, then $\alpha_{t}$, then
the observables in $\tt{Pre(\pi_{\tt{T}},\alpha_{t})}$ which are independent
from $\alpha_{t}$, followed by the suffix of $\pi_{\tt{T}}$ after
$\alpha_{t}$.

∎

###### Lemma G.11.

If $\pi_{\tt{T}}=\pi^{\prime}_{\tt{T}}\cdot\pi^{\prime\prime}_{T}$ and
$\alpha_{t}\in\pi^{\prime}_{\tt{T}}$ then
$\tt{Pre(\pi_{\tt{T}},\alpha_{t})}=\tt{Pre(\pi^{\prime}_{\tt{T}},\alpha_{t})}$.

###### Proof.

The proof is trivial once again, since all the transactions which are
$[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t$ are in the
prefix $\pi^{\prime}_{\tt{T}}$. ∎

###### Lemma G.12.

If $\langle\sigma,\tau\rangle\vdash_{\tt{G}}\pi_{\tt{T}}$ then
$\langle\sigma,\tau\rangle\vdash_{\tt{G_{T}}}\pi_{\tt{T}}\cdot\pi_{\tt{T^{2}}}$.

###### Proof.

This simply follows from the fact that we can extend the observation sequence
$\pi_{\tt{T}}$ to obtain a terminal configuration, since the DPOR algorithm
generates weak traces corresponding to terminating runs. ∎

###### Lemma G.13.

Consider a fulfilled trace $\tau$ such that $\tau\models{\tt CCv}$,
$\tau\vdash_{\tt{G}}\pi_{\tt{T}}\cdot\alpha_{t}$. Let each read event
$ev_{i}=r_{i}(p,t,x_{i},v)$ in $\alpha_{t}$ read from some transaction
$t_{i}$, and let $\pi_{\tt{T}}$ be $t$-free. Then
$\tau\vdash_{\tt{G}}\alpha^{\prime}_{t}\cdot\pi_{\tt{T}}$, where
$\alpha^{\prime}_{t}$ is the same as $\alpha_{t}$, with the exception that the
sources of its read events can be different. That is, each read event
$ev_{i}=r_{i}(p,t,x_{i},v)\in\alpha^{\prime}_{t}$ can read from some
transaction $t^{\prime}_{i}\neq t_{i}$.

###### Proof.

Let $\pi_{\tt{T}}=\alpha_{t_{1}}\alpha_{t_{2}}\dots\alpha_{t_{n}}$ and
$\tau_{0}\xrightarrow[]{\alpha_{t_{1}}}_{{\tt
ful}}\tau_{1}\xrightarrow[]{\alpha_{t_{2}}}_{{\tt
ful}}\dots\xrightarrow[]{\alpha_{t_{n}}}_{{\tt
ful}}\tau_{n}\xrightarrow[]{\alpha_{t}}_{{\tt ful}}\tau_{n+1}$, where
$\tau_{0}=\tau$. Let
$\tau_{i}=\langle\mathcal{T}_{i},{\color[rgb]{1,0,0}po}_{i},{\color[rgb]{0,0,1}\it{rf}}_{i},{\color[rgb]{1,.5,0}co}_{i}\rangle$.
Let there be $m$ read events in transaction $t$. Keeping in mind what we want
to prove, where we want to execute $t$ first followed by $\pi_{\tt{T}}$, and
obtain an execution $\alpha^{\prime}_{t}\pi_{\tt{T}}$, we do the following.

For each read event $ev_{i}=r_{i}(p,t,x_{i},v)$ we define
$t^{\prime}_{i}\in\mathcal{T}^{w,x_{i}}$ such that $(i)$
$t^{\prime}_{i}\in{\tt{readable}}(\tau_{0},t,x_{i})$, and $(ii)$ there is no
$t^{\prime\prime}_{i}\in{\tt{readable}}(\tau_{0},t,x_{i})$ where
$t^{\prime}_{i}[{\color[rgb]{1,0,0}po}_{n}\cup{\color[rgb]{0,0,1}\it{rf}}_{n}\cup{\color[rgb]{1,.5,0}co}_{n}]t^{\prime\prime}_{i}$.
Note that this is possible since $\pi_{\tt{T}}$ is $t$-free, so all the
observables $\alpha_{t_{i}}$ occurring in $\pi_{\tt{T}}$ are such that $t_{i}$
is issued in a process other than that of $t$. Thus, when $\alpha_{t}$ is
enabled, we can choose any of the writes done earlier, this fact is consistent
with the ${\tt CCv}$ semantics, since from Lemmas C.1-C.4 we know
$\tau_{n}\models{\tt CCv}$. Since $\tau_{n}\models{\tt CCv}$ such a
$t^{\prime}_{i}\in{\tt{readable}}(\tau_{0},t,x_{i})$ exists for each $ev_{i}$.

Next we define a sequence of traces which can give the execution
$\alpha^{\prime}_{t}\pi_{\tt{T}}$. Define a sequence of traces
$\tau^{\prime}_{0},\tau^{\prime}_{1},\dots\tau^{\prime}_{n}$ where
$\tau^{\prime}_{j}=\langle\mathcal{T}^{\prime}_{j},{\color[rgb]{1,0,0}po}^{\prime}_{j},{\color[rgb]{0,0,1}\it{rf}}^{\prime}_{j},{\color[rgb]{1,.5,0}co}^{\prime}_{j}\rangle$
is such that

  1. (1)

$\tau\vdash_{\tt{G}}{\alpha^{\prime}_{t}}$ and
$\alpha^{\prime}_{t}(\tau)=\tau^{\prime}_{0}$,

  2. (2)

$\tau^{\prime}_{j}\vdash_{\tt{G}}\alpha_{t_{j+1}}$ and
$\tau^{\prime}_{j+1}=\alpha_{t_{j+1}}(\tau^{\prime}_{j})$ for all $j:0\leq
j\leq n$.

  * •

Define $\mathcal{T}^{\prime}_{i}=\mathcal{T}_{i}\cup\\{t\\}$ for all $0\leq
i\leq n$,

  * •

Define
${\color[rgb]{1,0,0}po}^{\prime}=\\{t^{\prime}[{\color[rgb]{1,0,0}po}]t\mid
t^{\prime}$ is a transaction in $\tau$, in the same process as $t\\}$, and
${\color[rgb]{1,0,0}po}^{\prime}_{i}={\color[rgb]{1,0,0}po}_{i}\cup{\color[rgb]{1,0,0}po}^{\prime}$
for all $0\leq i\leq n$,

  * •

${\color[rgb]{0,0,1}\it{rf}}^{\prime}=\bigcup_{i:1\leq i\leq
m}t^{\prime}_{i}[{\color[rgb]{0,0,1}\it{rf}}^{x_{i}}]t$ (reads from relation
corresponding to each read event $ev_{i}\in\alpha^{\prime}_{t}$), and
${\color[rgb]{0,0,1}\it{rf}}^{\prime}_{i}={\color[rgb]{0,0,1}\it{rf}}_{i}\cup{\color[rgb]{0,0,1}\it{rf}}^{\prime}$
for all $i:1\leq i\leq n$,

  * •

${\color[rgb]{1,.5,0}co}^{\prime}=\bigcup_{j:1\leq j\leq
m}{\color[rgb]{1,.5,0}co}^{\prime}_{j}$ (each
${\color[rgb]{1,.5,0}co}^{\prime}_{j}$ corresponds to the updated
${\color[rgb]{1,.5,0}co}$ relation because of the read transition
$\xrightarrow[]{(read,t,t^{\prime}_{j})}_{{\tt ful}}$).

For $1\leq i\leq n$, we define ${\color[rgb]{1,.5,0}co}^{\prime}_{i}$
inductively as
${\color[rgb]{1,.5,0}co}^{\prime}_{i}={\color[rgb]{1,.5,0}co}_{i}\cup{\color[rgb]{1,.5,0}co}^{\prime}$
and show that $\tau^{\prime}_{i}\vdash_{\tt{G}}\alpha_{t_{i+1}}$ and
$\tau^{\prime}_{i+1}=\alpha_{t_{i+1}}(\tau^{\prime}_{i})$ holds good. First
define
${\color[rgb]{1,.5,0}co}^{\prime}_{0}={\color[rgb]{1,.5,0}co}_{0}\cup{\color[rgb]{1,.5,0}co}^{\prime}$.
Then define ${\color[rgb]{1,.5,0}co}^{\prime}_{i}$ to be the coherence order
corresponding to $\alpha_{t_{i}}(\tau^{\prime}_{i-1})$ where
$\tau^{\prime}_{i-1}=\langle\mathcal{T}^{\prime}_{{i-1}},{\color[rgb]{1,0,0}po}_{i-1},{\color[rgb]{0,0,1}\it{rf}}_{i-1},{\color[rgb]{1,.5,0}co}_{i-1}\rangle$
for all $i:1\leq i\leq n$.

Base case. The base case $\tau\vdash_{\tt{G}}{\alpha^{\prime}_{t}}$ and
$\alpha^{\prime}_{t}(\tau)=\tau^{\prime}_{0}$, holds trivially, by
construction.

Inductive hypothesis. Assume that
$\tau^{\prime}_{j}\vdash_{\tt{G}}\alpha_{t_{j+1}}$ and
$\tau^{\prime}_{j+1}=\alpha_{t_{j+1}}(\tau^{\prime}_{j})$ for $0\leq j\leq
i-1$.

We have to prove that $\tau^{\prime}_{i}\vdash_{\tt{G}}\alpha_{t_{i+1}}$ and
$\tau^{\prime}_{i+1}=\alpha_{t_{i+1}}(\tau^{\prime}_{i})$.

  1. (1)

If $t_{i+1}\in\mathcal{T}^{w}$ and $t_{i+1}\notin\mathcal{T}^{r}$, then the
proof holds trivially from the inductive hypothesis.

  2. (2)

Consider now $t_{i+1}\in\mathcal{T}^{r}$. Consider a read event
$ev^{i+1}=r(p,t_{i+1},x,v)\in\alpha_{t_{i+1}}$ which was reading from
transaction $t_{x}$ in $\pi_{\tt{T}}$. That is, we had
$t_{x}\in{\tt{readable}}(\tau_{i},t_{i+1},x)$. If
$t_{x}\in{\tt{readable}}(\tau^{\prime}_{i},t_{i+1},x)$, then we are done,
since we can simply extend the run from the inductive hypothesis.

Assume otherwise. That is,
$t_{x}\notin{\tt{readable}}(\tau^{\prime}_{i},t_{i+1},x)$.

Since $t_{x}$ $\in$ ${\tt{readable}}(\tau_{i},t_{i+1},x)$, we know that there
are some blocking transactions in the new path which prevents $t_{x}$ from
being readable. Basically, we have the blocking transactions since $t$ is
moved before $\pi_{\tt{T}}$.

     * •

Consider $tr_{1}\in{\tt{visible}}(\tau,t,y)$ for some variable $y$ such that,
in $\pi_{\tt{T}}.\alpha_{t}$, we had
$t_{x}[{\color[rgb]{1,0,0}po}_{i}\cup{\color[rgb]{0,0,1}\it{rf}}_{i}\cup{\color[rgb]{1,.5,0}co}_{i}]^{*}tr_{1}$.
This path is possible since $\alpha_{t}$ comes last in in
$\pi_{\tt{T}}.\alpha_{t}$, after $\alpha_{t_{i+1}}$.

     * •

Consider $tr_{2}\in{\tt{visible}}(\tau_{i},t_{i+1},x)$. Since $t_{x}$ $\in$
${\tt{readable}}(\tau_{i},t_{i+1},x)$, we have
$tr_{2}[{\color[rgb]{1,.5,0}co}^{x}_{i+1}]t_{x}$. Now, in
$\alpha^{\prime}_{t}.\pi_{\tt{T}}$, assume
$tr_{3}[{\color[rgb]{0,0,1}\it{rf}}^{\prime y}_{0}]t$, such that we have a
path from $tr_{3}$ to $t_{x}$, as
$tr_{3}[{\color[rgb]{1,0,0}po}_{i}\cup{\color[rgb]{0,0,1}\it{rf}}_{i}\cup{\color[rgb]{1,.5,0}co}_{i}]^{*}tr_{2}$.

Hence it follows that
$tr_{3}[{\color[rgb]{1,0,0}po}_{i}\cup{\color[rgb]{0,0,1}\it{rf}}_{i}\cup{\color[rgb]{1,.5,0}co}_{i}]^{*}tr_{2}$
$[{\color[rgb]{1,.5,0}co}^{x}_{i+1}]t_{x}$
$[{\color[rgb]{1,0,0}po}_{i}\cup{\color[rgb]{0,0,1}\it{rf}}_{i}\cup{\color[rgb]{1,.5,0}co}_{i}]^{*}tr_{1}$.
Hence we have
$tr_{3}[{\color[rgb]{1,0,0}po}_{i+1}\cup{\color[rgb]{0,0,1}\it{rf}}_{i+1}\cup{\color[rgb]{1,.5,0}co}_{i+1}]^{+}tr_{1}$,
i.e
$tr_{3}[{\color[rgb]{1,0,0}po}_{n}\cup{\color[rgb]{0,0,1}\it{rf}}_{n}\cup{\color[rgb]{1,.5,0}co}_{n}]^{+}tr_{1}$.
This leads to the contradiction since $tr_{1}\in{\tt{visible}}(\tau,t,y)$ and
$tr_{3}[{\color[rgb]{0,0,1}\it{rf}}^{\prime y}_{0}]t$.

Hence, $t_{x}$ $\in$ ${\tt{readable}}(\tau_{i},t_{i+1},x)$ and we can extend
the run from the inductive hypothesis obtaining
$\tau^{\prime}_{j}\vdash_{\tt{G}}\alpha_{t_{j+1}}$,
$\tau^{\prime}_{j+1}=\alpha_{t_{j+1}}(\tau^{\prime}_{j})$, for $0\leq j\leq
i-1$, and $\tau^{\prime}_{i}\vdash_{\tt{G}}\alpha_{t_{i+1}}$.

Now we prove that
${\color[rgb]{1,.5,0}co}^{\prime}_{i+1}={\color[rgb]{1,.5,0}co}_{i+1}\cup{\color[rgb]{1,.5,0}co}^{\prime}$.
Assume we have $(tr1,tr2)\in{\color[rgb]{1,.5,0}co}_{i+1}$. We show that
$(tr1,tr2)\in{\color[rgb]{1,.5,0}co}^{\prime}_{i+1}$. We have the following
cases:

  * (i)

$(tr1,tr2)\in{\color[rgb]{1,.5,0}co}_{i}$. From the inductive hypothesis it
follows that $(tr1,tr2)\in{\color[rgb]{1,.5,0}co}^{\prime}_{i}$ and hence in
${\color[rgb]{1,.5,0}co}^{\prime}_{i+1}$.

  * (ii)

$(tr1,tr2)\notin{\color[rgb]{1,.5,0}co}_{i}$ and some read event
$ev=r(p,t_{i+1},x,v)$ from $\alpha_{t_{i+1}}$ reads from $tr2$. That is,
$tr1,tr2\in{\tt{readable}}(\tau_{i},t_{i+1},x)$ and
$tr1\in{\tt{visible}}(\tau_{i},t_{i+1},x)$. Assume
$(tr1,tr2)\notin{\color[rgb]{1,.5,0}co}^{\prime}_{i+1}$. Since
$(tr1,tr2)\notin{\color[rgb]{1,.5,0}co}^{\prime}_{i+1}$, it follows that there
exists $tr3\in{\tt{visible}}(\tau^{\prime}_{i},t_{i+1},x)$ such that
$tr2[{\color[rgb]{1,0,0}po}^{\prime}_{i}\cup{\color[rgb]{0,0,1}\it{rf}}^{\prime}_{i}\cup{\color[rgb]{1,.5,0}co}^{\prime}_{i}]tr3$.
This means $tr2\in{\tt{readable}}(\tau_{i},t_{i+1},x)$, but
$tr2\notin{\tt{readable}}(\tau^{\prime}_{i},t_{i+1},x)$. However, as proved
earlier, this leads to a contradiction.

Thus, we have shown that
$\tau\vdash_{\tt{G}}\alpha^{\prime}_{t}\alpha_{t_{1}}\dots\alpha_{t_{i}}$ is
such that
$\alpha^{\prime}_{t}\alpha_{t_{1}}\dots\alpha_{t_{i}}(\tau)=\tau^{\prime}_{i}$
for all $0\leq i\leq n$. When $i=n$ we obtain
$\alpha^{\prime}_{t}\pi_{\tt{T}}(\tau)=\tau^{\prime}_{n}$, or
$\tau\vdash_{\tt{G}}\alpha^{\prime}_{t}\pi_{\tt{T}}$. ∎

###### Definition G.14 (Linearization of a Trace).

A observation sequence $\pi_{\tt{T}}$ is a _linearization_ of a trace
$\tau=\langle\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}\it{rf}},{\color[rgb]{1,.5,0}co}\rangle$
if $(i)$ $\pi_{\tt{T}}$ has the same transactions as $\tau$ and $(ii)$
$\pi_{\tt{T}}$ follows the
(${\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}})$ relation.

We say that our DPOR algorithm _generates an observation sequence_
$\pi_{\tt{T}}$ from state $\langle\sigma,\tau\rangle$ where $\sigma$ is a
configuration and $\tau$ is a trace if it invokes $ExploreTraces$ with
parameters $\sigma,\tau,\pi^{\prime}$, where $\pi^{\prime}$ is a
_linearization_ of $\tau$, and generates a sequence of recursive calls to
$ExploreTraces$ resulting in $\pi_{\tt{T}}$.

###### Lemma G.15.

If $\langle\sigma,\tau\rangle\vdash_{\tt{G_{T}}}\pi_{\tt{T}}$ then, the DPOR
algorithm generates $\pi^{\prime}_{\tt{T}}$ from state
$\langle\sigma,\tau\rangle$ for some
$\pi^{\prime}_{\tt{T}}\approx\pi_{\tt{T}}$.

###### Proof.

We use induction on $|\pi_{\tt{T}}|$. If $\sigma$ is $terminal$, then the
proof is trivial. Assume that we have
$\langle\sigma,\tau\rangle\vdash_{\tt{G_{T}}}\pi_{\tt{T}}$. Assume that
$\langle\sigma,\tau\rangle\vdash_{\tt{G}}\alpha_{t}$. It follows that
$\langle\sigma,\tau\rangle\vdash_{\tt{G}}\alpha_{t}$. Using Lemma G.9 we get
$\pi_{\tt{T}}=\pi_{\tt{T^{1}}}\cdot\alpha_{t}\cdot\pi_{\tt{T^{2}}}$, where
$\pi_{\tt{T^{1}}}$ is $t$-free. We consider the following two cases:

  * •

In the first case, we assume that all read events in $t$ read from
transactions in $\tau$. So in this case, $\pi_{\tt{T^{1}}}$ can be empty.
Assume there are $n$ read events in $t$ and each read event
$ev_{i}=r(p,t,x_{i},v)$ reads from transactions $t_{i}\in\tau$ for all
$i:1\leq i\leq n$. In this case the DPOR algorithm will let each read event
$ev_{i}$ read from all possible transactions
$t^{\prime}\in{\tt{readable}}(\tau,t,x_{i})$, including $t_{i}$.

  * •

In the second case, assume that there exists at least one read event
$ev^{\prime}=r(p,t,x,v)\in\alpha_{t}$ which reads from a transaction
$t^{\prime}\in\pi_{\tt{T^{1}}}$ (hence, $\pi_{\tt{T^{1}}}$ is non empty).

From Lemma G.13, we know that
$\langle\sigma,\tau\rangle\vdash_{\tt{G}}\alpha^{\prime}_{t}\cdot\pi_{\tt{T^{1}}}$.
From Lemma G.12, it follows that
$\langle\sigma,\tau\rangle\vdash_{\tt{G_{T}}}\alpha^{\prime}_{t}\cdot\pi_{\tt{T^{1}}}\cdot\pi_{\tt{T^{4}}}$,
for some $\pi_{\tt{T^{4}}}$. Hence there exists
$\langle\sigma^{\prime},\tau^{\prime}\rangle$ such that
$\langle\sigma^{\prime},\tau^{\prime}\rangle=\alpha^{\prime}_{t}(\langle\sigma,\tau\rangle)$
and
$\langle\sigma^{\prime},\tau^{\prime}\rangle\vdash_{\tt{G_{T}}}\pi_{\tt{T^{1}}}\cdot\pi_{\tt{T^{4}}}$.

Since $|\pi_{\tt{T^{1}}}\cdot\pi_{\tt{T^{4}}}|<|\pi_{\tt{T}}$, we can use the
inductive hypothesis. It follows that the DPOR algorithm generates from state
$\langle\sigma^{\prime},\tau^{\prime}\rangle$, the observation sequence
$\pi_{\tt{T^{5}}}$ such that
$\pi_{\tt{T^{5}}}\approx\pi_{\tt{T^{1}}}\cdot\pi_{\tt{T^{4}}}$.

Let $\pi_{\tt{T^{3}}}.\alpha_{t}=\tt{Pre(\pi_{\tt{T^{1}}},\alpha_{t})}$. Then
$\pi_{\tt{T^{5}}}\approx\pi_{\tt{T^{1}}}\cdot\pi_{\tt{T^{4}}}$ implies that
$\pi_{\tt{T^{3}}}\lessapprox\pi_{\tt{T^{5}}}$ (by applying Lemma G.11). Let
$\pi_{\tt{T^{6}}}\approx\pi_{\tt{T}}\oslash(\pi_{\tt{T^{3}}}\cdot\alpha_{t})$.
By applying Lemma G.10, we get
$\pi_{\tt{T}}\approx\pi_{\tt{T^{3}}}\cdot\alpha_{t}\cdot\pi_{\tt{T^{6}}}$.
Since $\langle\sigma,\tau\rangle\vdash_{\tt{G_{T}}}\pi_{\tt{T}}$ and
$\pi_{\tt{T}}\approx\pi_{\tt{T^{3}}}\cdot\alpha_{t}\cdot\pi_{\tt{T^{6}}}$, by
applying Lemma G.7, we get
$\langle\sigma,\tau\rangle\vdash_{\tt{G_{T}}}\pi_{\tt{T^{3}}}\cdot\alpha_{t}\cdot\pi_{\tt{T^{6}}}$.
Let
$\langle\sigma^{\prime},\tau^{\prime}\rangle=(\pi_{\tt{T^{3}}}\cdot\alpha_{t})(\langle\sigma,\tau\rangle)$.
Since
$\langle\sigma,\tau\rangle\vdash_{\tt{G_{T}}}\pi_{\tt{T^{3}}}\cdot\alpha_{t}\cdot\pi_{\tt{T^{6}}}$,
we have
$\langle\sigma^{\prime},\tau^{\prime}\rangle\vdash_{\tt{G_{T}}}\pi_{\tt{T^{6}}}$.
From inductive hypothesis it follows that
$\langle\sigma^{\prime},\tau^{\prime}\rangle$ generates $\pi_{\tt{T^{7}}}$
such that $\pi_{\tt{T^{7}}}\approx\pi_{\tt{T^{6}}}$.
In other words, $\langle\sigma,\tau\rangle$ generates
$\pi_{\tt{T^{3}}}\cdot\alpha_{t}\cdot\pi_{\tt{T^{7}}}$ where
$\pi_{\tt{T}}\approx\pi_{\tt{T^{3}}}\cdot\alpha_{t}\cdot\pi_{\tt{T^{7}}}$.

∎

Weak Causal Consistency ${\tt CC}$

##  Appendix H ${\tt CC}$ Semantics

The transition rules in the labeled transition system (LTS) for ${\tt CC}$ is
given in Figure 15.

$\begin{array}[]{c}\scriptsize\dfrac{\text{$\text{$\mathtt{begin}$}\in{\mathsf{inst}}(\mathsf{ls}({p}).\mathsf{pc})$
\quad$\mathsf{ls}(p).\mathsf{ts}<t$
\quad$s=\mathsf{ls}({p})[\mathsf{log}\mapsto\epsilon,\text{$\mathtt{snapshot}$}\mapsto\text{$\mathtt{buildSnapshot(store)}$},\mathsf{pc}\mapsto\mathsf{next}(\mathsf{pc})]$}}{\text{$(\mathsf{ls},\mathsf{msgs})\xrightarrow{\text{\tiny$\mathsf{begin}({p},{t})$}}(\mathsf{ls}[{p}\mapsto
s],\mathsf{msgs})$}}\\\\[16.00003pt]
\scriptsize\par\dfrac{\text{$r:=x\in{\mathsf{inst}}(\mathsf{ls}({p}).\mathsf{pc})$\quad$\mathit{cceval}(\mathsf{ls}({p}),x)=(v,t^{\prime})$
\quad$\mathit{rval}=\mathsf{ls}({p}).\mathsf{rval}[r\mapsto
v]$\quad$s=\mathsf{ls}({p})[\mathsf{rval}\mapsto\mathit{rval},\mathsf{pc}\mapsto\mathsf{next}(\mathsf{pc})]$}}{\text{$(\mathsf{ls},\mathsf{msgs})\xrightarrow{\text{\tiny$r({p},{t},x,v)$}}(\mathsf{ls}[{p}\mapsto
s],\mathsf{msgs})$}}\\\\[22.76219pt]
\scriptsize\par\dfrac{\text{$x:=v\in{\mathsf{inst}}(\mathsf{ls}({p}).\mathsf{pc})$\quad$\mathit{log}=(\mathsf{ls}({p}).\mathsf{log})\cdot(x,v)$\quad$s=\mathsf{ls}({p})[\mathsf{log}\mapsto\mathit{log},\mathsf{pc}\mapsto\mathsf{next}(\mathsf{pc})]$}}{\text{$(\mathsf{ls},\mathsf{msgs})\xrightarrow{\text{\tiny$\mathsf{isu}({p},{t},x,v)$}}(\mathsf{ls}[{p}\mapsto
s],\mathsf{msgs})$}}\\\\[16.00003pt]
\scriptsize\par\dfrac{\text{$\text{$\mathtt{end}$}\in{\mathsf{inst}}(\mathsf{ls}({p}).\mathsf{pc})$\quad$s=\mathsf{ls}({p})[\text{$\mathtt{snapshot}$}\mapsto\epsilon,\mathsf{pc}\mapsto\mathsf{next}(\mathsf{pc})]$}}{\text{$(\mathsf{ls},\mathsf{msgs})\xrightarrow{\text{\tiny$\mathsf{end}({p},{t})$}}(\mathsf{ls}[{p}\mapsto
s],\mathsf{msgs}\cup\\{({t},\mathsf{ls}(p).\mathsf{log})\\})$}}\\\\[22.76219pt]
\scriptsize\dfrac{\text{$\langle
t,\mathit{log}\rangle\in\mathsf{msgs}$\quad$\mathit{store}=\mathsf{ls}({p}).\mathsf{store}[x\mapsto\mathit{update}(\mathsf{ls}({p}),x,t,\mathit{last}(\mathit{log},x)):x\in\mathcal{V}]$
\quad$s=\mathsf{ls}({p})[\mathsf{store}\mapsto\mathit{store},\mathsf{pc}\mapsto\mathsf{next}(\mathsf{pc})]$
}}{\text{$(\mathsf{ls},\mathsf{msgs})\xrightarrow{\text{\tiny$\mathsf{del}({p},{t})$}}(\mathsf{ls}[{p}\mapsto
s],\mathsf{msgs})$}}\end{array}$ Figure 15. The set of transition rules
defining the weak causal semantics. The function
$\mathtt{buildSnapshot(store)}$ returns a consistent snapshot of the store.
Function $\mathit{cceval(\mathsf{ls}({p}),x)}$ returns the pair
($\mathit{last}(\mathit{log},x)$) if $\mathit{last}(\mathit{log},x)\neq\bot$,
otherwise returns the pair $(v,t^{\prime})$ in
$\mathsf{ls}({p})$.$\mathtt{snapshot}$$(x)$.

The set of executions of $\mathcal{P}$ under weak causal consistency, denoted
$\mathsf{Exec}_{{\tt CC}}(\mathcal{P})$ are those executions satisfying
transaction isolation and causal delivery. Figure 16(a) gives a sample program
and its execution under ${\tt CC}$. In this program, transactions $t1$ and
$t3$ are concurrent. Hence, $t5$ can read from $t1$ while $t4$ reads from
$t3$. We denote all executions starting from configuration $\sigma$ by ${\tt
ExecFrom}(\sigma)$.

(a) ${\tt CC}$ Program

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

(b) ${\tt CC}$ Execution Summary

(c) ${\tt CC}$ Consistent Trace

Figure 16. ${\tt CC}$ Execution and corresponding summary, trace

##  Appendix I ${\tt CC}$ Axiomatic Semantics

As done for ${\tt CCv}$ in the main paper, we present the notions of execution
summaries and traces first.

###  I.1. ${\tt CC}$ Execution Summaries, Traces

The notion of an execution summary is same for ${\tt CC}$ as it was for ${\tt
CCv}$. Given a ${\tt CC}$ 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)$. Thus, 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$. Fig.16(b) gives the execution summary for
the ${\tt CC}$ execution given in Fig.16(a)).

The execution summary $(\mathsf{EvSum}(\rho),<)$ induces two functions : the
_happens-before_ (as in ${\tt CCv}$), and _read from the concurrent writes_
relations (new in ${\tt CC}$) as follows.

$\bullet
S.hb:\mathcal{T}(\rho)^{r}\rightarrow\mathfrak{p}(\mathcal{T}(\rho)^{w})$
defined by
$S.hb(t_{1})=\\{t^{\prime}\in\mathcal{T}(\rho)^{w}\mid\mathsf{del}(p,t^{\prime})<\mathsf{isu}(p,t_{1})$
for any $p\in\mathbf{P}\\}$.

$\bullet
S.cw:\mathcal{T}(\rho)^{r}\times\mathcal{V}\rightarrow\mathfrak{p}(\mathcal{T}(\rho)^{w})$,
defined by $S.cw(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\lor(t^{\prime}$ and $t^{\prime\prime}$ are
_concurrent_)$\\}$. That is, $S.cw(t_{1},x)$ is the set of _concurrent_
transactions from which $t_{1}$ can read from.

##### Legal Summaries

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

  * 1.

Each transaction $t$ in the domain of $S.cw$ reads from a transaction
$t^{\prime}\in S.cw(t,x)$ for all $x$. Each read is from the one of the
eligible _concurrent_ writes.

  * 2.

For every transaction $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}$.

  * 3.

For every transaction $t$ and processes $p,p^{\prime}$,
$\mathsf{isu}(p,t)<\mathsf{del}(p^{\prime},t)$.

Note that only the first condition of legality differs from that of ${\tt
CCv}$.

##### Traces

Unlike ${\tt CCv}$, for ${\tt CC}$, traces are built using only
${\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}\it{rf}}$ relations. Thus, a trace
is given by
$\tau=(\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}\it{rf}})$. This
is due to the fact that ${\tt CC}$ maintains writes from concurrent
transactions to be read from. Recall that each time we begin a new transaction
$t$ in a process $p$, the local store of $p$ is updated so that, for each
variable $x$, $(v_{1},t_{1}),(v_{2},t_{2})\in\mathsf{ls}(p).\mathsf{store}(x)$
iff $t_{1},t_{2}\in\mathcal{T}^{w,x}$ are concurrent, and have happened before
$t$. Thus, ${\tt CC}$ does not impose a ${\color[rgb]{1,.5,0}co}$ between such
$t_{1},t_{2}$, and dynamically chooses to read from any one such, at the onset
of each fresh transaction $t$.

###### Definition I.1.

(Total and Partial Traces) We say a trace is total if
$\tau=(\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}\it{rf}})$ and
all external reads are covered by the ${\color[rgb]{0,0,1}\it{rf}}$ relation.
It is partial otherwise.

###### Definition I.2.

(Concurrent Transactions) Two transactions $t$ and $t^{\prime}$ are
$concurrent$ if
$\neg(t[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t^{\prime})$
and
$\neg(t^{\prime}[{\color[rgb]{1,0,0}po}\cup{\color[rgb]{0,0,1}\it{rf}}]^{+}t)$.

###### Definition I.3 ($\tau$-consistent 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}\it{rf}})$, we
say that $\rho$ is $\tau$-consistent denoted by $\rho\models\tau$ if the
following holds:

  * $\star$

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

  * $\star$

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

  * $\star$

For $t\neq t^{\prime}\in\mathcal{T}$, if $t$ [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
$t\in\mathcal{T}^{w,x}$, $t^{\prime}\in\mathcal{T}^{r,x}$ for some
$x\in\mathcal{V}$ and
$\forall\ell_{m}=\mathsf{del}(p,t^{\prime\prime}).((j<m<k\wedge
t^{\prime\prime}\in\mathcal{T}^{w,x})\implies$ ($t$ and $t^{\prime\prime}$ are
concurrent)).

  * $\star$

If $init_{x}$ [rf] $t$, then $t$ has the read instruction $r:=x$, which reads
from $init_{x}$ and the value read into $r$ is 0.

###### Definition I.4 (Partially Good Traces, ${\tt CC}$ consistent Traces).

For a trace
$\tau=(\mathcal{T},{\color[rgb]{1,0,0}po},{\color[rgb]{0,0,1}\it{rf}})$,