#  Repairing Serializability Bugs in Distributed Database Programs via
Automated Schema Refactoring

Kia Rahmani  0000-0001-9064-0797 Purdue University<EMAIL_ADDRESS>,
Kartik Nagar  IIT Madras<EMAIL_ADDRESS>,  Benjamin Delaware  Purdue
University<EMAIL_ADDRESS>and  Suresh Jagannathan  Purdue University
<EMAIL_ADDRESS>
(2021)

###### Abstract.

Serializability is a well-understood concurrency control mechanism that eases
reasoning about highly-concurrent database programs. Unfortunately, enforcing
serializability has a high performance cost, especially on geographically
distributed database clusters. Consequently, many databases allow programmers
to _choose_ when a transaction must be executed under serializability, with
the expectation that transactions would only be so marked when necessary to
avoid serious concurrency bugs. However, this is a significant burden to
impose on developers, requiring them to (a) reason about subtle concurrent
interactions among potentially interfering transactions, (b) determine when
such interactions would violate desired invariants, and (c) then identify the
minimum number of transactions whose executions should be serialized to
prevent these violations. To mitigate this burden, this paper presents a sound
and fully automated schema refactoring procedure that transforms a program’s
data layout – rather than its concurrency control logic – to eliminate
statically identified concurrency bugs, allowing more transactions to be
safely executed under weaker and more performant database guarantees.
Experimental results over a range of realistic database benchmarks indicate
that our approach is highly effective in eliminating concurrency bugs, with
safe refactored programs showing an average of 120% higher throughput and 45%
lower latency compared to a serialized baseline.

††copyright: none††copyright: rightsretained††doi:
10.1145/3453483.3454028††journalyear: 2021††submissionid:
pldi21main-p25-p††isbn: 978-1-4503-8391-2/21/06††conference: Proceedings of
the 42nd ACM SIGPLAN International Conference on Programming Language Design
and Implementation; June 20–25, 2021; Virtual, UK††booktitle: Proceedings of
the 42nd ACM SIGPLAN International Conference on Programming Language Design
and Implementation (PLDI ’21), June 20–25, 2021, Virtual, UK††ccs: Software
and its engineering System modeling languages††ccs: Software and its
engineering Application specific development environments

##  1\. Introduction

Programs that concurrently access shared data are ubiquitous: bank accounts,
shopping carts, inventories, and social media applications all rely on a
shared database to store information. For performance and fault tolerence
reasons, the underlying databases that manage state in these applications are
often replicated and distributed across multiple, geographically distant
locations (Sovran et al., 2011; Lloyd et al., 2013; Lakshman and Malik, 2010;
Schultz et al., 2019). Writing programs which interact with such databases is
notoriously difficult, because the programmer has to consider an exponential
space of possible interleavings of database operations in order to ensure that
a client program behaves correctly. One approach to simplifying this task is
to assume that sets of operations, or _transactions_ , executed by the program
are _serializable_ (Papadimitriou, 1979), i.e. that the state of the database
is always consistent with some sequential ordering of those transactions. One
way to achieve this is to rely on the underlying database system to seamlessly
enforce this property. Unfortunately, such a strategy typically comes at a
considerable performance cost. This cost is particularly significant for
distributed databases, where the system must rely on expensive coordination
mechanisms between different replicas, in effect limiting _when_ a transaction
can see the effects of another in a way that is consistent with a serializable
execution (Bailis et al., 2013). This cost is so high that developers default
to weaker consistency guarantees, using careful design and testing to ensure
correctness, only relying on the underlying system to enforce serializable
transactions when serious bugs are discovered (Lu et al., 2004;
Sivaramakrishnan et al., 2015; Gotsman et al., 2016; Rahmani et al., 2018).

Uncovering such bugs is a delicate and highly error-prone task even in
centralized environments: in one recent study, Warszawski and Bailis (2017)
examined 12 popular eCommerce applications used by over two million well-known
websites and discovered 22 security vulnerabilities and invariant violations
that were directly attributable to non-serializable transactions. To help
developers identify such bugs, the community has developed multiple program
analyses that report potential _serializability anomalies_ (Gotsman et al.,
2016; Nagar and Jagannathan, 2018; Kaki et al., 2018a; Brutschy et al., 2017,
2018). Automatically repairing these anomalies, however, has remained a
challenging open problem: in many cases full application safety is only
achievable by relying on the system to enforce strong consistency of all
operations. Such an approach results in developers either having to sacrifice
performance for the sake of correctness, or conceding to operate within a
potentially restricted ecosystem with specialized services and APIs (Bacon et
al., 2017) architected with strong consistency in mind.

In this paper, we propose a novel language-centric approach to resolving
concurrency bugs that arise in these distributed environments. Our solution is
to alter the _schema_ , or data layout, of the data maintained by the
database, rather than the consistency levels of the transactions that access
that data. Our key insight is that it is possible to modify shared state to
remove opportunities for transactions to witness changes that are inconsistent
with serializable executions. We, therefore, investigate automated schema
transformations that change _how_ client programs access data to ensure the
absence of concurrency bugs, in contrast to using expensive coordination
mechanisms to limit _when_ transactions can concurrently access the database.

For example, to prevent transactions from observing non-atomic updates to
different rows in different tables, we can fuse the offending fields into a
single row in a single table whose updates are guaranteed to be atomic under
any consistency guarantee. Similarly, consecutive reads and writes on a row
can be refactored into “functional” inserts into a new table, which removes
the race condition between concurrently running instances of the program. By
changing the schema (and altering how transactions access data accordingly),
without altering a transaction’s atomicity and isolation levels, we can make
clients of distributed databases _safer_ without _sacrificing performance_. In
our experimental evaluation, we were able to fix on average 74% of all
identified serializability anomalies with only a minimal impact (less than 3%
on average) on performance in an environment that provides only weak
eventually consistent guarantees (Burckhardt, 2014). For the remaining 26% of
anomalies that were not eliminated by our refactoring approach, simply marking
the offending transactions as serializable yields a provably safe program that
nonetheless improves the throughput (resp. latency) of its fully serialized
counterpart by 120% (resp. 45%) on average.

This paper makes the following contributions:

  1. (1)

We observe that serializability violations in database programs can be
eliminated by changing the schema of the underlying database and the client
programs in order to eliminate problematic accesses to shared database state.

  2. (2)

Using this observation, we develop an automated refactoring algorithm that
iteratively repairs statically identified serializability anomalies in
distributed database clients. We show this algorithm both preserves the
semantics of the original program and eliminates many identified
serializability anomalies.

  3. (3)

We develop a tool, (Atropos), implementing these ideas, and demonstrate its
ability to reduce the number of serializability anomalies in a corpus of
standard benchmarks with minimal performance impact over the original program,
but with substantially stronger safety guarantees.

The remainder of the paper is structured as follows. The next section presents
an overview of our approach. Section 3 defines our programming model and
formalizes the notion of concurrency bugs. Section 4 provides a formal
treatment of our schema refactoring strategy. Sections 5 and 6 describe our
repair algorithm and its implementation, respectively. Section 7 describes our
experimental evaluation. Related work and conclusions are given in Section 8
and Section 9.

##  2\. Overview

To illustrate our approach, consider an online course management program that
uses a database to manage a list of course offerings and registered students.
Figure 1 presents a simplified code snippet implementing such a program. The
database consists of three tables, maintaining information regarding courses,
students, and their email addresses. The $\mathtt{STUDENT}$ table maintains a
reference to a student’s email entry in schema $\mathtt{EMAIL}$ (via secondary
key $\mathtt{st\\_em\\_id}$) and a reference to a course entry in table
$\mathtt{COURSE}$ (via secondary key $\mathtt{st\\_co\\_id}$) that the student
has registered for. A student’s registration status is stored in field
$\mathtt{st\\_reg}$. Each entry in table $\mathtt{COURSE}$ also stores
information about the availability of a course and the number of enrolled
students.

The program includes three sets of database operations or _transactions_.
Transaction $\mathtt{getSt}$, given a student’s id, first retrieves all
information for that student (S1). It then performs two queries, (S2 and S3),
on the other tables to retrieve their email address and course availability.
Transaction $\mathtt{setSt}$ takes a student’s id and updates their name and
email address. It includes a query (S4) and an update (U1) to table
$\mathtt{STUDENT}$ and an update to the $\mathtt{EMAIL}$ table (U2). Finally,
transaction $\mathtt{regSt}$ registers a student in a course. It consists of
an update to the student’s entry (U3), a query to $\mathtt{COURSE}$ to
determine the number of students enrolled in the course they wish to register
for (S5), and an update to that course’s availability (U4) indicating that it
is available now that a student has registered for it.

The desired semantics of this program is these transactions should be
performed _atomically_ and in _isolation_. Atomicity guarantees that a
transaction never observes intermediate updates of another transaction.
Isolation guarantees that a transaction never observes changes to the database
by other committed transactions once it begins executing. Taken together,
these properties ensure that all executions of this program are _serializable_
, yielding behavior that corresponds to some sequential interleaving of these
transaction instances.

⬇

1getSt(id):

2 x:=select * from STUDENT where st_id=id//S1

3 y:=select em_addr from EMAIL where em_id=x.st_em_id//S2

4 z:=select co_avail from COURSE where co_id=x.st_co_id//S3

⬇

1setSt(id,name,email):

2 x := select st_em_id from STUDENT where st_id=id//S4

3 update STUDENT set st_name=name where st_id=id//U1

4 update EMAIL set em_addr=email where em_id=x.st_em_id//U2

⬇

1regSt(id,course):

2 update STUDENT set st_co_id=course, st_reg=true

3 where st_id=id//U3

4 x:=select co_st_cnt from COURSE where co_id=course//S5

5 update COURSE set co_st_cnt=x.co_st_cnt+1,

6 co_avail=true where co_id=course //U4

Figure 1. Database schemas and code snippets from an online course management
program

While serializability is highly desirable, it requires using costly
centralized locks (Garcia-Molina et al., 2008) or complex version management
systems (Bernstein and Goodman, 1983), which severely reduce the system’s
available concurrency, especially in distributed environments where database
state may be replicated or partitioned to improve availability. In such
environments, enforcing serializability typically either requires coordination
among all replicas whenever shared data is accessed or updated, or ensuring
replicas always witness the same consistent order of operations (Corbett et
al., 2012). As a result, in most modern database systems, transactions can be
executed under weaker isolation levels, e.g. permitting them to observe
updates of other committed transactions during their execution (MySQL, 2020;
PostgreSQL, 2020; Schultz et al., 2019; Lakshman and Malik, 2010).
Unfortunately, these weaker guarantees can result in _serializability
anomalies_ , or behaviors that would not occur in a serial execution. To
illustrate, Figure 2 presents three concurrent executions of this program’s
transaction instances that exhibit non-serializable behaviors.

The execution on the left shows instances of the $\mathtt{getSt}$ and
$\mathtt{setSet}$ transactions. Following the order in which operations
execute (denoted by red arrows), observe that (S2) witnesses the update to a
student’s email address, but (S1) does not see their updated name. This
anomaly is known as a _non-repeatable read_. The execution in the center
depicts the concurrent execution of instances of $\mathtt{getSt}$ and
$\mathtt{regSt}$. Here, (S1) witnesses the effect of (U3) observing that the
student is registered, but (S3) sees that the course is unavailable, since it
does not witness the effect of (U4). This is an instance of a _dirty-read_
anomaly. Lastly, the execution on the right shows two instances of
$\mathtt{regSt}$ that attempt to increment the number of students in a course.
This undesirable behavior, known as a _lost update_ , leaves the database in a
state inconsistent with any sequential execution of the two transaction
instances. All of these anomalies can arise if the strong atomicity and
isolation guarantees afforded by serializability are weakened.

Figure 2. Serializability Anomalies

Several recent proposals attempt to identify such undesirable behaviors in
programs using a variety of static or dynamic program analysis and monitoring
techniques (Brutschy et al., 2017, 2018; Nagar and Jagannathan, 2018;
Warszawski and Bailis, 2017). Given potential serializability violations, the
standard solution is to strengthen the atomicity and isolation requirements on
the offending transactions to eliminate the undesirable behaviour, at the cost
of increased synchronization overhead or reduced availability (Bailis et al.,
2014b; Sivaramakrishnan et al., 2015; Gotsman et al., 2016).

###  2.1. Atropos

Are developers obligated to sacrifice concurrency and availability in order to
recover the pleasant safety properties afforded by serializability?
Surprisingly, we are able to answer this question in the negative. To see why,
observe that a database program consists of two main components - a set of
computations that includes transactions, SQL operations (e.g., selects and
updates), locks, isolation-level annotations, etc.; and a memory abstraction
expressed as a relational schema that defines the layout of tables and the
relationship between them. The traditional candidates picked for repairing a
serializability anomaly are the transactions from the computational component:
by injecting additional concurrency control through the use of locks or
isolation-strengthening annotations, developers can control the degree of
concurrency permitted, albeit at the expense of performance and availability.

This paper investigates the under-explored alternative of transforming the
program’s schema to reduce the number of potentially conflicting accesses to
shared state. For example, by _aggregating_ information found in multiple
tables into a single row on a single table, we can exploit built-in _row-level
atomicity_ properties to eliminate concurrency bugs that arise because of
multiple non-atomic accesses to different table state. Row-level atomicity, a
feature supported in most database systems, guarantees that other concurrently
executing transactions never observe partial updates to a particular row.
Alternatively, it is possible to _decompose_ database state to minimize the
number of distinct updates to a field, for example by logging state changes
via table _inserts_ , rather than recording such changes via _updates_. The
former effectively acts as a functional update to a table. To be sure, these
transformations affect read and write performance to database tables and
change the memory footprint, but they notably impose no additional
synchronization costs. In scalable settings such as replicated distributed
environments, this is a highly favorable tradeoff since the cost of global
concurrency control or coordination is often problematic in these settings, an
observation that is borne our in our experimental results.

⬇

1getSt(id):

2 x:=select * from STUDENT where st_id=id //RS1,RS2,RS3

⬇

1setSt(id,name,email):

2 update STUDENT set st_name=name,st_em_addr=email

3 where st_id=id //RU1,RU2

⬇

1regSt(id,course):

2 update STUDENT set st_co_id=course, st_co_avail=true,

3 st_reg=true where st_id=id //RU3

4 insert into COURSE_CO_ST_CNT_LOG values

5 (co_id=course,log_id=uuid(),co_st_cnt_log=1) //RU4

Figure 3. Refactored transactions and database schemas Figure 4. Schematic
overview of Atropos

To illustrate the intuition behind our approach, consider the database program
depicted in Figure 3. This program behaves like our previous example, despite
featuring very different database schemas and transactions. The first of the
two tables maintained by the program, $\mathtt{STUDENT}$, removes the
references to other tables from the original $\mathtt{STUDENT}$ table, instead
maintaining independent fields for the student’s email address and their
course availability. These changes make the original course and email tables
obsolete, so they have been removed. In addition, the number of students in
each course is now stored in a dedicated table
$\mathtt{COURSE\\_CO\\_ST\\_CNT\\_LOG}$. Each time the enrollment of a course
changes, a new record is inserted into this table to record the change.
Subsequent queries can retrieve all corresponding records in the table and
aggregate them in the program itself to determine the number of students in a
course.

The transactions in the refactored program are also modified to reflect the
changes in the data model. The transaction $\mathtt{getSt}$ now simply selects
a single record from the student table to retrieve all the requested
information for a student. The transaction $\mathtt{setSt}$ similarly updates
a single record. Note that both these operations are executed atomically, thus
eliminating the problematic data accesses in the original program. Similarly,
$\mathtt{regSt}$ updates the student’s $\mathtt{st\\_co\\_id}$ field and
inserts a new record into the schema $\mathtt{COURSE\\_CO\\_ST\\_CNT\\_LOG}$.
Using the function $\mathtt{uuid()}$ ensures that a new record is inserted
every time the transaction is called. These updates remove potential
serializability anomalies by replacing the disjoint updates to fields in
different tables from the original with a simple atomic row insertion.
Notably, the refactored program can be shown to be a meaningful _refinement_
of the original program, despite eliminating problematic serializability
errors found in it. Program refinement ensures that the refactored program
maintains _all_ information maintained by the original program without
exhibiting _any_ new behaviour.

The program shown in Figure 3 is the result of several database schema
refactorings (Ambler, 2006; Faroult, 2008; Fowler, 2019), incremental changes
to a database program’s data model along with corresponding semantic-
preserving modifications to its logic. Manually searching for such a
refactored program is unlikely to be successful. On one hand, the set of
potential solutions is large (Ambler, 2006), rendering any manual exploration
infeasible. On the other hand, the process of rewriting an application for a
(even incrementally) refactored schema is extremely tedious and error-prone
(Wang et al., 2019).

We have implemented a tool named Atropos that, given a database program,
explores the space of its possible schema and program refactorings, and
returns a new version with possibly many fewer concurrency bugs. The
refactored program described above, for example, is automatically generated by
Atropos from the original shown in Figure 1. Figure 4 presents the Atropos
pipeline. A static analysis engine is used to identify potential
serializability anomalies in a given program. The program is then preprocessed
to extract the components which are involved in at least one anomaly, in order
to put it into a form amenable for our analysis. Next, a refactoring engine
applies a variety of transformations in an attempt to eliminate the bugs
identified by our static analysis. Finally, the program is analyzed to
eliminate dead code, and the refactored version is then reintegrated into the
program from which it was extracted.

##  3\. Database Programs

f∈FldNameρ∈SchmNamet∈TxnNamea∈Argx∈Varn∈Valagg∈{sum,min,max}e≔n ∣ a ∣ e⊕e ∣
e⊙e ∣ e ∘e ∣ iter ∣ agg(x.f) ∣ at^e(x.f)ϕ_≔this.f ⊙e ∣ ϕ_ ∘ϕ_q≔x:= SELECT
¯fFROM R WHERE ϕ ∣ UPDATE R SET ¯f = eWHERE ϕc≔q ∣ iterate(e){c} ∣ if(e){c} ∣
skip ∣ c;c ⊕∈{+, -, ×, /}⊙∈{<, ≤, =, >, ≥}∘∈{∧,∨}T≔t(¯a){c; return e
}R≔ρ:¯fF≔⟨¯f : n⟩P≔(¯R,¯T) Figure 5. Syntax of database programs

The syntax of our database programs is given in Figure 5. A program $P$ is
defined in terms of a set of database schemas ($\overline{R}$), and a set of
transactions ($\overline{T}$). A database schema consists of a schema name
($\rho$) and a set of field names ($\overline{f}$). A database _record_ ($F$)
for schema $R$ is comprised of a set of value bindings to $R$’s fields. A
database table is a set of records. Associated with each schema is a non-empty
subset of its fields that act as a _primary key_. Each assignment to these
fields identifies a unique record in the table. In the following, we write
$R_{\mathtt{id}}$ to denote the set of all possible primary key values for the
schema $R$. In our model, a table includes a record corresponding to _every_
primary key. Every schema includes a special Boolean field,
$alive\in\mathtt{FldName}$, whose value determines if a record is actually
present in the table. This field allows us to model
${\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{DELETE}\;}$and
${\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{INSERT}\;}$commands
without explicitly including them in our program syntax.

Transactions are uniquely named, and are defined by a sequence of parameters,
a body, and a return expression. The body of a transaction ($c$) is a sequence
of _database commands_ ($q$) and _control commands_. A database command either
modifies or retrieves a subset of records in a database table. The records
retrieved by a database query are stored locally and can be used in subsequent
commands. Control commands consist of conditional guards, loops, and return
statements. Both database commands
(${\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SELECT}\;}$and
${\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}\\!$)
require an explicit _where clause_ ($\phi$) to filter the records they
retrieve or update. $\phi_{\mathtt{fld}}$ denotes the set of fields appearing
in a clause $\phi$.

Expressions ($e$) include constants, transaction arguments, arithmetic and
Boolean operations and comparisons, iteration counters and field accessors.
The values of field $f$ of records stored in a variable $x$ can be aggregated
using $\mathtt{agg}(x.f)$, or accessed individually, using
$\mathtt{at}^{e}(x.f)$.

###  3.1. Data Store Semantics

Database states $\Sigma$ are modeled as a triple
$(\mathtt{str},\mathtt{vis},\mathtt{cnt})$, where $\mathtt{str}$ is a set of
_database events_ ($\eta$) that captures the history of all reads and writes
performed by a program operating over the database, and $\mathtt{vis}$ is a
partial order on those events. The execution counter, $\mathtt{cnt}$, is an
integer that represents a global timestamp that is incremented every time a
database command is executed; it is used to resolve conflicts among concurrent
operations performed on the same elements, which can be used to define a
_linearization_ or _arbitration order_ on updates (Burckhardt et al., 2014).
Given a database state ($\Sigma$), and a primary key $r\in R_{\texttt{id}}$,
it is possible to reconstruct each field $f$ of a record $r$, which we denote
as $\Sigma(r.f)$.

Retrieving a record from a table $R$ generates a set of _read events_ ,
${\color[rgb]{0.0390625,0.0390625,0.66796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.0390625,0.66796875}\mathsf{rd}(\tau,r,f)}$,
which witness that the field $f$ of the record with the primary key $r\in
R_{\mathtt{id}}$ was accessed when the value of the execution counter was
$\tau$. Similarly, a _write event_ ,
${\color[rgb]{0.0390625,0.0390625,0.66796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.0390625,0.66796875}\mathsf{wr}(\tau,r,f,n)}$,
records that the field $f$ of record $r$ was assigned the value $n$ at
timestamp $\tau$. The timestamp (resp. record) associated with an event $\eta$
is denoted by $\eta_{\tau}$ (resp. $\eta_{r}$).

Our semantics enforces record-level atomicity guarantees: transactions never
witness intermediate (non-committed) updates to a record in a table by another
concurrently executing one. Thus, all updates to fields in a record from a
database command happen atomically. This form of atomicity is offered by most
commercial database systems, and is easily realized through the judicious use
of locks. Enforcing stronger multi-record atomicity guarantees is more
challenging, especially in distributed environments with replicated database
state (Zellag and Kemme, 2014; Eswaran et al., 1976; Li et al., 2012;
Bernstein and Das, 2013; Bailis et al., 2014a). In this paper, we consider
behaviors induced when the database guarantees only a very weak form of
consistency and isolation that allows transactions to see an _arbitrary
subset_ of committed updates by other transactions. Thus, a transaction which
accesses multiple records in a table is not obligated to witness _all_ updates
performed by another transaction on these records.

To capture these behaviors, we use a _visibility_ relation between events,
$\mathtt{vis}$, that relates two events when one witnesses the other in its
_local view_ of the database at the time of its creation. A local view is
captured by the relation $\lhd\subseteq\Sigma\times\Sigma$ between database
states, which is constrained as follows:

(ConstructView)

str’⊆str ∀η’∈str’∀η∈str(ηr= η’r∧ ητ= η’τ)
⇒(η∈str’)vis’=vis|str’cnt’=cnt(str’,vis’,cnt’) ⊲(str,vis,cnt)

The above definition ensures that an event can only be present in a local
view, $\mathtt{str}^{\prime}$, if all other events on the same record with the
same counter value are also present in $\mathtt{str}^{\prime}$ (ensuring
record-level atomicity). Additionally, the visibility relation permitted on
the local view, $\mathtt{vis}^{\prime}$, must be consistent with the global
visibility relation, $\mathtt{vis}$.

(txn-invoke)

$\footnotesize\frac{\begin{array}[]{c}n\in\mathtt{Val}\qquad
t(\overline{a})\\{c;\mathtt{return}\;e\\}\in
P_{\mathtt{txn}}\end{array}}{\begin{array}[]{c}{\Sigma,\Gamma\Rightarrow{}\Sigma,\Gamma\\!\cup\\!\\{t:c[\overline{a/n}];\mathtt{skip}\;;e[\overline{a/n}];\varnothing\\}}\end{array}}$

(txn-step)

$\footnotesize\frac{\begin{array}[]{c}\Sigma,\Delta,c\xrightarrow{}\Sigma^{\prime},\Delta^{\prime},c^{\prime}\par\end{array}}{\begin{array}[]{c}{\Sigma,\\{t:c;e;\Delta\\}\\!\cup\\!\Gamma\Rightarrow{}\Sigma^{\prime},\\{t:c^{\prime};e;\Delta^{\prime}\\}\\!\cup\\!\Gamma}\end{array}}$

(txn-ret)

$\footnotesize\frac{\begin{array}[]{c}e\not\in\mathtt{Val}\qquad\Delta,e\Downarrow
m\end{array}}{\begin{array}[]{c}{\Sigma,\\{t:\mathtt{skip};e;\Delta\\}\\!\cup\\!\Gamma\Rightarrow{}\Sigma,\\{t:\mathtt{skip};m;\Delta\\}\\!\cup\\!\Gamma}\end{array}}$

(seq)

$\footnotesize\frac{\begin{array}[]{c}{\Sigma,\Delta,c\xrightarrow{}\Sigma^{\prime},\Delta^{\prime},c^{\prime\prime}\par}\end{array}}{\begin{array}[]{c}{\Sigma,\Delta,c;c^{\prime}\xrightarrow{}\Sigma^{\prime},\Delta^{\prime},c^{\prime\prime};c^{\prime}}\end{array}}$

(skip)

$\footnotesize\frac{\begin{array}[]{c}\\\
\end{array}}{\begin{array}[]{c}{\Sigma,\Delta,\mathtt{skip};c\xrightarrow{}\Sigma,\Delta,c}\end{array}}$

(cond-t)

$\footnotesize\frac{\begin{array}[]{c}\Delta,e\Downarrow\mathtt{true}\end{array}}{\begin{array}[]{c}{\Sigma,\Delta,\mathtt{if}(e)\\{c\\}\xrightarrow{}\Sigma,\Delta,c}\end{array}}$

(cond-f)

$\footnotesize\frac{\begin{array}[]{c}\Delta,e\Downarrow\mathtt{false}\end{array}}{\begin{array}[]{c}{\Sigma,\Delta,\mathtt{if}(e)\\{c\\}\xrightarrow{}\Sigma,\Delta,\mathtt{skip}}\end{array}}$

(iter)

$\footnotesize\frac{\begin{array}[]{c}\Delta,e\Downarrow
n\end{array}}{\begin{array}[]{c}{\Sigma,\Delta,\mathtt{iterate}(e)\\{c\\}\xrightarrow{}\Sigma,\Delta,\mathtt{concat}(n,c)}\end{array}}$

(select)

$\footnotesize\frac{\begin{array}[]{c}\Sigma^{\prime}\lhd\Sigma\qquad\varepsilon_{1}=\\{{\color[rgb]{0.0390625,0.0390625,0.66796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.0390625,0.66796875}\mathsf{rd}(\mathtt{cnt},r,f)}\,\mid\,r\in
R_{\mathtt{id}}\;\wedge\;f\in\phi_{\mathtt{fld}}\\}\\\
\qquad\mathtt{results}=\\{(r,\langle\overline{f:n}\rangle)\,\mid\,r\in
R_{\mathtt{id}}\;\wedge\;\Sigma^{\prime}(r)=\langle\overline{f^{\prime}:n^{\prime}}\rangle\;\wedge\\\
\qquad\qquad\Delta,\phi(\langle\overline{f^{\prime}:n^{\prime}}\rangle)\Downarrow\mathtt{true}\;\wedge\;\overline{f:n}\subseteq\overline{f^{\prime}:n^{\prime}}\\}\\\
\varepsilon_{2}=\\{{\color[rgb]{0.0390625,0.0390625,0.66796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.0390625,0.66796875}\mathsf{rd}(\mathtt{cnt},r,f^{\prime}_{i})}\,\mid\,(r,\langle\overline{f^{\prime}:n^{\prime}}\rangle)\in\mathtt{results}\;\wedge\;f^{\prime}_{i}\in\overline{f}\\}\\\
\mathtt{str}^{\prime}=\Sigma.\mathtt{str}\cup\varepsilon_{1}\cup\varepsilon_{2}\qquad\mathtt{vis}^{\prime}=\Sigma.\mathtt{vis}\cup\\{(\eta,\eta^{\prime})|\,\eta^{\prime}\in\varepsilon_{1}\cup\varepsilon_{2}\;\wedge\;\eta\in\Sigma^{\prime}.\mathtt{str})\\}\end{array}}{\begin{array}[]{c}{\Sigma,\Delta,x:={\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SELECT}\;}\overline{f}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{FROM}\;}R\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}\phi\xrightarrow{}(\mathtt{str}^{\prime},\mathtt{vis}^{\prime},\mathtt{cnt}+1),\Delta[x\mapsto\mathtt{results}],\texttt{skip}}\end{array}}$

(update)

$\footnotesize\frac{\begin{array}[]{c}\Sigma^{\prime}\lhd\Sigma\\\
{\varepsilon}=\\{{\color[rgb]{0.0390625,0.0390625,0.66796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.0390625,0.66796875}\mathsf{wr}(\mathtt{cnt},r,f_{i},m)}\,|\,r\in
R_{\mathtt{id}}\;\wedge\;\Sigma^{\prime}(r)=\langle\overline{f:n}\rangle\;\wedge\\\
\qquad\Delta,\phi(\langle\overline{f:n}\rangle)\Downarrow\mathtt{true}\;\wedge\;(f_{i}=e_{i})\in\overline{f=e}\;\wedge\;\Delta,e_{i}\Downarrow
m\\}\\\
\mathtt{str}^{\prime}=\Sigma.\mathtt{str}\cup\varepsilon\qquad\mathtt{vis}^{\prime}=\Sigma.\mathtt{vis}\cup\\{(\eta,\eta^{\prime})|\,\eta^{\prime}\in\varepsilon\wedge\eta\in\Sigma^{\prime}.\mathtt{str}\\}\end{array}}{\begin{array}[]{c}{\Sigma,\Delta,{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}R\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SET}\;}\overline{f=e}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}\phi\xrightarrow{}(\mathtt{str}^{\prime},\mathtt{vis}^{\prime},\mathtt{cnt}+1),\Delta,\texttt{skip}}\end{array}}$

Figure 6. Operational semantics of weakly-isolated database programs.

Figure 6 presents the operational semantics of our language, which is defined
by a small-step reduction relation, $\Rightarrow\
\subseteq\Sigma\times\Gamma\times\Sigma\times\Gamma$, between tuples of data-
store states ($\Sigma$) and a set of currently executing transaction instances
($\Gamma\subseteq c\times
e\times(\mathtt{Var}\rightharpoonup\overline{R_{\texttt{id}}\times F})$). A
transaction instance is a tuple consisting of the unexecuted portion of the
transaction body (i.e., its continuation), the transaction’s return
expression, and a local store holding the results of previously processed
query commands. The rules are parameterized over a program $P$ containing a
set of transactions, $P_{\mathtt{txn}}$. At every step, a new transaction
instance can be added to the set of currently running transactions via (txn-
invoke). Alternatively, a currently running transaction instance can be
processed via (txn-step). Finally, if the body of a transaction has been
completely processed, its $\mathtt{return}$ expression is evaluated via (txn-
ret); the resulting instance simply records the binding between the
transaction instance ($t$) and its return value ($m$).

The semantics of commands are defined using a local reduction relation
($\rightarrow$) on database states, local states, and commands. The semantics
for control commands are straightforward outside of the (iter) rule, which
uses an auxiliary function $\mathtt{concat}(n,c)$ to sequence $n$ copies of
the command $c$. Expression evaluation is defined using the big-step relation
$\Downarrow\,\subseteq(\mathtt{Var}\rightharpoonup\overline{R_{\texttt{id}}\times
F})\times e\times\mathtt{Val}$ which, given a store holding the results of
previous query commands, determines the final value of the expression. The
full definition of $\Downarrow$ can be found in the supplementary material.

The semantics of database commands, given by the (select) and (update) rules,
expose the interplay between global and local views of the database. Both
rules construct a local view of the database $(\Sigma^{\prime}\lhd\Sigma)$
that is used to select or update the contents of records. Neither rule imposes
any restrictions on $\Sigma^{\prime}$ other than the consistency constraints
defined by (ConstructView). The key component of each rule is how it defines
the set of new events ($\varepsilon$) that are added to the database. In the
select rule, $\varepsilon_{1}$ captures the retrievals that occur on database-
wide scans to identify records satisfying the
${\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SELECT}\;}$command’s
where clause. In an abuse of notation, we write
$\Delta,\phi(\langle\overline{f:n}\rangle)\Downarrow n$ as shorthand for
$\Delta,\phi[\overline{\mathtt{this.f}/n}]\Downarrow n$. $\varepsilon_{2}$
constructs the appropriate read events of these retrieved records. The
(update) rule similarly defines $\varepsilon$, the set of write events on the
appropriate fields of the records that satisfy the where clause of the
${\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}$command
under an arbitrary (but consistent) local view ($\Sigma^{\prime}$) of the
global store ($\Sigma$). Both rules increment the local timestamp, and
establish new global visibility constraints reflecting the dependencies
introduced by the database command, i.e., all the generated read and write
events depending upon the events in the local view. All updates are performed
atomically, as the set of corresponding write events all have the same
timestamp value, however, other transactions are not obligated to see all the
effects of an update since their local view may only capture a subset of these
events.

###  3.2. Anomalous Data Access Pairs

We reason about concurrency bugs on transactions induced by our data store
programming model using _execution histories_ ; finite traces of the form:
$\Sigma_{1},\Gamma_{1}\Rightarrow\Sigma_{2},\Gamma_{2}\Rightarrow\dots\Rightarrow\Sigma_{k},\Gamma_{k}$
that capture interleaved execution of concurrently executing transactions. A
_complete_ history is one in which all transactions have finished, i.e., the
final $\Gamma$ in the trace is of the form:
$\\{t_{1}:\texttt{skip};m_{1},\Delta_{1}\\}\cup\ldots\cup\\{t_{k}:\texttt{skip};m_{k},\Delta_{k}\\}$.
As a shorthand, we refer to the final state in a history $h$ as
$h_{\mathtt{fin}}$. A _serial_ execution history satisfies two important
properties:

  1. (1)

Strong Atomicity:
$(\forall{\eta,\eta^{\prime}}.\;\eta_{\mathtt{cnt}}<\eta^{\prime}_{\mathtt{cnt}}\Rightarrow\mathtt{vis}(\eta,\eta^{\prime}))\wedge\forall{\eta,\eta^{\prime},\eta^{\prime\prime}}.\;\mathtt{st}(\eta,\eta^{\prime})\wedge(\mathtt{vis}(\eta,\eta^{\prime\prime})\Rightarrow\mathtt{vis}(\eta^{\prime},\eta^{\prime\prime}))$

  2. (2)

Strong Isolation::
$\forall{\eta,\eta^{\prime},\eta^{\prime\prime}}.\;\mathtt{st}(\eta,\eta^{\prime})\wedge\mathtt{vis}(\eta^{\prime\prime},\eta^{\prime})\Rightarrow\mathtt{vis}(\eta^{\prime\prime},\eta)$.

The strong atomicity property prevents non-atomic interleavings of
concurrently executing transactions. The first constraint linearizes events,
relating timestamp ordering of events to visibility. The second generalizes
this notion to multiple events, obligating _all_ effects from the same
transaction (identified by the $\mathtt{st}$ relation) to be visible to
another if any of them are; in particular, any recorded event of a transaction
$T_{1}$ that precedes an event in $T_{2}$ requires all of $T_{1}^{\prime}s$
events to precede all of $T_{2}$’s.

The strong isolation property prevents a transaction from observing the
commits of other transactions once it begins execution. It does so through
visibility constraints on a transaction $T$ that require any event
$\eta^{\prime\prime}$ generated by any other transaction that is visible to an
event $\eta^{\prime}$ generated by $T$ to be visible to any event $\eta$ that
precedes it in $T$’s execution.

A _serializability anomaly_ is an execution history with a final state that
violates at least one of the above constraints. These sorts of anomalies
capture when the events of a transaction instance are either not made visible
to other events in totality (in the case of a violation of strong atomicity)
or which themselves witness different events (in the case of a violation of
strong isolation). Both kinds of anomalies can be eliminated by identifying
commands which generate sets of problematic events and altering them to ensure
_atomic execution_. Two events are executed atomically if they witness the
same set of events and they are both made visible to other events
simultaneously, i.e.
$\mathtt{atomic}(\eta,\eta^{\prime})\equiv\forall\eta^{\prime\prime}.\;(\mathtt{vis}(\eta,\eta^{\prime\prime})\Rightarrow\mathtt{vis}(\eta^{\prime},\eta^{\prime\prime}))\wedge(\mathtt{vis}(\eta^{\prime\prime},\eta)\Rightarrow\mathtt{vis}(\eta^{\prime\prime},\eta^{\prime}))$.

Given a program $P$, we define a _database access pair_ ($\chi$) as a
quadruple $(c_{1},\overline{f}_{1},c_{2},\overline{f}_{2})$ where $c_{1}$ and
$c_{2}$ are database commands from a transaction in $P$, and
$\overline{f}_{1}$ (resp. $\overline{f}_{2}$) is a subset of the fields that
are accessed by $c_{1}$ (resp. $c_{2}$). An access pair is anomalous if there
is at least one execution in the execution history of P that results in an
event generated by $c_{1}$ accessing a field $f_{1}\in\overline{f}_{1}$ which
induces a serializability anomaly with another event generated by $c_{2}$
accessing field $f_{2}\in\overline{f}_{2}$. An example of an anomalous access
pair for the program from in Section 2, is
$(S1,\\{\mathtt{st\\_name}\\},S2,\\{\mathtt{em\\_addr}\\})$ and
$(U1,\\{\mathtt{st\\_name}\\},$ $U2,\\{\mathtt{em\\_addr}\\})$; this pair
contributes to that program’s non-repeatable read anomaly from Figure 2.

We now turn to the development of an automated static repair strategy that
given a program $P$ and a set of anomalous access pairs produces a
semantically equivalent program $P^{\prime}$ with fewer anomalous access
pairs. In particular, we repair programs by _refactoring_ their database
schemas in order to benefit from record-level atomicity guarantees offered by
most databases, without introducing new observable behaviors. We elide the
details of how anomalous access pairs are discovered, but note that existing
tools (Brutschy et al., 2018; Rahmani et al., 2019) can be adapted for this
purpose. Section 6 provides more details about how this works in Atropos.

##  4\. Refactoring of Database Programs

In this section, we establish the soundness properties on the space of
database program refactorings and then introduce our particular choice of
sound refactoring rules.

The correctness of our approach relies on being able to show that each program
transformation maintains the invariant that _at every step in any history of a
refactored program, it is possible to completely recover the state of the
data-store for a corresponding history of the original program_. To establish
this property, we begin by formalizing the notion of a _containment_ relation
between tables.

###  4.1. Database Containment

Consider the tables in Figure 7, which are instances of the schemas from
Section 2. Note that every field of $\mathtt{COURSE}_{0}$ can be computed from
the values of some other field in either the $\mathtt{STUDENT}_{0}$ or
$\mathtt{COURSE\\_ST\\_CNT\\_LOG}_{0}$ tables: $\mathtt{co\\_avail}$
corresponds to the value of the $\mathtt{st\\_co\\_avail}$ field of a record
in $\mathtt{STUDENT}_{0}$, while $\mathtt{co\\_st\\_cnt}$ can be recovered by
summing up the values of the $\mathtt{co\\_cnt\\_log}$ field of the records in
$\mathtt{COURSE\\_ST\\_CNT\\_LOG}_{0}$ whose $\mathtt{co\\_id}$ field has the
same value as the original table.

The containment relation between a table (e.g. $\mathtt{COURSE}_{0}$) and a set of tables (e.g. $\mathtt{STUDENT}_{0}$ and $\mathtt{COURSE\\_ST\\_CNT\\_LOG}_{0}$) is defined using a set of mappings called _value correspondences_ (Wang et al., 2019). A value correspondence captures how to compute a field in the contained table from the fields of the containing set of tables. Formally, a value correspondence between field $f$ of schema $R$ and field $f^{\prime}$ of schema $R^{\prime}$ is defined as a tuple $(R,R^{\prime},f,f^{\prime},\theta,\alpha)$ in which:  (i) a total _record correspondence function_ , denoted by $\theta:R_{\mathtt{id}}\rightarrow\overline{R^{\prime}_{\mathtt{id}}}$, relates every record of any instance of $R$ to a _set_ of records in any instance of $R^{\prime}$ and  (ii) a fold function on values, denoted by $\alpha:\overline{\mathtt{Val}}\rightarrow\mathtt{Val}$ is used to aggregate a set of values.  We say that a table $X$ is contained by a set of tables $\overline{X}$ under a set of value correspondences $V$, if $V$ accurately explains how to compute $X$ from $\overline{X}$, i.e.  X ⊑_V ¯X≡∀f∈X_fld. ∃(R,R’,f,f’,θ,α)∈V. ∃X’ ∈¯X.∀r∈R_id. X(r.f) = α({m | r’∈θ(r)∧X’(r’.f’)=m})

Figure 7. An example illustrating value correspondences.

For example, the table $\mathtt{COURSE}_{0}$ is contained in the set of tables
$\\{\mathtt{STUDENT}_{0},\mathtt{COURSE\\_ST\\_CNT\\_LOG}_{0}\\}$ under the
pair of value correspondences, $(\mathtt{COURSE},$ $\mathtt{STUDENT},$
$\mathtt{co\\_avail},$ $\mathtt{st\\_co\\_avail}$, $\theta_{1},$
$\mathtt{any})$ and $(\mathtt{COURSE},$ $\mathtt{COURSE\\_ST\\_CNT\\_LOG},$
$\mathtt{co\\_st\\_cnt},\mathtt{co\\_cnt\\_log},$ $\theta_{2},\mathtt{sum})$,
where $\theta_{1}(1)=\\{100,200\\}$, $\theta_{1}(2)=\\{300\\}$,
$\theta_{2}(1)=\\{(1,11),(1,33)\\}$ and $\theta_{2}(2)=\\{(2,22)\\}$. The
aggregator function
$\mathtt{any}:\overline{\mathtt{Val}}\rightarrow\mathtt{Val}$ returns a non-
deterministically chosen value from a set of values. The containment relation
on tables is straightforwardly lifted to data store states, denoted by
$\Sigma\sqsubseteq_{V}\Sigma^{\prime}$, if all tables in $\Sigma$ are
contained by the set of tables in $\Sigma^{\prime}$.

We define the soundness of our program refactorings using a pair of
_refinement_ relations between execution histories and between programs. An
execution history $h^{\prime}$ (where
$h^{\prime}_{\mathtt{fin}}=(\Sigma^{\prime},\Gamma^{\prime})$) is a refinement
of an execution $h$ (where $h_{\mathtt{fin}}=(\Sigma,\Gamma)$) if and only if
$\Gamma^{\prime}$ and $\Gamma$ have the same collection of finalized
transaction instances and there is a set of value correspondences $V$ under
which $\Sigma$ is contained in $\Sigma^{\prime}$, i.e.
$\Sigma\sqsubseteq_{V}\Sigma^{\prime}$.

Lastly, we define a refactored program $P^{\prime}$ to be a refinement of the
original program $P$ if the following conditions are satisfied:

  1. (I)

Every history $h^{\prime}$ of $P^{\prime}$ has a corresponding history $h$ in
$P$ such that $h^{\prime}$ is a refinement of $h$.

  2. (II)

Every serializable history $h$ of $P$ has a corresponding history $h^{\prime}$
in $P^{\prime}$ such that $h^{\prime}$ is a refinement of $h$.

The first condition ensures that $P^{\prime}$ does not introduce any new
behaviors over $P$, while the second ensures that $P^{\prime}$ does not remove
any desirable behavior exhibited by $P$.

###  4.2. Refactoring Rules

We describe Atropos’s refactorings using a relation $\xhookrightarrow{}\
\subseteq\overline{V}\times P\times\overline{V}\times P$, between programs and
sets of value correspondences. The rules in Figure 8 are templates of the
three categories of transformations employed by Atropos. These categories are:
(1) adding a new schema to the program, captured by the rule (intro $\rho$);
(2) adding a new field to an existing schema $\rho$, captured by rule (intro
$\rho.f$); and, (3) relocating certain data from one table to another while
modifying the way it is accessed by the program, captured by the rule (intro
$v$).

The refactorings represented by (intro $v$) introduce a new value
correspondence $v$, and modify the body and return expressions of a programs
transactions via a rewrite function, ${[\\![.]\\!]}_{v}$. A particular
instantiation of ${[\\![.]\\!]}_{v}$ must ensure the same data is accessed and
modified by the resulting program, in order to guarantee that the refactored
program refines the original. At a high-level, it is sufficient for
${[\\![\cdot]\\!]}_{v}$ to ensure the following relationship between the
original ($P$) and refactored programs ($P^{\prime}$) :

  * (R1)

$P^{\prime}$ accesses the same data as $P$, which may be maintained by
different schemas;

  * (R2)

$P^{\prime}$ returns the same final value as $P$;

  * (R3)

and, $P^{\prime}$ properly updates all data maintained by $P$.

(intro $\rho$)ρ／∈¯RRelNames¯V,(¯R,¯T)↪¯V,(¯R∪{ρ:∅},¯T) (intro $\rho.f$)R =
ρ:¯ff／∈¯fR’ = ρ:¯f∪{f}¯V,({R}∪¯R,¯T)↪¯V,({R’}∪¯R,¯T)
(intro $v$)v／∈¯V¯T’= { t(¯a){[[c]]v;return [[e]]v} ∣ t(¯a){c;return e}
∈¯T}¯V,(¯R,¯T)↪¯V∪{v},(¯R,¯T’) Figure 8. Refactoring Rules

⬇

1getSt(id):

2 x:=select * from STUDENT where st_id=id//S1

3 y:=select em_addr from EMAIL where em_id=x.st_em_id//S2

4 z:=select co_avail from COURSE where co_id=x.st_co_id//S3

5 return (y.em_addr)

$\xhookrightarrow{\textsc{intro
$(\mathtt{EMAIL},\;\mathtt{STUDENT},\;\mathtt{em\\_addr},\;\mathtt{st\\_em\\_addr},\;\lceil\hat{\theta_{0}}\rceil,\;\mathtt{any})$}}$
⬇ 1getSt(id): 2 x:=select * from STUDENT where st_id=id //S1 3 y:=select
st_em_addr from STUDENT 4 where st_em_id=x.st_em_id //S2’ 5 z:=select co_avail
from COURSE where co_id=x.st_co_id//S3 6 return (y.st_em_addr)

⬇

1setSt(id,name,email):

2 x:=select st_em_id from STUDENT where st_id=id //S4

3 update STUDENT set st_name=name where st_id=id //U1

4 update EMAIL set em_addr=email where em_id=x.st_em_id//U2

5 return 0

$\xhookrightarrow{\textsc{intro
$(\mathtt{EMAIL},\;\mathtt{STUDENT},\;\mathtt{em\\_addr},\;\mathtt{st\\_em\\_addr},\;\lceil\hat{\theta_{0}}\rceil,\;\mathtt{any})$}}$
⬇ 1setSt(id,name,email): 2 x:=select st_em_id from STUDENT where st_id=id //S4
3 update STUDENT set st_name=name where st_id=id //U1 4 update STUDENT set
st_em_addr=email 5 where st_em_id=x.st_em_id //U2’ 6 return 0

Figure 9. A single program refactoring step, where
$\hat{\theta_{0}}(\mathtt{EMAIL.em\\_addr})=\mathtt{STUDENT.st\\_em\\_addr}$

To see how a rewrite function might ensure R1 to R3, consider the original
(top) and refactored (bottom) programs presented in Figure 9. This example
depicts a refactoring of transactions $\mathtt{getSt}$ and $\mathtt{setSt}$ to
utilize a value correspondence from $\mathtt{em\\_addr}$ to
$\mathtt{st\\_em\\_addr}$, moving email addresses to the $\mathtt{STUDENT}$
table, as described in Section 2. The select commands $\mathtt{S1}$ and
$\mathtt{S3}$ in $\mathtt{getS}$ remain unchanged after the refactoring, as
they do not access the affected table. However, the query $\mathtt{S2}$, which
originally accessed the $\mathtt{EMAIL}$ table is redirected to the
$\mathtt{STUDENT}$ table.

More generally, in order to take advantage of a newly added value
correspondence $v$, ${[\\![.]\\!]}_{v}$ must alter every query on the source
table and field in $v$ to use the target table of $v$ instead, so that the new
query accesses the same data as the original. This rewrite has the general
form:

$\begin{array}[]{l}[\\![x\\!:={\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SELECT}\;}f\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{FROM}\;}{R}{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}\phi]\\!]_{v}\equiv\\\
x\\!:={\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SELECT}\;}f^{\prime}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{FROM}\;}{R^{\prime}}\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}\mathtt{redirect}({\phi},v.\theta)\end{array}$

Intuitively, in order for this transformation to ensure R1, the
$\mathtt{redirect}$ function must return a new where clause on the target
table which selects a set of records corresponding to set selected by the
original clause.

In order to preserve R2, program expressions also need to be rewritten to
evaluate to the same value as in the original program. For example, observe
that the $\mathtt{return}$ expression in $\mathtt{getSt}$ is updated to
reflect that the records held in the variable $\mathtt{y}$ now adhere to a
different schema.

The transformation performed in Figure 9 also rewrites the update
($\mathtt{U2}$) of transaction $\mathtt{setSt}$. In this case, the update is
rewritten using the same redirection strategy as ($\mathtt{S2}$), so that it
correctly reflects the updates that would be performed by the original program
to the $\mathtt{EMAIL}$ record.

Taken together, $R1-R3$ are sufficient to ensure that a particular instance of
intro $v$ is sound111A complete formalization of all three refactoring rules,
their correctness criteria, and proofs of soundness is presented in the
supplementary materials of this submission.:

###### Theorem 4.1.

Any instance of intro $v$ whose instantiation of ${[\\![\cdot]\\!]}_{v}$
satisfies $R1-R3$ is always produces a refactored program that is a refinement
of the original.

Although our focus has been on preserving the semantics of refactored
programs, note that as a direct consequence of our definition of program
refinement, this theorem implies that sound transformations do not introduce
any new anomalies.

We now present the instantiations of intro $v$ used by Atropos, explaining
along the way how they ensure R1-R3.

####  4.2.1. The redirect rule

Our first refactoring rule is parameterized over the choice of schemas and
fields and uses the aggregator $\mathtt{any}$. Given data store states
$\Sigma$ and $\Sigma^{\prime}$, the record correspondence is defined as:
$\lceil\hat{\theta}\rceil(r)=\\{r^{\prime}\,\mid\,r^{\prime}\in
R^{\prime}_{\mathtt{id}}\wedge\forall_{f\in
R_{\mathtt{id}}}\forall_{n}.\;\Sigma(r.f)\Downarrow
n\Rightarrow\Sigma^{\prime}(r^{\prime}.\hat{\theta}(f))\Downarrow n\\}$. In
essence, the lifted function $\hat{\theta}$ identifies how the value of the
primary key $f$ of a record $r$ can be used to constrain the value of field
$\hat{\theta}(f)$ in the target schema to recover the set of records
corresponding to $r$, i.e. $\theta(r)$. The record correspondences from
Section 4.1 were defined in this manner, where

$\displaystyle\hat{\theta_{1}}(\mathtt{COURSE.co\\_id})=\mathtt{STUDENT.st\\_co\\_id}\,,\;\;\;\text{and}$
$\displaystyle\hat{\theta_{2}}(\mathtt{COURSE.co\\_id})=\mathtt{COURSE\\_CO\\_ST\\_CNT\\_LOG.co\\_id}.$

Defining the record correspondence this way ensures that if a record $r$ is
selected in $\Sigma$, the corresponding set of records in $\Sigma^{\prime}$
can be determined by identifying the values that were used to select $r$,
without depending on any particular instance of the tables.

The definition of $\mathtt{redirect}$ for this rule is straightforward:
redirect(ϕ,⌈^θ⌉) = ⋀_f∈ϕ_fld this.^θ(f)=ϕ[f]_exp The one wrinkle in this
definition of $\mathtt{redirect}$ is that it is only defined when the where
clause $\phi$ is _well-formed_ , i.e. $\phi$ only consists of conjunctions of
equality constraints on primary key fields. The expression used in such a
constraint is denoted by $\phi[f]_{\mathtt{exp}}$. As an example, the where
clause of command ($\mathtt{S2}$) in Figure 9 (left) is well-formed, where
$\phi[\mathtt{em\\_id}]_{\mathtt{exp}}=\mathtt{x.\mathtt{st}\\_e\\_id}$.
However, the where clause in ($\mathtt{S2}^{\prime}$) after the refactoring
step is not well-formed, since it does not constrain the primary key of the
schema. This restriction ensures only select clauses accessing a single record
of the original table will be rewritten. Expressions using variables
containing the results of those queries are rewritten by substituting the
source field name with the target field name, e.g.
${[\\![\mathtt{at}^{1}(x.f)]\\!]}_{v}\equiv\mathtt{at}^{1}(x.f^{\prime})$.

####  4.2.2. The logger rule

Unfortunately, instantiating intro $v$ is not so straightforward when we want
to utilize value correspondences with more complicated aggregation functions
than $\mathtt{any}$. To see why, consider how we would need to modify an
${\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}$
when $\alpha=\mathtt{sum}$ is used. In this case, our rule transforms the
program to insert _a new record_ corresponding to each update performed by the
original program. Hence, the set of corresponding records in the target table
always grows and cannot be statically identified.

We enable these sorts of transformations by using _logging_ schema for the
target schema. A logging schema for source schema $R$ and the field $f$ is
defined as follows:  (i) the target schema ($LogR$) has a primary key field,
corresponding to every primary key field of the original schema ($R$);  (ii)
the schema has one additional primary key field, denoted by
$LogR.\mathtt{log\\_id}$, which allows a _set_ of records in $LogR$ to
represent each record in $R$; and  (iii) the schema $LogR$ has a single field
corresponding to the original field $R.f$, denoted by $LogR.f^{\prime}$.

Intuitively, a logging schema captures the _history_ of updates performed on a
record, instead of simply replacing old values with new ones. Program-level
aggregators can then be utilized to determine the final value of each record,
by observing all corresponding entries in the logging schema. The schema
$\mathtt{COURSE\\_CO\\_ST\\_CNT\\_LOG}$ from Section 2 is an example of a
logging schema for the source schema and field
$\mathtt{COURSE}.\mathtt{co\\_st\\_cnt}$.

Under these restrictions, we can define an implementation of
${[\\![\cdot]\\!]}$ for the logger rule using $\mathtt{sum}$ as an aggregator.
This refactoring also uses a lifted function $\lceil\hat{\theta}\rceil$ for
its value correspondence, which allows ${[\\![\cdot]\\!]}$ to reuse our
earlier definition of $\mathtt{redirect}$. We define ${[\\![\cdot]\\!]}$ on
accesses to $f$ to use program-level aggregators, e.g.
${[\\![\mathtt{at}^{1}(x.f)]\\!]}_{v}:=\mathtt{sum}(x.f^{\prime})$.

Finally, the rewritten
${\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}$commands
simply need to log any updates to the field $f$, so its original value can be
recovered in the transformed program, e.g.

$\begin{array}[]{l}\\!\\!\\!\\!{[\\![{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}R\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SET}\;}f=e+\mathtt{at}^{1}(x.f)\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}\phi]\\!]}_{v}\;\equiv\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}R^{\prime}\\\
\;\;\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SET}\;}f^{\prime}={[\\![e]\\!]}_{v}{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}\mathtt{redirect}(\phi,v.\theta)\wedge
R^{\prime}.\mathtt{log\\_id}=\mathtt{uuid()}.\end{array}$

Having introduced the particular refactoring rules instantiated in Atropos, we
are now ready to establish the soundness of those refactorings:

###### Theorem 4.2.

(Soundness) Any sequence of refactorings using the rewrite rules described in
this section satisfy the correctness properties R1-R3.

Function : $\mathtt{repair}(P)$ $\overline{\chi}\leftarrow\mathcal{O}(P)$;
$P\leftarrow\mathtt{pre\\_process}(P,\overline{\chi})$ for
_$\chi\in\overline{\chi}$_ do

2 if  _$\mathtt{try\\_repair}(P,\chi)=\;P^{\prime}$_ then $P\leftarrow
P^{\prime}$

3

1 return $\mathtt{post\\_process}(P)$

Function : $\mathtt{try\\_repair}(P,\chi)$ $c_{1}\leftarrow\chi.c_{1}$;
$c_{2}\leftarrow\chi.c_{2}$ if  _$\mathtt{same\\_kind}(c_{1},c_{2})$_ then

2 if  _$\mathtt{same\\_schema}(c_{1},c_{2})$_ then

3 return $\mathtt{try\\_merging}(P,c_{1},c_{2})$

4 else if  _$\mathtt{try\\_redirect}(P,c_{1},c_{2})=\;P^{\prime}$_ then

5 return $\mathtt{try\\_merging}(P^{\prime},c_{1},c_{2})$

6

return $\mathtt{try\\_logging}(P,c_{1},c_{2})$

Figure 10. The repair algorithm

##  5\. Repair Procedure

Figure 10 presents our algorithm for eliminating serializability anomalies
using the refactoring rules from the previous section. The algorithm
($\mathtt{repair}$) begins by applying an anomaly detector $\mathcal{O}$ to a
program to identify a set of anomalous access pairs. As an example, consider
$\mathtt{regSt}$ from our running example. For this transaction, the anomaly
oracle identifies two anomalous access pairs:

($\chi_{1}$)
$\displaystyle\mathtt{(U3,\\{st\\_co\\_id,st\\_reg\\},U4,\\{co\\_avail\\})}$
($\chi_{2}$)
$\displaystyle\mathtt{(S5,\mathtt{\\{co\\_st\\_cnt\\}},\mathtt{U4},\mathtt{\\{co\\_st\\_cnt\\}})}$

The first of these is involved in the dirty read anomaly from Section 2, while
the second is involved in the lost update anomaly.

The repair procedure next performs a preprocessing phase, where database
commands are split into multiple commands such that each command is involved
in at most one anomalous access pair. For example, the first step of repairing
the $\mathtt{regSt}$ transaction is to split command $\mathtt{U4}$ into two
update commands, as shown in Figure 11 (top). Note that we only perform this
step if the split fields are not accessed together in other parts of the
program; this is to ensure that the splitting does not introduce new unwanted
serializability anomalies.

After preprocessing, the algorithm iterates over all detected anomalous access
pairs ($\overline{\chi}$) and attempts to repair them one by one using
$\mathtt{try\\_repair}$. This function attempts to eliminate a given anomaly
in two different ways; either by merging anomalous database commands into a
single command, and/or by removing one of them by making it obsolete. In the
remainder of this section, we present these two strategies in more detail,
using the running example from Figure 11.

⬇

1regSt(id,course):

2 update STUDENT set st_co_id=course,st_reg=true

3 where st_id=id//U3

4 x:=select co_st_cnt from COURSE where co_id=course//S5

5 update COURSE set co_st_cnt=x.co_st_cnt+1

6 where co_id=course//U4.1

7 update COURSE set co_avail=true where co_id=course//U4.2

$\xhookrightarrow{\textsc{intro
$(\mathtt{COURSE},\;\mathtt{STUDENT},\;\mathtt{co\\_avail},\;\mathtt{st\\_co\\_avail},\;\lceil\hat{\theta_{1}}\rceil,\;\mathtt{any})$}}$

⬇

1regSt(id,course):

2 update STUDENT set st_co_id=course,st_reg=true

3 where st_id=id//U3

4 x:=select co_st_cnt from COURSE where co_id=course//S5

5 update COURSE set co_st_cnt=x.co_st_cnt+1

6 where co_id=course//U4.1

7 update STUDENT set st_co_avail=true

8 where st_co_id=course//U4.2’

$\xhookrightarrow{\textsc{Intro}\;\mathtt{COURSE\\_CO\\_ST\\_CNT\\_LOG}}\;\;\ldots$
$\xhookrightarrow{\textsc{Intro}\;(\mathtt{COURSE},\;\mathtt{COURSE\\_ST\\_CNT\\_LOG},\;\mathtt{co\\_st\\_cnt},\;\mathtt{co\\_cnt\\_log},\;\lceil\hat{\theta_{2}}\rceil,\mathtt{sum})}$

⬇

1regSt(id,course):

2 update STUDENT set st_co_id=course, st_reg=true

3 where st_id=id//U3

4 x:=select co_st_cnt from COURSE where co_id=course//S5

5 insert into COURSE_CO_ST_CNT_LOG values

6 (co_id=course,log_id=uuid(),co_st_cnt_log=1)//U4.1’

7 update STUDENT set st_co_avail=true

8 where st_co_id=course//U4.2’

Figure 11. Repair steps of transaction $\mathtt{regSt}$

We first explain the merging approach. Two database commands can only be
merged if they are of the same kind (e.g. both are $\mathtt{selects}$) and if
they both access the same schema. These conditions are checked in lines 2-3.
Function $\mathtt{try\\_merge}$ attempts to merge the commands if it can
establish that their where clauses always select the exact same set of
records, i.e. condition (R1) described in Section 4.2.

Unfortunately, database commands involved in anomalies are rarely on the same
schema and cannot be merged as they originally are. Using the refactoring
rules discussed earlier, Atropos attempts to introduce value correspondences
so that the anomalous commands are redirected to the same table in the
refactored program and thus mergeable. This is captured by the call to the
procedure $\mathtt{try\\_redirect}$. This procedure first introduces a set of
fields into the schema accessed by $c_{1}$, each corresponding a field
accessed by $c_{2}$. Next, it attempts to introduce a sequence of value
correspondences between the two schemas using the redirect rule, such that
$c_{2}$ is redirected to the same table as $c_{1}$. The record correspondence
is constructed by analyzing the commands’ where clauses and identifying
equivalent expressions used in their constraints. If redirection is
successful, $\mathtt{try\\_merge}$ is invoked on the commands and the result
is returned (line 6).

For example, consider commands $\mathtt{U3}$ and $\mathtt{U4.2}$ in Figure 11
(top), which are involved in the anomaly $\chi_{1}$. By introducing a value
correspondence from $\mathtt{COURSE}$ to $\mathtt{STUDENT}$, Atropos refactors
the program into a refined version where $\mathtt{U4.2}$ is transformed into
$\mathtt{U4.2^{\prime}}$ and is mergeable with $\mathtt{U3}$.

Merging is sufficient to fix $\chi_{1}$, but fails to eliminate $\chi_{2}$.
The repair algorithm next tries to translate database updates into an
equivalent insert into a logging table using the $\mathtt{try\\_logging}$
procedure.This procedure first introduces a new logging schema (using the
intro $\rho$ rule) and then introduces fields into that schema (using intro
$\rho.f$). It then attempts to introduce a value correspondence from the
schema involved in the anomaly to the newly introduced schema using the logger
rule. The function returns successfully if such a translation exists and if
the select command involved in the anomaly becomes obsolete, i.e., the command
is dead-code. For example, in Figure 11, a value correspondence from
$\mathtt{COURSE}$ to the logger table $\mathtt{COURSE\\_CO\\_ST\\_CNT}$ is
introduced, which translates the $\mathtt{update}$ command involved in the
anomaly to an $\mathtt{insert}$ command. The select command is obsolete in the
final version, since variable $x$ is never used.

Once all anomalies have been iterated over, Atropos performs a post-processing
phase on the program to remove any remaining dead code and merge commands
whenever possible. For example, the transaction $\mathtt{regSt}$ is refactored
into its final version depicted in Figure 3 after post-processing. Both
anomalous accesses ($\chi_{1}$ and $\chi_{2}$) are eliminated in the final
version of the transaction.

##  6\. Implementation

Atropos is a fully automated static analyzer and program repair tool
implemented in Java. Its input programs are written in a DSL similar to the
one described in Figure 5, but it would be straightforward to extend the
front-end to support popular database programming APIs, e.g. JDBC or Python’s
DB-API. Atropos consists of a static anomaly detection engine and a program
refactoring engine and outputs the repaired program. The static anomaly
detector in Atropos adapts existing techniques to reason about serializability
violations over abstract executions of a database application (Brutschy et
al., 2018; Nagar and Jagannathan, 2018). In this approach, detecting a
serializability violation is reduced to checking the satisfiability of an FOL
formula constructed from the input program. This formula includes variables
for each of the transactional dependencies, as well as the visibility and
global time-stamps that can appear during a program’s execution. The
assignments to these variables in any satisfying model can be used to
reconstruct an anomalous execution. We use an off-the-shelf SMT solver, Z3 (de
Moura and Bjørner, 2008), to check for anomalies in the input program and
identify a set of anomalous access pairs. These access pairs are then used by
an implementation of the repair algorithm build a repaired version of the
input program.

##  7\. Evaluation

This section evaluates Atropos along two dimensions:

  1. (1)

Effectiveness: Does schema refactoring eliminate serializability anomalies in
real-world database applications? Is Atropos capable of repairing meaningful
concurrency bugs?

  2. (2)

Performance: What impact does Atropos have on the performance of refactored
programs? How does Atropos compare to other solutions to eliminating
serializability anomalies, in particular by relying on stronger database-
provided consistency guarantees?

###  7.1. Effectiveness

To assess Atropos’ effectiveness, we applied it to a corpus of standard
benchmarks from the database community, including TPC-C, SEATS and SmallBank
(Brutschy et al., 2018; Difallah et al., 2013; Sivaramakrishnan et al., 2015;
Gotsman et al., 2016; Rahmani et al., 2019). Table 1 presents the results for
each benchmark. The first four columns display the number of transactions
(#Txns), the number of tables in the original and refactored schemas
(#Tables), and the number of anomalies detected assuming eventually consistent
guarantees for the original (EC) and refactored (AT) programs. For each
benchmark, Atropos was able to repair at least half the anomalies, and in many
cases substantially more, suggesting that many serializability bugs can be
directly repaired by our schema refactoring technique.

In order to compare our approach to other means of anomaly elimination –
namely, by merely strengthening the consistency guarantees provided by the
underlying database – we modified Atropos’s anomaly oracle to only consider
executions permitted under causal consistency and repeatable read; the former
enforces causal ordering in the visibility relation, while the latter prevents
results of a newly committed transaction $T$ becoming visible to an executing
transaction that has already read state that is written by $T$. The next two
columns of Table 1, (CC) and (RR), show the result of this analysis: causal
consistency was only able to reduce the number of anomalies in one benchmark
(by 12%) and repeatable read in three (by 5%, 15% and 16%). This suggests that
only relying on isolation guarantees between eventual and sequential
consistency is not likely to significantly reduce the number of concurrency
bugs that manifest in an EC execution.

As a final measure of Atropos’s impact on correctness, we carried out a more
in-depth analysis of the SmallBank benchmark, in order to understand Atropos’s
ability to repair meaningful concurrency bugs. This benchmark maintains the
details of customers and their accounts, with dedicated tables holding
checking and savings entries for each customer. By analyzing this and similar
banking applications from the literature (Gotsman et al., 2016; Kaki et al.,
2018a; Warszawski and Bailis, 2017), we identified three invariants to be
preserved by each transaction222Detailed descriptions of each invariant can be
found in the supplementary materials of our submission: Interestingly, we were
able to detect violations of _all three_ invariants in the original program
under EC, while the repaired program violated _only one_. This is evidence
that the statically identified serializability anomalies eliminated by Atropos
are meaningful proxies to the application-level invariants that developers
care about.

Benchmark | #Txns |  #Tables | EC | AT | CC | RR |  Time (s)
---|---|---|---|---|---|---|---
TPC-C (TPC, 2020; Kaki et al., 2019) | 5 | 9, 16 | 33 | 8 | 33 | 33 | 81.2
SEATS (Difallah et al., 2013; Stonebraker and Pavlo, 2012) | 6 | 8, 12 | 35 | 10 | 35 | 33 | 61.5
Courseware (Gotsman et al., 2016; Kaki et al., 2018b) | 5 | 3, 2 | 5 | 0 | 5 | 5 | 12.7
SmallBank (Difallah et al., 2013; Sivaramakrishnan et al., 2015) | 6 | 3, 5 | 24 | 8 | 21 | 20 | 68.7
Twitter (Difallah et al., 2013) | 5 | 4, 5 | 6 | 1 | 6 | 5 | 3.6
FMKe (Tomás et al., 2017) | 7 | 7, 9 | 6 | 2 | 6 | 6 | 33.6
SIBench (Difallah et al., 2013) | 2 | 1, 2 | 1 | 0 | 1 | 1 | 0.3
Wikipedia (Difallah et al., 2013) | 5 | 12, 13 | 2 | 1 | 2 | 2 | 9.0
Killrchat (kil, Doan; Brutschy et al., 2018) | 5 | 3, 4 | 6 | 3 | 6 | 6 | 42.9
Table 1. Statically identified anomalous access pairs in the original and
refactored benchmark programs. Time (s) holds the total time to analyze and
repair each benchmark.

(a) SmallBank

(b) SEATS

(c) TPC-C

Figure 12. Performance evaluation of SmallBank, SEATS and TPC-C benchmarks
running on US cluster (see the supplementary materials for results of
experiments on other two clusters).

###  7.2. Performance

To evaluate the performance impact of schema refactoring, we conducted further
experiments on a real-world geo-replicated database cluster, consisting of
three AWS machines (M10 tier with 2 vCPUs and 2GB of memory) located across US
in N. Virginia, Ohio and Oregon. Similar results were exhibited by experiments
on a single data center and globally distributed clusters; see supplementary
materials for more details. Each node runs MongoDB (v.4.2.9), a modern
document database management system that supports a variety of data-model
design options and consistency enforcement levels. MongoDB documents are
equivalent to records and a collection of documents is equivalent to a table
instance, making all our techniques applicable to MongoDB clients.

Figure 12 presents the latency (top) and throughput (bottom) of concurrent
executions of SmallBank (left), SEATS (middle) and TPC-C (right) benchmarks.
These benchmarks are representative of the kind of OLTP applications best
suited for our refactoring approach. Horizontal axes show the number of
clients, where each client repeatedly submits transactions to the database
according to each benchmark’s specification. Each experiment was run for 90
seconds and the average performance results are presented. For each benchmark,
performance of four different versions of the program are compared:  (i)
original version running under EC ($\blacklozenge$ EC),  (ii) refactored
version running under EC ($\blacksquare$ AT-EC),  (iii) original version
running under SC (● SC) and  (iv) refactored version where transactions with
at least one anomaly are run under SC and the rest are run under EC
($\blacktriangle$ AT-SC)  . Across all benchmarks, SC results in poor
performance compared to EC, due to lower concurrency and additional
synchronization required between the database nodes. On the other hand, AT-EC
programs show negligible overhead with respect to their EC counterparts,
despite having fewer anomalies. Most interestingly, refactored programs show
an average of 120% higher throughput and 45% lower latency compared to their
counterparts under SC, while offering the _same level of safety_. These
results provide evidence that automated schema refactoring can play an
important role in improving both the correctness and performance of modern
database programs.

##  8\. Related Work

Wang et al. (2019) describe a synthesis procedure for generating programs
consistent with a database refactoring, as determined by a verification
procedure that establishes database program equivalence (Wang et al., 2017).
Their synthesis procedure performs enumerative search over a template whose
structure is derived by value correspondences extracted by reasoning over the
structure of the original and refactored schemas. Our approach has several
important differences. First, our search for a target program is driven by
anomalous access pairs that identify serializability anomalies in the original
program and does not involve enumerative search over the space of _all_
equivalent candidate programs. This important distinction eliminates the need
for generating arbitrarily-complex templates or sketches. Second, because we
_simultaneously_ search for a target schema and program consistent with that
schema given these access pairs, our technique does not need to employ
conflict-driven learning (Feng et al., 2018) or related mechanisms to guide a
general synthesis procedure as it recovers from a failed synthesis attempt.
Instead, value correspondences derived from anomalous access pairs help define
a restricted class of schema refactorings (e.g., aggregation and logging) that
directly informs the structure of the target program.

Identifying serializability anomalies in database systems is a well-studied
topic that continues to garner attention (Berenson et al., 1995; Bernstein et
al., 1987; Lu et al., 2004; Fekete, 2005; Jorwekar et al., 2007), although the
issue of automated repair is comparatively less explored. A common approach in
all these techniques is to model interactions among concurrently executing
database transactions as a graph, with edges connecting transactions that have
a data dependency with one another; cycles in the graph indicate a possible
serializability violation. Both dynamic (Warszawski and Bailis, 2017; Brutschy
et al., 2017) and static (Brutschy et al., 2018; Nagar and Jagannathan, 2018;
Rahmani et al., 2019) techniques have been developed to discover these
violations in various domains and settings.

An alternative approach to eliminating serializability anomalies is to develop
correct-by-construction methods. For example, to safely develop applications
for eventually-consistent distributed environments, conflict-free replicated
data-types (CRDTs) (Shapiro et al., 2011) have been proposed. CRDTs are
abstract data-types (e.g. sets, counters) equipped with commutative operations
whose semantics are invariant with respect to the order in which operations
are applied on their state. Alternatively, there have been recent efforts
which explore enriching specifications, rather than applications, with
mechanisms that characterize notions of correctness in the presence of
replication (Houshmand and Lesani, 2019; Sivaramakrishnan et al., 2015), using
these specifications to guide safe implementations. These techniques, however,
have not been applied to reasoning on the correctness of concurrent relational
database programs which have highly-specialized structure and semantics,
centered on table-based operations over inter-related schema definitions,
rather than control- and data-flow operations over a program heap.

##  9\. Conclusions

This paper presents Atropos, a database refactoring tool intended to repair
serializability violations. We have formalized the refactoring procedure and
demonstrated experimental results that schema refactoring is a viable strategy
for concurrency bug repair in modern database applications.

## References

  * (1)
  * TPC (2020) 2020\.  TPC-C Benchmark.  http://www.tpc.org/tpc_documents_current_versions/pdf/tpc-c_v5.11.0.pdf.  Online; Accessed April 2020.
  * kil (Doan) DuyHai Doan.  KillrChat, a scalable chat with Cassandra, AngularJS & Spring Boot.  https://github.com/doanduyhai/killrchat.  Online; Accessed October 2020.
  * Ambler (2006) Scott Ambler. 2006\.  _Refactoring databases : evolutionary database design_.  Addison Wesley, Upper Saddle River, NJ.
  * Bacon et al. (2017) David F. Bacon, Nathan Bales, Nico Bruno, Brian F. Cooper, Adam Dickinson, Andrew Fikes, Campbell Fraser, Andrey Gubarev, Milind Joshi, Eugene Kogan, Alexander Lloyd, Sergey Melnik, Rajesh Rao, David Shue, Christopher Taylor, Marcel van der Holst, and Dale Woodford. 2017.  Spanner: Becoming a SQL System. In _Proceedings of the 2017 ACM International Conference on Management of Data_ (Chicago, Illinois, USA) _(SIGMOD ’17)_. Association for Computing Machinery, New York, NY, USA, 331–343.  https://doi.org/10.1145/3035918.3056103
  * Bailis et al. (2013) Peter Bailis, Aaron Davidson, Alan Fekete, Ali Ghodsi, Joseph M. Hellerstein, and Ion Stoica. 2013\.  Highly Available Transactions: Virtues and Limitations.  _PVLDB_ 7, 3 (2013), 181–192.  http://www.vldb.org/pvldb/vol7/p181-bailis.pdf
  * Bailis et al. (2014a) Peter Bailis, Alan Fekete, Michael J. Franklin, Ali Ghodsi, Joseph M. Hellerstein, and Ion Stoica. 2014a.  Coordination Avoidance in Database Systems.  _Proc. VLDB Endow._ 8, 3 (Nov. 2014), 185–196.  https://doi.org/10.14778/2735508.2735509
  * Bailis et al. (2014b) Peter Bailis, Alan Fekete, Joseph M. Hellerstein, Ali Ghodsi, and Ion Stoica. 2014b.  Scalable Atomic Visibility with RAMP Transactions. In _Proceedings of the 2014 ACM SIGMOD International Conference on Management of Data_ (Snowbird, Utah, USA) _(SIGMOD ’14)_. ACM, New York, NY, USA, 27–38.  https://doi.org/10.1145/2588555.2588562
  * Berenson et al. (1995) Hal Berenson, Philip A. Bernstein, Jim Gray, Jim Melton, Elizabeth J. O’Neil, and Patrick E. O’Neil. 1995.  A Critique of ANSI SQL Isolation Levels. In _Proceedings of the 1995 ACM SIGMOD International Conference on Management of Data, San Jose, California, May 22-25, 1995._ 1–10.  https://doi.org/10.1145/223784.223785
  * Bernstein and Das (2013) Philip A. Bernstein and Sudipto Das. 2013.  Rethinking Eventual Consistency. In _Proceedings of the 2013 ACM SIGMOD International Conference on Management of Data_ (New York, New York, USA) _(SIGMOD ’13)_. ACM, New York, NY, USA, 923–928.  https://doi.org/10.1145/2463676.2465339
  * Bernstein and Goodman (1983) Philip A. Bernstein and Nathan Goodman. 1983.  Multiversion Concurrency Control - Theory and Algorithms.  _ACM Trans. Database Syst._ 8, 4 (Dec. 1983), 465–483.  https://doi.org/10.1145/319996.319998
  * Bernstein et al. (1987) Philip A. Bernstein, Vassco Hadzilacos, and Nathan Goodman. 1987\.  _Concurrency Control and Recovery in Database Systems_.  Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA.
  * Brutschy et al. (2017) Lucas Brutschy, Dimitar Dimitrov, Peter Müller, and Martin T. Vechev. 2017.  Serializability for Eventual Consistency: Criterion, Analysis, and Applications. In _Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017_. 458–472.  http://dl.acm.org/citation.cfm?id=3009895
  * Brutschy et al. (2018) Lucas Brutschy, Dimitar Dimitrov, Peter Müller, and Martin T. Vechev. 2018.  Static Serializability Analysis for Causal Consistency. In _Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018_. 90–104.  https://doi.org/10.1145/3192366.3192415
  * Burckhardt (2014) Sebastian Burckhardt. 2014\.  Principles of Eventual Consistency.  _Foundations and Trends® in Programming Languages_ 1, 1-2 (2014), 1–150.
  * Burckhardt et al. (2014) Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski. 2014.  Replicated Data Types: Specification, Verification, Optimality. In _Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (San Diego, California, USA) _(POPL ’14)_. ACM, New York, NY, USA, 271–284.  https://doi.org/10.1145/2535838.2535848
  * Corbett et al. (2012) James C. Corbett, Jeffrey Dean, Michael Epstein, Andrew Fikes, Christopher Frost, J. J. Furman, Sanjay Ghemawat, Andrey Gubarev, Christopher Heiser, Peter Hochschild, Wilson Hsieh, Sebastian Kanthak, Eugene Kogan, Hongyi Li, Alexander Lloyd, Sergey Melnik, David Mwaura, David Nagle, Sean Quinlan, Rajesh Rao, Lindsay Rolig, Yasushi Saito, Michal Szymaniak, Christopher Taylor, Ruth Wang, and Dale Woodford. 2012\.  Spanner: Google’s Globally-distributed Database. In _Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation_ (Hollywood, CA, USA) _(OSDI’12)_. USENIX Association, Berkeley, CA, USA, 251–264.  http://dl.acm.org/citation.cfm?id=2387880.2387905
  * de Moura and Bjørner (2008) Leonardo de Moura and Nikolaj Bjørner. 2008.  Z3: An Efficient SMT Solver. In _Tools and Algorithms for the Construction and Analysis of Systems_ , C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 337–340.
  * Difallah et al. (2013) Djellel Eddine Difallah, Andrew Pavlo, Carlo Curino, and Philippe Cudre-Mauroux. 2013.  OLTP-Bench: An Extensible Testbed for Benchmarking Relational Databases.  _Proc. VLDB Endow._ 7, 4 (Dec. 2013), 277–288.  https://doi.org/10.14778/2732240.2732246
  * Eswaran et al. (1976) K. P. Eswaran, J. N. Gray, R. A. Lorie, and I. L. Traiger. 1976\.  The Notions of Consistency and Predicate Locks in a Database System.  _Commun. ACM_ 19, 11 (Nov. 1976), 624–633.  https://doi.org/10.1145/360363.360369
  * Faroult (2008) Stephane Faroult. 2008\.  _Refactoring SQL applications_.  O’Reilly Media, Sebastopol, Calif.
  * Fekete (2005) Alan Fekete. 2005\.  Allocating isolation levels to transactions. In _Proceedings of the Twenty-fourth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 13-15, 2005, Baltimore, Maryland, USA_. 206–215.  https://doi.org/10.1145/1065167.1065193
  * Feng et al. (2018) Yu Feng, Ruben Martins, Osbert Bastani, and Isil Dillig. 2018\.  Program Synthesis Using Conflict-Driven Learning. In _Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Philadelphia, PA, USA) _(PLDI 2018)_. Association for Computing Machinery, New York, NY, USA, 420–435.  https://doi.org/10.1145/3192366.3192382
  * Fowler (2019) Martin Fowler. 2019\.  _Refactoring : improving the design of existing code_.  Addison-Wesley, Boston.
  * Garcia-Molina et al. (2008) Hector Garcia-Molina, Jeffrey D. Ullman, and Jennifer Widom. 2008\.  _Database Systems: The Complete Book_ (2 ed.).  Prentice Hall Press, Upper Saddle River, NJ, USA.
  * Gotsman et al. (2016) Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro. 2016.  ’Cause I’m Strong Enough: Reasoning about Consistency Choices in Distributed Systems. In _Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016_. 371–384.  https://doi.org/10.1145/2837614.2837625
  * Houshmand and Lesani (2019) Farzin Houshmand and Mohsen Lesani. 2019.  Hamsaz: Replication Coordination Analysis and Synthesis.  _PACMPL_ 3, POPL (2019), 74:1–74:32.  https://dl.acm.org/citation.cfm?id=3290387
  * Jorwekar et al. (2007) Sudhir Jorwekar, Alan Fekete, Krithi Ramamritham, and S. Sudarshan. 2007.  Automating the Detection of Snapshot Isolation Anomalies. In _Proceedings of the 33rd International Conference on Very Large Data Bases, University of Vienna, Austria, September 23-27, 2007_. 1263–1274.  http://www.vldb.org/conf/2007/papers/industrial/p1263-jorwekar.pdf
  * Kaki et al. (2018a) Gowtham Kaki, Kapil Earanky, KC Sivaramakrishnan, and Suresh Jagannathan. 2018a.  Safe Replication Through Bounded Concurrency Verification.  _Proc. ACM Program. Lang._ 2, OOPSLA, Article 164 (Oct. 2018), 27 pages.  https://doi.org/10.1145/3276534
  * Kaki et al. (2018b) Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, and Suresh Jagannathan. 2018b.  Alone Together: Compositional Reasoning and Inference for Weak Isolation.  _PACMPL_ 2, POPL (2018), 27:1–27:34.  https://doi.org/10.1145/3158115
  * Kaki et al. (2019) Gowtham Kaki, Swarn Priya, KC Sivaramakrishnan, and Suresh Jagannathan. 2019.  Mergeable Replicated Data Types.  _Proc. ACM Program. Lang._ 3, OOPSLA, Article 154 (Oct. 2019), 29 pages.  https://doi.org/10.1145/3360580
  * Lakshman and Malik (2010) Avinash Lakshman and Prashant Malik. 2010.  Cassandra: A Decentralized Structured Storage System.  _SIGOPS Operating Systems Review_ 44, 2 (April 2010), 35–40.  https://doi.org/10.1145/1773912.1773922
  * Li et al. (2012) Cheng Li, Daniel Porto, Allen Clement, Johannes Gehrke, Nuno Preguiça, and Rodrigo Rodrigues. 2012.  Making Geo-replicated Systems Fast As Possible, Consistent when Necessary. In _Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation_ (Hollywood, CA, USA) _(OSDI’12)_. USENIX Association, Berkeley, CA, USA, 265–278.  http://dl.acm.org/citation.cfm?id=2387880.2387906
  * Lloyd et al. (2013) Wyatt Lloyd, Michael J. Freedman, Michael Kaminsky, and David G. Andersen. 2013.  Stronger Semantics for Low-Latency Geo-Replicated Storage. In _Proceedings of the 10th USENIX Conference on Networked Systems Design and Implementation_ (Lombard, IL) _(nsdi’13)_. USENIX Association, USA, 313–328.
  * Lu et al. (2004) Shiyong Lu, Arthur Bernstein, and Philip Lewis. 2004\.  Correct Execution of Transactions at Different Isolation Levels.  _IEEE Transactions on Knowledge and Data Engineering_ 16, 9 (2004), 1070–1081.
  * MySQL (2020) MySQL 2020.  Transaction Isolation Levels.  https://dev.mysql.com/doc/refman/5.6/en/innodb-transaction-isolation-levels.html Accessed: 2020-01-1 10:00:00.
  * Nagar and Jagannathan (2018) Kartik Nagar and Suresh Jagannathan. 2018.  Automated Detection of Serializability Violations Under Weak Consistency. In _29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China_. 41:1–41:18.  https://doi.org/10.4230/LIPIcs.CONCUR.2018.41
  * Papadimitriou (1979) Christos H. Papadimitriou. 1979\.  The Serializability of Concurrent Database Updates.  _J. ACM_ 26, 4 (Oct. 1979), 631–653.  https://doi.org/10.1145/322154.322158
  * PostgreSQL (2020) PostgreSQL 2020.  Transaction Isolation.  https://www.postgresql.org/docs/9.1/static/transaction-iso.html Accessed: 2020-01-1 10:00:00.
  * Rahmani et al. (2018) Kia Rahmani, Gowtham Kaki, and Suresh Jagannathan. 2018\.  Fine-grained Distributed Consistency Guarantees with Effect Orchestration. In _Proceedings of the 5th Workshop on the Principles and Practice of Consistency for Distributed Data_ (Porto, Portugal) _(PaPoC ’18)_. ACM, New York, NY, USA, Article 6, 5 pages.  https://doi.org/10.1145/3194261.3194267
  * Rahmani et al. (2019) Kia Rahmani, Kartik Nagar, Benjamin Delaware, and Suresh Jagannathan. 2019.  CLOTHO: Directed Test Generation for Weakly Consistent Database Systems.  _Proc. ACM Program. Lang._ 3, OOPSLA, Article 117 (Oct. 2019), 28 pages.  https://doi.org/10.1145/3360543
  * Schultz et al. (2019) William Schultz, Tess Avitabile, and Alyson Cabral. 2019\.  Tunable Consistency in MongoDB.  _Proc. VLDB Endow._ 12, 12 (Aug. 2019), 2071–2081.  https://doi.org/10.14778/3352063.3352125
  * Shapiro et al. (2011) Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski. 2011.  Conflict-Free Replicated Data Types.  In _Stabilization, Safety, and Security of Distributed Systems_ , Xavier Défago, Franck Petit, and Vincent Villain (Eds.). Lecture Notes in Computer Science, Vol. 6976. Springer Berlin Heidelberg, 386–400.  https://doi.org/10.1007/978-3-642-24550-3_29
  * Sivaramakrishnan et al. (2015) KC Sivaramakrishnan, Gowtham Kaki, and Suresh Jagannathan. 2015\.  Declarative Programming over Eventually Consistent Data Stores. In _Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Portland, OR, USA) _(PLDI 2015)_. ACM, New York, NY, USA, 413–424.  https://doi.org/10.1145/2737924.2737981
  * Sovran et al. (2011) Yair Sovran, Russell Power, Marcos K. Aguilera, and Jinyang Li. 2011.  Transactional Storage for Geo-replicated Systems. In _Proceedings of the 23 rd ACM Symposium on Operating Systems Principles_ (Cascais, Portugal) _(SOSP ’11)_. ACM, New York, NY, USA, 385–400.  https://doi.org/10.1145/2043556.2043592
  * Stonebraker and Pavlo (2012) Michael Stonebraker and Andy Pavlo. 2012.  The SEATS Airline Ticketing Systems Benchmark.  http://hstore.cs.brown.edu/projects/seats
  * Tomás et al. (2017) Gonçalo Tomás, Peter Zeller, Valter Balegas, Deepthi Akkoorath, Annette Bieniusa, João Leitão, and Nuno Preguiça. 2017.  FMKe: A Real-World Benchmark for Key-Value Data Stores. In _Proceedings of the 3rd International Workshop on Principles and Practice of Consistency for Distributed Data_ (Belgrade, Serbia) _(PaPoC ’17)_. Association for Computing Machinery, New York, NY, USA, Article 7, 4 pages.  https://doi.org/10.1145/3064889.3064897
  * Wang et al. (2017) Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook. 2017.  Verifying Equivalence of Database-driven Applications.  _Proc. ACM Program. Lang._ 2, POPL, Article 56 (Dec. 2017), 29 pages.  https://doi.org/10.1145/3158144
  * Wang et al. (2019) Yuepeng Wang, James Dong, Rushi Shah, and Isil Dillig. 2019\.  Synthesizing Database Programs for Schema Refactoring. In _Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Phoenix, AZ, USA) _(PLDI 2019)_. ACM, New York, NY, USA, 286–300.  https://doi.org/10.1145/3314221.3314588
  * Warszawski and Bailis (2017) Todd Warszawski and Peter Bailis. 2017.  ACIDRain: Concurrency-Related Attacks on Database-Backed Web Applications. In _Proceedings of the 2017 ACM International Conference on Management of Data_ (Chicago, Illinois, USA) _(SIGMOD ’17)_. ACM, New York, NY, USA, 5–20.  https://doi.org/10.1145/3035918.3064037
  * Zellag and Kemme (2014) Kamal Zellag and Bettina Kemme. 2014.  Consistency Anomalies in Multi-tier Architectures: Automatic Detection and Prevention.  _The VLDB Journal_ 23, 1 (Feb. 2014), 147–172.  https://doi.org/10.1007/s00778-013-0318-x

##  Appendix A Complete Evaluation Results

In this section we present additional evaluation results omitted from the
paper.

###  A.1. Performance on Global and Local Database Clusters

Figures 13, 14 and 15 present our experimental results from running SmallBank,
SEATS and TPC-C benchmark on three different distributed database clusters.
Results for US cluster (middle) are also presented in the paper. The VA
cluster (left) consists of three AWS nodes all located in the same data center
in N. Virginia. The global cluster (right) consists of three nodes located in
N. Virgina, London and Tokyo. As we mentioned in the paper, M10 tier machines
with 2 vCPUs and 2GB memory are used and each node runs MongoDB (v.4.2.9).

Figure 13. Performance evaluation of SmallBank benchmark

Figure 14. Performance evaluation of SEATS benchmark

Figure 15. Performance evaluation of TPC-C benchmark

###  A.2. Application-Level Invariants

We ran further experiments on the SmallBank benchmark. This benchmark has six
transactions which maintain the details of customers and their accounts.
Specifically, each customer is assigned a checking entry and a savings entry
in dedicated tables. By analysing this benchmark and similar banking
applications from the literature, we defined the following application-level
invariants which should be preserved after the execution of any transaction:

  1. (1)

The checking and saving balance of accounts must always be non-negative,

  2. (2)

Each account must reflect the correct total amounts based on the history of
deposits performed on that account,

  3. (3)

Each client must always witness a consistent state of her checking and savings
accounts. For example, when transferring money from one to the other, users
must not witness an intermediate state where the money is deducted from the
checking account, but is not deposited into savings.

###  A.3. Comparison with Random Refactoring

We investigated the utility of using the results of our oracle to drive our
repair procedure. For these experiments we removed the initial phase of
analysis and instead randomly introduced tables and fields and prescribed
value correspondences between them. The results of these experiments for the
three benchmarks with the highest number of anomalies is presented in Figure
16. Each experiment was repeated for 5 hours, where at each round of
experiments 10 random refactorings were applied in the program. Each red dot
in Figure 16 records the number of anomalies at the end of each round of
(random) refactoring; the blue line is the number of anomalies in the repaired
program produced by Atropos. In our experiments, the vast majority of random
refactorings did not eliminate _any_ of the anomalies. Even those experiments
that managed to repair some anomalies still resulted in a program with many
more serializability bugs than that returned by Atropos’s oracle-guided repair
strategy.

Figure 16. Number of anomalous access pairs in randomly refactored programs

Definition of  $\Sigma(r.f)$: Given a database state
$\Sigma=(\mathtt{str},\mathtt{vis},\mathtt{cnt})$, a primary key $r\in R_{id}$
and a field $f$, we define $\Sigma(r.f)$ as follows:

$\Sigma(r.f)=v\Leftrightarrow\exists\eta\in\mathtt{str}.\eta_{r}=r\wedge\eta_{f}=f\wedge\eta_{v}=v\wedge(\forall\eta^{\prime}\in\mathtt{str}.\eta^{\prime}_{r}=r\wedge\eta^{\prime}_{f}=f\Rightarrow\eta^{\prime}_{\tau}\leq\eta_{\tau})$

Given a program $P$ and a value correspondence $v=$ $(R,R^{\prime},$
$f,f^{\prime},\theta,\alpha)$, let $\mathcal{V}^{\mathtt{id}}_{v,P}$ be the
set containing all identity value correspondences for all fields of all
relations of $P$ except the fields $f,f^{\prime}$ and the value correspondence
$v$. The notation also generalizes for a set of value correspondences $V$
(i.e. $\mathcal{V}^{\mathtt{id}}_{V,P}$ is the union of the set of all
identity value correspondences for all fields of all relations of $P$ except
the fields which are source and target fields in $V$, and the set of the value
correspondence $V$). In accordance with the definitions in the paper, here we
define a containment relation between sets of records as follows:

$\displaystyle X\sqsubseteq_{V}$ $\displaystyle X^{\prime}~{}~{}\equiv~{}~{}$
$\displaystyle\forall(R,R^{\prime},f,f^{\prime},\theta,\alpha)\in V.\;\forall
r\in R_{\mathtt{id}}.\;r\in X_{id}\Leftrightarrow$ $\displaystyle\theta(r)\cap
X^{\prime}_{\mathtt{id}}\neq\emptyset\wedge$ $\displaystyle
X(r.f)=\alpha(\\{m\,|\,r^{\prime}\in\theta(r)\cap
X^{\prime}_{\mathtt{id}}~{}\wedge~{}X^{\prime}(r^{\prime}.f^{\prime})=m\\})$

We begin the proofs by formalizing ${[\\![.]\\!]}$ and $R1-R3$ requirements in
more detail. The transformation on select commands is defined as follows:
[[c]]_v = (x:= SELECT f’ FROM R’ WHERE redirect(v, ϕ,)), where the function
$\mathtt{redirect}:v\times\phi\rightarrow\phi$ satisfies the following
constraint:

(R1)

$\footnotesize\frac{\begin{array}[]{c}r\in
R_{\mathtt{id}}\qquad\Sigma\sqsubseteq_{\mathcal{V}^{\mathtt{id}}_{v,P}}\Sigma^{\prime}\qquad\Delta\sqsubseteq_{\mathcal{V}^{\mathtt{id}}_{v,P}}\Delta^{\prime}\end{array}}{\begin{array}[]{c}r\in\Sigma_{\mathtt{id}}\wedge\Delta,\phi(\Sigma(r))\Downarrow\mathtt{true}\Leftrightarrow\theta(r)\cap\\{r^{\prime}\in
R^{\prime}_{\mathtt{id}}\,|\,r^{\prime}\in\Sigma^{\prime}\wedge\\\
\Delta^{\prime},{\mathtt{redirect}(v,\phi)}(\Sigma^{\prime}(r^{\prime}))\Downarrow\mathtt{true}\\}\neq\emptyset\wedge\\\
\Sigma(r.f)=\alpha(\\{\Sigma^{\prime}(r^{\prime}.f^{\prime})\ |\
r^{\prime}\in\theta(r)\wedge\Delta^{\prime},{\mathtt{redirect}(v,\phi)}(\Sigma^{\prime}(r^{\prime}))\Downarrow\mathtt{true}\\})\end{array}}$

(R2)

$\footnotesize\frac{\begin{array}[]{c}\Delta\sqsubseteq_{\mathcal{V}^{\mathtt{id}}_{v,P}}\Delta^{\prime}\par\end{array}}{\begin{array}[]{c}\Delta,e\Downarrow
n\Leftrightarrow\Delta^{\prime},{[\\![e]\\!]}_{v}\Downarrow n\end{array}}$

The redirect function takes a value correspondence and a WHERE clause, and
returns another WHERE clause. The rule (R1) ensures that if the database state
$\Sigma$ and local state $\Delta$ are contained inside $\Sigma^{\prime}$ and
$\Delta^{\prime}$ respectively, then the output of SELECT query in the
original program must be contained in the output of the SELECT query in the
refactored program. A sufficient condition for this is that for every record
$r$ in $\Sigma$ which satisfies the original WHERE clause $\phi$ (expressed as
$\Delta,\phi(\Sigma(r))\Downarrow\mathtt{true}$), there must be records in
$\theta(r)$ that satisfy the new WHERE clause (that is returned by
$redirect$), and that the values in the selected fields in the original record
$r$ can be determined using the records in $\theta(r)$.

The rule (R2) simply says that if the local database state $\Delta$ is
contained inside $\Delta^{\prime}$, then any expression $e$ on $\Delta$ or
$\Delta^{\prime}$ must evaluate to the same value.

For any command
$c={\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}R\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SET}\;}f=e\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}\phi$
in the original program, which is affected by the newly added
$v=(R,R^{\prime},f,f^{\prime},\theta,\alpha)$, the refactored command is given
by:

(1)
${[\\![c]\\!]}_{v}:={\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}R^{\prime}\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SET}\;}f^{\prime}=\\\
\mathtt{duplicate}(e,v)\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}\mathtt{duplicate}(\phi,v)$

The refactored command must satisfy the following property:

(R3)

$\footnotesize\frac{\begin{array}[]{c}\Sigma\sqsubseteq_{\mathcal{V}^{\mathtt{id}}_{v,P}}\Sigma^{\prime}\qquad\Delta\sqsubseteq_{\mathcal{V}^{\mathtt{id}}_{v,P}}\Delta^{\prime}\qquad\Sigma^{\prime},\Delta^{\prime},\llbracket
c\rrbracket_{v}\rightarrow\Sigma^{\prime\prime},\Delta^{\prime},\mathtt{skip}\qquad
r\in
R_{\mathtt{id}}\end{array}}{\begin{array}[]{c}r\in\Sigma_{\mathtt{id}}\wedge\Delta,\phi(\Sigma(r))\Downarrow\mathtt{true}\Leftrightarrow\\{r^{\prime}\in
R^{\prime}_{\mathtt{id}}\ |\
r^{\prime}\in\Sigma^{\prime}_{\mathtt{id}}\wedge\\\
\Delta^{\prime},\mathtt{duplicate}(\phi,v)(\Sigma(r^{\prime}))\Downarrow\mathtt{true}\\}\cap\theta(r)\neq\emptyset\\\
\Delta,e\Downarrow
n\Leftrightarrow\alpha(\\{\Sigma^{\prime\prime}(r^{\prime}.f^{\prime})\,|\,r^{\prime}\in\theta(r)\wedge
r^{\prime}\in\Sigma^{\prime\prime}_{\mathtt{id}}\\})=n\end{array}}$

The rule (R3) states that if the database state $\Sigma$ and local state
$\Delta$ are contained inside $\Sigma^{\prime}$ and $\Delta^{\prime}$
respectively, and if the execution of the refactored UPDATE leads to the new
database state $\Sigma^{\prime\prime}$refactored program executes the UPDATE
statement, then for every record $r$ whose field $f$ is modified by the
original UPDATEprogram (modified to the valuation of the expression $e$),
there must be records in $\theta(r)$ which must be modified by the refactored
UPDATE, and that the modification in the original UPDATE (i.e. value of
expression $e$) can be determined from the modified records obtained after the
execution of the refactored UPDATE. This ensures that the original UPDATE is
preserved by the refactored UPDATE.

  * (comm)

$\begin{array}[]{llcl}(1)&{[\\![c;c^{\prime}]\\!]}_{v}&\coloneqq&{[\\![c]\\!]}_{v};{[\\![c^{\prime}]\\!]}_{v}\\\
(2)&{[\\![\mathtt{skip}]\\!]}_{v}&\coloneqq&\mathtt{skip}\\\
(3)&{[\\![\mathtt{iterate}(e)\\{c\\}]\\!]}_{v}&\coloneqq&(4)\mathtt{iterate}({[\\![e]\\!]}_{v})\\{{[\\![c]\\!]}_{v}\\}\\\
(5)&{[\\![\mathtt{if}(e)\\{c\\}]\\!]}_{v}&\coloneqq&\mathtt{if}({[\\![e]\\!]}_{v})\\{{[\\![c]\\!]}_{v}\\}\\\
\end{array}$

  * (whc)

$\begin{array}[]{llcl}(6)&{[\\![\phi\circ\phi^{\prime}]\\!]}_{v}&\coloneqq&{[\\![\phi]\\!]}_{v}\circ{[\\![\phi^{\prime}]\\!]}_{v}\\\
(7)&{[\\![\mathtt{this}.f\odot
e]\\!]}_{v}&\coloneqq&\mathtt{this}.f\odot{[\\![e]\\!]}_{v}\\\ \end{array}$

  * (exp)

$\begin{array}[]{llcl}(8)&{[\\![\mathtt{at}^{e}(x.f^{\prime\prime})]\\!]}_{v}&\coloneqq&\mathtt{at}^{{[\\![e]\\!]}_{v}}(x.f^{\prime\prime})\\\
(9)&{[\\![\mathtt{agg}(x.f^{\prime\prime})]\\!]}_{v}&\coloneqq&\mathtt{agg}(x.f^{\prime\prime})\\\
(10)&{[\\![n]\\!]}_{v}&\coloneqq&n\\\ (11)&{[\\![a]\\!]}_{v}&\coloneqq&a\\\
(12)&{[\\![e\oplus
e^{\prime}]\\!]}_{v}&\coloneqq&{[\\![e]\\!]}_{v}\oplus{[\\![e^{\prime}]\\!]}_{v}\\\
(13)&{[\\![e\odot
e^{\prime}]\\!]}_{v}&\coloneqq&{[\\![e]\\!]}_{v}\odot{[\\![e^{\prime}]\\!]}_{v}\\\
(14)&{[\\![e\circ
e^{\prime}]\\!]}_{v}&\coloneqq&{[\\![e]\\!]}_{v}\circ{[\\![e^{\prime}]\\!]}_{v}\\\
(15)&{[\\![\mathtt{iter}]\\!]}_{v}&\coloneqq&\mathtt{iter}\\\ \end{array}$

  * (select)

$\begin{array}[]{llcl}(16)&{[\\![x:=\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SELECT}\;}f^{\prime\prime}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{FROM}\;}{R}\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}{\phi}]\\!]}_{v}&\coloneqq&(x:=\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SELECT}\;}{f^{\prime\prime}}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{FROM}\;}{R}\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}{[\\![\phi]\\!]}_{v})\\\
(17)&{[\\![x:=\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SELECT}\;}f^{\prime\prime}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{FROM}\;}{R^{\prime\prime}}\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}{\phi}]\\!]}_{v}&\coloneqq&(x:=\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SELECT}\;}{f^{\prime\prime}}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{FROM}\;}{R^{\prime\prime}}\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}{[\\![\phi]\\!]}_{v})\end{array}$

  * (update)

$\begin{array}[]{llcl}(19)&{[\\![{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}R\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SET}\;}f^{\prime\prime}=e\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}\phi]\\!]}_{v}&\coloneqq&{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}R\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SET}\;}f^{\prime\prime}={[\\![e]\\!]}_{v}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}{[\\![\phi]\\!]}_{v}\\\
(20)&{[\\![{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}R^{\prime\prime}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SET}\;}f^{\prime\prime}=e\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}\phi]\\!]}_{v}&\coloneqq&{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}R^{\prime\prime}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SET}\;}f^{\prime\prime}={[\\![e]\\!]}_{v}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}{[\\![\phi]\\!]}_{v}\\\
\end{array}$

Figure 17. Transformations triggered by a new value correspondence
$v=(R,R^{\prime},f,f^{\prime},\theta,\alpha)$

###### Lemma A.1.

Given a program $P$, let $v=(R,R^{\prime},f,f^{\prime},\theta,\alpha)$ be a
value correspondence and let $V=\mathcal{V}^{\mathtt{id}}_{v,P}$. Then, if
$(V_{1},P)\hookrightarrow_{\textsc{v}}(V_{1}\cup\\{v\\},P^{\prime})$ and the
refactoring semantics is equipped with the correct rewriting rules - which
satisfy $R1$, $R2$ and $R3$, then $P^{\prime}\preceq_{V}P$.

###### Proof.

First we will show that for all histories $h^{\prime}\in H(P^{\prime})$, there
exists a history $h\in H(P)$ such that
$h^{\prime}\preceq_{\mathcal{V}^{\mathtt{id}}_{v,P}}h$. Given $h^{\prime}$,
the history $h$ is constructed by instantiating the same transactions as those
in $h$ in the same order with the same arguments. Further, each command
$\llbracket c\rrbracket_{v}$ of $P^{\prime}$ executed in $h^{\prime}$
corresponds to command $c$ of P. Hence, to construct the history $h$, we will
execute the corresponding command for every execution step of $h^{\prime}$.
Formally, for a step $\Sigma^{\prime}_{1},\Delta^{\prime}_{1},\llbracket
c\rrbracket_{v}\rightarrow\Sigma^{\prime}_{2},\Delta^{\prime}_{2},\llbracket
c^{\prime}\rrbracket_{v}$ in the history $h^{\prime}$, we will perform the
step $\Sigma_{1},\Delta_{1},c\rightarrow\Sigma_{2},\Delta_{2},c^{\prime}$. We
will show that the following invariant is maintained at every step:
$\Sigma_{2}\sqsubseteq_{V}\Sigma_{2}^{{}^{\prime}}$, and
$\Delta_{2}\sqsubseteq_{V}\Delta_{2}^{{}^{\prime}}$. We will use induction on
the number of steps in the history $h^{\prime}$ (which is same as the number
of steps in history $h$).

Base Case: In the beginning, both $\Sigma^{\prime}$ and $\Delta^{\prime}$ are
empty. The first step in both $h$ and $h^{\prime}$ is necessarily the
application of the rule txn-invoke, which invokes an instance of some
transaction $t$ in both $h$ and $h^{\prime}$ with the same argument. Hence,
after this step, both $\Sigma^{\prime},\Delta^{\prime}$ and $\Sigma,\Delta$
continue to remain empty and so the invariant holds trivially.

Inductive Case: Assume that the step
$\Sigma_{1}^{{}^{\prime}},\Delta_{1}^{{}^{\prime}},\llbracket
V,c_{1}\rrbracket_{v}\rightarrow\Sigma_{2}^{{}^{\prime}},\Delta_{2}^{{}^{\prime}},\llbracket
V,c_{2}\rrbracket_{v}$ is performed in history $h^{\prime}$ and the step
$\Sigma_{1},\Delta_{1},c\rightarrow\Sigma_{2},\Delta_{2},c^{\prime}$ is
performed in the history $h$. By the inductive hypothesis,
$\Sigma_{1}\sqsubseteq_{V}\Sigma_{1}^{{}^{\prime}}$, and
$\Delta_{1}\sqsubseteq_{V}\Delta_{1}^{{}^{\prime}}$. We case split based on
the type of step taken:

txn-ret: For a return expression $e$, by $(R2)$, since
$\Delta_{1}\sqsubseteq_{V}\Delta_{1}^{{}^{\prime}}$, if
$\Delta_{1}^{{}^{\prime}},{[\\![e]\\!]}_{v}\Downarrow n$, then
$\Delta_{1},e\Downarrow n$. In this case, the corresponding transaction
instances in $h$ and $h^{\prime}$ return the same value $n$. Further,
$\Sigma_{2}^{{}^{\prime}}=\Sigma_{1}^{{}^{\prime}}$,
$\Delta_{2}^{{}^{\prime}}=\Delta_{1}^{{}^{\prime}}$ and
$\Sigma_{2}=\Sigma_{1}$, $\Delta_{2}=\Delta_{1}$ and hence the invariant
continues to hold. By similar reasoning, steps cond-t, cond-f, iter will also
preserve the invariant.

select: We further case-split based on whether the $SELECT$ accesses the
source field $f$ of the value correspondence $v$ or not. First, let us
consider the case where the $SELECT$ accesses a different field. WLOG, let the
command executed by $h^{\prime}$ be
${[\\![x:=\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SELECT}\;}f^{\prime\prime}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{FROM}\;}{R^{\prime\prime}}\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}{\phi}]\\!]}_{v}$.

This is defined to be the command

$x:=\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SELECT}\;}{f^{\prime\prime}}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{FROM}\;}{R^{\prime\prime}}\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}{[\\![\phi]\\!]}_{v}$

. In $h^{\prime}$, using the rule consistent-view, a view of the data store
$\Sigma^{{}^{\prime}*}\sqsubseteq\Sigma_{1}^{{}^{\prime}}$ will be generated.
Since the command accesses fields which are different from $f$, there are
identity value correspondences for all the accessed fields in $V$, and since
$\Sigma_{1}\sqsubseteq_{V}\Sigma_{1}^{{}^{\prime}}$, all the write events to
fields accessed by the command in store $\Sigma_{1}^{{}^{\prime}}$ will also
be present in $\Sigma_{1}$. Hence, there exists a view
$\Sigma^{*}\sqsubseteq\Sigma_{1}$ which contains the same write events to
fields accessed by the command as $\Sigma^{{}^{\prime}*}$. Finally, since
$\Delta_{1}\sqsubseteq_{V}\Delta_{1}^{{}^{\prime}}$, by $(R2)$ all expressions
$e$ present in the where clause $\phi$ will evaluate to same value in $h$ and
$h^{\prime}$. Hence, the same records will satisfy the where clauses
${[\\![\phi]\\!]}_{v}$ and $\phi$, leading to the same selection of records
and hence the same binding to $x$, thus preserving
$\Delta_{2}(x)\sqsubseteq_{V}\Delta_{2}^{{}^{\prime}}(x)$.

Now, let us consider the case where the command executed by $h^{\prime}$ is

${[\\![V,x:=\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SELECT}\;}f\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{FROM}\;}{R}\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}{\phi}]\\!]}_{v}$

. This is defined to be the command

$x:=\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SELECT}\;}{f^{\prime}}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{FROM}\;}{R^{\prime}}\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}{\color[rgb]{0.0390625,0.0390625,0.90234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.0390625,0.0390625,0.90234375}\mathtt{redirect}(V,{[\\![\phi]\\!]}_{v},v)}$

. In $h^{\prime}$, using the rule consistent-view, a view of the data store
$\Sigma^{{}^{\prime}*}\sqsubseteq\Sigma_{1}^{{}^{\prime}}$ will be generated
to determine the records which satisfy the $WHERE$ clause
$\mathtt{redirect}(V,{[\\![\phi]\\!]}_{v},v)$. Since
$\Sigma_{1}\sqsubseteq_{V}\Sigma_{1}^{{}^{\prime}}$, for any record which
satisfies $\mathtt{redirect}(V,{[\\![\phi]\\!]}_{v},v)$ and which is present
in $\Sigma_{1}^{{}^{\prime}}$, it corresponding record according to the value
correspondence will also be present in $\Sigma_{1}$. Hence, we can construct a
view of the data store $\Sigma^{*}\sqsubseteq\Sigma_{1}$ such that all fields
of all records accessed in the $WHERE$ clause evaluate to the same value, i.e.
$\Sigma^{*}\sqsubseteq\Sigma^{{}^{\prime}*}$. Now, by $(R1)$, it is guaranteed
that if records $\theta(r)$ are selected by $h^{\prime}$, then the record $r$
must be selected by $h$. Further, since
$\Sigma_{1}\sqsubseteq_{V}\Sigma_{1}^{{}^{\prime}}$ and $V$ includes the value
correspondence $v$, the value of $f$ in the selected record in $h$ will
satisfy the value correspondence $v$ w.r.t. the records $\theta(r)$ selected
in $h^{\prime}$. Hence,
$\Delta_{2}(x)\sqsubseteq_{V}\Delta_{2}^{{}^{\prime}}(x)$.

update: We case split based on whether the $UPDATE$ command modifies the
source field $f$. First, let us consider the case where the $UPDATE$ modifies
a different field. WLOG, let the command executed by $h$ be
${[\\![{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}R^{\prime\prime}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SET}\;}f^{\prime\prime}=e\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}\phi]\\!]}_{v}$.
This is defined to be the command
${\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}R^{\prime\prime}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SET}\;}f^{\prime\prime}={[\\![e]\\!]}_{v}\;{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}{[\\![\phi]\\!]}_{v}$.

In $h^{\prime}$, using the rule consistent-view, a view of the data store
$\Sigma^{{}^{\prime}*}\sqsubseteq\Sigma_{1}^{{}^{\prime}}$ will be generated.
Since the command accesses fields in the $WHERE$ clause which are different
from $f$, there are identity value correspondences for all the accessed fields
in $V$, and since $\Sigma_{1}\sqsubseteq_{V}\Sigma_{1}^{{}^{\prime}}$, all the
write events to the accessed fields in store $\Sigma_{1}^{{}^{\prime}}$ will
also be present in $\Sigma_{1}$. Hence, there exists a view
$\Sigma^{*}\sqsubseteq\Sigma_{1}$ which contains the same write events to the
accessed fields as present in $\Sigma^{{}^{\prime}*}$. This guarantees that
the same set of records in $R^{\prime\prime}$ will be selected by the $WHERE$
clauses in $h$ and $h^{\prime}$ .Finally, since
$\Delta_{1}\sqsubseteq_{V}\Delta_{1}^{{}^{\prime}}$, by $(R2)$, the
expressions ${[\\![V,e]\\!]}_{v}$ and $e$ will evaluate to the same value.
Hence, write events to the same field in the same set of records and writing
the same value will be generated in $h$ and $h^{\prime}$. This guarantees that
$\Sigma_{2}\sqsubseteq_{V}\Sigma_{2}^{{}^{\prime}}$.

Now, let us consider the case where the command executed by $h^{\prime}$ is

$\llbracket{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}R\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SET}\;}f=e\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}\phi\rrbracket_{v}$

. This is defined to be the command
${\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{UPDATE}\;}R^{\prime}\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{SET}\;}f^{\prime}=\mathtt{duplicate}(e,v)\
{\color[rgb]{0,0,0.62890625}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.62890625}\mathtt{WHERE}\;}\mathtt{duplicate}(\phi,v)$.
n $h^{\prime}$, using the rule consistent-view, a view of the data store
$\Sigma^{{}^{\prime}*}\sqsubseteq\Sigma_{1}^{{}^{\prime}}$ will be generated
to determine the records which satisfy the $WHERE$ clause
$\mathtt{duplicate}(\phi,v)$. Since
$\Sigma_{1}\sqsubseteq_{V}\Sigma_{1}^{{}^{\prime}}$, if $\theta(r)$ is present
in $\Sigma_{1}^{{}^{\prime}}$, then $r$ would also be present in $\Sigma_{1}$.
Hence, we can construct a corresponding view $\Sigma*\sqsubseteq\Sigma_{1}$
such that $\Sigma*\sqsubseteq_{V}\Sigma^{{}^{\prime}*}$. Now, $(R3)$
guarantees that if any record in $\theta(r)$ is updated by $h^{\prime}$, then
the corresponding record $r$ would also be updated by $h$ (since it would
satisfy the original $WHERE$ clause $\phi$). Further, $(R3)$ also guarantees
the update $\mathtt{duplicate}(e,v)$ in $h^{\prime}$ would satisfy the value
correspondence with the update in $h$. Hence, after the update
$\Sigma_{2}\sqsubseteq_{V}\Sigma_{2}^{{}^{\prime}}$.

Note that the proof that for every serial execution of $P$, there exists an
execution of $P^{\prime}$ would follow the exact same pattern as above. In
fact, we would actually construct a serial execution of $P^{\prime}$ which
would have the same behavior as the execution of $P$. ∎

###### Lemma A.2.

Given programs $P_{1}$, $P_{2}$ and $P_{3}$, a set of value-correspondences
$V$ and a value correspondence $v$ such that the source and target fields of
$v$ are not involved in any value correspondence in $V$, if
$P_{2}\preceq_{\mathcal{V}^{\mathtt{id}}_{V,P_{1}}}P_{1}$ and
$P_{3}\preceq_{\mathcal{V}^{\mathtt{id}}_{v,P_{2}}}P_{2}$, then
$P_{3}\preceq_{\mathcal{V}^{\mathtt{id}}_{V\cup\\{v\\},P_{1}}}P_{1}$.

###### Proof.

We are given $H_{1}:P_{2}\preceq_{\mathcal{V}^{\mathtt{id}}_{V,P_{1}}}P_{1}$
and $H_{2}:P_{3}\preceq_{\mathcal{V}^{\mathtt{id}}_{v,P_{2}}}P_{2}$. First we
will show that for all histories $h\in H(P_{3})$, there exists a history
$h^{\prime\prime}\in H(P_{1})$ such that
$h\preceq_{\mathcal{V}^{\mathtt{id}}_{V\cup\\{v\\},P_{1}}}h^{\prime\prime}$.
Let $h_{fin}=(\Sigma,\Gamma)$. By hypothesis $H_{2}$, there exists a history
$h^{\prime}\in H(P_{2})$, $h^{\prime}=(\Sigma^{\prime},\Gamma^{\prime})$ such
that $\Gamma=\Gamma^{\prime}$. By hypothesis $H_{1}$, there exists a history
$h^{\prime\prime}\in H(P_{1})$,
$h^{\prime\prime}=(\Sigma^{\prime\prime},\Gamma^{\prime\prime})$ such that
$\Gamma^{\prime\prime}=\Gamma^{\prime}$. Hence,
$\Gamma^{\prime\prime}=\Gamma$.

Now, by $H_{2}$,
$H_{3}:\Sigma^{\prime}\sqsubseteq_{\mathcal{V}^{\mathtt{id}}_{v,P_{2}}}\Sigma$,
and by $H_{1}$, we have
$H_{4}:\Sigma^{\prime\prime}\sqsubseteq_{\mathcal{V}^{\mathtt{id}}_{V,P_{1}}}\Sigma^{\prime}$.
We will show that
$\Sigma^{\prime\prime}\sqsubseteq_{\mathcal{V}^{\mathtt{id}}_{V\cup\\{v\\},P_{1}}}$.

Consider a value correspondence $u\in V$, such that
$u=(R,R^{\prime},f,f^{\prime},\theta,\alpha)$. Let $r\in R_{\mathtt{id}}$.
Suppose $r\in\Sigma^{\prime\prime}_{\mathtt{id}}$. Then, by $H_{4}$,
$\theta(r)\subseteq\Sigma^{\prime}_{\mathtt{id}}$. Now, since $f^{\prime}$ is
a field of $P_{2}$ which is not involved in value correspondence $v$, there
exists an identity value correspondence
$u^{\prime}\in\mathcal{V}^{\mathtt{id}}_{v,P_{2}}$, such that
$u^{\prime}=(R^{\prime},R^{\prime},f^{\prime},f^{\prime},\mathtt{id},\mathtt{id})$.
Hence, by $H_{3}$, we have $\theta(r)\subseteq\Sigma_{\mathtt{id}}$. In the
other direction, suppose $\theta(r)\subseteq\Sigma_{\mathtt{id}}$. Then, by
$H_{3}$, we have $\theta(r)\subseteq\Sigma^{\prime}_{\mathtt{id}}$, and hence
by $H_{2}$, we have $r\in\Sigma^{\prime\prime}_{\mathtt{id}}$.

Now, by $H_{4}$, $\Sigma^{\prime\prime}(r.f)=\alpha(\\{m\ |\
r^{\prime}\in\theta(r)\wedge\Sigma^{\prime}(r^{\prime}.f^{\prime})=m\\})$. By
$H_{3}$ and the existence of the value correspondence $u^{\prime}$, we have
$\Sigma^{\prime}(r^{\prime}.f^{\prime})=\Sigma(r^{\prime}.f^{\prime})$. Thus,
$\Sigma^{\prime\prime}(r.f)=\alpha(\\{m\ |\
r^{\prime}\in\theta(r)\wedge\Sigma(r^{\prime}.f^{\prime})=m\\})$.

Consider the value correspondence $v$ itself. Let

$v=(R,R^{\prime},f,f^{\prime},\theta,\alpha)$

. Since $f$ is not involved in any value correspondence in $V$, there exists
an identity value correspondence
$v^{\prime}=(R,R,f,f,\mathtt{id},\mathtt{id})$ such that
$v^{\prime}\in\mathcal{V}^{\mathtt{id}}_{V,P_{1}}$. Let $r\in
R_{\mathtt{id}}$. Suppose $r\in\Sigma^{\prime\prime}_{\mathtt{id}}$. Then by
$H_{4}$, $r\in Sigma^{\prime}_{\mathtt{id}}$. By $H_{3}$,
$\theta(r)\in\Sigma_{\mathtt{id}}$. The other direction is straightforward.

Now, by $H_{3}$, $\Sigma^{\prime}(r.f)=\alpha(\\{m\ |\
r^{\prime}\in\theta(r)\wedge\Sigma(r^{\prime}.f^{\prime})=m\\})$. By $H_{4}$,
$\Sigma^{\prime\prime}(r.f)=\Sigma^{\prime}(r.f)$.

Hence, $\Sigma^{\prime\prime}(r.f)=\alpha(\\{m\ |\
r^{\prime}\in\theta(r)\wedge\Sigma(r^{\prime}.f^{\prime})=m\\})$.

Finally, consider an identity value correspondence in
$\mathcal{V}^{\mathtt{id}}_{V\cup\\{v\\},P_{1}}$ whose source field is neither
in $V$ or in $v$. Then, this value correspondence is present in both
$\mathcal{V}^{\mathtt{id}}_{V,P_{1}}$ and
$\mathcal{V}^{\mathtt{id}}_{v,P_{2}}$. Hence, by $H_{3}$ and $H_{4}$, this
value correspondence will also be preserved between $\Sigma^{\prime\prime}$
and $\Sigma$. Hence,
$\Sigma^{\prime\prime}\sqsubseteq{\mathcal{V\cup\\{v\\}}^{\mathtt{id}}_{V,P_{1}}}\Sigma$.
Thus,
$h\preceq_{\mathcal{V}^{\mathtt{id}}_{V\cup\\{v\\},P_{1}}}h^{\prime\prime}$.

Now we will show that for all histories $h^{\prime\prime}\in
H(P_{1})_{\mathtt{ser}}$, there exists a history $h\in
H(P_{3})_{\mathtt{ser}}$ such that
$h\preceq_{\mathcal{V}^{\mathtt{id}}_{V\cup\\{v\\},P_{1}}}h^{\prime\prime}$.
Let $h^{\prime\prime}_{fin}=(\Sigma^{\prime\prime},\Gamma^{\prime\prime})$,
such that $h^{\prime\prime}\in H(P_{1})_{\mathtt{ser}}$. By hypothesis
$H_{1}$, there exists a history $h^{\prime}\in H(P_{2})_{\mathtt{ser}}$,
$h^{\prime}=(\Sigma^{\prime},\Gamma^{\prime})$ such that
$\Gamma^{\prime\prime}=\Gamma^{\prime}$ and
$\Sigma^{\prime\prime}\sqsubseteq_{\mathcal{V}^{\mathtt{id}}_{V,P_{1}}}\Sigma^{\prime}$.
By hypothesis $H_{2}$, there exists a history $h\in H(P_{3})_{\mathtt{ser}}$,
$h=(\Sigma,\Gamma)$ such that $\Gamma^{\prime}=\Gamma$ and
$\Sigma^{\prime}\sqsubseteq_{\mathcal{V}^{\mathtt{id}}_{v,P_{2}}}\Sigma$.
Hence, $\Gamma^{\prime\prime}=\Gamma$, and
$\Sigma^{\prime\prime}\sqsubseteq{\mathcal{V\cup\\{v\\}}^{\mathtt{id}}_{V,P_{1}}}\Sigma$.
Thus,
$h\preceq_{\mathcal{V}^{\mathtt{id}}_{V\cup\\{v\\},P_{1}}}h^{\prime\prime}$. ∎

###### Theorem A.3.

The refactoring semantics equipped with correct rewriting rules - which
satisfy $R1$, $R2$ and $R3$ \- is sound, i.e.
$\forall_{P,P^{\prime}}.\;\emptyset,P\hookrightarrow^{*}V,P^{\prime}\Rightarrow
P^{\prime}\preceq_{\mathcal{V}^{\mathtt{id}}_{V,P}}P$.

###### Proof.

Note that in order to express the result more formally, we have introduced new
notation in the Appendix which has resulted in a slight change in the theorem
statement from the main text of the paper. However, both statements signify
the same result, since $V^{\prime}$ used in the main text is actually the set
of value correspondences introduced by the refactoring rules (same as $V$ in
the above statement), and $\mathcal{V}^{\mathtt{id}}_{V,P}$ contains $V$.

We first assume that all additions to the schema (either new relations or new
fields) are carried out first using the rules intro $\rho$ and intro $\rho.f$.
These rules do not change the program, and since the original program $P$ is
guaranteed to not access the new additions, it is clear that the statement of
the theorem continues to hold after the above sequence of refactorings. Let
$\mathtt{Fld}_{o}$ be the set of all fields in the original program, and
$\mathtt{Fld}_{n}$ be the set of newly added fields. The rest of refactoring
steps will involve multiple applications of the intro $v$ rule. That is,

$(\emptyset,P)\hookrightarrow_{v_{1}}(\\{v_{1}\\},P_{1})\ldots\hookrightarrow_{v_{n}}(V,P_{n})$

where $v_{1},\ldots,v_{n}$ are the value correspondences that are introduced.
We assume that the source field $f_{i}$ of every $v_{i}$ is a field of the
original program i.e. $f_{i}\in\mathtt{Fld}_{o}$ and the target field is a
newly added field. We also assume that the no two value correspondences have
the same source field or the same target field. Let
$V=\\{v_{1},\ldots,v_{n}\\}$. We will show that
$P_{n}\preceq_{\mathcal{V}^{\mathtt{id}}_{V,P}}P$. We will use induction on
the number of refactoring steps ($n$).

Base Case: For the first step, by applying Lemma B.1,
$P_{1}\preceq_{\mathcal{V}^{\mathtt{id}}_{v_{1},P_{1}}}P$.

Inductive Case: Assume that after $k$ steps,
$P_{k}\preceq_{\mathcal{V}^{\mathtt{id}}_{V_{k},P_{1}}}P$, where
$V_{k}=\\{v_{1},\ldots,v_{k}\\}$. For the $(k+1)$th step
$(V_{k},P_{k})\hookrightarrow_{v_{k+1}}(V^{\prime},P_{k+1})$. Then, by Lemma
B.1, $P_{k+1}\preceq_{\mathcal{V}^{\mathtt{id}}_{v_{k+1},P_{k}}}P_{k}$. Now,
by Lemma B.2,
$P_{k+1}\preceq_{\mathcal{V}^{\mathtt{id}}_{V_{k}\cup\\{v_{k+1}\\},P_{1}}}P_{1}$.
∎

###### Theorem A.4.

The rewrite rules described in this section (i.e. by (I1.1), (I1.2), (I2.1),
(I2.2), (I3.1) and (I3.2)) satisfy the correctness properties (R1), (R2) and
(R3).

###### Proof.

We will first show that (I1.1) satisfies (R1). We are given a value
correspondence $v=(R,R^{\prime},f,f^{\prime},\theta,\alpha)$. Let
$V=\mathcal{V}^{\mathtt{id}}_{v,P}$. The value correspondence $v$ satisfies
the property that $\alpha=\mathtt{any}$ and $\theta$ selects records in
$R^{\prime}$ based only equality predicates on all the primary-key fields of
$R$. Assume that each primary key field $p\in R_{\mathtt{pk}}$ is equated with
expression $e_{p}$ in the where clause $\phi$. Given
$\Sigma,\Sigma^{\prime},\Delta,\Delta^{\prime}$ such that
$\Sigma\sqsubseteq\Sigma^{\prime}$ and $\Delta\sqsubseteq\Delta^{\prime}$,
consider $r\in R_{\mathtt{id}}$. Assume that $\Delta,e_{p}\Downarrow n_{p}$.
By (R2), we have $\Delta,e_{p}\Downarrow n_{p}$. Suppose
$r\in\Sigma_{\mathtt{id}}$.

$\displaystyle\Delta,\phi(\Sigma(r))\Downarrow\mathtt{true}$
$\displaystyle\Rightarrow\bigwedge_{p\in R_{\mathtt{pk}}}\Sigma(r.p)=n_{p}$

This in turn implies that $\theta(r)=\\{r^{\prime}\ |\ r^{\prime}\in
R^{\prime}_{\mathtt{id}}\wedge\forall p\in
R_{\mathtt{pk}}.\Sigma^{\prime}(r^{\prime}.\hat{\theta}(p))=n_{p}\\}$. Since
$\Sigma\sqsubseteq_{V}\Sigma^{\prime}$, at least one such record in
$\theta(r)$ is also present in $\Sigma^{\prime}$. Now, by definition of
$\mathtt{redirect}(v,\phi)$,

$\displaystyle
r^{\prime}\in\Sigma^{\prime}\wedge\Delta^{\prime},{\mathtt{redirect}(v,\phi)}(\Sigma^{\prime}(r^{\prime}))\Downarrow\mathtt{true}\\}\Rightarrow\bigwedge_{p\in
R_{\mathtt{pk}}}\Sigma^{\prime}(r^{\prime}.\hat{\theta}(p))=n_{p}$

We have just shown that at least one such record is guaranteed to be present
in $\Sigma^{\prime}$, and hence the intersection of $\theta(r)$ and above set
is non-empty. To prove the reverse direction, we follow the same steps in
reverse order. Since $\mathtt{redirect}$ picks exactly the records which
satisfy the above condition, the containment relation
$\Sigma\sqsubseteq_{V}\Sigma^{\prime}$ guarantees that
$\Sigma^{\prime}(r^{\prime}.f^{\prime})=\Sigma(r.f)$. This completes the proof
that (I1.1) satisfies (R1).

Now we will show that (I2.1) satisfies (R2). Consider the simple expression
$e=\mathtt{at}^{1}(x.f)$. Since $\Delta(x)\sqsubseteq\Delta^{\prime}(x)$,
there exists at least one record bound to $x$ in $\Delta^{\prime}$. Further,
the value at field $f^{\prime}$ in this record must be equal to the value at