
\(X \subseteq T\cup Q\cup A\) 
is a set of committed transactions and cl_uniform_barrier and attach events;

\(\textsl {client}: X \rightarrow \mathbb {C}\)  is a function that returns

the client \(\textsl {client}(t)\)  which issues the transaction
\(\mathit {t}\in (X \cap T)\) ,

the client \(\textsl {client}(q)\)  which issues the cl_uniform_barrier event
\(q\in (X \cap Q)\) , or

the client \(\textsl {client}(a)\)  which issues the attach event
\(a\in (X \cap A)\) ;


\(\textsl {dc}: X \rightarrow  is a functionthat returns the original data center \)dc(t)\(of transaction \) t(X T)\(,\)dc(q)\( of \textsc {cl\_uniform\_barrier}{} event \) q(X Q)\(,or \)dc(a)\( of \textsc {attach}{} event \) a(X A)\(;\item \)soX X\( is the \emph {session order} on \) X\(.Consider \) s1, s2 X\(.We say that \) s1\( precedes \) s2\(in the session order, denoted \) s1 so s2\(,if they are executed by the same clientand \) s1\( is executed before \) s2\(.\)
In the following, we denote components of \(H\)  as in \(H.X\) 
and often shorten \(H.X\)  by \(X\)  when it is clear.
Let \(V_{H} \triangleq \bigcup (H.X \cap T).Y\) 
be the set of transactional events in history \(H\) .
A consistency model is specified by a set of histories.
To define this set, we extend histories with two relations,
declaratively describing how the system processes transactions
and cl_uniform_barrier events.
Definition 3 (Abstract Executions)  
An abstract execution is a triple
\(A = ((X, \textsl {client}, \textsl {dc}, \textsl {so}), \textsl {vis}, \textsl {ar})\) 
such that

\((X, \textsl {client}, \textsl {dc}, \textsl {so})\)  is a history;

Visibility \(\textsl {vis}\subseteq X \times X\)  is a partial order;

Arbitration \(\textsl {ar}\subseteq X \times X\)  is a total order.


For \(H = (X, \textsl {client}, \textsl {dc}, \textsl {so})\) ,
we often shorten \(((X, \textsl {client}, \textsl {dc}, \textsl {so}), \textsl {vis}, \textsl {ar})\)  by \((H, \textsl {vis}, \textsl {ar})\) .
subsection2-.75.3Partial Order-Restrictions Consistency
We aim to show that UniStore implements a transactional variant
of Partial Order-Restrictions consistency
(PoR consistency) [1]}, [2]} for LWW registers.
A history \(H\)  of UniStore satisfies PoR, denoted \(H \models \textsc {PoR}\) ,
if it can be extended to an abstract execution that satisfies several axioms,
defined in the following:
\(H \models \textsc {PoR}\Leftrightarrow \; &\exists \textsl {vis}, \textsl {ar}.\; (H, \textsl {vis}, \textsl {ar}) \models \\&\qquad \textsc {RVal}\;\wedge \\&\qquad \textsc {CausalConsistency}\;\wedge \\&\qquad \textsc {ConflictOrdering}\;\wedge \\&\qquad \textsc {EventualVisibility}.\) 

\(\textsc {UniStore}\)  satisfies \(\textsc {PoR}\) , denoted \(\textsc {UniStore}\models \textsc {PoR}\) ,
if all its histories do.
Given an abstract execution \(A = (H, \textsl {vis}, \textsl {ar})\) ,
the axioms are defined as follows.
Definition 4 (\(\textsc {RVal}\) , [3]})  
The Return Value Consistency (RVal) specifies
the return value of each read event.
\(\textsc {RVal}\triangleq \textsc {IntRVal}\wedge \textsc {ExtRVal}.\) 
Here \(\textsc {IntRVal}\)  requires an internal read event \(e\) 
on key \(k\)  to read from the last update event on \(k\)  preceding \(e\) 
in the same transaction. Formally,
\(&\textsc {IntRVal}\triangleq \forall e \in R_{\textsc {int}}\cap R_{k} \cap V_{H}. \\&\quad \textsl {rval}(e) = \textsl {uval}\big (\max _{\textsl {po}}(\textsl {po}^{-1}(e) \cap U_{k})\big ).\) 

\(\textsc {ExtRVal}\)  requires an external read event \(e\) 
on key \(k\)  to read from the last update event on \(k\) 
in the last transaction preceding \(\textsl {tx}(e)\)  in \(\textsl {ar}\) ,
among the set of transactions visible to \(\textsl {tx}(e)\) .
Formally,
\(&\textsc {ExtRVal}\triangleq \forall e \in R_{\textsc {ext}}\cap R_{k} \cap V_{H}. \\&\quad \textsl {rval}(e) =\textsl {uval}\Big (\textsl {ud}\big (\max _{\textsl {ar}}\big (\textsl {vis}^{-1}(\textsl {tx}(e)) \cap T_{k}\big ), k\big )\Big ).\) 

Definition 5 (CausalConsistency, [4]})
\(\textsc {CausalConsistency}\triangleq \; &\textsc {CausalVisibility}\;\wedge \\&\textsc {CausalArbitration},\) 

where
\(\textsc {CausalVisibility}\triangleq (\textsl {so}\; \cup \textsl {vis})^{+} \subseteq \textsl {vis};\) 
\(\textsc {CausalArbitration}\triangleq \textsl {vis}\subseteq \textsl {ar}.\) 

The Conflict Ordering property requires that
out of any two conflicting strong transactions,
one must be visible to the other.
Formally,
Definition 6 (Conflict Relation)  
The conflict relation, denoted by \(\bowtie \) , between strong transactions
is a symmetric relation defined as follows:
\(&\forall \mathit {t}, \mathit {t}^{\prime } \in T_{\textsl {strong}}.\; \mathit {t}\bowtie \mathit {t}^{\prime } \Leftrightarrow \\&\quad (R(\mathit {t}) \cap W(\mathit {t}^{\prime }) \ne \varnothing ) \vee (W(\mathit {t}) \cap R(\mathit {t}^{\prime }) \ne \varnothing ).\) 

Definition 7 (ConflictOrdering)
\(&\textsc {ConflictOrdering}\triangleq \forall \mathit {t}_{1}, \mathit {t}_{2} \in X \cap T_{\textsl {strong}}.\; \\&\quad \mathit {t}_{1} \bowtie \mathit {t}_{2} \Rightarrow  \mathit {t}_{1} \xrightarrow{} \mathit {t}_{2} \vee \mathit {t}_{2} \xrightarrow{} \mathit {t}_{1}.\) 

The Eventual Visibility property requires that
a transaction that originates at a correct data center,
that is visible to some cl_uniform_barrier events,
or that is a strong transaction
eventually becomes visible at all correct data centers.
Let \( be the set of correct data centers.Formally,\begin{appdefinition}[\textsc {EventualVisibility}] {\begin{@align*}{1}{-1}&\textsc {EventualVisibility}\triangleq \forall \mathit {t}\in X \cap T.\; \\&\quad \textsl {dc}(\mathit {t}) \in (\exists q\in Q.\; \mathit {t}\xrightarrow{} q) \vee \mathit {t}\in T_{\textsl {strong}}\\&\qquad \Rightarrow  \left|\left\lbrace \mathit {t}^{\prime } \in T\mid \lnot (\mathit {t}\xrightarrow{} \mathit {t}^{\prime }) \right\rbrace  \right|< \infty .\end{@align*}}\end{appdefinition}\) section1
-3ex plus-1ex minus -.2ex2ex plus.2exTransaction Certification Service Specification
subsection2-.75.3Interface
The Transaction Certification Service (TCS) [5]}
is responsible for certifying strong transactions issued by transaction coordinators,
computing commit vectors and Lamport clocks for committed transactions,
and (asynchronously) delivering committed transactions to replicas.
Each strong transaction \(\mathit {t}\in T_{\textsl {all-strong}}\)  submitted to TCS
may be associated with its read set \(\textsl {rs}(\mathit {t})\) , write set \(\textsl {ws}(\mathit {t})\) ,
snapshot vector \(\textsl {snapshotVec}(\mathit {t})\)  (Definition REF ),
commit vector \(\textsl {commitVec}(\mathit {t})\)  (Definition REF ),
and Lamport clock \(\textsl {lclock}(\mathit {t})\)  (Definition REF ).
From \(\textsl {rs}(\mathit {t})\)  and \(\textsl {ws}(\mathit {t})\)  we can then define
\(W(t)\)  and \(R(t)\)  according to (REF ) and (), respectively.
Note that we have \(W(t) \subseteq R(t)\) .
Transaction coordinators for strong transactions interact with TCS
using two types of actions. Coordinators can make certification requests
(corresponding to procedure certify of Algorithm REF )
of the form
\({\sf certify}(\textsl {tid}(\mathit {t}), \textsl {ws}(\mathit {t}), R(\mathit {t}),\textsl {snapshotVec}(\mathit {t}), C(\mathit {t})),\) 
where \(\mathit {t}\in T_{\textsl {all-strong}}\)  and \(C(\mathit {t}) \in \mathbb {N}\) 
denotes the contribution of \(\textsl {client}(\mathit {t})\)  to the Lamport clock of \(\mathit {t}\) .
The TCS responses are of the form
\({\sf decide}(\textsl {tid}(\mathit {t}), \mathit {dec}, \mathit {vc}, \mathit {lc}),\) 
containing a decision \(\mathit {dec}\)  from \(\mathbb {D}= \lbrace \textsc {commit}, \textsc {abort}\rbrace \)  for \(\mathit {t}\) ,
a commit vector \(\mathit {vc}\)  from \(\mathbb {V}\)  for \(\mathit {t}\)  if \(\mathit {dec}= \textsc {commit}\) ,
and a Lamport clock \(\mathit {lc}\)  from \(\mathbb {N}\)  for \(\mathit {t}\)  if \(\mathit {dec}= \textsc {commit}\) .
If \(\mathit {dec}= \textsc {abort}\) , then \(\mathit {vc}\)  and \(\mathit {lc}\)  are irrelevant.
Besides, TCS can deliver some payload \(W\) 
to a replica via upcallactions \({\sf deliver}(W)\) 
(corresponding to procedure deliver_updates
of Algorithm REF ).
We denote by \({\sf deliver}^{m}_{d}(W)\)  the delivery of the payload \(W\)  to
a replica \(p^{m}_{d}\) , when the latter is relevant.
The payload \(W\)  in \({\sf deliver}^{m}_{d}(W)\)  is a set of tuples of the form
\(\langle \mathit {tid}, \mathit {wbuff}, \mathit {commitVec}, \mathit {lc}\rangle \) ,
each of which corresponds to the updates \(\mathit {wbuff}\subseteq \mathit {Key}\times \mathit {Val}\) 
performed at a particular partition \(m\) 
by a particular committed strong transaction
with transaction identifier \(\mathit {tid}\) , commit vector \(\mathit {commitVec}\) ,
and Lamport clock \(\mathit {lc}\) .
subsection2-.75.3Certification Functions
TCS is specified using a certification function
\(F: 2^{T_{\textsl {strong}}} \times T_{\textsl {all-strong}}\rightarrow \mathbb {D}\times \mathbb {V}\times \mathbb {N}.\) 

For a strong transaction \(\mathit {t}\in T_{\textsl {all-strong}}\) 
and the set \(T_{c}\subseteq T_{\textsl {strong}}\)  of previously committed strong transactions,
\(F(T_{c}, \mathit {t})\)  returns not only the decision \(\mathit {dec}\in \mathbb {D}\) ,
but also the commit vector \(\mathit {vc}\in \mathbb {V}\) 
and Lamport clock \(\mathit {lc}\in \mathbb {N}\)  for \(\mathit {t}\) .
We use \(F_{\rm dec}(T_{c}, \mathit {t})\) , \(F_{\rm vec}(T_{c}, \mathit {t})\) ,
and \(F_{\rm lc}(T_{c}, \mathit {t})\)  to select
the first, second, and third component
of \(F(T_{c}, \mathit {t})\) , respectively.
The decision \(F_{\rm dec}(T_{c}, \mathit {t})\)  should satisfy
\(&F_{\rm dec}(T_{c}, \mathit {t}) = \textsc {commit}\Leftrightarrow \forall k \in R(\mathit {t}).\; \forall \mathit {t}^{\prime } \in T_{c}.\nonumber \\&\quad \big (k \in W(\mathit {t}^{\prime }) \Rightarrow  \textsl {commitVec}(\mathit {t}^{\prime }) \le \textsl {snapshotVec}(\mathit {t})\big ).\) 
The commit vector \(F_{\rm vec}(T_{c}, \mathit {t})\)  should satisfy
\(&\phantom{\wedge \;} (\forall i \in \; F_{\rm vec}(T_{c}, \mathit {t})[i] = \textsl {snapshotVec}(\mathit {t})[i]) \nonumber \\&\wedge F_{\rm vec}(T_{c}, \mathit {t})[\textsl {strong}] > \textsl {snapshotVec}(\mathit {t})[\textsl {strong}] \nonumber \\&\wedge \forall \mathit {t}^{\prime } \in T_{c}.\; \mathit {t}\bowtie \mathit {t}^{\prime }\Rightarrow  F_{\rm vec}(T_{c}, \mathit {t}) \ge \textsl {commitVec}(\mathit {t}^{\prime }).\) 
The Lamport clock \(F_{\rm lc}(T_{c}, \mathit {t})\)  should satisfy
\(&F_{\rm lc}(T_{c}, \mathit {t}) \ge C(t) \;\wedge \nonumber \\&\quad \big (\forall \mathit {t}^{\prime } \in T_{c}.\; \mathit {t}\bowtie \mathit {t}^{\prime } \Rightarrow  F_{\rm lc}(T_{c}, \mathit {t}) > \textsl {lclock}(\mathit {t}^{\prime })\big ).\) 

subsection2-.75.3Histories of TCS
TCS executions are represented by histories,
which are (possibly infinite) sequences
of \({\sf certify}\) , \({\sf decide}\) , and \({\sf deliver}\)  actions.
For a TCS history \(h\) , we use \({\sf act}(h)\)  to denote the set of actions in \(h\) .
For actions \(\mathit {act}, \mathit {act}^{\prime } \in {\sf act}(h)\) ,
we write \(\mathit {act}\prec _{h} \mathit {act}^{\prime }\) 
when \(\mathit {act}\)  occurs before \(\mathit {act}^{\prime }\)  in \(h\) .
A strong transaction \(\mathit {t}\in T_{\textsl {all-strong}}\)  commits in a history \(h\) 
if \(h\)  contains \({\sf decide}(\textsl {tid}(\mathit {t}), \textsc {commit}, \_, \_)\) .
We denote by \({\sf committed}(h)\)  the projection of \(h\)  to actions
corresponding to the strong transactions that are committed in \(h\) .
Each history \(h\)  needs to meet the following requirements.


For each strong transaction \(\mathit {t}\in T_{\textsl {all-strong}}\) ,
there is at most one \({\sf certify}(\textsl {tid}(\mathit {t}), \_, \_, \_, \_)\) 
action in \(h\) .


For each action \({\sf decide}(\mathit {tid}, \_, \_, \_) \in {\sf act}(h)\) ,
there is exactly one \({\sf certify}(\mathit {tid}, \_, \_, \_, \_)\)  action in \(h\) 
such that
\({\sf certify}(\mathit {tid}, \_, \_, \_, \_)\prec _{h} {\sf decide}(\mathit {tid}, \_, \_, \_).\) 


For each action \({\sf deliver}(W) \in {\sf act}(h)\) 
and each \(\langle \mathit {tid}, \_, \_, \_ \rangle \in W\) ,
there is no \({\sf decide}(\mathit {tid}, \textsc {abort}, \_, \_)\)  action in \(h\) .


Every committed strong transaction is delivered at most once to each replica.


For each action \({\sf deliver}(W) \in {\sf act}(h)\) 
and each \(\langle \mathit {tid}, \_, \_, \_ \rangle \in W\) ,
there is a \({\sf certify}(\mathit {tid}, \_, \_, \_, \_)\)  action such that
\({\sf certify}(\mathit {tid}, \_, \_, \_, \_) \prec _{h} {\sf deliver}(W).\) 


At each replica \(p^{m}_{d}\) , committed strong transactions are delivered
in the increasing order of their strong timestamps.
Formally, for any two distinct actions
\({\sf deliver}^{m}_{d}(W_{1})\)  and \({\sf deliver}^{m}_{d}(W_{2})\) 
with payloads \(W_{1}\)  and \(W_{2}\) , respectively,
\(&{\sf deliver}^{m}_{d}(W_{1}) \prec _{h} {\sf deliver}^{m}_{d}(W_{2}) \Rightarrow  \\&\quad \forall \langle \_, \_, \mathit {commitVec}_{1}, \_ \rangle \in W_{1}.\;\\&\quad \forall \langle \_, \_, \mathit {commitVec}_{2}, \_ \rangle \in W_{2}.\; \\&\qquad \mathit {commitVec}_{1}[\textsl {strong}] < \mathit {commitVec}_{2}[\textsl {strong}].\) 

A history is complete if every \({\sf certify}\)  action
in it has a matching \({\sf decide}\)  action.
A complete history \(h\)  is sequential if
it consists of consecutive pairs of \({\sf certify}\)  and matching \({\sf decide}\)  actions.
For a complete history \(h\) , a permutation \(h^{\prime }\)  of \(h\) 
is a sequential history such that

\(h\)  and \(h^{\prime }\)  contain the same actions, i.e., \({\sf act}(h) = {\sf act}(h^{\prime })\) .

Transactions are certified in \(h^{\prime }\)  according to their session order.
\(&\forall \mathit {t}, \mathit {t}^{\prime } \in T_{\textsl {all-strong}}.\;\mathit {t}\xrightarrow{} \mathit {t}^{\prime } \Rightarrow  \\&\quad {\sf decide}(\textsl {tid}(\mathit {t}), \_, \_, \_) \prec _{h^{\prime }}{\sf certify}(\textsl {tid}(\mathit {t}^{\prime }), \_, \_, \_, \_).\) 

subsection2-.75.3TCS Correctness: Safety and Liveness
Safety of TCS
A complete sequential history \(h\)  is legal with respect to
a certification function \(F\) ,
if its results are computed so as to satisfy
(REF ) – (REF ) according to \(F\) :
\(&\forall \mathit {act}= {\sf decide}(\textsl {tid}(\mathit {t}), \mathit {dec}, \mathit {vc},\mathit {lc}) \in {\sf act}(h). \\&\quad (\mathit {dec}, \mathit {vc}, \mathit {lc})= F(\lbrace \mathit {t}^{\prime } \mid \\&\quad \quad {\sf decide}(\textsl {tid}(\mathit {t}^{\prime }), \textsc {commit}, \_, \_) \prec _{h} \mathit {act}\rbrace , \mathit {t}).\) 

A history \(h\)  is correct with respect to \(F\) 
if \(h \mid {\sf committed}(h)\)  has a legal permutation.
A TCS implementation is correct with respect to \(F\) 
if so are all its histories.

Liveness of TCS
TCS guarantees that every committed strong transaction
will eventually be delivered by every correct data center.
Formally,
\(&\forall \mathit {act}= {\sf decide}(\mathit {tid}, \textsc {commit}, \_, \_) \in {\sf act}(h).\nonumber \\&\quad \forall m \in \textsl {partitions}(\mathit {tid}).\; \forall c\in \nonumber \\&\qquad \exists \mathit {act}^{\prime } = {\sf deliver}^{m}_{c}(W) \in {\sf act}(h).\;\nonumber \\&\quad \qquad \langle \mathit {tid}, \_, \_, \_ \rangle \in W\wedge \mathit {act}\prec _{h} \mathit {act}^{\prime }.\) 

Here \(\textsl {partitions}(\mathit {tid})\)  denotes the set of partitions
that a particular transaction with transaction identifier \(\mathit {tid}\)  accesses.
A TCS implementation meets the liveness requirement if
every history produced by its maximal execution satisfies (REF ).
subsection2-.75.3TCS Correctness
The proof of TCS correctness is an adjustment
of the ones in [5]}, [7]}.
Theorem 8 
The TCS implementation in UniStore
(Algorithms REF  – REF )
is correct with respect to the certification function \(F\)  in (REF )
and meets the liveness requirement in (REF ).

section1
-3ex plus-1ex minus -.2ex2ex plus.2exThe Proof of UniStore Correctness
Consider an execution of UniStore with a history \(H = (X, \textsl {client}, \textsl {dc}, \textsl {so})\) .
We prove that \(H\)  satisfies PoR
by constructing an abstract execution \(A\)  (Theorem REF ).
We also establish the liveness guarantees of UniStore (Theorem REF ).
subsection2-.75.3Assumptions
We take the following assumptions about UniStore.
Assumption 1 
For any replica \(p^{m}_{d}\)  in data center \(d\) ,
\({\sf clock}\)  at \(p^{m}_{d}\)  is strictly increasing until \(d\)  (may) crash.

Assumption 2 
Replicas are connected by reliable FIFO channels:
messages are delivered in FIFO order,
and messages between correct data centers
are guaranteed to be eventually delivered.

Assumption 3 
We assume that in an execution of UniStore, any clients
and up to \(f\)  data centers may crash and that \(D > 2f\) .

Assumption 4 
We assume fairness of procedures of UniStore:
In an execution, if a procedure is enabled infinitely often,
then it will be executed infinitely often.

Assumption 5 
We consider only well-formed executions,
in which for each client:

transactions are issued in sequence; and

both cl_uniform_barrier and cl_attach events
can be issued only outside of transactions.


Assumption 6 
We consider only executions where
every causal commit event (i.e., commit_causal_tx) completes
and every strong commit event (i.e., commit_strong_tx) that calls the TCS completes.

We make the last assumption to simplify the technical development. The other
assumptions come from the system model.
subsection2-.75.3Notations
We use \(\mathit {cl}\)  to range over clients from a finite set \(\mathbb {C}\) .
We also use the following notations
to refer to different types of variables and their values
(below are some typical examples).

\({\sf snapVec}^{m}_{d}\) :
The variable \({\sf snapVec}\)  at replica \(p^{m}_{d}\) .

\(({\sf snapVec}^{m}_{d})_{e}\) :
The value of variable \({\sf snapVec}^{m}_{d}\) 
after the event \(e\)  is performed at replica \(p^{m}_{d}\) .

\({\sf snapVec}^{m}_{d}(\tau )\) :
The value of \({\sf snapVec}^{m}_{d}\)  at some specific time \(\tau \) .

\({\sf pastVec}_{\mathit {cl}}\) : The variable \({\sf pastVec}\)  at client \(\mathit {cl}\) .

\(({\sf pastVec}_{\mathit {cl}})_{e}\) :
The value of variable \({\sf pastVec}_{\mathit {cl}}\) 
after the event \(e\)  is performed at client \(\mathit {cl}\) .

\(\mathit {snapVec}_{(\textsc {get\_version}, e)}\) :
The actual value of parameter \(\mathit {snapVec}\)  of handler get_version
for event \(e\) .

\(\mathit {commitVec}_{(\textsc {commit\_causal}, e)}\) :
The value of the local variable \(\mathit {commitVec}\) 
in procedure commit_causal
after event \(e\)  is performed.

Besides, we use \(\textsl {coord}(t)\)  to denote the coordinator partition
of transaction \(\mathit {t}\) .
Each transaction is associated with a snapshot vector and a commit vector.
Definition 9 (Snapshot Vector)  
Let \(\mathit {t}\in T\)  be a transaction.
Let \(d \triangleq \textsl {dc}(\mathit {t})\)  and \(m \triangleq \textsl {coord}(\mathit {t})\) .
We define its snapshot vector \(\textsl {snapshotVec}(\mathit {t})\)  as
\(\textsl {snapshotVec}(\mathit {t}) \triangleq ({\sf snapVec}^{m}_{d})_{\textsl {st}(\mathit {t})}[\mathit {t}].\) 

Definition 10 (Commit Vector)  
Let \(\mathit {t}\in T\)  be a transaction.
Let \(d \triangleq \textsl {dc}(\mathit {t})\)  and \(m \triangleq \textsl {coord}(\mathit {t})\) .
We define its commit vector \(\textsl {commitVec}(\mathit {t})\)  as follows.

If \(\mathit {t}\)  is a read-only causal transaction, then
\(\textsl {commitVec}(\mathit {t}) \triangleq ({\sf snapVec}^{m}_{d})_{\textsl {ct}(\mathit {t})}[\mathit {t}].\) 

If \(\mathit {t}\)  is an update causal transaction, then
\(\textsl {commitVec}(\mathit {t}) \triangleq \mathit {commitVec}_{(\textsc {commit\_causal}, \textsl {ct}(\mathit {t}))}.\) 

If \(\mathit {t}\)  is a committed strong transaction, then
\(\textsl {commitVec}(\mathit {t}) \triangleq vc_{(\textsc {commit\_strong}, \textsl {ct}(\mathit {t}))}.\) 


Lemma 11
\(\forall \mathit {t}\in T.\; \textsl {commitVec}(\mathit {t}) \ge \textsl {snapshotVec}(\mathit {t}).\) 

We perform a case analysis according to the type of \(\mathit {t}\) .

\(\textsc {Case I}\) : \(\mathit {t}\)  is a read-only causal transaction.
By Definition REF  of \(\textsl {snapshotVec}(\mathit {t})\) ,
Definition REF  of \(\textsl {commitVec}(\mathit {t})\) ,
and Assumption REF ,
\(\textsl {commitVec}(\mathit {t}) = \textsl {snapshotVec}(\mathit {t}).\) 

\(\textsc {Case II}\) : \(\mathit {t}\)  is an update causal transaction.
By lines REF :REF 
and REF :REF ,
\(\textsl {commitVec}(\mathit {t}) \ge \textsl {snapshotVec}(\mathit {t}).\) 

\(\textsc {Case III}\) : \(\mathit {t}\)  is a strong transaction.
By line REF :REF 
and (REF ),
\(\textsl {commitVec}(\mathit {t}) \ge \textsl {snapshotVec}(\mathit {t}).\) 

For client \(\mathit {cl}\) , we use \(\textsl {cur\_dc}(\mathit {cl})\)  to denote the data center
to which \(\mathit {cl}\)  is currently attached.
We also use \(T|_{\mathit {cl}}\)  to denote the set of transactions issued by \(\mathit {cl}\) .
Formally,
\(T|_{\mathit {cl}} \triangleq \lbrace \mathit {t}\in T\mid \textsl {client}(\mathit {t}) = cl\rbrace .\) 
For a transaction \(\mathit {t}\)  and a partition \(m\) ,
we use \(\textsl {ws}(\mathit {t})[m]\)  to denote the subset of \(\textsl {ws}(\mathit {t})\) 
restricted to partition \(m\) .
Formally,
\(\textsl {ws}(\mathit {t})[m] \triangleq \lbrace \langle k, v \rangle \in \textsl {ws}(\mathit {t})\mid \mathtt {partition}(k) = m\rbrace .\) 
For notational convenience, we also define
\(\textsl {log}(\mathit {t}) \triangleq \lbrace \langle k, v, \textsl {commitVec}(\mathit {t}), \textsl {lclock}(\mathit {t})\rangle \mid \langle k, v \rangle \in \textsl {ws}(\mathit {t})\rbrace ,\) 

and
\(\textsl {log}(\mathit {t})[m] \triangleq \lbrace \langle k, v, \textsl {commitVec}(\mathit {t}), \textsl {lclock}(\mathit {t})\rangle \mid \langle k, v \rangle \in \textsl {ws}(\mathit {t})[m]\rbrace .\) 

For a key \(k \in \mathit {Key}\)  and a transaction \(\mathit {t}\in T_{k}\) ,
let \(\textsl {log}(\mathit {t})[k]\)  be the unique tuple
\(\langle k, v, \textsl {commitVec}(\mathit {t}), \textsl {lclock}(\mathit {t}) \rangle \) 
in \(\textsl {log}(\mathit {t})\) .
subsection2-.75.3Metadata for Causal Transactions
A causal transaction is committed when commit_causal for it returns.
A causal transaction is committed at replica \(p^{m}_{d}\) 
when commit for it at \(p^{m}_{d}\)  returns.

Properties of \({\sf knownVec}\)
Lemma 12 
For any replica \(p^{m}_{d}\)  in data center \(d\) ,
\({\sf knownVec}^{m}_{d}[d]\)  is non-decreasing.

Consider two points of time \(\tau _{1}\)  and \(\tau _{2}\)  such that \(\tau _{1} < \tau _{2}\) .
We need to show that
\({\sf knownVec}^{m}_{d}(\tau _{1})[d] \le {\sf knownVec}^{m}_{d}(\tau _{2})[d].\) 
Note that \({\sf knownVec}^{m}_{d}[d]\)  is updated only
at lines REF :REF 
or REF :REF .
We distinguish between the following four cases.

\(\textsc {Case I}\) :
Both \({\sf knownVec}^{m}_{d}(\tau _{1})[d]\)  and \({\sf knownVec}^{m}_{d}(\tau _{2})[d]\)  are set
at line REF :REF .
By line REF :REF 
and Assumption REF ,
\({\sf knownVec}^{m}_{d}(\tau _{1})[d] &= {\sf clock}^{m}_{d}(\tau _{1}) \\&< {\sf clock}^{m}_{d}(\tau _{2}) \\&= {\sf knownVec}^{m}_{d}(\tau _{2})[d].\) 

\(\textsc {Case II}\) :
\({\sf knownVec}^{m}_{d}(\tau _{1})[d]\)  is set
at line REF :REF 
and \({\sf knownVec}^{m}_{d}(\tau _{2})[d]\)  is set
at line REF :REF .
By line REF :REF ,
\({\sf knownVec}^{m}_{d}(\tau _{1})[d] = {\sf clock}^{m}_{d}(\tau _{1}).\) 
By the fact that \({\sf preparedCausal}^{m}_{d}(\tau _{1}) = \varnothing \) ,
\(\tau _{2} > \tau _{1}\) ,
and line REF :REF ,
\(\forall \langle \_, \_, &\mathit {ts}\rangle \in \; {\sf preparedCausal}^{m}_{d}(\tau _{2}).\; \\&\mathit {ts}> {\sf clock}^{m}_{d}(\tau _{1}) = {\sf knownVec}^{m}_{d}(\tau _{1})[d].\) 

Therefore, by line REF :REF ,
\(&{\sf knownVec}^{m}_{d}(\tau _{1})[d] \\&\quad \le \min \lbrace \mathit {ts}\mid \langle \_, \_, \mathit {ts}\rangle \in {\sf preparedCausal}^{m}_{d}(\tau _{2})\rbrace  - 1 \\&\quad = {\sf knownVec}^{m}_{d}(\tau _{2})[d].\) 

\(\textsc {Case III}\) :
\({\sf knownVec}^{m}_{d}(\tau _{1})[d]\)  is set
at line REF :REF 
and \({\sf knownVec}^{m}_{d}(\tau _{2})[d]\)  is set
at line REF :REF .
Let \(\mathit {t}_{1}\)  be the transaction in \({\sf preparedCausal}^{m}_{d}(\tau _{1})\) 
that has the minimum \(\mathit {ts}\) . Formally,
\(\mathit {t}_{1} \triangleq \operatornamewithlimits{argmin}\limits _{\mathit {t}}\lbrace \mathit {ts}\mid \langle \textsl {tid}(\mathit {t}), \_, \mathit {ts}\rangle \in {\sf preparedCausal}^{m}_{d}(\tau _{1})\rbrace .\) 

By lines REF :REF ,
REF :REF ,
REF :REF ,
and REF :REF ,
\({\sf knownVec}^{m}_{d}(\tau _{1})[d] &< \textsl {commitVec}(\mathit {t}_{1})[d] \\&\le {\sf clock}^{m}_{d}(\tau _{2}) \\&= {\sf knownVec}^{m}_{d}(\tau _{2})[d].\) 

\(\textsc {Case IV}\) :
Both \({\sf knownVec}^{m}_{d}(\tau _{1})[d]\)  and \({\sf knownVec}^{m}_{d}(\tau _{2})[d]\)  are set
at line REF :REF .
By lines REF :REF 
and REF :REF ,
\(&{\sf knownVec}^{m}_{d}(\tau _{1})[d] \\&\quad = \min \lbrace \mathit {ts}\mid \langle \_, \_, \mathit {ts}\rangle \in {\sf preparedCausal}^{m}_{d}(\tau _{1})\rbrace  - 1 \\&\quad \le \min \lbrace \mathit {ts}\mid \langle \_, \_, \mathit {ts}\rangle \in {\sf preparedCausal}^{m}_{d}(\tau _{2})\rbrace  - 1 \\&\quad = {\sf knownVec}^{m}_{d}(\tau _{2})[d].\) 

Lemma 13 
For \(i \in \lbrace d\rbrace \) ,
\({\sf knownVec}^{m}_{d}[i]\)  at any replica \(p^{m}_{d}\)  in data center \(d\) 
is non-decreasing.

Note that \({\sf knownVec}^{m}_{d}[i]\)  (\(i \in \lbrace d\rbrace \) )
can be updated only
at lines REF :REF 
and REF :REF .
Therefore, this lemma holds due to
lines REF :REF 
and REF :REF .
Lemma 14 
For \(i \in , \)knownVecmd[i]\( at any replica \) pmd\(in data center \) d\( is non-decreasing.\)
By Lemmas REF 
and REF .
Lemma 15 
For any replica \(p^{m}_{d}\)  in data center \(d\) ,
\({\sf knownVec}^{m}_{d}[d] \le {\sf clock}^{m}_{d}.\) 

Note that \({\sf knownVec}^{m}_{d}[d]\)  is updated only
at lines REF :REF 
or REF :REF .

\(\textsc {Case I}\) : \({\sf knownVec}^{m}_{d}[d]\)  is updated
at line REF :REF .
By Assumption REF ,
\({\sf knownVec}^{m}_{d}[d] \le {\sf clock}^{m}_{d}.\) 

\(\textsc {Case II}\) : \({\sf knownVec}^{m}_{d}[d]\)  is updated
at line REF :REF .
By line REF :REF ,
immediately after this update,
\({\sf knownVec}^{m}_{d}[d] < {\sf clock}^{m}_{d}.\) 

Lemma 16 
Let \(p^{m}_{d}\)  be a replica in data center \(d\) .
Consider \({\sf knownVec}^{m}_{d}(\tau )[d]\)  at time \(\tau \) 
and transaction \(\mathit {t}\in T_{\textsl {causal}}\)  committed at \(p^{m}_{d}\) 
after time \(\tau \) . Then
\(\textsl {commitVec}(\mathit {t})[d] > {\sf knownVec}^{m}_{d}(\tau )[d].\) 

Suppose that before time \(\tau \) ,
\({\sf knownVec}^{m}_{d}[d]\)  is last updated at time \(\tau ^{\prime } < \tau \) .
Therefore,
\({\sf knownVec}^{m}_{d}(\tau )[d] = {\sf knownVec}^{m}_{d}(\tau ^{\prime })[d].\) 
We distinguish between two cases according to whether
\({\sf preparedCausal}^{m}_{d}(\tau ^{\prime }) = \varnothing \) 
when \({\sf knownVec}^{m}_{d}[d]\)  is updated at time \(\tau ^{\prime }\) .

\(\textsc {Case I}\) : \({\sf preparedCausal}^{m}_{d}(\tau ^{\prime }) = \varnothing \) .
By line REF :REF ,
\({\sf knownVec}^{m}_{d}(\tau ^{\prime })[d] = {\sf clock}^{m}_{d}(\tau ^{\prime }).\) 
By line REF :REF ,
line REF :REF ,
and Assumption REF ,
\(\textsl {commitVec}(\mathit {t})[d] > {\sf clock}^{m}_{d}(\tau ^{\prime }).\) 
Therefore,
\(\textsl {commitVec}(\mathit {t})[d] &> {\sf knownVec}^{m}_{d}(\tau ^{\prime })[d] \\&= {\sf knownVec}^{m}_{d}(\tau )[d].\) 

\(\textsc {Case II}\) : \({\sf preparedCausal}^{m}_{d}(\tau ^{\prime }) \ne \varnothing \) .
We further distinguish between two cases according to whether
\(\langle \textsl {tid}(\mathit {t}), \_, \_ \rangle \in {\sf preparedCausal}^{m}_{d}(\tau ^{\prime }).\) 

\(\textsc {Case II-1}\) :
\(\langle \textsl {tid}(\mathit {t}), \_, \mathit {ts}\rangle \in {\sf preparedCausal}^{m}_{d}(\tau ^{\prime })\) .
By lines REF :REF 
and REF :REF ,
\(\textsl {commitVec}(\mathit {t})[d] &\ge \mathit {ts}\\&> {\sf knownVec}^{m}_{d}(\tau ^{\prime })[d] \\&= {\sf knownVec}^{m}_{d}(\tau )[d].\) 

\(\textsc {Case II-2}\) :
\(\langle \textsl {tid}(\mathit {t}), \_, \_ \rangle \notin {\sf preparedCausal}^{m}_{d}(\tau ^{\prime })\) .
By Lemma REF ,
Assumption REF ,
line REF :REF ,
and line REF :REF ,
\(\textsl {commitVec}(\mathit {t})[d] &> {\sf knownVec}^{m}_{d}(\tau ^{\prime })[d] \\&= {\sf knownVec}^{m}_{d}(\tau )[d].\) 


Lemma 17 
Let \(\mathit {t}\in T_{\textsl {causal}}\)  be a causal transaction
that originates at data center \(d\)  and accesses partition \(m\) .
If
\(\textsl {commitVec}(\mathit {t})[d] \le {\sf knownVec}^{m}_{d}[d],\) 
then
\(\textsl {log}(\mathit {t})[m] \subseteq {\sf opLog}^{m}_{d}.\) 

Suppose that the value \({\sf knownVec}^{m}_{d}[d]\)  is set at time \(\tau \) .
By Lemma REF ,
\(\mathit {t}\)  is committed at \(p^{m}_{d}\)  before time \(\tau \) .
Therefore, by line REF :REF ,
\(\textsl {log}(\mathit {t})[m] \subseteq {\sf opLog}^{m}_{d}.\) 
The following lemmas consider the replication and forwarding
of causal transactions.
Lemma 18 
Let \(p^{m}_{d}\)  be a replica in data center \(d\) .
Let \(\mathit {t}_{1}\)  and \(\mathit {t}_{2}\)  be two transactions
replicated by \(p^{m}_{d}\)  to sibling replicas
at time \(\tau _{1}\)  and \(\tau _{2}\) 
(line REF :REF ),
respectively. Then
\(\tau _{1} < \tau _{2} \Rightarrow  \textsl {commitVec}(\mathit {t}_{1})[d] < \textsl {commitVec}(\mathit {t}_{2})[d].\) 

Since \(\mathit {t}_{1}\)  is replicated at time \(\tau _{1}\) ,
by line REF :REF ,
\(\textsl {commitVec}(\mathit {t}_{1})[d] \le {\sf knownVec}^{m}_{d}(\tau _{1})[d].\) 
Assume that \(\tau _{1} < \tau _{2}\) .
We distinguish between two cases according to whether
\(\langle \textsl {tid}(\mathit {t}_{2}), \_, \_, \_ \rangle \in {\sf committedCausal}^{m}_{d}(\tau _{1})[d].\) 

\(\textsc {Case I}\) :
\(\langle \textsl {tid}(\mathit {t}_{2}), \_, \_, \_ \rangle \in {\sf committedCausal}^{m}_{d}(\tau _{1})[d]\) .
Since \(\mathit {t}_{2}\)  is not replicated at time \(\tau _{1}\) ,
by line REF :REF ,
\(\textsl {commitVec}(\mathit {t}_{2})[d] > {\sf knownVec}^{m}_{d}(\tau _{1})[d].\) 

\(\textsc {Case II}\) :
\(\langle \textsl {tid}(\mathit {t}_{2}), \_, \_, \_, \rangle \notin {\sf committedCausal}^{m}_{d}(\tau _{1})[d]\) .
Thus, \(\mathit {t}_{2}\)  is committed at \(p^{m}_{d}\)  after time \(\tau _{1}\) .
By Lemma REF ,
\(\textsl {commitVec}(\mathit {t}_{2})[d] > {\sf knownVec}^{m}_{d}(\tau _{1})[d].\) 

Therefore, in either case,
\(\textsl {commitVec}(\mathit {t}_{1})[d] < \textsl {commitVec}(\mathit {t}_{2})[d].\) 
Lemma 19 
Let \(p^{m}_{d}\)  be a replica in data center \(d\) .
Consider a heartbeat \({\sf knownVec}^{m}_{d}(\tau _{1})[d]\) 
sent by \(p^{m}_{d}\)  at time \(\tau _{1}\) 
(line REF :REF ).
Let \(\mathit {t}\)  be a transaction replicated by \(p^{m}_{d}\)  at time \(\tau _{2}\) 
(line REF :REF ).
Then
\(\tau _{1} < \tau _{2} \Leftrightarrow {\sf knownVec}^{m}_{d}(\tau _{1})[d] < \textsl {commitVec}(\mathit {t})[d].\) 

We first show that
\(\tau _{1} < \tau _{2} \Rightarrow  {\sf knownVec}^{m}_{d}(\tau _{1})[d] < \textsl {commitVec}(\mathit {t})[d].\) 
Assume that \(\tau _{1} < \tau _{2}\) .
We distinguish between two cases according to whether
\(\langle \textsl {tid}(\mathit {t}), \_, \_, \_ \rangle \in {\sf committedCausal}^{m}_{d}(\tau _{1})[d].\) 

\(\textsc {Case I}\) :
\(\langle \textsl {tid}(\mathit {t}), \_, \_, \_ \rangle \in {\sf committedCausal}^{m}_{d}(\tau _{1})[d]\) .
By line REF :REF ,
\(\textsl {commitVec}(\mathit {t})[d] > {\sf knownVec}^{m}_{d}(\tau _{1})[d].\) 

\(\textsc {Case II}\) :
\(\langle \textsl {tid}(\mathit {t}), \_, \_, \_ \rangle \notin {\sf committedCausal}^{m}_{d}(\tau _{1})[d]\) .
Thus, \(\mathit {t}\)  is committed at \(p^{m}_{d}\)  after time \(\tau _{1}\) .
By Lemma REF ,
\(\textsl {commitVec}(\mathit {t})[d] > {\sf knownVec}^{m}_{d}(\tau _{1})[d].\) 

Next we show that (note that \(\tau _{1} \ne \tau _{2}\) )
\(\tau _{2} < \tau _{1} \Rightarrow  \textsl {commitVec}(\mathit {t})[d] \le {\sf knownVec}^{m}_{d}(\tau _{1})[d].\) 
Since \(\mathit {t}\)  is replicated by \(p^{m}_{d}\)  at time \(\tau _{2}\) ,
by line REF :REF ,
\(\textsl {commitVec}(\mathit {t})[d] \le {\sf knownVec}^{m}_{d}(\tau _{2})[d].\) 
Assume that \(\tau _{2} < \tau _{1}\) .
By Lemma REF ,
\({\sf knownVec}^{m}_{d}(\tau _{2})[d] \le {\sf knownVec}^{m}_{d}(\tau _{1})[d].\) 
Putting it together yields
\(\textsl {commitVec}(\mathit {t})[d] \le {\sf knownVec}^{m}_{d}(\tau _{1})[d].\) 
Lemma 20 
Let \(p^{m}_{d}\)  be a replica in data center \(d\) . Then
\(&\forall i \ne d.\;\forall \langle \textsl {tid}(\mathit {t}), \_, \_, \_ \rangle \in {\sf committedCausal}^{m}_{d}[i]. \\&\quad \textsl {commitVec}(\mathit {t})[i] \le {\sf knownVec}^{m}_{d}[i].\) 

By lines REF :REF 
and REF :REF 
and Lemma REF .
Lemma 21 
For \(j \ne d\)  and \(i \notin \lbrace d, j\rbrace \) ,
\({\sf globalMatrix}^{m}_{d}[i][j]\)  at any replica \(p^{m}_{d}\) 
in data center \(d\)  is non-decreasing.

Note that \({\sf globalMatrix}^{m}_{d}[i][j]\)  can be updated only
at line REF :REF .
Therefore, by Lemma REF ,
it is non-decreasing.
Lemma 22 
Let \(p^{m}_{d}\)  be a replica in data center \(d\) .
Let \(\mathit {t}_{1}\)  and \(\mathit {t}_{2}\)  be two transactions
that originate at data center \(j \ne d\) 
and are forwarded by \(p^{m}_{d}\)  to
sibling replica \(p^{m}_{i}\)  in data center \(i \notin \lbrace d, j\rbrace \) 
at time \(\tau _{1}\)  and \(\tau _{2}\) 
(line REF :REF ),
respectively. Then
\(\tau _{1} < \tau _{2} \Rightarrow  \textsl {commitVec}(\mathit {t}_{1})[j] < \textsl {commitVec}(\mathit {t}_{2})[j].\) 

Since \(\mathit {t}_{1}\)  is forwarded by \(p^{m}_{d}\)  at time \(\tau _{1}\) ,
by line REF :REF ,
\(\langle \textsl {tid}(\mathit {t}_{1}), \_, \_, \_ \rangle \in {\sf committedCausal}^{m}_{d}(\tau _{1})[j].\) 
By Lemmas REF  and REF ,
\(\textsl {commitVec}(\mathit {t}_{1})[j] \le {\sf knownVec}^{m}_{d}(\tau _{1})[j].\) 

Assume that \(\tau _{1} < \tau _{2}\) .
We first argue that
\(\langle \textsl {tid}(\mathit {t}_{2}), \_, \_, \_ \rangle \notin {\sf committedCausal}^{m}_{d}(\tau _{1})[j].\) 

Otherwise, by line REF :REF ,
\(\textsl {commitVec}(\mathit {t}_{2})[j] \le {\sf globalMatrix}^{m}_{d}(\tau _{1})[i][j].\) 
By Lemma REF ,
\(\textsl {commitVec}(\mathit {t}_{2})[j] \le {\sf globalMatrix}^{m}_{d}(\tau _{2})[i][j].\) 
Therefore, by line REF :REF ,
\(\mathit {t}_{2}\)  would not be forwarded by \(p^{m}_{d}\)  to \(p^{m}_{i}\)  at time \(\tau _{2}\) .
Thus, (REF ) holds.
Since \(\mathit {t}_{2}\)  is forwarded by \(p^{m}_{d}\)  to \(p^{m}_{i}\)  at time \(\tau _{2}\) ,
\(\langle \textsl {tid}(\mathit {t}_{2}), \_, _, \_ \rangle \in {\sf committedCausal}^{m}_{d}(\tau _{2})[j].\) 
By Lemma REF 
and line REF :REF ,
\(\textsl {commitVec}(\mathit {t}_{2})[j] > {\sf knownVec}^{m}_{d}(\tau _{1})[j].\) 

Putting (REF ) and (REF ) together yields
\(\textsl {commitVec}(\mathit {t}_{1})[j] < \textsl {commitVec}(\mathit {t}_{2})[j].\) 
Lemma 23 
Let \(p^{m}_{d}\)  be a replica in data center \(d\) .
Consider a heartbeat \({\sf knownVec}^{m}_{d}(\tau _{1})[j]\)  (\(j \ne d\) )
sent by \(p^{m}_{d}\)  to sibling replica \(p^{m}_{i}\) 
in data center \(i \notin \lbrace d, j\rbrace \)  at time \(\tau _{1}\) 
(line REF :REF ).
Let \(\mathit {t}\)  be a transaction that originates at data center \(j\) 
and is forwarded by \(p^{m}_{d}\)  to \(p^{m}_{i}\)  at time \(\tau _{2}\) 
(line REF :REF ).
Then
\(\tau _{1} < \tau _{2} \Leftrightarrow {\sf knownVec}^{m}_{d}(\tau _{1})[j] < \textsl {commitVec}(\mathit {t})[j].\) 

We first show that
\(\tau _{1} < \tau _{2} \Rightarrow  {\sf knownVec}^{m}_{d}(\tau _{1})[j] < \textsl {commitVec}(\mathit {t})[j].\) 
Assume that \(\tau _{1} < \tau _{2}\) .
We first argue that
\(\langle \textsl {tid}(\mathit {t}), \_, \_, \_ \rangle \notin {\sf committedCausal}^{m}_{d}(\tau _{1})[j].\) 

Otherwise, since \(\mathit {t}\)  is not forwarded at time \(\tau _{1}\) ,
by line REF :REF ,
\(\textsl {commitVec}(\mathit {t})[j] \le {\sf globalMatrix}^{m}_{d}(\tau _{1})[i][j].\) 
By Lemma REF ,
\(\textsl {commitVec}(\mathit {t})[j] \le {\sf globalMatrix}^{m}_{d}(\tau _{2})[i][j].\) 
Therefore, by line REF :REF ,
\(\mathit {t}\)  would not be forwarded by \(p^{m}_{d}\)  to \(p^{m}_{i}\)  at time \(\tau _{2}\) .
Thus, (REF ) holds.
Since \(\mathit {t}\)  is forwarded by \(p^{m}_{d}\)  to \(p^{m}_{i}\)  at time \(\tau _{2}\) ,
\(\langle \textsl {tid}(\mathit {t}), \_, \_, \_ \rangle \in {\sf committedCausal}^{m}_{d}(\tau _{2})[j].\) 
By Lemma REF 
and line REF :REF ,
\({\sf knownVec}^{m}_{d}(\tau _{1})[j] < \textsl {commitVec}(\mathit {t})[j].\) 
Next we show that (note that \(\tau _{1} \ne \tau _{2}\) )
\(\tau _{2} < \tau _{1} \Rightarrow  \textsl {commitVec}(\mathit {t})[j] \le {\sf knownVec}^{m}_{d}(\tau _{1})[j].\) 
Since \(\mathit {t}\)  is forwarded by \(p^{m}_{d}\)  to \(p^{m}_{i}\)  at time \(\tau _{2}\) ,
by line REF :REF ,
\(\langle \textsl {tid}(\mathit {t}), \_, \_, \_ \rangle \in {\sf committedCausal}^{m}_{d}(\tau _{2})[j].\) 
By Lemmas REF  and REF ,
\(\textsl {commitVec}(\mathit {t})[j] \le {\sf knownVec}^{m}_{d}(\tau _{2})[j].\) 
Assume that \(\tau _{2} < \tau _{1}\) .
By Lemma REF ,
\({\sf knownVec}^{m}_{d}(\tau _{2})[j] \le {\sf knownVec}^{m}_{d}(\tau _{1})[j].\) 
Putting it together yields
\(\textsl {commitVec}(\mathit {t})[j] \le {\sf knownVec}^{m}_{d}(\tau _{1})[j].\) 
Lemma 24 
Let \(\mathit {t}\in T_{\textsl {causal}}\)  be a causal transaction
that originates at data center \(i\)  and accesses partition \(m\) .
If
\(\textsl {commitVec}(\mathit {t})[i] \le {\sf knownVec}^{m}_{d}[i]\) 
for replica \(p^{m}_{d}\)  in data center \(d \ne i\) ,
then
\(\textsl {log}(\mathit {t})[m] \subseteq {\sf opLog}^{m}_{d}.\) 

Note that for \(i \in \lbrace d\rbrace \) ,
\({\sf knownVec}^{m}_{d}[i]\)  can be updated
only at lines REF :REF 
or REF :REF 
due to replication of transactions or heartbeats respectively,
either directly from data center \(i\) 
(line REF :REF )
or indirectly from a third data center \(j \ne i\) 
(line REF :REF ).
We proceed by induction on the length of the execution.
In the following, for replica \(p^{m}_{d}\)  in data center \(d \in ,we denote the value of \)knownVecmd\( (resp. \)opLogmd\()after \) k\( steps in an executionby \)knownVecmd(k)\( (resp. \)opLogmd(k)\().\begin{itemize}\item \emph {Base Case.} k = 0.It holds trivially,since for replica p^{m}_{d} in any data center d \ne i,{\sf knownVec}^{m}_{d}(0)[i] = 0.\item \emph {Induction Hypothesis.}Suppose that for any execution of length k, we have{\begin{@align*}{1}{-1}&\forall d \in \lbrace i\rbrace .\;\forall \mathit {t}\in T_{\textsl {causal}}.\; \\&\quad \big (\textsl {commitVec}(\mathit {t})[i] \le {\sf knownVec}^{m}_{d}(k)[i] \\&\quad \quad \Rightarrow  \textsl {log}(\mathit {t})[m] \subseteq {\sf opLog}^{m}_{d}(k)\big ).\end{@align*}}\item \emph {Induction Step.}Consider an execution of length k + 1.If the (k+1)-st step of this execution does not update{\sf knownVec}^{m}_{d}[i] for replica p^{m}_{d} in any data center d \ne i,then by the induction hypothesis,{\begin{@align*}{1}{-1}&\forall d \in \lbrace i\rbrace .\;\forall \mathit {t}\in T_{\textsl {causal}}.\; \\&\quad \big (\textsl {commitVec}(\mathit {t})[i] \le {\sf knownVec}^{m}_{d}(k+1)[i] \\&\quad \quad \Rightarrow  \textsl {log}(\mathit {t})[m] \subseteq {\sf opLog}^{m}_{d}(k+1)\big ).\end{@align*}}Otherwise, we perform a case analysis according tohow {\sf knownVec}^{m}_{d}[i] of replica p^{m}_{d} in data center d \ne iis updated in the (k+1)-st step.\begin{itemize}\item \textsc {Case I:}{\sf knownVec}^{m}_{d}[i] is updated due to delivery of a messagefrom data center i.By Lemmas~\ref {lemma:knownvc-d-nondecreasing},\ref {lemma:replication-order}, and \ref {lemma:heartbeat-replication-order},local transactions and heartbeats are propagated by p^{m}_{i} to sibling replicasin increasing order of their local timestamps \mathit {commitVec}[i]and {\sf knownVec}^{m}_{i}[i] values.Therefore, by Assumption~\ref {assumption:message}and the induction hypothesis,{\begin{@align*}{1}{-1}&\forall \mathit {t}\in T_{\textsl {causal}}.\; \\&\quad \big (\textsl {commitVec}(\mathit {t})[i] \le {\sf knownVec}^{m}_{d}(k+1)[i] \\&\quad \quad \Rightarrow  \textsl {log}(\mathit {t})[m] \subseteq {\sf opLog}^{m}_{d}(k+1)\big ).\end{@align*}}\item \textsc {Case II:}{\sf knownVec}^{m}_{d}[i] is updated due to delivery of a messagefrom a third data center j \ne i.By Lemmas~\ref {lemma:knownvc-i-nondecreasing},\ref {lemma:forwarding-order}, and \ref {lemma:heartbeat-forwarding-order},transactions originating at data center i and heartbeats are forwardedby some replica, say p^{m}_{j} (j \ne i),to sibling replicas in increasing order oftheir local timestamps \mathit {commitVec}[i] and {\sf knownVec}^{m}_{j}[i] values.Therefore, by Assumption~\ref {assumption:message}and the induction hypothesis,{\begin{@align*}{1}{-1}&\forall \mathit {t}\in T_{\textsl {causal}}.\; \\&\quad \big (\textsl {commitVec}(\mathit {t})[i] \le {\sf knownVec}^{m}_{d}(k+1)[i] \\&\quad \quad \Rightarrow  \textsl {log}(\mathit {t})[m] \subseteq {\sf opLog}^{m}_{d}(k+1)\big ).\end{@align*}}\end{itemize}\end{itemize}\)
Lemma 25 (Property 1)  
Let \(\mathit {t}\in T_{\textsl {causal}}\)  be a causal transaction
that originates at data center \(i\) 
and accesses partition \(m\) .
If
\(\textsl {commitVec}(\mathit {t})[i] \le {\sf knownVec}^{m}_{d}[i]\) 
for replica \(p^{m}_{d}\)  in data center \(d\) ,
then
\(\textsl {log}(\mathit {t})[m] \subseteq {\sf opLog}^{m}_{d}.\) 

By Lemmas REF  and REF .
Properties of \({\sf stableVec}\)
Lemma 26 
For \(i \in , \)stableVecmd[i]\(at any replica \) pmd\( in data center \) d\( is non-decreasing.\)
Note that \({\sf stableVec}^{m}_{d}[i]\)  (\(i \in ) can be updatedonly at line~\ref {alg:unistore-clock}:\ref {line:knownvclocal-stablevc-causal}.By Lemma~\ref {lemma:knownvc-nondecreasing}and Assumption~\ref {assumption:message},\)stableVecmd[i]\( is non-decreasing.\)
Lemma 27 (Property 2)  
For any replica \(p^{m}_{d}\)  in data center \(d\) ,
\(\forall i \in \; \forall n \in \mathcal {P}.\;{\sf stableVec}^{m}_{d}[i] \le {\sf knownVec}^{n}_{d}[i].\) 

Note that \({\sf stableVec}^{m}_{d}[i]\)  (\(i \in )can be updated onlyat line~\ref {alg:unistore-clock}:\ref {line:knownvclocal-stablevc-causal}.By the way \)stableVecmd[i]\( is updatedand Lemmas~\ref {lemma:knownvc-d-nondecreasing}and \ref {lemma:knownvc-i-nondecreasing},\)\(\forall n \in \mathcal {P}.\; {\sf stableVec}^{m}_{d}[i] \le {\sf knownVec}^{n}_{d}[i].\)\(\)
Lemma 28 
Let \(\mathit {t}\in T_{\textsl {causal}}\)  be a causal transaction
that originates at data center \(i\) 
and accesses partition \(n\) .
If
\(\textsl {commitVec}(\mathit {t})[i] \le {\sf stableVec}^{m}_{d}[i]\) 
for some replica \(p^{m}_{d}\)  in data center \(d\) ,
then
\(\textsl {log}(\mathit {t})[n] \subseteq {\sf opLog}^{n}_{d}.\) 

By Lemma REF ,
\({\sf stableVec}^{m}_{d}[i] \le {\sf knownVec}^{n}_{d}[i].\) 
Therefore,
\(\textsl {commitVec}(\mathit {t})[i] \le {\sf knownVec}^{n}_{d}[i].\) 
By Lemma REF ,
\(\textsl {log}(\mathit {t})[n] \subseteq {\sf opLog}^{n}_{d}.\) 
Properties of \({\sf uniformVec}\)
Lemma 29 
For \(i \in , \)uniformVecmd[i]\(at any replica \) pmd\( in data center \) d\( is non-decreasing.\)
Note that whenever \({\sf uniformVec}^{m}_{d}[i]\)  is updated
at lines REF :REF ,
REF :REF ,
REF :REF ,
or REF :REF ,
we take the maximum of it and some scalar value.
Lemma 30 
Let \(e \in E\)  be an event issued by client \(\mathit {cl}\) 
to replica \(p^{m}_{d}\)  in data center \(d\) . Then
\(&e \in E \setminus Q\Rightarrow  \\&\quad \forall i \in \lbrace d\rbrace .\;({\sf pastVec}_{\mathit {cl}})_{e}[i] \le ({\sf uniformVec}^{m}_{d})_{e}[i],\) 

and
\(e \in Q\Rightarrow  ({\sf pastVec}_{\mathit {cl}})_{e}[d] \le ({\sf uniformVec}^{m}_{d})_{e}[d].\) 

We perform a case analysis according to the type of event \(e\) .

\(\textsc {Case I}\) : \(e \in S\) .
By line REF :REF ,
\(\forall i \in \lbrace d\rbrace .\;({\sf pastVec}_{\mathit {cl}})_{e}[i] \le ({\sf uniformVec}^{m}_{d})_{e}[i].\) 

\(\textsc {Case II}\) : \(e \in R \cup U\) .
In this case,
\(({\sf pastVec}_{\mathit {cl}})_{e} = ({\sf pastVec}_{\mathit {cl}})_{\textsl {st}(e)}.\) 
By Case I,
\(\forall i \in \lbrace d\rbrace .\;({\sf pastVec}_{\mathit {cl}})_{\textsl {st}(e)}[i] \le ({\sf uniformVec}^{m}_{d})_{\textsl {st}(e)}[i].\) 
By Lemma REF ,
\(\forall i \in \lbrace d\rbrace . \\({\sf uniformVec}^{m}_{d})_{\textsl {st}(e)} \le ({\sf uniformVec}^{m}_{d})_{e}.\) 
Putting it together yields
\(\forall i \in \lbrace d\rbrace .\;({\sf pastVec}_{\mathit {cl}})_{e}[i] \le ({\sf uniformVec}^{m}_{d})_{e}[i].\) 

\(\textsc {Case III}\) : \(e \in C_{\textsl {causal}}\) .
By line REF :REF ,
\(({\sf pastVec}_{\mathit {cl}})_{e} = vc_{(\textsc {commit\_causal\_tx}, e)}.\) 
By lines REF :REF ,
REF :REF ,
and REF :REF ,
\(&\forall i \in \lbrace d\rbrace . \\&\quad vc_{(\textsc {commit\_causal\_tx}, e)}[i] = ({\sf snapVec}^{m}_{d})_{e}[\textsl {tx}(e)][i].\) 

By line REF :REF ,
\(&\forall i \in \lbrace d\rbrace . \\&\quad ({\sf snapVec}^{m}_{d})_{e}[\textsl {tx}(e)][i] = ({\sf uniformVec}^{m}_{d})_{\textsl {st}(e)}[i].\) 

By Lemma REF ,
\(\forall i \in \lbrace d\rbrace . \\({\sf uniformVec}^{m}_{d})_{\textsl {st}(e)} \le ({\sf uniformVec}^{m}_{d})_{e}.\) 
Putting it together yields
\(\forall i \in \lbrace d\rbrace .\;({\sf pastVec}_{\mathit {cl}})_{e}[i] \le ({\sf uniformVec}^{m}_{d})_{e}[i].\) 

\(\textsc {Case IV}\) : \(e \in C_{\textsl {strong}}\) .
By line REF :REF ,
\(({\sf pastVec}_{\mathit {cl}})_{e} = vc_{(\textsc {commit\_strong\_tx}, e)}.\) 
By (REF ),
\(&\forall i \in \lbrace d\rbrace . \\&\quad vc_{(\textsc {commit\_strong\_tx}, e)}[i] = ({\sf snapVec}^{m}_{d})_{e}[\textsl {tx}(e)][i].\) 

Therefore, similar to Case III, we have
\(\forall i \in \lbrace d\rbrace .\;({\sf pastVec}_{\mathit {cl}})_{e}[i] \le ({\sf uniformVec}^{m}_{d})_{e}[i].\) 

\(\textsc {Case V}\) : \(e \in Q\) .
By line REF :REF ,
\(({\sf pastVec}_{\mathit {cl}})_{e}[d] \le ({\sf uniformVec}^{m}_{d})_{e}[d].\) 

\(\textsc {Case VI}\) : \(e \in A\) .
By line REF :REF ,
\(\forall i \in \lbrace d\rbrace .\;({\sf pastVec}_{\mathit {cl}})_{e}[i] \le ({\sf uniformVec}^{m}_{d})_{e}[i].\) 

Lemma 31 
Let \(\mathit {cl}\)  be a client and \(d \triangleq \textsl {cur\_dc}(\mathit {cl})\) .
At any time,
\(\forall i \in \lbrace d\rbrace .\;{\sf pastVec}_{\mathit {cl}}[i] \le {\sf uniformVec}^{m}_{d}[i]\) 
for some replica \(p^{m}_{d}\)  in data center \(d\) .

By a simple induction on the number of events that \(\mathit {cl}\)  issues
and Lemmas REF  and
REF .
Lemma 32 
Let \(\mathit {t}\)  be a transaction that originates at data center \(d\) .
At any time,
\(\forall i \in \lbrace d\rbrace .\;\textsl {snapshotVec}(\mathit {t})[i] \le {\sf uniformVec}^{m}_{d}[i]\) 
for some replica \(p^{m}_{d}\)  in data center \(d\) .

By line REF :REF 
and Lemma REF .
Lemma 33 (Property 3)  
For any replica \(p^{m}_{d}\)  in data center \(d\) ,
\(&\forall i \in \; \exists g \subseteq \; \Big (|g| \ge f + 1 \wedge d \in g\; \wedge \\&\; \big (\forall j \in g.\; \forall n \in \mathcal {P}.\;{\sf uniformVec}^{m}_{d}[i] \le {\sf knownVec}^{n}_{j}[i] \big )\Big ).\) 

Fix \(i \in .We proceed by induction on the length of the execution.In the following, we denote the value of\)knownVecmd\(, \)stableVecmd\(, \)uniformVecmd\(,\)stableMatrixmd\(, and \)pastVeccl\( (for some client \) cl\()after \) k\( steps of an execution by\)knownVecmd(k)\(, \)stableVecmd(k)\(, \)uniformVecmd(k)\(,\)stableMatrixmd(k)\(, and \)pastVeccl(k)\(, respectively.\begin{itemize}\item {\it Base Case.} k = 0. It holds trivially since{\sf uniformVec}^{m}_{d}(0)[i] = 0.\item {\it Induction Hypothesis.}Suppose that for any execution of length k,for any replica p^{m}_{d} in data center d,{\begin{@align*}{1}{-1}&\exists g \subseteq \; |g| \ge f + 1 \wedge d \in g\; \wedge \\&\quad \big (\forall j \in g.\; \forall 1 \le n \le N.\; \\&\qquad {\sf uniformVec}^{m}_{d}(k)[i] \le {\sf knownVec}^{n}_{j}(k)[i] \big ).\end{@align*}}\item {\it Induction Step.}Consider an execution of length k + 1.If the (k+1)-st step of this execution does not update{\sf uniformVec}^{m}_{d}[i] for any replica p^{m}_{d} in data center d,then by the induction hypothesis and Lemma~\ref {lemma:knownvc-nondecreasing},{\begin{@align*}{1}{-1}&\exists g \subseteq \; |g| \ge f + 1 \wedge d \in g\; \wedge \\&\quad \big (\forall j \in g.\; \forall 1 \le n \le N.\; \\&\qquad {\sf uniformVec}^{m}_{d}(k + 1)[i] = {\sf uniformVec}^{m}_{d}(k)[i] \\&\phantom{\qquad {\sf uniformVec}^{m}_{d}(k + 1)[i]}\le {\sf knownVec}^{n}_{j}(k)[i] \\&\phantom{\qquad {\sf uniformVec}^{m}_{d}(k + 1)[i]}\le {\sf knownVec}^{n}_{j}(k + 1)[i] \big ).\end{@align*}}Otherwise, we perform a case analysisaccording to how {\sf uniformVec}^{m}_{d}[i] is updated.\begin{itemize}\item \textsc {Case I}: {\sf uniformVec}^{m}_{d}[i] is updatedat line~\ref {alg:unistore-clock}:\ref {line:stablevc-uniformvc}.By line~\ref {alg:unistore-clock}:\ref {line:stablevc-g},{\begin{@align}{1}{-1}&\exists g^{\prime } \subseteq \; |g^{\prime }| \ge f + 1 \wedge d \in g^{\prime }\; \wedge  \\&\quad {\sf uniformVec}^{m}_{d}(k+1)[i] = \nonumber \\&\qquad \max \big \lbrace {\sf uniformVec}^{m}_{d}(k)[i], \nonumber \\&\qquad \qquad \;\; \min _{j \in g^{\prime }} {\sf stableMatrix}^{m}_{d}(k+1)[j][i]\big \rbrace . \nonumber \end{@align}}By the induction hypothesis and Lemma~\ref {lemma:knownvc-i-nondecreasing},{\begin{@align}{1}{-1}&\exists g^{\prime \prime } \subseteq \; |g^{\prime \prime }| \ge f + 1 \wedge d \in g^{\prime \prime }\; \wedge  \\&\quad \big (\forall j \in g^{\prime \prime }.\; \forall n \in \mathcal {P}. \nonumber \\&\qquad {\sf uniformVec}^{m}_{d}(k)[i] \le {\sf knownVec}^{n}_{j}(k)[i] \nonumber \\&\phantom{\qquad {\sf uniformVec}^{m}_{d}(k)[i] }\le {\sf knownVec}^{n}_{j}(k+1)[i]\big ). \nonumber \end{@align}}By Lemma~\ref {lemma:stablevc-nondecreasing},for the particular g^{\prime } \subseteq  in (\ref {eqn:g-prime}),{\begin{@align}{1}{-1}\forall j \in g^{\prime }.\; &{\sf stableMatrix}^{m}_{d}(k+1)[j][i] \\&\le {\sf stableVec}^{m}_{j}(k+1)[i].\nonumber \end{@align}}By Lemmas~\ref {lemma:stablevc-knownvc} and \ref {lemma:knownvc-i-nondecreasing},for any replica p^{m}_{j} in data center j,{\begin{@align}{1}{-1}&\forall n \in \mathcal {P}.\; {\sf stableVec}^{m}_{j}(k+1)[i]\\&\qquad \;\;\; \le {\sf knownVec}^{n}_{j}(k+1)[i]. \nonumber \end{@align}}Therefore, for the particular g^{\prime } \subseteq  in (\ref {eqn:g-prime}),{\begin{@align}{1}{-1}&\forall j^{\prime } \in g^{\prime }.\; \forall n \in \mathcal {P}.\;\min _{j \in g^{\prime }} {\sf stableMatrix}^{m}_{d}(k+1)[j][i]\nonumber \\&\qquad \qquad \qquad \;\; \le {\sf knownVec}^{n}_{j^{\prime }}(k+1)[i]. \end{@align}}By (\ref {eqn:g-prime}), (\ref {eqn:g-prime-prime}),and (\ref {eqn:j-prime}),we can either take g = g^{\prime } in (\ref {eqn:g-prime})or g = g^{\prime \prime } in (\ref {eqn:g-prime-prime}) such that{\begin{@align*}{1}{-1}&\forall j \in g.\; \forall n \in \mathcal {P}. \\&\;\; {\sf uniformVec}^{m}_{d}(k+1)[i] \le {\sf knownVec}^{n}_{j}(k+1)[i].\end{@align*}}Therefore,{\begin{@align*}{1}{-1}&\exists g \subseteq \; |g| \ge f + 1 \wedge d \in g\; \wedge \\&\; \big (\forall j \in g.\; \forall n \in \mathcal {P}.\; \\&\quad {\sf uniformVec}^{m}_{d}(k+1)[i] \le {\sf knownVec}^{n}_{j}(k+1)[i] \big ).\end{@align*}}\item \textsc {Case II}: {\sf uniformVec}^{m}_{d}[i](i \in \lbrace d\rbrace ) is updatedat line~\ref {alg:unistore-coord}:\ref {line:start-uniformvc}.Then there exists some client \mathit {cl} with d = \textsl {cur\_dc}(\mathit {cl}) such that{\begin{@align}{1}{-1}&{\sf uniformVec}^{m}_{d}(k+1)[i] =  \\&\quad \max \big \lbrace {\sf pastVec}_{\mathit {cl}}(k)[i], {\sf uniformVec}^{m}_{d}(k)[i]\big \rbrace .\nonumber \end{@align}}By the induction hypothesis and Lemma~\ref {lemma:knownvc-i-nondecreasing},{\begin{@align}{1}{-1}&\exists g^{\prime } \subseteq \; |g^{\prime }| \ge f + 1 \wedge d \in g^{\prime }\; \wedge  \\&\quad \big (\forall j \in g^{\prime }.\; \forall n \in \mathcal {P}. \nonumber \\&\qquad {\sf uniformVec}^{m}_{d}(k)[i] \le {\sf knownVec}^{n}_{j}(k)[i] \nonumber \\&\phantom{\qquad {\sf uniformVec}^{m}_{d}(k)[i] }\le {\sf knownVec}^{n}_{j}(k+1)[i]\big ). \nonumber \end{@align}}By Lemma~\ref {lemma:pastvc-uniformvc}, the induction hypothesis,and Lemma~\ref {lemma:knownvc-nondecreasing},{\begin{@align}{1}{-1}&\exists g^{\prime \prime } \subseteq \; |g^{\prime \prime }| \ge f + 1 \wedge d \in g^{\prime \prime }\; \wedge  \\&\quad \big (\forall j \in g^{\prime \prime }.\; \forall n \in \mathcal {P}. \nonumber \\&\qquad {\sf pastVec}_{\mathit {cl}}(k)[i] \le {\sf knownVec}^{n}_{j}(k+1)[i]. \nonumber \end{@align}}By (\ref {eqn:uniformvc-pastvc}), (\ref {eqn:g-prime-2}),and (\ref {eqn:g-prime-prime-2}),we can take g = g^{\prime } in (\ref {eqn:g-prime-2})or g = g^{\prime \prime } in (\ref {eqn:g-prime-prime-2}) such that{\begin{@align*}{1}{-1}&\forall j \in g.\; \forall n \in \mathcal {P}.\; \\&\;\; {\sf uniformVec}^{m}_{d}(k+1)[i] \le {\sf knownVec}^{n}_{j}(k+1)[i].\end{@align*}}Therefore,{\begin{@align*}{1}{-1}&\exists g \subseteq \; |g| \ge f + 1 \wedge d \in g\; \wedge \\&\; \big (\forall j \in g.\; \forall n \in \mathcal {P}.\; \\&\;\; {\sf uniformVec}^{m}_{d}(k+1)[i] \le {\sf knownVec}^{n}_{j}(k+1)[i] \big ).\end{@align*}}\item \textsc {Case III}: {\sf uniformVec}^{m}_{d}[i](i \in \lbrace d\rbrace ) is updatedat lines~\ref {alg:unistore-replica}:\ref {line:readkey-uniformvc}or \ref {alg:unistore-replica}:\ref {line:preparecausal-uniformvc}.Therefore, there exists some transaction \mathit {t}originating at data center d such that{\begin{@align}{1}{-1}&{\sf uniformVec}^{m}_{d}(k+1)[i] =  \\&\quad \max \big \lbrace \textsl {snapshotVec}(\mathit {t})[i], {\sf uniformVec}^{m}_{d}(k)[i]\big \rbrace .\nonumber \end{@align}}By the induction hypothesis and Lemma~\ref {lemma:knownvc-nondecreasing},{\begin{@align}{1}{-1}&\exists g^{\prime } \subseteq \; |g^{\prime }| \ge f + 1 \wedge d \in g^{\prime }\; \wedge  \\&\quad \big (\forall j \in g^{\prime }.\; \forall n \in \mathcal {P}. \nonumber \\&\qquad {\sf uniformVec}^{m}_{d}(k)[i] \le {\sf knownVec}^{n}_{j}(k)[i] \nonumber \\&\phantom{\qquad {\sf uniformVec}^{m}_{d}(k)[i] }\le {\sf knownVec}^{n}_{j}(k+1)[i]\big ). \nonumber \end{@align}}By Lemma~\ref {lemma:snapshotvc-uniformvc}, the induction hypothesis,and Lemma~\ref {lemma:knownvc-nondecreasing},{\begin{@align}{1}{-1}&\exists g^{\prime \prime } \subseteq \; |g^{\prime \prime }| \ge f + 1 \wedge d \in g^{\prime \prime }\; \wedge  \\&\quad \big (\forall j \in g^{\prime \prime }.\; \forall n \in \mathcal {P}. \nonumber \\&\qquad \textsl {snapshotVec}(\mathit {t})[i] \le {\sf knownVec}^{n}_{j}(k+1)[i]. \nonumber \end{@align}}By (\ref {eqn:uniformvc-snapshotvc}), (\ref {eqn:g-prime-3}),and (\ref {eqn:g-prime-prime-3}),we can take g = g^{\prime } in (\ref {eqn:g-prime-3})or g = g^{\prime \prime } in (\ref {eqn:g-prime-prime-3}) such that{\begin{@align*}{1}{-1}&\forall j \in g.\; \forall n \in \mathcal {P}.\; \\&\;\; {\sf uniformVec}^{m}_{d}(k+1)[i] \le {\sf knownVec}^{n}_{j}(k+1)[i].\end{@align*}}Therefore,{\begin{@align*}{1}{-1}&\exists g \subseteq \; |g| \ge f + 1 \wedge d \in g\; \wedge \\&\; \big (\forall j \in g.\; \forall n \in \mathcal {P}.\; \\&\quad {\sf uniformVec}^{m}_{d}(k+1)[i] \le {\sf knownVec}^{n}_{j}(k+1)[i] \big ).\end{@align*}}\end{itemize}\end{itemize}\)
Lemma 34 
For any replica \(p^{m}_{d}\)  in data center \(d\) ,
\(\forall i \in \; \forall n \in \mathcal {P}.\;{\sf uniformVec}^{m}_{d}[i] \le {\sf knownVec}^{n}_{d}[i].\) 

By Lemma REF .
Lemma 35 
Let \(\mathit {t}\in T_{\textsl {causal}}\)  be a causal transaction
that originates at data center \(i\) 
and accesses partition \(n\) .
If
\(\textsl {commitVec}(\mathit {t})[i] \le {\sf uniformVec}^{m}_{d}[i]\) 
for some replica \(p^{m}_{d}\)  in data center \(d\) ,
then
\(\textsl {log}(\mathit {t})[n] \subseteq {\sf opLog}^{n}_{d}.\) 

By Lemma REF ,
\({\sf uniformVec}^{m}_{d}[i] \le {\sf knownVec}^{n}_{d}[i].\) 
Therefore,
\(\textsl {commitVec}(\mathit {t})[i] \le {\sf knownVec}^{n}_{d}[i].\) 
By Lemma REF ,
\(\textsl {log}(\mathit {t})[n] \subseteq {\sf opLog}^{n}_{d}.\) 
Lemma 36 
For any replica \(p^{m}_{d}\)  in data center \(d\) ,
\({\sf uniformVec}^{m}_{d}[d] \le {\sf clock}^{m}_{d}.\) 

By Lemma REF ,
\({\sf uniformVec}^{m}_{d}[d] \le {\sf knownVec}^{m}_{d}[d].\) 
By Lemma REF ,
\({\sf knownVec}^{m}_{d}[d] \le {\sf clock}^{m}_{d}.\) 
Putting it together yields
\({\sf uniformVec}^{m}_{d}[d] \le {\sf clock}^{m}_{d}.\) 
Properties of \({\sf pastVec}\)
Lemma 37 
Let \(e \in S\)  be a start event of transaction \(\mathit {t}\) 
issued by client \(\mathit {cl}\) . Then
\(({\sf pastVec}_{\mathit {cl}})_{e} \le \textsl {snapshotVec}(\mathit {t}).\) 

By Definition REF  of \(\textsl {snapshotVec}(\mathit {t})\) 
and lines REF :REF –
REF :REF .
Lemma 38 
For \(i \in , \)pastVeccl[i]\( at any client \) cl\(is non-decreasing.\)
Note that \({\sf pastVec}_{\mathit {cl}}[i]\)  (\(i \in ) is updated onlyat lines~\ref {alg:unistore-client}:\ref {line:commitcausaltx-pastvc}or \ref {alg:unistore-client}:\ref {line:commitstrongtx-pastvc}when some transaction is committed.Therefore, the lemma holds due to Lemmas~\ref {lemma:snapshotvc-commitvc}and \ref {lemma:start-pastvc-snapshotvc}.\)
subsection2-.75.3Metadata for Strong Transactions
Lemma 39 
For any replica \(p^{m}_{d}\)  in any data center \(d\) ,
\({\sf knownVec}^{m}_{d}[\textsl {strong}]\)  is non-decreasing.

By REF 
and line REF :REF .
Lemma 40 
For any replica \(p^{m}_{d}\)  in any data center \(d\) ,
\({\sf stableVec}^{m}_{d}[\textsl {strong}]\)  is non-decreasing.

By Lemma REF ,
Assumption REF ,
and line REF :REF .
Lemma 41 (Property 6)  
Let \(\mathit {t}\in T_{\textsl {strong}}\)  be a strong transaction
that originates at data center \(i\) 
and accesses partition \(m\) .
If
\(\textsl {commitVec}(\mathit {t})[\textsl {strong}] \le {\sf knownVec}^{m}_{d}[\textsl {strong}]\) 
for some replica \(p^{m}_{d}\)  in data center \(d\) ,
then
\(\textsl {log}(\mathit {t})[m] \subseteq {\sf opLog}^{m}_{d}.\) 

Note that \({\sf knownVec}^{m}_{d}[\textsl {strong}]\)  can be updated
only at line REF :REF .
By REF ,
all committed strong transactions with strong timestamps
less than or equal to \({\sf knownVec}^{m}_{d}[\textsl {strong}]\) 
have been delivered to \(p^{m}_{d}\) .
By line REF :REF ,
\(\textsl {log}(\mathit {t})[m] \subseteq {\sf opLog}^{m}_{d}.\) 
subsection2-.75.3Timestamps
Definition 42 (Timestamps of Events)  
Let \(e \in C_{\textsl {causal}} \cup C_{\textsl {strong}} \cup Q\cup A\) 
be an event issued by client \(\mathit {cl}\) .
We define its timestamp \(\textsl {ts}(e)\)  as
\(\textsl {ts}(e) \triangleq ({\sf pastVec}_{\mathit {cl}})_{e}.\) 
Let \(e \in S\)  be a start event of transaction \(\mathit {t}\) .
Let \(d \triangleq \textsl {dc}(\mathit {t})\)  and \(m \triangleq \textsl {coord}(\mathit {t})\) .
We define its timestamp \(\textsl {ts}(e)\)  as
\(\textsl {ts}(e) \triangleq ({\sf snapVec}^{m}_{d})_{e}[\mathit {t}].\) 
See lines REF :REF ,
REF :REF ,
REF :REF ,
REF :REF ,
and REF :REF 
for start, commit_causal_tx, commit_strong_tx, cl_uniform_barrier,
and cl_attach events, respectively.

Definition 43 (Timestamps of Transactions)  
The timestamp \(\textsl {ts}(\mathit {t})\)  of a transaction \(\mathit {t}\) 
is that of its commit event, i.e.,
\(\forall \mathit {t}\in T.\;\textsl {ts}(\mathit {t}) \triangleq \textsl {ts}(\textsl {ct}(\mathit {t})).\) 

Lemma 44 
Let \(e \in S\)  be a start event.
Let \(d \triangleq \textsl {dc}(\textsl {tx}(e))\)  and \(m \triangleq \textsl {coord}(\textsl {tx}(e))\) .
Then
\((\forall i \in \; \textsl {ts}(e)[i] \ge ({\sf uniformVec}^{m}_{d})_{e}[i])\;\wedge \\\textsl {ts}(e)[\textsl {strong}] \ge ({\sf stableVec}^{m}_{d})_{e}[\textsl {strong}].\) 

By lines REF :REF ,
REF :REF ,
and REF :REF .
Lemma 45 
Let \(e \in R_{\textsc {ext}}\)  be an external read event.
Let \(d \triangleq \textsl {dc}(\textsl {tx}(e))\)  and \(m \triangleq \textsl {coord}(\textsl {tx}(e))\) .
Then
\(\textsl {ts}(\textsl {st}(e)) &= \textsl {snapshotVec}(\textsl {tx}(e)) \\&= \mathit {snapVec}_{(\textsc {get\_version}, e)} \\&= ({\sf snapVec}^{m}_{d})_{\textsl {st}(e)}[\textsl {tx}(e)].\) 

By Definition REF  of timestamps,
line REF :REF ,
and line REF :REF .
Lemma 46 
Let \(e \in R_{\textsc {ext}}\)  be an external read event
which reads from transaction \(\mathit {t}\) . Then
\(\textsl {ts}(\mathit {t}) \le \textsl {ts}(\textsl {st}(e)).\) 

By line REF :REF ,
\(\mathit {commitVec}_{(\textsc {get\_version}, e)} \le \mathit {snapVec}_{(\textsc {get\_version}, e)}.\) 
Since \(e\)  reads from \(\mathit {t}\) ,
\(\textsl {ts}(\mathit {t}) = \mathit {commitVec}_{(\textsc {get\_version}, e)}.\) 
By Lemma REF ,
\(\textsl {ts}(\textsl {st}(e)) = \mathit {snapVec}_{(\textsc {get\_version}, e)}.\) 
Therefore,
\(\textsl {ts}(\mathit {t}) \le \textsl {ts}(\textsl {st}(e)).\) 
Lemma 47
\(&\forall e \in (C_{\textsc {rw}}\cap C_{\textsl {causal}})\cup C_{\textsl {strong}}.\; \\&\quad \textsl {ts}(e) = \textsl {ts}(\textsl {tx}(e))= \textsl {commitVec}(\textsl {tx}(e)).\) 

By Definition REF  of timestamps
and Definition REF  of \(\textsl {commitVec}(\textsl {tx}(e))\) .
Lemma 48
\(\forall \mathit {t}\in T.\; \textsl {ts}(\mathit {t}) \ge \textsl {ts}(\textsl {st}(\mathit {t})).\) 

By Lemmas REF , REF ,
and REF .
subsection2-.75.3Session Order
Lemma 49
\(&\forall s_{1}, s_{2} \in X.\;s_{1} \xrightarrow{} s_{2} \Rightarrow  \big (\textsl {ts}(s_{1}) \le \textsl {ts}(s_{2}) \\&\quad \wedge \big (s_{2} \in T\Rightarrow  \textsl {ts}(s_{1})\le \textsl {ts}(\textsl {st}(s_{2}))\le \textsl {ts}(s_{2})\big )\big ).\) 

By Definitions REF  and REF  of timestamps
and Lemma REF ,
\(\textsl {ts}(s_{1}) \le \textsl {ts}(s_{2}),\) 
and
\(s_{2} \in T\Rightarrow  \textsl {ts}(s_{1}) \le \textsl {ts}(\textsl {st}(s_{2})).\) 
Besides, by Lemma REF ,
\(s_{2} \in T\Rightarrow  \textsl {ts}(\textsl {st}(s_{2})) \le \textsl {ts}(s_{2}).\) 
Therefore,
\(s_{2} \in T\Rightarrow  \textsl {ts}(s_{1}) \le \textsl {ts}(\textsl {st}(s_{2}))\le \textsl {ts}(s_{2}).\) 
subsection2-.75.3Lamport Clocks
Definition 50 (Lamport Clocks of Events)  
Let \(e \in C_{\textsl {causal}} \cup C_{\textsl {strong}} \cup Q\cup A\) 
be an event issued by client \(\mathit {cl}\) .
We define its Lamport clock \(\textsl {lclock}(e)\)  as
\(\textsl {lclock}(e) \triangleq ({\sf lc}_{\mathit {cl}})_{e}.\) 
See lines REF :REF ,
REF :REF ,
REF :REF ,
and REF :REF 
for commit_causal_tx, commit_strong_tx, cl_uniform_barrier, and cl_attach events, respectively.

Definition 51 (Lamport Clocks of Transactions)  
The Lamport clock \(\textsl {lclock}(\mathit {t})\)  of a transaction \(\mathit {t}\) 
is that of its commit event, i.e.,
\(\forall \mathit {t}\in T.\;\textsl {lclock}(\mathit {t}) \triangleq \textsl {lclock}(\textsl {ct}(\mathit {t})).\) 

Lemma 52 
Let \(e \in R_{\textsc {ext}}\)  be an external read event issued by client \(\mathit {cl}\) .
Then
\(({\sf lc}_{\mathit {cl}})_{e} < \textsl {lclock}(\textsl {tx}(e)).\) 

If \(\textsl {tx}(e)\)  is a causal transaction,
by line REF :REF ,
\(\textsl {lclock}(e) < \textsl {lclock}(\textsl {ct}(e)) = \textsl {lclock}(\textsl {tx}(e)).\) 
If \(\textsl {tx}(e)\)  is a strong transaction,
by line REF :REF 
and (REF ),
\(\textsl {lclock}(e) < \textsl {lclock}(\textsl {ct}(e)) = \textsl {lclock}(\textsl {tx}(e)).\) 
Definition 53 (Lamport Clock Order)  
The Lamport clock order \(\textsl {lc}\)  on \(X\) 
is the total order defined by their Lamport clocks,
with their client identifiers for tie-breaking.

Lemma 54
\(\textsl {so}\subseteq \textsl {lc}.\) 

By lines REF :REF ,
REF :REF ,
(REF ),
REF :REF ,
REF :REF ,
and REF :REF .
Lemma 55 
Let \(e \in R_{\textsc {ext}}\)  be an external read event
which reads from transaction \(\mathit {t}\) . Then
\(\mathit {t}\xrightarrow{} \textsl {tx}(e).\) 

Suppose that \(e\)  is issued by client \(\mathit {cl}\) .
By line REF :REF ,
\(\textsl {lclock}(\mathit {t}) \le ({\sf lc}_{\mathit {cl}})_{e}.\) 
By Lemma REF ,
\(({\sf lc}_{\mathit {cl}})_{e} < \textsl {lclock}(\textsl {tx}(e)).\) 
Therefore,
\(\textsl {lclock}(\mathit {t}) < \textsl {lclock}(\textsl {tx}(e)).\) 
By Definition REF  of \(\textsl {lc}\) ,
\(\mathit {t}\xrightarrow{} \textsl {tx}(e).\) 
subsection2-.75.3Visibility Relation
Definition 56 (Visibility Relation)
\(&\forall s_{1}, s_{2} \in X.\;s_{1} \xrightarrow{} s_{2} \Leftrightarrow \\&\quad \big ((s_{2} \in T\Rightarrow  \textsl {ts}(s_{1}) \le \textsl {ts}(\textsl {st}(s_{2}))) \\&\quad \quad \wedge (s_{2} \in Q\cup A\Rightarrow  \textsl {ts}(s_{1}) \le \textsl {ts}(s_{2}))\big )\wedge s_{1} \xrightarrow{} s_{2}.\) 

Theorem 57
\(A \models \textsc {ConflictOrdering}.\) 

We need to show that
\(\forall \mathit {t}_{1}, \mathit {t}_{2} \in T_{\textsl {strong}}.\;\mathit {t}_{1} \bowtie \mathit {t}_{2} \Rightarrow  \mathit {t}_{1} \xrightarrow{} \mathit {t}_{2} \vee \mathit {t}_{2} \xrightarrow{} \mathit {t}_{1}.\) 
Consider the history \(h\)  of TCS.
By Theorem REF ,
\(h \mid {\sf committed}(h)\)  has a legal permutation \(\pi \) .
Suppose that
\({\sf certify}(\textsl {tid}(\mathit {t}_{1}), \_, \_, \_, \_) \prec _{\pi }{\sf certify}(\textsl {tid}(\mathit {t}_{2}), \_, \_, \_, \_).\) 
Since \(\mathit {t}_{1} \bowtie \mathit {t}_{2}\)  and \(\mathit {t}_{2}\)  is committed,
by (REF ),
\(\textsl {commitVec}(\mathit {t}_{1}) \le \textsl {snapshotVec}(\mathit {t}_{2}).\) 
By Lemmas REF  and REF ,
\(\textsl {ts}(\mathit {t}_{1}) \le \textsl {ts}(\textsl {st}(\mathit {t}_{2})).\) 
On the other hand, by (REF ),
\(\textsl {lclock}(\mathit {t}_{1}) < \textsl {lclock}(\mathit {t}_{2}).\) 
By Definition REF  of \(\textsl {lc}\) ,
\(\mathit {t}_{1} \xrightarrow{} \mathit {t}_{2}.\) 
Therefore, by Definition REF  of \(\textsl {vis}\) ,
\(\mathit {t}_{1} \xrightarrow{} \mathit {t}_{2}.\) 
Lemma 58
\(\textsl {so}\subseteq \textsl {vis}.\) 

By Lemmas REF  and REF .
Lemma 59 
The visibility relation \(\textsl {vis}\)  is a partial order.

We need to show that

\(\textsl {vis}\)  is irreflexive.
This holds because \(\textsl {lc}\)  is irreflexive.

\(\textsl {vis}\)  is transitive.
Suppose that \(s_{1} \xrightarrow{} s_{2} \xrightarrow{} s_{3}\) .
By Definition REF  of \(\textsl {vis}\) ,
\(s_{1} \xrightarrow{} s_{2} \xrightarrow{} s_{3}.\) 
By Definition REF  of \(\textsl {lc}\) ,
\(s_{1} \xrightarrow{} s_{3}.\) 
Regarding timestamps,
we distinguish between the following four cases
and use Lemma REF .

\(s_{2} \in Q\cup A\wedge s_{3} \in Q\cup A\) .
\(\textsl {ts}(s_{1}) \le \textsl {ts}(s_{2})\le \textsl {ts}(s_{3}).\) 

\(s_{2} \in Q\cup A\wedge s_{3} \in T\) .
\(\textsl {ts}(s_{1}) \le \textsl {ts}(s_{2})\le \textsl {ts}(\textsl {st}(s_{3})).\) 

\(s_{2} \in T\wedge s_{3} \in Q\cup A\) .
\(\textsl {ts}(s_{1}) \le \textsl {ts}(\textsl {st}(s_{2}))\le \textsl {ts}(s_{2}) \le \textsl {ts}(s_{3}).\) 

\(s_{2} \in T\wedge s_{3} \in T\) .
\(\textsl {ts}(s_{1}) \le \textsl {ts}(\textsl {st}(s_{2}))\le \textsl {ts}(s_{2}) \le \textsl {ts}(\textsl {st}(s_{3})).\) 

By Definition REF  of \(\textsl {vis}\) ,
\(s_{1} \xrightarrow{} s_{3}.\) 

Theorem 60
\(A \models \textsc {CausalVisibility}.\) 

By Lemmas REF  and REF ,
\((\textsl {so}\cup \textsl {vis})^{+} = \textsl {vis}^{+} = \textsl {vis}.\) 
Lemma 61 (Property 5)  
For any two conflicting transactions \(\mathit {t}_{1}\)  and \(\mathit {t}_{2}\) ,
\(&\mathit {t}_{1} \xrightarrow{} \mathit {t}_{2} \Leftrightarrow \\&\quad \textsl {commitVec}(\mathit {t}_{1})[\textsl {strong}] < \textsl {commitVec}(\mathit {t}_{2})[\textsl {strong}].\) 

We first show that
\(&\mathit {t}_{1} \xrightarrow{} \mathit {t}_{2} \Rightarrow   \\&\quad \textsl {commitVec}(\mathit {t}_{1})[\textsl {strong}] < \textsl {commitVec}(\mathit {t}_{2})[\textsl {strong}].\nonumber \) 

Assume that \(\mathit {t}_{1} \xrightarrow{} \mathit {t}_{2}\) .
By Definition REF  of \(\textsl {vis}\) ,
\(\textsl {ts}(\mathit {t}_{1}) \le \textsl {ts}(\textsl {st}(\mathit {t}_{2})).\) 
By Lemmas REF  and REF ,
\(\textsl {commitVec}(\mathit {t}_{1}) \le \textsl {snapshotVec}(\mathit {t}_{2}).\) 
Therefore,
\(\textsl {commitVec}(\mathit {t}_{1})[\textsl {strong}] \le \textsl {snapshotVec}(\mathit {t}_{2})[\textsl {strong}].\) 
By (REF ),
\(\textsl {commitVec}(\mathit {t}_{2})[\textsl {strong}] > \textsl {snapshotVec}(\mathit {t}_{2})[\textsl {strong}].\) 
Putting it together yields
\(\textsl {commitVec}(\mathit {t}_{1})[\textsl {strong}] < \textsl {commitVec}(\mathit {t}_{2})[\textsl {strong}].\) 
Next we show that
\(&\mathit {t}_{1} \xrightarrow{} \mathit {t}_{2} \\&\quad \textsl {commitVec}(\mathit {t}_{1})[\textsl {strong}] < \textsl {commitVec}(\mathit {t}_{2})[\textsl {strong}].\) 

Assume that
\(\textsl {commitVec}(\mathit {t}_{1})[\textsl {strong}] < \textsl {commitVec}(\mathit {t}_{2})[\textsl {strong}].\) 

Since \(\mathit {t}_{1} \bowtie \mathit {t}_{2}\) , by Theorem REF ,
\(\mathit {t}_{1} \xrightarrow{} \mathit {t}_{2} \vee \mathit {t}_{2} \xrightarrow{} \mathit {t}_{1}.\) 
By (REF ) and (REF ),
\(\lnot (\mathit {t}_{2} \xrightarrow{} \mathit {t}_{1}).\) 
Therefore,
\(\mathit {t}_{1} \xrightarrow{} \mathit {t}_{2}.\) 
subsection2-.75.3Execution Order
Definition 62 (Execution Points)  
Let \(k\)  be a key.
The “execution point” \({\sf ep}(e, k)\)  of event
\(e \in (R_{\textsc {ext}}\cap R_{k}) \cup C_{k}\)  is defined as follows:

If \(e \in R_{\textsc {ext}}\cap R_{k}\) ,
then \({\sf ep}(e, k)\)  is at
line REF :REF ;

If \(e \in C_{k} \cap C_{\textsl {causal}}\) ,
then \({\sf ep}(e, k)\)  is at
line REF :REF 
for this particular key \(k\) ;

If \(e \in C_{k} \cap C_{\textsl {strong}}\) 
then \({\sf ep}(e, k)\)  is at
line REF :REF 
for delivery of the update of \(\textsl {tx}(e)\)  on this particular key \(k\) .
Note that deliver is asynchronous with the commit event \(e\) .


Definition 63 (Per-key Execution Order)  
Let \(k\)  be a key.
Suppose that \(\lbrace e_{1}, e_{2}\rbrace  \subseteq (R_{\textsc {ext}}\cap R_{k}) \cup C_{k}\) .
Event \(e_1\)  is executed before event \(e_2\) , denoted \(e_1 \xrightarrow{} e_2\) ,
if \({\sf ep}(e_{1}, k)\)  is executed before \({\sf ep}(e_{2}, k)\)  in real time.

Lemma 64 
Let \(k \in \mathit {Key}\)  be a key, \(\mathit {t}\in T_{k}\)  be a transaction,
and \(e \in R_{\textsc {ext}}\cap R_{k}\)  be an external read event.
Suppose that \(d \triangleq \textsl {dc}(\mathit {t}) = \textsl {dc}(\textsl {tx}(e))\) .
Then
\(\mathit {t}\xrightarrow{} \textsl {tx}(e) \Rightarrow  \textsl {ct}(\mathit {t}) \xrightarrow{} e.\) 

By Definition REF  of \(\textsl {vis}\) ,
\(\textsl {ts}(\mathit {t}) \le \textsl {ts}(\textsl {st}(e)).\) 
Since \(e \in R_{\textsc {ext}}\) , by Lemma REF ,
\(\textsl {ts}(\mathit {t}) \le \mathit {snapVec}_{(\textsc {get\_version}, e)}.\) 
In the following, we distinguish between two cases
according to whether \(\mathit {t}\in T_{\textsl {causal}}\) 
or \(\mathit {t}\in T_{\textsl {strong}}\) .
Let \(m \triangleq \mathtt {partition}(k)\) .

\(\textsc {Case I}\) : \(\mathit {t}\in T_{\textsl {causal}}\) .
By Lemma REF ,
\(\textsl {ts}(\mathit {t}) = \textsl {commitVec}(\mathit {t}) \le \mathit {snapVec}_{(\textsc {get\_version}, e)}.\) 
Therefore, after line REF :REF 
for \(e\) ,
\(({\sf knownVec}^{m}_{d})_{e}[d]&\ge \mathit {snapVec}_{(\textsc {get\_version}, e)}[d] \\&\ge \textsl {commitVec}(\mathit {t})[d].\) 

By Lemma REF ,
commit of Algorithm REF 
for \(\textsl {ws}(\mathit {t})[m] \ni \langle k, \_ \rangle \) 
finishes before \(e\)  starts at replica \(p^{m}_{d}\) .
By Definition REF  of \(\textsl {eo}_{k}\) ,
\(\textsl {ct}(\mathit {t}) \xrightarrow{} e.\) 

\(\textsc {Case II}\) : \(\mathit {t}\in T_{\textsl {strong}}\) .
By Lemma REF ,
\(\textsl {ts}(\mathit {t}) = \textsl {commitVec}(\mathit {t}) \le \mathit {snapVec}_{(\textsc {get\_version}, e)}.\) 
Therefore, after line REF :REF 
for \(e\) ,
\(({\sf knownVec}^{m}_{d})_{e}[\textsl {strong}]&\ge \mathit {snapVec}_{(\textsc {get\_version}, e)}[\textsl {strong}] \\&\ge \textsl {commitVec}(\mathit {t})[\textsl {strong}].\) 

By Lemma REF ,
deliver of Algorithm REF 
for \(\textsl {ws}(\mathit {t})[m] \ni \langle k, \_ \rangle \) 
finishes before \(e\)  starts at replica \(p^{m}_{d}\) .
By Definition REF  of \(\textsl {eo}_{k}\) ,
\(\textsl {ct}(\mathit {t}) \xrightarrow{} e.\) 

subsection2-.75.3Arbitration Relation
Definition 65 (Arbitration Relation)  
We define the arbitration relation \(\textsl {ar}\)  on \(X\) 
as the Lamport clock order between them, i.e.,
\(\textsl {ar}= \textsl {lc}.\) 

Theorem 66
\(A \models \textsc {CausalArbitration}.\) 

By Definition REF  of \(\textsl {vis}\)  and Definition REF  of \(\textsl {ar}\) ,
\(\textsl {vis}\subseteq \textsl {lc}= \textsl {ar}.\) 
subsection2-.75.3Return Values
It is straightforward to show that \(\textsc {IntRVal}\)  holds
for internal read events.
Theorem 67
\(A \models \textsc {IntRVal}.\) 

Let \(e \in R_{\textsc {int}}\cap R_{k}\)  be an internal read event.
The transaction \(\textsl {tx}(e)\)  contains update events on \(k\) .
By line REF :REF ,
\(e\)  reads from the last update event on \(k\) 
preceding \(e\)  in \(\textsl {tx}(e)\) .
Now let \(e\)  be an external read event.
For notational convenience,
we define \(V_{e}\)  to be the set of update transactions on \(k\) 
that are visible to \(\textsl {tx}(e)\) ,
and \(S_{e}\)  the set of update transactions on \(k\)  that are safe to read
at line REF :REF .
By Assumption REF ,
REF , and
REF ,
all transactions in \(S_{e}\)  are committed.
Formally,
Definition 68 (Visibility Set) 

Let \(e \in R_{\textsc {ext}}\cap R_{k}\)  be an external read event on key \(k\) .
\(V_{e} \triangleq \textsl {vis}^{-1}(\textsl {tx}(e)) \cap T_{k}.\) 

Definition 69 (Safe Set) 

Let \(e \in R_{\textsc {ext}}\cap R_{k}\)  be an external read event on key \(k\) .
Suppose that \(e\)  is issued to replica \(p^{m}_{d}\)  in data center \(d\) .
\(S_{e} \triangleq \lbrace \mathit {t}\in T_{k}:&\; \textsl {ts}(\mathit {t}) \le \mathit {snapVec}_{(\textsc {get\_version}, e)}\; \wedge \\&\; \textsl {log}[\mathit {t}][k] \in ({\sf opLog}^{m}_{d})_{e}[k]\rbrace .\) 

Lemma 70 
Let \(e \in R_{\textsc {ext}}\cap R_{k}\)  be an external read event on key \(k\) .
Suppose that \(e\)  is issued to replica \(p^{m}_{d}\)  in data center \(d\) .
When \(e\)  returns at \(p^{m}_{d}\) 
(line REF :REF ),
we have
\(V_{e} \subseteq S_{e}.\) 

For each \(\mathit {t}\in V_{e}\) ,
we need to show that \(\mathit {t}\in S_{e}\) .
That is,
\(\textsl {ts}(\mathit {t}) \le \mathit {snapVec}_{(\textsc {get\_version}, e)}\) 
and
\(\textsl {log}[\mathit {t}][k] \in ({\sf opLog}^{m}_{d})_{e}[k].\) 
We first show that (REF ) holds.
Since \(\mathit {t}\in V_{e}\) ,
\(\mathit {t}\xrightarrow{} \textsl {tx}(e).\) 
By Definition REF  of \(\textsl {vis}\) ,
\(\textsl {ts}(\mathit {t}) \le \textsl {ts}(\textsl {st}(e)).\) 
By Lemma REF ,
\(\textsl {ts}(\mathit {t}) \le \mathit {snapVec}_{(\textsc {get\_version}, e)}.\) 
To show that (REF ) holds,
we perform a case analysis according to
whether \(\mathit {t}\)  is a local transaction in data center \(d\) 
or a remote one in data center \(i \ne d\) .

\(\textsc {Case I}\) : \(\mathit {t}\)  is a local transaction in data center \(d\) .
Since \(\mathit {t}\xrightarrow{} \textsl {tx}(e)\) ,
by Lemma REF ,
\(\textsl {ct}(\mathit {t}) \xrightarrow{} e.\) 
Therefore,
\(\textsl {log}[\mathit {t}][k] \in ({\sf opLog}^{m}_{d})_{e}[k].\) 

\(\textsc {Case II}\) : \(\mathit {t}\)  is a remote transaction
in data center \(i \ne d\) .
We distinguish between two cases
according to whether \(\mathit {t}\in T_{\textsl {causal}}\)  or \(\mathit {t}\in T_{\textsl {strong}}\) .

\(\textsc {Case I}\) : \(\mathit {t}\in T_{\textsl {causal}}\) .
Since \(i \ne d\) ,
by line REF :REF ,
\(\mathit {snapVec}_{(\textsc {get\_version}, e)}[i] \le ({\sf uniformVec}^{m}_{d})_{e}[i].\) 
By (REF ),
\(\textsl {ts}(\mathit {t})[i] \le ({\sf uniformVec}^{m}_{d})_{e}[i].\) 
By Lemma REF ,
\(\textsl {log}[\mathit {t}][k] \in ({\sf opLog}^{m}_{d})_{e}[k].\) 

\(\textsc {Case II}\) : \(\mathit {t}\in T_{\textsl {strong}}\) .
By line REF :REF ,
\(&\mathit {snapVec}_{(\textsc {get\_version}, e)}[\textsl {strong}] \\&\qquad \le ({\sf knownVec}^{m}_{d})_{e}[\textsl {strong}].\) 

By (REF ),
\(\textsl {ts}(\mathit {t})[\textsl {strong}] \le ({\sf knownVec}^{m}_{d})_{e}[\textsl {strong}].\) 
By Lemma REF ,
\(\textsl {log}[\mathit {t}][k] \in ({\sf opLog}^{m}_{d})_{e}[k].\) 


Theorem 71
\(A \models \textsc {ExtRVal}.\) 

Let \(e \in R_{\textsc {ext}}\cap R_{k}\) 
be an external read event on key \(k\) .
Suppose that \(e\)  reads from transaction \(\mathit {t}\)  in \(S_{e}\) .
Since all transactions in \(S_{e}\)  are committed,
\(\mathit {t}\)  is committed.
By Lemma REF ,
\(\textsl {ts}(\mathit {t}) \le \textsl {ts}(\textsl {st}(e)).\) 
By Lemma REF ,
\(\mathit {t}\xrightarrow{} \textsl {tx}(e).\) 
By Definition REF  of \(\textsl {vis}\) ,
\(\mathit {t}\xrightarrow{} \textsl {tx}(e).\) 
By Definition REF  of \(V_{e}\) ,
\(\mathit {t}\in V_{e}.\) 
Both \(V_{e}\)  and \(S_{e}\) 
are totally ordered by \(\textsl {lc}\) .
Since \(\mathit {t}\)  is the latest one in \(S_{e}\) 
and \(V_{e} \subseteq S_{e}\) 
(Theorem REF ),
\(\mathit {t}\)  is also the latest one in \(V_{e}\) .
Thus, \(e\)  reads from \(\mathit {t}\)  in \(V_{e}\) .
That is, \(e\)  reads from the update event
\(\textsl {ud}(\mathit {t}, k)\)  of \(V_{e}\) .
Theorem 72
\(A \models \textsc {RVal}.\) 

By Theorems REF  and REF .
subsection2-.75.3Uniformity
Uniformity of Causal Transactions Originating at Correct Data Centers
Lemma 73 
For any replica \(p^{m}_{d}\)  in any correct data center \(d \in ,\)knownVecmd[d]\( grows without bound.\)
Since data center \(d\)  is correct, by Assumption REF ,
propagate_local_txs of Algorithm REF 
will be executed infinitely often.

\(\textsc {Case I}\) :
Line REF :REF 
is executed infinitely often.
By Assumption REF ,
\({\sf knownVec}^{m}_{d}[d]\)  grows without bound.

\(\textsc {Case II}\) :
Line REF :REF 
is executed infinitely often.
That is, it is infinitely often that
\({\sf preparedCausal}^{m}_{d} \ne \varnothing .\) 
By Assumption REF ,
causal transactions in \({\sf preparedCausal}^{m}_{d}\) 
will eventually be committed and removed from \({\sf preparedCausal}^{m}_{d}\) 
(line REF :REF ).
Thus, it is infinitely often that new causal transactions
are prepared and added into \({\sf preparedCausal}^{m}_{d}\) 
(line REF :REF )
with larger and larger prepare timestamps
(line REF :REF ).
Therefore,
\(\min \lbrace \mathit {ts}\mid \langle \_, \_, \mathit {ts}\rangle \in {\sf preparedCausal}^{m}_{d}\rbrace \) 
and
\(&{\sf knownVec}^{m}_{d}[d] \\&\quad = \min \lbrace \mathit {ts}\mid \langle \_, \_, \mathit {ts}\rangle \in {\sf preparedCausal}^{m}_{d}\rbrace  - 1\) 

grow without bound.

Lemma 74 
Let \(p^{m}_{d}\)  be a replica in a correct data center \(d \in .If for some \) j  and some value \(x \in \mathbb {N}\)
\({\sf knownVec}^{m}_{d}[j] \ge x,\) 
then eventually
\(\forall c\in \; {\sf knownVec}^{m}_{c}[j] \ge x.\) 

Since data center \(d\)  is correct, by Assumption REF ,
for each other data center \(i \ne d\) , replica \(p^{m}_{d}\)  will keep

replicating to data center \(i\)  the write sets
\(\langle \_, \mathit {wbuff}, \mathit {commitVec}, \_ \rangle \in {\sf committedCausal}^{m}_{d}[j]\) 
that have not been received by \(i\)  from the perspective of \(d\) 
(\(\mathit {commitVec}[d] \le {\sf knownVec}^{m}_{d}[d]\) 
at line REF :REF 
and \(\mathit {commitVec}[j] > {\sf globalMatrix}^{m}_{d}[i][j]\)  at
line REF :REF );

or sending heartbeats with up-to-date
\({\sf knownVec}^{m}_{d}[j]\)  to data center \(i\) 
(lines REF :REF 
and REF :REF ).

By Assumption REF ,
\({\sf knownVec}^{m}_{c}[j]\)  at replica \(p^{m}_{c}\)  of
each correct data center \(c\in  will eventually be updated(lines~\ref {alg:unistore-replication}:\ref {line:replicate-knownvc}and \ref {alg:unistore-replication}:\ref {line:heartbeat-knownvc})such that\)\({\sf knownVec}^{m}_{c}[j] \ge {\sf knownVec}^{m}_{d}[j] \ge x.\)\(\)
Lemma 75 
Let \(d \in  be a correct data center.For any replica \) pmc\(in any correct data center \) c,
\({\sf uniformVec}^{m}_{c}[d]\)  grows without bound.

By Lemmas REF  and REF ,
for any replica \(p^{m}_{c}\) 
in any correct data center \(c\in ,\)knownVecmc[d]\( grows without bound.By lines~\ref {alg:unistore-clock}:\ref {line:bcast-call-knownvclocal}and \ref {alg:unistore-clock}:\ref {line:knownvclocal-stablevc-causal},for any replica \) pmc\(in any correct data center \) c,
\({\sf stableVec}^{m}_{c}[d]\)  grows without bound.
By line REF :,
Assumptions REF  and REF ,
and lines REF :REF –
REF :REF ,
for any replica \(p^{m}_{c}\) 
in any correct data center \(c\in ,\)uniformVecmc[d]\( grows without bound.\)
Lemma 76 (Property 4)  
Let \(p^{m}_{d}\)  be any replica in any data center \(d\) .
For any time \(\tau \) , there exists some time \(\tau ^{\prime }\)  such that
\(&\forall i \in \; \forall c\in \; \forall n \in \mathcal {P}. \\&\quad {\sf uniformVec}^{n}_{c}(\tau ^{\prime })[i] \ge {\sf uniformVec}^{m}_{d}(\tau )[i].\) 

By Lemma REF ,
Assumption REF , and the fact that at most
\(f\)  data centers may fail,
\(&\forall i \in \; \exists c\in \; \forall n \in \mathcal {P}. \\&\quad {\sf uniformVec}^{m}_{d}(\tau )[i] \le {\sf knownVec}^{n}_{c}(\tau )[i].\) 

By Lemma REF ,
there exists some time \(\tau ^{\prime \prime }\)  such that
\(&\forall i \in \; \forall c\in \; \forall n \in \mathcal {P}. \\&\quad {\sf uniformVec}^{m}_{d}(\tau )[i] \le {\sf knownVec}^{n}_{c}(\tau ^{\prime \prime })[i].\) 

By Algorithm REF  and Assumption REF ,
there exists some time \(\tau ^{\prime }\)  such that
\(&\forall i \in \; \forall c\in \; \forall n \le \mathcal {P}. \\&\quad {\sf uniformVec}^{n}_{c}(\tau ^{\prime })[i] \ge {\sf uniformVec}^{m}_{d}(\tau )[i].\) 
Lemma 77 
Let \(d \in  be a correct data centerand \) tTcausal\( be a causal transactionthat originates at \) d\(.Then for any replica \) pmc\(in any correct data center \) c, eventually
\(\forall i \in \; \textsl {ts}(\mathit {t})[i] \le {\sf uniformVec}^{m}_{c}[i].\) 

Since \(d\)  is correct, by Lemma REF ,
there exists some time \(\tau ^{\prime }\)  such that
\(\textsl {ts}(\mathit {t})[d] \le {\sf uniformVec}^{m}_{c}(\tau ^{\prime })[d].\) 
On the other hand,
by Definition REF  of timestamps
and Lemma REF 
(let \(n \triangleq \textsl {coord}(\mathit {t})\)  and \(cl \triangleq \textsl {client}(\mathit {t})\) ),
\(\forall i \in \lbrace d\rbrace .\;\textsl {ts}(\mathit {t})[i] &= ({\sf pastVec}_{\mathit {cl}})_{\textsl {ct}(\mathit {t})}[i] \\&\le ({\sf uniformVec}^{n}_{d})_{\textsl {ct}(\mathit {t})}[i].\) 

By Lemma REF ,
there exists some time \(\tau ^{\prime \prime }\)  such that
\(\forall i \in \lbrace d\rbrace .\;\textsl {ts}(\mathit {t})[i] \le ({\sf uniformVec}^{m}_{c})(\tau ^{\prime \prime })[i].\) 
Let
\(\tau \triangleq \max \lbrace \tau ^{\prime }, \tau ^{\prime \prime }\rbrace .\) 
By Lemma REF ,
\(\forall i \in \; \textsl {ts}(\mathit {t})[i] \le {\sf uniformVec}^{m}_{c}(\tau )[i].\) 
Uniformity of Causal Transactions Visible to cl_uniform_barrier events
Lemma 78 
Let \(\mathit {t}\in T_{\textsl {causal}}\)  be a causal transaction
and \(q\in Q\)  be a cl_uniform_barrier event.
If \(\mathit {t}\xrightarrow{} q\) ,
then for any replica \(p^{m}_{c}\) 
in any correct data center \(c\in , eventually\)\(\forall i \in \; \textsl {ts}(\mathit {t})[i] \le {\sf uniformVec}^{m}_{c}[i].\)\(\)
Since \(\mathit {t}\xrightarrow{} q\) , by Definition REF  of \(\textsl {vis}\) ,
\(\textsl {ts}(\mathit {t}) \le \textsl {ts}(q).\) 
Suppose that \(q\)  is issued by client \(\mathit {cl}\) 
to replica \(p^{n}_{d}\)  in data center \(d\) 
and is returned at time \(\tau _{q}\) .
By Definition REF  of timestamps
and Lemma REF ,
\(\textsl {ts}(\mathit {t})[d] \le \textsl {ts}(q)[d] \le ({\sf uniformVec}^{n}_{d})_{q}[d].\) 
By Lemma REF ,
there exists some time \(\tau ^{\prime }\)  such that
\(\textsl {ts}(\mathit {t})[d] \le ({\sf uniformVec}^{m}_{c})(\tau ^{\prime })[d].\) 
On the other hand, by Definition REF  of timestamps
and Lemma REF ,
\(\forall i \in \lbrace d\rbrace .\;\textsl {ts}(\mathit {t})[i] &\le \textsl {ts}(q)[i] \\&= ({\sf pastVec}_{\mathit {cl}})_{q}[i] \\&\le {\sf uniformVec}^{l}_{d}(\tau _{q})[i]\) 

for some replica \(p^{l}_{d}\)  in data center \(d\) .
By Lemma REF ,
there exists some time \(\tau ^{\prime \prime }\)  such that
\(\forall i \in \lbrace d\rbrace .\;\textsl {ts}(\mathit {t})[i] \le ({\sf uniformVec}^{m}_{c})(\tau ^{\prime \prime })[i].\) 
Let
\(\tau \triangleq \max \lbrace \tau ^{\prime }, \tau ^{\prime \prime }\rbrace .\) 
By Lemma REF ,
\(\forall i \in \; \textsl {ts}(\mathit {t})[i] \le {\sf uniformVec}^{m}_{c}(\tau )[i].\) 
Uniformity of Strong Transactions
Lemma 79 
For any replica \(p^{m}_{c}\) 
in any correct data center \(c\in ,\)knownVecmc[strong]\( grows without bound.\)
By Assumption REF 
and Theorem REF ,
replica \(p^{m}_{c}\)  will either deliver committed strong transactions
infinitely often (deliver of Algorithm REF )
or submit dummy strong transactions infinitely often
(heartbeat_strong of Algorithm REF ).
Thus, \({\sf knownVec}^{m}_{c}[\textsl {strong}]\)  grows without bound.
Lemma 80 
Let \(\mathit {t}\in T\)  be a transaction.
Then for any replica \(p^{m}_{c}\) 
in any correct data center \(c\in , eventually\)\(\textsl {ts}(\mathit {t})[\textsl {strong}] \le {\sf stableVec}^{m}_{c}[\textsl {strong}].\)\(\)
By Lemma REF 
and lines REF :REF 
and REF :REF ,
\({\sf stableVec}^{m}_{c}[\textsl {strong}]\)  grows without bound.
Therefore, there exists some time \(\tau \)  such that
\(\textsl {ts}(\mathit {t})[\textsl {strong}] \le {\sf stableVec}^{m}_{c}(\tau )[\textsl {strong}].\) 
Lemma 81 
Let \(\mathit {t}\in T_{\textsl {strong}}\)  be a strong transaction.
Then for any replica \(p^{m}_{c}\) 
in any correct data center \(c\in , eventually\)\(\forall i \in \; \textsl {ts}(\mathit {t})[i] \le {\sf uniformVec}^{m}_{c}[i].\)\(\)
Let \(d \triangleq \textsl {dc}(\mathit {t})\) ,
\(n \triangleq \textsl {coord}(\mathit {t})\) , and \(cl \triangleq \textsl {client}(\mathit {t})\) .
By Definition REF  of timestamps,
\(\textsl {ts}(\mathit {t}) = ({\sf pastVec}_{\mathit {cl}})_{\textsl {ct}(\mathit {t})}.\) 
On the one hand, by Lemma REF ,
\(\forall i \in \lbrace d\rbrace .\;\textsl {ts}(\mathit {t})[i] &= ({\sf pastVec}_{\mathit {cl}})_{\textsl {ct}(\mathit {t})}[i] \\&\le ({\sf uniformVec}^{n}_{d})_{\textsl {ct}(\mathit {t})}[i].\) 

By Lemma REF ,
there exists some time \(\tau ^{\prime }\)  such that
\(\forall i \in \lbrace d\rbrace .\;\textsl {ts}(\mathit {t})[i] \le ({\sf uniformVec}^{m}_{c})(\tau ^{\prime })[i].\) 
On the other hand, by Lemma REF ,
\(\textsl {ts}(\mathit {t})[d] = \textsl {commitVec}(\mathit {t})[d].\) 
By (REF ),
\(\textsl {commitVec}(\mathit {t})[d] = \textsl {snapshotVec}(\mathit {t})[d].\) 
By lines REF :REF 
and REF :REF ,
\(\textsl {snapshotVec}(\mathit {t})[d] \le ({\sf uniformVec}^{n}_{d})_{\textsl {ct}(\mathit {t})}[d].\) 
Putting it together yields,
\(\textsl {ts}(\mathit {t})[d] \le ({\sf uniformVec}^{n}_{d})_{\textsl {ct}(\mathit {t})}[d].\) 
By Lemma REF ,
there exists some time \(\tau ^{\prime \prime }\)  such that
\(\textsl {ts}(\mathit {t})[d] \le ({\sf uniformVec}^{m}_{c})(\tau ^{\prime \prime })[d].\) 
Let
\(\tau \triangleq \max \lbrace \tau ^{\prime }, \tau ^{\prime \prime }\rbrace .\) 
By Lemma REF ,
\(\forall i \in \; \textsl {ts}(\mathit {t})[i] \le {\sf uniformVec}^{m}_{c}(\tau )[i].\) 
subsection2-.75.3Eventual Visibility
Theorem 82
\(A \models \textsc {EventualVisibility}.\) 

Consider a transaction \(\mathit {t}\in T\)  such that
\(\textsl {dc}(\mathit {t}) \in (\exists q\in Q.\; \mathit {t}\xrightarrow{} q)\vee \mathit {t}\in T_{\textsl {strong}}.\) 

By Lemma REF ,
it suffices to show that for any client \(\mathit {cl}\) ,
\(\Big \vert T|_{\mathit {cl}} \Big \vert = \infty \Rightarrow  \exists \mathit {t}^{\prime } \in T|_{\mathit {cl}}.\; \mathit {t}\xrightarrow{} \mathit {t}^{\prime }.\) 
By Lemmas REF ,
REF , REF ,
and REF ,
there exists some time \(\tau \)  such that
\(&\forall c\in \; \forall n \in \mathcal {P}. \nonumber \\&\quad (\forall i \in \; \textsl {ts}(\mathit {t})[i]\le {\sf uniformVec}^{n}_{c}(\tau )[i])\;\wedge \nonumber \\&\quad \;\; \textsl {ts}(\mathit {t})[\textsl {strong}]\le {\sf stableVec}^{n}_{c}(\tau )[\textsl {strong}].\) 

Since \(\Big \vert T|_{\mathit {cl}} \Big \vert = \infty \) ,
there exists some correct data center \(d \in to which \) cl\( issues an infinite number of transactions.Let \) t' T\( be the first transactionissued by client \) cl\( to data center \) d\(which starts after time \)\( such that\)\(\textsl {lclock}(\mathit {t}) < \textsl {lclock}(\mathit {t}^{\prime }).\)\(Thus, by Definition~\ref {def:lco} of \)lc\(,\)\(\mathit {t}\xrightarrow{} \mathit {t}^{\prime }.\)\(Let \) m coord(t')\(.Since \) d\( is correct, by (\ref {eqn:time-t}),{\begin{@align*}{1}{-1}&(\forall i \in \; \textsl {ts}(\mathit {t})[i] \le {\sf uniformVec}^{m}_{d}(\tau )[i])\;\wedge \\&\;\;\textsl {ts}(\mathit {t})[\textsl {strong}] \le {\sf stableVec}^{m}_{d}(\tau )[\textsl {strong}].\end{@align*}}By Lemma~\ref {lemma:uniformvc-nondecreasing},\)\(\forall i \in \;{\sf uniformVec}^{m}_{d}(\tau )[i] \le ({\sf uniformVec}^{m}_{d})_{\textsl {st}(\mathit {t}^{\prime })}[i].\)\(By Lemma~\ref {lemma:stablevc-strong-nondecreasing},\)\({\sf stableVec}^{m}_{d}(\tau )[\textsl {strong}] \le ({\sf stableVec}^{m}_{d})_{\textsl {st}(\mathit {t}^{\prime })}[\textsl {strong}].\)\(By Lemma~\ref {lemma:ts-start},\begin{gather*}(\forall i \in \; ({\sf uniformVec}^{m}_{d})_{\textsl {st}(\mathit {t}^{\prime })}[i]\le \textsl {ts}(\textsl {st}(\mathit {t}^{\prime }))[i])\;\wedge \\({\sf stableVec}^{m}_{d})_{\textsl {st}(\mathit {t}^{\prime })}[\textsl {strong}]\le \textsl {ts}(\textsl {st}(\mathit {t}^{\prime }))[\textsl {strong}].\end{gather*}Putting it together yields\)\(\textsl {ts}(\mathit {t}) \le \textsl {ts}(\textsl {st}(\mathit {t}^{\prime })).\)\(By Definition~\ref {def:vis-tx} of \)vis\(,\)\(\mathit {t}\xrightarrow{} \mathit {t}^{\prime }.\)\(\)
subsection2-.75.3UniStore Correctness
Theorem 83
\(\textsc {UniStore}\models \textsc {PoR}.\) 

By Theorems REF , REF ,
REF , REF , and REF .
subsection2-.75.3UniStore Liveness
Lemma 84 
Each client migration cl_attach to a correct data center
will eventually terminate, provided that the client managed to
complete its cl_uniform_barrier call at its original data center
just before cl_attach.

Suppose that client \(\mathit {cl}\)  in its current data center \(d \triangleq \textsl {cur\_dc}(\mathit {cl})\) 
issues a cl_attach event \(a\) 
to replica \(p^{m}_{c}\)  in correct data center \(c\in .\) Let \(e \in C\)  be the last commit event
issued by client \(\mathit {cl}\)  before \(a\) .
If \(e\)  does not exist, then
\(\forall i \in \; {\sf pastVec}_{\mathit {cl}}[i] = 0.\) 
Therefore, the wait condition
\(\forall i \in \lbrace c\rbrace .\; {\sf uniformVec}^{m}_{c}[i] \ge 0\) 
at line REF :REF 
at replica \(p^{m}_{c}\)  will eventually hold.
Thus, the cl_attach event \(a\)  eventually terminates.
Otherwise, suppose that \(e\)  is issued to replica \(p^{n^{\prime }}_{d^{\prime }}\) 
in data center \(d^{\prime }\) .
By Lemma REF ,
\(\forall i \in \lbrace d^{\prime }\rbrace .\;({\sf uniformVec}^{n^{\prime }}_{d^{\prime }})_{e}[i] \ge ({\sf pastVec}_{\mathit {cl}})_{e}[i].\) 

Note that it is possible that \(d^{\prime } \ne d\) ,
since there may exist other cl_attach events between \(e\)  and \(a\) .
Therefore, we distinguish between the following two cases:

Case I: \(d^{\prime } = d\) . By (REF ),
\(\forall i \in \lbrace d\rbrace .\;({\sf uniformVec}^{n^{\prime }}_{d})_{e}[i] \ge ({\sf pastVec}_{\mathit {cl}})_{e}[i].\) 

Case II: \(d^{\prime } \ne d\) .
Consider the last cl_attach event, denoted \(a^{\prime }\) , before \(a\) .
Suppose that \(a^{\prime }\)  is issued to replica \(p^{n}_{d}\)  in data center \(d\) .
By Lemma REF , when \(a^{\prime }\)  terminates,
\(\forall i \in \lbrace d\rbrace .\;&({\sf uniformVec}^{n}_{d})_{a^{\prime }}[i] \ge ({\sf pastVec}_{\mathit {cl}})_{a^{\prime }}[i] \nonumber \\&\quad = ({\sf pastVec}_{\mathit {cl}})_{e}[i].\) 

Let \(q\in Q\)  be the cl_uniform_barrier event issued by client \(\mathit {cl}\) 
just before \(a\) .
Suppose that \(q\)  is issued to replica \(p^{l}_{d}\)  in data center \(d\) .
By Lemma REF ,
\(({\sf uniformVec}^{l}_{d})_{q}[d] &\ge ({\sf pastVec}_{\mathit {cl}})_{q}[d]\nonumber \\&= ({\sf pastVec}_{\mathit {cl}})_{e}[d].\) 
By (REF ), (REF ),
(REF ), and Lemma REF ,
eventually for the correct data center \(c\) ,
\(\forall i \in \;{\sf uniformVec}^{m}_{c}[i] \ge ({\sf pastVec}_{\mathit {cl}})_{e}[i].\) 
Therefore, the wait condition
\(\forall i \in \lbrace c\rbrace .\;{\sf uniformVec}^{m}_{c}[i] \ge ({\sf pastVec}_{\mathit {cl}})_{e}[i]\) 
at line REF :REF 
at replica \(p^{m}_{c}\)  will eventually hold.
Thus, the cl_attach event \(a\)  eventually terminates.
Theorem 85 
Any client event issued at a correct data center
will eventually terminate.

Consider any event \(e\)  issued by client \(\mathit {cl}\) 
at a correct data center \(c \in .It suffices to show that each wait condition in the execution of \) e\(,if any, will eventually hold.In the following, we perform a case analysisaccording to the type of event \) e\(.\begin{itemize}\item \textsc {Case I}: e \in S.The theorem holds trivially.\item \textsc {Case II}: e \in R.If e \in R_{\textsc {int}}, the theorem holds trivially.Otherwise, e \in R_{\textsc {ext}}.By Lemmas~\ref {lemma:knownvc-d-no-bound}and \ref {lemma:knownvc-strong-no-bound},the wait condition atline~\ref {alg:unistore-replica}:\ref {line:readkey-wait-util-knownvc}for e will eventually hold.\item \textsc {Case III}: e \in U.The theorem holds trivially.\item \textsc {Case IV}: e \in C_{\textsl {causal}}.Since data center c is correct,the wait condition atline~\ref {alg:unistore-coord}:\ref {line:commitcausal-wait-prepareack}will eventually hold.\item \textsc {Case V}: e \in C_{\textsl {strong}}.By Lemma~\ref {lemma:uniformvc-c-no-bound},the wait condition atline~\ref {alg:unistore-replica}:\ref {line:uniformbarrier-wait-uniformvc-d}will eventually hold.Thus, line~\ref {alg:unistore-strong-commit}:\ref {line:commitstrong-call-uniformbarrier}will eventually terminate.Then, by Assumption~\ref {assumption:complete-execution},the procedure \textsc {certify} and thus the event e will eventually terminate.\item \textsc {Case VI}: e \in \textsc {cl\_uniform\_barrier}.By Lemma~\ref {lemma:uniformvc-c-no-bound},the wait condition atline~\ref {alg:unistore-replica}:\ref {line:uniformbarrier-wait-uniformvc-d}will eventually hold.\item \textsc {Case VII}: e \in \textsc {cl\_attach}.The theorem holds due to \textsc {Case VI} and Lemma~\ref {lemma:migrate-terminate}.\end{itemize}\)
