Notice that an assignment of a tuple to a variable $\vx$ determines the tuples assigned to all variables $\vy$ with $\vx \varimplies{F}{D} \vy$ for some sequence of function names $F$. From Lemma <ref> it follows that each such implied tuple is witnessed by a path in the corresponding schema graph $\sgname$. Therefore, the maximal number of different tuples implied by $\vx$ corresponds to the number of paths in $\sgname$ starting in $\type{\vx}$, which is finite when $\sgname$ is acyclic.
Because there can be multiple paths between nodes in the schema graph, it is no longer the case as in the previous section that variables of the same type connected in $D$ must be assigned the same value.
So, instead of using type mappings, we introduce tuple-contexts
to represent the sets of all tuples implied by the assignment of a given variable.
Formally, a tuple-context for a type $R \in \schRel$ is a function from paths with source $R$ in  $\sg{\schRel, \schFunc}$ to tuples in $\objects$ of the appropriate type. That is, for each tuple-context $c$ for type $R$ and for each path $R \asgimplies{F}{\sgname} S$ in $\sgname$, $\type{c(R \asgimplies{F}{\sgname} S)} = S$.

Similar to Lemma <ref>, we show
that we can represent a counterexample schedule based on $D$
by assigning a tuple-context to each variable in $\transcopies{D}$, taking special care when assigning contexts to variables connected in $D$ to make sure that they are properly related to each other. For this,
we introduce a (partial) function $\contextfunc: \variables \to \contextset$ mapping (a subset of) variables in $\transcopies{D}$ to tuple-contexts in $\contextset$ (for $\contextset$ a set of tuple-contexts)and refer to it as a (partial) context assignment for $D$ over $\contextset$. In a sequence of lemmas, we show that $\contextfunc$ can always be expanded into a total function and an approach based on enumeration of quintuples analogous to Lemma <ref> suffices to decide robustness. A major difference with the previous section is that there is no longer a constant bound on the number of tuple-contexts that are needed and consistency between tuple-contexts in connected variables needs to be maintained.

We call node $S$ a descendant of node $R$ and $R$ an ancestor of $S$ in an acyclic schema graph $\sgname$. We write $R \asgimplies{\varepsilon}{\sgname}S$, with $\varepsilon$ denoting the empty labeling, for the case $R=S$. This means that a node is a descendant and ancestor of itself. When $F$ is not relevant, we simply write $R \asgimplies{}{\sgname} S$.

Let $c_R$ and $c_{S}$ be two tuple-contexts for types $R$ and $S$, respectively, such that $S$ is a descendant of $R$ in $\sgname$, witnessed by the path $R \asgimplies{F}{\sgname} S$ in $\sgname$.
We then say that $c_{S}$ is a tuple-subcontext of $c_R$ witnessed by $F$ if $c_{S}(S \asgimplies{F'}{\sgname} S') = c_{R}(R \asgimplies{F \cdot F'}{\sgname} S')$ for every path $S \asgimplies{F'}{\sgname} S'$ in $\sgname$.
It should be noted that $R \asgimplies{F \cdot F'}{\sgname} S'$ is indeed a valid path in $\sgname$, as it concatenates the paths $R \asgimplies{F}{\sgname} S$ and $S \asgimplies{F'}{\sgname} S'$. For a given tuple-context $c$ for a type $R$ in the schema graph $\sgname$, we will often write $c(F)$ as a shorthand notation for $c(R \asgimplies{F}{\sgname} S)$.

Similar to Lemma <ref> for sets of  admitting multi-tree bijectivity,
Lemma <ref> shows that we can represent a counterexample schedule based on a  $D$ over an acyclic schema by assigning a tuple-context to each variable in $\transcopies{D}$, taking special care when assigning contexts to variables connected in $D$ to make sure that they are properly related to each other.
For a set of tuple-contexts $\contextset$, we refer to a (partial) function $\contextfunc: \variables \to \contextset$ mapping (a subset of) variables in $\transcopies{D}$ to tuple-contexts in $\contextset$ as a (partial) context assignment for $D$ over $\contextset$. We furthermore say that $\contextfunc$ is a total context assignment for $D$ over $\contextset$ if $\contextfunc$ is defined for every variable in $\transcopies{D}$.

Two variables $\vx$ and $\vy$ occurring in $\transcopies{D}$ are equivalent in $D$, denoted $\vx \varequiv{D} \vy$ if

* $\vx = \vy$;

* there exists a pair of variables $\vz$ and $\vw$ and a sequence of function names $F$ with $\vz \varequiv{D} \vw$, $\vz \varimplies{F}{D} \vx$ and $\vw \varimplies{F}{D} \vy$; or

* there exists a variable $\vz$ with $\vx \varequiv{D} \vz$ and $\vz \varequiv{D} \vy$.

Similarly, two variables $\vx$ and $\vy$ occurring in a  $\tau$ are equivalent in $\tau$, denoted $\vx \varequiv{\tau} \vy$ if

* $\vx = \vy$;

* there exists a pair of variables $\vz$ and $\vw$ in $\tau$ and a sequence of function names $F$ with $\vz \varequiv{\tau} \vw$, $\vz \varimplies{F}{\tau} \vx$ and $\vw \varimplies{F}{\tau} \vy$; or

* there exists a variable $\vz$ with $\vx \varequiv{\tau} \vz$ and $\vy \varequiv{\tau} \vz$.

Intuitively, every variable mapping admissible for a given database will assign the same tuple to equivalent variables (see Lemma <ref>).
Due to these equivalent variables, the assignment of a tuple to a variable $\vx$ for a given database might imply the tuple assigned to a variable $\vy$, even if $\vx \varimplies{}{D} \vy$ does not hold.
We capture this observation by introducing variable determination, which is stronger than the previously defined variable implication.
Formally, a variable $\vx$ determines a variable $\vy$ in $D$ witnessed by a sequence of function names $F$, denoted $\vx \vardet{F}{D} \vy$ if:

* $\vx \varimplies{F}{D} \vy$;

* $F = \varepsilon$ and $\vx \varequiv{D} \vy$; or

* there exists a variable $\vz$ with $\vx \vardet{F_1}{D} \vz$, $\vz \vardet{F_2}{D} \vy$ and $F = F_1 \cdot F_2$.

For two variables $\vx$ and $\vy$ in a  $\tau \in \transcopies{D}$ we furthermore say that $\vx$ determines $\vy$ in $\tau$ witnessed by a sequence of function names $F$, denoted $\vx \vardet{F}{\tau} \vy$ if:

* $\vx \varimplies{F}{\tau} \vy$;

* $F = \varepsilon$ and $\vx \varequiv{\tau} \vy$; or

* there exists a variable $\vz$ with $\vx \vardet{F_1}{\tau} \vz$, $\vz \vardet{F_2}{\tau} \vy$ and $F = F_1 \cdot F_2$.

For a multiversion split schedule $\schedule$ based on a  $C$ over a set of transactions $\transset$ consistent with a set of  $\workload$ and a database $\db$, let $\barmu$ be the variable mapping for a  $D$ over $\workload$ with $\barmu(D) = C$.
Then, for every combination of variables $\vw, \vx, \vy, \vz$ occurring in $\transcopies{D}$, if $\vz \varimplies{F}{D} \vx$, $\vw \varimplies{F}{D} \vy$ and $\barmu(\vz) = \barmu(\vw)$, then $\barmu(\vx) = \barmu(\vy)$.

By definition of $\vz \varimplies{}{D} \vx$, there is a sequence of variables $\vx_1, \vx_2\, \ldots, \vx_n$ with $\vx_1 = \vz$ and $\vx_n = \vx$ such that for each pair of adjacent variables $\vx_i$ and $\vx_{i+1}$:

$(\dagger)$ $\vx_i$ and $\vx_{i+1}$ both occur in the same  $\tau \in \transcopies{D}$ and $\vx_{i+1} = f(\vx_i) \in \Cset(\tau)$ for some function name $f$; or

$(\ddagger)$ $\type{\vx_i} = \type{\vx_{i+1}}$ and there is a  $(\tau_j, o_j, p_k, \tau_k)$ in $D$
with either $\myvar{o_j} = \vx_i$ and $\myvar{p_k} = \vx_{i+1}$ or $\myvar{p_k} = \vx_i$ and $\myvar{o_j} = \vx_{i+1}$.

Furthermore, the sequence $F$ corresponds to the function names used in applications of $(\dagger)$. Analogously, $\vw \varimplies{}{D} \vy$, implies a sequence of variables $\vy_1, \vy_2\, \ldots, \vy_n$ with $\vy_1 = \vw$ and $\vy_m = \vy$ with the same properties. Notice that the lengths of these two sequences of variables, namely $n$ and $m$, are not necessarily equal to each other and to the length of $F$ due to possible applications of $(\ddagger)$.
For a variable $\vx_i$ in the sequence $\vx_1, \vx_2, \ldots, \vx_n$, we denote the sequence of function names derived from applications of $(\dagger)$ in the subsequence $\vx_i, \ldots, \vx_n$ by $\fsuffix(\vx_i)$. Notice that $\fsuffix(\vx_i)$ is indeed always a suffix of $F$, and that $\fsuffix(\vx_1) = \fsuffix(\vy_1)=F$ and $\fsuffix(\vx_n)=\fsuffix(\vy_n) = \varepsilon$.

We argue by induction that for every $i\in[1,n]$ and $j\in [1,m]$, if $\fsuffix(\vx_i)=\fsuffix(\vy_j)$ then $\barmu(\vx_i) = \barmu(\vy_j)$. This then implies $\barmu(\vx) = \barmu(\vx_n) = \barmu(\vy_m) = \barmu(\vy)$.
(base case) Note that $\barmu(\vx_1) = \barmu(\vz) = \barmu(\vw) = \barmu(\vy_1)$ and $\fsuffix(\vx_1) = F = \fsuffix(\vy_1)$.
(inductive case)
Let $\fsuffix(\vx_{i+1}) = \fsuffix(\vy_{j+1})$. Then,
we distinguish the following cases:

* $\fsuffix(\vx_{i}) = \fsuffix(\vx_{i+1})$: This means that $(\ddagger)$ applies to $\vx_i$ and $\vx_{i+1}$, and there is a  $(\tau_k, o_k, p_\ell, \tau_\ell)$ in $D$
with either $\myvar{o_k} = \vx_i$ and $\myvar{p_\ell} = \vx_{i+1}$ or $\myvar{p_\ell} = \vx_i$ and $\myvar{o_k} = \vx_{i+1}$. By definition of $\barmu$, we have $\barmu(\vx_{i+1}) = \barmu(\vx_{i})$ and by induction that $\barmu(\vx_{i+1}) = \barmu(\vy_{j+1})$ implying that
$\barmu(\vx_{i+1}) = \barmu(\vx_{j+1})$.

* $\fsuffix(\vy_j) = \fsuffix(\vy_{j+1})$: similar as previous argument;

* $\fsuffix(\vx_{i}) \neq \fsuffix(\vx_{i+1})$ and $\fsuffix(\vy_j) \neq \fsuffix(\vy_{j+1})$: Then, $(\dagger)$ applies to both $\vx_i$ and $\vx_{i+1}$, and $\vy_j$ and $\vy_{j+1}$. Furthermore, $\fsuffix(\vx_i) = \fsuffix(\vy_{j}) = f\cdot F'$ for some $f$ and $F'$. By induction, $\barmu(\vx_i)=\barmu(\vy_j)$. Then, $\vx_{i+1} = f(\vx_i)$ is a constraint in some  $\tau_k \in \transcopies{D}$ and $\vy_{j+1} = f(\vy_j)$ is a constraint in some  $\tau_\ell\in \transcopies{D}$.
Since $\barmu$ is admissible for database $\db$ and $\barmu(\vx_i) = \barmu(\vy_j)$, it follows that $\barmu(\vx_{i+1}) = f^\db(\barmu(\vx_i)) = f^\db(\barmu(\vy_j)) = \barmu(\vy_{j+1})$.

The next Lemma shows that every variable mapping admissible for a given database will assign the same tuple to equivalent variables.

For a multiversion split schedule $\schedule$ based on a  $C$ over a set of transactions $\transset$ consistent with a set of  $\workload$ and a database $\db$, let $\barmu$ be the variable mapping for a  $D$ over $\workload$ with $\barmu(D) = C$.
Then, for every pair of variables $\vx$ and $\vy$ occurring in  $\tau_i$ and $\tau_j$ in $\transcopies{D}$ respectively, if $\vx \varequiv{D} \vy$, then $\barmu(\vx) = \barmu(\vy)$.

The proof is by induction on the definition of $\vx \varequiv{D} \vy$. (base case) If $\vx = \vy$, then the result is immediate.
(inductive cases)
If there are two variables $\vz$ and $\vw$ and a sequence of function names $F$ such that $\vz \varequiv{D} \vw$, $\vz \varimplies{F}{D} \vx$ and $\vw \varimplies{F}{D} \vy$, then by induction we have $\barmu(\vz) = \barmu(\vw)$.
The proof that $\barmu(\vx) = \barmu(\vy)$ is now immediate by application of Lemma <ref>.
If instead there is a variable $\vz$ with $\vx \varequiv{D} \vz$ and $\vy \varequiv{D} \vz$, then we can argue by induction that $\barmu(\vx) = \barmu(\vz)$ and $\barmu(\vy) = \barmu(\vz)$, and hence $\barmu(\vx) = \barmu(\vy)$.

Let $D$ be a , $\contextset$ a set of tuple-contexts and $\contextfunc$ a partial context assignment for $D$ over $\contextset$.
We say that $\contextfunc$ respects the constraints of $D$ if,
for every two (not necessarily different) variables $\vx$ and $\vy$ occurring in $D$ that $\contextfunc$ is defined for,
the following conditions are true, where $c_\vx = \contextfunc(\vx)$ and $c_\vy = \contextfunc(\vy)$:

*  $c_\vx$ is a tuple-context for $\type{\vx}$;

*  for every $\vx \vardet{F_1}{D} \vz$ and $\vy \vardet{F_2}{D} \vz$, $c_\vx(F_1) = c_\vy(F_2)$;

*  for every $\vx \vardet{F_1}{D} \vw$ and $\vy \vardet{F_2}{D} \vz$ with $\vw \neq \vz$ a constraint in a  $\tau$, $c_\vx(F_1) \neq c_\vy(F_2)$;

*  for every $\vx \vardet{F_1}{D} \vw$ and $\vy \vardet{F_2}{D} \vz$, if $c_\vx(F_1) = c_\vy(F_2)$, then there is no constraint $\vw \neq \vz$ in a  $\tau \in \transcopies{D}$;

*  if $\vx \vardet{F}{D} \vy$, then $c_\vy$ is a tuple-subcontext of $c_\vx$ witnessed by $F$; and

*  for every pair of tuple-subcontexts $c_\vx'$ and $c_\vy'$ of $c_\vx$ and $c_\vy$ witnessed by respectively $F_\vx$ and $F_\vy$, if $c_\vx(F_\vx) = c_\vy(F_\vy)$, then $c_\vx' = c_\vy'$.

The next Lemma shows that we can represent a counterexample schedule based on a sequence of potentially conflicting quadruples D over an acyclic schema by assigning a tuple-context to each variable in Trans(D).

For a multiversion split schedule $\schedule$ based on a  $C$ over a set of transactions $\transset$ consistent with a set of  $\workload \in \acyctemplates$ and a database $\db$, let $\barmu$ be the variable mapping for a  $D$ over $\workload$ with $\barmu(D) = C$.
Then a set $\contextset$ of tuple-contexts and a total context assignment $\contextfunc$ for $D$ over $\contextset$
exist with:

* $\contextfunc$ respects the constraints of $D$; and

* $\barmu(\vx) = c_\vx(\epsilon)$ for every variable $\vx$, with $c_\vx = \contextfunc(\vx)$.

We first assign a tuple-context to each tuple in database $\db$, based on the functions in $\db$. Let $(\schRel, \schFunc)$ be the schema over which $\workload$ is defined.
Since the schema graph $\sg{\schRel, \schFunc}$ is acyclic, a total order $<_\sgname$ over $\schRel$ exists such that there is no path from type $R$ to type $S$ in $\sgname$ if $R <_\sgname S$.
We now assign tuple-contexts to tuples based on the order implied by $<_\sgname$. That is, we first consider all tuples of the type that is ordered first by $<_\sgname$, then all tuples of the type that is ordered second, etc. If there are multiple tuples of the same type, the relative order in which we handle them is not important.
For each tuple $\x$, we construct a tuple-context $c_\x$ with $c_\x(\varepsilon) = \x$, and for each path $F = f \cdot F'$ in $\sgname$ starting in $\type{\x}$, set $c_\x(F) = c_\y(F')$, with $\y = f^\db(\x)$.
Notice that $c_\y$ is already defined for $\y$, as there is a path from $\type{\x}$ to $\type{\y}$ in $\sgname$ and, hence, $\type{\y} <_\sgname \type{\x}$.
By construction, $c_\y$ is a tuple-subcontext of $c_\x$ witnessed by $f$.

Next, we construct $\contextfunc$ as follows: $\contextfunc(\vx) = c_\x$ with $\barmu(\vx) = \x$ for every variable $\vx$ occurring in $\transcopies{D}$.
We argue by induction on the definition of  $\vardet{F}{D}$ that

$c_\x(F) = \barmu(\vy)$ for every $\vx \vardet{F}{D} \vy$ (with $c_\x = \contextfunc(\vx)$). $(\dagger)$

If $\vx \varimplies{F}{D} \vy$, then
by construction of $\contextfunc$ and since $\barmu$ is admissible for $\db$, we have $c_\x(F) = \barmu(\vy)$. If $F = \varepsilon$ and $\vx \varequiv{D} \vy$, then $c_\x(\varepsilon) = \barmu(\vx) = \barmu(\vy)$ by Lemma <ref>.
Otherwise, if there exists a variable $\vz$ with $\vx \vardet{F_1}{D} \vz$, $\vz \vardet{F_2}{D} \vy$ and $F = F_1 \cdot F_2$,
then by induction $c_\x(F_1) = \barmu(\vz) = \y$ and $c_\y(F_2) = \barmu(\vy)$, with $\contextfunc(\vz) = c_\y$. By construction of $c_\x$ and $c_\y$, the desired $c_\x(F) = \barmu(\vy)$ now follows.

It remains to verify that $\contextfunc$ indeed satisfies all required properties. By construction, $\barmu(\vx) = c_\x(\varepsilon)$ with $c_\x = \contextfunc(\vx)$, so we only need to show that $\contextfunc$ respects the constraints of $D$ by verifying all properties in Definition <ref>.
To this end, let $\vx$ and $\vy$ be two variables occurring in $\transcopies{D}$, and let $c_\x = \contextfunc(\vx)$ and $c_\y = \contextfunc(\vy)$.
(<ref>) By construction, $c_\x$ is a tuple-context for $\type{\vx}$.
(<ref>) $c_\x(F_1) = \barmu(\vz) = c_\y(F_2)$ by $(\dagger)$.
(<ref>) If $\vw \neq \vz$ is a constraint, then $\barmu(\vw) \neq \barmu(\vz)$ as $\barmu$ is admissible for $\db$. By $(\dagger)$, it follows that $c_\x(F_1) = \barmu(\vw) \neq \barmu(\vz) = c_\y(F_2)$.
(<ref>) If $c_\x(F_1) = c_\y(F_2)$, then $\barmu(\vw) = c_\x(F_1) = c_\y(F_2) = \barmu(\vz)$ by $(\dagger)$. Since $\barmu$ is admissible for $\db$, there cannot be a constraint $\vw \neq \vz$.
(<ref>) If $\vx \vardet{F}{D} \vy$, then by construction of the tuple-contexts $c_\x$ and $c_\y$ it follows that $c_\y$ is a tuple-subcontext of $c_\x$ witnessed by $F$.
(<ref>) Let $c_{\x'}$ and $c_{\y'}$ be tuple-subcontexts of $c_{\x}$ and $c_{\y}$ witnessed by respectively $F_\vx$ and $F_\vy$.
If $c_{\x}(F_\vx) = c_{\y}(F_\vy) = \z$ for some tuple $\z$, then by construction of $c_{\x}$ and $c_{\y}$ we have $c_{\x'} = c_{\y'} = c_\z$, with $c_\z$ the tuple-context assigned to this tuple $\z$.

From $D = (\tau_1, o_1, p_2, \tau_2), \ldots, (\tau_m, o_m, p_1, \tau_1)$ and $\contextfunc$ as in Lemma <ref>
we can derive a sequence of quintuples $E = (\tau_1, o_1, c_{o_1}, p_1, c_{p_1}), \ldots, (\tau_m, o_m, c_{o_m}, p_m, c_{p_m})$ such that $c_{o_i} = \contextfunc(\vx_i)$ (respectively $c_{p_i} = \contextfunc(\vy_i)$) for $i \in [1,m]$ with $o_i$ (respectively $p_i$) an operation over variable $\vx_i$ (respectively $\vy_i$). Intuitively, this sequence of quintuples can be used to reconstruct the original multiversion split schedule $\schedule$.
To this end, notice that we can derive the original  $D$ and a partial context assignment $\contextfunc'$ from $E$ that is defined for each variable $\vx_i$ occurring in either an operation $o_i$ or $p_i$ in $\tau_i$. We first show that we can extend this partial context assignment $\contextfunc'$ to a total context assignment respecting the constraints in $D$ (Lemma <ref>),
and then prove that such a total context assignment respecting the constraints in $D$ implies a variable assignment $\barmu$ such that the $C = \barmu(D)$ is a valid  (Lemma <ref>).

Let $D = (\tau_1, o_1, p_2, \tau_2), \ldots, (\tau_m, o_m, p_1, \tau_1)$ be a  over a set of  $\workload \in \acyctemplates$ and $\contextfunc$ a partial context assignment defined for every variable $\vx_i$ of $o_i$ and $\vy_i$ of $p_i$ in every $\tau_i$.

* $\contextfunc$ respects the constraints of $D$; and

* for every pair of variables $\vx$ and $\vy$ in a  $\tau_i$ with $\vx \varequiv{\tau_i} \vy$, there is no constraint $\vx \neq \vy$ in $\tau_i$;

then we can extend $\contextfunc$ to a total context assignment $\contextfunc'$ for $D$ respecting the constraints of $D$.

By definition of equivalence, $\varequiv{D}$ partitions all variables occurring in $\transcopies{D}$ in equivalence classes. That is, two variables $\vx$ and $\vy$ are in the same equivalence class iff $\vx \varequiv{D} \vy$. For a given variable $\vx$, we denote the equivalence class $\vx$ belongs to by $\varequivclass{\vx}$.
Note that for any pair of variables $\vx$ and $\vy$ occurring  in $\transcopies{D}$, if $\vx \vardet{F}{D} \vy$, then $\vx' \vardet{F}{D} \vy'$ for any pair of variables $\vx' \in \varequivclass{\vx}$ and $\vy' \in \varequivclass{\vy}$.
By slight abuse of notation, we use $\vx \vardet{F}{D} \varequivclass{\vy}$ and $\varequivclass{\vx} \vardet{F}{D} \vy$ to denote that
$\vx \vardet{F}{D} \vy'$ for every $\vy' \in \varequivclass{\vy}$ and $\vx' \vardet{F}{D} \vy$ for every $\vx' \in \varequivclass{\vx}$, respectively.

Let $(\schRel, \schFunc)$ be the schema over which $\workload$ is defined.
Since the schema graph $\sg{\schRel, \schFunc}$ is acyclic, a total order $<_\sgname$ over $\schRel$ exists such that there is no path from type $R$ to type $S$ in $\sgname$ if $R <_\sgname S$.
We now define $\contextfunc'$ for variables in $\transcopies{D}$ according to the order implied by $<_\sgname$. If there are multiple variables of the same type, the relative order in which we handle them is not important.

The proof is as follows. Assume $\contextfunc$ respects the constraints of $D$ and is at least defined for every variable $\vx_i$ of $o_i$ and $\vy_i$ of $p_i$ in every $\tau_i$.
We extend $\contextfunc$ towards $\contextfunc'$ by defining $\contextfunc'$ for the whole equivalence class $\varequivclass{\vx}$ of the first (according to $<_\sgname$) variable $\vx$ for which $\contextfunc$ is not defined.
The precise construction is by case. In the first case, the tuple-context that should be assigned to variables in $\varequivclass{\vx}$ is already implied, as it is the tuple-subcontext of an existing tuple-context. In the second case, we construct a fresh tuple-context, including existing tuple-contexts as tuple-subcontexts where we need to make sure that $\contextfunc'$ respects the constraints in $D$.
In each case, we then argue that $\contextfunc'$ still respects the constraints in $D$.
By repeating this argument, we can extend the context assignment to a total context assignment defined for all variables occurring in $\transcopies{D}$.

(Case 1) If a variable $\vy$ exists with $\contextfunc$ defined for $\vy$ and $\vy \vardet{F}{D} \varequivclass{\vx}$, then $\contextfunc'(\vx') = c_{\vx'}$ for every variable $\vx' \in \varequivclass{\vx}$, with $c_{\vx'}$ the tuple-subcontext of $c_\vy = \contextfunc(\vy)$ witnessed by $F$.
Notice that this is well defined, even if there are multiple such $\vy$, as they all agree on $c_{\vx'}$ by Definition <ref> (<ref>, <ref>).
Also note that the special case where $\contextfunc$ is already defined for at least one variable $\vx' \in \varequivclass{\vx}$ is covered by this case as well, as $\vx' \vardet{\varepsilon}{D} \varequivclass{\vx}$ follows from $\vx' \in \varequivclass{\vx}$. In this special case, the tuple-subcontext of $\contextfunc(\vx')$ witnessed by $\varepsilon$ (i.e., $\contextfunc(\vx')$ itself) will be assigned to each variable in $\varequivclass{\vx}$.

We show that $\contextfunc'$ indeed respects the constraints in $D$ according to the properties stated in Definition <ref>.
To this end, let $\vx'$ and $\vy'$ be two variables, with $c_{\vx'} = \contextfunc'(\vx')$ and $c_{\vy'} = \contextfunc'(\vy')$.
(<ref>) By construction, $c_{\vx'}$ is a tuple-context for $\type{\vx'}$.
(<ref>-<ref>) Note that if $\vx'' \vardet{F'}{D} \vz''$ with $\vx'' \in \varequivclass{\vx}$, then $\vy \vardet{F \cdot F'}{D} \vz''$
and $c_{\vx''} = \contextfunc'(\vx'')$ is the tuple-subcontext of $c_\vy = \contextfunc(\vy)$ witnessed by $F'$, implying that $c_{\vx''}(F') = c_{\vy}(F \cdot F')$. If $\vx'$ and/or $\vy'$ are in $\varequivclass{\vx}$, then we can apply this substitution and use the fact that $\contextfunc$ respects the constraints in $\tau$ to conclude that the desired properties hold for $\contextfunc'$.
(<ref>) Assume $\vx' \vardet{F'}{D} \vy'$. If both $\vx' \in \varequivclass{\vx}$ and $\vy' \in \varequivclass{\vx}$, then $F' = \varepsilon$ as otherwise the schema graph is not acyclic.
Since $c_{\vy'} = c_{\vx'}$, it follows that $c_{\vy'}$ is a tuple-subcontext of $c_{\vx'}$ witnessed by $\varepsilon$.
If $\vx' \in \varequivclass{\vx}$ and $\vy' \not\in \varequivclass{\vx}$, then $\vy \vardet{F \cdot F'}{\tau} \vy'$ and $c_{\vy'}$ is a tuple-subcontext of $c_{\vy}$ witnessed by $F \cdot F'$ as $\contextfunc$ respects the constraints of $\tau$.
Since $c_{\vx'}$ is the tuple-subcontext of $c_\vy$ witnessed by $F$, it follows that $c_{\vy'}$ is a tuple-subcontext of $c_{\vx'}$ witnessed by $F'$.
If $\vx' \not\in \varequivclass{\vx}$ and $\vy' \in \varequivclass{\vx}$, then $\vy \vardet{F}{\tau} \vy'$.
Since $\contextfunc$ respects the constraints in $D$, we apply Definition <ref> (<ref>, <ref>, <ref>) to conclude that $c_{\vy'}$ is a tuple-subcontext of $c_{\vx'}$ witnessed by $F'$.
(<ref>) Assume $c_{\vx'}(F_{\vx'}) = c_{\vy'}(F_{\vy'})$, and let $c_{\vx''}$ and $c_{\vy''}$ be the tuple-subcontexts of respectively $c_{\vx'}$ witnessed by $F_{\vx'}$ and $c_{\vy'}$ witnessed by $F_{\vy'}$.
We argue that $c_{\vx''} = c_{\vy''}$.
Note that, if $\vx' \in \varequivclass{\vx}$, then $c_{\vx''}$ is the tuple-subcontext of $c_\vy$ witnessed by $F \cdot F_{\vx'}$. The reasoning for $\vy' \in \varequivclass{\vx}$ is analogous. Since $\contextfunc$ respects the constraints in $D$, it follows that $c_{\vx''} = c_{\vy''}$.

(Case 2) Otherwise, we construct a fresh tuple-context $c_\vx$ and define $\contextfunc'(\vx') = c_\vx$ for every variable $\vx' \in \varequivclass{\vx}$. This tuple-context $c_\vx$ is constructed as follows: $c_\vx(\varepsilon) = \x_\vx$, with $\x_\vx$ a fresh tuple of the appropriate type.
For every path $F = f \cdot F'$ in $\sgname$ starting in $\type{\vx}$, if there is a variable $\vy$ with $\varequivclass{\vx} \vardet{f}{D} \vy$, then $c_\vx(F) = c_\vy(F')$, with $c_\vy = \contextfunc(\vy)$. In other words, $c_\vy$ is the tuple-subcontext of $c_\vx$ witnessed by $f$.
Note that due to the order $<_\sgname$, $\contextfunc(\vy)$ has to be defined already.
Also note that this is well defined, even if multiple such $\vy$ exist. In that case, all these $\vy$ are equivalent to each other by definition of $\varequiv{D}$, and by construction of $\contextfunc$ they are assigned the same tuple-context. If instead no such variable $\vy$ exists, we define $c_\vx(F) = \x_F$, with $\x_F$ a fresh tuple of the appropriate type.

We show that $\contextfunc'$ indeed respects the constraints in $D$ according to the properties stated in Definition <ref>.
To this end, let $\vx'$ and $\vy'$ be two variables occurring in $\transcopies{D}$, with $c_{\vx'} = \contextfunc'(\vx')$ and $c_{\vy'} = \contextfunc'(\vy')$.
(<ref>) By construction, $c_{\vx'}$ is a tuple-context for $\type{\vx'}$.
(<ref>) Assume $\vx' \vardet{F_1}{D} \vz$ and $\vy' \vardet{F_2}{D} \vz$ for some variable $\vz$.
We argue that there exists a pair of variables $\vx''$ and $\vy''$ and two sequences of function names $F_1'$ and $F_2'$ such that $c_{\vx'}(F_1) = c_{\vx''}(F_1') = c_{\vy''}(F_2') = c_{\vy'}(F_2)$, where $c_{\vx''} = \contextfunc'(\vx'')$ and $c_{\vy''} = \contextfunc'(\vy'')$.
If $\vx' \in \varequivclass{\vx}$,
then either $F_1 = f \cdot F_1'$ or $F_1 = \varepsilon$. In the former case there is a variable $\vx''$ with $\vx'' \vardet{f}{D} \vz$ such that $c_{\vx'}(F_1) = c_{\vx''}(F_1')$, where $c_{\vx''} = \contextfunc(\vx'')$.
In the later case, $\vz \in \varequivclass{\vx}$, and we simply take $\vx'' = \vx'$ and $F_1' = F_1$.
If $\vx' \not\in \varequivclass{\vx}$, we take $\vx'' = \vx'$ and $F_1' = F_1$.
For $\vy' \in \varequivclass{\vx}$ and $\vy' \in \not\varequivclass{\vx}$, the reasoning is analogous.
It remains to argue that $c_{\vx''}(F_1') = c_{\vy''}(F_2')$. By choice of $\vx''$ and $\vy''$, either $\vx'' \not\in \varequivclass{\vx}$ and $\vy'' \not\in \varequivclass{\vx}$; or $\vz \in \varequivclass{\vx}$.
In te former case, $c_{\vx''}(F_1') = c_{\vy''}(F_2')$ follows by the fact that $\contextfunc$ respects the constraints of $D$. In the latter case, both $\vx'' \in \varequivclass{\vx}$ and $\vy'' \in \varequivclass{\vx}$, as otherwise (Case 1) would apply to $\varequivclass{\vx}$ instead. Then, $c_{\vx''}(F_1') = c_{\vy''}(F_2') = c_{\vx}(\varepsilon) = \x_\vx$.
(<ref>, <ref>) The reasoning is analogous to the previous property. Note in particular that by construction of the new $c_\vx$ we have $c_{\vx'}(F_1) = c_{\vy'}(F_2)$ if $\vw \varequiv{D} \vz$.
Since $\vw \varequiv{D} \vz$ implies that there is no constraint $\vw \neq \vz$ by the assumptions on $\contextfunc$ and on the disequality constraints in each  $\tau \in \transcopies{D}$, this does not lead to contradictions.
(<ref>) If $\vx' \vardet{F'} \vy'$, then $\vy' \in \varequivclass{\vx}$ only if $\vx' \in \varequivclass{\vx}$, as otherwise (Case 1) would apply to $\varequivclass{\vx}$ instead. We argue by case that $c_{\vy'}$ is a tuple-subcontext of $c_{\vx'}$ witnessed by $F'$.
If $\vx' \not\in \varequivclass{\vx}$ and $\vy' \not\in \varequivclass{\vx}$, the result is immediate by the fact that $\contextfunc$ respects the constraints of $D$.
If $\vx' \in \varequivclass{\vx}$ and $\vy' \not\in \varequivclass{\vx}$, then $c_{\vx'} = c_\vx$ and a variable $\vz$ exists such that $F' = f \cdot F''$, $\vx' \vardet{f}{D} \vz$, $\vz \vardet{F''}{D} \vy'$,
and, by construction of $c_\vx$, $c_{\vy'}$ is a tuple-subcontext of $\contextfunc(\vz)$ witnessed by $F''$. It now follows that $c_{\vy'}$ is a tuple-subcontext of $c_\vx$ witnessed by $F'$.
Lastly, If both $\vx' \in \varequivclass{\vx}$ and $\vy' \in \varequivclass{\vx}$, then $F' = \varepsilon$, as otherwise the schema graph is not acyclic. The result is immediate, as $c_{\vy'} = c_{\vx'} = c_{\vx}$ is by definition a tuple-subcontext of itself witnessed by $\varepsilon$.
(<ref>) Assume $c_{\vx''}(F_1) = c_{\vy''}(F_1)$ for some pair of tuple-contexts $c_{\vx''}$ and $c_{\vy''}$ that are tuple-subcontexts of respectively $c_{\vx'}$ witnessed by $F_1$ and $c_{\vy'}$ witnessed by $F_2$. We argue that $c_{\vx''} = c_{\vy''}$.
If both $c_{\vx'}$ and $c_{\vy'}$ are different from $c_\vx$, the result is immediate as $\contextfunc$ respects the constraints of $D$.
Otherwise, since the construction of $c_\vx$, either copies existing tuple-contexts as tuple-subcontexts, or introduces fresh variables. the result holds if $c_{\vx'}$ and/or $c_{\vy'}$ are equal to $c_\vx$.

Given a total context assignment respecting the constraints in $D$ as in Lemma <ref>, we show in the next Lemma that such a total context assignment implies a variable assignment $\barmu$ such that the $C = \barmu(D)$ is a valid .

Let $D = (\tau_1, o_1, p_2, \tau_2), \ldots, (\tau_m, o_m, p_1, \tau_1)$ be a  over a set of  $\workload$ and $\contextfunc$ a total context assignment for $D$ respecting the constraints of $D$.
The variable mapping $\barmu$ obtained by defining $\barmu(\vx) = c_\vx(\epsilon)$ for every variable $\vx$ in $\transcopies{D}$ with $c_\vx = \contextfunc(\vx)$ then is
a valid variable mapping admissible for some database $\db$.

We first argue that $\barmu$ is valid by showing for each  $(\tau_i, o_i, p_j, \tau_j)$ in $D$ that $\barmu(\vx) = \barmu(\vy)$ with $\vx = \myvar{o_i}$ and $\vy = \myvar{p_j}$.
By definition, $\vx \varimplies{\varepsilon}{D} \vy$, and hence $\vx \vardet{\varepsilon}{D} \vy$. Let $c_\vx = \contextfunc(\vx)$ and $c_\vy = \contextfunc(\vy)$.
Since $\contextfunc$ respects the constraints of $D$, $c_\vy$ is a tuple-subcontext of $c_\vx$ witnessed by $\varepsilon$.
By definition of tuple-subcontexts, $c_\vx(\varepsilon) = c_\vy(\varepsilon)$, and, as a result, $\barmu(\vx) = c_\vx(\varepsilon) = c_\vy(\varepsilon) = \barmu(\vy)$.

Next, we construct a database $\db$ and show that $\barmu$ is admissible for $\db$. To this end, we add the tuple $\barmu(\vx)$ to $\db$ for each variable $\vx$ occurring in $\transcopies{D}$.
For each
functional constraint $\vy = f(\vx)$ in a  in $\transcopies{D}$, we define $\barmu(\vy) = f^\db(\barmu(\vx))$ for the corresponding function $f^\db$ in $\db$.
Note that this is well defined.
Towards a contradiction, assume that we have both $\barmu(\vy) = f^\db(\barmu(\vx))$ and $\barmu(\vw) = f^\db(\barmu(\vz))$, with $\barmu(\vx) = \barmu(\vz)$ but $\barmu(\vy) \neq \barmu(\vw)$.
Let $c_\vx = \contextfunc(\vx)$, $c_\vy = \contextfunc(\vy)$, $c_\vz = \contextfunc(\vz)$ and $c_\vw = \contextfunc(\vw)$.
By construction of $\barmu$, we have $c_\vx(\varepsilon) = \barmu(\vx) = \barmu(\vz) = c_\vz(\varepsilon)$ and $c_\vy(\varepsilon) = \barmu(\vy) \neq \barmu(\vw) = c_\vw(\varepsilon)$.
By Definition <ref> (<ref>), it now follows that $c_\vx = c_\vz$, since $c_\vx$ (respectively $c_\vz$) is a tuple-subcontext of itself witnessed by $\varepsilon$ and $c_\vx(\varepsilon) = c_\vz(\varepsilon)$.
Since we defined $\barmu(\vy) = f^\db(\barmu(\vx))$, there is a constraint $\vy = f(\vx)$ in some  in $\transcopies{D}$, and hence $\vx \vardet{f}{D} \vy$. Analogously, $\vz \vardet{f}{D} \vw$.
By Definition <ref> (<ref>), $c_\vy$ and $c_\vw$ are tuple-subcontexts of respectively $c_\vx$ and $c_\vz$ witnessed by $f$.
As $c_\vx = c_\vz$, it immediately follows that $c_\vy = c_\vw$, and in particular $c_\vy(\varepsilon) = c_\vw(\varepsilon)$, leading to the desired contradiction.

To conclude the proof, we show that $\barmu$ is indeed admissible for $\db$.
By construction of $\db$ based on $\barmu$, $\barmu(\vy) = f^\db(\barmu(\vx))$ is immediate for each constraint $\vy = f(\vx)$ in a  $\tau \in \transcopies{D}$.
We still need to argue that $\barmu(\vx) \neq \barmu(\vy)$ for each constraint $\vx \neq \vy$ in a  $\tau \in \transcopies{D}$.
Let $c_\vx = \contextfunc(\vx)$ and $c_\vy = \contextfunc(\vy)$.
By construction of $\barmu$ we have $\barmu(\vx) = c_\vx(\varepsilon)$ and $\barmu(\vy) = c_\vy(\varepsilon)$.
Note that $\vx \vardet{\varepsilon}{D} \vx$ and $\vy \vardet{\varepsilon}{D} \vy$.
Therefore, we can apply Definition <ref> (<ref>) to conclude that $c_\vx(\varepsilon) \neq c_\vy(\varepsilon)$, and hence $\barmu(\vx) \neq \barmu(\vy)$.

In order to decide robustness against , one can now construct a sequence of quintuples $E$ and derive the  $D$ and partial context assignment $\contextfunc$ from it.
If $\contextfunc$ respects the constraints in $D$, then it follows from Lemma <ref> and Lemma <ref> that we can construct a variable assignment $\barmu$ such that $C = \barmu(D)$ is a valid .
However, in this construction of $E$, care should be taken to guarantee that $\contextfunc$ indeed respects the constraints in $D$, and that the resulting multiversion split schedule based on $C$ indeed satisfies all properties in Definition <ref>.

In the algorithm that we are about to propose, we search for such a sequence of quintuples $E$, but without fixating all the tuples in each context.
For this, we generalize our definition of tuple-contexts to allow variables: A context for a type $R$ is a function from paths with source $R$ in  $\sg{\schRel, \schFunc}$ to variables in $\variables$ and
tuples in $\objects$ of the appropriate type. The purpose of variables is to encode equalities and disequalities within each context, without being explicit about the precise tuples. That is, if two paths ending in the same node in $\sgname$ are mapped on the same variable, then they will represent the same tuple; if they are mapped on different variables, then they represent a different tuple. We remark that a same variable occurring in different contexts can still represent different tuples.
Analogous to tuple-subcontexts, for two types $R$ and $S$ with $R \asgimplies{F}{\sgname} S$, we say that a context $c_{S}$ for type $S$ is a subcontext of a context $c_R$ for type $R$ witnessed by $F$ if:

* for every path $S \asgimplies{F'}{\sgname} S'$ in $\sgname$, if $c_{R}(F \cdot F')$ is a tuple, then $c_{S}(F') = c_{R}(F \cdot F')$; otherwise, $c_{S}(F')$ is a variable; and

* for every pair of paths $S \asgimplies{F_1}{\sgname} S_1$ and $S \asgimplies{F_2}{\sgname} S_2$ in $\sgname$ with $c_{R}(F \cdot F_1)$ and $c_{R}(F \cdot F_2)$ variables, $c_{S}(F_1) = c_{S}(F_2)$ iff $c_{R}(F \cdot F_1) = c_{R}(F \cdot F_2)$.

We call a context a variable-context if all paths are mapped on variables.

For a  $\tau$, tuple-context $c_p$ for $p$ and $c_o$ for $o$ in $\tau$, we consider the set $\contextdomain[SG,\tau,p,c_p, o,c_o]$ of all different (not-necessarily tuple-) contexts $c$ (up to isomorphisms over the variables in $c$) that can be obtained, starting from a variable-context $c'$, by performing substitutions of subcontexts of $c'$ with subcontexts of $c_p$ and/or $c_o$.
More formally, these substitutions are of the form:
For a path $R_c \asgimplies{F}{\sgname} S$ (here $R_c$ is the type that $c$ is for) and $R_p \asgimplies{F'}{\sgname} S$ (with $R_p$ the type that $c_p$ is for) then $c(F \cdot F'') = c_p(F' \cdot F'')$ for every path $S \asgimplies{F''}{\sgname} S'$ in $\sgname$ and with $c(F \cdot F'') = c'(F \cdot F'')$ otherwise. (The substitution rule can be applied for $c_p$ as well as for $c_o$.)

Let $\workload$ be a set of  over an acyclic schema.
Then, $\workload$ is not robust against if, and only if, there is a sequence of quintuples $E = (\tau_1, o_1, c_{o_1}, p_1, c_{p_1}),\allowbreak \ldots,\allowbreak (\tau_m, o_m, c_{o_m}, p_m, c_{p_m})$
with $m \geq 2$ such that for each quintuple $(\tau_i, o_i, c_{o_i}, p_i, c_{p_i})$ in $E$, with $q_i$ and $r_i$ two (not necessarily different) operations in $\{o_i, p_i\}$,

*  if $i = 1$, then $c_{o_1}$ and $c_{p_1}$ are tuple-contexts for $\type{\myvar{o_1}}$ and $\type{\myvar{p_1}}$.
Furthermore, for every pair of tuple-subcontexts $c_{o_1}'$ and $c_{p_1}'$ of $c_{o_1}$ and $c_{p_1}$ witnessed by respectively $F$ and $F'$, if $c_{o_1}(F) = c_{p_1}(F')$, then $c_{o_1}' = c_{p_1}'$;

*  if $i \neq 1$, then $c_{o_i}, c_{p_i} \in \contextdomain[\sgname,\tau_1,p_1,c_{p_1}, o_1,c_{o_1}]$ are contexts for $\type{\myvar{o_i}}$ and $\type{\myvar{p_i}}$;

*  for every pair of variables $\vw_i$ and $\vz_i$ in $\tau_i$ with $\vw_i \varequiv{\tau_i} \vz_i$, there is no constraint $\vw_i \neq \vz_i$ in $\tau_i$;

*  for every $\myvar{q_i} \vardet{F_1}{\tau_i} \vz_i$ and $\myvar{r_i} \vardet{F_2}{\tau_i} \vz_i$, the subcontext of $c_{q_i}$ witnessed by $F_1$ is equal (up to isomorphisms over variables) to the subcontext of $c_{r_i}$ witnessed by $F_2$.

*  for every $\myvar{q_i} \vardet{F_1}{\tau_i} \vw_i$ and $\myvar{r_i} \vardet{F_2}{\tau_i} \vz_i$ with $\vw_i \neq \vz_i$ a constraint in $\tau_i$,
$c_{q_i}(F_1) \neq c_{r_i}(F_2)$ or $c_{q_i}(F_1)$ and $c_{r_i}(F_2)$ are both variables;

*  for every $\myvar{q_i} \varimplies{F_1}{\tau_i} \vw_i$ and $\myvar{r_i} \varimplies{F_2}{\tau_i} \vz_i$, if $c_{q_i}(F_1)$ and $c_{r_i}(F_2)$ are the same tuple, then there is no constraint $\vw_i \neq \vz_i$ in $\tau_i$;

*  if $\myvar{q_i} \vardet{F}{\tau_i} \myvar{r_i}$, then $c_{r_i}$ is a subcontext of $c_{q_i}$ witnessed by $F$; and

*  If $i \neq 1$ and $c_{q_i}(F) = c_{q_1}(F')$ is a tuple for some $q_1 \in \{o_1, p_1\}$ and some sequence of function names $F$ and $F'$,
then there is no operation $o_i' \in \tau_i$ potentially ww-conflicting with an operation $o_1' \in \prefix{\tau_1}{o_1}$ with
$\myvar{q_i} \vardet{F}{\tau_i} \myvar{o_i'}$ and $\myvar{q_1} \vardet{F'}{\tau_1} \myvar{o_1'}$.

Furthermore, for each pair of adjacent quintuples $(\tau_i, o_i, c_{o_i}, p_i, c_{p_i})$ and $(\tau_j, o_j, c_{o_j}, p_j, c_{p_j})$ in $E$ with $j = i + 1$, or $i = m$ and $j = 1$:

*  $o_i$ is potentially conflicting with $p_j$ and $c_{o_i} = c_{p_j}$;

*  if $i = 1$ and $j = 2$, then $o_1$ is potentially rw-conflicting with $p_2$; and

*  if $i = m$ and $j = 1$, then $o_1 <_{\tau_1} p_1$ or $o_m$ is potentially rw-conflicting with $p_1$.

(if) Let $D = (\tau_1, o_1, p_2, \tau_2), \ldots, (\tau_m, o_m, p_1, \tau_1)$ be the  derived from $E$.
Note that each $(\tau_i, o_i, p_j, \tau_j) \in D$ is indeed a valid , as $o_i$ is potentially conflicting with $p_j$ by (<ref>).
We show in Lemma <ref> that a partial context assignment $\contextfunc$ over a set of tuple-contexts $\contextset$ exists such that

* for every pair of operations $o_i$ and $p_i$ occurring in $D$, $\contextfunc$ is defined for  $\myvar{o_i}$ and $\myvar{p_i}$;

* $\contextfunc$ respects the constraints in $D$; and

* for every  $\tau_i$ in $D$ with $i \neq 1$ and for every $q_i \in \{o_i, p_i\}$ and $q_1 \in \{o_1, p_1\}$, let $c_{q_i} = \contextfunc(\myvar{q_i})$ and  $c_{q_1} = \contextfunc(\myvar{q_1})$.
If $c_{q_i}(F) = c_{q_1}(F')$ for some sequence of function names $F$ and $F'$,
then there is no operation $o_i' \in \tau_i$ potentially ww-conflicting with an operation $o_1' \in \prefix{\tau_1}{o_1}$ with
$\myvar{q_i} \vardet{F}{\tau_i} \myvar{o_i'}$ and $\myvar{q_1} \vardet{F'}{\tau_1} \myvar{o_1'}$.

Because of (<ref>), we can now apply Lemma <ref> extending $\contextfunc$ to a total context assignment defined for all variables occurring in $\transcopies{D}$, without losing the property that $\contextfunc$ respects all constraints in $D$.
Let $\barmu$ be the variable mapping obtained by defining $\barmu(\vx) = c_\vx(\varepsilon)$ for every variable $\vx$ in $\transcopies{D}$ with $c_\vx = \contextfunc(\vx)$.
By Lemma <ref>, $\barmu$ is a valid variable mapping and a database $\db$ exists such that $\barmu$ is admissible for $\db$.

We now prove that the  $C = \barmu(D)$ satisfies the conditions stated in Definition <ref> to show that $\workload$ is indeed not robust against .
Condition (<ref>) and Condition (<ref>) are immediate by respectively (<ref>) and (<ref>).
Towards a contradiction, assume Condition (<ref>) does not hold.
Then, there is an operation $o_i'$ in a  $\tau_i$ potentially ww-conflicting with an operation $o_1' \in \prefix{\tau_1}{o_1}$,
and $\barmu(\myvar{o_i'}) = \barmu(\myvar{o_1'})$. Let $c_{o_i'} = \contextfunc(\myvar{o_i'})$ and $c_{o_1'} = \contextfunc(\myvar{o_1'})$.
By construction of $\barmu$, we have $c_{o_i'}(\varepsilon) = c_{o_1'}(\varepsilon)$.
By construction of the total context assignment in Lemma <ref>, this is only the case if for some $q_i \in \{o_i, p_i\}$ and $q_1 \in \{o_1, p_1\}$
it holds that $\myvar{q_i} \vardet{F}{\tau_i} \myvar{o_i'}$ with $c_{q_i}(F) = c_{o_i'}(\varepsilon)$ and $\myvar{q_1} \vardet{F}{\tau_1} \myvar{o_1'}$ with $c_{q_1}(F') = c_{o_1'}(\varepsilon)$.
Consequently, $c_{q_i}(F) = c_{q_1}(F')$, contradicting Lemma <ref>.

(only if) Since $\workload$ is not robust against , a multiversion split schedule $\schedule$ exists
based on a  $C$ over a set of transactions $\transset$ consistent with a set of  $\workload \in \acyctemplates$ and a database $\db$.
Let $\barmu$ be the variable mapping for a  $D = (\tau_1, o_1, p_2, \tau_2), \ldots, (\tau_m, o_m, p_1, \tau_1)$ with $\barmu(D) = C$.
By Lemma <ref> a set $\contextset$ of tuple-contexts and a total context assignment $\contextfunc$ for $D$ over $\contextset$
exist with:

* $\contextfunc$ respects the constraints of $D$; and

* $\barmu(\vx) = c_\vx(\epsilon)$ for every variable $\vx$, with $c_\vx = \contextfunc(\vx)$.

Let $\lambda: \objects \to \objects \cup \variables$ with $\lambda(\x) = \x$ if $\x$ occurs in $\contextfunc(\myvar{o_1})$ or $\contextfunc(\myvar{p_1})$;
and $\lambda(\x) \in \variables$ otherwise, such that $\lambda(\x) \neq \lambda(\y)$ if $\x \neq \y$.
From $D$ and $\contextfunc$ we derive the sequence of quintuples $E = (\tau_1, o_1, c_{o_1}, p_1, c_{p_1}), \ldots, (\tau_m, o_m, c_{o_m}, p_m, c_{p_m})$ with $c_{o_i} = \lambda \circ c'_{o_i}$ and $c_{p_i} = \lambda \circ c'_{p_i}$ for each $o_i$ and $p_i$,
where $c'_{o_i} = \contextfunc(\myvar{o_i})$ and $c'_{p_i} = \contextfunc(\myvar{p_i})$.
Intuitively, we modify the tuple-contexts for each $\myvar{o_i}$ and $\myvar{p_i}$ as defined by $\contextfunc$ into contexts over tuples and variables by replacing all tuples that do not occur in $\contextfunc(\myvar{o_1})$ and $\contextfunc(\myvar{p_1})$ with unique variables.
Note that by construction $c_{o_1} = \contextfunc(\myvar{o_1})$ and $c_{p_1} = \contextfunc(\myvar{p_1})$.

Next, we show that $E$ satisfies all properties.
In the argumentation below, we denote $\contextfunc(\myvar{o_i})$ by $c'_{o_i}$ and $\contextfunc(\myvar{p_i})$ by $c'_{p_i}$ for each $o_i$ and $p_i$ in $E$.
(<ref>) By construction, $c_{o_1} = c'_{o_1}$ is a tuple-context for $\type{\myvar{o_1}}$, and $c_{p_1} = c'_{p_1}$ is a tuple-context for $\type{\myvar{p_1}}$.
By Condition (<ref>) of Definition <ref>, we have $c_{o_1}' = c_{p_1}'$ if $c_{o_1}(F) = c_{p_1}(F')$
for every pair of tuple-subcontexts $c_{o_1}'$ and $c_{p_1}'$ of $c_{o_1}$ and $c_{p_1}$ witnessed by respectively $F$ and $F'$.
(<ref>) This property follows by construction of $c_{o_i}$ and $c_{p_i}$ based on $\lambda$ and $\contextfunc$. For completeness sake, one should note that for each group of contexts up to isomorphisms over variables, $\contextdomain[\sgname,\tau_1,p_1,c_{p_1}, o_1,c_{o_1}]$
contains only one context.
W.l.o.g. we can implicitly assume that each $c_{o_i}$ and $c_{p_i}$ in $E$ is replaced by the same context in $\contextdomain[\sgname,\tau_1,p_1,c_{p_1}, o_1,c_{o_1}]$ up to isomorphisms,
as we will never directly test for equality or disequality between two variables of different contexts.
(<ref>) Assume $\vw_i \varequiv{\tau_i} \vz_i$, then $\vw_i \vardet{\varepsilon}{D} \vz_i$.
Since $\contextfunc$ respects the constraints in $D$, $c_{\vz_i}$ is a tuple-subcontext of $c_{\vw_i}$ witnessed by $\varepsilon$, with $c_{\vz_i} = \contextfunc(\vz_i)$ and $c_{\vw_i} = \contextfunc(\vw_i)$.
Then, $c_{\vz_i} = c_{\vw_i}$, and in particular $c_{\vz_i}(\varepsilon) = c_{\vw_i}(\varepsilon)$.
By Lemma <ref>, $\barmu(\vz_i) = c_{\vz_i}(\varepsilon) = c_{\vw_i}(\varepsilon) = \barmu(\vw_i)$. Since $\barmu$ is admissible for $\db$, the constraint $\vw_i \neq \vz_i$ cannot exist.
(<ref>) Since $\contextfunc$ respects the constraints in $D$, it follows from Conditions (<ref>) and (<ref>) in Definition <ref> that the tuple-subcontext of $c'_{q_i}$ witnessed by $F_1$ is equal to the tuple-subcontext of $c'_{r_i}$ witnessed by $F_2$.
As a result, the subcontext of $c_{q_i} = \lambda \circ c'_{r_i}$ witnessed by $F_1$ is equal (up to isomorphisms over variables) to the subcontext of $c_{r_i} = \lambda \circ c'_{r_i}$ witnessed by $F_2$.
(<ref>) Analogous to the previous case, we can conclude that $c_{q_i}(F_1) = \lambda \circ c'_{q_i}(F_1)$ and $c_{r_i}(F_2) = \lambda \circ c'_{r_i}(F_2)$ are either two different tuples, or both a variable.
(<ref>) If $c_{q_i}(F_1) = \lambda \circ c'_{q_i}(F_1) = \lambda \circ c'_{r_i}(F_2) = c_{r_i}(F_2)$ is a tuple, then $c'_{q_i}(F_1) = c'_{r_i}(F_2)$. Since $\contextfunc$ respects the constraints in $D$, it follows that there is no constraint $\vw_i \neq vz_i$.
(<ref>) If $\myvar{q_i} \vardet{F}{\tau_i} \myvar{r_i}$, then $c'_{r_i}$ is a tuple-subcontext of $c'_{q_i}$, as $\contextfunc$ respects the constraints of $D$. By construction of $c_{q_i}$ and $c_{r_i}$ based on respectively $c'_{q_i}$ and $c'_{r_i}$, it immediately follows that $c_{r_i}$ is a subcontext of $c_{q_i}$.
The case for $\vy_i \vardet{F}{\tau_i} \vx_i$ is analogous.
(<ref>) Assume towards a contradiction that $c_{q_i}(F) = c_{q_1}(F')$ is a tuple for some $q_1 \in \{o_1, p_1\}$ and some sequence of function names $F$ and $F'$,
and there is an operation $o_i' \in \tau_i$ potentially ww-conflicting with an operation $o_1' \in \prefix{\tau_1}{o_1}$ with
$\myvar{q_i} \vardet{F}{\tau_i} \myvar{o_i'}$ and $\myvar{q_1} \vardet{F'}{\tau_1} \myvar{o_1'}$.
Since $c_{q_i}(F) = c_{q_1}(F')$ is a tuple, $c'_{q_i}(F) = c_{q_i}(F) = c_{q_1}(F') = c'_{q_1}(F')$.
By definition of $\barmu$ and since $\contextfunc$ respects the constraints in $D$, we conclude that $\barmu(o_i')$ in $\barmu(\tau_i)$ is ww-conflicting with $\barmu(o_1')$ in $\prefix{\barmu(\tau_1)}{\barmu(o_1)}$, thereby contradicting Condition (<ref>) of Definition <ref>.
(<ref>) Since $E$ is based on $C$, the operation $o_i$ is potentially conflicting with $p_j$. Furthermore, since $\myvar{o_i} \varequiv{D} \myvar{p_j}$ and since $\contextfunc$ respects the constraints of $D$, $c'_{o_i} = c'_{p_j}$, and hence $c_{o_i} = c_{p_j}$.
(<ref>) Immediate by Condition (<ref>) of Definition <ref>.
(<ref>) Immediate by Condition (<ref>) of Definition <ref>.

Central to the correctness of the if-direction of Lemma <ref> is the observation that for any sequence $E$ satisfying the stated conditions, we can assign tuples to variables in each context, thereby replacing contexts with tuple-contexts, in such a way that the resulting context assignment over tuple-contexts respects the constraints of the corresponding  $D$. This observation is formalized in the following Lemma:

Let $E = (\tau_1, o_1, c_{o_1}, p_1, c_{p_1}), \ldots, (\tau_m, o_m, c_{o_m}, p_m, c_{p_m})$ be a sequence of quintuples satisfying the conditions stated in Lemma <ref>, and let $D = (\tau_1, o_1, p_2, \tau_2), \ldots, (\tau_m, o_m,\allowbreak p_1, \tau_1)$ be the  derived from $E$.
Then a partial context assignment $\contextfunc$ over a set of tuple-contexts $\contextset$ exists such that

* for every pair of operations $o_i$ and $p_i$ occurring in $D$, $\contextfunc$ is defined for  $\myvar{o_i}$ and $\myvar{p_i}$;

* $\contextfunc$ respects the constraints in $D$; and

* for every  $\tau_i$ in $D$ with $i \neq 1$ and for every $q_i \in \{o_i, p_i\}$ and $q_1 \in \{o_1, p_1\}$, let $c_{q_i} = \contextfunc(\myvar{q_i})$ and  $c_{q_1} = \contextfunc(\myvar{q_1})$.
If $c_{q_i}(F) = c_{q_1}(F')$ for some sequence of function names $F$ and $F'$,
then there is no operation $o_i' \in \tau_i$ potentially ww-conflicting with an operation $o_1' \in \prefix{\tau_1}{o_1}$ with
$\myvar{q_i} \vardet{F}{\tau_i} \myvar{o_i'}$ and $\myvar{q_1} \vardet{F'}{\tau_1} \myvar{o_1'}$.

The general proof idea is as follows. We iteratively extend $\contextfunc$ by deriving $\contextfunc(\myvar{o_i})$ and $\contextfunc(\myvar{p_i})$ from contexts $c_{o_i}$ and $c_{p_i}$ for each quintuple $(\tau_i, o_i, c_{o_i}, p_i, c_{p_i})$ in the order that they appear in $E$.
Afterwards, we argue that $\contextfunc$ respects the constraints in $D$
and for every $q_i \in \{o_i, p_i\}$ with $i \neq 1$ and $q_1 \in \{o_1, p_1\}$ with $c_{q_i} = \contextfunc(\myvar{q_i})$ and  $c_{q_1} = \contextfunc(\myvar{q_1})$, and for every pair of sequences of function names $F$ and $F'$ with $c_{q_i}(F) = c_{q_1}(F')$,
there is no operation $o_i' \in \tau_i$ potentially ww-conflicting with an operation $o_1' \in \prefix{\tau_1}{o_1}$ with
$\myvar{q_i} \vardet{F}{\tau_i} \myvar{o_i'}$ and $\myvar{q_1} \vardet{F'}{\tau_1} \myvar{o_1'}$.

Let $(\tau_1, o_1, c_{o_1}, p_1, c_{p_1})$ be the first quintuple in the sequence $E$. We initiate $\contextfunc$ by defining $\contextfunc(\myvar{o_1}) = c_{o_1}$ and $\contextfunc(\myvar{p_1}) = c_{p_1}$.
Next, we iteratively extend $\contextfunc$ by considering the remaining quintuples in $E$ in order.
To this end, let $(\tau_{i-1}, o_{i-1}, c_{o_{i-1}}, p_{i-1}, c_{p_{i-1}})$ be the last considered quintuple and $(\tau_i, o_i, c_{o_i}, p_i, c_{p_i})$ the next quintuple in $E$.
We define $\contextfunc(\myvar{p_i}) = c'_{p_i} = \contextfunc(\myvar{o_{i-1}})$ and $\contextfunc(\myvar{o_i}) = c'_{o_i} = \lambda_i \circ c_{o_i}$,
where $\lambda_i: \objects \cup \variables \to \objects$ is a function mapping tuples and variables occurring in $c_{o_i}$ to tuples such that[Note that $\lambda_i$ is defined over variables in the context $c_{o_i}$. These variables are unrelated to the variables occurring in $\transcopies{D}$. We therefore denote these variables by $\vq$ instead of the usual $\vw, \vx, \vy, \vz$ to avoid confusion.]

* $\lambda_i(\x) = \x$ for each tuple $\x$ occurring in $c_{o_i}$;

* $\lambda_i(\vq) = \y$ for each variable $\vq$ occurring in $c_{o_i}$ for which there is a variable $\vz$ in $\tau_i$ and sequences of function names $F$, $F'$ and $F''$
with $\myvar{p_i} \vardet{F}{\tau_i} \vz$, $\myvar{o_i} \vardet{F'}{\tau_i} \vz$, $c'_{p_i}(F \cdot F'') = \y$ and $c_{o_i}(F' \cdot F'') = \vq$; and

* $\lambda_i(\vq) = \x_{i,\vq}$, for the remaining variables $\vq$ in $c_{o_i}$ where $\x_{i,\vq}$ is a fresh tuple.

Note that this $\lambda_i$ is well defined. In particular, the second rule intuitively states that the tuple-subcontext of the resulting $c'_{o_i}$ witnessed by $F'$ is equal to the tuple-subcontext of $c'_{p_i}$ witnessed by $F$, given that there is a variable $\vz$ with $\myvar{o_i} \vardet{F'}{\tau_i} \vz$ and $\myvar{p_i} \vardet{F}{\tau_i} \vz$.
This substitution is well defined since in this case the subcontext of $c_{o_i}$ witnessed by $F'$ is equal (up to isomorphisms over variables) to the subcontext of $c_{p_i}$ witnessed by $F$ according to Condition <ref> of Lemma <ref>.

It remains to show that $\contextfunc$ indeed satisfies the conditions stated in Lemma <ref>. To this end, note that by definition of variable determination,
if $\vx \vardet{F}{D} \vy$ with $\vx$ in a  $\tau_i$ and $\vy$ in a  $\tau_i$ in $\transcopies{D}$,
then a sequence of variables $\vx_{k_1}, \vy_{k_1}, \ldots, \vx_{k_m}, \vy_{k_m}$ exists such that $(\dagger)$:

* $\vx_{k_1} = \vx$ and $\vy_{k_m} = \vy$;

* each pair of (not necessarily different) variables $\vx_{k_i}, \vy_{k_i}$ occur in the same  $\tau_{k_i}$ in $\transcopies{D}$ and $\vx_{k_i}, \vardet{F_i}{\tau_{k_i}} \vy_{k_i}$ with $F = F_1 \cdot \ldots, F_m$;

* in the implied sequence of  $\tau_{k_1}, \ldots, \tau_{k_m}$, these $\tau_{k_i}, \ldots, \tau_{k_{i+1}}$ are neighbouring in $E$ (where we assume that $\tau_1$ is neighbouring to $\tau_n$ in $E$); and

* for each pair of variables $\vy_{k_i}, \vx_{k_{i+1}}$, there is a sequence of function names $F'$ such that $\myvar{o_{k_i}} \vardet{F'}{\tau_{k_i}} \vy_{k_i}$ and $\myvar{p_{k_{i+1}}} \vardet{F'}{\tau_{k_{i+1}}} \vx_{k_{i+1}}$
(i.e., equivalence of $\vy_{k_i}$ and $\vx_{k_{i+1}}$ in $D$ is implied by equivalence of $\myvar{o_{k_i}}$ and $\myvar{p_{k_{i+1}}}$).

In other words, $\vx \vardet{F}{D} \vy$ can be broken down into a sequence of $\vx_{k_i} \vardet{F_i}{\tau_{k_i}} \vy_{k_i}$ through a sequence of neighbouring , where equivalence between each $\vy_{k_i}$ and $\vx_{k_{i+1}}$ is implied by the variables in the potentially conflicting operations $o_{k_i}$ and $p_{k_{i+1}}$.
For ease of exposition, we implicitly assumed that $\tau_{k_1}, \ldots, \tau_{k_m}$ agrees with the order in $E$. If the order is opposite to the order in $E$ instead, the above still holds, but the occurrences of $o_{k_i}$ and $p_{k_{i+1}}$ should be replaced with $p_{k_i}$ and $o_{k_{i+1}}$.

We argue by construction of $\contextfunc$ that for every pair of variables $\vx$ and $\vy$ for which $\contextfunc$ is defined with $c_\vx = \contextfunc(\vx)$ and $c_\vy = \contextfunc(\vy)$,
if $c_\vx(F) = c_\vy(F')$ for some sequence of function names $F$ and $F'$, then $c'_\vx = c'_\vy$, where $c'_\vx$ and $c'_\vy$ are the tuple-subcontexts of $c_\vx$ witnessed by $F$ and $c_\vy$ witnessed by $F'$, respectively $(\ddagger)$.
If $\vx = \myvar{o_1}$ and $\vy =\myvar{p_1}$ (or the other way around), the result is immediate by Lemma <ref> (<ref>).
Otherwise, let $\vx$ be the variable in a  $\tau_i$ and $\vy$ the variable in a  $\tau_j$ such that $j \leq i$ (i.e., $\tau_i$ does not occur before $\tau_j$ in $E$).
W.l.o.g., we assume that $\vx = \myvar{o_i}$ with $i \neq 1$ (the case where $\vx = \myvar{p_i}$ is analogous, as $\contextfunc(\myvar{p_i}) = \contextfunc(\myvar{o_{i-1}})$ by construction).
By construction of each $c'_{o_i}$ based on $c'_{p_i}$ and $\lambda_i$, if $c'_{o_i}(F_i) = c'_{p_i}(F_i')$, then the whole tuple-subcontext of $c'_{o_i}$ witnessed by $F_i$ is copied over from the tuple-subcontext of $c'_{p_i}$ witnessed by $F_i'$. Indeed $\lambda_i$ introduces fresh tuples whenever the tuple for $c'_{o_i}(F_i)$ is not implied by $c'_{p_i}$.

The desired properties now follow from $(\dagger)$ and $(\ddagger)$ as well as the conditions in Lemma <ref>.
In particular, $\contextfunc$ respecting the constraints of $D$ can now be derived from Conditions (<ref>, <ref>, <ref>-<ref>) in Lemma <ref>,
and the last condition of Lemma <ref> follows from Condition (<ref>) in Lemma <ref>.

A algorithm proving the correctness of Theorem <ref> is now immediate by Lemma <ref>, as we can iteratively guess and verify quintuples in $E$ while only keeping track of the very first quintuple and the previous quintuple. Since in an acyclic schema graph the number of paths starting in a given type is at most exponential in the total number of types, each context is defined over at most an exponential number of paths. However, to formally argue that these contexts can be encoded in exponential space, we still need to show that each tuple or variable used in a context can be encoded in at most exponential space. Since the only tuples used are those mentioned in $c_{o_1}$ and $c_{p_1}$, and since we can reuse the same variables over all contexts, both the maximal number of tuples and the maximal number of variables needed are exponential in the total number of types.

§.§ Lowering complexity

Next, we consider restrictions that lower the complexity. To this end,
we say that two variables $\vx$ and $\vy$ occurring in a  $\tau$ are equivalent in $\tau$, denoted $\vx \varequiv{\tau} \vy$ if

* $\vx = \vy$;

* there exists a pair of variables $\vz$ and $\vw$ in $\tau$ and a sequence of function names $F$ with $\vz \varequiv{\tau} \vw$, $\vz \varimplies{F}{\tau} \vx$ and $\vw \varimplies{F}{\tau} \vy$; or

* there exists a variable $\vz$ with $\vx \varequiv{\tau} \vz$ and $\vy \varequiv{\tau} \vz$.

Then, a  $\tau$ is  if for every combination of variables $\vx, \vy, \vw, \vz$ in $\tau$ with $\vx \varimplies{}{\tau} \vw$ and $\vy \varimplies{}{\tau} \vz$,
either $\vw \varequiv{\tau} \vz$, $\vw \varimplies{}{\tau} \vz$ or $\vz \varimplies{}{\tau} \vw$.
We denote by $\acycrestemplates$ the class of all sets of  over acyclic schemas.

*  is decidable in .

*  is decidable in when the number of paths between any two nodes in the schema graph is bounded by a constant $k$.

Regarding (1), all templates in TPC-C with the exception of NewOrder are restricted. Regarding (2), when the schema graph is a multi-tree then $k=1$ and for TPC-C $k=2$ (recall that in general there can be an exponential number of paths), leading to a more practical algorithm for robustness in those cases.

The result in Theorem <ref> for workloads over a schema $(\schRel, \schFunc)$ where the number of paths between any two nodes in the schema graph is bounded by a constant $k$ is immediate by the nondeterministic algorithm based on Lemma <ref> presented for Theorem <ref>. Indeed, in this case, the total number of paths starting in a given type is at most $k . |\schRel|$ and therefore each context is defined over at most a polynomial number of paths, instead of an exponential number of paths for the general case in Theorem <ref>.

The result in Theorem <ref> for workloads in follows from a deterministic algorithm based on Lemma <ref>. In the remainder of this section, we first present the algorithm, and then discuss its complexity.

*A deterministic algorithm

Towards a deterministic algorithm, assume the first quintuple $(\tau_1, o_1, c_{o_1}, p_1, c_{p_1})$ of $E$ is fixed. We now translate the problem of deciding whether we can extend $E$ such that it satisfies all properties to a graph problem over a graph $G(\tau_1, o_1, c_{o_1}, p_1, c_{p_1})$. This graph is constructed as follows:

* each quintuple $(\tau_i, o_i, c_{o_i}, p_i, c_{p_i})$ satisfying Conditions (<ref>-<ref>) of Lemma <ref> is added as a node to $G(\tau_1, o_1, c_{o_1}, p_1, c_{p_1})$; and

* there is an edge from a node $(\tau_i, o_i, c_{o_i}, p_i, c_{p_i})$ to a node $(\tau_j, o_j, c_{o_j}, p_j, c_{p_j})$ if $o_i$ is potentially conflicting with $p_j$ and $c_{o_i} = c_{p_j}$ (c.f. Condition (<ref>) of Lemma <ref>).

By construction, it is now easy to see that there is a sequence $E$ satisfying Lemma <ref> if there is a path from a quintuple $(\tau_2, o_2, c_{o_2}, p_2, c_{p_2})$ to a quintuple $(\tau_m, o_m, c_{o_m}, p_m, c_{p_m})$ in $G(\tau_1, o_1, c_{o_1}, p_1, c_{p_1})$ (where we allow a zero-length path with $2 = m$), such that $(\dagger)$

* $c_{o_1} = c_{p_2}$ and $c_{o_m} = c_{p_1}$ (c.f. Condition (<ref>) of Lemma <ref>);

* $o_1$ is potentially rw-conflicting with $p_2$ (c.f. Condition (<ref>) of Lemma <ref>); and

* $o_1 <_{\tau_1} p_1$ or $o_m$ is potentially rw-conflicting with $p_1$ (c.f. Condition (<ref>) of Lemma <ref>).

Given a set of  $\workload$ over a schema $(\schRel, \schFunc)$,
the algorithm iterates over all possible quintuples $(\tau_1, o_1, c_{o_1}, p_1, c_{p_1})$ satisfying Condition (<ref>, <ref>-<ref>) of Lemma <ref>,
where we consider all possible tuple-contexts $c_{o_1}$ and $c_{p_1}$ up to isomorphisms.
For each such quintuple, the graph $G(\tau_1, o_1, c_{o_1}, p_1, c_{p_1})$ is constructed. Let $TC$ be the reflexive-transitive closure of $G$.
If there is a pair of quintuples $(\tau_2, o_2, c_{o_2}, p_2, c_{p_2})$ and $(\tau_m, o_m, c_{o_m}, p_m, c_{p_m})$ in $TC$ satisfying $(\dagger)$, the algorithm emits a reject, indicating that $\workload$ is not robust against $\mvrc$.
Otherwise, it proceeds with a new choice for $(\tau_1, o_1, c_{o_1}, p_1, c_{p_1})$. If, the algorithm didn't reject after considering all such quintuples, it accepts, indicating that $\workload$ is indeed robust against .
The correctness of this algorithm is immediate by Lemma <ref>.

*Complexity analysis

We show the complexity of the presented algorithm.
For this, first, notice that we have defined contexts $c$ based on a type $S$ (with $S$ not necessarily a root of ). For encoding purposes it makes sense to encode these as contexts for a root type $R$ in combination with the intended type $S$. The context as defined in the previous section can then be derived by taking the left-most subtree with root $S$. Notice that this is purely an encoding choice that will simplify the analysis.

For a schema graph $\sg{\schRel, \schFunc}$ the total number of non-isomorphic tuple-contexts can be expressed using Bell's number $B(n)$, denoting the number of partitions for a set of size $n$, and the set $\pathr = \{ (R,F,S) \mid R \asgimplies{F}{\sgname} S \}$ expressing the different paths from one node $R$ to another node $S$ in $\sgname$.

\[
\ssize{\tcontextdomain[SG]} \le \sum_{R\in \roots(\sgname)}\prod_{S\in \schRel} B(\pathrcount) = B^*
\]

where $\tcontextdomain[SG]$ denotes the set containing all different tuple-contexts (up to isomorphisms).

Now let $c_1$ and $c_2$ be two fixed contexts for types that are descendants of roots $R_1$ and root $R_2$, respectively, in , and let $c$ be a context for a type descending from root $R$.
To express a bound on the number of substitutions in $c$ from (parts of) $c_1$ and $c_2$, we need some additional terminology: Let $\pathr[R,*] = \bigcup_{S\in \schRel}\pathr$. We say that a path $R \asgimplies{F_1}{\sgname} S$ is a prefix of a path $R \asgimplies{F}{\sgname} S'$ in  if there is a (possibly empty) sequence of function names $F_2$ with $F = F_1 \cdot F_2$.
The number of substitutions in $c$ from (parts of) $c_1$ and $c_2$ is now bounded by

\begin{equation*}
\begin{split}
\sum_{\text{Part} \subseteq \pathr[R,*]}\indicator[PFP]\prod_{R \asgimplies{F}{\sgname} S \in \text{Part}} \left(|\pathr[R_1, S]| + |\pathr[R_2,S]|\right)
&\le T^\ell.(2P)^\ell \\
&\le (2TP)^\ell
\end{split}
\end{equation*}

In the above expression, $\indicator[PFP]$ is an indicator variable that equals $1$ if no path in Part is a prefix of another path in Part and that equals $0$ otherwise. Further:
$P$ denotes the maximum number of different paths between a particular root and a particular node in , $T$ denotes the maximum number of different paths from a particular root to nodes in SG, and $\ell$ denotes the maximal size of a set in which no path is a prefix of another path in the set. The latter is trivially bounded by $T$.

A special cases exists if all templates $\tau$ in $\workload$ are .
In that case, the size of sets $\text{Part}$ is bounded by $2$, hence $\ell \le 2$.

With the above bounds, the complexity of the presented algorithm is rather straightforward.
The iteration over all possible quintuples $(\tau_1, o_1, c_{o_1}, p_1, c_{p_1})$ requires at most $\ssize{\workload} . t^2.\left(B^*\right)^2$ iterations, with $t$ denoting the maximal number of operations in a  of $\workload$.
The remainder of the computation is dominated by the transitive-closure computation. Since the constructed graph $G(\tau_1, o_1, c_{o_1}, p_1, c_{p_1})$ has at most $\ssize{\workload}.t^2.\left(B^*.(2TP)^\ell\right)^2$ nodes, the transitive closure computation requires $\left(\ssize{\workload}.t^2.\left(B^*.(2TP)^\ell\right)^2\right)^3$ steps.  Putting these numbers together, we obtain:

\[\mathcal{O}(\ssize{\workload}^4.t^8.\left(B^*\right)^8.(2TP)^{6\ell}).
\]

Since $\ell$ is bounded by a constant if all  are , and since $B^*$, $T$ and $P$ can be exponential in the size of the input, the presented algorithm indeed decides  in .

§ RELATED WORK

*Transaction Programs Previous work on static robustness testing [14, 2] for transaction programs is based on the following key insight: when a schedule is not serializable, then the dependency graph constructed from that schedule contains a cycle satisfying a condition specific to the isolation level at hand (dangerous structure for and the presence of a counterflow edge for ). That insight is extended to a workload of transaction programs through the construction of a so-called static dependency graph where each program is represented by a node, and there is a conflict edge from one program to another if there can be a schedule that gives rise to that conflict.  The absence of a cycle satisfying the condition specific to that isolation level then guarantees robustness while the presence of a cycle does not necessarily imply non-robustness.

Other work studies robustness within a framework for uniformly specifying different isolation levels in a declarative way [9, 8, 10]. A key assumption here is atomic visibility requiring that either all or none of the updates of each transaction are visible to other transactions.
These approaches aim at higher isolation levels and cannot be used for , as does not admit atomic visibility.

*Transaction Templates
The static robustness approach based on transaction templates [19] differs in two ways. First, it makes more underlying assumptions explicit within the formalism of transaction templates (whereas previous work departs from the static dependency graph that should be constructed in some way by the dba). Second, it allows for a decision procedure that is sound and complete for robustness testing
against , allowing to detect larger subsets of transactions to be robust [19].

The formalization of transactions and conflict serializability in [19] and this paper is based on [13], generalized to operations over attributes of tuples and extended with $\myUP$-operations that combine $\myR$- and $\myW$-operations into one atomic operation. These definitions are closely related to the formalization presented by Adya et al. [3], but we assume a total rather than a partial order over the operations in a schedule.
There are also a few restrictions to the model: there needs to be a fixed set of read-only attributes that cannot be updated and which are used to select tuples for update. The most typical example of this are primary key values passed to transaction templates as parameters.
The inability to update primary keys is not an important restriction in many workloads, where keys, once assigned, never get changed, for regulatory or data integrity reasons.

In [19], a decision procedure is obtained for robustness against RC for templates without functional constraints and the present paper improves that result to .
In addition,
an experimental study was performed showing how an approach based on robustness and making transactions robust through promotion can improve transaction throughput.

Fekete [13] is the first work that provides a necessary and sufficient condition for deciding robustness against for a workload of concrete transactions (not transaction programs).
That work provides a characterization for acceptable allocations when every transaction runs under either
or strict two-phase locking (S2PL).
The allocation then is acceptable when every possible execution respecting the allocated isolation levels is serializable. As a side result, this work indirectly provides a necessary and sufficient condition for robustness against , since robustness against holds iff the allocation where each transaction is allocated to is acceptable.
Ketsman et al. [15] provide full characterizations for robustness against and under lock-based semantics. In addition, it is shown that the corresponding decision problems are complete for and , respectively, which should be contrasted with the polynomial time characterization obtained in [19] for robustness against multiversion read committed.

§ CONCLUSION

This paper falls within a more general research line
investigating how transaction throughput can be improved through an approach based on robustness testing that can be readily applied  without making any changes to the underlying database system. As argued in Section <ref>, incorporating functional constraints can detect larger sets of templates to be robust and requires less $\myR$-operations to be promoted to $\myUP$-operations. In future work, we plan to look at lower bounds,  restrictions that lower complexity, and consider other referential integrity constraints to further enlarge the modelling power of transaction templates.

§ ACKNOWLEDGMENT

This work is funded by FWO-grant G019921N.

[1]
Mohammad Alomari, Michael Cahill, Alan Fekete, and Uwe Rohm.
The cost of serializability on platforms that use snapshot isolation.
In ICDE, pages 576–585, 2008.

[2]
Mohammad Alomari and Alan Fekete.
Serializable use of read committed isolation level.
In AICCSA, pages 1–8, 2015.

[3]
Atul Adya, Barbara Liskov, and Patrick E. O'Neil.
Generalized isolation level definitions.
In ICDE, pages 67–78, 2000.

[4]
Sidi Mohamed Beillahi, Ahmed Bouajjani, and Constantin Enea.
Checking robustness against snapshot isolation.
In CAV, pages 286–304, 2019.

[5]
Sidi Mohamed Beillahi, Ahmed Bouajjani, and Constantin Enea.
Robustness against transactional causal consistency.
In CONCUR, pages 1–18, 2019.

[6]
Hal Berenson, Philip A. Bernstein, Jim Gray, Jim Melton, Elizabeth J. O'Neil,
and Patrick E. O'Neil.
A critique of ANSI SQL isolation levels.
In SIGMOD, pages 1–10, 1995.

[7]
Peter Bailis, Aaron Davidson, Alan Fekete, Ali Ghodsi, Joseph M. Hellerstein,
and Ion Stoica.
Highly available transactions: Virtues and limitations.
PVLDB, 7(3):181–192, 2013.

[8]
Giovanni Bernardi and Alexey Gotsman.
Robustness against consistency models with atomic visibility.
In CONCUR, pages 7:1–7:15, 2016.

[9]
Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman.
A framework for transactional consistency models with atomic
In CONCUR, pages 58–71, 2015.

[10]
Andrea Cerone and Alexey Gotsman.
Analysing snapshot isolation.
J.ACM, 65(2):1–41, 2018.

[11]
Andrea Cerone, Alexey Gotsman, and Hongseok Yang.
Algebraic Laws for Weak Consistency.
In CONCUR, pages 26:1–26:18, 2017.

[12]
Ashok K. Chandra and Moshe Y. Vardi.
The implication problem for functional and inclusion dependencies is
SIAM J. Comput., 14(3):671–677, 1985.

[13]
Alan Fekete.
Allocating isolation levels to transactions.
In PODS, pages 206–215, 2005.

[14]
Alan Fekete, Dimitrios Liarokapis, Elizabeth J. O'Neil, Patrick E. O'Neil, and
Dennis E. Shasha.
Making snapshot isolation serializable.
ACM Trans. Database Syst., 30(2):492–528, 2005.

[15]
Bas Ketsman, Christoph Koch, Frank Neven, and Brecht Vandevoort.
Deciding robustness for lower SQL isolation levels.
In PODS, pages 315–330, 2020.

[16]
Christos H. Papadimitriou.
The Theory of Database Concurrency Control.
Computer Science Press, 1986.

[17]
Emil L. Post.
A variant of a recursively unsolvable problem.
Bull. Amer. Math. Soc., pages 264–268, 1946.

[18]
On-line transaction processing benchmark.

[19]
Brecht Vandevoort, Bas Ketsman, Christoph Koch, and Frank Neven.
Robustness against read committed for transaction templates.
PVLDB, 14(11):2141–2153, 2021.

[20]
Brecht Vandevoort, Bas Ketsman, Christoph Koch, and Frank Neven.
Robustness against read committed for transaction templates with
functional constraints.
In ICDT, pages 16:1–16:17, 2022.

§ SMALLBANK BENCHMARK SQL CODE