has to occur

Robustness against RC for Transaction Templates with Functional Constraints]Robustness against Read Committed for Transaction Templates with Functional Constraints

*The present paper is the full version of [20] and supplies all proofs.

B. Vandevoort]Brecht Vandevoort0000-0001-7212-4625[a]
B. Ketsman]Bas Ketsman0000-0002-4032-0709[b]
C. Koch]Christoph Koch0000-0002-9130-7205[c]
F. Neven]Frank Neven0000-0002-7143-1903[a]

UHasselt, Data Science Institute, ACSL, Belgium

<EMAIL_ADDRESS><EMAIL_ADDRESS>
Vrije Universiteit Brussel, Belgium

École Polytechnique Fédérale de Lausanne, Switzerland

The popular isolation level Multiversion Read Committed (RC) trades some of the strong guarantees of serializability for increased transaction throughput.
Sometimes, transaction workloads can be safely executed under RC obtaining serializability at the lower cost of RC.
Such workloads are said to be robust against RC. Previous work has yielded a tractable procedure for deciding robustness against RC for workloads generated by transaction programs modeled as transaction templates. An important insight of that work is that, by more accurately modeling transaction programs, we are able to recognize larger sets of workloads as robust.
In this work, we increase the modeling power of transaction templates by extending them with functional constraints, which are useful for capturing data dependencies like foreign keys. We show that the incorporation of functional constraints can identify more workloads as robust that otherwise would not be. Even though we establish that the robustness problem becomes undecidable in its most general form, we show that various restrictions on functional constraints lead to decidable and even tractable fragments that can be used to model and test for robustness against RC for realistic scenarios.

§ INTRODUCTION

Many database systems implement several isolation levels, allowing users to trade isolation guarantees for improved performance. The highest, serializability, projects the appearance of a complete absence of concurrency, and thus perfect isolation. Executing transactions concurrently under weaker isolation levels can introduce certain anomalies. Sometimes,
a transactional workload can be executed at an isolation level lower than serializability without introducing any anomalies. This is a desirable scenario: a lower isolation level, usually implementable with a cheaper concurrency control algorithm, yields the stronger isolation guarantees of serializability
for free.
This formal property is called robustness [13, 8]: a set of transactions $\transset$ is called robust against a given isolation level if every possible interleaving of the transactions in $\transset$ that is allowed under the specified isolation level is serializable.

Robustness received quite a bit of attention in the literature.
Most existing work focuses on Snapshot Isolation (SI) [1, 4, 13, 14] or higher isolation levels [5, 8, 9, 11].
It is particularly interesting to consider robustness against lower level isolation levels like multi-version Read Committed (referred to as from now on). Indeed,  is widely available, often the default in database systems (see, e.g., [7]), and is generally expected to have better throughput than stronger isolation levels.

In previous work [19], we provided a tractable decision procedure for robustness against for workloads generated by transaction programs modeled as transaction templates. The approach is centered on a novel characterization of robustness against in the spirit of [13, 15] that improves over the sufficient condition presented in [2], and on a formalization of transaction programs, called transaction templates, facilitating fine-grained reasoning for robustness against .
Conceptually, transaction templates as introduced in [19] are functions with parameters, and can, for instance, be derived from stored procedures inside a database system (c.f. Figure <ref>  for an example).  The abstraction generalizes transactions as usually studied in concurrency control research – sequences of read and write operations – by making the objects worked on variable, determined by input parameters. Such parameters are typed to add additional power to the analysis. They support atomic updates (that is, a read followed by a write of the same database object, to make a relative change to its value). Furthermore, database objects read and written are considered at the granularity of fields, rather than just entire tuples, decoupling conflicts further and allowing to recognize additional cases that would not be recognizable as robust on the tuple level.

An important insight obtained from [19] is that more accurate modeling of the workload allows to recognize larger sets of transaction programs as robust. Processing workloads under RC increases the throughput of the transactional database system compared to when executing the workload under SI or serializable SI, so larger robust sets mean better performance of the database system.

In this work, we increase the modeling power of transaction templates by extending them with functional constraints, which are useful for capturing data dependencies like foreign keys (inclusion dependencies). This appears to be a sweet spot for strengthening modelling power – as we show in this paper,
it allows us to remain with abstractions that have been well established within database theory, without having to move to general program analysis,
and it pushes the robustness frontier on popular transaction processing benchmarks. Generally speaking, workloads can profit more from richer modelling the larger and more complex they get, so the fact that adding functional constraints yields larger robust sets already on these simple benchmarks suggests that these techniques are practically useful.

Our contributions can be summarized as follows:

* We argue in Section <ref> through the SmallBank and TPC-C benchmarks that the incorporation of functional constraints can identify more workloads as robust that otherwise would not be, and that they reduce the extent to which changes need to be made to workloads to make them robust against RC.

* In Section <ref>, we establish that robustness in its most general form becomes undecidable. The proof is a reduction from PCP and relies on cyclic dependencies between functions allowing to connect data values through an unbounded application of functions.

* We consider a fragment in Section <ref> that only allows a very limited form of cyclic dependencies between functions and assumes additional constraints on templates that, together, imply that functions behave as bijections. Robustness against RC can be decided in and this fragment is general enough to model the SmallBank benchmark.

* In Section <ref>, we obtain an decision procedure when the schema graph is acyclic (so, no cyclic dependencies between functions).
Even for small input sizes, such a result is not practical. We provide various restrictions that lower the complexity to and , and which allow to model the TPC-C benchmark as discussed.
Notice that, for robustness testing, an exponential time decision procedure is considered to be practical as the size of the input is small and robustness is a static property that can be tested offline.

These contributions should be contrasted with our earlier work [19], where we focused on a characterization for robustness against for basic  without functional constraints and performed an experimental study to show how the robustness property can improve transaction throughput.

§ APPLICATION

We present a small extension of the SmallBank benchmark [1] to exemplify the modeling power of transaction templates and discuss how the addition of functional constraints can detect larger sets of transaction templates to be robust. Finally, we discuss in the context of the TPC-C benchmark how the incorporation of functional constraints requires less changes to templates in making them robust.

The SmallBank schema consists of three tables:
Account(Name, CustomerID, IsPremium),
Savings(CustomerID, Balance, InterestRate), and
Checking(CustomerID, Balance).
Underlined attributes are primary keys.
The table associates customer names with IDs and keeps track of the premium status (Boolean); CustomerID is a UNIQUE attribute. The other tables contain the balance (numeric value) of the savings and checking accounts of customers identified by their ID. (CustomerID) is a foreign key referencing both the columns
(CustomerID) and (CustomerID).
The interest rate on a savings account is based on a number of parameters, including the account status (premium or not).
The application code can interact with the database through a fixed number of transaction programs:

* Balance($N$): returns the total balance (savings & checking) for a customer with name $N$.

* DepositChecking($N$,$V$): makes a deposit of amount $V$
on the checking account of the customer with name $N$.

* TransactSavings($N$,$V$): makes a deposit or withdrawal $V$ on the savings account of the customer with name $N$.

* Amalgamate($N_1$,$N_2$): transfers all the funds from
$N_1$ to

* WriteCheck($N$,$V$): writes a check $V$ against the account of the customer with name $N$, penalizing if overdrawing.

* GoPremium($N$): converts the account of the customer with name $N$ to a premium account and updates the interest rate of the corresponding savings account.  This transaction program is an extension w.r.t. [1].

The transaction templates for these programs are presented in Figure <ref>.
The corresponding SQL code is given in Appendix <ref>.

\[
\begin{array}{l}
\R[]{\vx: \Account\ListAttr{N, C}}\\
\R[]{\vy: \Savings\ListAttr{C, B}}\\
\R[]{\vz: \Checking\ListAttr{C, B}}\\
\vy = \fas(\vx),\ \vx = \fsa(\vy)\\
\vz = \fac(\vx),\ \vx = \fca(\vz)
\end{array}
\]

\[
\begin{array}{l}
\R[]{\vx: \Account\ListAttr{N, C}}\\
\UP[]{\vz: \Checking\ListAttr{C, B}\ListAttr{B}}\\
\vz = \fac(\vx),\ \vx = \fca(\vz)
\end{array}
\]

\[
\begin{array}{l}
\R[]{\vx: \Account\ListAttr{N, C}}\\
\UP[]{\vy: \Savings\ListAttr{C, B}\ListAttr{B}}\\
\vy = \fas(\vx),\ \vx = \fsa(\vy)
\end{array}
\]

\[
\begin{array}{l}
\R[]{\vx_1: \Account\ListAttr{N, C}}\\
\R[]{\vx_2: \Account\ListAttr{N, C}}\\
\UP[]{\vy_1: \Savings\ListAttr{C, B}\ListAttr{B}}\\
\UP[]{\vz_1: \Checking\ListAttr{C, B}\ListAttr{B}}\\
\UP[]{\vz_2: \Checking\ListAttr{C, B}\ListAttr{B}}\\
\vx_1\neq \vx_2,\\
\vy_1 = \fas(\vx_1),\ \vx_1 = \fsa(\vy_1)\\
\vy_2 = \fas(\vx_2),\ \vx_2 = \fsa(\vy_2)\\
\vz_1 = \fac(\vx_1),\ \vx_1 = \fca(\vz_1)\\
\vz_2 = \fac(\vx_2),\ \vx_2 = \fca(\vz_2)
\end{array}
\]

\[
\begin{array}{l}
\R[]{\vx: \Account\ListAttr{N, C}}\\
\R[]{\vy: \Savings\ListAttr{C, B}}\\
\R[]{\vz: \Checking\ListAttr{C, B}}\\
\UP[]{\vz: \Checking\ListAttr{C, B}\ListAttr{B}}\\
\vy = \fas(\vx),\ \vx = \fsa(\vy)\\
\vz = \fac(\vx),\ \vx = \fca(\vz)
\end{array}
\]

\[
\begin{array}{l}
\UP[]{\vx: \Account\ListAttr{N, C}\ListAttr{I}}\\
\R[]{\vy: \Savings\ListAttr{C, I}}\\
\UP[]{\vy:\Savings\ListAttr{C}\ListAttr{I}}\\
\vy = \fas(\vx),\ \vx = \fsa(\vy)
\end{array}
\]

Transaction templates for SmallBank.

In short, a transaction template is a sequence of read (), write () and update () statements over typed variables ($\vx$, $\vy$, …) with additional equality and disequality constraints. For instance, $\R[]{\vy :\Savings\{C,I\}\}}$ in  indicates that a read operation is performed to a tuple in relation $\Savings$ on the attributes CustomerID and InterestRate. We abbreviate the names of attributes by their first letter to save space. The set $\{C,I\}$ is the read set.
Write operations have an associated write set while update operations contain a read set followed by a write set: e.g.,
$\UP[]{\vx :\Account\{N,C\}\{I\}\}}$ in  first reads the Name and CustomerID of tuple $\vx$ and then writes to the attribute InterestRate.
To capture the dependencies between tuples induced by the foreign keys, we use two unary functions:  $\f$ maps a tuple of type to a tuple of type , while $\g$ maps a tuple of type to a tuple of type . As (CustomerID) is UNIQUE, every savings and checking accounts is associated to a unique tuple. This is modelled through the functions $\fca$ and $\fsa$ with an analogous interpretation. Notice that the equality constraints for each template in Figure <ref> imply that these functions are bijections and each others inverses.

A transaction $T$ over a database $\bf D$ is an instantiation of a transaction template $\tau$ if there is a variable mapping $\mu$ from the variables in $\tau$ to tuples in $\bf D$ that satisfies all the constraints in $\tau$ such that with $\mu(\tau)=T$.
For instance, consider a database $\bf D$ with tuples $\mya_1,\mya_2,\ldots$ of type ,
$\mys_1,\mys_2,\ldots$ of type , and $\myc_1,\myc_2,\ldots$ of type  with $\fas^{\bf D}(\mya_i)=\mys_i$, $\fac^{\bf D}(\mya_i)=\myc_i$, $\fsa^{\bf D}(\mys_i)=\mya_i$, $\fca^{\bf D}(\myc_i)=\mya_i$ for each $i$.
Then, for $\mu_1=\{\vx\to \mya_1, \vy\to\mys_1\}$,
$\mu_1(\GoPremium)=\UP[]{\mya_1}\R[]{\mys_1}\UP[]{\mys_1}$ is an instantiation of GoPremium whereas $\mu_2(\GoPremium)$ with $\mu_2=\{\vx\to \mya_1, \vy\to\mys_2\}$ is not as the functional constraint $\vy=\fas(\vx)$ is not satisfied. Indeed, $\mu_2(\vy)=\mys_2\neq\mys_1=\fas^{\bf D}(\mya_1)=\fas^{\bf D}(\mu_2(\vx))$.
We then say that a set of transactions is consistent with a set of templates if every transaction is an instantiation of a transaction template.

Functional constraints do not replace the more usual data consistency constraints like key constraints, functional dependencies or denial constraints, …. The latter are intended to verify data consistency, whereas the former are intended to verify whether a set of transactions instantiated from  are indeed consistent with these .
The abstraction of functional constraints provides a straightforward mechanism to capture dependencies between tuples implied by e.g. foreign key constraints. Consider for example variables $\vx$ and $\vy$ in . Rather than specifying that the value of the attribute in the tuple assigned to $\vx$ should agree with the value of the attribute in the tuple assigned to $\vy$ and combining this information with the defined foreign key from to to conclude that two instantiations of that agree on the tuple assigned to $\vx$ should also agree on the tuple assigned to $\vy$, the functional constraint $\vy = \fas(\vx)$ expresses this dependency more directly.
An additional benefit of our abstraction is that this approach is not limited to dependencies implied by foreign keys. For the SmallBank benchmark, for example, we can infer from the fact that (CustomerID) is UNIQUE that each checking and savings account is associated to exactly one tuple, even though no foreign key from respectively and to is defined in the schema.

Our previous work [19], which did not consider functional constraints, has shown that {Am,DC,TS}, {Bal,DC}, and {Bal,TS} are maximal robust sets of transaction templates. This means that for any database, for any set of transactions $\transset$ that is consistent with one of the three mentioned sets, any possible interleaving of the transactions in $\transset$ that is allowed under RC is always serializable!
Using the results from Section <ref>, it follows that when functional constraints are taken into account GoPremium can be added to each of these sets as well: {Am,DC,GP,TS}, {Bal,DC,GP}, {Bal,TS,GP} are maximal robust sets.

We argue that incorporating functional constraints is crucial. Indeed, without functional constraints it's easy to show that even the set $\{\GoPremium\}$ is not robust. Consider the schedule  over two instantiations $\trans[1]$ and $\trans[2]$ of , where we use the mappings $\mu_1$
and $\mu_2$ as defined above
for respectively $\trans[1]$ and $\trans[2]$ (we show the read and write sets to facilitate the discussion):

\arraycolsep=.1em
\begin{array}{lcccc}
\trans[1]:\,  \UP[1]{\mya_1\ListAttr{N,C}\ListAttr{I}} \, \R[1]{\mys_1\ListAttr{C,I}} \, & & \UP[1]{\mys_1\ListAttr{C}\ListAttr{I}} \, \CT[1]\\
\trans[2]:& \UP[2]{\mya_2\ListAttr{N,C}\ListAttr{I}} \, \R[2]{\mys_1\ListAttr{C,I}} \, \UP[2]{\mys_1\ListAttr{C}\ListAttr{I}} \, \CT[2]&
\end{array}

The above schedule is allowed under RC as there is no dirty write, but it is not conflict serializable. Indeed, there is a rw-conflict between $\R[1]{\mys_1\ListAttr{C,I}}$ and $\UP[2]{\mys_1\ListAttr{C}\ListAttr{I}}$ as the former reads the attribute $I$ that is written to by the latter, which implies that $T_1$ should occur before $T_2$ in an equivalent serial schedule. But, there is a ww-conflict between $\UP[2]{\mys_1\ListAttr{C}\ListAttr{I}}$ and $\UP[1]{\mys_1\ListAttr{C}\ListAttr{I}}$ as both write to
the common attribute $I$ implying that $T_2$ should occur before $T_1$ in an equivalent serial schedule. Consequently, the schedule is not serializable.
However, taking functional constraints into account, $\{T_1,T_2\}$ is not consistent with $\{\GoPremium\}$ as $\mu_2(\vy)=\mys_1\neq \mys_2 = \fas(a_2)=\fas(\mu_2(\vx))$ implying that the above schedule is not a counter example for robustness.

The second benchmark is based on the TPC-C benchmark [18]. We modified the schema and  to turn all predicate reads into key-based accesses.
The schema consists of six relations:

* Warehouse(WarehouseID, Info, YTD),

* District(WarehouseID, DistrictID, Info, YTD, NextOrderID),

* Customer(WarehouseID, DistrictID, CustID, Info, Balance),

* Order(WarehouseID, DistrictID, OrderID, CustID, Status),

* OrderLine(WarehouseID, DistrictID, OrderID, OrderLineID, ItemID, DeliveryInfo, Quantity), and

* Stock(WarehouseID, ItemID, Quantity).

The function names belonging to this schema are given in Table <ref>.

$f$     $\dom{f}$     $\range{f}$

$\fdisttowh$     $\District$     $\Warehouse$

$\fcusttodist$     $\Customer$     $\District$

$\fordtocust$     $\Order$     $\Customer$

$\flinetoord$     $\OrderLine$     $\Order$

$\flinetostock$     $\OrderLine$     $\Stock$

$\fstocktowh$     $\Stock$     $\Warehouse$

Function names for the TPC-C benchmark schema.

We focus on five different :

* NewOrder($W$, $D$, $C$, $I_1$, $Q_1$, $I_2$, $Q_2$, …): creates a new order for the customer identified by $(W,D,C)$. The id for this order is obtained by increasing the NextOrderID attribute of the District tuple identified by $(W,D)$ by one. Each order consists of a number of items $I_1, I_2, \ldots$ with respectively quantities $Q_1, Q_2, \ldots$. For each of these items, a new OrderLine tuple is created and the related stock quantity is decreased.

* Payment($W$, $D$, $C$, $A$): represents a customer identified by $(W,D,C)$ paying an amount $A$. This payment is reflected in the database by increasing the balance of this customer by $A$. This amount is furthermore added to the YearToDate (YTD) income of both the related warehouse and district.

* OrderStatus($W$, $D$, $C$, $O$): requests information about the current status of the order identified by $(W,D,O)$. This  collects information of the customer identified by $(W,D,C)$ who created the order, the order itself, and the different OrderLine tuples related to this order.

* Delivery($W$, $D$, $C$, $O$): delivers the order represented by $(W,D,O)$. The status of the order is updated, as well as the DeliveryInfo attribute of each OrderLine tuple related to this order. The total price of the order is deduced from the balance of the customer who made this order, identified by $(W,D,C)$.

* StockLevel($W$, $I$): returns the current stock level of item $I$ in warehouse $W$.

A detailed abstraction of each  is given in Figure <ref>. To shorten the presentation, we only show two orderlines per order.

\[
\begin{array}{l}
\R[]{\vx: \Warehouse\ListAttr{W, Inf}}\\
\UP[]{\vy: \District\ListAttr{W, D, Inf, N}\ListAttr{N}}\\
\R[]{\vz: \Customer\ListAttr{W, D, C, Inf}}\\
\W[]{\myvs: \Order\ListAttr{W, D O, C, Sta}}\\
\UP[]{\vt_1: \Stock\ListAttr{W, I, Qua}\ListAttr{Qua}}\\
\W[]{\myvv_1: \OrderLine\ListAttr{W, D, O, OL, I, Del, Qua}}\\
\UP[]{\vt_2: \Stock\ListAttr{W, I, Qua}\ListAttr{Qua}}\\
\W[]{\myvv_2: \OrderLine\ListAttr{W, D, O, OL, I, Del, Qua}}\\
\vx = \fdisttowh(\vy),\ \vy = \fcusttodist(\vz),\ \vz = \fordtocust(\myvs)\\
\myvs = \flinetoord(\myvv_1),\ \myvs = \flinetoord(\myvv_2)\\
\vt_1 = \flinetostock(\myvv_1),\ \vt_2 = \flinetostock(\myvv_2)\\
\vx = \fstocktowh(\vt_1),\ \vx = \fstocktowh(\vt_2)
\end{array}
\]

\[
\begin{array}{l}
\UP[]{\vx: \Warehouse\ListAttr{W, YTD}\ListAttr{YTD}}\\
\UP[]{\vy: \District\ListAttr{W, D, YTD}\ListAttr{YTD}}\\
\UP[]{\vz: \Customer\ListAttr{W, D, C, Bal}\ListAttr{Bal}}\\
\vx = \fdisttowh(\vy),\ \vy = \fcusttodist(\vz)\\
\phantom{\myvs = \flinetoord(\myvv_1),\ \myvs = \flinetoord(\myvv_2)}
\end{array}
\]

\[
\begin{array}{l}
\R[]{\vz: \Customer\ListAttr{W, D, C, Inf, Bal}}\\
\R[]{\myvs: \Order\ListAttr{W, D, O, C, Sta}}\\
\R[]{\myvv_1: \OrderLine\ListAttr{W, D, O, OL, I, Del, Qua}}\\
\R[]{\myvv_2: \OrderLine\ListAttr{W, D, O, OL, I, Del, Qua}}\\
\vz = \fordtocust(\myvs),\ \myvs = \flinetoord(\myvv_1),\ \myvs = \flinetoord(\myvv_2)
\end{array}
\]

\[
\begin{array}{l}
\UP[]{\myvs: \Order\ListAttr{W, D, O}\ListAttr{Sta}}\\
\UP[]{\myvv_1: \OrderLine\ListAttr{W, D, O, OL, Del}\ListAttr{Del}}\\
\UP[]{\myvv_2: \OrderLine\ListAttr{W, D, O, OL, Del}\ListAttr{Del}}\\
\UP[]{\vz: \Customer\ListAttr{W, D, C, Bal}\ListAttr{Bal}}\\
\vz = \fordtocust(\myvs),\ \myvs = \flinetoord(\myvv_1),\ \myvs = \flinetoord(\myvv_2)
\end{array}
\]

\[
\begin{array}{l}
\R[]{\vt: \Stock\ListAttr{W, I, Qua}}\\
\phantom{\myvs = \flinetoord(\myvv_1),\ \myvs = \flinetoord(\myvv_2)}
\end{array}
\]

Abstraction for the TPC-C . Attribute names are abbreviated.

Incorporating functional constraints for TPC-C can not identify larger sets of templates to be robust. However,
when a set of  $\workload$ is not robust against , an equivalent set of  $\workload'$ can be constructed from $\workload$ by promoting certain $\myR$-operations to $\myUP$-operations [19]. By incorporating functional constraints it can be shown that fewer $\myR$-operations need to be promoted leading to an increase in throughput as $\myR$-operations do not take locks whereas
$\myUP$-operations do.
Consider for example the subset $\workload = \{\text{Delivery}, \text{OrderStatus}\}$ of the TPC-C benchmark, given in Figure <ref>, where functional constraints are added to express the fact that a tuple of type OrderLine implies the tuple of type Order (function $\flinetoord$), which in turn implies the tuple of type Customer (function $\fordtocust$).
This set $\workload$ is not robust against , but robustness can be achieved by promoting the $\myR$-operation over Customer in OrderStatus to a $\myUP$-operation.
However, without functional constraints, this single promoted operation no longer guarantees robustness, as witnessed by the following schedule:

\arraycolsep=.1em
\begin{array}{lcccc}
\trans[1] \text{(Orderstatus)}:\,  \UP[1]{c} \, \R[1]{a} \, & & \R[1]{b_1} \, \R[1]{b_2} \, \CT[1]\\
\trans[2] \text{(Delivery)}:& \UP[2]{a} \, \UP[2]{b_1} \, \UP[2]{b_2} \, \UP[2]{c'} \, \CT[2]&
\end{array}

Notice in particular how this schedule implicitly assumes in $\trans[2]$ that Order $\mathtt{a}$ belongs to Customer $\mathtt{c'}$ instead of Customer $\mathtt{c}$ to avoid a dirty write on $\mathtt{c}$. Without functional constraints,
$\workload$ is only robust against if all $\myR$-operations in OrderStatus are promoted to $\myUP$-operations.

§ DEFINITIONS

We recall the necessary definitions from [19] and extend them with functional constraints.

§.§ Databases

A relational schema is a pair $(\schRel,\schFunc)$ where $\schRel$ is a set of relation names and $\schFunc$ is a set of function names.
A finite set of attribute names $\Attr{R}$ is associated to every relation $R\in\schRel$.
Relations will be instantiated by abstract objects that serve as an abstraction of relational tuples. To this end, for every relation $R\in\schRel$, we fix an infinite set of tuples
Furthermore, we assume that $\objectsRes{R} \cap \objectsRes{S} = \emptyset$ for all  $R,S\in\schRel$ with $R\neq S$. We then denote by $\objects$ the set $\bigcup_{R\in\schRel} \objectsRes{R}$ of all possible tuples. Notice that, by definition, for every $\x\in\objects$ there is a unique relation $R \in \schRel$ such that $\x\in\objectsRes{R}$.
In that case, we say that $\x$ is of type $R$ and denote the latter by $\type{\x}=R$. Each function name $f\in \schFunc$ has a domain $\dom{f}\in\schRel$ and a range $\range{f}\in\schRel$. Functions are used to encode relationships between tuples like for instance those implied by foreign-keys constraints. For instance, in the SmallBank example $\schFunc=\{f_{A\to S},f_{A\to C}\}$, $\dom{f_{A\to S}}=\dom{f_{A\to C}}=A$,
$\range{f_{A\to S}}=S$, and $\range{f_{A\to C}}=C$.
A database $\db$ over schema $(\schRel,\schFunc)$ assigns to every relation name $R\in \schRel$ a finite set $R^{\db} \subset\objectsRes{R}$ and to every function name $f \in \schFunc$ a function $f^{\db}$ from $\dom{f}^{\db}$ to $\range{f}^{\db}$.

§.§ Transactions and Schedules

For a tuple $\x \in \objects$, we distinguish three operations $\R[]{\x}$, $\W[]{\x}$, and $\UP[]{\x}$ on $\x$, denoting that tuple $\x$ is read, written, or updated, respectively. We say that the operation is on the tuple $\x$.
The operation $\UP[]{\x}$ is an atomic update and should be viewed as an atomic sequence of a read of $\x$ followed by a write to $\x$.
We will use the following terminology: a read operation is an $\R[]{\x}$ or a $\UP[]{\x}$, and a write operation is a $\W[]{\x}$ or a $\UP[]{\x}$. Furthermore, an -operation is an $\R[]{\x}$, a -operation is a $\W[]{\x}$, and a -operation is a $\UP[]{\x}$.
We also assume a special commit operation denoted $\CT[]$.
To every operation $o$ on a tuple of type $R$, we associate the set of attributes
$\ReadSet{o}\subseteq\Attr{R}$ and $\WriteSet{o}\subseteq\Attr{R}$ containing, respectively, the set of attributes that $o$ reads from and writes to. When $o$ is a $\myR$-operation then $\WriteSet{o}=\emptyset$. Similarly, when $o$ is a $\myW$-operation then $\ReadSet{o}=\emptyset$.

A transaction $\trans[]$
is a sequence of read and write operations
followed by a commit.
We assume that a transactions starts when its first operation is executed, but no earlier.
Formally, we model a transaction as a linear order $(\trans[],\leq_{\trans[]})$, where $\trans[]$ is the set of (read, write and commit) operations occurring in the transaction and $\leq_{\trans[]}$ encodes the ordering of the operations. As usual, we use $<_{\trans[]}$ to denote the strict ordering.

When considering a set $\transset$ of transactions, we assume that every transaction in the set has a unique id $i$ and write $\trans$ to make this id explicit. Similarly, to distinguish the operations of different transactions, we add this id as a subscript to the operation. That is, we write $\W{\x}$, $\R{\x}$, and $\UP{\x}$ to denote a $\W[]{\x}$, $\R[]{\x}$, and $\UP[]{\x}$ occurring in transaction $\trans$; similarly $\CT[i]$ denotes the commit operation in transaction $T_i$.
This convention is consistent with the literature (see, [6, 13]).
To avoid ambiguity of notation, we assume that a transaction performs at most one write, one read, and one update per tuple.
The latter is a common assumption (see,  [13]). All our results carry over to the more general setting in which multiple writes and reads per tuple are allowed.

A (multiversion) schedule $\schedule$ over a set $\transset$ of transactions is a tuple $(O_\schedule, \leq_\schedule, {\ll_\schedule,} v_\schedule)$ where $O_\schedule$ is the set
containing all operations of transactions in $\transset$ as well as a special operation $\sstart$ conceptually writing the initial versions of all existing tuples, $\leq_\schedule$ encodes the ordering of these operations, $\ll_\schedule$ is a version order providing for each tuple $\x$ a total order over all write operations on $\x$ occurring in $\schedule$, and $v_\schedule$ is a version function mapping each read operation $a$ in $\schedule$ to either $\sstart$ or to a write[Recall that a write operation is either a $\W[]{x}$ or a $\UP[]{x}$.] operation different from $a$ in $\schedule$.
We require that $\sstart \leq_\schedule a$ for every operation $a \in {O_\schedule}$, $\sstart \ll_\schedule a$ for every write operation $a \in {O_\schedule}$, and that $a <_{\trans[]} b$ implies $a <_\schedule b$ for every $\trans[] \in \transset$ and every $a,b \in \trans[]$.[Recall that $<_{\trans[]}$ denotes the order of operations in transaction $\trans[]$.]
We furthermore require that for every read operation $a$, $v_\schedule(a) <_\schedule a$ and, if $v_\schedule(a) \neq \sstart$, then the operation $v_\schedule(a)$ is on the same tuple as $a$.
Intuitively, $\sstart$ indicates the start of the schedule, the order of operations in $s$ is consistent with the order of operations in every transaction $\trans[]\in\transset$, and the version function maps each read operation $a$ to the operation that wrote the version observed by $a$.
If $v_\schedule(a)$ is $\sstart$, then $a$ observes the initial version of this tuple.
The version order $\ll_\schedule$ represents the order in which different versions of a tuple are installed in the database. For a pair of write operations on the same tuple, this version order does not necessarily coincide with $\leq_\schedule$. For example, under the version order is based on the commit order instead.

We say that a schedule $\schedule$ is a single version schedule if $\ll_\schedule$ coincides with $\leq_\schedule$ and every read operation always reads the last written version of the tuple. Formally, for each pair of write operations $a$ and $b$ on the same tuple, $a \ll_\schedule b$ iff $a <_\schedule b$, and for every read operation $a$ there is no write operation $c$ on
the same tuple as $a$
with $v_\schedule(a) <_\schedule c  <_\schedule a$.
A single version schedule over a set of transactions $\transset$ is single version
serial if its transactions are not interleaved with operations from other transactions. That is, for every $a,b,c \in {O_\schedule}$ with $a <_{\schedule}
b<_{\schedule} c$ and $a,c \in \trans[]$ implies $b \in \trans[]$ for every
$\trans[] \in \transset$.

The absence of aborts in our definition of schedule is consistent with the common assumption [13, 8] that an underlying recovery mechanism will rollback aborted transactions. We only consider isolation levels that only read committed versions. Therefore there will never be cascading aborts.

§.§ Conflict Serializability

Let $a_j$ and $b_i$ be two operations on the same tuple from different transactions $\trans[j]$ and $\trans[i]$ in a set of transactions $\transset$. We then say that $a_j$ is conflicting with $b_i$ if:

* (ww-conflict) $\WriteSet{a_j} \cap \WriteSet{b_i} \neq \emptyset$; or,

* (wr-conflict) $\WriteSet{a_j} \cap \ReadSet{b_i} \neq \emptyset$; or,

* (rw-conflict) $\ReadSet{a_j} \cap \WriteSet{b_i} \neq \emptyset$.

In this case, we also say that $a_j$ and $b_i$ are conflicting operations.
Furthermore, commit operations and the special operation $\sstart$ never conflict with any other operation.
When $a_j$ and $b_i$ are conflicting operations in $\transset$, we say that $a_j$ depends on $b_i$ in a schedule $\schedule$ over $\transset$, denoted $b_i \rightarrow_\schedule a_j$ if:[Throughout the paper, we adopt the following convention:  a $b$ operation can be understood as a `before' while an $a$ can be interpreted as an `after'.]

* (ww-dependency) $b_i$ is ww-conflicting with $a_j$ and $b_i \ll_{\schedule} a_j$; or,

* (wr-dependency) $b_i$ is wr-conflicting with $a_j$ and $b_i = v_\schedule(a_j)$ or $b_i \ll_{\schedule} v_\schedule(a_j)$; or,

* (rw-antidependency) $b_i$ is rw-conflicting with $a_j$ and $v_\schedule(b_i) \ll_{\schedule} a_j$.

Intuitively, a ww-dependency from $b_i$ to $a_j$ implies that $a_j$ writes a version of a tuple that is installed after the version written by $b_i$.
A wr-dependency from $b_i$ to $a_j$ implies that $b_i$ either writes the version observed by $a_j$, or it writes a version that is installed before the version observed by $a_j$.
A rw-antidependency from $b_i$ to $a_j$ implies that $b_i$ observes a version installed before the version written by $a_j$.

Two schedules $\schedule$ and $\schedule'$ are conflict equivalent if they are over the same set $\transset$ of transactions and for every pair of conflicting operations $a_j$ and $b_i$, $b_i \rightarrow_\schedule a_j$ iff $b_i \rightarrow_{\schedule'} a_j$.

A schedule $\schedule$ is conflict serializable if it is conflict equivalent to a single version serial schedule.

A conflict graph $\cg{\schedule}$ for schedule $\schedule$ over a set of transactions $\transset$ is the graph whose nodes are the transactions in $\transset$ and where there is an edge from $T_i$ to $T_j$ if $T_i$ has an operation $b_i$ that conflicts with an operation $a_j$ in $T_j$ and $b_i \rightarrow_\schedule a_j$.
A schedule $\schedule$ is conflict serializable iff the conflict graph for
$\schedule$ is acyclic.

§.§ Multiversion Read Committed

Let $\schedule$ be a schedule for a set $\transset$ of transactions.
Then, $\schedule$ exhibits a dirty write
iff there are two ww-conflicting operations $a_j$ and $b_i$ in $\schedule$ on the same tuple $\x$
with $a_j \in \trans[j]$, $b_i \in \trans[i]$ and $\trans[j] \neq \trans[i]$
such that $b_i <_\schedule a_j <_\schedule \CT[i].$
That is, transaction $T_j$ writes to an attribute of a tuple that has
been modified earlier by $T_i$, but $T_i$ has not yet issued a commit.

For a schedule $\schedule$, the version order $\ll_\schedule$ corresponds to the commit order in $\schedule$ if for every pair of write operations $a_j \in \trans[j]$ and $b_i \in \trans[i]$, $b_i \ll_\schedule a_j$ iff $\CT[i] <_\schedule a_j$.
We say that a schedule $\schedule$ is read-last-committed (RLC) if $\ll_\schedule$ corresponds to the commit order and for every read operation $a_j$ in $\schedule$ on some tuple $\x$ the following holds:

* $v_\schedule(a_j) = \sstart$ or $\CT[i] <_\schedule a_j$ with $v_\schedule(a_j) \in \trans[i]$; and

* there is no write[Recall that a write operation is either a $\myW$ or a $\myUP$-operation.] operation $c_k \in \trans[k]$ on $\x$ with $\CT[k] <_\schedule a_j$ and $v_\schedule(a_j) {\ll_\schedule} c_k$.

So, $a_j$ observes the most recent version of $\x$ (according to the order of commits) that is committed before $a_j$. Note in particular that a schedule cannot exhibit dirty reads, defined in the traditional way [6], if it is read-last-committed.

A schedule is allowed under isolation level read committed (RC) if
it is read-last-committed and does not exhibit dirty writes.

are transactions where operations are defined over typed variables together with functional constraints on these variables. Types of variables are relation names in $\schRel$ and indicate that variables can only be instantiated by tuples from the respective type.
We fix an infinite set of variables $\variables$ that is disjoint from $\objects$. Every variable $\vx\in\variables$ has an associated relation name in $\schRel$ as type that we denote by $\type{\vx}$.
For an operation $o_i$ in a , $\myvar{o_i}$ denotes the variable in $o_i$.
An equality constraint is an expression of the form $\vx = f(\vy)$ where $\vx,\vy\in\variables$, $\dom{f}=\type{\vy}$ and $\range{f}=\type{\vx}$. A disequality constraint is an expression of the form $\vx\ne\vy$ where $\type{\vx}=\type{\vy}$.

A  is a transaction $\tau$
over $\variables$ together with a set
$\Cset(\tau)$ of equality and disequality constraints.
In addition, for every operation $o$ in $\tau$ over a variable $\vx$,
$\ReadSet{o}\subseteq \Attr{\type{\vx}}$ and $\WriteSet{o}\subseteq \Attr{\type{\vx}}$.

Recall that we denote variables by capital letters $\vx,\vy,\vz$ and tuples by small letters $\x,\y$.
A variable assignment $\mu$ is a mapping from $\variables$ to $\objects$
such that $\mu(\vx)\in \objects_{\type{\vx}}$.
Furthermore, $\mu$ satisfies a constraint $\vx = f(\vy)$ (resp., $\vx\ne\vy$) over a database $\db$ when $\mu(\vx) = f^{\db}(\mu(\vy))$ (resp., $\mu(\vx)\ne \mu(\vy)$).
A variable assignment $\tmap$ for a
$\tau$ is admissible for
$\db$ if
it satisfies all constraints in $\Cset(\tau)$ over $\db$.
By $\tmap (\templ[])$, we denote the transaction obtained by replacing each variable $\vx$ in $\templ[]$ with $\tmap (\vx)$.

A set of transactions $\transset$ is consistent with a set of  $\workload$ and
database $\db$, if for every transaction $\trans[]$ in $\transset$ there is a
$\tau\in \workload$ and a variable mapping $\mu_{\trans[]}$ that is admissible for $\db$ such that $\mu_{\trans[]}(\tau) = \trans[]$.

§.§ Robustness

We define the robustness property [8] (also called acceptability in [13, 14]), which guarantees serializability for all schedules of a given set of transactions for a given isolation level.

[Transaction Robustness]

A set $\transset$ of transactions is robust against RC
if every schedule for $\transset$ that is allowed under RC is
conflict serializable.

In the next definition, we represent conflicting operations from transactions in a set  $\transset$ as quadruples $(T_i, b_i, a_j, T_j)$ with $b_i$ and $a_j$ conflicting operations, and $T_i$ and $T_j$ their respective transactions in $\transset$. We call these quadruples  for $\transset$.
Further, for an operation $b\in \trans[]$, we denote by $\prefix{\trans[]}{b}$ the restriction of $\trans[]$ to all operations that are before or equal to $b$ according to $\leq_{\trans[]}$. Similarly, we denote by $\postfix{\trans[]}{b}$ the restriction of $\trans[]$ to all operations that are strictly after $b$ according to $\leq_{\trans[]}$. Throughout the paper, we interchangeably consider transactions both as linear orders as well as sequences.
Therefore, $\trans[]$ is then equal to the sequence $\prefix{\trans[]}{b}$ followed by $\postfix{\trans[]}{b}$ which we denote by $\prefix{\trans[]}{b}\cdot \postfix{\trans[]}{b}$ for every $b\in T$.

[t0](.5,1) rectangle (2.3,.7);         [t0](5.8,1) rectangle (7.5,.7);
[t0](2.4,.6) rectangle (3.5,.3);
[t0](3.6,.2) rectangle (4.7,-.1);
[t0](4.8,-.2) rectangle (5.7,-.5);
[anchor=west] at (0,.8) $T_1$;
[anchor=west] at (0,.4) $T_2$;
[anchor=west] at (0,.0) $T_3$;
[anchor=west] at (0,-.4) $T_4$;

(Aa) at (2.1,.85) $b_1$;          (Ab) at (6.75,.85) $a_1$;
(Ba) at (3,.45) $b_2$;
(Bb) at (3.3,.45) $a_2$;
(Ca) at (4.15,.05) $a_3$;
(Cb) at (4.45,.05) $b_3$;
(Da) at (5.2,-.35) $a_4$;
(Db) at (5.5,-.35) $b_4$;

[->](Aa) edge[bend left] node (Bb);
[->](Ba) edge[bend right] node (Ca);
[->](Cb) edge[bend left] node (Da);
[->](Db) edge[bend right] node (Ab);

[->](0,-.7) – (7.5,-.7);

Multiversion split schedule.

[Multiversion split schedule]
Let $\transset$ be a set of transactions and $C = (T_1, b_1, a_2, T_2), (T_2, b_2, a_3, T_3), \ldots, (T_m,\allowbreak b_m,\allowbreak a_1,\allowbreak T_1)$ a  for $\transset$ such that each transaction in $\transset$ occurs in at most two different quadruples. A multiversion split schedule for $\transset$ based on $C$ is a multiversion
schedule that has the following form:

$$ \prefix{\trans[1]}{b_1}\cdot \trans[2]\cdot \ldots \cdot \trans[m] \cdot \postfix{\trans[1]}{b_1}\cdot \trans[m+1] \cdot \ldots \cdot \trans[n],$$

*  there is no write operation in $\prefix{\trans[1]}{b_1}$ ww-conflicting with a write operation in any of the transactions $T_2, \ldots, T_m$;

*  $b_1 <_{\trans[1]} a_1$ or $b_{m}$ is rw-conflicting with $a_{1}$; and,

*  $b_{1}$ is rw-conflicting with $a_{2}$.

Furthermore, $\trans[m+1],\ldots,\trans[n]$ are the remaining transactions in $\transset$ (those not mentioned in $C$) in an arbitrary order.

Figure <ref> depicts a schematic multiversion split schedule. The name stems from the fact that the schedule is obtained by splitting one transaction in two ($T_1$ at operation $b_1$ in Figure <ref>) and placing all other transactions in $C$ in between. The figure does not display the trailing transactions $\trans[m+1], \trans[m+2], \ldots$ and assumes $b_1<_{T_1} a_1$.

The following theorem characterizes non-robustness in terms of the existence of a multiversion split schedule.
For a set of transactions $\transset$, the following are equivalent:

*  $\transset$ is not robust against ;

*  there is a multiversion split schedule $\schedule$ for $\transset$ based on some $C$.

Let $\workload$ be a set of  and $\db$ be a database.
Then, $\workload$ is robust against RC over $\db$ if for every set of transactions $\transset$ that is consistent with $\workload$ and $\db$, it holds that $\transset$ is robust against RC.

[ Robustness]
A set of
$\workload$ is robust against RC if $\workload$ is robust against RC for every database $\db$.

We say that a  $(\tau,\Cset)$ is a variable  when $\Cset=\emptyset$ and
an equality  when all constraints in $\Cset$ are equalities.
We denote these sets by and , respectively.
For an isolation level $\isolationlevel$ and a class of  $\classC$,  is the problem to decide if a given set of  $\workload\in \classC$ is robust against . When $\classC$ is the class of all , we simply write .
is decidable in .

In Section <ref> we start out with a negative result and argue that the addition of functional constraints in its most general form is undecidable by proving undecidability for . Notice in particular that the undecidability result does not even require disequalities.
To obtain decidable fragments, we introduce restrictions on the structure of functional constraints. The schema graph $\sg{\schRel, \schFunc}$ of a schema $(\schRel,\schFunc)$ is a directed multigraph having the relations in $\schRel$ as nodes, and in which there are as many edges from a node $R\in \schRel$ to node $S \in \schRel$ as there are functions $f \in \schFunc$ with $\dom{f} = R$ and $\range{f} = S$.
We say that a schema $(\schRel, \schFunc)$ is acyclic if the multigraph $\sg{\schRel, \schFunc}$ is acyclic and that it is a  if there is at most one directed path between any two nodes in $\sg{\schRel, \schFunc}$.

[draw, circle,text width=.8em,align=center] (P) at (0,0) $P$;
[draw, circle,text width=0.8em,align=center] (Q) at (2,0) $Q$;
[draw, circle,text width=0.8em,align=center] (R) at (1,-1) $R$;
[draw, circle,text width=0.8em,align=center] (S) at (2,-2) $S$;
[->] (P) – (R) node[midway,below left=-.5em] $f_{P,R}$;
[->] (Q) – (R) node[midway,above left=-.4em] $f_{Q,R}$;
[->] (R) – (S) node[midway,below left=-.5em] $f_{R,S}$;
[->, dashed] (Q) – (S) node[midway,right=-.2em] $f_{Q,S}$;

Acyclic schema graph over the schema $(\{P,Q,R,S\},\allowbreak \{f_{P,R},f_{Q,R},\allowbreak f_{R,S},\allowbreak f_{Q,S}\})$. If we remove function name $f_{Q,S}$ (dashed edge), the resulting schema graph is a multi-tree.

Consider the schema $(\{P,Q,R,S\}, \{f_{P,R},f_{Q,R},f_{R,S}\})$ with $\dom{f_{i,j}} = i$ and $\range{f_{i,j}} = j$ for each function $f_{i,j}$. The corresponding schema graph with solid lines is given in Figure <ref>. This schema is a multi-tree, as there is at most one path between any pair of nodes. Notice that the definition of a multi-tree is more general than a forest, as a node can still have multiple parents (e.g., node $R$ in our example).  Adding the function name $f_{Q,S}$ with $\dom{f_{Q,S}} = Q$ and $\range{f_{Q,S}} = S$ results in the schema graph given in Figure <ref>
that is still acyclic, but no longer a multi-tree as there are now two paths from $Q$ to $S$. $\Box$

The schema graph constructed in the proof of Theorem <ref> contains several cycles (cf., Figure <ref>).
We consider in Section <ref> robustness for a fragment where a restricted form of cycles in the schema graph is allowed but where
additional constraints on the  are assumed.
We consider robustness for acyclic schema graphs in Section <ref>.

§ ROBUSTNESS FOR

We start out with a negative result and show that the robustness problem in its most general form is undecidable (even when disequalities are not allowed).
The proof is a reduction from Post's Correspondence Problem (PCP) [17] and relies on cyclic dependencies between functional constraints.
The proof can be found in
the remainder of this section
and is quite elaborate but the basic intuition is simple:
the counterexample split schedule will build up the two strings that need to be generated by the PCP instance by repeated application of functional constraints.

is undecidable.

It might be tempting to relate the above result to the undecidability of the implication problem for functional and inclusion dependencies [12]. Functional constraints indeed allow to define inclusion dependencies (as in the SmallBank example) but they always relate complete tuples and are not suited to define functional dependencies. Furthermore, the proof of Theorem <ref> makes use of only unary relations, for which the implication problem for functional dependencies and inclusion dependencies is known to be decidable.

The remainder of this section is devoted to proving the correctness of Theorem <ref>. We first present the reduction from the PCP problem in Section <ref>. Afterwards, we show that this reduction is indeed correct by proving both directions in respectively Section <ref> and Section <ref>.

§.§ Reduction

\[
\begin{array}{l}
\W[]{\vx_1: Boolean} \\
\R[]{\vi : InitialConflict} \\
\R[]{\vs_1 : String} \\
\R[]{\vs_e : String} \\
\W[]{\vc:PCPSolution}\\
\vx_1 = \ufunc{is-non-empty}(\vs_1)\\
\vx_1 = \ufunc{is-error}(\vs_e)\\
\vc = \ufunc{final-domino-sequence}(\vi) \\
\vs_1 = \ufunc{final-dominoes-string}(\vi)\\
\vs_e = \ufunc{error-string}(\vi)\\
\vs_1 = \ufunc{solution-string}(\vc)  \\
\vi = \ufunc{defines}(\vx_1)
\end{array}
\]

\[
\begin{array}{l}
\W[]{\vx_2: Boolean} \\
\W[]{\vi: InitialConflict}\\
\R[]{\vs_0: String}\\
\R[]{\vs_e: String}\\
\R[]{\vs_1: String}\\
\W[]{\vb:DominoSequence}\\
\vx_2  = \ufunc{is-non-empty}(\vs_0)\\
\vx_2  = \ufunc{is-error}(\vs_0)\\
\vs_1 = \ufunc{final-dominoes-string}(\vi)\\
\vs_0  = \ufunc{top-string}(\vb)\\
\vs_0  = \ufunc{bottom-string}(\vb)\\
\vs_0 = \ufunc{empty-string}(\vb)\\
\vs_1 = \ufunc{future-solution-string}(\vb)\\
\vs_e = \ufunc{detach}(\vs_0) \\
\vs_e = \ufunc{detach}(\vs_e) \\
\vi = \ufunc{defines}(\vx_2) \\
\vb = \ufunc{empty-domino-sequence}(\vs_1)
\end{array}
\]

\[
\begin{array}{l}
\W[]{\vb:DominoSequence}\\
\R[]{\vs_t : String}\\
\R[]{\vs_b : String}\\
\R[]{\vs_1 : String}\\
\W[]{\vc:PCPSolution}\\
\vs_t  = \ufunc{top-string}(\vb)\\
\vs_b  = \ufunc{bottom-string}(\vb)\\
\vs_1 = \ufunc{future-solution-string}(\vb) \\
\vc = \ufunc{DS$\rightarrow$PCP}(\vb) \\
\vs_t = \ufunc{solution-string}(\vc) \\
\vs_b = \ufunc{solution-string}(\vc) \\
\vs_1 = \ufunc{solution-string}(\vc) \\
\vb = \ufunc{PCP$\rightarrow$DS}(\vc) \\
\end{array}
\]

For every domino $d_i = (a_1a_2\ldots a_h, b_1b_2\ldots b_k) \in \dominoset$ a  i($\vb$):

\[
\begin{array}{l}
\W[]{\vb:DominoSequence}\\
\R[]{\vs_0:String}\\
\R[]{\vs_1:String}\\
\R[]{\vs_t:String}\\
\R[]{\vs_{t\mathit{a_1}}:String}\\
\R[]{\vs_{t\mathit{a_1a_2}}:String}\\
\ldots\\
\R[]{\vs_{t\mathit{a_1a_2\ldots a_h}}:String}\\
\R[]{\vs_b:String}\\
\R[]{\vs_{b\mathit{b_1}}:String}\\
\R[]{\vs_{b\mathit{b_1b_2}}:String}\\
\ldots\\
\R[]{\vs_{b\mathit{b_1b_2\ldots b_k}}:String}\\
\W[]{\vb_{next}:DominoSequence}\\
\end{array}
\]

\[
\begin{array}{l}
\vs[t]  = \ufunc{top-string}(\vb)\\
\vs[t\mathit{a_1}] = \ufunc{append-$a_1$}(\vs[t])\\
\vs[t\mathit{a_1a_2}] = \ufunc{append-$a_2$}(\vs[t\mathit{a_1}])\\
\ldots\\
\vs[t\mathit{a_1a_2\ldots a_h}] = \\
\qquad\quad \ufunc{append-$a_h$}(\vs[t\mathit{a_1\ldots a_{h-1}}])\\
\vs[t]  = \ufunc{detach}(\vs[t\mathit{a_1}])\\
\vs[t\mathit{a_1}]  = \ufunc{detach}(\vs[t\mathit{a_1a_2}])\\
\ldots\\
\vs[t\mathit{a_1a_2\ldots a_{h-1}}]  =\\
\qquad\quad \ufunc{detach}(\vs[t\mathit{a_1a_2\ldots a_h}])\\
\vs[t\mathit{a_1a_2\ldots a_h}]  = \ufunc{top-string}(\vb_\text{next}) \\
\vs[\mathit{a_1}] = \ufunc{top}(\vs[t\mathit{a_1}]) \\
\vs[\mathit{a_2}] = \ufunc{top}(\vs[t\mathit{a_1a_2}]) \\
\ldots \\
\vs[\mathit{a_h}] = \ufunc{top}(\vs[t\mathit{a_1a_2\ldots a_h}]) \\
\vs_1 = \ufunc{future-solution-string}(\vb) \\
\vs_0 = \ufunc{empty-string}(\vb)
\end{array}
\]

\[
\begin{array}{l}
\vs[b]  = \ufunc{bottom-string}(\vb)\\
\vs[b\mathit{b_1}] = \ufunc{append-$b_1$}(\vs[b])\\
\vs[b\mathit{b_1b_2}] = \ufunc{append-$b_2$}(\vs[b\mathit{b_1}])\\
\ldots\\
\vs[b\mathit{b_1b_2\ldots b_k}] =\\
\qquad\quad \ufunc{append-$b_k$}(\vs[b\mathit{b_1\ldots b_{k-1}}])\\
\vs[b]  = \ufunc{detach}(\vs[t\mathit{b_1}])\\
\vs[b\mathit{b_1}]  = \ufunc{detach}(\vs[b\mathit{b_1b_2}])\\
\ldots\\
\vs[b\mathit{b_1b_2\ldots b_{k-1}}]  =\\
\qquad\quad \ufunc{detach}(\vs[b\mathit{b_1b_2\ldots b_k}])\\
\vs[b\mathit{b_1b_2\ldots b_k}]  =\\
\qquad\quad \ufunc{bottom-string}(\vb_\text{next}) \\
\vs[\mathit{b_1}] = \ufunc{top}(\vs[b\mathit{b_1}]) \\
\vs[\mathit{b_2}] = \ufunc{top}(\vs[b\mathit{b_1b_2}]) \\
\ldots\\
\vs[\mathit{b_k}] = \ufunc{top}(\vs[b\mathit{b_1b_2\ldots b_k}]) \\
\vs_1 = \ufunc{future-solution-string}(\vb_\text{next}) \\
\vs_0 = \ufunc{empty-string}(\vb_\text{next})\\
\vb_\text{next} = \ufunc{next-sequence}(\vb)\\
\vb = \ufunc{previous-sequence}(\vb_\text{next})
\end{array}
\]

for the proof of Theorem <ref>.

The proof is based on a reduction from the Post's Correspondence Problem (PCP), which is known to be undecidable [17].
A domino is a pair $(\vec{a}, \vec{b})$ of two non-empty strings over $\Sigma$.
Henceforth we call $\vec{a}$ its top value and $\vec{b}$ its bottom value.
Given a set of dominoes $\mathcal{D}$, the PCP asks if a non-empty sequence $d_1, d_2, \ldots, d_r$ of dominoes in $\mathcal{D}$ exists such that, with $d_i = (\vec{a_i}, \vec{b_i})$, the strings $\vec{a_1}\vec{a_2}\ldots\vec{a_r}$ and $\vec{b_1}\vec{b_2}\ldots\vec{b_r}$ are identical.

For the reduction to non-robustness against , we construct a set $\workload$ of  consisting of the  in Figure <ref> for $\dominoset$.
There are the transactions $\ttinit$, $\ttinitb$ and $\ttclose$ (whose meaning will be explained next) and for every domino in $\mathcal{D}$ there is a template in Figure <ref> representing that domino and the action of appending that domino to a sequence of dominoes.  The schema consists of the relations $\{
\text{\tt Boolean}, \text{\tt InitialConflict}, \text{\tt String},
\text{\tt PCPSolution}, \text{\tt DominoSequence}\}$ whose meaning will be explained below together with a discussion of all the functions.
The schema graph is presented in Figure <ref> and contains various cycles.

(IC)   at (.5,-.5)  InitialConflict;
(B)    at (1,-3) Boolean;
(PCP)  at (5,0) PCPSolution;
(S)    at (5,-2.5) String;
(D)    at (10,-1) DominoSequence;

[->,postaction=decorate,decoration=raise=0ex,text along path,text align=center,text=||defines] (B) to[bend left] (IC);
[<-,postaction=decorate,decoration=raise=0ex,text along path,text align=center,text=||is-non-empty] (B) to[bend right=40] (S);
[<-,postaction=decorate,decoration=raise=0ex,text along path,text align=center,text=||is-error] (B) to[bend right=20] (S);
[->,postaction=decorate,decoration=raise=0ex,text along path,text align=center,text=||final-domino-sequence] (IC) to[bend right=10] (S);
[->,postaction=decorate,decoration=raise=0ex,text along path,text align=center,text=||error-string] (IC) to[bend left=10] (S);
[->] (S) edge[out=330,in=300,looseness=6] nodetop (S);
[->] (S) edge[out=335,in=290,looseness=7] nodedetach (S);
[->] (S) edge[out=340,in=280,looseness=8] nodeappend-0 (S);
[->] (S) edge[out=345,in=270,looseness=10] nodeappend-1 (S);
[->] (D) edge[out=330,in=300,looseness=6] nodenext-sequence (D);
[->] (D) edge[out=335,in=290,looseness=7] nodeprevious-sequence (D);
[<-,postaction=decorate,decoration=raise=0ex,text along path,text align=center,text=||solution-string] (S) to[bend left] (PCP);
[->,postaction=decorate,decoration=raise=0ex,text along path,text align=center,text=||final-domino-sequence] (IC) to[bend left] (PCP);
[<-,postaction=decorate,decoration=raise=0ex,text along path,text align=center,text=||top-string] (S) to[bend left=5] (D);
[<-,postaction=decorate,decoration=raise=0ex,text along path,text align=center,text=||bottom-string] (S) to[bend left=15] (D);
[<-,postaction=decorate,decoration=raise=0ex,text along path,text align=center,text=||empty-string] (S) to[bend right=5] (D);
[<-,postaction=decorate,decoration=raise=0ex,text along path,text align=center,text=||future-solution-string]  (S) to[bend right=15] (D);
[->,postaction=decorate,decoration=raise=0ex,text along path,text align=center,text=||pcp-ds] (PCP) to[bend left] (D);
[<-,postaction=decorate,decoration=raise=0ex,text along path,text align=center,text=||ds-pcp] (PCP) to[bend left=20] (D);

Schema graph for the  in Figure <ref> (for any set of dominoes).

To prove Theorem <ref>, we will show that there is a solution for PCP if and only if $\workload$ is not robust against . For the only-if direction, we show that, if there is a solution $\vec{d} =d_1,d_2,\ldots,d_r$ for the PCP problem over $\mathcal{D}$, then there is a multiversion split schedule that encodes this solution in a particular way: in this schedule the split transaction is an instantiation of  $\ttinit$, the next transaction is an instantiation of $\ttinitb$, then followed by instantiations of  $\ttdomino{d_1}, \ldots, \ttdomino{d_r}$ representing the sequence of dominoes in solution $\vec{d}$, and finally an instantiation of  $\ttclose$. Henceforth, we call a schedule that encodes a sequence of dominoes $\vec{d}$ in this way a schedule-encoding of $\vec{d}$. For the if-direction, we first show that every multiversion split schedule consistent with the  in Figure <ref> for some set $\dominoset$ of dominoes is a schedule-encoding for some sequence $\vec{d}$ of dominoes from $\dominoset$, and then that for every schedule-encoding of a sequence $\vec{d}$ of dominoes, $\vec{d}$ is always a solution for the PCP problem over a set of dominoes containing those in $\vec{d}$.

§.§ Only-if direction
We first prove the only-if direction of Theorem <ref>.

Let $\dominoset$ be a set of dominoes with a solution $\vec{d}$ for the PCP problem for $\dominoset$. Then there exists a schedule-encoding of $\vec{d}$ that is consistent with the  in Figure <ref> and some database $\db$.

Let $\vec{d} = d_1,d_2,\ldots,d_r$ be a solution to the PCP problem for $\dominoset$. Let $\vec{a_1}\vec{a_2}\ldots\vec{a_r}$ be the
read of top values and $\vec{b_1}\vec{b_2}\ldots\vec{b_r}$ be the
read of bottom values, which thus represent an identical string $\vec{\charc} = \charc_1 \cdots \charc_n$, with $\charc_i \in \Sigma$.
We now construct a schedule $\schedule$ and database $\db$ as in Definition <ref> with transactions based on the  $\workload$ in Figure <ref>.

Relation  contains a tuple that we interpret as the PCP solution $\vec{d} = d_1,d_2,\ldots,d_r$. Relation  contains $r+1$ tuples, one for every prefix of $\vec{d}$, including the empty sequence $()$ and the PCP solution $\vec{d}$ itself. For convenience of notation, we will henceforth often represent tuples by their interpretation, which is justified by the fact that every tuple in a particular relation will have a different interpretation, and the relation itself can always be derived from the context (e.g., the function signature).

Since the PCP solution has an interpretation in both the relations  and , we assume two functions, $\ufunc{PCP$\rightarrow$DS}:\textsf{PCPSolution}\to\textsf{DominoSequence}$ and $\ufunc{DS$\rightarrow$PCP}:\textsf{DominoSequence}\to\textsf{PCPSolution}$ that map these interpretations on one another. That is,
$\ufunc{PCP$\rightarrow$DS}^{\db}(\vec{d}) = \vec{d}$ and $\ufunc{typecase-to-C}^{\db}(\vec{d}) = \vec{d}$.

Further, we have functions $\ufunc{next-sequence}:\textsf{DominoSequence}\to\textsf{DominoSequence}$ and $\ufunc{previous-sequence}:\textsf{DominoSequence}\to\textsf{DominoSequence}$ with following interpretation:

\begin{align*}
\ufunc{next-sequence}^{\db}(\vec{d'}) &= \vec{d'}d & \text{with $d'$ a strict prefix of $\vec{d}$ followed by domino $d$ in $\vec{d}$}, \\
\ufunc{next-sequence}^{\db}(\vec{d}) &= \vec{d}, \\
\ufunc{previous-sequence}^{\db}(\vec{d'}d) &= \vec{d'} &\text{with $d'$ a strict prefix of $\vec{d}$ followed by domino $d$ in $\vec{d}$}, \\
\ufunc{previous-sequence}^{\db}(()) &= ().
\end{align*}

Relation $\textsf{String}^{\db}$ contains a tuple representing the read $\vec{\charc}$ of PCP-solution sequence $\vec{d}$, a tuple representing an error $\langle\text{error}\rangle$, and a tuple for every substring of $\vec{\charc}$,
including the empty string $\langle\rangle$. We assume that all these tuples are different. We use notation $\langle\rangle$ to denote the empty string to distinguish it from $()$, which denotes the empty sequence of dominoes.

Functions $\ufunc{append-0}:\textsf{String}\to\textsf{String}$, $\ufunc{append-1}:\textsf{String}\to\textsf{String}$, $\ufunc{detach}:\textsf{String}\to\textsf{String}$, and $\ufunc{top}:\textsf{String}\to\textsf{String}$ simulate standard string operations for the interpretations of tuples in relation . Thus, tuples representing a (possibly empty) string $\vec{\chare}$:

\begin{align*}
\ufunc{append-\textit{c}}^{\db}(\langle\vec{\chare}\rangle) &= \left\{
\begin{array}{ll}
\langle\vec{\chare}c\rangle &\text{ with $\vec{\chare}$ a (possibly empty) string over $\Sigma$, $c \in \Sigma$, and} \\
& \text{ $\langle\vec{\chare}c\rangle$ a substring of $\vec{\charc}$,} \\
\langle\text{error}\rangle & \text{ otherwise},
\end{array}\right. \\
\ufunc{detach}^{\db}(\langle\vec{\chare}c\rangle) &= \langle\vec{\chare}\rangle  \text{ with $\vec{\chare}$ a (possibly empty) string over $\Sigma$, and $c \in \Sigma$}, \\
\ufunc{detach}^{\db}(\langle\rangle) &= \ufunc{detach}(\langle\text{error}\rangle) = \langle\text{error}\rangle, \\
\ufunc{top}^{\db}(\langle\vec{\chare}c\rangle) &= \langle c\rangle \text{ with $\vec{\chare}$ a (possibly empty) string over $\Sigma$, and $c \in \Sigma$},
\\
\ufunc{top}^{\db}(\langle\rangle) &= \ufunc{top}(\langle\text{error}\rangle) = \langle\text{error}\rangle.
\end{align*}

Notice that these function interpretations are closed under $\db$, that is, every tuple from relation $^\db$ maps onto a tuple that is in relation $^\db$.

Every tuple in  is associated with three tuples in  representing, respectively, the read of top values, the read of bottom values, and the empty string. The association is made via functions $\ufunc{top-string}:\textsf{DominoSequence}\to\textsf{String}$, $\ufunc{bottom-string}:\textsf{DominoSequence}\to\textsf{String}$, and $\ufunc{empty-string}:\textsf{DominoSequence}\to\textsf{String}$ with following interpretations in $\db$:

\begin{align*}
\ufunc{top-string}^{\db}(\vec{d'}) &= \vec{\chare} \text{, with $\vec{\chare}$ the read of top values on dominoes in $\vec{d'}$}, \\
\ufunc{bottom-string}^{\db}(\vec{d'}) &= \vec{\chare} \text{, with $\vec{\chare}$ the read of bottom values on dominoes in $\vec{d'}$, and} \\
\ufunc{empty-string}^{\db}(\vec{d'}) &= \langle\rangle.
\end{align*}

We emphasize that in the expressions above the read $\vec{\chare}$ of top and bottom values on dominoes in $\vec{d'}$ might be empty.

Finally, for function $\ufunc{future-solution-string}:\textsf{DominoSequence}\to\textsf{String}$ we consider the interpretation that associates every domino sequence $\vec{d'}$ represented by a tuple in relation  in $\db$ to the final read $\ufunc{future-solution-string}^{\db}(\vec{d'}) = \vec{\charc}$. Function $\ufunc{solution-string}:\textsf{PCPSolution}\to\textsf{String}$ does the same for the single tuple representing $\vec{d}$ in , thus with $\ufunc{solution-string}^{\db}(\vec{d}) = \vec{\charc}$.
Function $\ufunc{empty-domino-sequence}:\textsf{String}\to\textsf{DominoSequence}$ is interpreted to map every tuple in  onto the tuple from  representing the empty sequence $()$.

All other relations and functions have as purpose to pass tuples from one transaction to another in a schedule and to enforce that certain tuples do not collide, which is useful for the (if)-part of the proof.

Relation $\textsf{Boolean}^{\db}$ contains two tuples, which we interpret as Boolean values $0$ and $1$. Function $\ufunc{is-non-empty}:\textsf{String}\to\textsf{Boolean}$ and $\ufunc{is-error}:\textsf{String}\to\textsf{Boolean}$ are interpreted as follows:

\begin{align*}
\ufunc{is-non-empty}^{\db}(s) &= \left\{
\begin{array}{ll}
1 & \text{if }s \ne \langle \rangle, \\
0 & \text{otherwise},
\end{array}\right.\text{, and} \\
\ufunc{is-error}^{\db}(s) &= \left\{
\begin{array}{ll}
1 & \text{if } s = \langle \text{error}\rangle, \\
0 & \text{otherwise},
\end{array}\right.\text{, and}.
\end{align*}

Finally, relation $\textsf{InitialConflict}^{\db}$ contains a single tuple, which we refer to by $\langle \text{init} \rangle$. The interpretation of $\ufunc{defines}:\textsf{Boolean}\to\textsf{InitialConflict}$ maps $1$ and $0$ onto
$\langle \text{init} \rangle$. Function $\ufunc{error-string}:\textsf{InitialConflict}\to\textsf{String}$ maps $\langle \text{init} \rangle$ onto $\langle\text{error}\rangle$. Functions $\ufunc{final-domino-string}:\textsf{InitialConflict}\to\textsf{DominoSequence}$ and $\ufunc{final-domino-sequence}:\textsf{InitialConflict}\to\textsf{PCPSolution}$ map $\langle \text{init} \rangle$ onto the solution domino sequence $\vec{d}$, respectively on the final read $\vec{\charc}$ of $\vec{d}$.

Now the schedule $\prefix{\trans[1]}{b_1}\cdot \trans[2]\cdot \ldots \cdot \trans[m] \cdot \postfix{\trans[1]}{b_1}$, taking $\trans[1] = \ttinit(\langle \text{init} \rangle)$, $\trans[2] = \ttinitb(\langle \text{init} \rangle)$, for $i: 1 \le i \le r$, transaction $\trans[i+2] =  \ttdomino{i}(( d_1, \ldots, d_i))$, $\trans[m] = \ttclose(( d_1, \ldots, d_r))$ and $b_1 = \langle \text{init} \rangle$ has the conditions of Definition <ref>. Indeed, it is based on sequence of conflict quadruples $(T_1,
\R[1]{\langle\text{init}\rangle}, \W[2]{\langle \text{init}\rangle}, T_2),\allowbreak (T_2, \W[2]{()}, \W[3]{()}, T_3),\allowbreak (T_3, \W[3]{(d_1)},\allowbreak \W[4]{(d_2)}, T_4),\allowbreak \ldots, (T_{r+2}, \W[r+2]{(d_1,\ldots,d_r)},\allowbreak \W[r+3]{(d_1,\ldots,d_r)}, T_{r+3}),\allowbreak (T_{r+3}, \W[r+3]{\vec{d}}, \W[1]{\vec{d}}, T_1)$.

Condition (<ref>) is true because there is no ww-conflict between a write operation in $\prefix{\trans[1]}{b_1}$ and a write operation in any of the transactions $T_2, \ldots, T_m$, since the first write operation, respectively second write operation, in $\ttinit(\langle \text{init} \rangle)$ has a type that only occurs before the conflict with $\ttinitb(\langle \text{init} \rangle)$,
and is the conflict with $\ttclose((d_1, \ldots, d_r))$, respectively. Furthermore (<ref>) is true because $b_1 <_{\trans[1]} a_1$ and Condition (<ref>) is true because $b_{1}$ and $a_{2}$ are rw-conflicting.

§.§ Helpful lemma
Before proving the opposite direction of Theorem <ref>, we first establish the following Lemma.

If a set $\workload$ of  is not robust against then there is a multiversion split schedule
$\prefix{\trans[1]}{b_1}\cdot \trans[2]\cdot \ldots \cdot \trans[m] \cdot \postfix{\trans[1]}{b_1}$ for a set $\transset = \{\trans[1], \ldots, \trans[m]\}$ of transactions consistent with $\workload$ in which an operation from a transaction $T_j$ depends on an operation from transaction $T_i$ only if $j=i+1$ or $i=m$ and $j=1$.

If $\workload$ is not robust against , then there is a database $\db$ and a
multiversion split schedule $\schedule = \prefix{\trans[1]}{b_1}\cdot \trans[2]\cdot \ldots \cdot \trans[m] \cdot \postfix{\trans[1]}{b_1}\cdot \trans[m+1] \cdot \ldots \cdot \trans[n]$
based on a sequence of conflict quadruples $C$
for a set of transactions $\transset$ that is consistent with $\workload$ and $\db$ having the properties of Definition <ref>.

We can assume that $n=m$. Otherwise removing the transactions $T_{m+1}, \ldots, T_{n}$ from $\transset$, $\schedule$, and $C$. We can also assume that $\schedule$ is read-last-committed. Otherwise, choosing an appropriate version order $\ll_\schedule$ and version function $v_\schedule$.

Now suppose that there is a transaction $T_j$ with an operation $a'_j$ that depends on an operation $b'_i$ from transaction $T_i$ and with $j \ne i + 1$ or $i=m$ and $j\ne 1$. Clearly, by definition of dependency and the structure of a multiversion split schedule, $i < j$ or $j=1$.

We proceed the proof by a construction showing that, then, there is an alternative schedule $\schedule'$ that is also a multiversion split schedule, but for a strict subset of transactions in $\transset$ (thus also still consistent with $\workload$ and $\db$). The result of the lemma then follows from the observation that repeated application of this construction must lead to a schedule with the properties of the lemma, without existence of such a dependency.

For the construction, we proceed by case distinction.

If $i\ne 1$ and $j\ne 1$, we construct a schedule $\schedule'$ from $\schedule$ by removing all operations from transactions $\trans[h]$ with $i<h<j$. Notice that we remove at least one transaction, since $i < i+1 < j$. We can derive a sequence of conflict quadruples $C'$ from $C$ by removing all occurrences of these transactions $\trans[h]$ and adding the conflict quadruple $(\trans[i], b'_i, a'_j, \trans[j])$ instead.
By construction, $\schedule'$ is a multiversion split schedule based on $C'$ over a set of transactions consistent with $\workload$ and $\db$. It remains to show that the newly constructed schedule $\schedule'$ has the properties of Definition <ref>. The latter is straightforward since $C$ and $C'$ agree on their first and last quadruple, due to assumption $i\ne 1$ and $j\ne 1$.

If $i = 1$, it follows that $i<j$ and thus $j\ne 1$. Then, we
construct a schedule $\schedule'$ from $\schedule$ by removing all operations from transactions $\trans[h]$ with $i<h<j$ and updating the prefix and postfix of $\trans[1]$, now based on $b'_i$.
Notice that we again remove at least one transaction, since $i < i+1 < j$ and that
we can derive a sequence of conflict quadruples $C'$ from $C$ in the same way as before, by removing all occurrences of these transactions $\trans[h]$ and adding the conflict quadruple $(\trans[i], b'_i, a'_j, \trans[j])$ instead. By construction, $\schedule'$ is a multiversion split schedule based on $C'$ over a set of transactions consistent with $\workload$ and $\db$. It remains to show that the newly constructed schedule $\schedule'$ has the properties of Definition <ref>.

First, we observe that $b'_1$ and $a'_j$ are rw-conflicting, which immediately implies that Condition (3) is true for $\schedule'$. The argument is by exclusion. Indeed, if $b'_1$ and $a'_j$ would be ww-conflicting, then $b'_1 \ll_\schedule a'_j$ implying $b'_1 <_\schedule a_j'$ (due to the assumed read-last committed) and thus $b'_1 \le_\schedule b_1$, which is not allowed by condition (1) on $\schedule$. It follows from a similar argument that $b'_1$ and $a'_j$ are not wr-conflicting: both $b'_1 = v_\schedule(a'_j)$ and $b'_1 \ll_\schedule v_\schedule(a'_j)$ imply $b'_1 <_\schedule C_1 <_\schedule a'_j$, which contradicts with $C_1$ being the last operation in $\schedule$.

Since $b'_1$ is rw-conflicting with $a'_j$, we have $v_\schedule(b'_1) \ll_\schedule a_j'$, implying $b'_1 <_\schedule a_j'$ (due to read-last-committed and the structure of a multiversion split schedule),
thus $b'_1 \le_\schedule b_1$. Therefore, Condition (1) again transfers from $\schedule$ to $\schedule'$. For similar reasons Condition (2) applies on $\schedule'$: If $b_1 <_{\trans[1]} a_1$ then $b'_1 \le_{\trans[1]}b_1<_{\trans[1]} a_1$.

Otherwise, if $j=1$, it follows that $1 < i$. Then, we
construct a schedule $\schedule'$ from $\schedule$ by removing all operations from transactions $\trans[h]$ with $i<h$.
Notice that we remove at least one transaction, since $i < m$. We can derive a  $C'$ from $C$ by removing all occurrences of these transactions $\trans[h]$ and adding the  $(\trans[i], b'_i, a'_j, \trans[j])$ instead.

In this schedule $\schedule'$, Condition (1) and (3) transfer from $\schedule$ by its construction. To see that Condition (2) is true on $\schedule'$, simply notice that if $b_i'$ and $a_1'$ are ww or wr-conflicting, then either $b_i' \ll_\schedule a_j'$ or $b_i' = v_\schedule(a_j')$ or $b_i' \ll_\schedule v_\schedule(a_j')$, which all imply $b_i <_\schedule C_i <_\schedule a_1'$ and thus that $b_1 <_\schedule a_1'$, implying $b_1 <_{\schedule'} a_1'$.

§.§ If direction

It remains to argue that the if direction of Theorem <ref> is indeed correct.

Next, we show that, if there exists a multiversion split schedule for the set of  in Figure <ref> for some set $\dominoset$ of dominoes, then this schedule is always a schedule-encoding of a sequence of dominoes in $\dominoset$.

Let $\dominoset$ be a set of dominoes. If there is a multiversion split schedule $\schedule$ for a set of transactions consistent with the  in Figure <ref> for $\dominoset$ and some database $\db$, then this schedule $\schedule$ is a schedule-encoding of some sequence $\vec{d}$ of dominoes in $\dominoset$.

For the proof, let $\db$ be a database and $\schedule = \prefix{\trans[1]}{b_1}\cdot \trans[2]\cdot \ldots \cdot \trans[m] \cdot \postfix{\trans[1]}{b_1}$ a multiversion split schedule for a set of transactions $\transset$ consistent with $\workload$ and $\db$, with the conditions of Lemma <ref> and based on some sequence of conflict quadruples $C = (\trans[1],b_1,a_2,\trans[2]), (\trans[2],b_2,a_3,\trans[3]) \ldots, (\trans[m],b_m, a_1,\trans[1])$.
We show through a sequence of properties (Lemmas <ref>, <ref>, <ref>, and <ref>), that $\schedule$ is a schedule-encoding of a sequence $\vec{d}$ of dominoes in $\dominoset$.

As a first property (Lemma <ref>), we observe that  in $\workload$ heavily constrain the possible variable instantiations. For   $\ttinit$, for example, a variable mapping depends entirely on the choice of the value for variable $\vi$. Since Lemma <ref> forbids the presence of duplicate transactions in $\transset$, two transactions $T_i$ and $T_j$ (with $i\ne j$) based on  $\ttinit$ cannot agree on their choice for variable $\vi$ in $\schedule$. By applying this argument to other , we obtain the following corollary of Lemma <ref>.
Here, for each transaction $\trans[i]$ in $\schedule$, we write $\tau_i$ to denote the  in $\workload$ that it is based on, and by $\mu_i$ the associated variable mapping for $\tau_i$, with $\mu_i(\tau_i) = \trans[i]$.

for two transactions $T_i$ and $T_j$ in $\schedule$, with $i\ne j$:

* if $T_i$ and $T_j$ are based on $\ttinit$, then $\mu_i(\vi) \ne \mu_j(\vi)$;

* if $T_i$ and $T_j$ are based on $\ttinitb$ then $\mu_i(\vs_1) \ne \mu_j(\vs_1)$;

* if $T_i$ and $T_j$ are based on $\ttclose$ then $\mu_i(\vb) \ne \mu_j(\vb)$ and $\mu_i(\vc) \ne \mu_j(\vc)$;

* if $T_i$ and $T_j$ are based on domino  then $\mu_i(\vb) \ne \mu_j(\vb)$ and $\mu_i(\vb_{\text{next}}) \ne \mu_j(\vb_\text{next})$.

We conclude the proof of Proposition <ref> with the necessary arguments (Lemmas <ref>, <ref>, <ref> and <ref>) that $\schedule$ is indeed a schedule-encoding for some sequence of dominoes.

Transaction $T_1$ is based on $\ttinit$,  $T_2$ is based on $\ttinitb$, and $\mu_1(\vi) = \mu_2(\vi)$, $\mu_1(\vx_1) \ne \mu_2(\vx_2)$, and $\mu_1(\vs_1) = \mu_2(\vs_1) \ne \mu_2(\vs_0)$.

Since $b_{1}$ and $a_{2}$ are rw-conflicting (cf, Definition <ref>), and there are no updates in the considered , operation $b_1$ must be a read. Since  is the only type allowing for conflicts involving a read, it is immediate that $T_1$ must be based on $\ttinit$ and $T_2$ based on $\ttinitb$, with $\mu_1(\vi) = \mu_2(\vi)$.  From this equality and function $\ufunc{final-dominoes-string}$ it follows that $\mu_1(\vs_1) =  \mu_2(\vs_1)$.

From Definition <ref>, particularly that there is no ww-conflict between a write operation in $\prefix{\trans[1]}{b_1}$ and a write operation in any of the transactions $T_2, \ldots, T_m$, it follows that $\mu_1(\vx_1) \ne \mu_2(\vx_2)$.
Finally, function $\ufunc{is-non-empty}$, which maps $\vs_1$ onto $\vx_1$ in  $\ttinit$ and $\vs_0$ onto $\vx_2$ in  $\ttinitb$, implies $\mu_1(\vs_1) \ne \mu_2(\vs_0)$.

There is a transaction $T_3$ in $\schedule$ and it is based on a domino , with $\mu_3(\vs_1) = \mu_2(\vs_1)$.

First, suppose towards a contradiction that $m=2$. We already know from Lemma <ref> that
$\mu_1(\vi) = \mu_2(\vi)$ and $\mu_1(\vx_1) \ne \mu_2(\vx_2)$, thus $a_1 = b_1 = \R[]{\mu_1(\vi)}$ and $b_2 = a_2 = \W[]{\mu_2(\vi)}$, indicating $b_1 \rightarrow_s a_2$, particularly, $v_\schedule(b_1) \ll_s a_2$, thus implying that $a_1$ cannot depend on $b_2$, which is the desired contradiction.

The remainder of the proof is by exclusion. Transaction $T_3$ is not based on  $\ttinitb$, because all possible conflicts between $T_2$ and an instantiation of  $\ttinitb$ (implying either $\mu_2(\vx_2) = \mu_3(\vx_2)$,  $\mu_2(\vb) =  \mu_3(\vb)$, or $\mu_2(\vi) =  \mu_3(\vi)$) would imply the equality $\mu_2(\vs_1) = \mu_3(\vs_1)$ (through functional constraints $\vi = \ufunc{defines}(\vx_2)$, $\vs_1 = \ufunc{future-solution-string}(\vb)$, and $\vs_1 = \ufunc{final-dominoes-string}(\vi)$), which is forbidden by Lemma <ref>.
The argument that transaction $T_3$ cannot based on  $\ttinit$ is similar: every possible conflict between $T_2$ and an instantiation of $\ttinit$ implies $\mu_1(\vi) = \mu_2(\vi) = \mu_3(\vi)$ either directly (taking $\mu_2(\vi_2) = \mu_3(\vi_1)$ as conflict) or, when taking
$\mu_2(\vx_2) = \mu_3(\vx_1)$ as conflict, through constraints $\vi = \ufunc{defines}(\vx_1)$ and $\vi = \ufunc{defines}(\vx_2)$ in $\trans[2]$ and $\trans[3]$, respectively. Either way, $\mu_1(\vi) = \mu_3(\vi)$ is forbidden by Lemma <ref>.
Finally, to see that $\trans[3]$ is not based on  $\ttclose$, we observe that a conflict between $\trans[2]$ and an instantiation of  $\ttclose$ must be ww-conflicting involving variables $\vb$, thus with $\mu_2(\vb) = \mu_3(\vb)$.
Then, $\mu_2(\vs_0) = \mu_3(\vs_t)$, due to functional constraint $\vs_0 = \ufunc{top-string}(\vb)$ in $\trans[2]$ and $\vs_t = \ufunc{top-string}(\vb)$ in $\trans[3]$, and $\mu_2(\vs_1) = \mu_3(\vs_1)$, due to functional constraint $\vs_1 = \ufunc{future-solution-string}(\vb)$ in $\trans[2]$ and $\trans[3]$.
However, we also have $\mu_3(\vs_1) = \mu_3(\vs_t)$, due to constraints $\vs_1 = \ufunc{solution-string}(\vb)$ and $\vs_t=\ufunc{solution-string}(\vb)$, thus implying $\mu_2(\vs_0) = \mu_3(\vs_t) = \mu_3(\vs_1) = \mu_2(\vs_1)$, which contradicts with earlier proven Lemma <ref>.
We conclude that $T_3$ is indeed based on a domino .
Therefore, the conflict quadruple $(T_2, b_2, a_3, T_3)$ must admit ww-conflicting operations over variable $\vb$ in $\trans[2]$ and either variable $\vb$ or $\vb_{next}$ in $\trans[3]$. We notice that $\mu_2(\vs_1) = \ufunc{future-solution-string}(\mu_2(\vb))$, $\mu_3(\vs_1) = \ufunc{future-solution-string}(\mu_3(\vb))$, and $\mu_3(\vs_1) = \ufunc{future-solution-string}(\mu_3(\vb_{next}))$, thus independent of the variable $\vb_{next}$ or $\vb$ in $\trans[3]$, we have $\mu_2(\vs_1) = \mu_3(\vs_1)$.

For a transaction $T_i$, with $i\ge 4$, for which all $T_j$'s, with $j \in \{3,\ldots,i-1\}$, are based on domino , transaction $T_i$ is based on a domino  or on  $\ttclose$. Furthermore $\mu_2(\vs_1) = \mu_i(\vs_1)$.

Since domino  do not mention variables of type  and write only to variables of type , it remains to show that $\trans[i+1]$ is not based on  $\ttinitb$.

For this,  observe that $\mu_2(\vs_1) = \mu_{i-1}(\vs_1)$. Indeed, every conflict quadruple $(T_i, b_i, a_{i+1},\allowbreak T_{i+1})$, with $i \in \{3,\ldots, i-1\}$, admits ww-conflicting operations with variables of type . No matter if the conflict is via a variable $\vb$ or $\vb_{next}$, the constraints $\vs_1 = \ufunc{future-solution-string}(\vb)$ and $\vs_1 = \ufunc{future-solution-string}(\vb_{next})$ ensure $\mu_2(\vs_1) = \mu_{i-1}(\vs_1)$.

Now, assume towards a contradiction that $\trans[i+1]$ is based on $\ttinitb$, thus admitting a conflict quadruple $(T_{i}, b_i, a_{i+1}, T_{i+1})$ in $C$.
Then either $b_i=\mu_i(\vb)$ and $a_{i+1} = \mu_{i+1}(\vb)$ or $b_i=\mu_i(\vb_\text{next})$ and $a_{i+1} = \mu_{i+1}(\vb)$. Both of these equalities imply $\mu_i(\vs_1) = \mu_{i+1}(\vs_1)$ due to constraints
$\vs_1 = \ufunc{future-solution-string}(\vb)$ and $\vs_1 = \ufunc{future-solution-string}(\vb_{next})$, thus implying $\mu_i(\vs_1) = \mu_2(\vs_1)$, this contradict with Lemma <ref>. We conclude that $\trans[i]$ is indeed based on a domino  or on  $\ttclose$. That $\mu_{i-1}(\vs_1) = \mu_i(\vs_1)$ follows again from the constraints using function $\ufunc{future-solution-string}$.

If $T_i$ is based on  $\ttclose$, then $i=m$.

Let $T_j$ be the transaction following $T_i$. We already know about $T_j$ that either $j=1$ or must be a transaction that is different to all foregoing transactions  $T_1, \ldots, T_i$ (due to Lemma <ref>).

We first show, by exclusion, that transaction $T_j$ is based on $\ttinit$: Transaction $T_{j}$ cannot be based on $\ttclose$, as then either $\mu_i(\vb) = \mu_{j}(\vb)$ or $\mu_i(\vc) = \mu_{j}(\vc)$, which directly contradicts Lemma <ref>.
Similarly, transaction $T_{j}$ cannot be based on $\ttinitb$,  as then $\mu_i(\vb) = \mu_{j}(\vb)$ implying $\mu_2(\vs_1) = \mu_i(\vs_1) = \mu_{j}(\vs_1)$, due to the constraints involving function $\ufunc{future-solution-string}$.
Finally, transaction $T_{j}$ cannot be based on a domino , because then $\mu_{j}(\vb_\text{next}) = \mu_{i}(\vb) = \mu_{j}(\vb)$
or $\mu_{i-1}(\vb_\text{next}) = \mu_{i}(\vb) = \mu_{j}(\vb_\text{next})$, thus with $T_{i}$ and $T_{j}$ contradicting Lemma <ref>. We can thus indeed conclude that transaction $T_j$ is based on $\ttinit$.

To see that $j=1$, recall that $\mu_1(\vs_1) = \mu_{i-1}(\vs_1)$ and the only possible conflict between $T_i$ and $T_j$ implies $\mu_i(\vc) = \mu_{j}(\vc)$.
From the latter we obtain  $\mu_{i-1}(\vs_1) = \mu_{i}(\vs_1)$, due to $\mu_{i-1}(\vb_\text{next}) = \mu_{i}(\vb)$ and function $\ufunc{future-solution-string}$.
From this it follows that $\mu_1(\vi) = \mu_j(\vi)$ through $\vi = (\ufunc{defines} \circ \ufunc{is-non-empty})(\vs_1)$ in  $\ttinit$. That $j=1$ then follows from Lemma <ref>.

Finally, we show that if there is a multiversion split schedule with the properties of Lemma <ref> that is a schedule-encoding for a sequence of dominoes $\vec{d}$, then this sequence $\vec{d}$ is also a solution to the respective PCP problem. The next Proposition thus finalizes the proof for the if-direction of Theorem <ref>.

Let $\dominoset$ be a set of dominoes. Let $\schedule$ be a multiversion split schedule with the properties of Lemma <ref> that is consistent with the  in Figure <ref> for $\dominoset$ and with some database $\db$. If $\schedule$ is a schedule-encoding of a sequence $\vec{d}$ of dominoes in $\dominoset$, then $\vec{d}$ is a solution for the PCP problem on input $\dominoset$.

Let $a_1a_2\ldots a_h$ and $b_1b_2\ldots b_k$ be the two strings (with $a_i, b_i \in \Sigma$) obtained by reading from left to right, symbol by symbol, the values on the top, respectively, the bottom of dominoes $d_1, \ldots, d_r$. Let us say that $a_1a_2\ldots a_h = \vec{a_1}\vec{a_2}\ldots\vec{a_r}$ and $b_1b_2\ldots b_k = \vec{b_1}\vec{b_2}\ldots\vec{b_r}$. Notice that $h$ and $k$ are not necessarily equal to $r$ as the top and bottom value of an individual domino can be of different length.

For convenience of notation, we introduce for every $i \in \{0, \ldots, h\}$ and $j \in \{1, \ldots, k\}$ the following notation:

\begin{align*}
\alpha_i \mydef & (\ufunc{append-$a_i$}\circ  \ufunc{append-$a_{i-1}$} \circ \cdots \circ \ufunc{append-$a_1$})(\mu_2(\vs_0)). \\
\beta_j \mydef & (\ufunc{append-$b_j$}\circ  \ufunc{append-$b_{j-1}$} \circ \cdots \circ \ufunc{append-$b_1$})(\mu_2(\vs_0)).
\end{align*}

First, we show that

\begin{align}
\alpha_h = \mu_2(\vs_1) = \beta_k.\label{align:a}
\end{align}

This result follows from the assumed structure of schedule $\schedule$. More precisely, since an instantiation of $\ttinitb$ with an instantiation of $\ttdomino{d_1}$ can only have conflicts on instantiations of $\W[]{\vb:DominoSequence}$, we have $\mu_2(\vb) = \mu_3(\vb)$, from which it follows that $\mu_2(\vs_1) = \mu_3(\vs_1)$.

For every individual instantiation of $\ttdomino{d_i}$ in $\schedule$, we have that $\ufunc{append-$a_i^{\ell_a}$}\circ\cdots \circ \ufunc{append-$a_i^1$}(\mu_i(\vs_t)) = \mu_i(\vs_{t\vec{a_i}})$ and $\ufunc{append-$b_i^{\ell_b}$}\circ\cdots \circ \ufunc{append-$b_i^1$}(\mu_i(\vs_b)) = \mu_i(\vs_{b\vec{b_i}})$, with $\vec{a_i} = a_1a_2\ldots a_{\ell_a}$ and $\vec{b_i} = b_1b_2\ldots b_{\ell_b}$.

For transactions $\trans[i]$, with $i \in \{3,\ldots,m+1\}$, (thus representing an instantiation of $\ttdomino{d_{i-2}}$ which is followed in $\schedule$ by an instantiation of $\ttdomino{d_{i-1}}$), the only possible conflict is between the instantiation of $\W[]{\vb_{next}:DominoSequence}$ ($\trans[i]$) and the instantiation of $\W[]{\vb:DominoSequence}$ in ($\trans[i+1]$) – notice that this is indeed the only option due to Lemma <ref> – thus with $\mu_i(\vb_{next}) = \mu_{i+1}(\vb)$, implying $\mu_i(\vs_{t\vec{a_i}}) = \mu_{i+1}(\vs_t)$, $\mu_i(\vs_{b\vec{b_i}}) = \mu_{i+1}(\vs_b)$, and $\mu_{i}(\vs_1) = \mu_{i+1}(\vs_1)$.

Finally, transaction $\trans[m-1]$ (an instantiation of $\ttdomino{d_m}$) can only conflict with transaction $\trans[m]$ (an instantiation of $\ttclose$) on instantiations of $\vb_{next}$ (in $\ttdomino{d_m}$, and $\vb$ (in $\ttclose$), thus with $\mu_{m-1}(\vb_{next}) = \mu_{m}(\vb)$, implying $\mu_{m-1}(\vs_{t\vec{a_r}}) = \mu_m(\vs_t) = \mu_{m}(\vs_b) = \mu_{m-1}(\vs_{b\vec{b_r}})$.

Combining the above equalities indeed proves Condition (<ref>).

From Condition (<ref>) we can now derive that,

\begin{align}
\alpha_i = \mu_2(\vs_1) = \beta_i, \text{ for every $i \in \{ 1,\ldots \min\{h,k\}\}$,}\label{align:b}
\end{align}

by following an analogous approach. Indeed, in every instantiation of $\ttdomino{i}$, there is a functional constraint for every application of the append function that requires its input to be the result of the detach function applied over its output, which indeed implies Condition (<ref>).

To see that $k=h$, we observe that $k \ne h$ implies an application of the detach function over the instantiation of $\vs_1$ (for which we already argued it has the same tuple assigned for every domino instantiation) for the shortest string, which contradicts with Condition (<ref>) because such an application results in the same instantiation as $\vs_e$,  which can never equal the instantiation for $\vs_1$.

The desired result that the individual symbols in the top and bottom reads of dominoes in sequence $\vec{d}$ are the same now follows from the functional constraint that every interpretation of a string sequence mapped via function $\ufunc{top}$ onto either the interpretation for $\vs_1$ (representing symbol $1 \in \Sigma$) or $\vs_0$ (representing symbol $0 \in \Sigma$).

§ ROBUSTNESS FOR  ADMITTING MULTI-TREE BIJECTIVITY

[draw, rounded rectangle,align=center] (A) at (0,0) ;
[draw, rounded rectangle,align=center] (S) at (-2.5,0) ;
[draw, rounded rectangle,align=center] (C) at (2.5,0) ;
[->,dashed] (A) to [bend right] node[midway,above=-.2em] $\fas$ (S) ;
[->] (S) to [bend right] node[midway,below=-.2em] $\fsa$ (A) ;
[->,dashed] (A) to [bend left] node[midway,above=-.2em] $\fac$ (C) ;
[->] (C) to [bend left] node[midway,below=-.2em] $\fca$ (A) ;

Schema graph for the SmallBank benchmark. The dashed edges correspond to the multi-tree schema graph for the schema restricted to $\fas$ and $\fac$.

We say that a set of  $\workload$ over a schema $(\schRel, \schFunc)$ admits multi-tree bijectivity if a disjoint partitioning of $\schFunc$ in pairs $(f_1, g_1),(f_2, g_2), \ldots, (f_n, g_n)$ exists such that $\domf(f_i) = \rangef(g_i)$ and $\domf(g_i) = \rangef(f_i)$ for every pair of function names $(f_i, g_i)$;
every schema graph $\sg{\schRel, \{h_1, h_2, \ldots, h_n\}}$ over the schema restricted to function names $\{h_1, h_2, \ldots, h_n\}$ (with $h_i = f_i$ or $h_i= g_i$) is a multi-tree; and,
for every pair of function names $(f_i, g_i)$ and for every pair of variables $\vx, \vy$ occurring in a  $\tau_j \in \workload$, we have $f_i(\vx) = \vy \in \Cset_j$ iff $g_i(\vy) = \vx \in \Cset_j$.
Intuitively, we can think of $f_i$ as a bijective function, with $g_i$ its inverse. We denote the class of all sets of  admitting multi-tree bijectivity by $\mtbtemplates$. The SmallBank benchmark given in Figure <ref> is in $\mtbtemplates$, witnessed by the partitioning $\{(\fac, \fca), (\fas, \fsa)\}$. For example, the schema graph restricted to $\fac$ and $\fas$ is a tree and therefore also a , as illustrated in Figure <ref>.

The next theorem allows disequalities whereas Theorem <ref> does not require them.

is decidable in .

The approach followed in the proof of Theorem <ref> is to repeatedly pick a transaction template while maintaining an overall consistent variable mapping in search for a counterexample multiversion split schedule
that by Theorem <ref> suffices to show that robustness does not hold.
The main challenge is to show that a variable mapping consistent with all functional constraints can be maintained in logarithmic space and that all requirements for a multiversion split schedule can be verified in .

Central to our approach is a generalization of conflicting operations.
Let $\workload$ be a set of .
$\tau_i$ and $\tau_j$ in $\workload$, we say that an operation $o_i \in \tau_i$ is potentially conflicting with an operation $o_j \in \tau_j$ if $o_i$ and $o_j$ are operations over a variable of the same type, and at least one of the following holds:

* $\WriteSet{o_i}\cap \WriteSet{o_j}\neq \emptyset$ (potentially ww-conflicting);

* $\WriteSet{o_i}\cap \ReadSet{o_j}\neq \emptyset$ (potentially wr-conflicting); or

* $\ReadSet{o_i}\cap \WriteSet{o_j}\neq \emptyset$ (potentially rw-conflicting).

Intuitively, potentially conflicting operations lead to conflicting operations when the variables of these operations are mapped to the same tuple by a variable assignment. In analogy to  over a set of transactions as in Definition <ref>, we consider  $(\tau_i, o_i, p_j,  \tau_j)$ over
$\workload$ with $\tau_i, \tau_j \in \workload$, and $o_i \in \tau_i$ an operation that is potentially conflicting with an operation $p_j \in \tau_j$.
For a  $D = (\tau_1, o_1, \allowbreak p_2,\allowbreak \tau_2), \ldots, (\tau_m, o_m, p_1, \tau_1)$ over
$\workload$, we write $\transcopies{D}$ to denote the set $\{\tau_1,\ldots,\tau_m\}$ of  mentioned in $D$. For ease of exposition, we assume a variable renaming such that any pair of templates in $\transcopies{D}$ uses a disjoint set of variables.[To be formally correct, the latter would require to add every such variable-renamed template to $\workload$ creating a larger set $\workload'$. This does not influence the complexity of Theorem <ref> as $\transcopies{D}$ nor $\workload'$ are used in the algorithm. Their only purpose is to reason about properties of $\bar \mu$.]
The sequence $D$
induces a  $C = (\trans[1], b_1, a_2, \trans[2]),\allowbreak \ldots,\allowbreak (\trans[m], b_m, a_1, \trans[1])$
by applying a variable assignment $\mu_i$ to each $\tau_i$ in $\transcopies{D}$.
We call such a set of variable assignments simply a variable mapping for $D$, denoted $\barmu$, and write $\barmu(D) = C$. For a variable $\vx$ occurring in a  $\tau_i$, we write $\barmu(\vx)$ as a shorthand notation for $\mu_i(\vx)$, with $\mu_i$ the variable assignment over $\tau_i$ in $\barmu$. This is well-defined as all templates in $\transcopies{D}$ are variable-disjoint.
Furthermore, $\barmu(\myvar{o_i}) = \barmu(\myvar{p_j})$ for each  $(\tau_i, o_i, p_j, \tau_j)$ in $D$
as otherwise the induced quadruple $(\trans[i], b_i, a_j, \trans[j])$ is not a valid  in $C$.
We say that a variable mapping $\barmu$ is admissible for a database $\db$ if every variable assignment $\mu_i$ in $\barmu$ is admissible for $\db$.

A basic insight is that if there is a multiversion split schedule $\schedule$ for some $C$ over a set of transactions $\transset$ consistent with $\workload$ and a database $\db$,
then there is a  $D$ such that $\barmu(D) = C$ for some $\barmu$. We will verify the existence of such a $C$,
satisfying the properties of Definition <ref>,
by nondeterministically constructing $D$ on-the-fly together with a mapping $\bar\mu$. We show in Lemma <ref> that when $\workload\in \mtbtemplates$,
$\bar \mu$ is a collection of disjoint type mappings  (that map variables of the same type to the same tuple) such that variables that are “connected” in $D$ (in a way that we will make precise next) are mapped using the same type mapping. Lemma <ref> then shows that already a constant number of those type mappings suffice.

We introduce the necessary notions to capture when two variables are connected in $D$. We can think of equality constraints $\vy = f(\vx)$ in a template $\tau$ as constraints on the possible variable assignments $\mu$ for $\tau$ when a database $\db$ is given. Indeed, if we fix $\mu(\vx)$ to a tuple in $\db$, then $\mu(\vy) = f^\db(\mu(\vx))$ is immediately implied.
These constraints can cause a chain reaction of implications. If for example $\vz = g(\vy)$ is a constraint in $\tau$ as well, then $\mu(\vx)$ immediately implies $\mu(\vz) = g^\db(f^\db(\mu(\vx)))$. We formalize this notion of implication next. We use sequences of function names
$F = f_1\cdots f_n$,
denoting the empty sequence as $\epsilon$ and the concatenation of two sequences $F$ and $G$ by $F \cdot G$.
For two variables $\vx, \vy$ occurring in a  $\tau$ and a (possibly empty) sequence of function names $F$, we say that $\vx$ implies $\vy$ by $F$ in $\tau$, denoted $\vx \varimplies{F}{\tau} \vy$, if $\vx = \vy$ and $F = \epsilon$ or if
there is a variable $\vz$ such that $\vy = f(\vz)$ is a constraint in $\tau$, $\vx \varimplies{F'}{\tau} \vz$ and $F = F' \cdot f$.
We next extend the notions of implication
to sequences of .
Let $D = (\tau_1, o_1, \allowbreak p_2,\allowbreak \tau_2), \ldots, (\tau_m, o_m, p_1, \tau_1)$ be a ,
and let $\vx$ and $\vy$ be two variables occurring in  $\tau_i$ and $\tau_j$ in $\transcopies{D}$, respectively.
Then $\vx$ implies $\vy$ by a sequence of function names $F$ in $D$, denoted $\vx \varimplies{F}{D} \vy$ if

* $i=j$
and $\vx \varimplies{F}{\tau_i} \vy$ (implication within the same template);

* $F = \epsilon$ and $(\tau_i, o_i, p_j, \tau_j)$ or $(\tau_j, o_j, p_i, \tau_i)$ is a  in $D$ with $o_i$ (respectively $p_i$) an operation over $\vx$ and $p_j$ (respectively $o_j$) an operation over $\vy$ (implication between templates, notice that $\vx \varimplies{\epsilon}{D} \vy$ iff $\vy \varimplies{\epsilon}{D} \vx$); or

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

Two variables $\vx$ and $\vy$ occurring in $\transcopies{D}$ are connected in $D$, denoted D, if $\vx \varimplies{F}{D} \vy$ or $\vy \varimplies{F}{D} \vx$,
or if there is a variable $\vz$ with $\conn{\vx}{\vz}{D}$
and either $\vz \varimplies{F}{D} \vy$ or $\vy \varimplies{F}{D} \vz$ for some sequence
$F$. Furthermore, two variables $\vx$ and $\vy$ occurring in a   $\tau$ are connected in $\tau$, denoted
τ, if $\vx \varimplies{F}{\tau} \vy$ or $\vy \varimplies{F}{\tau} \vx$,
or if there is a variable $\vz$ with $\conn{\vx}{\vz}{\tau}$
and either $\vz \varimplies{F}{\tau} \vy$ or $\vy \varimplies{F}{\tau} \vz$ for some sequence
$F$. These definitions of connectedness can be trivially extended to operations over variables: two operations in $D$ (respectively $\tau$) are connected in $D$ (respectively $\tau$) if they are over variables that are connected in $D$ (respectively $\tau$). When $F$ is not important we drop it from the notation. For instance, we denote by
$\vx \varimplies{}{D} \vy$ that there is an $F$ with $\vx \varimplies{F}{D} \vy$.

Let $D$ be a  over
$\workload\in \mtbtemplates$. Then D
implies $\vx \varimplies{}{D} \vy$ and $\vy \varimplies{}{D} \vx$.
Furthermore, if $\type{\vx} = \type{\vy}$
then $\barmu(\vx) = \barmu(\vy)$ for every variable mapping $\barmu$ for $D$ that is admissible for some database $\db$.

Before proving the correctness of Lemma <ref>, we first present two additional lemmas that will be used in the correctness proof.

Let $(\schRel, \schFunc)$ be a schema for which a disjoint partitioning of $\schFunc$ in pairs $P = (f_1, g_1),(f_2, g_2), \ldots, (f_n, g_n)$ exists such that $\domf(f_i) = \rangef(g_i)$ and $\domf(g_i) = \rangef(f_i)$ for every $(f_i, g_i) \in P$ and
every schema graph $\sg{\schRel, \{h_1, h_2, \ldots, h_n\}}$ over the schema restricted to function names $\{h_1, h_2, \ldots, h_n\}$ with $h_i \in (f_i, g_i)$ is a multi-tree. Then:

*  there is no function name $f \in \schFunc$ with $\domf(f) = \rangef(f)$; and

*  for every path in $\sg{\schRel, \schFunc}$, say visiting the nodes $R_1, R_2, \ldots, R_{m-1}, R_m$, if $R_1 = R_m$ and $R_1 \neq R_i$ for every $i \in [2, m-1]$,
then $R_2 = R_{m-1}$ and $(f,g)$ is a pair in $P$ with $f$ the edge from $R_1$ to $R_2$ and $g$ the edge from $R_{m-1}$ to $R_m$.

Towards a contradiction, assume (<ref>) does not hold. That is, there is a function name $f_i$ with $\domf(f_i) = \rangef(f_i) = R$ for some type $R$. Let $g_i$ be the function name such that $(f_i,g_i)$ is a pair in $P$. By definition, $\domf(g_i) = \rangef(g_i) = R$. But then we cannot pick a $h_i \in (f_i, g_i)$ such that the resulting schema graph is a multi-tree. Indeed, in both cases, there is a self-loop on $R$, leading to the desired contradiction.

For (<ref>), assume towards a contradiction that $R_2 \neq R_{m-1}$. Without loss of generality, we can assume that each node is visited only once in $R_2, \ldots, R_{m-1}$.
Otherwise, $R_2, \ldots, R_{m-1}$ contains a loop that can be removed from this sequence without altering $R_2$ and $R_{m-1}$.
Since $R_1, R_2, \ldots, R_{m-1}, R_m$ is a path in $\sg{\schRel, \schFunc}$, there is a sequence of function names $F = e_1 \cdots e_{m-1}$ such that each $e_i$ is an edge from $R_i$ to $R_{i+1}$ in $\sg{\schRel, \schFunc}$, implying $\domf(e_i) = R_i$ and $\rangef(e_i) = R_{i+1}$.
By assumption that each type $R_i$ occurs only once in $R_2, \ldots, R_{m-1}$ (notice that, for $i=1$, this follows from Condition (2) of the lemma) and type $R_1 = R_m$ does not appear in $R_2, \ldots, R_{m-1}$, there is no pair of function names $e_i$ and $e_j$ in $F$ with $i\ne j$, $\domf(e_i) = \rangef(e_j)$ and $\rangef(e_i) = \domf(e_j)$.
Therefore, at most one function name of each pair in $P$ appears in $F$.
But then we can choose $h_i = e_i$ for each such pair in $P$, with $e_i$ the function name appearing in $F$.
Since $F$ describes a cycle in $\sg{\schRel, \schFunc}$, the resulting schema graph restricted to these $h_i$ cannot be a multi-tree, as it contains a cycle.

It remains to argue that if $f$ is the edge from $R_1$ to $R_2$ and $g$ is the edge from $R_{m-1}$ to $R_m$ on this path, then $(f, g)$ is a pair in $P$.
To this end, note that $\domf(f) = \rangef(g)$ and $\rangef(f) = \domf(g)$, as $R_1 = R_m$ and $R_2 = R_{m-1}$.
If $(f, g)$ is not a pair in $P$, then there are two pairs $(f, f')$ and $(g, g')$ in $P$ with $\domf(f) = \domf(g') = \rangef(f') = \rangef(g) = R_1$ and $\rangef(f) = \rangef(g') = \domf(f') = \domf(g) = R_2$.
Then we can choose $f$ in $(f, f')$ and $g$ in $(g, g')$.
Since the resulting schema graph cannot be a multi-tree, as there is a cycle between $R_1$ and $R_2$, this choice leads to a contradiction.

Let $D$ be a  over $\workload\in \mtbtemplates$. Then

* $\vx \varimplies{}{\tau} \vy$ iff $\vy \varimplies{}{\tau} \vx$ for every pair of variables $\vx$ and $\vy$ occurring in a template $\tau$; and

* $\vx \varimplies{}{D} \vy$ iff $\vy \varimplies{}{D} \vx$ for every pair of variables $\vx$ and $\vy$ occurring in $D$.

(1) We argue by induction on the definition of $\vx \varimplies{}{\tau} \vy$ that $\vx \varimplies{}{\tau} \vy$ implies $\vy \varimplies{}{\tau} \vx$. The other direction is analogous. The base case is immediate, as $\vx = \vy$ implies $\vy \varimplies{}{\tau} \vx$ by definition. For the inductive case, assume a variable $\vz$ such that $\vy = f(\vz)$ is a constraint in $\tau$ and $\vx \varimplies{}{\tau} \vz$.
By the induction hypothesis, $\vz \varimplies{F}{\tau} \vx$ for some sequence of function names $F$. Since $\workload \in \mtbtemplates$, there is a constraint $\vz = f'(\vy)$ in $\tau$ as well. It follows that $\vy \varimplies{F'}{\tau} \vx$ with $F' = f' \cdot F$.

(2) We argue by induction on the definition of $\vx \varimplies{}{D} \vy$ that $\vx \varimplies{}{D} \vy$ implies $\vy \varimplies{}{D} \vx$. The other direction is again analogous. The first base case is now immediate, as we already argued that $\vx \varimplies{}{\tau} \vy$ implies $\vy \varimplies{}{\tau} \vx$.
For the second base case, assume $\vx \varimplies{\epsilon}{D} \vy$ and $(\tau_i, o_i, p_j, \tau_j)$ is a  in $D$ with $\myvar{o_i} = \vx$ and $\myvar{p_j} = \vy$ (the case for $(\tau_j, o_j, p_i, \tau_i)$ is analogous). $\vy \varimplies{\epsilon}{D} \vx$ then follows by definition.
For the inductive case, let $\vz$ be a variable such that $\vx \varimplies{F_1}{D} \vz$ and $\vz \varimplies{F_2}{D} \vy$. Then by induction hypothesis $\vz \varimplies{F_1'}{D} \vx$ and $\vy \varimplies{F_2'}{D} \vz$ for some sequence of function names $F_1'$ and $F_2'$.
By definition, $\vy \varimplies{F'}{D} \vx$ with $F' = F_2' \cdot F_1'$.

We are now ready to prove the correctness of Lemma <ref>.

Assuming $\conn{\vx}{\vy}{D}$, we first show by induction on the definition of connectedness that $\vx \varimplies{}{D} \vy$.
By Lemma <ref>, $\vy \varimplies{}{D} \vx$ then follows.
For the base case, both $\vx \varimplies{}{D} \vy$ and $\vy \varimplies{}{D} \vx$ imply $\vx \varimplies{}{D} \vy$, where the former is immediate and the latter is by Lemma <ref>.
For the inductive case, let $\vz$ be a variable with $\conn{\vx}{\vz}{D}$ and either $\vz \varimplies{}{D} \vy$ or $\vy \varimplies{}{D} \vz$. Again, $\vz \varimplies{F_2}{D} \vy$ for some sequence of function names $F_2$ is implied in both cases. By induction hypothesis, $\vx \varimplies{F_1}{D} \vz$ for some sequence of function names $F_1$.
As a result, $\vx \varimplies{F}{D} \vy$ with $F = F_1 \cdot F_2$.

Next, let $\vx$ and $\vy$ be two variables occurring in $\transcopies{D}$ with $\conn{\vx}{\vy}{D}$ and $\type{\vx} = \type{\vy}$ and let $\barmu$ be a variable mapping for $D$ that is admissible for a database $\db$. We prove that $\barmu(\vx) = \barmu(\vy)$.

We already argued that $\conn{\vx}{\vy}{D}$ implies $\vx \varimplies{}{D} \vy$.
By definition of $\vx \varimplies{}{D} \vy$, there is a sequence of variables $\vx_1, \vx_2\, \ldots, \vx_n$ with $\vx_1 = \vx$ and $\vx_n = \vy$ 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}$.

In the remainder of this proof, we show that for each pair of variables $\vx_i$ and $\vx_j$ in this sequence with $\type{\vx_i} = \type{\vx_j}$ that $\barmu(\vx_i) = \barmu(\vx_j)$. The desired $\barmu(\vx) = \barmu(\vy)$ then follows immediately as $\vx=\vx_1$ and $\vy=\vx_n$.
Note that it suffices to show this property only for pairs of variables $\vx_i$ and $\vx_j$ for which no variable $\vx_k$ exists with $i<k<j$ and $\type{\vx_i} = \type{\vx_j} = \type{\vx_k}$. Indeed, if such an $\vx_k$ exists, we can recursively argue that $\barmu(\vx_i) = \barmu(\vx_k)$ and $\barmu(\vx_k) = \barmu(\vx_j)$.
The argument is by induction on the number of variables between $\vx_i$ and $\vx_j$.

If $j = i+1$ (base case), then $(\ddagger)$ applies to $\vx_i$ and $\vx_j$.
Indeed, if $(\dagger)$ would apply instead, then there would be a function name $f$ with $\domf(f) = \type{\vx_i} = \type{\vx_j} = \rangef(f)$, contradicting Condition (<ref>) of Lemma <ref>.
By definition of $\barmu$, we have $\barmu(\vx_i) = \barmu(\vx_j)$.

Next, let $i+1 < j$ (inductive case), and assume that $\barmu(\vx_k) = \barmu(\vx_\ell)$ for all $\vx_k$ and $\vx_\ell$ with $i < k \leq \ell < j$ and $\type{\vx_k} = \type{\vx_\ell}$ (induction hypothesis).
From this sequence $\vx_i, \ldots \vx_j$, we derive a sequence of function names $F = f_1 \cdots f_{m-1}$, where each function name $f_i$ is based on an application of $(\dagger)$ on adjacent variables (notice that applications of $(\ddagger)$ do not result in a function name being added to $F$).
By assumption on the types of variables $\vx_k$ with $i < k < j$, we have in particular $\type{\vx_{i+1}} \neq \type{\vx_i}$ and $\type{\vx_{j-1}} \neq \type{\vx_j}$.
This implies that $(\dagger)$ is applicable for $\vx_{i}$ and $\vx_{i+1}$ (respectively $\vx_{j-1}$ and $\vx_{j}$).
Furthermore, $\vx_{i}$ and $\vx_{i+1}$ appear in the same , say $\tau_i$ (respectively $\tau_j$ for $\vx_{j-1}$ and $\vx_{j}$), and $\vx_{i+1} = f_1(\vx_i) \in \Cset(\tau_i)$ (respectively $\vx_{j} = f_{m-1}(\vx_{j-1}) \in \Cset(\tau_j)$).
By construction, $F$ then describes a path in $\sg{\schRel, \schFunc}$ visiting the nodes $R_1, R_2, \ldots, R_{m-1}, R_m$ with $\type{\vx_i} = R_1$, $\type{\vx_{i+1}} = R_2$, $\type{\vx_{j-1}} = R_{m-1}$ and $\type{\vx_{j}} = R_{m}$.
Since this path satisfies Condition <ref> in Lemma <ref>, it follows that $\type{\vx_{i+1}} = \type{\vx_{j-1}}$ and $(f_1, f_{m-1})$ is a pair in the pairwise partitioning of $\schFunc$ witnessing $\workload \in \mtbtemplates$.
By definition of $\mtbtemplates$, $\vx_{i+1} = f_1(\vx_i) \in \Cset(\tau_i)$ then implies $\vx_{i} = f_{m-1}(\vx_{i+1}) \in \Cset(\tau_i)$.
According to the induction hypothesis, $\barmu(\vx_{i+1}) = \barmu(\vx_{j-1})$. Since $\barmu$ is admissible for $\db$, we conclude that $\barmu(\vx_i) = f_{m-1}^\db(\barmu(\vx_{i+1})) = f_{m-1}^\db(\barmu(\vx_{j-1})) = \barmu(\vx_j)$.

It follows from Lemma <ref> that, if we group connected variables, then the same tuple is assigned to all variables of the same type in this group.
We encode this choice of tuples for variables through (total) functions $c:\schRel\to\objects$ that we call type mappings and which map a relation onto a particular tuple of that relation's type. For instance, in SmallBank, a type mapping $c$ is determined by an Account tuple $\mya$, a Savings tuple $\mys$, and a Checking tuple $\myc$.
The following Lemma makes explicit how $\bar\mu$ can be decomposed into type mappings such that connected variables use the same type mapping and disequalities enforce the use of different type mappings.
For a multiversion split schedule $\schedule$ based on a  $C$ over a set of transactions $\transset$ consistent with
a $\workload\in \mtbtemplates$ and a database $\db$, let $\barmu$ be the variable mapping for a  $D$ over $\workload$ with $\barmu(D) = C$.
Then, a set $\typemapset$ of type mappings over disjoint ranges and a function $\typemapfunc: \variables \to \typemapset$
exist with:

* $\barmu(\vx) = c(\type{\vx})$ for every variable $\vx$, with $c = \typemapfunc(\vx)$;

* $\typemapfunc(\vx) = \typemapfunc(\vy)$ whenever
D; and,

* $\typemapfunc(\vx) \neq \typemapfunc(\vy)$
for every constraint $\vx \neq \vy$ occurring in a template $\tau \in \transcopies{D}$.

To aid the construction of $\typemapset$ and $\typemapfunc$, we first define a coloring function $\colorf$
that assigns a color to each tuple occurring in the schedule $\schedule$
such that the following holds:
for every pair of tuples $\x$ and $\y$ occurring in $\schedule$:

* connected tuples are mapped to the same color: if $\barmu(\vx) = \x$, $\barmu(\vy) = \y$ and $\conn{\vx}{\vy}{D}$ for some variables $\vx, \vy$ occurring in $\transcopies{D}$, then $\colorf(\x) = \colorf(\y)$; and

* different tuples of the same type are mapped to different colors: if $\type{\x} = \type{\y}$ and $\x \neq \y$, then $\colorf(\x) \neq \colorf(\y)$.

Note that we can always construct such a function $\colorf$
as by Lemma <ref>, it cannot be the case that $\type{\x} = \type{\y}$, $\x \neq \y$ and there is a pair of variables $\vx, \vy$ with $\barmu(\vx) = \x$, $\barmu(\vy) = \y$, and $\conn{\vx}{\vy}{D}$ .

For $\alpha\in\range{\colorf}$, define the type mapping $c_{\alpha}$ as follows: for every type $R \in \schRel$:

c_{\alpha}(R) =
\begin{cases}
\x & \text{if $\colorf(\x) = \alpha$ and $\type{\x} = R$,}\\
\y_{c,R} & \text{otherwise,}
\end{cases}

where $\y_{c,R}$ is an arbitrary tuple of type $R$ not occurring in $\schedule$ or any other type mapping $c_{\beta}$ for $\beta\in\range{\colorf}$. Define $\typemapset=\{c_\alpha\mid \alpha\in\range{\colorf}\}$.
By construction, every type mapping in $\typemapset$ is well defined and all type mappings are over disjoint ranges.
Furthermore, $c_\alpha \neq c_\beta$ whenever $\alpha\neq\beta$.

We now construct $\typemapfunc$ as follows:
$\typemapfunc(\vx) = c_{\alpha}$ with $\alpha = \colorf(\barmu(\vx))$
for every variable $\vx$ occurring in $\transcopies{D}$. It remains to argue that $\typemapfunc$ indeed satisfies all properties stated in Lemma <ref>. By construction of $\typemapset$ and $\typemapfunc$, we have $\barmu(\vx) = c(\type{\vx})$ for every variable $\vx$, with $c  = \typemapfunc(\vx)$.
Towards the second property, notice that $\conn{\vx}{\vy}{D}$ implies $\typemapfunc(\vx) = c_{\colorf(\barmu(\vx))} = c_{\colorf(\barmu(\vy))} = \typemapfunc(\vy)$ by definition of $\colorf$ and $\typemapfunc$.
For the last property, assume $\vx \neq \vy$ occurs in a  $\tau \in \transcopies{D}$ and $\type{\vx} = \type{\vy}$. Since $\barmu$ is admissible for database $\db$, $\barmu(\vx) \neq \barmu(\vy)$.
Then, by definition of $\colorf$ and $\typemapfunc$, we have $\typemapfunc(\vx) = c_{\colorf(\barmu(\vx))} \neq c_{\colorf(\barmu(\vy))} = \typemapfunc(\vy)$.

From $D = (\tau_1, o_1, p_2, \tau_2), \ldots, (\tau_m, o_m, p_1, \tau_1)$ and $\typemapfunc$ 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} = \typemapfunc(\myvar{o_i})$ and $c_{p_i} = \typemapfunc(\myvar{p_i})$ for $i \in [1,m]$.
Intuitively, this sequence of quintuples can be used to reconstruct the original multiversion split schedule $\schedule$.
The next Lemma shows that we can decide robustness against over a set of  admitting multi-tree bijectivity by searching for a specific sequence of quintuples over at most four type mappings.

Let $\workload\in \mtbtemplates$
and let $\typemapset = \{c_1, c_2, c_3, c_4\}$ be a set consisting of four type mappings with disjoint ranges. Then, $\workload$ is not robust against iff there is 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})$ with $m \geq 2$ such that for each quintuple $(\tau_i, o_i, c_{o_i}, p_i, c_{p_i})$ in $E$:

*  $o_i$ and $p_i$ are operations in $\tau_i$, and $c_{o_i}, c_{p_i} \in \typemapset$;

*  $\notconn{\vx_i}{\vy_i}{\tau_i}$ for each constraint $\vx_i \neq \vy_i$ in $\tau_i$;

*  $c_{o_i} = c_{p_i}$ if

*  $c_{o_i} \neq c_{p_i}$ if there is a constraint $\vx_i \neq \vy_i$ in $\tau_i$ with
$\conn{\vx_i}{\myvar{o_i}}{\tau_i}$ and $\conn{\vy_i}{\myvar{p_i}}{\tau_i}$;

*  if $i \neq 1$ and $c_{q_i} = c_{q_1}$ for some $q_i \in \{o_i, p_i\}$ and $q_1 \in \{o_1, p_1\}$,
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 $\conn{\myvar{o_i'}}{\myvar{q_i}}{\tau_i}$ and $\conn{\myvar{o_1'}}{\myvar{q_1}}{\tau_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$.

The items have the following meaning: (<ref>) $\tau_i$ is satisfiable; (<ref>) connected operations are assigned the same type mapping; (<ref>)
variables connected through an inequality are assigned a different type mapping;
(<ref>) $\typemapfunc$ only assigns the same type mapping
to $o_1$ or $p_1$ in $\tau_1$ and $o_i$ or $p_i$ in $\tau_i$ if it does not introduce a dirty write in the resulting multiversion split schedule (cf. Condition (<ref>) in Definition <ref>);
(<ref>) each pair of variables in operations used for conflicts are assigned the same type mapping;
(<ref>, <ref>) the operations used for conflicts between $\tau_1$, $\tau_2$ and $\tau_m$ are restricted to satisfy respectively Condition (<ref>) and (<ref>) in Definition <ref> in the resulting multiversion split schedule.

We first present an additional Lemma derived from Lemma <ref> that will be used in the proof of Lemma <ref>.

Let $D$ be a . If $\conn{\vx}{\vy}{D}$ and $\conn{\vy}{\vz}{D}$ then $\conn{\vx}{\vz}{D}$ for every triple of variables $\vx, \vy, \vz$ occurring in $\transcopies{D}$.

According to Lemma <ref>, $\conn{\vx}{\vy}{D}$ and $\conn{\vy}{\vz}{D}$ imply respectively $\vx \varimplies{}{D} \vy$ and $\vy \varimplies{}{D} \vz$.
By definition, $\vx \varimplies{}{D} \vz$ and hence $\conn{\vx}{\vz}{D}$.

(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$. Notice in particular that $D$ is indeed a  by (<ref>) and (<ref>).
We construct a variable mapping $\barmu$ for $D$ admissible for a database $\db$ such that the  $C = \barmu(D)$ satisfies the conditions in Definition <ref>, thereby proving that $\workload$ is not robust against .

Let $\typemapfunc: \variables \to \typemapset$ be the (partial) function assigning a type mapping in $\typemapset$ to each variable occurring in an operation in $E$:

\typemapfunc(\vx) =
\begin{cases}
c_{o_i} & \text{if $\myvar{o_i} = \vx$ for some $(\tau_i, o_i, c_{o_i}, p_i, c_{p_i}) \in E$,}\\
c_{p_i} & \text{if $\myvar{p_i} = \vx$ for some $(\tau_i, o_i, c_{o_i}, p_i, c_{p_i}) \in E$.}
\end{cases}

This function $\typemapfunc$ is well defined: if there is a $(\tau_i, o_i, c_{o_i}, p_i, c_{p_i}) \in E$ with $\myvar{o_i} = \myvar{p_i} = \vx$, then $\conn{o_i}{p_i}{\tau_i}$ and hence $c_{o_i} = c_{p_i}$ by (<ref>).
Recall that we assume that templates in $E$ are variable-disjoint.
We argue that $\typemapfunc(\vx) = \typemapfunc(\vy)$ if $\conn{\vx}{\vy}{D}$ for each pair of variables $\vx$ and $\vy$ for which $\typemapfunc$ is defined.
From Lemma <ref>, it follows that $\vx \varimplies{}{D} \vy$ whenever $\conn{\vx}{\vy}{D}$. Let $\tau_i$ and $\tau_j$ be the  in which respectively $\vx$ and $\vy$ occur. The argument is now by induction on the definition of $\vx \varimplies{}{D} \vy$:

* If $i = j$ and $\vx \varimplies{}{\tau_i} \vy$, then $\typemapfunc(\vx) = \typemapfunc(\vy)$ is immediate by (<ref>);

* If $(\tau_i, o_i, p_j, \tau_j) \in D$ with $\myvar{o_i} = \vx$ and $\myvar{p_j} = \vy$ (respectively $(\tau_j, o_j, p_i, \tau_i) \in D$ with $\myvar{o_j} = \vy$ and $\myvar{p_i} = \vx$), then $\typemapfunc(\vx) = \typemapfunc(\vy)$ is immediate by (<ref>);

* Otherwise, if $\vx \varimplies{}{D} \vz$ and $\vz \varimplies{}{D} \vy$ for some variable $\vz$, then by induction $\typemapfunc(\vx) = \typemapfunc(\vz) = \typemapfunc(\vy)$.

By Lemma <ref>, $\conn{}{}{D}$ is an equivalence relation. For $\vx$ occurring in $\transcopies{D}$, denote by $[\vx]$ the equivalence class of $\vx$. Let $\typemapset'$ be obtained by extending $\typemapset$ with a type mapping $c_{[\vx]}$ for each equivalence class where no variable $\vy\in[\vx]$ is defined in $\typemapfunc[\typemapset]$. Furthermore, each of the $c_{[\vx]}$ are picked such that all type mappings in $\typemapset'$ have disjoint ranges.

Next, we extend $\typemapfunc$ to a function $\typemapfunc[\typemapset']: \variables \to \typemapset'$ assigning a type mapping to each variable $\vx$ occurring in $\transcopies{D}$
as follows:

\typemapfunc[\typemapset'](\vx) =
\begin{cases}
\typemapfunc(\vx) & \text{if $\typemapfunc$ is defined for $\vx$,}\\
\typemapfunc[\typemapset](\vy) & \text{if $\typemapfunc$ is defined for $\vy$ but not for $\vx$ and $\conn{\vx}{\vy}{D}$,}\\
c_{[\vx]} & \text{otherwise.}
\end{cases}

Notice, furthermore, that in the second case $\vx$ might be connected in $D$ to multiple variables for which $\typemapfunc$ is defined, say $\vy_1$ and $\vy_2$.
Then, by Lemma <ref>, $\conn{\vy_1}{\vy_2}{D}$ and hence $\typemapfunc(\vy_1) = \typemapfunc(\vy_2)$. We therefore conclude that $\typemapfunc[\typemapset'](\vx)$ is well defined.
We argue that $\typemapfunc[\typemapset'](\vx) = \typemapfunc[\typemapset'](\vy)$ if $\conn{\vx}{\vy}{D}$ for each pair of variables $\vx$ and $\vy$.
If $\typemapfunc$ is defined for both $\vx$ and $\vy$, then the result is immediate by $\typemapfunc(\vx) = \typemapfunc(\vy)$.
If $\typemapfunc$ is defined for one of these two variables, say $\vx$, then $\typemapfunc[\typemapset'](\vx) = \typemapfunc[\typemapset](\vx) = \typemapfunc[\typemapset'](\vy)$ by construction of $\typemapfunc[\typemapset']$.
If $\typemapfunc$ is not defined for both $\vx$ and $\vy$, then either there exists a variable $\vz$ for which $\typemapfunc$ is defined and $\vz$ is connected in $D$ to one of these two variables, say $\vx$, or no such variable $\vz$ exists.
In the former case, $\conn{\vz}{\vy}{D}$ follows from Lemma <ref>, implying $\typemapfunc[\typemapset'](\vx) = \typemapfunc[\typemapset](\vz) = \typemapfunc[\typemapset'](\vy)$.
In the latter case, $\typemapfunc[\typemapset'](\vx) = c_{[\vx]}=c_{[\vy]}=\typemapfunc[\typemapset'](\vy)$ by construction of $\typemapfunc[\typemapset']$.

We now define the variable mapping $\barmu$ from $\typemapfunc[\typemapset']$ as
$\barmu(\vx) = c(\type{\vx})$ for each variable $\vx$, where $c = \typemapfunc[\typemapset](\vx)$.
Next, we construct the database $\db$. For each  $\tau_i$ and corresponding variable mapping $\mu_i$ in $\barmu$, we add all tuples in $\mu_i(\tau_i)$ to the database $\db$.
Furthermore, for each constraint $\vx = f(\vy)$ in $\Cset(\tau_i)$, we have $f^\db(\mu_i(\vx)) = \mu_i(\vy)$ in $\db$.
This is well defined for each function $f^\db$.
Towards a contradiction, assume we have $f^\db(\barmu(\vx_i)) = \barmu(\vy_i)$ witnessed by a  $\tau_i$ and $f^\db(\barmu(\vx_j)) = \barmu(\vy_j)$ witnessed by a  $\tau_j$, where $\barmu(\vx_i) = \barmu(\vx_j)$, but $\barmu(\vy_i) \neq \barmu(\vy_j)$.
Since $\conn{\vx_i}{\vy_i}{D}$, $\conn{\vx_j}{\vy_j}{D}$ and $\barmu(\vx_i) = \barmu(\vx_j)$, we have $\typemapfunc[\typemapset'](\vy_i) = \typemapfunc[\typemapset'](\vx_i) = \typemapfunc[\typemapset'](\vx_j) = \typemapfunc[\typemapset'](\vy_j)$.
Then, $\barmu(\vy_i) = \barmu(\vy_j)$, leading to a contradiction.
In order to argue that $\barmu$ is indeed admissible for $\db$, it remains to show that for each constraint $\vx \neq \vy$ in a template $\tau_i$, we have $\barmu(\vx) \neq \barmu(\vy)$. Again towards a contradiction, assume $\barmu(\vx) = \barmu(\vy)$, and let $(\tau_i, o_i, c_{o_i}, p_i, c_{p_i})$ be the corresponding quintuple in $E$.
By definition of $\barmu$, we have $\typemapfunc[\typemapset'](\vx) = \typemapfunc[\typemapset'](\vy)$.
It follows from $\typemapfunc[\typemapset']$ that either $\conn{\vx}{\vy}{\tau_i}$;
or $\conn{\vx}{\myvar{o_i}}{\tau_i}$ (respectively $\conn{\vy}{\myvar{o_i}}{\tau_i}$), $\conn{\vy}{\myvar{p_i}}{\tau_i}$ (respectively $\conn{\vx}{\myvar{p_i}}{\tau_i}$) and $c_{o_i} = c_{p_i}$. However, the former is contradicted by (<ref>) and the latter by (<ref>).
We therefore conclude that $\barmu$ is admissible for $\db$, as it satisfies all constraints.

It remains to argue that the  $C = \barmu(D)$ satisfies all conditions stated in Definition <ref>. The second and third condition are immediate by respectively (<ref>) and (<ref>).
Towards a contradiction, assume the first condition holds. Then, there is an operation $b_1'$ in $\prefix{\barmu(\tau_1)}{\barmu{o_1}}$ ww-conflicting with an operation $b_i'$ in a transaction $\barmu{\tau_i}$.
Let $b_1' = \barmu(o_1')$ with $\myvar{o_1'} = \vx_1$ and $b_i' = \barmu(o_i')$ with $\myvar{o_i'} = \vx$, and let $(\tau_1, o_1, c_{o_1}, p_1, c_{p_1})$ and $(\tau_i, o_i, c_{o_i}, p_i, c_{p_i})$ be the corresponding quintuples in $E$.
Note that $o_1'$ is potentially ww-conflicting with $o_i'$ and $\barmu(\vx_1) = \barmu(\vx_i)$. Then, $\contextfunc[\contextset'](\vx_1) = \contextfunc[\contextset'](\vx_i)$.
By construction of $\contextfunc[\contextset']$, this can only hold if $\conn{\vx_1}{\myvar{q_1}}{\tau_1}$, $\conn{\vx_i}{\myvar{q_i}}{\tau_i}$ and $c_{q_1} = c_{q_i}$ for some $q_1 \in {o_1, p_1}$ and $q_i \in {o_i, p_i}$, thereby contradicting (<ref>).

(only if) If $\workload$ is not robust against , then there exists a multiversion split schedule $\schedule$ based on a  $C$ over a set of transactions $\transset$ consistent with $\workload$ and a database $\db$.
Let $\barmu$ be the variable mapping for a  $D = (\tau_1, o_1, p_1, \tau_2), \ldots, (\tau_m, o_m, p_1, \tau_1)$ over $\workload$ with $\barmu(C) = D$, and let $\typemapset$ and $\typemapfunc$ be as in Lemma <ref>.

From this sequence $D$ and function $\typemapfunc$, we derive the sequence of quintuples $E = (\tau_1, o_1, \typemapfunc(\myvar{o_1}), p_1, \typemapfunc(\myvar{p_1})), \ldots, (\tau_m, o_m, \typemapfunc(\myvar{o_m}), p_m, \typemapfunc(\myvar{p_m}))$.
Let $\typemapfunc' = \{c_1, c_2, c_3, c_4\}$ be a set consisting of four type mappings with disjoint ranges. We adapt each quintuple in $E$ in order, thereby creating a sequence $E'$ satisfying the properties stated in Lemma <ref>. First, we add $(\tau_1, o_1, c_1, p_1, c_k)$ to $E'$, where $c_k = c_1$ if $\typemapfunc(\myvar{o_1})= \typemapfunc(\myvar{p_1})$, and $c_k = c_2$ otherwise.
For each of the remaining quintuples in $E$, let $(\tau_{i-1}, o_{i-1}, c_{o_{i-1}}, p_{i-1}, c_{p_{i-1}})$ be the quintuple previously added to $E'$. We then add $(\tau_i, o_i, c_{o_i},\allowbreak p_i, c_{p_i})$ to $E'$ where $c_{o_i} = c_{p_{i-1}}$ and

\begin{cases}
c_{o_i} & \text{if $\typemapfunc(\myvar{o_i})= \typemapfunc(\myvar{p_i})$,}\\
c_1 & \text{if $\typemapfunc(\myvar{o_i})= \typemapfunc(\myvar{o_1})$,}\\
c_2 & \text{if $\typemapfunc(\myvar{o_i})= \typemapfunc(\myvar{p_1})$ and $\typemapfunc(\myvar{o_1}) \neq \typemapfunc(\myvar{p_1})$,}\\
c_3 & \text{if $\typemapfunc(\myvar{o_i})\neq \typemapfunc(\myvar{p_i})$ and $c_{p_i} \neq c_3$,}\\
c_4 & \text{otherwise.}
\end{cases}

By construction, for every quintuple $(\tau_i, o_i, c_{o_i}, p_i, c_{p_i})$ in $E'$ we now have

* $c_{o_i}$ = $c_{p_i}$ iff $\typemapfunc(\myvar{o_i}) = \typemapfunc(\myvar{p_i})$; and

* $c_{q_i}$ = $c_{q_1}$ iff $\typemapfunc(\myvar{q_i}) = \typemapfunc(\myvar{q_1})$ for every $q_i \in \{o_i, p_i\}$ and $q_1 \in \{o_1, p_1\}$.

It remains to argue that $E'$ indeed satisfies all required properties.
(<ref>) is trivial by construction.
(<ref>) If $\vx_i \neq \vy_i$ is a constraint in $\tau_i$, then $\typemapfunc(\vx) \neq \typemapfunc(\vy)$ and $\notconn{\vx}{\vy}{D}$ according to Lemma <ref>.
(<ref>) If $\conn{o_i}{p_i}{\tau_i}$, then $\typemapfunc(\myvar{o_i}) = \typemapfunc(\myvar{p_i})$ by Lemma <ref>, and hence $c_{o_i} = c_{p_i}$.
(<ref>) Assume there is a constraint $\vx_i \neq \vy_i$ in a  $\tau_i$ with $\conn{\vx_i}{\myvar{o_i}}{\tau_i}$ and $\conn{\vy_i}{\myvar{p_i}}{\tau_i}$.
By Lemma <ref>, $\typemapfunc(\vx_i) = \typemapfunc(\myvar{o_i}) \neq \typemapfunc(\myvar{p_i}) = \typemapfunc(\vy_i)$, and therefore $c_{o_i} \neq c_{p_i}$.
(<ref>) Let $c_{q_i} = c_{q_1}$ for some $q_i \in \{o_i, p_i\}$ and $q_1 \in \{o_1, p_1\}$, with $i \neq 1$.
Assume towards a contradiction that there is an operation $o_i'$ in $\tau_i$ potentially ww-conflicting with an operation $o_1'$ in $\prefix{\tau_1}{o_1}$ with $\conn{\myvar{o_i'}}{\myvar{q_i}}{\tau_i}$ and $\conn{\myvar{o_1'}}{\myvar{q_1}}{\tau_1}$.
But then $\typemapfunc(\myvar{o_i'}) = \typemapfunc(\myvar{q_i}) = \typemapfunc(\myvar{q_1}) = \typemapfunc(\myvar{o_1'})$, implying that $\barmu(o_i')$ is ww-conflicting with $\barmu(o_1')$, contradicting the properties of $C$ stated in Definition <ref>.
(<ref>) is again trivial by construction.
(<ref>) By Definition <ref>, $\barmu(o_1)$ is rw-conflicting with $\barmu(p_2)$ in $C$. Therefore, $o_1$ is potentially rw-conflicting with $p_2$.
(<ref>) By Definition <ref>, $\barmu(o_1) <_{\barmu(\tau_1)} \barmu(p_1)$ or $\barmu(o_m)$ is rw-conflicting with $\barmu(p_1)$ in $C$. As a result, $o_1 <_{\tau_1} p_1$ or $o_m$ is rw-conflicting with $p_1$.

The characterization for  in Lemma <ref> implies an algorithm guessing the counterexample sequence $E$, thereby proving Theorem <ref>.
Indeed, the algorithm guesses the sequence of quintuples $E$, verifying all conditions for each newly guessed quintuple while only requiring logarithmic space.
Notice in particular that we only need to keep track of two other quintuples when verifying all conditions for the newly guessed quintuple, namely the first quintuple over $\tau_1$ and the quintuple immediately preceding the newly guessed one.
As usual, we can think of the encoding of  and operations mentioned in each quintuple as pointers referring to the corresponding  and operations on the input tape.
Furthermore, we do not encode the four type mappings explicitly as such a representation of a mapping might require polynomial space.
Since we are only interested in (dis)equality between type mappings, an encoding where these four type mappings are represented by four arbitrary strings of constant size suffices.

The algorithm goes as follows: We start by guessing three initial quintuples, representing respectively the first, second and last quintuple of the possible sequence of quintuples as in Lemma <ref>. Consistent with previously used notation, we refer to these quintuples by $E_1$, $E_2$, and $E_m$, with $E_i = (\tau_i, o_i, c_{o_i}, p_i, c_{p_i})$. Note that the indices we use here are not part of the algorithm. They are only used to distinguish between the different considered quintuples in the proof argument.

We store all three quintuples using a logarithmic amount of space, by storing pointers to the respective  in $\workload$, the positions of operations in the respective , and the number $1,2,3$ or $4$ for the type mappings.

At this point, we verify that Condition (7) and (8) are true, that Conditions (1-5) are true for all chosen  and operations, and that Condition (6) is true for $\tau_1$ and $\tau_2$, and $\tau_2$ and $\tau_m$. We reject the guessed quintuples if any of the conditions is false.

If all previous checks are true, we proceed by inserting another step. Let $i=2$. We guess a new quintuple $E_{i+1}$ and verify that Condition (5) is true for $\tau_{i}$ and $\tau_{i+1}$ and that Conditions (1-6) are true for $\tau_{i+1}$ and reject the entire construction if one of these conditions failed. Notice that all Conditions, including Condition (5) can be checked easily, particularly because quintuple $E_1$ is stored. To proceed, we discard quintuple $E_i$ and store $E_{i+1}$ instead, thus without increasing the  amount of space we use.

If $\tau_{i+1}$ and $\tau_m$ (from quintuple $E_m$) have Condition (6), the algorithm emits an accept. Indeed, then the sequence $E_1, \ldots, E_i, E_{i+1}, E_m$ of guessed quintuples has all the properties of Lemma <ref>. Otherwise, the algorithm proceeds with another insertion step, for $i=i+1$.

§ ROBUSTNESS FOR  OVER ACYCLIC SCHEMAS

[draw, rounded rectangle,align=center] (W) at (-5,0) ;
[draw, rounded rectangle,align=center] (D) at (-2.5,0) ;
[draw, rounded rectangle,align=center] (C) at (0,0) ;
[draw, rounded rectangle,align=center] (O) at (2.5,0) ;
[draw, rounded rectangle,align=center] (OL) at (5,0) ;
[draw, rounded rectangle,align=center] (S) at (0,-1) ;
[->] (D) to (W) ;
[->] (C) to (D) ;
[->] (O) to (C) ;
[->] (OL) to (O) ;
[->] (S.west) to [bend left=10] (W) ;
[->] (OL) to [bend left=10] (S.east) ;

Acyclic schema graph for the TPC-C benchmark.

We denote by  the class of all sets of  over acyclic schemas.
As a concrete example, the schema graph for the TPC-C benchmark is given in Figure <ref>. Since this schema graph does not contain any cycles, the TPC-C benchmark is situated within . Notice in particular how this acyclic schema graph corresponds to the hierarchical structure of many-to-one relationships inherent to the schema for this benchmark. For example, every orderline belongs to exactly one order, and every order is related to exactly one customer, but the opposite is never true (i.e., a customer can be related to multiple orders, each of which can be related to multiple orderlines). In general, the results presented in this section can be applied to all workloads over schemas with such a hierarchical structure.

is decidable in .

We first provide some intuition for the proof. For a given acyclic schema graph $\sgname$,
$R \asgimplies{F}{\sgname} S$ denotes the directed path from node $R$ to node $S$ in $\sgname$ with $F$ the sequence of edge labels on the path.
The next lemma relates implication between variables to paths in $\sgname$.

Let $D$ be a  over a set of  $\workload\in \acyctemplates$. For every pair of variables $\vx, \vy$ occurring in $\transcopies{D}$, if $\vx \varimplies{F}{D} \vy$,
then $\type{\vx} \asgimplies{F}{SG} \type{\vy}$, with $\sgname$ the corresponding schema graph.

Let $\tau_i$ and $\tau_j$ be the  in $D$ in which $\vx$ and $\vy$ occur, respectively.
The proof is by induction on the definition of $\vx \varimplies{F}{D} \vy$.

(Implication within the same ) If
$i=j$ and $\vx \varimplies{F}{\tau_i} \vy$, then either $F = \varepsilon$ and $\vx = \vy$, or there is a variable $\vz$ such that $\vy = f(\vz)$ is a constraint in $\Cset(\tau_i)$, $\vx \varimplies{F'}{\tau_i} \vz$ and $F = F' \cdot f$.
In the former case, $\type{\vx} = \type{\vy}$, so $\type{\vx} \asgimplies{\varepsilon}{\sgname} \type{\vy}$ is immediate. In the latter case, it follows by induction that $\type{\vx} \asgimplies{F'}{\sgname} \type{\vz}$.
Since $\dom{f} = \type{\vz}$ and $\range{f} = \type{\vy}$, it follows by definition that $\type{\vz} \asgimplies{f}{\sgname} \type{\vy}$ and furthermore $\type{\vx} \asgimplies{F}{\sgname} \type{\vz}$ holds.

(Implication between ) If $F = \varepsilon$ and $(\tau_i, o_i, p_j, \tau_j)$ (respectively $(\tau_j, o_j, p_i, \tau_i)$) is a  in $D$, with $\myvar{o_i} = \vx$ and $\myvar{p_j} = \vy$ (respectively $\myvar{p_i} = \vx$ and $\myvar{o_j} = \vy$), then $\type{\vx} = \type{\vy}$ by definition of potentially conflicting operations. So, $\type{\vx} \asgimplies{\varepsilon}{\sgname} \type{\vy}$ is again immediate.

(Inductive case) If $\vx \varimplies{F_1}{D} \vz$ and $\vz \varimplies{F_2}{D} \vy$ for some variable $\vz$ with $F = F_1 \cdot F_2$,
then $\type{\vx} \asgimplies{F_1}{\sgname} \type{\vz}$ and $\type{\vz} \asgimplies{F_2}{\sgname} \type{\vy}$ follow by induction. We conclude that $\type{\vx} \asgimplies{F}{\sgname} \type{\vy}$.