Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels]Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels

Ahmed Bouajjani

Université Paris Cité, CNRS, IRIF

Constantin Enea

LIX, Ecole Polytechnique, CNRS and Institut Polytechnique de Paris

Enrique Román-Calvo

Université Paris Cité, CNRS, IRIF

Modern applications, such as social networking systems and e-commerce platforms are centered around using large-scale databases for storing and retrieving data. Accesses to the database are typically enclosed in transactions that allow computations on shared data to be isolated from other concurrent computations and resilient to failures. Modern databases trade isolation for performance. The weaker the isolation level is, the more behaviors a database is allowed to exhibit and it is up to the developer to ensure that their application can tolerate those behaviors.

In this work, we propose stateless model checking algorithms for studying correctness of such applications that rely on dynamic partial order reduction. These algorithms work for a number of widely-used weak isolation levels, including Read Committed, Causal Consistency, Snapshot Isolation and Serializability. We show that they are complete, sound and optimal, and run with polynomial memory consumption in all cases. We report on an implementation of these algorithms in the context of Java Pathfinder applied to a number of challenging applications drawn from the literature of distributed systems and databases.

<concept_desc>Theory of computation Verification by model checking</concept_desc>
<concept_desc>Theory of computation Distributed computing models</concept_desc>

<concept_desc>Software and its engineering Formal software verification</concept_desc>

[500]Theory of computation Verification by model checking
[500]Theory of computation Distributed computing models

[500]Software and its engineering Formal software verification

§ INTRODUCTION

Data storage is no longer about writing data to a single
disk with a single point of access. Modern applications require not just data
reliability, but also high-throughput concurrent accesses.
Applications concerning supply chains, banking, etc. use traditional relational databases
for storing and processing data, whereas applications such as social networking
software and e-commerce platforms
use cloud-based storage systems (such as Azure Cosmos DB <cit.>, Amazon DynamoDB
<cit.>, Facebook TAO <cit.>, etc.).

Providing high-throughput processing, unfortunately, comes at an unavoidable cost of weakening
the consistency guarantees offered to users:
Concurrently-connected clients may end up observing different versions of the same data.
These “anomalies” can be prevented by using a strong isolation level
such as Serializability <cit.>, which essentially offers a single version of the data to all clients at any point in time.
However, serializability requires expensive synchronization and incurs a high performance cost. As a
consequence, most storage systems use weaker isolation levels, such as
Causal Consistency <cit.>,
Snapshot Isolation <cit.>, Read
Committed <cit.>, etc. for better performance.
In a recent survey of
database administrators <cit.>, 86% of the participants responded that
most or all of the transactions in their databases execute at Read Committed level.

A weaker isolation level allows for more possible behaviors than stronger
isolation levels. It is up to the developers then to ensure that their
application can tolerate this larger set of behaviors. Unfortunately, weak
isolation levels are hard to understand or reason about
<cit.> and resulting application bugs
can cause loss of business <cit.>.

Model Checking Database-Backed Applications.
This paper addresses the problem of model checking code for correctness against a given isolation level.

Model checking <cit.> explores the state space of a given program in a systematic manner and it provides high coverage of program behavior. However, it faces the infamous state explosion problem, i.e., the number of executions grows exponentially in the number of concurrent clients.

Partial order reduction (POR) <cit.> is an approach that limits the number of explored executions without sacrificing coverage. POR relies on an equivalence relation between executions where e.g., two executions are equivalent if one can be obtained from the other by swapping consecutive independent (non-conflicting) execution steps. It guarantees that at least one execution from each equivalence class is explored. Optimal POR techniques explore exactly one execution from each equivalence class. Beyond this classic notion of optimality, POR techniques may aim for optimality by avoiding visiting states from which the exploration is blocked.

Dynamic partial order reduction (DPOR) <cit.> has been introduced to explore the execution space (and tracking the equivalence relation between executions) on-the-fly without relying on a-priori static analyses. This is typically coupled with stateless model checking (SMC) <cit.> which explores executions of a program without storing visited states, thereby, avoiding excessive memory consumption.

There is a large body of work on (D)POR techniques that address their soundness when checking a certain class of specifications for a certain class of programs, as well as their completeness and their theoretical optimality (see Section <ref>). Most often these works consider shared memory concurrent programs executing under a strongly consistent memory model.

In the last few years, some works have studied DPOR in the case of shared memory programs running under weak memory models such as TSO or Release-Acquire, e.g. <cit.>. While these algorithms are sound and complete, they have exponential space complexity when they are optimal.

More recently, <cit.> defined a DPOR algorithm that has a polynomial space complexity, in addition of being sound, complete and optimal. This algorithm can be applied for a range of shared memory models.

While the works mentioned above concern shared memory programs, we are not aware of any published work addressing the case of database transactional programs running under weak isolation levels. In this paper, we address this case and propose new stateless model checking algorithms relying on DPOR techniques for database-backed applications.  We assume that all the transactions in an application execute under the same isolation level, which happens quite frequently in practice (as mentioned above, most database applications are run on the default isolation level of the database).
Our work generalizes the approach introduced by <cit.>. However, this generalization to the transactional case, covering the most relevant isolation levels, is not a straightforward adaptation of <cit.>. Ensuring optimality while preserving the other properties, e.g., completeness and polynomial memory complexity, is very challenging.

Next, we explain the main steps and features of our work.

Formalizing Isolation Levels.
Our algorithms rely on the axiomatic definitions of isolation
levels introduced by <cit.>. These
definitions use logical constraints called axioms to characterize the
set of executions of a database (e.g., key-value store) that conform to a particular isolation
level (extensible to SQL queries <cit.>). These constraints refer to a specific set of
relations between events/transactions in an execution that describe control-flow
or data-flow dependencies: a program order $\po$ between events in the same
transaction, a session order $\so$ between transactions in the same session[A
session is a sequential interface to the storage system. It corresponds to what
is also called a connection.], and a write-read $\wro$ (read-from) relation that
associates each read event with a transaction that writes the value returned by
the read. These relations along with the events in an
execution are called a history.
A history describes only the
interaction with the database, omitting application-side events (e.g., computing
values written to the database).

Execution Equivalence. DPOR algorithms are parametrized by an equivalence relation on executions, most often, Mazurkiewicz equivalence <cit.>. In this work, we consider a weaker equivalence relation, also known as read-from equivalence <cit.>, which considers that two executions are equivalent when their histories are precisely the same (they contain the same set of events, and the relations $\po$, $\so$, and $\wro$ are the same).
In general, reads-from equivalence is coarser than Mazurkiewicz equivalence, and its equivalence classes can be exponentially-smaller than Mazurkiewicz traces in certain cases <cit.>.

SMC Algorithms.
Our SMC algorithms enumerate executions of a given program under a given isolation level $I$. They are sound, i.e., enumerate only feasible executions (admitted by the program under $I$), complete, i.e., they output a representative of each read-from equivalence class, and optimal, i.e., they output exactly one complete execution from each read-from equivalence class.

For isolation levels weaker than and including Causal Consistency, they satisfy a notion of strong optimality which says that additionally, the enumeration avoids states from which the execution is “blocked”, i.e., it cannot be extended to a complete execution of the program.

For Snapshot Isolation and Serializability, we show that there exists no algorithm in the same class (to be discussed below) that can ensure such a strong notion of optimality. All the algorithms that we propose are polynomial space, as opposed to many DPOR algorithms introduced in the literature.

As a starting point, we define a generic class of SMC algorithms, called swapping based, generalizing the approach adopted by <cit.>, which enumerate histories of program executions. These algorithms focus on the interaction with the database assuming that

the other steps in a transaction concern local variables visible only within the scope of the enclosing session.  Executions are extended according to a generic scheduler function $\genericNext$ and every read event produces several exploration branches, one for every write executed in the past that it can read from. Events in an execution can be swapped to produce new exploration “roots” that lead to different histories. Swapping events is required for completeness, to enumerate histories where a read $r$ reads from a write $w$ that is scheduled by $\genericNext$ after $r$. To ensure soundness, we restrict the definition of swapping so that it produces a history that is feasible by construction (extending an execution which is possibly infeasible may violate soundness). Such an algorithm is optimal w.r.t. the read-from equivalence when it enumerates each history exactly once.

We define a concrete algorithm in this class that in particular, satisfies the stronger notion of optimality mentioned above for every isolation level $I$ which is prefix-closed and causally-extensible, e.g.,  Read Committed and Causal Consistency. Prefix-closure means that every prefix of a history that satisfies $I$, i.e., a subset of transactions and all their predecessors in the causal relation, i.e., $(\so\cup\wro)^+$, is also consistent with $I$, and causal extensibility means that any pending transaction in a history that satisfies $I$ can be extended with one more event to still satisfy $I$, and if this is a read event, then, it can read-from a transaction that precedes it in the causal relation. To ensure strong optimality, this algorithm uses a carefully chosen condition for restricting the application of event swaps, which makes the proof of completeness in particular, quite non-trivial.

We show that isolation levels such as Snapshot Isolation and Serializability are not causally-extensible and that there exists no swapping based SMC algorithm which is sound, complete, and strongly optimal at the same time (independent of memory consumption bounds). This impossibility proof uses a program to show that any $\genericNext$ scheduler and any restriction on swaps would violate either completeness or strong optimality. However, we define an extension of the previous algorithm which satisfies the weaker notion of optimality, while preserving soundness, completeness, and polynomial space complexity. This algorithm will simply enumerate executions according to a weaker prefix-closed and causally-extensible isolation level, and filter executions according to the stronger isolation levels Snapshot Isolation and Serializability at the end, before outputting.

We implemented these algorithms in the Java Pathfinder (JPF) model checker <cit.>, and evaluated them on a number of challenging database-backed applications drawn from the literature of distributed systems and databases.

Our contributions and outline are summarized as follows:

<ref> identifies a class of isolation levels called prefix-closed and causally-extensible that admit efficient SMC.

<ref> defines a generic class of swapping based SMC algorithms based on DPOR which are parametrized by a given isolation level.

<ref> defines a swapping based SMC algorithm which is sound, complete, strongly-optimal, and polynomial space, for any isolation level that is prefix-closed and causally-extensible.

<ref> shows that there exists no swapping based algorithm for Snapshot Isolation and Serializability, which is sound, complete, and strongly-optimal at the same time, and proposes a swapping based algorithm which satisfies “plain” optimality.

<ref> reports on an implementation and evaluation of these algorithms.

Section <ref> recalls the formalization of isolation levels of Biswas and Enea <cit.>, while Sections <ref> and <ref> conclude with a discussion of related work and concluding remarks. Additional formalization, proofs, and experimental data can be found in the technical report <cit.>.

§ TRANSACTIONAL PROGRAMS

§.§ Program Syntax

\begin{align*}
\key\in \Vars\quad \xvar\in\LVars
\end{align*}

\begin{align*}
\mathsf{Prog} &  \eqdef  \mathsf{Sess} \ \mid\  \mathsf{Sess}\,||\,\mathsf{Prog} \\
\mathsf{Sess} & \eqdef  \mathsf{Trans} \ \mid\  \mathsf{Trans}; \mathsf{Sess} \\
\mathsf{Trans} & \eqdef  \ibegin; \mathsf{Body}; \icommit\\
\end{align*}

\begin{align*}
\mathsf{Body} & \eqdef  \mathsf{Instr} \ \mid\  \mathsf{Instr}; \mathsf{Body} \\
\mathsf{Instr} & \eqdef  \mathsf{InstrDB} \ \mid\  a := e \mid\ \iif{\phi(\vec{a})}{\mathsf{Instr}} \\
\mathsf{InstrDB} & \eqdef \xvar := \iread(\key)  \ \mid\  \iwrite(\key,\xvar) \ \mid \ \iabort
%\mathsf{Local} & \eqdef  x := e
\end{align*}

Program syntax. The set of global variables is denoted by $\Vars$ while $\LVars$ denotes the set of local variables.
We use $\phi$ to denote Boolean expressions over local variables, and $e$ to denote expressions over local variables interpreted as values. We use $\vec{\cdot}$ to denote vectors of elements.

Figure <ref> lists the definition of a simple programming language
that we use to represent applications running on top of a database. A program is a set of sessions running in parallel, each
session being composed of a sequence of transactions. Each transaction is
delimited by $\ibegin$ and either $\icommit$ or $\iabort$ instructions,

and its body contains instructions that access the
database and manipulate a set $\LVars$ of local variables.
We use symbols $a$, $b$, etc. to denote elements of $\LVars$.

For simplicity, we abstract the database state as a valuation to a set $\Vars$ of global variables[In the context of a relational database, global variables correspond to fields/rows of a table while in the context of a key-value store, they correspond to keys.], ranged over using $x$, $y$, etc. The instructions accessing the database correspond to reading the value of a global variable and storing it into a local variable $a$ ($a := \iread(x)$) , writing the value of a local variable $a$ to a global variable $x$ ($\iwrite(x,a)$), or an assignment to a local variable $a$ ($a := e$). The set of values of global or local variables is denoted by $\Vals$. Assignments to local variables use expressions $e$ over local variables, which are interpreted as values and whose syntax is left unspecified. Each of these instructions can be guarded by a Boolean condition $\phi(\vec{a})$ over a set of local variables $\vec{a}$ (their syntax is not important). Our results assume bounded programs, as usual in SMC algorithms, and therefore, we omit other constructs like $\mathtt{while}$ loops.
SQL statements (SELECT, JOIN, UPDATE) manipulating relational tables can be compiled to reads or writes of variables representing rows in a table (see for instance, <cit.>).

§.§ Isolation Levels

We present the axiomatic framework introduced
by <cit.> for defining isolation levels.
Isolation levels are defined as logical constraints, called axioms, over histories, which are an abstract representation of the interaction between a program and the database in an execution.

§.§.§ Histories

Programs interact with a database by issuing transactions formed of $\ibegin$, $\icommit$, $\iabort$, $\textsf{read}$ and $\textsf{write}$ instructions. The effect of executing one such instruction is represented using an event $\langle e, \mathit{type} \rangle$ where $e$ is an identifier and $\mathit{type} $ is a type. There are five types of events: $\ebegin$, $\ecommit$, $\eabort$, $\erd{x}$ for reading the global variable $x$, and $\ewrt{x,v}$ for writing value $v$ to $x$. $\Events$ denotes the set of events.
For a read/write event $e$, we use $\mathit{var}(e)$ to denote the variable $x$.

A transaction log $\tup{t,E, \po_t}$ is an identifier $t$ and a finite set of events $E$ along with a strict total order $\po_t$ on $E$, called program order (representing the order between instructions in the body of a transaction).

The minimal element of $\po_t$ is a $\ebegin$ event. A transaction log without neither a $\ecommit$ nor an $\eabort$ event is called pending. Otherwise, it is called complete. A complete transaction log with a $\ecommit$ event is called committed and aborted otherwise. If a $\ecommit$ or an $\eabort$ event occurs, then it is maximal in $\po_t$; $\ecommit$ and $\eabort$ cannot occur in the same log. The set $E$ of events in a transaction log $t$ is denoted by $\events{t}$. Note that a transaction is aborted because it executed an $\iabort$ instruction. Histories do not include transactions aborted by the database because their effect should not be visible to other transactions and the abort is not under the control of the program. For simplicity, we may use the term transaction instead of transaction log.

Isolation levels differ in the values returned by read events which are not preceded by a write on the same variable in the same transaction. We assume in the following that every transaction in a program is executed under the same isolation level. For every isolation level that we are aware of,

if a read of a global variable $x$ is preceded by a write to $x$ in $\po_t$, then it should return the value written by the last write to $x$ before the read (w.r.t. $\po_t$).

The set of $\erd{x}$ events in a transaction log $t$ that are not preceded by a write to $x$ in $\po_t$, for some $x$, is denoted by $\readOp{t}$.

Also, if $t$ does not contain an $\eabort$ event, the set of $\ewrt{x,\_}$ events in $t$ that are not followed by other writes to $x$ in $\po_t$, for some $x$, is denoted by $\writeOp{t}$. If a transaction contains multiple writes to the same variable, then only the last one (w.r.t. $\po_t$) can be visible to other transactions (w.r.t. any isolation level that we are aware of). If $t$ contains an abort event, then we define $\writeOp{t}$ to be the empty set. This is because the effect of aborted transactions (its set of writes) should not be visible to other transactions.
The extension to sets of transaction logs is defined as usual.
Also, we say that a transaction log $t$ writes $x$, denoted by $\writeVar{t}{x}$, when $\writeOp{t}$ contains some $\ewrt{x,\_}$ event.

A history contains a set of transaction logs (with distinct identifiers)
ordered by a (partial) session order $\so$ that represents the order
between transactions in the same session.
It also includes a

write-read relation (also called read-from) that defines read values by associating each read to a transaction that wrote that value. Read events do not contain a value, and their return value is defined as the value written by the transaction associated by the write-read relation.

Let $T$ be a set of transaction logs.
For a write-read relation $\wro\subseteq T\times \readOp{T}$$\wro\subseteq \writeOp{T}\times \readOp{T}$ and variable $\key$, $\wro_\key$ is the restriction of $\wro$ to reads of $\key$, $\wro_\key=\wro\cap (T\times \{ e\ |\ e \mbox{ is a }\erd{\key} \mbox{ event}\})$$\wro_\key=\wro\cap (\writeOp{T}\times \{ e\ |\ e \mbox{ is a }\erd{\key} \mbox{ event}\})$. We extend the relations $\wro$ and $\wro_\key$ to pairs of transactions by $\tup{t_1,t_2}\in \wro$, resp., $\tup{t_1,t_2}\in \wro_\key$, iff there exists a $\wrt{x}{\_}$ event $w$ in $t_1$ and a $\rd{\key}$ event $r$ in $t_2$  s.t. $\tup{t_1,e}\in \wro$, resp., $\tup{t_1,e}\in \wro_\key$$\tup{w,r}\in \wro$, resp., $\tup{w, r}\in \wro_\key$. Analogously, $\wro$ and $\wro_\key$ can be extended to tuples formed of a transaction (containing a write) and a read event. We say that the transaction log $t_1$ is read by the transaction log $t_2$ when $\tup{t_1,t_2}\in \wro$.

A history $\tup{T, \so, \wro}$ is a set of transaction logs $T$ along with a strict partial session order $\so$, and a
write-read relation $\wro\subseteq T\times \readOp{T}$$\wro\subseteq \writeOp{T}\times \readOp{T}$ such that

* the inverse of $\wro$ is a total function,

* if $(t,e)\in \wro$, where $e$ is a $\erd{x}$ event, then $\writeOp{t}$ contains a $\ewrt{x,\_}$ event,if $(w,r)\in \wro$, then $w$ and $r$ are a write and respectively, a read, of the same variable, and

* $\so\cup\wro$ is acyclic (here we use the extension of $\wro$ to pairs of transactions).

Every history includes a distinguished transaction writing the initial values of all global variables. This transaction precedes all the other transactions in $\so$. We use $\hist$, $\hist_1$, $\hist_2$, $\ldots$ to range over histories.

The set of transaction logs $T$ in a history $\hist=\tup{T, \so, \wro}$ is denoted by $\tlogs{\hist}$, and $\events{\hist}$ is the union of $\events{t}$ for $t\in T$. For a history $\hist$ and an event $e$ in $\hist$, $\trans{h}{e}$ is the transaction $t$ in $\hist$ that contains $e$. Also, $\writeOp{\hist}=\bigcup_{t\in \tlogs{h}}\writeOp{t}$ and $\readOp{\hist}=\bigcup_{t\in \tlogs{h}}\readOp{t}$.

We extend $\so$ and $\wro$ to pairs of events by $(e_1,e_2)\in \so$ if $(\trans{h}{e_1},\trans{h}{e_2})\in\so$. Also, $\po=\bigcup_{t\in T} \po_t$.

§.§.§ Axiomatic Framework

[->,>=stealth,shorten >=1pt,auto,node distance=4cm,
semithick, transform shape]
[transaction state, text=black] at (0,0)       (t_1)           $t_1$;
[transaction state] at (2,0)       (t_3)           $t_3$;
[transaction state, text=black,label=above:$\writeVar{ }{\key}$] at (-.5,1.5) (t_2) $t_2$;
(t_1) edge[wrColor] node $\wro_x$ (t_3);

(t_2) edge[bend left] node $(\so \cup \wro)^+$ (t_3);

(t_2) edge[left,double equal sign distance,coColor] node $\co$ (t_1);

$ $

$t_1\neq t_2\ \land \tup{t_1,t_3}\in \wro_x \ \land $

$\writeVar{t_2}{x}\ \land$

$\tup{t_2,t_3}\in(\so \cup \wro)^+$

$\implies \tup{t_2,t_1}\in\co$

$\mathsf{Causal\ Consistency}$

[->,>=stealth,shorten >=1pt,auto,node distance=4cm,
semithick, transform shape]
[transaction state, text=black] at (0,0)       (t_1)           $t_1$;
[transaction state] at (2,0)       (t_3)           $t_3$;
[transaction state, text=black,label=above:$\writeVar{ }{x}$] at (-0.5,1.5) (t_2) $t_2$;
[transaction state] at (1.5,1.5) (t_4) $t_4$;
(t_1) edge[wrColor] node $\wro_x$ (t_3);

(t_2) edge[] node $\co^*$ (t_4);
(t_4) edge[left] node $(\so \cup \wro)$ (t_3);
(t_2) edge[left,double, coColor] node $\co$ (t_1);

$ $

$t_1\neq t_2\ \land \tup{t_1,t_3}\in \wro_x \ \land $

$\writeVar{t_2}{x}\ \land$

$\implies \tup{t_2,t_1}\in\co$

[->,>=stealth,shorten >=1pt,auto,node distance=4cm,
semithick, transform shape]
[transaction state, text=black] at (0,0)       (t_1)           $t_1$;
[transaction state, label=[xshift=-5]below:$\writeVar{ }{\yvar}$] at (2,0)       (t_3)           $t_3$;
[transaction state, text=black,label=above:$\writeVar{}{x}$] at (-.5,1.5) (t_2) $t_2$;
[transaction state, label=[yshift=-2]above:$\writeVar{}{\yvar}$] at (1.5,1.5) (t_4) $t_4$;
(t_1) edge[wrColor] node $\wro_x$ (t_3);

(t_2) edge node $\co^*$ (t_4);
(t_4) edge node $\co$ (t_3);
(t_2) edge[left,double, coColor] node $\co$ (t_1);

$t_1\neq t_2\ \land \ \tup{t_1,t_3}\in \wro_x \ \land$

$ \writeVar{t_2}{\xvar}\ \land \ \writeVar{t_3}{\yvar}\ \land$

$ \writeVar{t_4}{\yvar} \land  \tup{t_2,t_4}\in\co^*$

$\land \ \tup{t_4,t_3}\in\co$

$\implies \tup{t_2,t_1}\in\co$

[->,>=stealth,shorten >=1pt,auto,node distance=4cm,
semithick, transform shape]
[transaction state, text=black] at (0,0)       (t_1)           $t_1$;
[transaction state] at (2,0)       (t_3)           $t_3$;
[transaction state, text=black, label=above:$\writeVar{ }{x}$] at (-.5,1.5) (t_2) $t_2$;
(t_1) edge[wrColor] node $\wro_x$ (t_3);

(t_2) edge[bend left] node $\co$ (t_3);
(t_2) edge[left,double, coColor] node $\co$ (t_1);

$ $

$ $

$t_1\neq t_2\ \land \ \tup{t_1,t_3}\in \wro_x \land$

$ \writeVar{t_2}{x}\ \land \ \tup{t_2,t_3}\in\co$

$\implies \tup{t_2,t_1}\in\co$

Axioms defining isolations levels (all logical variables representing transactions, e.g., $t_1$, are universally quantified). The reflexive and transitive, resp., transitive, closure of a relation $rel$ is denoted by $rel^*$, resp., $rel^+$. Also, $\circ$ denotes the composition of two relations, i.e., $rel_1 \circ rel_2 = \{\tup{a, b} | \exists c. \tup{a, c} \in rel_1 \land \tup{c, b} \in rel_2\}$.

A history satisfies a certain isolation level if there is a strict total order $\co$ on its transactions, called commit order, which extends the write-read relation and the session order, and which satisfies certain properties. These properties, called axioms, relate the commit order with the $\so$ and $\wro$ relations in a history and are

defined as
first-order formulas of the form:

\begin{align}
& \forall \key,\ \forall \tr_1\neq \tr_2,\ \forall \tr_3.\ \nonumber\\
& \hspace{3mm}  \tup{\tr_1,t_3}\in \wro_\key \land \writeVar{\tr_2}{\key} \land \phi(\tr_2,\tr_3) \implies \tup{\tr_2,\tr_1}\in\co \label{eq:axiom}
%  & \hspace{5.4cm} \implies \tup{\tr_2,\tr_1}\in\co \nonumber
\end{align}

where $\phi$ is a property relating $\tr_2$ and $\tau$ (i.e., the read or the
transaction reading from $\tr_1$) that varies from one axiom to another.[These formulas are interpreted on tuples $\tup{\hist,\co}$ of a history $\hist$ and a commit order $\co$ on the transactions in $\hist$ as usual.] Note that an aborted transaction $t$ cannot take the role of $\tr_1$ nor $\tr_2$ in equation <ref> as the set $\writeOp{t}$ is empty. Intuitively, this axiom schema states the following: in order for $\tau$ to read specifically $t_1$'s write on $k$, it must be the case that every $t_2$ that also writes $k$ and satisfies $\phi(t_2,\tau)$ was committed before $t_1$.

The property $\phi$ relates $\tr_2$ and $\tau$ using the relations in a history and the commit order.
Figure <ref> shows two axioms which correspond to their homonymous isolation levels: Causal Consistency ($\CC$) and Serializability ($\SER$). The conjunction of the other two axioms Conflict and Prefix defines Snapshot Isolation ($\SI$). Read Atomic ($\RA$) is a weakening of $\CC$ where $(\so \cup \wro)^+$ is replaced with $\so \cup \wro$. Read Committed ($\RC$) is defined similarly(see Appendix <ref>).

Note that $\SER$ is stronger than $\SI$ (i.e., every history satisfying $\SER$ satisfies $\SI$ as well), $\SI$ is stronger than $\CC$, $\CC$ is stronger than $\RA$, and $\RA$ is stronger than $\RC$.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0, label=[font=]180:$t_1$] (t1) at (0, 1.4) $\ewrt{x,1}$;
[draw, rounded corners=2mm,outer sep=0,label=[font=]0:$t_2$] (t2) at (3, 1.4)  $\erd{x}$
$\ewrt{x,2}$ ;
[draw, rounded corners=2mm,outer sep=0,label=[font=]0:$t_3$] (t3) at (3, 0)  $\erd{x}$
$\erd{y}$ ;
[draw, rounded corners=2mm,outer sep=0,label=[font=]180:$t_4$] (t4) at (0, 0)  $\erd{x}$

(t1) edge[above] node[yshift=0,xshift=0] $\wro_x$ (t2);

(t1) edge[below] node[yshift=-3,xshift=3] $\wro_x$ (t3);

(t2) edge[above] node[yshift=-6,xshift=-18] $\wro_x$ (0,0.58);

(t4) edge[below] node[yshift=0,xshift=0] $\wro_y$ (t3);

Causal Consistency violation. Boxes group events from the same transaction.

For instance, the axiom defining Causal Consistency <cit.> states that for any transaction $\tr_1$ writing a variable $x$ that is read in a transaction $\tr_3$, the set of $(\wro\cup \so)^+$ predecessors of $\tr_3$ writing $x$ must precede $\tr_1$ in commit order ($(\wro\cup \so)^+$ is usually called the causal order). A violation of this axiom can be found in Figure <ref>: the transaction $\tr_2$ writing 2 to $x$ is a $(\wro\cup \so)^+$ predecessor of the transaction $\tr_3$ reading 1 from $x$ because the transaction $\tr_4$, writing 1 to $y$, reads $x$ from $\tr_2$ and $\tr_3$ reads $y$ from $\tr_4$. This implies that $\tr_2$ should precede in commit order the transaction $\tr_1$ writing 1 to $x$, which is inconsistent with the write-read relation ($\tr_2$ reads from $\tr_1$).

The $\mathsf{Serializability}$ axiom requires that for any transaction $\tr_1$ writing to a variable $x$ that is read in a transaction $\tr_3$, the set of $\co$ predecessors of $\tr_3$ writing $x$ must precede $\tr_1$ in commit order. This ensures that each transaction observes the effects of all the $\co$ predecessors.

For an isolation level $I$ defined by a set of axioms $X$, a history
$\hist=\tup{T, \so, \wro}$ satisfies $I$ iff there is a strict total
order $\co$ s.t. $\wro\cup\so\subseteq \co$ and $\tup{h,\co}$ satisfies $X$.

A history that satisfies an isolation level $I$ is called $I$-consistent. For two isolation levels $I_1$ and $I_2$, $I_1$ is weaker than $I_2$ when every $I_1$-consistent history is also $I_2$-consistent.

§.§ Program Semantics

We define a small-step operational semantics for transactional programs, which is parametrized by an isolation level $I$. The semantics keeps a history of previously executed database accesses in order to maintain consistency with $I$.

For readability, we define a program as a partial function $\prog:\mathsf{SessId}\rightharpoonup \mathsf{Sess}$ that associates session identifiers in $\mathsf{SessId}$ with concrete code as defined in Figure <ref> (i.e., sequences of transactions). Similarly, the session order $\so$ in a history is defined as a partial function $\so:\mathsf{SessId}\rightharpoonup \mathsf{Tlogs}^*$ that associates session identifiers with sequences of transaction logs. Two transaction logs are ordered by $\so$ if one occurs before the other in some sequence $\so(j)$ with
$j\in \mathsf{SessId}$.

The operational semantics is defined as a transition relation $\Rightarrow_I$ between configurations, which are defined as tuples containing the following:

* history $\hist$ storing the events generated by database accesses executed in the past,

* a valuation map $\vec{\gamma}$ that records local variable values in the current transaction of each session ($\vec{\gamma}$ associates identifiers of sessions with valuations of local variables),

* a map $\vec{B}$ that stores the code of each live transaction (mapping session identifiers to code),

* sessions/transactions $\prog$ that remain to be executed from the original program.

The relation $\Rightarrow_I$ is defined using a set of rules as expected(their precise definition can be found in Appendix <ref>).
Starting a new transaction in a session $j$ is enabled as long as this session has no live transactions ($\vec{\mathsf{B}}(j) = \epsilon$) and results in adding a transaction log with a single $\ebegin$ event to the history and scheduling the body of the transaction (adding it to $\vec{\mathsf{B}}(j)$). Local steps, i.e., checking a Boolean condition or computation with local variables, use the local variable valuations and advance the code as expected. Read instructions of some global variable $x$ can have two possible behaviors: (1) if the read follows a write on $x$ in the same transaction, then it returns the value written by the last write on $x$ in that transaction, and (2) otherwise, the read reads from another transaction $\tr'$ which is chosen non-deterministically as long as extending the current history with the write-read dependency associated to this choice leads to a history that still satisfies $I$. Depending on the isolation level, there may not exist a transaction $\tr'$ the read can read from(see Appendix <ref> for a concrete example). For other instructions, e.g., $\icommit$ and $\iabort$, the history is simply extended with the corresponding events while ending the transaction execution in the case of $\iabort$.

An initial configuration for program $\prog$ contains the program $\prog$, a history $\hist=\tup{\{\tr_0\},\emptyset,\emptyset}$ where $\tr_0$ is a transaction log containing writes that write the initial value for all variables, and empty current transaction code ($\mathsf{B}=\epsilon$).
An execution of a program $\prog$ under an isolation level $I$ is a sequence of configurations $c_0 c_1\ldots c_n$ where $c_0$ is an initial configuration for $\prog$, and $c_m\Rightarrow_I c_{m+1}$, for every $0\leq m < n$. We say that $c_n$ is $I$-reachable from $c_0$.
The history of such an execution is the history $\hist$ in the last configuration $c_n$.
A configuration is called final if it contains the empty program ($\prog=\emptyset$).
Let $\histOf[I]{\prog}$ denote the set of all histories of an execution of $\prog$ under $I$ that ends in a final configuration.

§ PREFIX-CLOSED AND CAUSALLY-EXTENSIBLE ISOLATION LEVELS

We define two properties of isolation levels, prefix-closure and causal extensibility, which enable efficient DPOR algorithms (as shown in Section <ref>).

§.§ Prefix Closure

For a relation $R\subseteq A\times A$, the restriction of $R$ to $A'\times A'$, denoted by $R\downarrow A'\times A'$, is defined by $\{(a,b): (a,b)\in R, a,b\in A'\}$. Also, a set $A'$ is called $R$-downward closed when it contains $a\in A$ every time it contains some $b\in A$ with $(a,b)\in R$.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t1) at (-3.25, 0)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0] (t2) at (-3.25, -1.6)
[draw, rounded corners=2mm,outer sep=0] (t3) at (0, 0)
[draw, rounded corners=2mm,outer sep=0] (t4) at (0, -1.6)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1x);
(t2.north west) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.west) coordinate[pos=0.67] (t3x);

(t3.west) edge [below] node[right] $\wro_x$ (t2.north east);
(t1.south) edge [above] node[left] $\so \cap \wro_y$ (t2.north);
(t1.east) edge [above] node[above] $\so$ (t3.west);
(t3.south) edge node[right] $\wro_x$ (t4.north);
(t1.south east) edge node[below] $\so$ (t4.north west);

A history.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t1) at (-3.25, 0)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0] (t2) at (-3.25, -1.6)
[draw, rounded corners=2mm,outer sep=0] (t3) at (0, 0)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1x);
(t2.north west) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.west) coordinate[pos=0.67] (t3x);

(t3.west) edge [below] node[right] $\wro_x$ (t2.north east);
(t1.south) edge [above] node[left] $\so \cap \wro_y$ (t2.north);
(t1.east) edge [above] node[above] $\so$ (t3.west);

A prefix.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t1) at (-3.25, 0)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0, ] (t2) at (-3.25, -1.4)

[draw, rounded corners=2mm,outer sep=0] (t4) at (0, -1.4)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1x);
(t2.north west) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.west) coordinate[pos=0.67] (t3x);

(t1.south east) edge node[below] $\so$ (t4.north west);

(t1.south) edge [above] node[left] $\so \cap \wro_y$ (t2.north);

Not a prefix.

Explaining the notion of prefix of a history. $\init$ denotes the transaction log writing initial values. Boxes group events from the same transaction.

A prefix of a transaction log $\tup{t,E, \po_t}$ is a transaction log $\tup{t,E', \po_t \downarrow E'\times E'}$ such that $E'$ is $\po_t$-downward closed.
A prefix of a history $\hist=\tup{T, \so, \wro}$ is a history $\hist'=\tup{T',\so\downarrow T'\times T',\wro\downarrow T'\times T'}$ such that every transaction log in $T'$ is a prefix of a different transaction log in $T$ but carrying the same id, $\events{\hist'}\subseteq\events{\hist}$, and $\events{\hist'}$ is $(\po\cup \so \cup \wro)^*$-downward closed.
For example, the history pictured in Fig. <ref> is a prefix of the one in Fig. <ref> while the history in Fig. <ref> is not. The transactions on the bottom of Fig. <ref> have a $\wro$ predecessor in Fig. <ref> which is not included.

An isolation level $I$ is called prefix-closed when every prefix of an $I$-consistent history is also $I$-consistent.

Every isolation level $I$ discussed above is prefix-closed because if a history $\hist$ is $I$-consistent with a commit order $\co$, then the restriction of $\co$ to the transactions that occur in a prefix $\hist'$ of $\hist$ satisfies the corresponding axiom(s) when interpreted over $\hist'$.

Read Committed, Read Atomic, Causal Consistency, Snapshot Isolation, and Serializability are prefix closed.

Let $\hist$ be a history that satisfies one of these isolation levels, and let $\co$ be a commit order of $\hist$ that satisfies the corresponding axiom(s). The restriction of $\co$ to the transactions that occur in a prefix $\hist'$ of $\hist$ satisfies the corresponding axiom(s) when interpreted over $\hist'$.

§.§ Causal Extensibility

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t1) at (-3.25, 0)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0] (t2) at (-3.25, -1.6)
[draw, rounded corners=2mm,outer sep=0] (t3) at (0, 0)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1x);
(t2.north west) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.west) coordinate[pos=0.67] (t3x);

(t3.west) edge [below] node[right] $\wro_x$ (t2.north east);
(t1.south) edge [above] node[left] $\so$ (t2.north);
(t1.east) edge [above] node[above] $\so$ (t3.west);

Extensible history.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t1) at (-3.25, 0)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0] (t2) at (-3.25, -1.6)
[draw, rounded corners=2mm,outer sep=0] (t3) at (0, 0)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1x);
(t2.north west) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.west) coordinate[pos=0.67] (t3x);

(t3.west) edge [below] node[right] $\wro_x$ (t2.north east);
(t1.south) edge [above] node[left] $\so \cap \wro_y$ (t2.north);
(t1.east) edge [above] node[above] $\so$ (t3.west);

Non-extensible history.

Explaining causal extensibility. $\init$ denotes the transaction log writing initial values. Boxes group events from the same transaction.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t1) at (-1.5, -0.25)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0] (t2) at (-3, -2)
[draw, rounded corners=2mm,outer sep=0] (t3) at (0, -2)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1sw);
(t1.south east) – (t1.south) coordinate[pos=0.67] (t1se);
(t2.north east) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.north) coordinate[pos=0.67] (t3x);

(t1sw) edge [left] node $\wro_x$ (t2x);
(t1se) edge [right] node $\wro_y$ (t3x);

A counter-example to causal extensibility for $\SI$ and $\SER$.

The $\so$-edges from $\init$ to the other transactions are omitted for legibility.

We start with an example to explain causal extensibility. Let us consider the histories $h_1$ and $h_2$ in Figures <ref> and <ref>, respectively, without the events $\erd{y}$ and $\ewrt{y,2}$ written in blue bold font. These histories satisfy Read Atomic.

The history $h_1$ can be extended by adding the event $\rd{y}$ and the $\wro$ dependency $\wro(\init,\rd{y})$ while still satisfying Read Atomic.

On the other hand, the history $h_2$ can not be extended with the event $\wrt{y}{2}$ while still satisfying Read Atomic. Intuitively, if the reading transaction on the bottom reads $x$ from the transaction on the right, then it should read $y$ from the same transaction because this is more “recent” than $\init$ w.r.t. session order. The essential difference between these two extensions is that the first concerns a transaction which is maximal in $(\so\cup\wro)^+$ while the second no. The extension of $\hist_2$ concerns the transaction on the right in Figure <ref> which is a $\wro$ predecessor of the reading transaction. Causal extensibility will require that at least the $(\so\cup\wro)^+$ maximal (pending) transactions can always be extended with any event while still preserving consistency. The restriction to $(\so\cup\wro)^+$ maximal transactions is intuitively related to the fact that transactions should not read from non-committed (pending) transactions, e.g., the reading transaction in $\hist_2$ should not read from the still pending transaction that writes $x$ and later $y$.

Formally, let  $\hist=\tup{T, \so, \wro}$ be a history. A transaction $t$ is called $(\so \cup \wro)^+$-maximal in $h$ if $h$ does not contain any transaction $t'$ such that $(t,t')\in (\so \cup \wro)^+$. We define a causal extension of a pending transaction $t$ in $h$ with an event $e$ as a history $h'$ such that:

* $e$ is added to $t$ as a maximal element of $\po_t$,

* if $e$ is a read event and $t$ does not contain a write to $\mathit{var}(e)$, then $\wro$ is extended with some tuple $(t',e)$ such that $(t', t) \in  (\so \cup \wro)^+$ in $h$ (if $e$ is a read event and $t$ does contain a write to $\mathit{var}(e)$, then the value returned by $e$ is the value written by the latest write on $\mathit{var}(e)$ before $e$ in $t$; the definition of the return value in this case is unique and does not involve $\wro$ dependencies),

* the other elements of $\hist$ remain unchanged in $h'$.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t0) at (-1.5, 0)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0, label=[font=]100:$t_1$] (t1) at (-3, -1.6)
[draw, rounded corners=2mm,outer sep=0, label=[font=]50:$t_2$] (t2) at (-3, -3.2)
[draw, rounded corners=2mm,outer sep=0, label=[font=]50:$t_3$] (t3) at (0, -1.6)
[draw, rounded corners=2mm,outer sep=0, label=[font=]50:$t_4$] (t4) at (0, -3.2)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1x);
(t2.north west) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.west) coordinate[pos=0.67] (t3x);

(t3.south) edge node[right] $\so$ (t4.north);
(t1.south) edge node[left] $\so$ (t2.north);
(t1.south east) edge node[above] $\wro_y$ (t4.north west);
(t0.south) edge node[above] $\so$ (t1.north);
(t0.south) edge node[above] $\so$ (t3.north);

History $\hist$.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t0) at (-1.5, 0)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0, label=[font=]100:$t_1$] (t1) at (-3, -1.6)
[draw, rounded corners=2mm,outer sep=0, label=[font=]50:$t_2$] (t2) at (-3, -3.2)
[draw, rounded corners=2mm,outer sep=0, label=[font=]50:$t_3$] (t3) at (0, -1.6)
[draw, rounded corners=2mm,outer sep=0, label=[font=]50:$t_4$] (t4) at (0, -3.2)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1x);
(t2.north west) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.west) coordinate[pos=0.67] (t3x);

(t3.south) edge node[right] $\so$ (t4.north);
(t1.south) edge node[left] $\so$ (t2.north);
(t1.south east) edge node[above, xshift = 4mm,yshift=-1mm] $\wro_y$, $\wro_x$ (t4.north west);
(t0.south) edge node[above] $\so$ (t1.north);
(t0.south) edge node[above] $\so$ (t3.north);

$t_4$ reads $x$ and $y$ from $t_1$.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t0) at (-1.5, 0)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0, label=[font=]100:$t_1$] (t1) at (-3, -1.6)
[draw, rounded corners=2mm,outer sep=0, label=[font=]50:$t_2$] (t2) at (-3, -3.2)
[draw, rounded corners=2mm,outer sep=0, label=[font=]50:$t_3$] (t3) at (0, -1.6)
[draw, rounded corners=2mm,outer sep=0, label=[font=]10:$t_4$] (t4) at (0, -3.2)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1x);
(t2.north west) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.west) coordinate[pos=0.67] (t3x);

(t1.south east) edge node[above] $\wro_y$ (t4.north west);
(t3.south) edge node[right] $\so \cap \wro_x$ (t4.north);
(t1.south) edge node[left] $\so$ (t2.north);
(t0.south) edge node[above] $\so$ (t1.north);
(t0.south) edge node[above] $\so$ (t3.north);

$t_4$ reads $x$ from $t_3$, $y$ from $t_1$.

Two causal extensions of the history $h$ on the left with the $\erd{x}$ event written in blue.

For example, Figure <ref> and <ref> present two causal extensions with a $\erd{x}$ event of the transaction $t_4$ in the history $\hist$ in Figure <ref>. The new read event reads from transaction $t_1$ or $t_3$ which were already related by $(\so \cup \wro)^+$ to $t_4$.
An extension of $h$ where the new read event reads from $t_2$ is not a causal extension because $(t_2, t_4) \not\in (\so \cup \wro)^+$.

An isolation level $I$ is called causally-extensible if for every $I$-consistent history $h$, every $(\so \cup \wro)^+$-maximal pending transaction $t$ in $h$, and every event $e$, there exists a causal extension $\hist'$ of $t$ with $e$ that is $I$-consistent.

The proof of the following theorem can be found in Appendix <ref>.

Causal Consistency, Read Atomic, and Read Committed are causally-extensible.

Snapshot Isolation and Serializability are not causally extensible.
Figure <ref> presents a counter-example to causal extensibility: the causal extension of the history $\hist$ that does not contain the $\ewrt{x,2}$ written in blue bold font with this event does not satisfy neither Snapshot Isolation nor Serializability although $\hist$ does. Note that the causal extension with a write event is unique. (Note that both $h$ and this causal extension satisfy Causal Consistency and therefore, as expected, this counter-example does not apply to isolation levels weaker than Causal Consistency.)

§ SWAPPING-BASED MODEL CHECKING ALGORITHMS

We define a class of stateless model checking algorithms for enumerating executions of a given transactional program, that we call swapping-based algorithms. Section <ref> will describe a concrete instance that applies to isolation levels that are prefix-closed and causally extensible.

These algorithms are defined by the recursive function explore listed in Algorithm <ref>. The function explore receives as input a program $\prog$, an ordered history $\hist_<$, which is a pair $(\hist,<)$ 0pt

explore algorithm
[1]
explore$\prog$, $\hist_<$, $\locals$
$j, e, \gamma \gets  \genericNext(\prog, \hist_<, \locals)$

$\locals' \gets \locals[e\mapsto \gamma]$
$e = \bot$ and $\genericEvaluate(h)$

output $h$, $\locals'$

$\mathit{type}(e) = \iread$

$t \in \genericValidWrites(h,e)$
$h'_< \gets h_< \oplus_j e \oplus \wro(t,e)$

$\textsc{explore}(\prog, h'_< , \locals')$

$\textsc{exploreSwaps}(\prog, h'_< , \locals')$

$h'_< \gets h_< \oplus_j e$
$\textsc{explore}(\prog, h'_<,\locals')$
$\textsc{exploreSwaps}(\prog, h'_< , \locals')$

of a history and a total order $<$ on all the events in $\hist$, and a mapping $\locals$ that associates each event $e$ in $\hist$ with the valuation of local variables in the transaction of $e$ ($\trans{h}{e}$) just before executing $e$.
For an ordered history $(\hist,<)$ with $\hist=\tup{T, \so, \wro}$, we assume that $<$ is consistent with $\po$, $\so$, and $\wro$, i.e., $e_1 < e_2$ if $(\trans{h}{e_1},\trans{h}{e_2})\in (\so\cup\wro)^+$ or $(e_1,e_2)\in\po$. Initially, the ordered history and the mapping $\locals$ are empty.

The function explore starts by calling $\genericNext$ to obtain an event representing the next database access in some pending transaction of $\prog$, or a  $\ebegin$/$\ecommit$/$\eabort$ event for starting or ending a transaction. This event is associated to some session $j$. For example, a typical implementation of $\genericNext$ would choose one of the pending transactions (in some session $j$), execute all local instructions until the next database instruction in that transaction (applying the transition rules if-true, if-false, and localfrom Figure <ref> in Appendix <ref>) and return the event $e$ corresponding to that database instruction and the current local state $\gamma$. $\genericNext$ may also return $\bot$ if the program finished.

If $\genericNext$ returns $\bot$, then the function $\genericEvaluate$ can be used to filter executions that satisfy the intended isolation level before outputting the current history and local states (the use of $\genericEvaluate$ will become relevant in Section <ref>).

Otherwise, the event $e$ is added to the ordered history $h_<$. If $e$ is a read event, then $\genericValidWrites$ computes a set of write events $w$ in the current history that are valid for $e$, i.e., adding the event $e$ along with the $\wro$ dependency $(w,e)$ leads to a history that still satisfies the intended isolation level.

Concerning notations, let $\hist$ be a history where $\so$ is represented as a function $\so:\mathsf{SessId}\rightharpoonup \mathsf{Tlogs}^*$ (as in  <ref>).

For event $e$, $\hist\oplus_j e$ is the history obtained from $\hist$ by adding $e$ to the last transaction in $\so(j)$ as the last event in $\po$ (i.e.,  if $\so(j)=\sigma; \tup{t,E,\po_t}$, then the session order $\so'$ of $\hist\oplus_j e$ is defined by $\so'(k)=\so(k)$ for all $k\neq j$ and $\so(j) =\sigma; \tup{t,E\cup\{e\},\po_t\cup \{(e',e): e'\in E\}}$). This is extended to ordered histories: $(\hist,<) \oplus_j e$ is defined as $(\hist \oplus_j e, < \cdot\ e)$ where $<\cdot\ e$ means that $e$ is added as the last element of $<$. Also, $\hist \oplus_j (e,\ebegin)$ is a history where $\tup{\tr,\{\tup{e,\ebegin}\},\emptyset}$ with $\tr$ a fresh id is appended to $\so(j)$, and
$\hist\oplus\wro(t,e)$ is defined by adding $(t,e)$ to the write-read of $\hist$.

[1]
exploreSwaps$\prog$, $\hist_<$, $\locals$

$l \gets \genericCompute(h_<)$
$(\alpha, \beta) \in l$
$\genericProtocol(h_<, \alpha, \beta,\locals)$
$\textsc{explore}(\prog,\genericSwap(h_<, \alpha, \beta, \locals))$

Once an event is added to the current history, the algorithm may explore other histories obtained by re-ordering events in the current one. Such re-orderings are required for completeness. New read events can only read from writes executed in the past which limits the set of explored histories to the scheduling imposed by $\genericNext$. Without re-orderings, writes scheduled later by $\genericNext$ cannot be read by read events executed in the past, although this may be permitted by the isolation level.

The function $\textsc{exploreSwaps}$ calls $\genericCompute$ to compute pairs of sequences of events $\alpha, \beta$ that should be re-ordered; $\alpha$ and $\beta$ are contiguous and disjoint subsequences of the total order $<$, and $\alpha$ should end before $\beta$ (since $\beta$ will be re-ordered before $\alpha$). Typically, $\alpha$ would contain a read event $r$ and $\beta$ a write event $w$ such that re-ordering the two enables $r$ to read from $w$. Ensuring soundness and avoiding redundancy, i.e., exploring the same history multiple times, may require restricting the application of such re-orderings. This is modeled by the Boolean condition called $\genericProtocol$. If this condition holds, the new explored histories are computed by the function $\genericSwap$. This function returns local states as well, which are necessary for continuing the exploration.

We assume that $\genericSwap(\hist_<, \alpha, \beta, \locals)$ returns pairs $(\hist'_{<'},\locals')$ such that

* $\hist'$ contains at least the events in $\alpha$ and $\beta$,

* $\hist'$ without the events in $\alpha$ is a prefix of $\hist$, and

* if a read $r$ in $\alpha$ reads from different writes in $\hist$ and $\hist'$ (the $\wro$ relations of $\hist$ and $\hist'$ associate different transactions to $r$),

then $r$ is the last event in its transaction (w.r.t. $\po$).

The first condition makes the re-ordering “meaningful” while the last two conditions ensure that the history $\hist'$ is feasible by construction, i.e., it can be obtained using the operational semantics defined in Section <ref>. Feasibility of $\hist'$ is ensured by keeping prefixes of transaction logs from $\hist$ and all their $\wro$ dependencies except possibly for read events in $\alpha$ (second condition). In particular, for events in $\beta$, it implies that $\hist'$ contains all their $(\po\cup\so\cup\wro)^*$ predecessors. Also, the change of a read-from dependency is restricted to the last read in a transaction (third condition) because changing the value returned by a read may disable later events in the same transaction[Different $\wro$ dependencies for previous reads can be explored  in other steps of the algorithm.].

A concrete implementation of explore is called:

* $I$-sound if it outputs only histories in $\histOf[I]{\prog}$ for every program $\prog$,

* $I$-complete if it outputs every history in $\histOf[I]{\prog}$ for every program $\prog$,

* optimal if it does not output the same history twice,

* strongly optimal if it is optimal and never engages in fruitless explorations, i.e., explore is never called (recursively) on a history $\hist$ that does not satisfy $I$, and every call to explore results in an output or another recursive call to explore.

§ SWAPPING-BASED MODEL CHECKING FOR PREFIX-CLOSED AND CAUSALLY-EXTENSIBLE ISOLATION LEVELS

We define a concrete implementation of $\textsc{explore}$, denoted as $\textsc{explore-ce}$, that is $I$-sound, $I$-complete, and strongly optimal for any isolation level $I$ that is prefix-closed and causally-extensible. The isolation level $I$ is a parameter of $\textsc{explore-ce}$. The space complexity of $\textsc{explore-ce}$ is polynomial in the size of the program. An important invariant of this implementation is that it explores histories with at most one pending transaction and this transaction is maximal in session order. This invariant is used to avoid fruitless explorations: since $I$ is assumed to be causally-extensible, there always exists an extension of the current history with one more event that continues to satisfy $I$. Moreover, this invariant is sufficient to guarantee completeness in the sense defined above of exploring all histories of “full” program executions (that end in a final configuration).

Section <ref> describes the implementations of $\genericNext$ and $\genericValidWrites$ used to extend a given execution, Section <ref> describes the functions $\genericCompute$ and $\genericSwap$ used to compute re-ordered executions, and Section <ref> describes the $\genericProtocol$ restriction on re-ordering. We assume that the function $\genericEvaluate$ is defined as simply $\genericEvaluate(\hist) ::= true$ (no filter before outputting). Section <ref> discusses correctness arguments (see App. <ref> for proofs).

§.§ Correctness

The following theorem states the correctness of the algorithm presented in this section:

For any prefix-closed and causally extensible isolation level $I$, $\textsc{explore-ce}$ is $I$-sound, $I$-complete, strongly optimal, and polynomial space.

$I$-soundness is a consequence of the $\genericValidWrites$ and $\genericProtocol$ definitions which guarantee that all histories given to recursive calls are $I$-consistent, and of the $\genericSwap$ definition which ensures to only produce feasible histories (which can be obtained using the operational semantics defined in Section <ref>). The fact that this algorithm never engages in fruitless explorations follows easily from causal-extensibility which ensures that any current history can be extended with any event returned by $\genericNext$. Polynomial space is also quite straightforward since the for all loops in Algorithm <ref> have a linear number of iterations: the number of iterations of the loop in $\textsc{explore}$, resp., $\textsc{exploreSwaps}$, is bounded by the number of write, resp., read, events in the current history (which is smaller than the size of the program; recall that we assume bounded programs with no loops as usual in SMC algorithms). On the other hand, the proofs of $I$-completeness and optimality are quite complex. For $I$-completeness, given a history $\hist\in \histOf[I]{\prog}$, we first show how to effectively compute the order $<$ associated to $\hist$ if $\textsc{explore}$ were to output this history. Then, we define an “inverse” of $\textsc{explore-sc}$ and an invariant on ordered histories reached by $\textsc{explore-sc}$, which enable constructing a chain of ordered histories going backwards from $(\hist,<)$ to the initial empty history. Then, we show that $\textsc{explore-sc}$ can proceed forwardly  in this chain and indeed output $\hist$.

$I$-completeness means that for any given program $\prog$, the algorithm outputs every history $h$ in $\histOf[I]{\prog}$. The proof of $I$-completeness defines a sequence of histories produced by the algorithm starting with an empty history and ending in $h$, for every such history $h$.

It consists of several steps:

* Define a canonical total order $<$ for every unordered partial history $h$, such that if the algorithm reaches $h_{<'}$, for some order $<'$, then $<$ and $<'$ coincide. This canonical order is useful in future proof steps as it allows to extend several definitions to arbitrary histories that are not necessarily reachable, such as $\genericProtocol$ or $\textsc{swapped}$.

* Define the notion of $\ora$-respectfulness, an invariant satisfied by every (partial) ordered history reached by the algorithm. Briefly, a history is $\ora$-respectful if it has only one pending transaction and for every two events $e, e'$ such that $e <_{\ora} e'$, either $e < e'$ or there is a swapped event $e''$ in between.

* Define a deterministic function $\prev$ which takes as input a partial history (not necessarily reachable), such that if $h$ is reachable, then $\prev(h)$ returns the history computed by the algorithm just before $h$ (i.e., the previous history in the call stack). Prove that if a history $h$ is $\ora$-respectful, then $\prev(h)$ is also $\ora$-respectful.

* Deduce that if $h$ is $\ora$-respectful, then there is a finite collection of $\ora$-respectful histories $H_h = \{h_i\}_{i=0}^{n}$ such that $h_n = h$, $h_0 = \emptyset$, and $h_i = \prev(h_{i+1})$ for each $i$. The $\ora$-respectfulness invariant and the causal-extensibility of the isolation level are key to being able to construct such a collection. In particular, they are used to prove that $h_i$ has at most the same number of swapped events as $h_{i+1}$ and in case of equality, $h_i$ contain exactly one event less than $h_{i+1}$, which implies that the collection is indeed finite.

* Prove that if $h$ is $\ora$-respectful and $\prev(h)$ is reachable, then $h$ is also reachable. Conclude by induction that every history in $H_h$ is reachable, as $h_0$ is the initial state and $h_i = \prev(h_{i+1})$.

The proof of strong optimality relies on arguments employed for $I$-completeness. It can be shown that if the algorithm would reach a (partial) history $h$ twice, then for one of the two exploration branches, the history $h'$ computed just before $h$ would be different from $\prev(h)$, which contradicts the definition of $\prev(h)$.

In terms of time complexity, the $\textsc{explore-ce}(I)$ algorithm achieves polynomial time between consecutive outputs for isolation
levels $I$ where checking $I$-consistency of a history is polynomial time, e.g., , , and .

§ SWAPPING-BASED MODEL CHECKING FOR SNAPSHOT ISOLATION AND SERIALIZABILITY

For $\textsc{explore-ce}$, the part of strong optimality concerning not engaging in fruitless explorations was a direct consequence of causal extensibility (of the isolation level). However, isolation levels such as SI and SER are not causally extensible (see Section <ref>). Therefore, the question we investigate in this section is whether there exists another implementation of $\textsc{explore}$ that can ensure strong optimality along with $I$-soundness and $I$-completeness for $I$ being SI or SER. We answer this question in the negative, and as a result, propose an SMC algorithm that extends $\textsc{explore-ce}$ by just filtering histories before outputting to be consistent with SI or SER.

If $I$ is Snapshot Isolation or Serializability, there exists no $\textsc{explore}$ algorithm that is $I$-sound, $I$-complete, and strongly optimal.

The proof of Theorem <ref> given in App. <ref> defines a program with two transactions and shows that

any concrete instance of $\textsc{explore}$ in Alg. <ref> cannot be both $I$-complete and strongly optimal.

Given this negative result, we define an implementation of $\textsc{explore}$ for an isolation level $I\in\{SI,SER\}$ that ensures optimality instead of strong optimality, along with soundness, completeness, and polynomial space bound. Thus, let $\textsc{explore-ce}(I_0)$ be an instance of $\textsc{explore-ce}$ parametrized by $I_0\in \{\RC,\RA,\CC\}$. We define an implementation of $\textsc{explore}$ for $I$, denoted by $\textsc{explore-ce}^*(I_0,I)$, which is exactly $\textsc{explore-ce}(I_0)$ except that

instead of $\genericEvaluate(\hist) ::= true$, it uses

\begin{equation*}
\begin{array}{ccc}
\genericEvaluate(\hist) & \coloneqq & \hist \mbox{ satisfies }I
\end{array}
\vspace{-1mm}
\end{equation*}

$\textsc{explore-ce}^*(I_0,I)$ enumerates exactly the same histories as $\textsc{explore-ce}(I_0)$ except that it outputs only histories consistent with $I$. The following is a direct consequence of Theorem <ref>.

For any isolation levels $I_0$ and $I$ such that $I_0$ is prefix-closed and causally extensible, and $I_0$ is weaker than $I$, $\textsc{explore-ce}^*(I_0,I)$ is $I$-sound, $I$-complete, optimal, and polynomial space.

We implemented algorithm $\textsc{explore-ce}$ and $\textsc{explore-ce}^*$ on top of Java PathFinder (JPF) cite JPF, a verification tool for Java concurrent programs. We admit as input a Java program that (1) can be parsed and executed by JPF and (2) employs the API according to the specifications. Our tool is parametric in the isolation levels employed.

The API provided allow $\ibegin, \iwrite, \iread$ and $\icommit$ operations. Thanks to this API, we can maintain the database state separately from JPF's internal state and update the current history in each database call. We do not rely on any concrete database but store the information as a collection of String, one per write API call executed; along with the $\so$, $\wro$-dependencies between the events associated to them. Any time there is a need to connect data from the local state to the database one or viceversa we copy and store the concrete String value from one state to the other.

Our implementation is compatible with JPF's standards, as both algorithm are instances of DFSearch; a JPF for DFS exploring algorithms. Moreover, we built consistency checkers based on the algorithm's presented in Ranadeep and Enea's paper for different isolation levels to ensure database's soundness.

However, for performance issues, we developed an iterative version of the algorithm <ref> for reducing the actual memory consumption. We employ an annotated stack of database states that is modified in each $\textsc{explore-ce}$ call; and we consider the algorithm works with list instead of simply sets.
At every step where we execute a $\iread$, we annotate which $\iwrite$ event is reading from and  when the state pops from the stack, we change the $\wro$-dependency. Analogously, at every step we produce a swap, we annotate which tuple given by $\compute$ we used in the swap for selecting a different tuple when the state is popped out.

§ EXPERIMENTAL EVALUATION

We evaluate an implementation of $\textsc{explore-ce}$ and $\textsc{explore-ce}^*$ in the context of the Java Pathfinder (JPF) <cit.> model
checker for Java concurrent programs. As benchmark, we use bounded-size client programs of a number of database-backed applications drawn from the literature.
The experiments were performed on an Apple M1 with $8$ cores and $16$ GB of RAM.

§.§ Implementation

We implemented our algorithms as an extension of the  class in JPF. For performance reasons, we implemented an iterative version of these algorithms where roughly, inputs to recursive calls are maintained as a collection of histories instead of relying on the call stack. For checking consistency of a history with a given isolation level, we implemented the algorithms proposed by <cit.>.

Our tool takes as input a Java program and isolation levels as parameters. We assume that the program uses a fixed API for interacting with the database, similar to a key-value store interface. This API consists of specific methods for starting/ending a transaction, and reading/writing a global variable. The fixed API is required for being able to maintain the database state separately from the JVM state (the state of the Java program) and update the current history in each database access. This relies on a mechanism for “transferring” values read from the database state to the JVM state.

§.§ Benchmark

We consider a set of benchmarks inspired by real-world applications and evaluate them under different types of client programs and isolation levels.

Shopping Cart <cit.> allows users to add, get and remove items from their shopping cart and modify the quantities of the items present in the cart.

Twitter <cit.> allows users to follow other users, publish tweets and get their followers, tweets and tweets published by other followers.

Courseware <cit.> manages the enrollment of students in courses in an institution. It allows to open, close and delete courses, enroll students and get all enrollments. One student can only enroll to a course if it is open and its capacity has not reached a fixed limit.

Wikipedia <cit.> allows users to get the content of a page (registered or not), add or remove pages to their watching list and update pages.

TPC-C <cit.> models an online shopping application with five types of transactions: reading the stock of a product, creating a new order, getting its status, paying it and delivering it.

SQL tables are modeled using a “set” global variable whose content is the set of ids (primary keys) of the rows present in the table, and a set of global variables, one variable for each row in the table (the name of the variable is the primary key of that row). SQL statements such as INSERT and DELETE statements are modeled as writes on that “set” variable while SQL statements with a WHERE clause (SELECT, JOIN, UPDATE) are compiled to a read of the table's set variable followed by reads or writes of variables that represent rows in the table (similarly to <cit.>).

§.§ Experimental Results

We designed three experiments where we compare the performance of a baseline model checking algorithm, $\textsc{explore-ce}$ and $\textsc{explore-ce}^*$ for different (combinations of) isolation levels, and we explore the scalability of $\textsc{explore-ce}$ when increasing the number of sessions and transactions per session, respectively.
All data is exhibited in Appendix <ref> in the supplementary material <cit.>. For each experiment we report running time, memory consumption, and the number of end states, i.e., histories of complete executions and in the case of $\textsc{explore-ce}^*$, before applying the $\genericEvaluate$ filter. As the number of end states for a program on a certain isolation level increases, the running time of our algorithms naturally increases as well.

The first experiment  compares the performance of our algorithms for different combinations of isolation levels and a baseline model checking algorithm that performs no partial order reduction. We consider as benchmark five (independent) client programs[For an application that defines a number of transactions, a client program consists of a number of sessions, each session containing a sequence of transactions defined by the application.] for each application described above ($25$ in total), each program with 3 sessions and 3 transactions per session. Running time, memory consumption, and number of end states are reported in Fig. <ref> as cactus plots <cit.>.

Running time.

Memory consumption.

End states.

[where every history is consistent]Cactus plots comparing different algorithms in terms of time, memory, and end states. For readability, we use $\CC$ to denote $\textsc{explore-ce}$ under $\CC$, $I_1 + I_2$ stands for $\textsc{explore-ce}^*(I_1, I_2)$, and $\texttt{true}$ is the trivial isolation level where every history is consistent. Differences between $\CC$, $\CC + \SI$ and $\CC + \SER$ are very small and their graphics overlap. Moreover, $\textsc{DFS}(\CC)$ denotes a standard DFS traversal of the semantics defined in Section <ref>. These plots exclude benchmarks that timeout ($30$ mins): $3$ benchmarks for $\CC$, $\langle \SI, \CC \rangle$ and $\langle \SER, \CC \rangle$ and $6$, $17$, $20$ and $20$ benchmarks timeout for $\langle \RA, \CC \rangle$, $\langle \RC, \CC \rangle$, $\langle \texttt{true}, \CC \rangle$ and $\textsc{DFS}(\CC)$ respectively.

To justify the benefits of partial order reduction, we implement a baseline model checking algorithm $\textsc{DFS}(\CC)$ that performs a standard DFS traversal of the execution tree w.r.t. the formal semantics defined in Section <ref> for $\CC$ (for fairness, we restrict interleavings so at most one transaction is pending at a time). This baseline algorithm may explore the same history multiple times since it includes no partial order reduction mechanism. In terms of time, $\textsc{DFS}(\CC)$ behaves poorly: it timeouts for $20$ out of the $25$ programs and it is less efficient even when it terminates. We consider a timeout of $30$ mins. In comparison the strongly optimal algorithm $\textsc{explore-ce}(\CC)$ (under $\CC$) finishes in $17$ seconds in average.in $3' 26''$ seconds in average (counting timeouts). $\textsc{DFS}(\CC)$ is similiar to $\textsc{explore-ce}(\CC)$also worse in terms of memory consumption. The memory consumption of $\textsc{DFS}(\CC)$ is $441$MB$381$MB in average, compared to $317$MB$508$MB for $\textsc{explore-ce}(\CC)$ (JPF forces a minimum consumption of $256$MB).

To show the benefits of strong optimality, we compare $\textsc{explore-ce}(\CC)$ which is strongly optimal with “plain” optimal algorithms $\textsc{explore-ce}^*(I_0,\CC)$ for different levels $I_0$. As shown in Figure <ref>(a), $\textsc{explore-ce}(\CC)$ is more efficient time-wise than every “plain” optimal algorithm, and the difference in performance grows as $I_0$ becomes weaker. In the limit, when $I_0$ is the trivial isolation level $\texttt{true}$ where every history is consistent, $\textsc{explore-ce}^*(\texttt{true},\CC)$ timeouts for $20$$12$ out of the $25$ programs. The average speedup (average of individual speedups) of $\textsc{explore-ce}(\CC)$ w.r.t. $\textsc{explore-ce}^*(\RA,\CC)$, $\textsc{explore-ce}^*(\RC,\CC)$ and $\textsc{explore-ce}^*(\texttt{true},\CC)$ is $2$, $31$, and $54$$3$, $18$ and $15$. respectively (we exclude timeout cases when computing speedups). All algorithms consume around 300 MB$500$MB of memory in average.

For the $\SI$ and $\SER$ isolation levels that admit no strongly optimal $\textsc{explore}$ algorithm, we observe that the overhead of $\textsc{explore-ce}^*(\CC,\SI)$ or $\textsc{explore-ce}^*(\CC,\SER)$ relative to $\textsc{explore-ce}(\CC)$ is negligible (the corresponding lines in Figure <ref> are essentially overlapping). This is due to the fact that the consistency checking algorithms of <cit.> are polynomial time when the number of sessions is fixed, which makes them fast at least on histories with few sessions.

In our second experiment, we investigate the scalability of $\textsc{explore-ce}$ when increasing the number of sessions. For each $i\in [1,5]$, we consider 5 (independent) client programs for TPC-C and 5 for Wikipedia[We focus on these two applications because they are of similar complexity.]
(10 in total) with $i$ sessions, each session containing 3 transactions. We start with 10 programs with 5 sessions, and remove sessions one by one to obtain programs with fewer sessions. We take $\CC$ as isolation level.

The plot in Figure <ref> shows average running time and memory consumption for each number $i\in [1,5]$ of sessions.
As expected, increasing the number of sessions is a bottleneck running time wise because the number of histories increases significantly. However, memory consumption does not grow with the same trend, cf. the polynomial space bound.

Increasing sessions.

Increasing transactions per session.

Evaluating the scalability of $\textsc{explore-ce}(\CC)$ for TPC-C and Wikipedia client programs when increasing their size. These plots include benchmarks that timeout ($30$ mins): $4$, $9$ and $10$ for $3$, $4$ and $5$ sessions respectively in Figure <ref>, and $5$, $8$ and $10$ for $3$, $4$ and $5$ transactions per sessions respectively in Figure <ref>.

Finally, we evaluate the scalability of $\textsc{explore-ce}(\CC)$ when increasing the number of transactions per session. We consider 5 (independent) TPC-C client programs and 5 (independent) Wikipedia programs with $3$ sessions and $i$ transactions per session, for each $i\in [1,5]$.

Figure <ref> shows average running time and memory consumption for each number $i\in [1,5]$ of transactions per session. Increasing the number of transactions per session is a bottleneck for the same reasons.

§ RELATED WORK

Checking Correctness of Database-Backed Applications.

One line of work is concerned with the logical formalization
of isolation levels
Our work relies on the axiomatic definitions of isolation levels introduced by <cit.>, which have also investigated
the problem of checking whether a given history satisfies a certain isolation
level. Our SMC algorithms rely on these algorithms to check consistency of a history with a given isolation level.

Another line of work focuses on the problem of finding “anomalies”:
behaviors that are not possible under serializability. This is typically done
via a static analysis of the application code that builds a static dependency graph that
over-approximates the data dependencies in all possible
executions of the application <cit.>.
Anomalies with respect to a given isolation level then correspond to a
particular class of cycles in this graph. Static dependency graphs turn out to
be highly imprecise in representing feasible executions, leading to false
positives. Another source of false positives is that an anomaly might not be a
bug because the application may already be designed to handle the
non-serializable behavior <cit.>.
Recent work has tried to address these issues by using more precise
logical encodings of the application <cit.>, or
by using user-guided heuristics <cit.>.
Another approach consists of modeling the application
logic and the isolation level in first-order logic and relying on SMT solvers to
search for anomalies <cit.>,
or defining specialized reductions to assertion
checking <cit.>.
Our approach, based on SMC, does not generate false positives because we systematically
enumerate only valid executions of a program which allows to check for user-defined assertions.

Several works have looked at the problem of reasoning about the correctness of
applications executing under weak isolation and introducing additional
synchronization when
necessary <cit.>.
These are based on static analysis or logical proof arguments.
The issue of repairing applications is orthogonal to our work.

MonkeyDB <cit.> is a mock storage system for testing storage-backed applications.
While being able to scale to larger code, it has the inherent incompleteness of testing. As opposed to MonkeyDB, our algorithms perform a systematic and complete exploration of executions and can establish correctness at least in some bounded context, and they avoid redundancy, enumerating equivalent executions multiple times. Such guarantees are beyond the scope of MonkeyDB.

Dynamic Partial Order Reduction.

<cit.> introduced the concept of source sets which provided the first strongly optimal DPOR algorithm for Mazurkiewicz trace equivalence. Other works study DPOR techniques for coarser equivalence relations, e.g., <cit.>. In all cases, the space complexity is exponential when strong optimality is ensured.

Other works focus on extending DPOR to weak memory models either by targeting a specific memory model <cit.> or by being parametric with respect to an axiomatically-defined memory model <cit.>. Some of these works can deal with the coarser reads-from equivalence, e.g., <cit.>. Our algorithms build on the work of <cit.> which for the first time, proposes a DPOR algorithm which is both strongly optimal and polynomial space. The definitions of database isolation levels are quite different with respect to weak memory models, which makes these previous works not extensible in a direct manner. These definitions include a semantics for transactions which are collections of reads and writes, and this poses new difficult challenges.
For instance, reasoning about the completeness and the (strong) optimality of existing DPOR algorithms for shared-memory is agnostic to the scheduler ($\genericNext$ function) while the strong optimality of our $\textsc{explore-ce}$ algorithm relies on the scheduler keeping at most one transaction pending at a time. In addition, unlike TruSt, explore-ce ensures that no swapped events can be swapped again and that the history order $<$ is an extension of $\so \cup \wro$. This makes our completeness and optimality proofs radically different.
Moreover, even for transactional programs with one access per transaction, where $\SER$ and $\SC$ are equivalent, TruSt under $\SC$ and $\textsc{explore-ce}^*(I_0,\SER)$ do not coincide, for any $I_0 \in \{\RC, \RA, \CC\}$. In this case, TruSt enumerates only $\SC$-consistent histories at the cost of solving an NP-complete problem at each step while the $\textsc{explore-ce}^*$ step cost is polynomial time at the price of not being strongly-optimal.
Furthermore, we identify isolation levels ($\SI$ and $\SER$) for which it is impossible to ensure both strong optimality and polynomial space bounds with a swapping-based algorithm, a type of question that has not been investigated in previous work.

§ CONCLUSIONS

We presented efficient SMC algorithms based on DPOR for transactional programs running under standard isolation levels. These algorithms are instances of a generic schema, called swapping-based algorithms, which is parametrized by an isolation level. Our algorithms are sound and complete, and  polynomial space. Additionally, we identified a class of isolation levels, including $\RC$, $\RA$, and $\CC$, for which our algorithms are strongly optimal, and we showed that swapping-based algorithms cannot be strongly optimal for stronger levels $\SI$ and $\SER$ (but just optimal). For the isolation levels we considered, there is an intriguing coincidence between the existence of a strongly optimal swapping-based algorithm and the complexity of checking if a given history is consistent with that level. Indeed, checking consistency is polynomial time for $\RC$, $\RA$, and $\CC$, and NP-complete for $\SI$ and $\SER$.

Investigating further the relationship between strong optimality and polynomial-time consistency checks is an interesting direction for future work.

§ ACKNOWLEDGEMENTS

We thank anonymous reviewers for their feedback, and Ayal Zaks for shepherding our paper. This work was partially supported by the project AdeCoDS of the French National Research Agency.

§ DATA AVAILABILITY STATEMENT

The implementation is open-source and can be found in <cit.>.

§ RELATED WORK

Checking Correctness of Database-Backed Applications.

One line of work is concerned with the logical formalization
of isolation levels
Our work relies on the axiomatic definitions of isolation levels introduced by <cit.>, which have also investigated
the problem of checking whether a given history satisfies a certain isolation
level. Our SMC algorithms rely on these algorithms to check consistency of a history with a given isolation level.

Another line of work focuses on the problem of finding “anomalies”:
behaviors that are not possible under serializability. This is typically done
via a static analysis of the application code that builds a static dependency graph that
over-approximates the data dependencies in all possible
executions of the application <cit.>.
Anomalies with respect to a given isolation level then correspond to a
particular class of cycles in this graph. Static dependency graphs turn out to
be highly imprecise in representing feasible executions, leading to false
positives. Another source of false positives is that an anomaly might not be a
bug because the application may already be designed to handle the
non-serializable behavior <cit.>.
Recent work has tried to address these issues by using more precise
logical encodings of the application <cit.>, or
by using user-guided heuristics <cit.>.
Another approach consists of modeling the application
logic and the isolation level in first-order logic and relying on SMT solvers to
search for anomalies <cit.>,
or defining specialized reductions to assertion
checking <cit.>.
Our approach, based on SMC, does not generate false positives because we systematically
enumerate only valid executions of a program which allows to check for user-defined assertions.

Several works have looked at the problem of reasoning about the correctness of
applications executing under weak isolation and introducing additional
synchronization when
necessary <cit.>.
These are based on static analysis or logical proof arguments.
The issue of repairing applications is orthogonal to our work.

MonkeyDB <cit.> is a mock storage system for testing storage-backed applications.
While being able to scale to larger code, it has the inherent incompleteness of testing. As opposed to MonkeyDB, our algorithms perform a systematic and complete exploration of executions and can establish correctness at least in some bounded context, and they avoid redundancy, enumerating equivalent executions multiple times. Such guarantees are beyond the scope of MonkeyDB.

Dynamic Partial Order Reduction.

<cit.> introduced the concept of source sets which provided the first strongly optimal DPOR algorithm for Mazurkiewicz trace equivalence. Other works study DPOR techniques for coarser equivalence relations, e.g., <cit.>. In all cases, the space complexity is exponential when strong optimality is ensured.

Other works focus on extending DPOR to weak memory models either by targeting a specific memory model <cit.> or by being parametric with respect to an axiomatically-defined memory model <cit.>. Some of these works can deal with the coarser reads-from equivalence, e.g., <cit.>. Our algorithms build on the work of <cit.> which for the first time, proposes a DPOR algorithm which is both strongly optimal and polynomial space. The definitions of database isolation levels are quite different with respect to weak memory models, which makes these previous works not extensible in a direct manner. These definitions include a semantics for transactions which are collections of reads and writes, and this poses new difficult challenges.
For instance, reasoning about the completeness and the (strong) optimality of existing DPOR algorithms for shared-memory is agnostic to the scheduler ($\genericNext$ function) while the strong optimality of our $\textsc{explore-ce}$ algorithm relies on the scheduler keeping at most one transaction pending at a time. In addition, unlike TruSt, explore-ce ensures that no swapped events can be swapped again and that the history order $<$ is an extension of $\so \cup \wro$. This makes our completeness and optimality proofs radically different.
Moreover, even for transactional programs with one access per transaction, where $\SER$ and $\SC$ are equivalent, TruSt under $\SC$ and $\textsc{explore-ce}^*(I_0,\SER)$ do not coincide, for any $I_0 \in \{\RC, \RA, \CC\}$. In this case, TruSt enumerates only $\SC$-consistent histories at the cost of solving an NP-complete problem at each step while the $\textsc{explore-ce}^*$ step cost is polynomial time at the price of not being strongly-optimal.
Furthermore, we identify isolation levels ($\SI$ and $\SER$) for which it is impossible to ensure both strong optimality and polynomial space bounds with a swapping-based algorithm, a type of question that has not been investigated in previous work.

§ AXIOMATIC LEVELS: READ COMMITTED AND READ ATOMIC.

[->,>=stealth,shorten >=1pt,auto,node distance=1cm,
semithick, transform shape]
[transaction state, text=black] at (0,0)       	(t_1)           $t_1$;
[transaction state, text=black, label=above:$\writeVar{ }{x}$] at (-0.5,1.5) (t_2) $t_2$;
[transaction state, text=black] at (2,0)       (o_1)           $\alpha$;
[transaction state] at (1.5,1.5) (o_2) $\beta$;
(t_1) edge[color=wrColor] node $\wro_x$ (o_1);

(t_2) edge[color=wrColor] node $\wro$ (o_2);
(o_2) edge[color=poColor] node $\po$ (o_1);
(t_2) edge[left,double,color=coColor] node $\co$ (t_1);

$\forall x,\ \forall t_1, t_2,\ \forall \alpha.\ t_1\neq t_2\ \land$

$\tup{t_1,\alpha}\in \wro_x \land \writeVar{t_2}{x}\ \land$

$\implies \tup{t_2,t_1}\in\co$

$\mathsf{Read\ Committed}$

[->,>=stealth,shorten >=1pt,auto,node distance=1cm,
semithick, transform shape]
[transaction state, text=black] at (0,0)       (t_1)           $t_1$;
[transaction state] at (2,0)       (t_3)           $t_3$;
[transaction state, text=black,label=above:$\writeVar{ }{\xvar}$] at (-.5,1.5) (t_2) $t_2$;
(t_1) edge[wrColor] node $\wro_x$ (t_3);

(t_2) edge[bend left] node $\so \cup \wro$ (t_3);
(t_2) edge[left, double ,coColor] node $\co$ (t_1);

$\forall x,\ \forall t_1, t_2,\ \forall t_3.\ t_1\neq t_2\ \land$

$\tup{t_1,t_3}\in \wro_x \land \writeVar{t_2}{x}\ \land$

$\tup{t_2,t_3}\in\so \cup \wro$

$\implies \tup{t_2,t_1}\in\co$

$\mathsf{Read\ Atomic}$

Axioms defining isolations levels. The reflexive and transitive, resp., transitive, closure of a relation $rel$ is denoted by $rel^*$, resp., $rel^+$. Also, $\circ$ denotes the composition of two relations, i.e., $rel_1 \circ rel_2 = \{\tup{a, b} | \exists c. \tup{a, c} \in rel_1 \land \tup{c, b} \in rel_2\}$.

The axioms defined above in Figure <ref> define the homonymous isolation levels Read Atomic (also called Repeatable Read in the literature) and Read Committed.

§ RULES OF THE OPERATIONAL SEMANTICS (SECTION <REF>).

[spawn]  e   𝖯(j) = ; 𝖡𝗈𝖽𝗒; ; 𝖲   𝖡⃗(j) = ϵ
⊕_j ,{e,},∅,γ⃗[j↦∅],𝖡⃗[j↦𝖡𝗈𝖽𝗒; ],𝖯[j↦𝖲]

[if-true]ψ(x⃗)[x↦γ⃗(j)(x): x∈x⃗]

𝖡⃗(j) = ψ(x⃗)𝖨𝗇𝗌𝗍𝗋;𝖡

,γ⃗,𝖡⃗, 𝖯

[if-false]ψ(x⃗)[x↦γ⃗(j)(x): x∈x⃗]

𝖡⃗(j) = ψ(x⃗)𝖨𝗇𝗌𝗍𝗋;𝖡

,γ⃗,𝖡⃗, 𝖯

[local]v = γ⃗(j)(e)
𝖡⃗(j) = a := e;𝖡

,γ⃗,𝖡⃗, 𝖯

[write]v = γ⃗(j)(x)  e   𝖡⃗(j) = (,);𝖡  ⊕_j e,,

,γ⃗,𝖡⃗, 𝖯
⊕_j e,,,γ⃗,𝖡⃗[j↦𝖡], 𝖯

𝖡⃗(j) = := ();𝖡

,γ⃗,𝖡⃗, 𝖯
⊕_j e,,γ⃗[(j,)↦],𝖡⃗[j↦𝖡],𝖯

𝖡⃗(j) = := ();𝖡

' = (⊕_j e,) ⊕(',e)

' I
,γ⃗,𝖡⃗, 𝖯

[commit]e   𝖡⃗(j) =
,γ⃗,𝖡⃗, 𝖯
⊕_j e,,γ⃗,𝖡⃗[j↦ϵ], 𝖯

[abort]e   𝖡⃗(j) = ; B

,γ⃗,𝖡⃗, 𝖯
⊕_j e,,γ⃗,𝖡⃗[j↦ϵ], 𝖯

An operational semantics for transactional programs. Above, $\mathit{last}(h,j)$ denotes the last transaction log in the session order $\so(j)$ of $h$, and $\transC{\hist}$ denotes the set of transaction logs in $\hist$ that are committed.

Figure <ref> uses the following notation. Let $\hist$ be a history that contains a representation of $\so$ as above. We use $\hist\oplus_j \tup{\tr,E,\po_t}$ to denote a history where $\tup{\tr,E,\po_t}$ is appended to $\so(j)$.
Also, for an event $e$, $\hist\oplus_j e$ is the history obtained from $\hist$ by adding $e$ to the last transaction log in $\so(j)$ and as a last event in the program order of this log (i.e.,  if $\so(j)=\sigma; \tup{t,E,\po_t}$, then the session order $\so'$ of $\hist\oplus_j e$ is defined by $\so'(k)=\so(k)$ for all $k\neq j$ and $\so(j) =\sigma; \tup{t,E\cup\{e\},\po_t\cup \{(e',e): e'\in E\}}$). Finally, for a history $\hist = \tup{T, \so, \wro}$, $\hist\oplus\wro(\tr,e)$ is the history obtained from $\hist$ by adding $(\tr,e)$ to the write-read relation.

spawn starts a new transaction in a session $j$ provided that this session has no live transaction ($\vec{\mathsf{B}}(j) = \epsilon$). It adds a transaction log with a single $\ebegin$ event to the history and schedules the body of the transaction. if-true and if-false check the truth value of a Boolean condition of an $\mathtt{if}$ conditional. local models the execution of an assignment to a local variable which does not impact the stored history. read-local and read-extern concern read instructions. read-local handles the case where the read follows a write on the variable $x$ in the same transaction: the read returns the value written by the last write on $x$ in that transaction. Otherwise, read-extern corresponds to reading a value written in another transaction $\tr'$. The transaction $\tr'$ is chosen non-deterministically as long as extending the current history with the write-read dependency associated to this choice leads to a history that still satisfies $I$. read-extern applies only when the executing transaction contains no write on the same variable. commit confirms the end of a transaction making its writes visible while abort ends the transaction's execution immediately.

§ PROOF OF THEOREM <REF>

Let $I$ be an isolation level in $\{\CC, \RA, \RC\}$. We show that any commit order $\co$ justifying that a history $h$ is $I$-consistent can also be used to justify that a causal extension $\hist'$ of a $(\so \cup \wro)^*$-maximal pending transaction $t$ in $h$ with an event $e$ is $I$-consistent as well.
We consider a causal extension $\hist'$ where if $e$ is a read event, then it reads from the last transaction $t_w$ in $\co$ such that $t_w$ writes $\mathit{var}(e)$ and $(t_w, t) \in (\so \cup \wro)^+$.

Assume by contradiction that this is not the case. Let $\phi_{\CC}(h', t', e') = t' \ (\so \cup \wro)^+ \ \trans{h'}{e'}$, $\phi_{\RA}(h',t', e') = t' \ (\so \cup \wro) \ \trans{h'}{e'}$ and $\phi_{\RC}(h',t', e') = t' \ (\wro \circ \po) \ e'$ be sub-formulas of the axioms defining the corresponding isolation level. Then,

$\hist'$ contains transactions $t_1, t_2, t_3$  such that $t_2$ writes some variable $x$, $t_3$ contains some read event $e'$, $(t_1, e') \in \wro_x$ and $\phi_{I}(h', t_2, e')$ but $(t_1, t_2) \in \co$. The assumption concerning $\co$ implies that the extended transaction $t$ is one of $t_1, t_2, t_3$ (otherwise, $\co$ would not be a “valid” commit order for $\hist$). Since $t$ is $(\so \cup \wro)^+$-maximal in $\hist$, we have that $t\not\in \{t_1,t_2\}$. If

$e$ is not a read event, or if $e$ is a read event different from $e'$, then $t \neq t_3$, as $t_1$, $t_2$ and $t_3$ would satisfy the same constraints in $h$, which is impossible by the hypothesis. Otherwise, if $e=e'$, then this contradicts the choice we made for the transaction $t_w$ that $e$ reads from. Since $(t_1, t_2) \in \co$ and $t_2$ writes $\mathit{var}(e)$, it means that $t_w=t_1$ is not maximal w.r.t. $\co$ among transactions that write $\mathit{var}(e)$ and precede $t$ in $(\so \cup \wro)^+$. Both cases lead to a contradiction, which implies that $\hist'$ is $I$-consistent, and therefore the theorem holds.

§ PROOF OF THEOREM <REF>

max width=

[xleftmargin=5mm,basicstyle=,escapeinside=(**), tabsize=1]
a = read((*$x$*));

[xleftmargin=5mm,basicstyle=,escapeinside=(**), tabsize=1]
b = read((*$y$*));

Program (2 sessions).

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t1) at (-1.5, -0.25)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0] (t2) at (-3, -2)
[draw, rounded corners=2mm,outer sep=0] (t3) at (0, -2)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1sw);
(t1.south east) – (t1.south) coordinate[pos=0.67] (t1se);
(t2.north east) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.north) coordinate[pos=0.67] (t3x);

(t1sw) edge [left] node $\wro_x$ (t2x);
(t1se) edge [right] node $\wro_y$ (t3x);

History $\hist$.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t1) at (-1.5, -0.25)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0] (t2) at (-3, -2)
[draw, rounded corners=2mm,outer sep=0] (t3) at (0, -2)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1sw);
(t1.south east) – (t1.south) coordinate[pos=0.67] (t1se);
(t2.north east) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.north) coordinate[pos=0.67] (t3x);

(t1sw) edge [left] node $\wro_x$ (t2x);

[shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]

(-1.5,0) edge[dashed] (2,0);

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t1) at (-1.5, -0.25)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0] (t2) at (-3, -2)

[draw, rounded corners=2mm,outer sep=0] (t3) at (0, -2)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1sw);
(t1.south east) – (t1.south) coordinate[pos=0.67] (t1se);
(t2.north east) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.north) coordinate[pos=0.67] (t3x);

(t1se) edge [right] node $\wro_y$ (t3x);

Two histories. The top history is called $\hist_1$.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t1) at (-1.5, -0.25)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0] (t2) at (-3, -2)
[draw, rounded corners=2mm,outer sep=0] (t3) at (0, -2)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1sw);
(t1.south east) – (t1.south) coordinate[pos=0.67] (t1se);
(t2.north east) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.north) coordinate[pos=0.67] (t3x);

(t1sw) edge [left] node $\wro_x$ (t2x);

History $\hist_{2}$.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t1) at (-1.5, -0.25)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0] (t2) at (-3, -2)
[draw, rounded corners=2mm,outer sep=0] (t3) at (0, -2)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1sw);
(t1.south east) – (t1.south) coordinate[pos=0.67] (t1se);
(t2.north east) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.north) coordinate[pos=0.67] (t3x);

(t1sw) edge [left] node $\wro_x$ (t2x);

History $\hist_{3}$.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t1) at (-1.5, -0.25)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0] (t2) at (-3, -2)
[draw, rounded corners=2mm,outer sep=0] (t3) at (0, -2)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1sw);
(t1.south east) – (t1.south) coordinate[pos=0.67] (t1se);
(t2.north east) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.north) coordinate[pos=0.67] (t3x);

(t1sw) edge [left] node $\wro_x$ (t2x);
(t1se) edge [right] node $\wro_y$ (t3x);

History $\hist_{11}$.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t1) at (-1.5, -0.25)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0] (t2) at (-3, -2)
[draw, rounded corners=2mm,outer sep=0] (t3) at (0, -2)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1sw);
(t1.south east) – (t1.south) coordinate[pos=0.67] (t1se);
(t2.north east) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.north) coordinate[pos=0.67] (t3x);

(t1sw) edge [left] node $\wro_x$ (t2x);
(t1se) edge [right] node $\wro_y$ (t3x);

History $\hist_{21}$.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t1) at (-1.5, -0.25)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0] (t2) at (-3, -2)
[draw, rounded corners=2mm,outer sep=0] (t3) at (0, -2)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1sw);
(t1.south east) – (t1.south) coordinate[pos=0.67] (t1se);
(t2.north east) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.north) coordinate[pos=0.67] (t3x);

(t1sw) edge [left] node $\wro_x$ (t2x);
(t1se) edge [right] node $\wro_y$ (t3x);

History $\hist_{31}$.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t1) at (0, 0)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0] (t2) at (0, -1.8)
[draw, rounded corners=2mm,outer sep=0] (t3) at (0, -4.5)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1sw);
(t1.south east) – (t1.south) coordinate[pos=0.67] (t1se);
(t2.north east) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.north) coordinate[pos=0.67] (t3x);

(t1.south) edge [left] node $\wro_x$ (t2.north);
(t2.south) edge [left] node $\wro_y$ (t3.north);

History $\hist_{32}$.

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (t1) at (0, 0)  $\init$ ;
[draw, rounded corners=2mm,outer sep=0] (t3) at (0, -1.8)
[draw, rounded corners=2mm,outer sep=0] (t2) at (0, -4.5)

(t1.south west) – (t1.south) coordinate[pos=0.67] (t1sw);
(t1.south east) – (t1.south) coordinate[pos=0.67] (t1se);
(t2.north east) – (t2.north) coordinate[pos=0.67] (t2x);
(t3.north west) – (t3.north) coordinate[pos=0.67] (t3x);

(t1.south) edge [left] node $\wro_y$ (t3.north);
(t3.south) edge [left] node $\wro_x$ (t2.north);

History $\hat{\hist}$.

A program and some partial histories. Events in grey are not yet added to the history. For $\hist_3$, $\hist_{31}$ and $\hist_{32}$, the number of events that follow $\ewrt{y,1}$ and $\ewrt{x,2}$ is not important (we use black $\ldots$  to signify that).

[->,>=stealth',shorten >=1pt,auto,node distance=3cm,
semithick, transform shape]
[draw, rounded corners=2mm,outer sep=0] (h0) at (-3, -1.5) $\emptyset$;
[draw, rounded corners=2mm,outer sep=0] (h1) at (-1.5, -1.5)  $h_1$;
[draw, rounded corners=2mm,outer sep=0] (h2) at (0, -1.5) $h_2$;
[draw, rounded corners=2mm,outer sep=0] (h3) at (1.5, -1.5) $h_3$;
[draw, rounded corners=2mm,outer sep=0] (h11) at (-1.5, -3) $h_{11}$;
[draw, rounded corners=2mm,outer sep=0] (h21) at (0, -3)  $h_{21}$;
[draw, rounded corners=2mm,outer sep=0] (h31) at (1.5, -3) $h_{31}$;
[draw, rounded corners=2mm,outer sep=0] (h32) at (3, -3) $h_{32}$;
[draw, red, rounded corners=2mm,outer sep=0] (h) at (0, -4.5) $h$;
[draw, rounded corners=2mm,outer sep=0] (h') at (3, -4.5) $\hat{h}$;
[red] (x) at (3, -3.65) $\bigtimes$;

(h0.east) edge [below] node[right]  (h1.west);
(h1.east) edge [below] node[right]  (h2.west);
(h2.east) edge [below] node[right]  (h3.west);
(h1.south) edge [below] node[right]  (h11.north);
(h2.south) edge [below] node[right]  (h21.north);
(h3.south) edge [below] node[right]  (h31.north);
(h3.south) edge [below] node[right]  (h32.north);
(h11.south) edge [below, dashed] node[right]  (h.north);
(h21.south) edge [below, dashed] node[right]  (h.north);
(h31.south) edge [below, dashed] node[right]  (h.north);
(h32.south) edge [below, dashed] node[right]  (h'.north);

Summary of all possible execution paths from $\textsc{explore}$. Black arrows represent alternative explored options depending on $\genericNext$ while dashed arrows are mandatory visited histories from such state.

We consider the program in Figure <ref>, and show that any concrete instance of the $\textsc{explore}$ function in Algorithm <ref> can not be both $I$-complete and strongly optimal. This program contains two transactions, where only the first three instructions in each transaction are important.
We show that if $\textsc{explore}$ is $I$-complete, then it will necessarily be called recursively on a history $\hist$ like in Figure <ref> which does not satisfy $I$, thereby violating strong optimality. In the history $\hist$, both Snapshot Isolation and Serializability forbid the two reads reading initial values while the writes following them are also executed (committed). A diagram of the proof can be seen in Figure <ref>.

Assuming that the function $\genericNext$ is not itself blocking (which would violate strong optimality), the $\textsc{explore}$ will be called recursively on exactly one of the two histories in Figure <ref>, depending on which of the two reads is returned first by $\genericNext$.
We will continue our discussion with the history $\hist_1$ on the top of Figure <ref>. The other case is similar (symmetric).

From $\hist_1$, depending on order defined by $\genericNext$ between $\ewrt{z,1}$ and $\erd{y}$, $\textsc{explore}$ can be called recursively either on $\hist_{11}$ in Figure <ref> or on $\hist_{2}$ in Figure <ref>. Analogously, from $\hist_2$ two alternatives arise depending on the order defined by $\genericNext$ between $\erd{y}$ and the rest of events in the left transaction: exploring $\hist_{21}$ in Figure <ref> if $\erd{y}$ is added before $\ewrt{y,1}$ or $\hist_3$ in Figure <ref> otherwise. Thus, from $\hist_3$ two alternatives arise when added $\erd{y}$ depending on where it reads from: $\hist_{31}$ in Figure <ref> if it reads from $\init$ and $\hist_{32}$ in Figure <ref> if it reads from the left transaction.

However, from histories $\hist_{11}$, $\hist_{21}$ or $\hist_{31}$ $\textsc{explore}$ will necessarily be called recursively on a history $\hist$ like in Figure <ref> which does not satisfy $I$, thereby violating strong optimality: $\textsc{explore}$ always explore branches that enlarge the current history. Thus, any $\textsc{explore}$ implementation that is strong optimal should only explore $\hist_{32}$. In such case, by the restrictions on the $\genericSwap$ function (defined in Section <ref>), any extension of $\hist_{32}$ does not allow to explore the history $\hat{h}$ in Figure <ref> where $\erd{x}$ reads from $\ewrt{x,2}$: any outcome of a re-ordering between two contiguous subsequences $\alpha$ and $\beta$ must be prefix of such extension when the events in $\alpha$ are taken out. In particular, for any extension $\hist'$ of $\hist_{32}$ and pair of contiguous sequences $\alpha, \beta$ such that $\hist' \setminus \alpha$ is a prefix of $\hist'$, if an event from the second transaction belongs to $\beta$, $\erd{y}$ must also be in $\beta$. Therefore, $\ewrt{x, 2}$ must be in $\beta$ as it is $\wro^{-1}(\erd{y})$. Hence, $\erd{x}$ must also be in $\beta$. Analogously, if $\erd{x}$ belongs to $\beta$, $\init$ belongs to it. Altogether, if $\beta$ contains any element, then $\alpha$ must be empty; so no swaps can be produced from $h_{32}$. To conclude, in this case $\textsc{explore}$ violates $I$-completeness.

We consider the program in Figure <ref>, and show that any concrete instance of the $\textsc{explore}$ function in Algorithm <ref> can not be both $I$-complete and strongly optimal. This program contains two transactions, where only the first three instructions in each transaction are important.
We show that if $\textsc{explore}$ is $I$-complete, then it will necessarily be called recursively on a history $\hist$ like in Figure <ref> which does not satisfy $I$, thereby violating strong optimality. In the history $\hist$, both Snapshot Isolation and Serializability forbid the two reads reading initial values while the writes following them are also executed (committed).

Assuming that the function $\genericNext$ is not itself blocking (which would violate strong optimality), the $\textsc{explore}$ will be called recursively on exactly one of the four histories in Figure <ref> and Figure <ref>, depending on which of the two reads is returned first by $\genericNext$ and the order defined by $\genericNext$ between the writes.
We will continue our discussion with the history $\hist_1$ on the top of Figure <ref> and the history $\hist_2$ on the left of Figure <ref>. The other cases are similar (symmetric).

From $\hist_1$, $\textsc{explore}$ can be called recursively either on $\hist_{11}$ in Figure <ref>, or on $\hist_{12}$ and $\hist_{12}'$ in Figure <ref> and Figure <ref>, depending on the order defined by $\genericNext$ between $\erd{y}$ and $\ewrt{y,1}$ ($\erd{y}$ is returned by $\genericNext$ before $\ewrt{y,1}$ in $\hist_{11}$ and vice-versa in $\hist_{12}$ and $\hist_{12}'$).

The histories $\hist_{12}$ and $\hist_{12}'$ differ in the read-from associated to $\erd{y}$, and exploring at least $\hist_{12}'$ is the best scenario towards ensuring $I$-completeness.

If $\textsc{explore}$ is called recursively only on $\hist_{12}$, then $I$-completeness is violated because $\hist_{12}$ and any extension does not enable any re-ordering, and the history where $\erd{x}$ reads from $\ewrt{x,2}$ will never be explored. Thus, let $\hist_e$ be an extension of $h_{12}$. By the restrictions on the $\genericSwap$ function (defined in Section <ref>), any outcome of a re-ordering between two subsequences $\alpha$ and $\beta$ must be prefix of $\hist_e$ when the events in $\alpha$ are taken out. Since the bottom transaction $t_2$ in $h_e$  reads from the top transaction $t_1$, removing any event different from $t_2$'s last event (the read of $y$) from $\hist_e$ will make the history a non-prefix. Then, having $\alpha$ be this last event is not possible since there is no other event after it to create a $\beta$ (as mentioned in Section <ref>, the events in $\alpha$ should occur before those in $\beta$).

From histories $\hist_{11}$ or $\hist_{12}'$, $\textsc{explore}$ will necessarily be called recursively on a history $\hist$ like in Figure <ref>

which does not satisfy $I$, thereby violating strong optimality.

From $\hist_2$, $\textsc{explore}$ can be called recursively on $\hist_{21}$ in Figure <ref> and $\hist_{21}'$ in Figure <ref>. As explained above for $\hist_{12}=\hist_{21}$, being called recursively only on $\hist_{21}$ violates $I$-completeness, while being called recursively on $\hist_{21}' = \hist_{12}'$ leads to an inconsistent history, thereby violating strong optimality.

§ PROOF OF THEOREM <REF>

As explained in Section <ref>, $I$-soundness, the polynomial space bound, and the part of strong completeness that refers to not engaging in fruitless explorations follow directly from definitions. In the following, we focus on $I$-completeness and then optimality. For the sake of the proof's readability, we will omit all local states of the algorithm's definition during the proof. Therefore, we consider programs where we can describe all their events.

§ EXPERIMENTAL DATA

§.§ Application Scalability

4cCC                              4cCC + SI                              4cCC + SER
2-5 7-10 12-15
Histories     End states     Time       Mem.              Histories     End states     Time       Mem.              Histories     End states     Time       Mem.
courseware-1     216     216     00:00:22     370           81     216     00:00:25     370           72     216     00:00:23     370

courseware-2     46     46     00:00:06     316           34     46     00:00:06     308           34     46     00:00:06     314

courseware-3     12790     12790     00:12:45     533           6197     12790     00:13:59     533           960     12790     00:12:37     557

courseware-4     69     69     00:00:07     314           39     69     00:00:08     324           17     69     00:00:07     370

courseware-5     388     388     00:00:25     308           136     388     00:00:27     370           71     388     00:00:24     370

shoppingCart-1     444     444     00:00:19     308           108     444     00:00:22     308           81     444     00:00:19     308

shoppingCart-2     2934     2934     00:00:55     308           811     2934     00:01:13     444           480     2934     00:00:58     308

shoppingCart-3     1594     1594     00:00:55     308           1077     1594     00:01:05     308           338     1594     00:01:00     308

shoppingCart-4     58677     58677     TL      444           12440     49589     TL      444           779     60194     TL      383

shoppingCart-5     4686     4686     00:02:56     444           1986     4686     00:03:07     444           780     4686     00:02:41     308

tpcc-1     165     165     00:00:43     794           47     165     00:00:47     808           47     165     00:00:45     796

tpcc-2     353     353     00:01:25     699           35     353     00:01:29     879           31     353     00:01:25     704

tpcc-3     1593     1593     00:10:12     966           232     1593     00:10:29     1054           116     1593     00:10:05     803

tpcc-4     105     105     00:00:15     450           22     105     00:00:16     485           1     105     00:00:15     396

tpcc-5     7836     7836     TL      1732           695     6973     TL      1647           271     7617     TL      1640

twitter-1     36     36     00:00:05     256           29     36     00:00:06     308           18     36     00:00:05     256

twitter-2     876     876     00:00:48     459           263     876     00:01:03     1066           122     876     00:00:56     513

twitter-3     1072     1072     00:01:24     444           576     1072     00:01:33     569           216     1072     00:01:21     444

twitter-4     12915     12915     00:08:36     444           1680     12915     00:10:59     640           1680     12915     00:09:12     533

twitter-5     12915     12915     00:07:53     444           1680     12915     00:11:18     533           1680     12915     00:07:43     444

wikipedia-1     649     649     00:03:59     820           95     649     00:02:34     699           95     649     00:02:32     695

wikipedia-2     3610     3610     00:13:51     792           328     3610     00:14:13     696           292     3610     00:13:50     798

wikipedia-3     2339     2339     00:05:44     640           175     2339     00:06:04     640           175     2339     00:05:41     640

wikipedia-4     691     691     00:01:54     774           246     691     00:02:01     768           108     691     00:01:55     774

wikipedia-5     21317     21317     TL      620           292     19840     TL      533           220     22307     TL      444

4cRA + CC                              4cRC + CC                              4c + CC                    3cDFS(CC)
2-5 7-10 12-15 17-19
Histories     End states     Mem.       Time              Histories     End states     Mem.       Time              Histories     End states     Mem.      Time          End states     Mem.       Time
courseware-1     216     893     00:00:52     370           216     11751     00:07:02     370           216     124399     TL     444           58072     00:13:52     308

courseware-2     46     106     00:00:06     308           46     588     00:00:11     308           46     1074     00:00:15     308           18010     00:02:12     308

courseware-3     10585     47570     TL     444           40     65075     TL     308           40     119388     TL     370           186758     TL     308

courseware-4     69     88     00:00:07     308           69     2392     00:00:29     308           69     3779     00:00:39     315           37956     00:07:19     308

courseware-5     388     765     00:00:39     308           388     66557     00:27:12     370           320     96681     TL     660           68074     TL     308

shoppingCart-1     444     1620     00:00:34     370           444     202066     TL     370           370     173904     TL     308           69396     TL     308

shoppingCart-2     2934     32976     00:19:58     450           366     224700     TL     370           366     508967     TL     370           93549     TL     308

shoppingCart-3     1594     6291     00:01:41     308           1594     131226     00:18:23     308           1594     223740     TL     308           99522     TL     533

shoppingCart-4     19945     53687     TL     533           151     256686     TL     308           11     267433     TL     308           270996     TL     370

shoppingCart-5     4686     16323     00:06:43     370           2469     265924     TL     469           371     420084     TL     444           191813     TL     404

tpcc-1     165     958     00:02:13     839           7     50588     TL     1045           3     84272     TL     545           18489     TL     1383

tpcc-2     353     3958     00:11:24     809           3     7029     TL     1153           1     23097     TL     670           25253     TL     1029

tpcc-3     1475     10969     TL     1029           20     22934     TL     688           2     119267     TL     459           18124     TL     1251

tpcc-4     105     114     00:00:15     474           17     50203     TL     640           3     112330     TL     670           22645     TL     948

tpcc-5     271     9178     TL     1629           3     4059     TL     662           3     48306     TL     768           36060     TL     1284

twitter-1     36     44     00:00:05     256           36     4104     00:01:07     370           36     12384     00:02:56     473           35056     00:20:25     533

twitter-2     876     2917     00:02:01     592           876     18219     00:09:30     548           876     37943     00:17:35     544           145070     TL     533

twitter-3     1072     2272     00:02:05     576           1072     9514     00:08:10     533           1072     20164     00:16:14     588           108792     00:24:34     452

twitter-4     12915     48363     00:29:09     476           10     114588     TL     370           1     147462     TL     533           50404     TL     533

twitter-5     12915     48363     00:27:07     444           84     70376     TL     444           84     136241     TL     370           57654     TL     444

wikipedia-1     649     2296     00:04:16     672           64     37382     TL     832           4     66814     TL     699           54510     TL     660

wikipedia-2     2049     8451     TL     979           17     19697     TL     795           2     85523     TL     930           43629     TL     650

wikipedia-3     2339     6170     00:10:06     640           100     28952     TL     522           50     23974     TL     581           43962     TL     682

wikipedia-4     691     1781     00:02:57     925           5     44937     TL     567           3     61334     TL     543           24873     TL     1188

wikipedia-5     13159     26384     TL     533           29     72930     TL     444           23     78413     TL     695           97881     TL     444

§.§ Session Scalability

3cOne thread         3cTwo threads            3cThree threads          3cFour threads           3cFive threads
2-4 6-8 10-12 14-16 18-20
Histories     Mem.       Time              Histories     Mem.       Time              Histories     Mem.       Time              Histories     Mem.       Time              Histories     Mem.       Time
courseware-1        1             256MB      00:00:01          6             256MB      00:00:02          62            256MB      00:00:04          882           311MB      00:00:13          19102         370MB      00:02:37

courseware-2        1             256MB      00:00:02          11            256MB      00:00:02          143           256MB      00:00:04          1859          308MB      00:00:23          40040         256MB      00:05:02

shoppingcart-1      1             256MB      00:00:01          20            256MB      00:00:02          775           308MB      00:00:10          57426         308MB      00:04:46          146774        370MB      TL

shoppingcart-2      1             256MB      00:00:01          13            256MB      00:00:02          392           397MB      00:00:10          11598         308MB      00:01:27          217380        370MB      TL

tpcc-1              1             256MB      00:00:02          4             308MB      00:00:03          12            256MB      00:00:05          176           540MB      00:00:20          5520          837MB      00:04:56

tpcc-2              1             256MB      00:00:02          10            308MB      00:00:04          30            446MB      00:00:07          90            672MB      00:00:20          900           923MB      00:03:16

twitter-1           1             256MB      00:00:02          3             256MB      00:00:02          17            256MB      00:00:03          564           370MB      00:00:11          31455         314MB      00:05:34

twitter-2           1             256MB      00:00:02          1             256MB      00:00:02          20            256MB      00:00:03          1995          308MB      00:01:13          103890        444MB      TL

wikipedia-1         1             256MB      00:00:02          27            256MB      00:00:04          5488          371MB      00:04:39          130848        370MB      TL          45018         400MB      TL

wikipedia-2         1             256MB      00:00:02          6             323MB      00:00:03          216           329MB      00:00:08          2984          394MB      00:12:57          31124         1164MB     TL

3cOne session         3cTwo sessions          3cThree sessions          3cFour sessions           3cFive sessions
2-4 6-8 10-12 14-16 18-20
Histories     Time       Mem.              Histories     Time       Mem.              Histories     Time       Mem.              Histories     Time       Mem.              Histories     Time       Mem.
tpcc-1     1     00:00:02     256          6     00:00:03     256          1540     00:05:42     804          3081     TL     4096          14525     TL     4096

tpcc-2     1     00:00:03     256          66     00:00:17     587          9630     TL     2900          17637     TL     4076          2442     TL     4096

tpcc-3     1     00:00:03     256          12     00:00:09     384          4824     00:25:43     1503          3463     TL     4096          2940     TL     4096

tpcc-4     1     00:00:03     256          90     00:00:41     674          6355     TL     1728          1722     TL     4096          2634     TL     4096

tpcc-5     1     00:00:03     256          96     00:00:41     692          3659     TL     1765          1343     TL     4092          1481     TL     4096

wikipedia-1     1     00:00:02     256          199     00:00:19     370          19654     TL     640          16377     TL     533          12419     TL     4096

wikipedia-2     1     00:00:02     256          38     00:00:14     536          7055     00:22:07     768          21000     TL     3520          16985     TL     4096

wikipedia-3     1     00:00:02     256          67     00:00:14     444          9346     TL     768          9451     TL     4096          3264     TL     4096

wikipedia-4     1     00:00:02     256          7     00:00:07     374          73     00:00:14     602          3940     00:20:40     4096          1325     TL     4096

wikipedia-5     1     00:00:02     256          28     00:00:08     308          336     00:05:41     662          10914     TL     4096          563     TL     3936

§.§ Transaction Scalability

3cOne transaction         3cTwo transactions            3cThree transactions          3cFour transactions           3cFive transactions
2-4 6-8 10-12 14-16 18-20
Histories     Mem.       Time              Histories     Mem.       Time              Histories     Mem.       Time              Histories     Mem.       Time              Histories     Mem.       Time
tpcc-1     4     00:00:03     256           107     00:00:46     674           303     00:01:32     812           13780     00:27:59     3904           13431     TL     4096

tpcc-2     18     00:00:11     444           4030     00:16:10     1063           5162     TL     2012           5351     TL     4096           3243     TL     4096

tpcc-3     3     00:00:04     256           219     00:01:38     881           6679     TL     1327           6533     TL     4093           2036     TL     4096

tpcc-4     20     00:00:13     444           5187     00:20:04     1046           3262     TL     2066           1548     TL     4096           2045     TL     4096

tpcc-5     1     00:00:03     256           23     00:00:15     596           171     00:01:31     901           1812     TL     3933           4091     TL     4096

wikipedia-1     16     00:00:04     308           2428     00:02:30     444           22289     TL     533           17113     TL     640           14648     TL     4096

wikipedia-2     9     00:00:06     256           56     00:00:20     533           739     00:02:02     690           5364     TL     4068           3568     TL     3977

wikipedia-3     18     00:00:07     308           1109     00:01:24     640           26110     TL     768           15339     TL     3621           15138     TL     3822

wikipedia-4     4     00:00:05     256           43     00:00:12     444           3919     00:29:57     1649           3501     TL     4096           2506     TL     4096

wikipedia-5     2     00:00:03     256           20     00:00:10     444           46     00:00:20     370           754     00:05:42     2521           2573     TL     4096