Dr Bengt Jonsson

Dr Ilya Sergey

Dr Mihaela Sighireanu

Dr Noam Rinetzky

Dr Viktor Vafeiadis Bengt

Mohamed Sidi

Berk Beil- Lahi

Suha Orhun Cirisci

Mutluergil

Biswas

Krishnapada Paik

Subhajit, Mouli, Sanchari, Kanchan, Sougata, Abhishek Arpita Poulomi

Keywords: Formal Methods, Concurrency, Distributed Systems, Databases, Automated Testing, Weak Consistency, Replicated Data Types, Transactions, Isolation Levels, Complexity iii Méthodes formelles, Concurrence, Systèmes distribués, Bases de données, Teste automatisé, Cohérence faible, Types de données répliqués, Transactions, Complexité. iv ], or linearizability [, ]

As internet grows to be cheaper and faster, distributed software systems and applications are becoming more and more ubiquitous. Today they are the backbone of a large number of online services like banking, e-commerce, social networking, etc. As the popularity of these softwares increases, it is very important that they ensure strong levels of reliability and security.

Modern distributed software is centered around using large-scale storage systems for storing and retrieving data. To ensure persistence and availability of data in the presence of failures, these systems maintain data in multiple copies that are stored on di erent nodes in the network. Then, for performance reasons, these copies are allowed to (temporarily) diverge, an instance of the socalled weak-consistency, which makes the semantics of concurrent accesses to data quite complex.

Over the recent years, many solutions for implementing weakly-consistent storage systems have been proposed. These implementations are most often very complex and error-prone. The speci c levels of weak consistency they ensure are most often described only informally, which makes it di cult to reason about them. Moreover, in many cases, there are signi cant discrepancies between the guarantees claimed in their documentation and the guarantees that they really provide.

The objective of this dissertation is to propose algorithmic techniques for automated testing of weakly-consistent distributed systems against formal specifications. We focus on an important class of distributed data types, called Conflict-Free Replicated Data Types (CRDT s for short), that include many variations like registers, ags, sets, arrays, etc., and on Transactional Systems (Databases), which enable computations on shared data that are isolated from other concurrent computations and resilient to failures. We introduce formal speci cations for such systems and investigate the asymptotic complexity of checking whether a given execution conforms to such speci cations. We also study the problem of testing applications that run on top of weakly-consistent transactional systems, introducing an mock in-memory storage system that simulates the behaviors of such systems according to their formal speci cations.

CRDTs are data types designed to favor availability over consistency by replicating the type instances across multiple nodes of a network, and allowing di erent nodes to temporarily have di erent views of the same instance. However, CRDTs guarantee that the di erent states of the multiple nodes will eventually converge to a unique state common to all nodes [ , ]. Importantly, this convergence property is intrinsic to the data type design and in general no synchronization is needed among nodes, hence achieving availability.

A client, i.e. a program issuing calls to a data type instance, connects to any node holding a copy of the instance, called replica, and performs the operation in that replica. The state of the instance is read only at that replica, and if the state needs to be changed as part of the operation, an update is generated, which will be asynchronously propagated to all the other replicas. When updates eventually reach all replicas, they may be received in di erent orders by di erent replicas. To ensure convergence, con icts between concurrent updates need to be resolved. This is quite non-trivial and an important source of complexity.

For instance, Figure . pictures an execution of a CRDT called OR-Set [ ], a set data type with standard add(_), remove(_), contains(_) operations. add(_) and remove(_) are the only update operations. Two updates are in con ict if they are trying to insert or remove the same element, and possible con icts are resolved by assuming that an add(_) operation will always "win" among multiple con icting concurrent updates, i.e., it will overwrite their e ect. In Figure . , each replica executes the rst two add operations in isolation (without being aware of operations on the other replica), receives the rst add update from the other replica, and executes a remove operation before receiving the second add update from the other replica (as mentioned above, updates are propagated to other replicas asynchronously). The element b, resp., a, is again a member of the set on the top replica, resp., bottom replica, after receiving the last add update because the latter is concurrent (not causally related) to the remove on the receiving replica and the con ict is resolved by assuming that the add wins. This is witnessed by the last two contains operations on each replica that both return true. Note that this execution is an instance of weak consistency since the return values of the contains operations cannot be explained using an interleaving of these operations (consistent with the order between operations on the same replica) as in classic variations of strong consistency, e.g., sequential consistency [ ] or linearizability[ ].

In this thesis we study the tractability of checking whether an execution of a CRDT conforms to the intended speci cation for di erent classes of data types; Figure . summarizes some of our trating example, consider the Payment procedure in Figure . to be executed by two di erent processes. If we allow the internal read and write operations to be interleaved, we can have a scenario where both reads happen before a write. This would allow a user to pay € while his balance decreases only by € . Executing the code of Payment as a transaction can disable such a behavior since each invocation is executed in isolation without interference from the other invocation. Modern databases provide transactions in various forms corresponding to di erent tradeo s between consistency and availability. The strongest level of consistency is achieved with serializable transactions [ ] whose outcome in concurrent executions is the same as if the transactions were executed atomically in some order. Unfortunately, serializability carries a signi cant penalty on the availability of the system assuming, for instance, that the database is accessed over a network that can su er from partitions or failures. For this reason, modern databases often provide weaker guarantees about transactions, formalized by weak consistency models, e.g., causal consistency [ ] and snapshot isolation [ ].

Implementations of large-scale databases providing transactions are di cult to build and test. For instance, distributed (replicated) databases must account for partial failures, where some components or the network can fail and produce incomplete results. Ensuring fault-tolerance relies on intricate protocols that are di cult to design and reason about. The black-box testing framework Jepsen [ ] found a remarkably large number of subtle problems in many production distributed databases.

Testing a transactional database raises two issues: ( ) deriving a suitable set of testing scenarios, e.g., faults to inject into the system and the set of transactions to be executed, and ( ) deriving e cient algorithms for checking whether a given execution satis es the considered consistency model. The Jepsen framework aims to address the rst issue by using randomization, e.g., introducing faults at random and choosing the operations in a transaction randomly. The e ectiveness of this approach has been proved formally in recent work [ ]. The second issue is, however, largely unexplored. Jepsen checks consistency in a rather ad-hoc way, focusing on speci c classes of violations to a given consistency model, e.g., dirty reads (reading values from aborted transactions). This problem is challenging because the consistency speci cations are non-trivial and they cannot be checked using, for instance, standard local assertions added to the client's code.

Besides serializability, the complexity of checking correctness of an execution w.r.t. some consistency model is unknown. Checking serializability has been shown to be NP-complete [ ], and checking causal consistency in a non-transactional context is known to be polynomial time [ ].

In this thesis, we try to ll this gap by investigating the complexity of this problem w.r.t. several consistency models and, in the case of NP-completeness, devising algorithms that are polynomial time assuming xed bounds for certain parameters of the input executions, e.g., the number of sessions.

We consider several consistency models that are the most prevalent in practice. The weakest of them, Read Committed (RC) [ ], requires that every value read in a transaction is written by a committed transaction. Read Atomic (RA) [ ] requires that successive reads of the same variable in a transaction return the same value (also known as Repeatable Reads [ ]), and that a transaction "sees" the values written by previous transactions in the same session. In general, we assume that transactions are organized in sessions [ ], an abstraction of the sequence of transactions performed during the execution of an application. Causal Consistency (CC) [ ] requires that if a transaction t 1 "a ects" another transaction t 2 , e.g., t 1 is ordered before t 2 in the same session or t 2 reads a value written by t 1 , then these two transactions are observed by any other transaction in this order. Prefix Consistency (PC) [ ] requires that there exists a total commit order between all the transactions such that each transaction observes a pre x of this sequence. Snapshot Isolation (SI) [ ] further requires that two di erent transactions observe di erent pre xes if they both write to a common variable.

We establish that checking whether an execution satis es RC, RA, or CC is polynomial time, while the same problem is NP-complete for PC and SI. Moreover, in the case of the NP-complete consistency models (PC, SI, SER), we show that their veri cation problem becomes polynomial time provided that, roughly speaking, the number of sessions in the input executions is considered to be xed (i.e., not counted for in the input size). In more detail, we establish that checking SER reduces to a search problem in a space that has polynomial size when the number of sessions is xed. (This algorithm applies to arbitrary executions, but its complexity would be exponential in the number of sessions in general.) Then, we show that checking PC or SI can be reduced in polynomial time to checking SER using a transformation of executions that, roughly speaking, splits each transaction in two parts: one part containing all the reads, and one part containing all the writes (SI further requires adding some additional variables in order to deal with transactions writing on a common variable). We extend these results even further by relying on an abstraction of executions called communication graphs [ ]. Roughly speaking, the vertices of a communication graph correspond to sessions, and the edges represent the fact that two sessions access (read or write) the same variable. We show that all these criteria are polynomial-time checkable provided that the biconnected components of the communication graph are of xed size.

These results rely on a novel speci cation framework for such criteria which is of independent interest. This framework uses logical constraints, called axioms, to characterize the set of executions that conform to a particular consistency level. An execution is modeled using a speci c set of relations between events/transactions that describe control-ow or data-ow dependencies: a program order po between events in the same transaction, a session order so between transactions in the same session, and a write-read wr (read-from) relation that associates each read event with a transaction that writes the value returned by the read. These relations along with the events (also called, operations) in an execution are called a history. A given history is said to satisfy a consistency model if it admits a total commit order between its transactions satisfying a speci c set of axioms, which intuitively, de ne lower bounds on the set of transactions t 1 that must precede in commit order a transaction t 2 that is read in the execution.

We provide an experimental evaluation of our algorithms on executions of several production databases, that makes it possible to uncover new bugs or contradictions to their documentation. In particular, we show that, although the asymptotic complexity of our algorithms is exponential in general (w.r.t. the number of sessions), the worst-case behavior is not exercised in practice. ). We use the term storage system to refer to any such database system/service.

Providing high-throughput processing, unfortunately, comes at an unavoidable cost of weakening the guarantees o ered to users. Concurrently-connected clients may end up observing different views of the same data. These "anomalies" can be prevented by using a strong consistency model such as serializability, which essentially o ers a single view of the data. However, since serializability requires expensive synchronization and incurs a high performance cost, most storage systems use weaker consistency models, such as RC, CC, or SI. In a recent survey of database administrators [ ], % of the participants responded that most or all of the transactions in their databases execute at read committed (RC) consistency models.

A weaker consistency model allows for more possible behaviors than stronger consistency models. It is up to the developers then to ensure that their application can tolerate this larger set of behaviors. Unfortunately, weak consistency models are hard to understand or reason about [ , ] and resulting application bugs can cause loss of business [ ]. Consider a simple shopping cart application that stores a per-client shopping cart in a key-value store (key is the client ID and value is a multi-set of items). Figure . shows procedures for adding an item to the cart (AddItem) and deleting all instances of an item from the cart (DeleteItem). Each procedure executes in a transaction, represented by the calls to Begin and Commit. Suppose that initially, a user u has a single instance of item I in their cart. Then the user connects to the application via two di erent sessions (for instance, via two browser windows), adds I in one session (AddItem(I, u)) and deletes I in the other session (DeleteItem(I, u)). With serializability, the cart can either be left in the state {I} (delete happened rst, followed by the add) or ∅ (delete happened second). However, with causal consistency (or read committed), it is possible that with two sequential reads of the shopping cart, the cart is empty in the rst read (signaling that the delete has succeeded), but there are two instances of I in the second read! The history corresponding to this behavior is given on the bottom of Figure . (read operations include the read value, and boxes group events from the same transaction). Such anomalies, of deleted items reappearing, have been noted in previous work [ ].

In this thesis, we address the problem of testing code for correctness against weak behaviors: a developer should be able to write a test that runs their application and then asserts for correct behavior. The main di culty today is getting coverage of weak behaviors during the test. If one runs the test against the actual production storage system, it is very likely to only result in serializable behaviors because of their optimized implementation. For instance, only .

% of all reads performed on Facebook's TAO storage system were not serializable [ ]. Emulators, o ered by cloud providers for local development, on the other hand, do not support weaker consistency models at all [ ]. Another option, possible when the storage system is available open-source, is to set it up with a tool like Jepsen [ ] to inject noise (bring down replicas or delay packets on the network). This approach is unable to provide good coverage at the level of client operations [ ] ( § . ). Another line of work has focussed on nding anomalies by identifying non-serializable behavior ( § . ). Anomalies, however, do not always correspond to bugs [ , ]; they may either not be important (e.g., gather statistics) or may already be handled in the application (e.g., checking and deleting duplicate items).

We present MonkeyDB, a mock in-memory storage system meant for testing correctness of storage-backed applications. MonkeyDB supports common APIs for accessing data (key-value updates, as well as SQL queries), making it an easy substitute for an actual storage system. Mon-keyDB can be con gured with one of several consistency models. On a read operation, MonkeyDB computes the set of all possible return values allowed under the chosen consistency models, and randomly returns one of them. The developer can then simply execute their test multiple times to get coverage of possible weak behaviors. For the program in Figure . , if we write a test asserting that two sequential reads cannot return empty-cart followed by {I, I}, then it takes only runs of the test (on average) to fail the assert. In contrast, the test does not fail when using MySQL with read committed, even after k runs. D M DB MonkeyDB does not rely on stress generation, fault injection, or data replication. Rather, it works directly with a formalization of the given consistency model in order to compute allowed return values.

MonkeyDB implements a centralized operational semantics for key-value stores, which is based on the axiomatic de nitions of consistency models that we introduced while investigating the algorithmic questions described in Section . . Transactions are executed serially, one after another, the concurrency being simulated during the handling of read events. This semantics maintains a history that contains all the past events (from all transactions/sessions), and write events are simply added to the history. The value returned by a read event is established based on a non-deterministic choice of a write-read dependency (concerning this read event) that satis es the axioms of the considered consistency model. Depending on the weakness of the consistency model, this makes it possible to return values written in arbitrarily "old" transactions, and simulate any concurrent behavior. For instance, the history in Figure . can be obtained by executing AddItem, DeleteItem, and then the two reads (serially). The read in DeleteItem can take its value from the initial state and "ignore" the previously executed AddItem, because the obtained history validates the axioms of causal consistency (or read committed). The same happens for the two later reads in the same session, the rst one being able to read from DeleteItem and the second one from AddItem.

We formally prove that this semantics does indeed simulate any concurrent behavior, by showing that it is equivalent to a semantics where transactions are allowed to interleave. In comparison with concrete implementations, this semantics makes it possible to handle a wide range of consistency models in a uniform way. It only has two sources of non-determinism: the order in which entire transactions are submitted, and the choice of write-read dependencies in read events. This enable better coverage of possible behaviors, the penalty in performance not being an issue in safety testing workloads which are usually small (see our evaluation).

We also extend our semantics to cover SQL queries as well, by compiling SQL queries down to transactions with multiple key-value reads/writes. A table in a relational database is represented using a set of primary key values (identifying uniquely the set of rows) and a set of keys, one for each cell in the table. The set of primary key values is represented using a set of Boolean keyvalue pairs that simulate its characteristic function (adding or removing an element corresponds to updating one of these keys to true or false). Then, SQL queries are compiled to read or write accesses to the keys representing a table. For instance, a SELECT query that retrieves the set of rows in a table that satisfy a WHERE condition is compiled to ( ) reading Boolean keys to identify the primary key values of the rows contained in the table, ( ) reading keys that represent columns used in the WHERE condition, and ( ) reading all the keys that represent cells in a row satisfying the WHERE condition. This rewriting contains the minimal set of accesses to the cells of a table that are needed to ensure the conventional speci cation of SQL. It makes it possible to "export" formalizations of key-value store consistency models to SQL transactions.

We present an evaluation of MonkeyDB on several applications, showcasing its superior coverage of weak behaviors as well as bug-nding abilities.

T O

The rest of this dissertation is organized as follows:

• Chapter investigates the problem of testing implementations of CRDTs. It presents formal speci cations for such datatypes and studies the asymptotic complexity of checking whether a given execution satis es a CRDT formal speci cation.

• Chapter de nes axiomatic speci cations of several transactional consistency models and establishes complexity results concerning the problem of checking conformance to such speci cations for a given execution. It shows that consistency models weaker than Causal Consistency can be checked in polynomial time, while the problem becomes NP-complete for stronger models. In the latter case, it identi es a parameter of executions which enables polynomial-time algorithms when xed.

• Chapter investigates the testing coverage problem for distributed applications built on top of transactional datastores. It presents the mock in-memory storage system MonkeyDB, which simulates transactional datastores according to their formal speci cations. The experimental evaluation of MonkeyDB shows that it provides better test coverage than state of the art setups.

• Chapter concludes and discusses directions for future work.

C C C F R D T
In this chapter we study the tractability of runtime CRDT consistency checking: deciding whether a given execution of a CRDT is consistent with its speci cation. Our setting captures executions across a set of replicas as per-replica sequences of operations called histories. Roughly speaking, a history is consistent so long as each operation's return value can be justi ed according to the operations that its replica has observed so far. In the setting of CRDTs, the determination of a replica's observations is essentially an implementation choice: replicas are only obliged to observe their own operations, and the predecessors of those it has already observed. This relatively-weak constraint on replicas' observations makes the CRDT consistency checking problem unique.

We present logical characterizations of CRDTs, which are built on a notion of abstract execution, which relates the operations of a given history with three separate relations: a read-from relation, governing the observations from which a given operation constitutes its own return value; a happens-before relation, capturing the causal relationships among operations; and a linearization relation, capturing any necessary arbitration among non-commutative e ects which are executed concurrently, e.g., following a last-writer-wins policy. Accordingly, we capture data type specications with logical axioms interpreted over the read-from, happens-before, and linearization relations of abstract executions, reducing the consistency problem to: does there exist an abstract execution over the given history which satis es the axioms of the given data type?

We demonstrate the intractability of several replicated data types by reduction from propositional satis ability (SAT) problems. In particular, we consider the -in-SAT problem [ ], which asks for a truth assignment to the variables of a given set of clauses such that exactly one literal per clause is assigned true. Our reductions essentially simulate the existential choice of a truth assignment with the existential choice of the read-from and happens-before relations of an abstract execution. For a given -in-SAT instance, we construct a history of replicas obeying carefully-tailored synchronization protocols, which is consistent exactly when the corresponding SAT instance is positive.

Finally, we develop tractable consistency-checking algorithms for individual data types and special cases: replicated growing arrays; multi-value and last-writer-wins registers, when each value is written only once; counters, when replicas are bounded; and sets and ags, when their sizes are also bounded. While the algorithms for each case are tailored to the algebraic properties of the data types they handle, they essentially all function by constructing abstract executions incrementally, processing replicas' operations in pre x order.

The remainder of this chapter is organized as follows:

• Section . presents logical characterizations of consistency for the replicated register, ag, set, counter, and array data types;

• Section . introduces reductions from propositional satis ability problems to consistency checking to demonstrate intractability for replicated ags, sets, counters, and registers; and

• Section . de nes polynomial time consistency-checking algorithms for replicated growable arrays, registers, when written values are unique, counters, when replicas are bounded, and sets and ags, when their sizes are also bounded.

Section . overviews related work, and Section . concludes.

A L C R D T

In this section we describe an axiomatic framework for de ning the semantics of replicated data types. We consider a set of method names M, and that each method m ∈ M has a number of arguments and a return value sampled from a data domain D. We will use operation labels of the form m(a)

i ⇒ b to represent the call of a method m ∈ M, with argument a ∈ D, and resulting in the value b ∈ D. Since there might be multiple calls to the same method with the same arguments and result, labels are tagged with a unique identi er i. We will ignore identi ers when unambiguous.

The interaction between a data type implementation and a client is represented by a history h = Op, ro which consists of a set of operation labels Op and a partial replica order ro ordering operations issued by the client on the same replica. Usually, ro is a union of sequences, each sequence representing the operations issued on the same replica, and the width of ro, i.e., the maximum number of mutually-unordered operations, gives the number of replicas in a given history.

To characterize the set of histories h = Op, ro admitted by a certain replicated data type, we use abstract executions e = rf, hb, lin , which include:

• a read-from binary relation rf over operations in Op, which identi es the set of updates needed to "explain" a certain return value, e.g., a write operation explaining the return value of a read,

• a strict partial happens-before order hb, which includes ro and rf, representing the causality constraints in an execution, and

• a strict total linearization order lin, which includes hb, used to model con ict resolution policies based on timestamps.

In this work, we consider replicated data types which satisfy causal consistency [ ], i.e., updates which are related by cause and e ect relations are observed by all replicas in the same order. This follows from the fact that the happens-before order is constrained to be a partial order, and thus transitive (other forms of weak consistency don't pose this constraint). Some of the replicated data types we consider in this work do not consider resolution policies based on timestamps and in those cases, the linearization order can be ignored. A replicated data type is de ned by a set of rst-order axioms Φ characterizing the relations in an abstract execution. A history h is admitted by a data type when there exists an abstract execution e such that h, e |= Φ. The satisfaction relation |= is de ned as usual in rst order logic. The admissibility problem is the problem of checking whether a history h is admitted by a given data type.

R F (R) ∀o1, o2. rf(o1, o2) ⇒ R(o1, o2) R F M (R) ∀o1, o2, o3. rf(o1, o2) ∧ R(o3, o2) ⇒ ¬hb(o1, o3) ∨ ¬hb(o3, o2) R A M (R) ∀o1, o2. hb(o1, o2) ∧ R(o1, o2) ⇒ ∃o3. hb * (o1, o3) ∧ rf(o3, o2) C RF(R) ∀o1, o2, o3. R(o1, o2) ∧ hb(o1, o3) ∧ rf(o3, o2) ⇒ rf(o1, o2) R S (X, v, Y ) ∀o1. meth(o1) = X ∧ ret(o1) = v ⇔ ∃o2. rf(o2, o1) ∧ meth(o2) = Y ∧ arg(o1) = arg(o2) R C ∀o1. meth(o1) = read ⇒ ret(o1) = |{o2 : meth(o2) = inc ∧ rf(o2, o1)}| -|{o2 : meth(o2) = dec ∧ rf(o2, o1)}| L LWW ∀o1, o2, o3. rf(o1, o2) ∧ meth(o3) = write ∧ arg 1 (o3) = arg(o2) ∧ hb(o3, o2) ⇒ lin(o3, o1) R R ∀o1, v.meth(o1) = read ∧ v ∈ ret(o1) ⇒ ∃!o2.rf(o2, o1) ∧ meth(o2) = write ∧ arg 2 (o2) = v
In the following, we de ne the replicated data types with respect to which we study the complexity of the admissibility problem. The axioms used to de ne them are listed in Figure . and Figure . . These axioms use the function symbols meth-od, arg-ument, and ret-urn interpreted over operation labels, whose semantics is self-explanatory.

R S F

The Add-Wins Set and Remove-Wins Set [ ] are two implementations of a replicated set with operations add(x), remove(x), and contains(x) for adding, removing, and checking membership of an element x. Although the meaning of these methods is self-evident from their names, the result of con icting concurrent operations is not evident. When concurrent add(x) and remove(x) operations are delivered to a certain replica, the Add-Wins Set chooses to keep the element x in the set, so every subsequent invocation of contains(x) on this replica returns true, while the Remove-Wins Set makes the dual choice of removing x from the set. The formal de nition of their semantics uses abstract executions where the read-from relation associates sets of add(x) and remove(x) operations to contains(x) operations. Therefore, the predicate ReadOk(o 1 , o 2 ) is de ned by

meth(o 1 ) ∈ {add, remove} ∧ meth(o 2 ) = contains ∧ arg(o 1 ) = arg(o 2 )
Checking Consistency for Conflict-Free Replicated Data Types and the Add-Wins Set is de ned by the following set of axioms:

R F (ReadOk) ∧ R F M (ReadOk) ∧ R A M (ReadOk) ∧ R S (contains, true, add) R F M
says that every operation read by a contains(x) is maximal among its hbpredecessors that add or remove x while R A M says that all such maximal hbpredecessors are read. The R S instantiation ensures that a contains(x) returns true i it reads-from at least one add(x).

The de nition of the Remove-Wins Set is similar, except for the parameters of R S , which become R S (contains, false, remove), i.e., a contains(x) returns false i it readsfrom at least one remove(x).

The Enable-Wins Flag and Disable-Wins Flag are implementations of a set of ags with operations: enable(x), disable(x), and read(x), where enable(x) turns the ag x to true, disable(x) turns x to false, while read(x) returns the state of the ag x. Their semantics is similar to the Add-Wins Set and Remove-Wins Set, respectively, where enable(x), disable(x), and read(x) play the role of add(x), remove(x), and contains(x), respectively. Their axioms are de ned as above.

R R

We consider two variations of replicated registers called Multi-Value Register (MVR) and Last-Writer-Wins Register (LWW) [ ] which maintain a set of registers and provide write(x,v) operations for writing a value v on a register x and read(x) operations for reading the content of a register x (the domain of values is kept unspeci ed since it is irrelevant). While a read(x) operation of MVR returns all the values written by concurrent writes which are maximal among its happens-before predecessors, therefore, leaving the responsibility for solving con icts between concurrent writes to the client, a read(x) operation of LWW returns a single value chosen using a con ict-resolution policy based on timestamps. Each written value is associated to a timestamp, and a read operation returns the most recent value w.r.t. the timestamps. This order between timestamps is modeled using the linearization order of an abstract execution. Therefore, the predicate ReadOk(o 1 , o 2 ) is de ned by

meth(o 1 ) = write ∧ meth(o 2 ) = read ∧ arg 1 (o 1 ) = arg(o 2 ) ∧ arg 2 (o 1 ) ∈ ret(o 2 )
(we use arg 1 (o 1 ) to denote the rst argument of a write operation, i.e., the register name, and arg 2 (o 1 ) to denote its second argument, i.e., the written value) and the MVR is de ned by the following set of axioms:

R F (ReadOk) ∧ R F M (ReadOk) ∧ R A M (ReadOk) ∧ R R
where R R ensures that a read(x) operation reads from a write(x,v) operation, for each value v in the set of returned values .

For simplicity, we assume that every history contains a set of write operations writing the initial values of variables, which precede every other operation in replica order. LWW is obtained from the de nition of MVR by replacing R A M with the axiom L LWW which ensures that every write(x,_) operation which happens-before a read(x) operation is linearized before the write(x,_) operation from where the read(x) takes its value (when these two write operations are di erent). This de nition of LWW is inspired by the "bad-pattern" characterization in [ ], corresponding to their causal convergence criterion.

R F RGA ∀o2. meth(o2) = addAfter ⇒ arg 1 (o2) = • ∨ ∃o1. meth(o1) = addAfter ∧ arg 2 (o1) = arg 1 (o2) ∧ rf(o1, o2) ∧ meth(o2) = remove ⇒ ∃o1. meth(o1) = addAfter ∧ arg 2 (o1) = arg(o2) ∧ rf(o1, o2) ∧ meth(o2) = read ⇒ ∀v ∈ ret(o2) ∃o1.meth(o1) = addAfter ∧ arg 2 (o1) = v ∧ rf(o1, o2) R RGA ∀o1, o2. meth(o1) = read ∧ meth(o2) = addAfter ∧ hb(o2, o1) ∧ arg 2 (o2) ∈ ret(o1) ⇒ ∃o3. meth(o3) = remove ∧ arg(o3) = arg 2 (o2) ∧ rf(o3, o1) L RGA ∀o1, o2. meth(o1) = meth(o2) = addAfter ∧ arg 1 (o1) = arg 1 (o2) ∧ ∃o3, o4, o5. meth(o3) = meth(o4) = addAfter ∧ rf * addAfter (o1, o3) ∧ rf * addAfter (o2, o4)∧ meth(o5) = read ∧ arg 2 (o4) <o 5 arg 2 (o3) ⇒ lin(o1, o2)

R C

The replicated counter datatype [ ] maintains a set of counters interpreted as integers (the counters can become negative). This datatype provides operations inc(x) and dec(x) for incrementing and decrementing a counter x, and read(x) operations to read the value of the counter x. The semantics of the replicated counter is quite standard: a read(x) operation returns the value computed as the di erence between the number of inc(x) operations and dec(x) operations among its happens-before predecessors. The axioms de ned below will enforce the fact that a read(x) operation reads-from all its happens-before predecessors which are inc(x) or dec(x) operations. Therefore, the predicate ReadOk(o 1 , o 2 ) is de ned by

meth(o 1 ) ∈ {inc, dec} ∧ meth(o 2 ) = read ∧ arg(o 1 ) = arg(o 2 )
and the replicated counter is de ned by the following set of axioms:

R F (ReadOk) ∧ C RF(ReadOk) ∧ R C .

R G A

The Replicated Growing Array (RGA) [ ] is a replicated list used for text-editing applications. RGA supports three operations: addAfter(a,b) which adds the character b immediately after the occurrence of the character a assumed to be present in the list, remove(a) which removes a assumed to be present in the list, and read() which returns the list contents. It is assumed that a character is added at most once . The con icts between concurrent addAfter operations that add a character immediately after the same character is solved using timestamps (i.e., each added character is associated to a timestamp and the order between characters depends on the order between the corresponding timestamps), which in the axioms below are modeled by the linearization order.

Figure . lists the axioms de ning RGA. R F RGA ensures that:

• every addAfter(a,b) operation reads-from the addAfter(_,a) adding the character a, except when a = • which denotes the "root" element of the list ,

• every remove(a) operation reads-from the operation adding a, and

• every read operation returning a list containing a reads-from the operation addAfter(_,a) adding a.

Then, R RGA ensures that a read operation o 1 happening-after an operation adding a character a reads-from a remove(a) operation when a doesn't occur in the list returned by o 1 (the history must contain a remove(a) operation because otherwise, a should have occurred in the list returned by the read).

Finally, L RGA models the con ict resolution policy by constraining the linearization order between addAfter(a,_) operations adding some character immediately after the same character a. As a particular case, L RGA enforces that addAfter(a,b) is linearized before addAfter(a,c) when a read operation returns a list where c precedes b (addAfter(a,b) results in the list a•b and applying addAfter(a,c) on a • b results in the list a • c • b). However, this is not su cient: assume that the history contains the two operations addAfter(a,b) and addAfter(a,c) along with two operations remove(b) and addAfter(b,d). Then, a read operation returning the list a • c • d must enforce that addAfter(a,b) is linearized before addAfter(a,c) because this is the only order between these two operations that can lead to the result a • c • d, i.e., executing addAfter(a,b), addAfter(b,d), remove(b), addAfter(a,c) in this order. L RGA deals with any scenario where arbitrarily-many characters can be removed from the list: rf * addAfter is the re exive and transitive closure of the projection of rf on addAfter operations and < o 5 denotes the order between characters in the list returned by the read operation o 5 .

I R S F C

In this section, we demonstrate that checking the consistency is intractable for many widely-used data types. While this is not completely unexpected, since some related consistency-checking problems like sequential consistency are also intractable [ ], this contrasts recent tractability results for checking strong consistency (i.e., linearizability) of common non-replicated data types like sets, maps, and queues [ ]. In fact, in many cases, we show that intractability even holds if the number of replicas is xed.

Our proofs of intractability follow the general structure of Gibbons and Korach's proofs for the intractability of checking sequential consistency (SC) for atomic registers with read and write In a practical context, this can be enforced by tagging characters with replica identi ers and sequence numbers. This element is not returned by read operations. Figure .

: The encoding of a -in-SAT problem m i=1 (α i ∨ β i ∨ γ i ) over variables x 1 , . . . , x n as areplica history of a ag data type. Besides the ag variable x j for each propositional variable x j , the encoding adds per-replica variables y j for synchronization barriers.

operations [ ]. In particular, we reduce a specialized type of NP-hard propositional satis ability (SAT) problem to checking whether histories are admitted by a given data type. While our construction borrows from Gibbons and Korach's, the adaptation from SC to CRDT consistency requires a signi cant extension to handle the consistency relaxation represented by abstract executions: rather than a direct sequencing of threads' operations, CRDT consistency requires the construction of three separate relations: read-from, happens-before, and linearization.

Technically, our reductions start from the -in-SAT problem [ ]: given a propositional formula m i=1 (α i ∨ β i ∨ γ i ) over variables x 1 , . . . , x n with only positive literals, i.e., α i , β i , γ i ∈ {x 1 , . . . , x n }, does there exist an assignment to the variables such that exactly one of α i , β i , γ i per clause is assigned true? The proofs of Theorems . . and . . reduce -in-SAT to CRDT consistency checking.

Theorem . . . The admissibility problem is NP-hard when the number of replicas is fixed for the following data types: Add-Wins Set, Remove-Wins Set, Enable-Wins Flag, Disable-Wins Flag, Multi-Value Register, and Last-Writer-Wins Register. Proof. We demonstrate a reduction from the -in-SAT problem. For a given problem p = m i=1 (α i ∨ β i ∨ γ i ) over variables x 1 , . . . , x n , we construct a -replica history h p of the ag data type -either enable-or disable-wins -as illustrated in Figure . . The encoding includes a ag variable x j for each propositional variable x j , along with a per-replica ag variable y j used to implement synchronization barriers. Intuitively, executions of h p proceed in m + 1 rounds: the rst round corresponds to the assignment of a truth valuation, while subsequent rounds check the validity of each clause given the assignment. The reductions to sets and registers are slight variations on this proof, in which the Read, Enable, and Disable operations are replaced with Contains, Add, and Remove, respectively, and Read and Writes of values and , respectively.

It su ces to show that the constructed history h p is admitted if and only if the given problem p is satis able (it is easy to see that the size of h p is linear in the size of p, and that h p can be computed in linear time). Since the ag data type does not constrain the linearization relation of its abstract executions, we regard only the read-from and happens-before components. The construction of h p ensures the happens-before relations of its abstract executions:

. does not interleave operations from di erent rounds. Each consecutive rounds are separated by the barriers in happens-before relations; and

. at each round, only one replica, say replica i, can nish its Reads then nish its Enables/Disables, then (i+1) mod 3 replica can nish its Reads and so on. And these Enables/Disables from one round are totally ordered between replicas by the happens-before relation.

In other words, replicas appear to execute atomically per round, in a round-robin fashion. Furthermore, since all operations in a given round happen before the operations of subsequent rounds, the values of ag variables are consistent across rounds -i.e., as read by the rst replica to execute in a given round -and determined in the initial round either by con ict resolution -i.e., enable-or disable-wins -or by happens-before, in case of con ict resolution would have been inconsistent with subsequent reads.

The correctness of the construction is stated in the following lemma:

Lemma . . . p = m i=1 (α i ∨ β i ∨ γ i ) is satisfiable if and only if h p is admissible Proof. (Only-if direction). Assume that 1 i=1 (α i ∨β i ∨γ i ) is satis able, i.e.
, there exists a variable assignment γ for which each clause has exactly one literal interpreted as true.

We construct a happens-before relation hb such that: ( ) if γ(x i ) = f alse, then Enable(x i ) in Replica is visible to Disable(x i ) in Replica , i.e. (Enable(x i ), Disable(x i )) ∈ hb (this ensures that the value of x i is f alse after Barrier ), and similarly, ( ) if γ(x i ) = true, then (Disable(x i ), Enable(x i )) ∈ hb. Note this does not introduce any cycle in hb because x i s are Enabled and Disabled in the same order in Replica and Replica .

Then, for each barrier i, all the Enable operations happen-before all the Read operations. Also, for each round i, if α i is true in clause i (w.r.t. γ), then we make all the operations of the round i at replica happen-before operations of the round i at replica , and all the operations of the round i at replica happen-before operations of the round i at replica . This makes the history admissible because if α 1 is true, then β 1 and γ 1 are false. So the reads of round i at replica are correct. Then the updates of round i at replica make α 1 false and β 1 true (γ 1 remains false). So now, the reads of round i at replica are also correct. The same reasoning can be applied for the reads at replica . The cases β i true or γ i true lead to a similar de nition of happens-before, ordering replicas in the order , , if β i is true, and , , , if γ 1 is true. A straightforward proof by induction allows to prove that the history is admissible w.r.t. a happens-before relation de ned in this manner.

(If direction). Assume that h p is admissible. We give a series of lemmas that characterize the happens-before (read-from) relation of h p .

Lemma . . . The Reads of each barrier read-from the Enables or Disables of the same barrier.

Proof. We give a proof by induction on the number of the barrier. (Base case). Note that only replica i Enables or Disables y i . Assume by contradiction that at barrier , Read(y j ) = true at replica i reads from an operation in a barrier other than . Then, it must read from an operation of barrier at least (y j is set to true at odd numbered barriers). Now at barrier and replica j, Read(y i ) = f alse reads from a Disable because replica j has Read(y i ) = true at barrier . So at barrier and replica j, Read(y i ) = f alse can read from a Disable which is at even numbered barriers, at least from barrier . This de nes a cycle in the happens-before order, which contradicts the admissibility of h p :

• Enable(y j ) at barrier ≥ 3 and replica j happens-before Read(y j ) = true at barrier and replica i because of read-from,

• Read(y j ) = true at barrier and replica i happens-before Disable(y i ) at barrier ≥ 2 and replica i,

• Disable(y i ) at barrier ≥ 2 and replica i happens-before Read(y i ) = f alse at barrier and replica j because of read-form, and

• Read(y i ) = f alse at barrier and replica j happens-before Enable(y j ) at barrier ≥ 3 and replica j.

(Induction step). By the induction hypothesis, barrier k always reads from barrier k itself. Therefore, Read(y j ) of barrier (k + 1) happens after the update of y j from barrier k. Without loss of generality, let us assume that barrier k contains Enable operations. Since barrier k contains Enable operations, the f alse reads in barrier (k + 1) must read from a barrier strictly greater than k. Using the same logic from the base case, this would imply a cycle in the happens-before relation.

Lemma . . ensures that all the operations from all replicas before barrier i happen before every operation (from any replica) after barrier i.

We say that two Read operations see the same value of x i when one Read reads-from an Enable(x i ) if and only if the other Read also reads-from an Enable(x i ) (these Enable operations may not be the same). Also, a read in a round k is called initial if it does not happen before an Enable or Disable from the same round. Lemma . . . Initial Reads of two consecutive rounds see the same value of x i , for each i.

Proof. Note that the Reads from each round read only from updates from the same round or from preceding rounds. Reading from any later round is not possible, because, by Lemma . . , that will introduce a happen-before cycle between the current round and that later round. Also, in each round, there exist one replica which does not read-from other replicas in the same round. If replica p is reading from replica q, then replica q again can not read from replica p, because it will create a cycle in hb between replica p and q in the same round. So replica q has to read from replica r. But then replica r will have to read from replica p, which creates a cycle between replica p, q, and r in the same round.

So there exists one replica, which reads-from updates till last round. Since the Reads of that replica are successful, it ensures only one of α k , β k , γ k are true i.e. only one of those Reads readsfrom an Enable. Hence, the rst true Reads at other replicas must read-from the updates in the same round. Therefore, all the operations from a round k ≥ 1 are totally ordered w.r.t. the happens-before, all operations in one replica before all operations in another. That is, if replica was the rst one to nish its reads, Read(β k ) = true reads-from Enable(β k ) and Read(γ k ) = true reads-from Enable(γ k ). Since the updates are totally ordered and they only ip the read values of x i twice, i.e. if the rst read on x i is f alse, then it does not read-from any Enable till round (k -1) and at round k, after Read(x i ) = f alse, Enable(x i ) and Disable(x i ) are ordered by hb. So the hb-maximal update on x i on round k stays Disable(x i ). Similarly we can show, the hb-maximal update on x i on round k stays Enable(x i ) when the rst Read(x i ) was true.

When round (k + 1) begins, because of Lemma . . , it "sees" all the updates at the end of round k, which includes the updates from earlier rounds.

• If x i is not modi ed in round k, then round (k + 1) will read-from from the same update for x i as round k.

• If x i is modi ed in round k, any hb-maximal Read(x i ) at round (k + 1) will read-form hb-maximal updates at round k by lemma . . . And, the hb-maximal update on x i at the end of round k stays the same as the update which round k read-form at the beginning.

Going back to the proof of Lemma . . , p is satis able using an assignment de ned by the initial Reads of each round (which see the same values by Lemma . . ). This assignment satis es the -in-SAT formula p because at each round, there is a replica that happens-before operations in the same round at the other replicas, and the Reads of that replica see exactly one ag as true.

Theorem . . establishes intractability of consistency for the aforementioned sets, ags, and registers, independently from the number of replicas. In contrast, our proof of Theorem . . for counter data types depends on the number of replicas, since our encoding requires two replicas per propositional variable. Intuitively, since counter increments and decrements are commutative, the initial round in the previous encoding would have xed all counter values to zero. Instead, the next encoding isolates initial increments and decrements to independent replicas.

Theorem . . . The admissibility problem for the Counter data type is NP-hard.

We demonstrate a reduction from the -in-SAT problem. For a given problem p = m i=1 (α i ∨ β i ∨ γ i ) over variables x 1 , . . . , x n , we construct a history h p of the counter data type over 2n + 3 replicas, as illustrated in Figure . .

Besides the di erences imposed due to the commutativity of counter increments and decrements, our reduction follows the same strategy as in the proof of Theorem . . : the happensbefore relation of h p 's abstract executions order every pair of operations in distinct rounds (of

Replica Replica 2j +1 Replica 2j +2 Round    Inc(y) Inc(y) Inc(x j ) Dec(x j ) Read(y) = n Replica Replica Barrier    Inc(y 0 ) Inc(y 1 ) Inc(y 2 ) Read(y 1 ) = 1 Read(y 2 ) = 1 Read(y 0 ) = 1 Read(y 2 ) = 1 Read(y 0 ) = 1 Read(y 1 ) = 1 Round          Read(α 1 ) = 1 Read(β 1 ) = 1 Read(γ 1 ) = 1 Read(β 1 ) = -1 Read(γ 1 ) = -1 Read(α 1 ) = -1 Read(γ 1 ) = -1 Read(α 1 ) = -1 Read(β 1 ) = -1 Dec(α 1 ); Dec(α 1 ) Dec(β 1 ); Dec(β 1 ) Dec(γ 1 ); Dec(γ 1 ) Inc(β 1 ); Inc(β 1 ) Inc(γ 1 ); Inc(γ 1 ) Inc(α 1 ); Inc(α 1 ) Barrier    Dec(y 0 ) Dec(y 1 ) Dec(y 2 ) Read(y 1 ) = 0 Read(y 2 ) = 0 Read(y 0 ) = 0 Read(y 2 ) = 0 Read(y 0 ) = 0 Read(y 1 ) = 0 . . . . . . . . . Round m          Read(αm) = 1 Read(βm) = 1 Read(γm) = 1 Read(βm) = -1 Read(γm) = -1 Read(αm) = -1 Read(γm) = -1 Read(αm) = -1 Read(βm) = -1 Dec(αm); Dec(αm) Dec(βm); Dec(βm) Dec(γm); Dec(γm) Inc(βm); Inc(βm) Inc(γm); Inc(γm) Inc(αm); Inc(αm) Barrier m+1    Inc(y 0 ) or Dec(y 0 ) Inc(y 1 ) or Dec(y 1 ) Inc(y 2 ) or Dec(y 2 ) Read(y 1 ) = 1 or 0 Read(y 2 ) = 1 or 0 Read(y 0 ) = 1 or 0 Read(y 2 ) = 1 or 0 Read(y 0 ) = 1 or 0 Read(y 1 ) = 1 or 0 Round m+1 Read(y) = n Figure . : The encoding of a -in-SAT problem m i=1 (α i ∨ β i ∨ γ i ) over variables x 1 , . . . ,
x n as the history of a counter over 2n + 3 replicas. Besides the counter variables x j encoding propositional variables x j , the encoding adds a variable y encoding the number of initial increments and decrements, and a variable z to implement synchronization barriers.

Replicas -), and every operation in a given (non-initial) round. As before, Replicas -appear to execute atomically per round, in a round-robin fashion, and counter variables are consistent across rounds. The key di erence is that here abstract executions' happens-before relations only relate the operations of either Replica 2j+1 or 2j+2, for each j = 1, . . . , n, to operations in subsequent rounds: the other's operations are never observed by other replicas. Our encoding ensures that exactly one of each is observed by ensuring that the counter y is incremented exactly n times -and relying on the fact that every variable appears in some clause so that a read that observed neither or both would yield the value zero, which is inconsistent with h p . Otherwise, our reasoning follows the proof of Theorem . . , in which the read-from relation selects all increments and decrements of the same counter variable in happens-before order.

P T A R A

We show that the problem of checking consistency is polynomial time for RGA, and even for LWW and MVR under the assumption that each value is written at most once, i.e., for each value Input: A di erentiated history h = Op, ro and a datatype T . Output: true i h satis es the axioms of T . v, the input history contains at most one write operation write(x,v). Histories satisfying this assumption are called di erentiated. The latter is a restriction motivated by the fact that practical implementations of these datatypes are data-independent [ ], i.e., their behavior doesn't depend on the concrete values read or written and any potential buggy behavior can be exposed in executions where each value is written at most once. Also, in a testing environment, this restriction can be enforced by tagging each value with a replica identi er and a sequence number.

rf ← ComputeRF(h,R F [T ],R [T ] ); if rf = ⊥ then return false; hb ← (ro ∪ rf) + ; if hb is cyclic or h, rf, hb |= R F M [T ] ∧ R A M [T ]
In all three cases, the feature that enables polynomial time consistency checking is the fact that the read-from relation becomes xed for a given history, i.e., if the history is consistent, then there exists exactly one read-from relation rf that satis es the R F and R axioms, and rf can be derived syntactically from the operation labels (using those axioms). Then, our axiomatic characterizations enable a consistency checking algorithm which roughly, consists in instantiating those axioms in order to compute an abstract execution.

The consistency checking algorithm for RGA, LWW, and MVR is listed in Algorithm . It computes the three relations rf, hb, and lin of an abstract execution using the datatype's axioms. The history is declared consistent i there exist satisfying rf and hb relations, and the relations hb and lin computed this way are acyclic. The acyclicity requirement comes from the de nition of abstract executions where hb and lin are required to be partial/total orders. While an abstract execution would require that lin is a total order, this algorithm computes a partial linearization order. However, any total order compatible with this partial linearization would satisfy the axioms of the datatype.

ComputeRF computes the read-from relation rf satisfying the R F and R axioms. In the case of LWW and MVR, it de nes rf as the set of all pairs formed of write(x,v) and read(x) operations where v belongs to the return value of the read. By R , each read(x) operation must be associated to at least one write(x,_) operation. Also, the fact that each value is written at most once implies that this rf relation is uniquely de ned, e.g., for LWW, it is not possible to nd two write operations that could be rf related to the same read operation. In general, if there exists no rf relation satisfying these axioms, then ComputeRF returns a distinguished value ⊥ to signal a consistency violation. Note that the computation of the read-from for LWW and MVR is quadratic time since the constraints imposed by the axioms relate only to the op-Assuming constant time lookup/insert operations (e.g., using hashmaps), this complexity is linear time. Algorithm : The procedure ComputeRF for RGA. eration labels, the methods they invoke or their arguments. The case of RGA is slightly more involved because the axiom R RGA introduces more read-from constraints based on the happens-before order which includes ro and the rf itself. In this case, the computation of rf relies on a xpoint computation, which converges in at most quadratic time (the maximal size of rf), described in Algorithm . Essentially, we use the axiom R F RGA to populate the readfrom relation and then, apply the axiom R RGA iteratively, using the read-from constraints added in previous steps, until the computation converges.

Input:

A history h = Op, ro of RGA. Output: An rf satisfying R F RGA ∧ R RGA, if exists; ⊥ o/w rf ← {(o1, o2) : meth(o1) = addAfter, meth(o2) ∈ {addAfter, remove, read}, arg 2 (o1) = arg 1 (o2) ∨ arg 2 (o1) ∈ ret(o2)}; if h, rf |= R F RGA
After computing the read-from relation, our algorithm de nes the happens-before relation hb as the transitive closure of ro union rf. This is sound because none of the axioms of these datatypes enforce new happens-before constraints, which are not already captured by ro and rf. Then, it checks whether the hb de ned this way is acyclic and satis es the datatype's axioms that constrain hb, i.e., R F M and R A M (when they are present). Finally, in the case of LWW and RGA, the algorithm computes a (partial) linearization order that satis es the corresponding L axioms. Starting from an initial linearization order which is exactly the happens-before, it computes new constraints by instantiating the universally quanti ed axioms L LWW and L RGA. Since these axioms are not "recursive", i.e., they don't enforce linearization order constraints based on other linearization order constraints, a standard instantiation of these axioms is enough to compute a partial linearization order such that any extension to a total order satis es the datatype's axioms.

Theorem . . . Algorithm returns true i the input history is consistent.

The following holds because Algorithm runs in polynomial time -the rank depends on the number of quanti ers in the datatype's axioms. Indeed, Algorithm represents a least xpoint computation which converges in at most a quadratic number of iterations (the maximal size of rf).

Corollary . . . The admissibility problem is polynomial time for RGA, and for LWW and MVR on di erentiated histories.

Input: History h = (Op, ro), pre x map m, and set seen of invalid pre x maps Output: false if there exists no read-from and happens-before relations rf and hb such that m ⊆ hb, and h, rf, hb satis es the counter axioms.

if m is complete then return true;

foreach replica i do foreach replica j = i do m ← m[i ← m(i) ∪ m(j)]; if m ∈ seen and checkCounter(h, m , seen) then return true; seen ← seen ∪ {m }; if ∃o1. ro 1 (lasti(m), o1) then if meth(o1) = read and arg(o1) = x ∧ ret(o1) = |{o ∈ m[i]|o = inc(x)}| -|{o ∈ m[i]|o = dec(x)}| then return false; m ← m[i ← m(i) ∪ {o1}]; if m ∈

R C

In this section, we propose a sound polynomial time algorithm for replicated counter datatype assuming the number of replicas in the input history is xed (i.e. the width of the rpelica order ro is xed). The algorithm constructs a valid happens-before order (note that the semantics of the replicated counter doesn't constrain the linearization order) incrementally, following the replica order. At any time, the happens-before order is uniquely determined by a prefix mapping that associates to each replica a prefix of the history, i.e., a set of operations which is downward-closed w.r.t. replica order (i.e., if it contains an operation it contains all of its ro predecessors). This models the fact that the replica order is included in the happens-before and therefore, if an operation o 1 happens-before another operation o 2 , then all the ro predecessors of o 1 happen-before o 2 . The happens-before order can be extended in two ways: ( ) adding an operation issued on the replica i to the pre x of replica i, or ( ) "merging" the pre x of a replica j to the pre x of a replica i (this models the delivery of an operation issued on replica j and all its happens-before predecessors to the replica i). Verifying that an extension of the happens-before is valid, i.e., that the return values of newly-added read operations satisfy the R C axiom, doesn't depend on the happens-before order between the operations in the pre x associated to some replica (it is enough to count the inc and dec operations in that pre x). Therefore, the algorithm can be seen as a search in the space of pre x mappings. If the number of replicas in the input history is xed, then the number of possible pre x mappings is polynomial in the size of the history, which implies that the search can be done in polynomial time.

Let h = (Op, ro) be a history. To simplify the notations, we assume that the replica order is a union of sequences, each sequence representing the operations issued on the same replica.

Therefore, each operation o ∈ Op is associated with a replica identi er rep(o) ∈ [1..n h ], where n h is the number of replicas in h.

A prefix of h is a set of operation Op ⊆ Op such that all the ro predecessors of operations in Op are also in Op , i.e., ∀o ∈ Op. ro -1 (o) ∈ Op. Note that the union of two pre xes of h is also a pre x of h. The last operation of replica i in a pre x Op is the ro-maximal operation o with rep(o) = i included in Op . A pre x Op is called valid if (Op , ro ), where ro is the projection of ro on Op , is admitted by the replicated counter.

A prefix map is a mapping m which associates a pre x of h to each replica i ∈ [1..n h ]. Intuitively, a pre x map de nes for each replica i the set of operations which are "known" to i, i.e., happen-before the last operation of i in its pre x. Formally, a pre x map m is included in a happens-before relation hb,

denoted by m ⊆ hb, if for each replica i ∈ [1..n h ], hb(o, o i ) for each operation in o ∈ m(i) \ {o i },
where o i is the last operation of i in m(i). We call o i the last operation of i in m, and denoted it by last i (m). A pre x map m is valid if it associates a valid pre x to each replica, and complete if it associates the whole history h to each replica i.

Algorithm lists our algorithm for checking consistency of replicated counter histories. It is de ned as a recursive procedure checkCounter that searches for a sequence of valid extensions of a given pre x map (initially, this pre x map is empty) until it becomes complete. The axiom R C is enforced whenever extending the pre x map with a new read operation (when the last operation of a replica i is "advanced" to a read operation). The following theorem states the correctness of the algorithm.

Theorem . . . checkCounter(h, ∅, ∅) returns false if the input history is inconsistent.

When the number of replicas is xed, the number of pre x maps becomes polynomial in the size of the history. This follows from the fact that pre xes are uniquely de ned by their ro-maximal operations, whose number is xed. Since the possible number of pre x-map is polynomial when the number of replicas is xed, the algorithm terminates after exploring polynomially many states. Since the each step of the recursion happens in polynomial time, the algorithm always run in polynomial time in the size of the history when the number of replicas is xed.

I

As a correction of our previous work [ ], we show that Algorithm is actually incomplete, i.e., it may return false while the history is admissible. The history of a replicated counter in Figure . is a counterexample to completeness. This history admits a single read-from relation as witness of admissibility, which is given by the edges in the gure. [inc(a)] r 1 must propagate after [read(a) = 2] r 2 and before [read(a) = 3] r 2 . To simulate this propagation, the algorithm must reach a pre x map which had [inc(a)] r 1 and [read(a) = 2] r 2 as the ro-maximal operations from each replica. Symmetrically, the same argument holds when [inc(a)] r 2 needs to propagate after [read(a) = 2] r 1 and before [read(a) = 3] r 1 . So the algorithm must reach another pre x map which had [inc(a)] r 2 and [read(a) = 2] r 1 as the ro-maximal operations from each replica.

Since the algorithm always extends the maintained pre x map i.e. when successful, the sequence of valid extensions from the empty pre x map are always related by inclusion. But these two pre x-maps are not related by inclusion. So no sequence of extensions of empty pre x map will see both of them together, and the algorithm will return false because at least one of the read(a) = 3 from one replica will be unsuccessful. To construct hb incrementally, we would need to propagate a partial hb at arbitrary future operations at each replica. Naively, this requires maintaining a pre x map at each read operation which is not included in current pre x map. Although the number of possible pre x maps is polynomially bounded for a given history with a bounded number of replicas, maintaining n pre x maps at each read where n is linear in the size of the history, creates exponentially many possible states to explore. The asymptotic complexity of checking admissibility for a Counter history with a bounded number of replicas remains an open question.

S F

While Theorem . . shows that the admissibility problem is NP-complete for replicated sets and ags even if the number of replicas is xed, we propose a sound algorithm which runs in polynomial time when additionally, the number of values added to the set, or the number of ags, is also xed. Note that this doesn't limit the number of operations in the input history which can still be arbitrarily large. In the following, we focus on the Add-Wins Set, the other cases being very similar.

The algorithm for checking consistency is actually an extension of the one presented in Section . . for replicated counters. The additional complexity in checking consistency for the Add-Wins Set comes from the validity of contains(x) return values which requires identifying the maximal predecessors in the happens-before relation that add or remove x (which are not necessarily the maximal hb-predecessors all-together). In the case of counters, it was enough just to count happens-before predecessors. Therefore, we extend the algorithm for replicated counters such that along with the pre x map, we also keep track of the hb-maximal add(x) and remove(x) operations for each element x and each replica i. When extending a pre x map with a contains operation, these hb-maximal operations (which de ne a witness for the read-from relation) are enough to verify the R V S axiom. Extending the pre x of a replica with an add or remove operation (issued on the same replica), or by merging the pre x of another replica, may require an update of these hb-maximal predecessors.

To represent the maximal hb-predecessors, we use a mapping u, called read-from map, that associates a set of operations add(x) and remove(x) on di erent replicas to each replica i and element x. Note that two operations on the same replica are necessarily related by hb and cannot be both maximal. A pair of pre x-map m and read-from map u de nes a partial read-from relation that associates all the operations in u(x, i) to the last operation of i, i.e., last i (m), if this is a contains(x) operation. For a given read-from relation rf, m, u ⊆ rf denotes the fact that this partial read-from relation is included in rf. A pre x m(i) is called valid in the context of a readfrom map u if it is admitted by the Add-Wins Set with a read-from relation rf such that m, u ⊆ rf. A pair m, u is called valid if m(i) is valid for each replica i.

Algorithm lists our algorithm for checking consistency of Add-Wins Set histories. As for replicated counters, it is de ned as a recursive procedure CheckAWSet that searches for a sequence of valid extensions of a given pre x map and read-from map (initially, both of them are empty) until the pre x map becomes complete.

Input: A history h = (Op, ro), a pre x map m, a read-from map u, and a set seen of invalid pre x map and read-from map pairs. Output: false if there exists no read-from relation rf and happens-before order hb such that m ⊆ hb, m, u ⊆ rf, and h, rf, hb satis es the replicated Add-Wins Set axioms.

if m is complete then return true; The following theorem states the correctness of the algorithm.

foreach replica i do foreach replica j = i do m ← m[i ← m(i) ∪ m(j)]; u (x) ← u(x)[i ← (u(x, i) \ (m(j) \ u(x, j)) ∪ (u(x, j) \ (m(i) \ u(x, i)))]; if m , u ∈ seen and CheckAWSet(h, m , u , seen) then return true; seen ← seen ∪ { m , u }; if ∃o1. ro 1 (lasti(m), o1) then u ← u; if meth(o1) = contains then if ret(o1) = true ⇔ ∃o2 ∈ u(arg(o1), i) st. meth(o2) = add ∧ arg(o2) = arg(o1) then return false; else u (arg(o1), i) ← {o1}; m ← m[i ← m(i) ∪ {o1}]; if m , u ∈

Theorem . . . CheckAWSet(h, ∅, ∅, ∅) returns false if the input history is not consistent for the Add-Wins Set.

When the number of replicas and elements are xed, the number of read-from maps is polynomial in the size of the history -recall that the number of operations associated by a read-from map to a replica and set element is bounded by the number of replicas. Since the possible number of pre x-map and read-from map is polynomial when the number of replicas and elements are xed, the algorithm terminates after exploring polynomially many states. Since the each step of the recursion happens in polynomial time, the algorithm always run in polynomial time in the size of the history when the number of replicas and elements are xed.

I

This algorithm can be shown to be incomplete in a way similar to the Counter case. This corrects a statement we have made in our previous work This work studies the complexity of the admissibility problem for the replicated LWW register. It shows that this problem is NP-complete in general and polynomial time when each value is written only once. Our NP-completeness result is stronger since it assumes a xed number of replicas, and our algorithm for the case of unique values is more general and can be applied uniformly to MVR and RGA. While Bouajjani et al. [ , ] considers the complexity for individual linearizable collection types, we are the rst to establish (in)tractability of individual replicated data types. Others have developed e ective consistency checking algorithms for sequential consistency [ , , , ], serializability [ , , , ], linearizability [ , , , ], and even weaker notions like eventual consistency [ ] and sequential happens-before consistency [ , ]. In contrast, we are the rst to establish precise polynomialtime algorithms for runtime veri cation of replicated data types.

C

In this chapter, we studied various CRDTs, namely Counter, Set, Flag, Registers, Growing Array. We provide novel formal characterizations for these replicated data types, and study the asymptotic complexity of checking conformance for a given execution. We provide polynomial time algorithms for Growing Array and Registers (when the read-from relation is xed). For other data types, we prove NP-completeness results based on polynomial time reductions from SAT problems. Then, we provide sound polynomial time algorithms for Counters, Set, Flag when the number of replicas and/or elements are bounded by a xed constant. Since the latter algorithms are not complete, the asymptotic complexity remains open in these cases.

C T C

In this chapter, we consider the issue of automated testing for transactional databases. More precisely, we focus on the complexity of checking correctness of an execution w.r.t. some transactional consistency model. We consider several consistency models that are the most prevalent in practice:

Read Committed (RC) [ ], Read Atomic (RA) [ ], Causal Consistency (CC) [ ], Pre- fix Consistency (PC) [ ], Snapshot Isolation (SI) [ ],
and Serializability (SER) [ ]. In case of intractability, we introduce algorithms that are polynomial time assuming xed bounds for certain parameters of the input executions, e.g., the number of sessions.

We de ne a new speci cation framework for these consistency models that relies on the fact that the write-read relation in an execution (also known as read-from), relating reads with the transactions that wrote their value, can be de ned e ectively. The write-read relation can be extracted easily from executions where each value is written at most once (a variable can be written an arbitrary number of times). This can be easily enforced by tagging values with unique identiers (e.g., a local counter that is incremented with every new write coupled with a client/session identi er) . Since practical database implementations are data-independent [ ], i.e., their behavior doesn't depend on the concrete values read or written in the transactions, any potential buggy behavior can be exposed in executions where each value is written at most once. Therefore, this assumption is without loss of generality.

Previous work [ , , ] has formalized such consistency models using two auxiliary relations: a visibility relation de ning for each transaction the set of transactions it observes, and a commit order de ning the order in which transactions are committed to the "global" memory. An execution satisfying some consistency model is de ned as the existence of a visibility relation and a commit order obeying certain axioms. In our case, the write-read relation derived from the execution plays the role of the visibility relation. This simpli cation allows us to state a series of axioms de ning these consistency models, which have a common shape. Intuitively, they de ne lower bounds on the set of transactions t 1 that must precede in commit order a transaction t 2 that is read in the execution. Besides shedding a new light on the di erences between these consistency models, these axioms are essential for the algorithmic issues we investigate afterwards.

We establish the precise complexity for checking whether an execution satis es RC, RA, or CC is polynomial time, while the same problem is NP-complete for PC and SI. Moreover, in the case of the NP-complete consistency models (PC, SI, SER), we show that their veri cation problem becomes polynomial time provided that, roughly speaking, the number of sessions in the input executions is considered to be xed (i.e., not counted for in the input size). We extend these results even further by relying on an abstraction of executions called communication graphs [ ]. Roughly speaking, the vertices of a communication graph correspond to sessions, and the edges represent the fact that two sessions access (read or write) the same variable. We show that all these criteria are polynomial-time checkable provided that the biconnected components of the communication graph are of xed size.

We provide an experimental evaluation of our algorithms on executions of CockroachDB [ ], which claims to implement serializability [ ] acknowledging however the possibility of anomalies, Galera [ ], whose documentation contains contradicting claims about whether it implements snapshot isolation [ , ], and AntidoteDB [ ], which claims to implement causal consistency [ ]. Our implementation reports violations of these criteria in all cases. The consistency violations we found for AntidoteDB are novel and have been con rmed by its developers. We show that our algorithms are e cient and scalable. In particular, we show that, although the asymptotic complexity of our algorithms is exponential in general (w.r.t. the number of sessions), the worst-case behavior is not exercised in practice.

The remainder of this chapter is organized as follows:

• Section . de nes a new speci cation framework for describing common transactionalconsistency criteria;

• Section . shows that checking RC, RA, and CC is polynomial time while checking PC and SI is NP-complete;

• Section . and Section . show that PC, SI, and SER are polynomial-time checkable assuming that the communication graph of the input execution has xed-size biconnected components;

• Section . describes an empirical evaluation of our algorithms on executions generated by production databases;

Section . overviews related work, and Section . concludes.

C C H

We consider a transactional database storing a set of variables Var = {x, y, . . .}. Clients interact with the database by issuing transactions formed of read and write operations. Assuming an unspeci ed set of values Val and a set of operation identi ers OId, we let

Op = {read i (x, v), write i (x, v) : i ∈ OId, x ∈ Var, v ∈ Val}
be the set of operations reading a value v or writing a value v to a variable x. We omit operation identi ers when they are not important.

De nition . . . A transaction log t, O, po is a transaction identifier t and a finite set of operations O along with a strict total order po on O, called program order.

x = ;

... ...

read(x);

(a)

x = ;

... ... ...

ABORT;

... The program order po represents the order between instructions in the body of a transaction. We assume that each transaction log is well-formed in the sense that if a read of a variable x is preceded by a write to x in po, then it should return the value written by the last write to x before the read (w.r.t. po). This property is implicit in the de nition of every isolation level or consistency model that we are aware of. For simplicity, we may use the term transaction instead of transaction log and ignore transaction identi er assuming all transaction is uniquely identi ed. The set of all transaction logs is denoted by Tlogs.

We use t, t 1 , t 2 , . . . to range over transactions. The set of read, resp., write, operations in a transaction t is denoted by reads(t), resp., writes(t). The extension to sets of transactions is de ned as usual. Also, we say that a transaction t writes a variable x, denoted by t writes x, when write i (x, v) ∈ writes(t) for some i and v. Similarly, a transaction t reads a variable x when read i (x, v) ∈ reads(t) for some i and v.

To simplify the exposition, we assume that each transaction t contains at most one write operation to each variable , and that a read of a variable x cannot be preceded by a write to x in the same transaction . If a transaction would contain multiple writes to the same variable, then only the last one should be visible to other transactions (w.r.t. any consistency criterion considered in practice). For instance, the read(x) in Figure . a should not return because this is not the last value written to x by the other transaction. It can return the initial value or . Also, if a read would be preceded by a write to the same variable in the same transaction, then it should return a value written in the same transaction (i.e., the value written by the latest write to x in that transaction). For instance, the read(x) in Figure . b can only return (assuming that there are no other writes on x in the same transaction). These two properties can be veri ed easily (in a syntactic manner) on a given execution. Beyond these two properties, the various consistency criteria used in practice constrain only the last writes to each variable in each transaction and the reads that are not preceded by writes to the same variable in the same transaction.

Consistency criteria are formalized on an abstract view of an execution called history. A history includes only successful or committed transactions. In the context of databases, it is always assumed that the e ect of aborted transactions should not be visible to other transactions, and therefore, they can be ignored. For instance, the read(x) in Figure . c should not return the value written by the aborted transaction. The transactions are ordered according to a (partial) session

That is, for every transaction t, and every write(x, v), write(y, v ) ∈ writes(t), we have that x = y. That is, for every transaction t = O, po , if write(x, v) ∈ writes(t) and there exists read(x, v) ∈ reads(t), then we have that read(x, v), write(x, v) ∈ po order so which represents ordering constraints imposed by the applications using the database. Most often, so is a union of sequences, each sequence being called a session. We assume that the history includes a write-read relation that identi es the transaction writing the value returned by each read in the execution. As mentioned before, such a relation can be extracted easily from executions where each value is written at most once. Since in practice, databases are data-independent [ ],

i.e., their behavior does not depend on the concrete values read or written in the transactions, any potential buggy behavior can be exposed in such executions.

De nition . . . A history T, so, wr is a set of transactions T along with a strict partial order so called session order, and a relation wr ⊆ T × reads(T ) called write-read relation, s.t.

• the inverse of wr is a total function, and if (t, read(x, v)) ∈ wr, then write(x, v) ∈ t, and

• so ∪ wr is acyclic.

To simplify the technical exposition, we assume that every history includes a distinguished transaction writing the initial values of all variables. This transaction precedes all the other transactions in so. We use h, h 1 , h 2 , . . . to range over histories.

We say that the read operation read(x, v) reads value v from variable x written by t when (t, read(x, v)) ∈ wr. For a given variable x, wr x denotes the restriction of wr to reads of variable x, i.e. , wr x = wr ∩ (T × {read(x, v) | v ∈ Val}). Moreover, we extend the relations wr and wr x to pairs of transactions as follows: t 1 , t 2 ∈ wr, resp., t 1 , t 2 ∈ wr x , i there exists a read operation read(x, v) ∈ reads(t 2 ) such that t 1 , read(x, v) ∈ wr, resp., t 1 , read(x, v) ∈ wr x . We say that the transaction t 1 is read by the transaction t 2 when t 1 , t 2 ∈ wr, and that it is read when it is read by some transaction t 2 .

A F

We describe an axiomatic framework to characterize the set of histories satisfying a certain consistency criterion. The overarching principle is to say that a history satis es a certain criterion if there exists a strict total order on its transactions, called commit order and denoted by co, which extends the write-read relation and the session order, and which satis es certain properties. These properties are expressed by a set of axioms that relate the commit order with the session-order and the write-read relation in the history.

The axioms we use have a uniform shape: they de ne mandatory co predecessors t 2 of a transaction t 1 that is read in the history. For instance, the criterion called R C (RC) [ ] requires that every value read in the history was written by a committed transaction, and also, that the reads in the same transaction are "monotonic" in the sense that they do not return values that are older, w.r.t. the commit order, than other values read in the past . While the rst condition holds for any history (because of the surjectivity of wr), the second condition is expressed by the axiom Read Committed in Figure . a. This axiom states that for any transaction t 1 writing a variable x that is read in a transaction t, the set of transactions t 2 writing x and read previously in the same transaction must precede t 1 in commit order. For instance, every write is guarded by the acquisition of a lock on the written variable, that is held until the end of the transaction. (e) Causal violation. and a (partial) commit order that does not satisfy this axiom because read(x) returns the value written in a transaction "older" than the transaction read in the previous read(y). An example of a history and commit order satisfying this axiom is given in Figure . b. More precisely, the axioms are rst-order formulas of the following form:

∀x, ∀t 1 , t 2 , ∀α. t 1 = t 2 ∧ t 1 , α ∈ wr x ∧ t 2 writes x ∧ φ(t 2 , α) ⇒ t 2 , t 1 ∈ co ( . )
where φ is a property relating t 2 and α (i.e., the read or the transaction reading from t 1 ) that varies from one axiom to another. Intuitively, this axiom schema states the following: in order for α to read speci cally t 1 's write on x, it must be the case that every t 2 that also writes x and satis es φ(t 2 , α) was committed before t 1 . Note that in all cases we consider, φ(t 2 , α) already ensures that t 2 is committed before the read α, so this axiom schema ensures that t 2 is furthermore committed before t 1 's write.

The axioms used throughout the chapter are given in Figure . . The property φ relates t 2 and α using the write-read relation and the session order in the history, and the commit order.

In the following, we explain the rest of the consistency criteria we consider and the axioms de ning them. R A (RA) [ ] is a strengthening of R C de ned by the axiom Read Atomic, which states that for any transaction t 1 writing a variable x that is read in a transaction t 3 , the set of wr or so predecessors of t 3 writing x must precede t 1 in commit order. The case of wr predecessors corresponds to the Repeatable Read criterion in [ ], which requires that successive reads of the same variable in the same transaction return the same value, Figure . b showing a violation, and also that every read of a variable x in a transaction t returns the value written by the maximal transaction t (w.r.t. the commit order) that is read by t, Figure . d showing a violation (for any commit order between the transactions on the left, either read(x) or read(y) will return a value not written by the maximal transaction). The case of so predecessors corresponds to the "read-my-writes" guarantee [ ] concerning sessions, which states that a transaction t must observe previous writes in the same session. For instance, read(y) returning in Figure . c shows that the last transaction on the right does not satisfy this guarantee: the transaction writing to y was already visible to that session before it wrote to y, and therefore the value should have been read. Read Atomic requires that the so predecessor of the transaction reading y be ordered in co before the transaction writing to y, which makes the union co ∪ wr cyclic.

The following lemma shows that for histories satisfying Read Atomic, the inverse of wr x extended to transactions is a total function. Lemma . . . Let h = T, so, wr be a history. If h, co satisfies Read Atomic, then for every transaction t and two reads read

i 1 (x, v 1 ), read i 2 (x, v 2 ) ∈ reads(t), wr -1 (read i 1 (x, v 1 )) = wr -1 (read i 2 (x, v 2 )) and v 1 = v 2 . Proof. Let t 1 , read i 1 (x, v 1 ) , t 2 , read i 2 (x, v 2 ) ∈ wr x .
Then t 1 , t 2 write to x. Let us assume by contradiction, that t 1 = t 2 . By Read Atomic, t 2 , t 1 ∈ co because t 1 , read i 1 (x, v 1 ) ∈ wr x and t 2 writes to x. Similarly, we can also show that t 1 , t 2 ∈ co. This contradicts the These formulas are interpreted on tuples h, co of a history h and a commit order co on the transactions in h as usual. fact that co is a strict total order. Therefore, t 1 = t 2 . We also have that v 1 = v 2 because each transaction contains a single write to x.

C C (CC)

[ ] is de ned by the axiom Causal, which states that for any transaction t 1 writing a variable x that is read in a transaction t 3 , the set of (wr ∪so) + predecessors of t 3 writing x must precede t 1 in commit order ((wr ∪ so) + is usually called the causal order). A violation of this axiom can be found in Figure . e: the transaction t 2 writing to x is a (wr ∪ so) + predecessor of the transaction t 3 reading from x because the transaction t 4 , writing to y, reads x from t 2 and t 3 reads y from t 4 . This implies that t 2 should precede in commit order the transaction t 1 writing to x, which again, is inconsistent with the write-read relation (t 2 reads from t 1 ). P (PC) [ ] is a strengthening of CC, which requires that every transaction observes a pre x of a commit order between all the transactions. With the intuition that the observed transactions are wr ∪ so predecessors, the axiom Prefix de ning PC, states that for any transaction t 1 writing a variable x that is read in a transaction t 3 , the set of co * predecessors of transactions observed by t 3 writing x must precede t 1 in commit order (we use co * to say that even the transactions observed by t 3 must precede t 1 ). This ensures the pre x property stated above. An example of a PC violation can be found in Figure . f: the two transactions on the bottom read from the three transactions on the top, but any serialization of those three transactions will imply that one of the combinations x= , y= or x= , y= cannot be produced at the end of a pre x in this serialization. S I (SI) [ ] is a strengthening of PC that disallows two transactions to observe the same pre x of a commit order if they conflict, i.e., write to a common variable. It is de ned by the conjunction of Prefix and another axiom called Conflict, which requires that for any transaction t 1 writing a variable x that is read in a transaction t 3 , the set of co * predecessors writing x of transactions con icting with t 3 and before t 3 in commit order, must precede t 1 in commit order. Figure . g shows a Conflict violation.

Finally, S (SER) [ ] is de ned by the axiom with the same name, which requires that for any transaction t 1 writing to a variable x that is read in a transaction t 3 , the set of co predecessors of t 3 writing x must precede t 1 in commit order. This ensures that each transaction observes the e ects of all the co predecessors. The next lemma states the relationship between these axioms.

Lemma . . . The following entailments hold:

Causal ⇒ Read Atomic ⇒ Read Committed Prefix ⇒ Causal Serializability ⇒ Prefix ∧ Conflict
Proof. We will show the contrapositive of each implication:

• If h, co does not satisfy Read Committed, then ∃x, ∃t 1 , t 2 , ∃α, β. t 1 , α ∈ wr x ∧ t 2 writes x ∧ t 2 , β ∈ wr ∧ β, α ∈ po ∧ t 1 , t 2 ∈ co.
Let t 3 the transaction containing α and β. We have that t 2 , t 3 ∈ wr. But then we have t 1 , t 2 , t 3 such that t 1 , t 3 ∈ wr x and t 2 , t 3 ∈ wr and t 2 writes x. So by Read Atomic, t 2 , t 1 ∈ co. This contradicts the fact that co is a strict total order. Therefore, h, co does not satisfy Read Atomic.

• If h, co does not satisfy Read Atomic, then

∃x, ∃t 1 , t 2 , t 3 . t 1 , t 3 ∈ wr x ∧ t 2 writes x ∧ t 2 , t 3 ∈ wr ∪ so ∧ t 1 , t 2 ∈ co.
Then t 2 , t 3 ∈ (wr ∪ so) + . Then, by Causal, we have t 2 , t 1 ∈ co, which contradicts the fact that co is a strict total order. Therefore, h, co does not satisfy Causal.

• If h, co does not satisfy Causal, then ∃x, ∃t 1 , t 2 , t 3 . t 1 , t 3 ∈ wr x ∧ t 2 writes x ∧ t 2 , t 3 ∈ (wr ∪ so) + ∧ t 1 , t 2 ∈ co.

But, (wr ∪ so) + = (wr ∪ so) * • (wr ∪ so) ⊆ co * • (wr ∪ so). Therefore, t 2 , t 3 ∈ co * • (wr ∪ so). Then, by Prefix, we have t 2 , t 1 ∈ co, which contradicts the fact that co is a strict total order. Therefore, h, co does not satisfy Prefix. t 4 , t 3 ∈ (wr ∪ so) if it violates Prefix.

In both cases, we have that t 4 , t 3 ∈ co. Because co is transitive, t 2 , t 4 ∈ co * and t 4 , t 3 ∈ co imply that t 2 , t 3 ∈ co. Then by Serializability, we have t 2 , t 1 ∈ co, which contradicts the fact that co is a strict total order. Therefore, h, co does not satisfy Serializability. De nition . . . Given a set of axioms X defining a criterion C like in Table . , a history h = T, so, wr satis es C i there exists a strict total order co such that wr ∪ so ⊆ co and h, co satisfies X.

Checking Transactional Consistency

De nition . . and Lemma . . imply that each consistency criterion in Table . is stronger than its predecessors (reading them from top to bottom), e.g., CC is stronger than RA and RC. This relation is known to be strict [ ], e.g., RA is not stronger than CC.

C C C

This section establishes the complexity of checking the di erent consistency criteria in Table .  for a given history. More precisely, we show that R C , R A , and C C can be checked in polynomial time while the problem of checking the rest of the criteria is NP-complete.

Intuitively, the polynomial time results are based on the fact that the axioms de ning those consistency criteria do not contain the commit order (co) on the left-hand side of the entailment. Therefore, proving the existence of a commit order satisfying those axioms can be done using a saturation procedure that builds a "partial" commit order based on instantiating the axioms on the write-read relation and the session order in the given history. Since the commit order must be an extension of the write-read relation and the session order, it contains those two relations from the beginning. This saturation procedure stops when the order constraints derived this way become cyclic. For instance, let us consider applying such a procedure corresponding to RA on the histories in b on the rst history, since the transaction on the right reads from y, we get that its wr x predecessor (i.e., the rst transaction on the left) must precede the transaction writing to y in commit order (the red edge). This holds because the wr x predecessor writes on y. Similarly, since the same transaction reads from x, we get that its wr y predecessor must precede the transaction writing to x in commit order (the blue edge). This already implies a cyclic commit order, and therefore, this history does not satisfy RA. On the other hand, for the history in Figure . b, all the axiom instantiations are vacuous, i.e., the left part of the entailment is false, and therefore, it satis es RA. Checking CC on the history in Figure . c requires a single saturation step: since the transaction on the bottom right reads from x, its wr x • wr y predecessor that writes on x (the transaction on the bottom left) must precede in commit order the transaction writing to x. Since this is already inconsistent with the session order, we get that this history violates CC. Algorithm : Checking C .

Algorithm lists our procedure for checking CC. As explained above, co is initially set to so ∪ wr, and then, it is saturated with other ordering constraints implied by non-vacuous instantiations of the axiom Causal (where the left-hand side of the implication evaluates to true). The algorithms concerning RC and RA are de ned in a similar way by essentially changing the test at line so that it corresponds to the left-hand side of the implication in the corresponding axiom. Algorithm can be rewritten as a Datalog program containing straightforward Datalog rules for computing transitive closures and relation composition, and a rule of the form

t 2 , t 1 ∈ co :-t 1 = t 2 , t 1 , t 3 ∈ wr x , t 2 , t 3 ∈ (so ∪ wr) +
to represent the Causal axiom. The following is a consequence of the fact that these algorithms run in polynomial time (or equivalently, the corresponding Datalog programs can be evaluated in polynomial time over a database that contains the wr and so relations in a given history).

Theorem . . . For any criterion C ∈ {R

C , R A , C }, the problem of checking whether a given history satisfies C is polynomial time.

On the other hand, checking PC, SI, and SER is NP-complete in general. We show this using a reduction from boolean satis ability (SAT) that covers uniformly all the three cases. In the case of SER, it provides a new proof of the NP-completeness result by [ ], which uses a reduction from the so-called non-circular SAT and which cannot be extended to PC and SI.

Theorem . . . For any criterion C ∈ {P

C , S I , S } the problem of checking whether a given history satisfies C is NP-complete.

Proof. Given a history, any of these three criteria can be checked by guessing a total commit order on its transactions and verifying whether it satis es the corresponding axioms. This shows that the problem is in NP.

We write Datalog rules using a standard notation head :body where head is a relational atom (written as a, b ∈ R where a, b are elements and R a binary relation) and body is a list of relational atoms. To show NP-hardness, we de ne a reduction from boolean satis ability. Therefore, let ϕ = D 1 ∧ . . . ∧ D m be a CNF formula over the boolean variables x 1 , . . . , x n where each D i is a disjunctive clause with m i literals. Let λ ij denote the j-th literal of D i .

a k b k w ij y ij writes v ij z ij z i,j-1 y i,j+1 co co co co wr v ij so so so so (a) λij = xk b k a k w ij y ij writes v ij z ij z i,j-1 y i,j+1 co co co co wr v ij
We construct a history h ϕ such that ϕ is satis able if and only if h ϕ satis es PC, SI, or SER. Since SER ⇒ SI ⇒ PC, we show that ( ) if h ϕ satis es PC, then ϕ is satis able, and ( ) if ϕ is satis able, then h ϕ satis es SER.

C

h ϕ The main idea of the construction is to represent truth values of each of the variables and literals in ϕ with the polarity of the commit order between corresponding transaction pairs. For each variable x k , h ϕ contains a pair of transactions a k and b k , and for each literal λ ij , h ϕ contains a set of transactions w ij , y ij and z ij . We want to have that x k is false if and only if a k , b k ∈ co, and λ ij is false if and only if y ij , z ij ∈ co (the transaction w ij is used to "synchronize" the truth value of the literals with that of the variables, which is explained later).

The history h ϕ should ensure that the co ordering constraints corresponding to an assignment that falsi es the formula (i.e. one of its clauses) form a cycle. To achieve that, we add all pairs z ij , y i,(j+1)%m i in the session order so. An unsatis ed clause D i , i.e. every λ ij is false, leads to a cycle of the form

y i1 co -→ z i1 so -→ y i2 co -→ z i2 • • • z im i so -→ y i1 .
The most complicated part of the construction is to ensure some consistency between the truth value of the literals and the truth value of the variables, e.g., λ ij = x k is true i x k is true, for at least one literal λ ij interpreted as true in every clause D i (if such a literal exists).

PC

h ϕ ϕ If h ϕ satis es PC, then there exists a total commit order co between the transactions described above, which together with h ϕ satis es Prefix. We show that the assignment of the variables x k explained above (de ned by the co order between a k and b k , for each k) satis es the formula ϕ. For each clause D i , the so constraints between the We assume that the transactions a k and b k associated to a variable x k are distinct and di erent from the transactions associated to another variable x k = x k or to a literal λij. Similarly, for the transactions wij, yij and zij associated to a literal λij.

transactions y ij , z ij with 1 ≤ j ≤ m i imply that there exist some z ij that is committed before its corresponding y ij . These two transactions are included in the sub-history corresponding to the literal λ The de nition of this sub-history ensures that the interpretation to true of the literal λ ij (given by the order in co between z ij and y ij ) is consistent with the assignment of the variable it contains (de ned by the co order between a k , b k ). More precisely, it ensures that if the co goes upwards on the left-hand side ( z ij , y ij ∈ co) like in this case, then it must also go upwards on the righthand side ( b k , a k ∈ co in the case of a positive literal, and a k , b k ∈ co in the case of a negative literal) to satisfy Prefix. For instance, if λ ij = x k is a positive literal and we assume by contradiction that a k , b k ∈ co, then y ij , w ij ∈ so • co • so. Therefore, for every commit order co such that h ϕ , co satis es Prefix, a k , b k ∈ co implies y ij , z ij ∈ co, which contradicts the hypothesis. Indeed, if a k , b k ∈ co, instantiating the Prefix axiom where y ij plays the role of t 2 , z ij plays the role of t 1 , and w ij plays the role of t 3 , we obtain that y ij , z ij ∈ co.

Therefore, the assignment of the variables x k leads to at least one literal interpreted to true in each clause D i , and the formula ϕ is satis able.

S

ϕ SER h ϕ Let γ be a satisfying assignment for ϕ. Also, let co be a binary relation that includes so and wr such that if γ( Note that co is acyclic: no cycle can contain w ij because w ij has no "outgoing" dependency (i.e. co contains no pair with w ij as a rst component), there is no cycle including some pair of transactions a k , b k and some pair y ij , z ij because there is no way to reach y ij or z ij from a k or b k , there is no cycle including only transactions a k and b k because a k 1 and b k 1 are not related to a k 2 and b k 2 , for k 1 = k 2 , there is no cycle including transactions y i 1 ,j 1 , z i 1 ,j 1 and y i 2 ,j 2 , z i 2 ,j 2 for i 1 = i 2 since these are disconnected as well, and nally, there is no cycle including only transactions y ij and z ij , for a xed i, because ϕ is satis able. It can be proved easily that the acyclic relation co can be extended to a total commit order co which together with h ϕ satis es the Serializability axiom. Therefore, h ϕ satis es SER.

x k ) = false, then a k , b k ∈ co , y ij , z ij ∈ co for each λ ij = x k , and z ij , y ij ∈ co for each λ ij = ¬x k , and if γ(x k ) = true, then b k , a k ∈ co , z ij , y ij ∈ co for each λ ij = x k ,

C C B W H

In this section, we show that checking pre x consistency, snapshot isolation, and serializability becomes polynomial time under the assumption that the width of the given history, i.e., the maximum number of mutually-unordered transactions w.r.t. the session order, is bounded by a xed constant. If we consider the standard case where the session order is a union of transaction sequences (modulo the ctitious transaction writing the initial values), i.e., a set of sessions, then the width of the history is the number of sessions. We start by presenting an algorithm for checking serializability that is polynomial time when the width is bounded by a xed constant. In general, the asymptotic complexity of this algorithm is exponential in the width of the history, but this worstcase behavior is not exercised in practice as shown in Section . . Then, we prove that checking

Checking Transactional Consistency (b) Figure . : Applying the serializability checking algorithm checkSER (Algorithm ) on the serializable history on the left. The right part pictures a search for valid extensions of serializable pre xes, represented by their boundaries. The red arrow means that the search is blocked (the pre x at the target is not a valid extension), while blue arrows mean that the search continues.

pre x consistency and snapshot isolation can be reduced in polynomial time to the problem of checking serializability.

C S

We present an algorithm for checking serializability of a given history which constructs a valid commit order (satisfying Serialization), if any, by "linearizing" transactions one by one in an order consistent with the session order. At any time, the set of already linearized transactions is uniquely determined by an antichain of the session order (i.e., a set of mutually-unordered transactions w.r.t. so), and the next transaction to linearize is chosen among the immediate so successors of the transactions in this antichain. The crux of the algorithm is that the next transaction to linearize can be chosen such that it does not produce violations of Serialization in a way that does not depend on the order between the already linearized transactions. Therefore, the algorithm can be seen as a search in the space of so antichains. If the width of the history is bounded (by a xed constant), then the number of possible so antichains is polynomial in the size of the history, which implies that the search can be done in polynomial time.

A prefix of a history h = T, so, wr is a set of transactions T ⊆ T such that all the so predecessors of transactions in T are also in T , i.e., ∀t ∈ T. so -1 (t) ∈ T . A pre x T is uniquely determined by the set of transactions in T that are maximal w.r.t. so. This set of transactions forms an antichain of so, i.e., any two elements in this set are incomparable w.r.t. so. Given an antichain {t 1 , . . . , t n } of so, we say that {t 1 , . . . , t n } is the boundary of the pre x T = {t : ∃i. t, t i ∈ so ∨ t = t i }. For instance, given the history in Figure . a, the set of transactions {t 0 , t 1 , t 2 } is a pre x with boundary {t 1 , t 2 } (the latter is an antichain of the session order).

A pre x T of a history h is called serializable i there exists a partial commit order co on the transactions in h such that the following hold:

• co does not contradict the session order and the write-read relation in h, i.e., wr ∪ so ∪ co is acyclic,

• co is a total order on transactions in T ,

• co orders transactions in T before transactions in T \ T , i.e., t 1 , t 2 ∈ co for every t 1 ∈ T and t 2 ∈ T \ T ,

• co does not order any two transactions t 1 , t 2 ∈ T

• the history h along with the commit order co satis es the axiom de ning serializability, i.e., h, co |= Serialization.

For the history in Figure . a, the pre x {t 0 , t 1 , t 2 } is serializable since there exists a partial commit order co that orders t 0 , t 1 , t 2 in this order, and both t 1 and t 2 before t 3 and t 4 . The axiom Serialization is satis ed trivially, since the pre x contains a single transaction writing x and all the transactions outside of the pre x do not read x.

A pre x T {t} of h is called a valid extension of a serializable pre x T of h, denoted by T T {t}if:

• t does not read from a transaction outside of T , i.e., for every t ∈ T \ T , t , t ∈ wr, and

• for every variable x written by t, there exists no transaction t 2 = t outside of T that reads a value of x written by a transaction t 1 in T , i.e., for every x written by t and every t 1 ∈ T and t 2 ∈ T \ (T {t}), t 1 , t 2 ∈ wr.

For the history in Figure . a, we have {t 0 , t 1 } {t 0 , t 1 } {t 2 } because t 2 reads from t 0 and it does not write any variable. On the other hand {t 0 , t 1 } {t 0 , t 1 } {t 3 } because t 3 writes x and the transaction t 2 , outside of this pre x, reads from the transaction t 0 included in the pre x.

Let * denote the re exive and transitive closure of .

The following lemma is essential in proving that iterative valid extensions of the initial empty pre x can be used to show that a given history is serializable.

Lemma . . . For a serializable prefix T of a history h, a prefix T

{t} is serializable if it is a valid extension of T .

Proof. Let co be the partial commit order for T which satis es the serializable pre x conditions. We extend co to a partial order co = co ∪ { t, t |t ∈ T {t }}. We show that h, co |= Serialization. The other conditions for T {t} being a serializable pre x are satis ed trivially by co.

Assume by contradiction that h, co does not satisfy the axiom Serialization. Then, there exists t 1 , t 2 , t 3 , x ∈ vars(h) s.t. t 1 , t 3 ∈ wr x and t 2 writes on x and t 1 , t 2 , t 2 , t 3 ∈ co. Since h, co satis es this axiom, at least one of these two co ordering constraints are of the form t, t where t ∈ T {t}:

• the case t 1 = t and t 2 ∈ T {t} is not possible because co contains no pair of the form t , _ ∈ co with t ∈ T (recall that t 2 , t 3 should be also included in co).

• If t 2 = t then, t 1 , t 2 ∈ co and t 2 , t 3 for some t 3 ∈ T {t}. But, by the de nition of valid extension, for all variables x written by t, there exists no transaction t 3 ∈ T {t} such that it reads x from t 1 ∈ T . Therefore, this is also a contradiction. Algorithm lists our algorithm for checking serializability. It is de ned as a recursive procedure that searches for a sequence of valid extensions of a given pre x (initially, this pre x is empty) until covering the whole history.

Theorem . . . A history h is serializable i checkSER(h, ∅) returns true.

Proof. The "if" direction is a direct consequence of Lemma . . . For the reverse, assume that h = T, so, wr is serializable with a (total) commit order co. Let co i be the set of transactions in the pre x of co of length i. Since co is consistent with so, we have that co i is a pre x of h, for any i. We show by induction that co i+1 is a valid extension of co i . The base case is trivial. For the induction step, let t be the last transaction in the pre x of co of length i + 1. Then,

• t cannot read from a transaction outside of co i because co is consistent with the write-read relation wr,

• also, for every variable x written by t, there exists no transaction t 2 = t outside of co i that reads a value of x written by a transaction t 1 ∈ co i . Otherwise, t 1 , t 2 ∈ wr x , t, t 2 ∈ co, and t 1 , t ∈ co which implies that h, co does not satisfy Serializability.

This implies that checkSER(h, ∅) returns true.

Algorithm enumerates pre xes of the given history h, each pre x being uniquely determined by an antichain of h containing the so-maximal transactions in that pre x. By de nition, the size of each antichain of a history h is smaller than the width of h. Therefore, the number of possible antichains (pre xes) of a history h is O(size(h) width(h) ) where size(h), resp., width(h), is the number of transactions, resp., the width, of h. Since the valid extension property can be checked

We assume that t ∈ T which is implied by the use of the disjoint union . in quadratic time, the asymptotic time complexity of the algorithm de ned by checkSER is upper bounded by O(size(h) width(h) •size(h) 3 ). The following corollary is a direct consequence of these observations. Corollary . . . For an arbitrary but fixed constant k ∈ N, the problem of checking serializability for histories of width at most k is polynomial time.

R P C S

We describe a polynomial time reduction of checking pre x consistency of bounded-width histories to the analogous problem for serializability. Intuitively, as opposed to serializability, pre x consistency allows that two transactions read the same snapshot of the database and commit together even if they write on the same variable. Based on this observation, given a history h for which we want to check pre x consistency, we de ne a new history h R|W where each transaction t is split into a transaction performing all the reads in t and another transaction performing all the writes in t (the history h R|W retains all the session order and write-read dependencies of h). We show that if the set of read and write transactions obtained this way can be shown to be serializable, then the original history satis es pre x consistency, and vice-versa. For instance, Figure . shows this transformation on the two histories in Figure . a and Figure . c, which represent typical anomalies known as "long fork" and "lost update", respectively. The former is not admitted by PC while the latter is admitted. It can be easily seen that the transformed history corresponding to the "long fork" anomaly is not serializable while the one corresponding to "lost update" is serializable. We show that this transformation leads to a history of the same width, which by Corollary . . , implies that checking pre x consistency of bounded-width histories is polynomial time. Thus, given a history h = T, wr, so , we de ne the history h R|W = T , wr , so as follows:

• T contains a transaction R t , called a read transaction, and a transaction W t , called a write transaction, for each transaction t in the original history, i.e., T = {R t |t ∈ T }∪{W t |t ∈ T }

• the write transaction W t writes exactly the same set of variables as t, i.e., for each variable x, W t writes to x i t writes to x.

• the read transaction R t reads exactly the same values and the same variables as t, i.e., for each variable x,

wr x = { W t 1 , R t 2 | t 1 , t 2 ∈ wr x }
• the session order between the read and the write transactions corresponds to that of the original transactions and read transactions precede their write counterparts, i.e.,

so = { R t , W t |t ∈ T } ∪ { R t 1 , R t 2 , R t 1 , W t 2 , W t 1 , R t 2 , W t 1 , W t 2 | t 1 , t 2 ∈ so}
The following lemma is a straightforward consequence of the de nitions. so so (d) Lost update (transformed) Figure . : Reducing PC to SER. Initially, the value of every variable is . Next, we show that h R|W is serializable if h is pre x consistent. Formally, we show that

Lemma . . . The histories

W t 1 W t 2 co + 1 co + 1 co 1 (a) Wt 1 , Wt 2 ∈ co 1 W t 1 W t 2 co + 1 co + 1 co 1 (b) Wt 2 , Wt 1 ∈ co 1
∀co. ∃co . h, co |= Prefix ⇒ h R|W , co |= Serializability
Thus, let co be a commit (total) order on transactions of h which together with h satis es the pre x consistency axiom. We de ne two partial commit orders co 1 and co 2 , co 2 a strengthening of co 1 , which we prove that they are acyclic and that any linearization co of co 2 is a valid witness for h R|W satisfying serializability. Thus, let co 1 be a partial commit order on transactions of h R|W de ned as follows:

co 1 = { R t , W t |t ∈ T } ∪ { W t 1 , W t 2 | t 1 , t 2 ∈ co} ∪ { W t 1 , R t 2 | t 1 , t 2 ∈ wr ∪ so}
We show that if co 1 were to be cyclic, then it contains a minimal cycle with one read transaction, and at least one but at most two write transactions. Then, we show that such cycles cannot exist.

Lemma . . . The relation co 1 is acyclic.

P

We rst show that if co 1 were to be cyclic, then it contains a minimal cycle with one read transaction, and at least one but at most two write transactions. Then, we show that such cycles cannot exist. Therefore, let us assume that co 1 is cyclic. Then,

• Since W t 1 , W t 2 ∈ co 1 implies t 1 , t 2 ∈ co, for every t 1 and t 2 , a cycle in co 1 cannot contain only write transactions. Otherwise, it will imply a cycle in the original commit order co. Therefore, a cycle in co 1 must contain at least one read transaction.

• Assume that a cycle in co 1 contains two write transactions W t 1 and W t 2 which are not consecutive, like in Figure . . Since either W t 1 , W t 2 ∈ co 1 or W t 1 , W t 2 ∈ co 1 , there exists a smaller cycle in co 1 where these two write transactions are consecutive. If W t 1 , W t 2 ∈ co 1 , then co 1 contains the smaller cycle on the lower part of the original cycle (Figure . a), and if W t 2 , W t 1 ∈ co 1 , then co 1 contains the cycle on the upper part of the original cycle (Figure . b). Thus, all the write transactions in a minimal cycle of co 1 must be consecutive.

• If a minimal cycle were to contain three write transactions, then all of them cannot be consecutive unless they all three form a cycle, which is not possible. So a minimal cycle contains at most two write transactions.

• Since co 1 contains no direct relation between read transactions, it cannot contain a cycle with two consecutive read transactions, or only read transactions.

This shows that a minimal cycle of co 1 would include a read transaction and a write transaction, and at most one more write transaction. We prove that such cycles are however impossible:

• if the cycle is of size , then it contains two transactions

W t 1 and R t 2 such that W t 1 , R t 2 ∈ co 1 and R t 2 , W t 1 ∈ co 1 . Since all the R _ , W _ dependencies in co 1 are of the form R t , W t , it follows that t 1 = t 2 . Then, we have W t 1 , R t 1 ∈ co 1 which implies t 1 , t 1 ∈ wr ∪ so, a contradiction.
• if the cycle is of size , then it contains three transactions W t 1 , W t 2 , and R t 3 such that

W t 1 , W t 2 ∈ co 1 , W t 2 , R t 3 ∈ co 1 , and R t 3 , W t 1 ∈ co 1 .
Using a similar argument as in the previous case, R t 3 , W t 1 ∈ co 1 implies t 3 = t 1 . Therefore, t 1 , t 2 ∈ co and t 2 , t 1 ∈ wr ∪ so, which contradicts the fact that wr ∪ so ⊆ co.

We de ne a strengthening of co 1 where intuitively, we add all the dependencies from read transactions t 3 to write transactions t 2 that "overwrite" values read by t 3 . Formally, co 2 = co 1 ∪ RW(co 1 ) where

RW(co 1 ) = { t 3 , t 2 |∃x ∈ vars(h). ∃t 1 ∈ T . t 1 , t 3 ∈ wr x , t 1 , t 2 ∈ co 1 , t 2 writes x}
It can be shown that any cycle in co 2 would correspond to a Prefix violation in the original history. Therefore, Lemma . . . The relation co 2 is acyclic.

Proof. Assume that co 2 is cyclic. Any minimal cycle in co 2 still satis es the properties of minimal cycles of co 1 proved in Lemma . . (because all write transactions are still totally ordered and co 2 doesn't relate directly read transactions). So, a minimal cycle in co 2 contains a read transaction and a write transaction, and at most one more write transaction.

Since co 1 is acyclic, a cycle in co 2 , and in particular a minimal one, must necessarily contain a dependency from RW(co 1 ). Note that a minimal cycle cannot contain two such dependencies since this would imply that it contains two non-consecutive write transactions. The red edges in Figure . a show a minimal cycle of co 2 satisfying all the properties mentioned above. This cycle

W t 1 R t 3 W t 2 writes x W t 4 wr x co * 1 co 1 co 1 R W ( c o 1 ) (a)
W t 1 , W t 2 ∈ co 1 and W t 2 , W t 4 ∈ co * 1 imply t 1 , t 2 ∈ co and t 2 , t 4 ∈ co * , respectively, W t 1 , W t 3 ∈ wr x implies t 1 , t 3 ∈ wr x , and W t 4 , R t 3 ∈ co 1 implies t 4 , t 3 ∈ wr ∪ so.
This implies that h, co doesn't satisfy the Prefix axiom, a contradiction.

Lemma . . . If a history h satisfies prefix consistency, then h R|W is serializable.

Proof. Let co be any total order consistent with co 2 . Assume by contradiction that h R|W , co doesn't satisfy Serializability. Then, there exist t 1 , t 2 , t 3 ∈ T such that t 1 , t 2 , t 2 , t 3 ∈ co and t 1 , t 2 write on some variable x and t 1 , t 3 ∈ wr x . But then t 1 , t 2 are write transactions and co 1 must contain t 1 , t 2 . Therefore, RW(co 1 ) and co 2 should contain t 3 , t 2 , a contradiction with co being consistent with co 2 .

Finally, it can be proved that any linearization co of co 2 satis es Serializability (together with h R|W ). Moreover, it can also be shown that the serializability of h R|W implies that h satis es PC. Therefore,

Theorem . . . A history h satisfies prefix consistency i h R|W is serializable.

P

The "only-if" direction is proven by Lemma . . . For the reverse, we show that

∀co . ∃co. h R|W , co |= Serializability ⇒ h, co |= Prefix
Thus, let co be a commit (total) order on transactions of h R|W which together with h R|W satis es the serializability axiom. Let co be a commit order on transactions of h de ned by co = { t 1 , t 2 | W t 1 , W t 2 ∈ co } (co is clearly a total order). If co were not to be consistent with wr ∪ so, then there would exist transactions t 1 and t 2 such that t 1 , t 2 ∈ wr ∪ so and t 2 , t 1 ∈ co, which would imply that W t 1 , R t 2 , R t 2 , W t 2 ∈ wr ∪ so and W t 2 , W t 1 ∈ co , which violates the acylicity of co . We show that h, co satis es Prefix. Assume by contradiction that there exists a Prefix violation between t 1 , t 2 , t 3 , t 4 (shown in Figure . a), i.e., for some x ∈ vars(h), t 1 , t 3 ∈ wr x and t 2 writes x, t 1 , t 2 ∈ co, t 2 , t 4 ∈ co * and t 4 , t 3 ∈ wr ∪ so. Then, the corresponding transactions W t 1 , W t 2 , W t 4 , R t 3 in h R|W would be related as follows: W t 1 , W t 2 ∈ co and W t 1 , R t 3 ∈ wr x because t 1 , t 3 ∈ wr x and t 1 , t 2 ∈ co. Since co satis es Serializability, then R t 3 , W t 2 ∈ co . But t 2 , t 4 ∈ co * and t 4 , t 3 ∈ wr ∪ so imply that W t 2 , W t 4 ∈ co * and W t 4 , R t 3 ∈ wr ∪ so , which show that co is cyclic (the red cycle in Figure . b), a contradiction.

Since the history h R|W can be constructed in linear time, Lemma . . , Theorem . . , and Corollary . . imply the following result.

Corollary . . . For an arbitrary but fixed constant k ∈ N, the problem of checking prefix consistency for histories of width at most k is polynomial time.

R S I S

We extend the reduction of pre x consistency to serializability to the case of snapshot isolation.

Compared to pre x consistency, snapshot isolation disallows transactions that read the same snapshot of the database to commit together if they write on a common variable (stated by the Conflict axiom). More precisely, for any pair of transactions t 1 and t 2 writing to a common variable, t 1 must observe the e ects of t 2 or vice-versa. We re ne the de nition of h R|W such that any "serialization" (i.e.., commit order satisfying Serializability) disallows that the read transactions corresponding to two such transactions are ordered both before their write counterparts. We do this by introducing auxiliary variables that are read or written by these transactions. For instance, Figure . shows this transformation on the two histories in Figure . a and Figure . c, which represent the anomalies known as "lost update" and "write skew", respectively. The former is not admitted by SI while the latter is admitted. Concerning "lost update", the read counterpart of the transaction on the left writes to a variable x that is read by its write counterpart, but also written by the write counterpart of the other transaction. This forbids that the latter is serialized in between the read and write counterparts of the transaction on the left. A similar scenario is imposed on the transaction on the right, which makes that the transformed history is not serializable. Concerning the "write skew" anomaly, the transformed history is exactly as for the PC reduction since the two transactions don't write on a common variable. It is clearly serializable. For a history h = T, wr, so , the history h c R|W = T , wr , so is de ned as h R|W with the following additional construction: for every two transactions t 1 and t 2 ∈ T that write on a common variable,

• R t 1 and W t 2 (resp., R t 2 and W t 1 ) write on a variable x 1,2 (resp., x 2,1 ),

• the write transaction of t i reads x i,j from the read transaction of t i , for all i = j ∈ {1, 2}, i.e., wr Note that h R|W and h c R|W have the same width (the session order is de ned exactly in the same way), which implies, by Lemma . . , that h and h c R|W have the same width. The following result can be proved using similar reasoning as in the case of pre x consistency.

x 1,2 = { R t 1 , W t 1 } and wr x 2,1 = { R t 2 , W t 2 }.

Theorem . . . A history h satisfies snapshot isolation i h c

R|W is serializable. Note that h c R|W and h have the same width, and that h c R|W can be constructed in linear time. Therefore, Theorem . . , and Corollary . . imply the following result.

Corollary . . . For an arbitrary but fixed constant k ∈ N, the problem of checking snapshot isolation for histories of width at most k is polynomial time.

C

In this section, we present an extension of the polynomial time results for PC, SI, and SER, which allows to handle histories where the sharing of variables between di erent sessions is sparse. For the results in this section, we take the simplifying assumption that the session order is a union of transaction sequences (modulo the ctitious transaction writing the initial values), i.e., each transaction sequence corresponding to the standard notion of session . We represent the sharing of variables between di erent sessions using an undirected graph called a communication graph. For instance, the communication graph of the history in Figure . a is given in Figure . b. For readability, the edges are marked with the variables accessed by the two sessions.

We show that the problem of checking PC, SI, or SER is polynomial time when the size of every biconnected component of the communication graph is bounded by a xed constant. This is stronger than the results in Section . because the number of biconnected components can be arbitrarily large which means that the total number of sessions is unbounded. In general, we prove that the time complexity of these consistency criteria is exponential only in the maximum size of such a biconnected component, and not the whole number of sessions.

An undirected graph is biconnected if it is connected and if any one vertex were to be removed, the graph will remain connected, and a biconnected component of a graph G is a maximal biconnected subgraph of G. Figure . b shows the decomposition in biconnected components of a communication graph. This graph contains sessions while every biconnected component is of size at most . Intuitively, if a history h is a violation to some consistency criterion C ∈ {PC, SI, SER}, then there exists a projection of h on sessions from the same biconnected

The results can be extended to arbitrary session orders by considering maximal transaction sequences in session order instead of sessions. component which is also a violation to C (the reverse is trivially true). Therefore, checking any of these criteria can be done in isolation for each biconnected component (more precisely, on sub-histories that contain only sessions in the same biconnected component). Actually, this decomposition argument works even for RC, RA, and CC. For instance, in the case of the history in Figure . a, any consistency criterion can be checked looking in isolation at three sub-histories: a sub-history with S 1 and S 2 , a sub-history with S 2 , S 3 , and S 4 , and a sub-history with S 4 and S 5 . Formally, a communication graph of a history h is an undirected graph Comm(h) = (V, E) where the set of vertices V is the set of sessions in h, and (v, v ) ∈ E i the sessions v and v contain two transactions t 1 and t 2 , respectively, such that t 1 and t 2 read or write a common variable x.

We begin with a technical lemma showing that minimal paths of certain form in the graph representing a history h and a relation co (on the transactions of h) lie within a single biconnected component of the underlying communication graph. This is used to show that any consistency violation can be exposed by looking at a single biconnected component at a time. The graph representing a history h and a relation co on the transactions of h is denoted by G(h, co) .

Given a graph G(h, co) and a relation r on its vertices, a term over the relations so, wr, and co, e.g., (wr ∪ so) + , a path of the form r (or an r-path) is a sequence of edges representing so, wr, or co dependencies as speci ed by the term r, e.g., a sequence of wr or so dependencies. Lemma . . . Let B 1 ,. . .,B n be the biconnected components of Comm(h) for a history h = T, wr, so . For each B i , let co i be a total order on the transactions of B i extending the session order so on the transactions of B i . Also, let co = i co i . Then, for every term r ∈ {co + , (wr ∪ so) + }, any minimal r-path in the graph G(h, co) between two transactions from the same biconnected component includes only transactions of that biconnected component.

P

We consider the case r = co + . Consider a minimal co + -path π = t 0 , . . . , t n between two transactions t 0 and t n from the same biconnected component B of Comm(h) (i.e., from sessions in B). Assume by contradiction, that π traverses multiple biconnected components. We de ne a path π s = v 0 , . . . , v m between sessions, i.e., vertices of Comm(h), which contains an edge (v j , v j+1 ) i π contains an edge (t i , t i+1 ) with t i a transaction of session v j and t i+1 a transaction of session v j+1 = v j . Since any graph decomposes to a forest of biconnected components, this path must necessarily leave and enter some biconnected component B 1 to and from

The transaction writing the initial values is considered as a distinguished session. The nodes of G(h, co) correspond to transactions in h and the edges connect pairs of transactions in so, wr, or co. That is, transactions that are included in the sessions in Bi. the same biconnected component B 2 , i.e., π s must contain two vertices v j 1 and v j 2 in B 1 such that the successor v j 1 +1 of v j 1 and the predecessor v j 2 -1 of v j 2 are from B 2 . Let t 1 , t 2 , t 3 , t 4 be the transactions in the path π corresponding to v j 1 , v j 2 , v j 1 +1 , and v j 2 -1 , respectively. Now, since any two biconnected components share at most one vertex, it follows that t 3 and t 4 are from the same session and

t 3 t 4 t 1 t 2 B 2 B 1 co + 2 co * 1 co * 1 co + 2 so (a) t3, t4 ∈ so t 3 t 4 t 1 t 2 B 2 B 1 co + 2 co * 1 co * 1 co + 2 so (b) t4, t3 ∈ so
• if t 3 , t 4 ∈ so, then there exists a shorter path between t 0 and t 1 that uses the so relation between t 3 , t 4 (we recall that so ⊆ i co i ) instead of the transactions in B 2 , pictured in Figure . a, which is a contradiction to the minimality of π,

• if t 4 , t 3 ∈ so, then, we have a cycle in i co i ∪ so, pictured in Figure . b, which is also a contradiction.

The case r = (wr ∪ so) + can be proved in a similar manner since the reasoning outlined in Figure . reduces to short-circuiting a path using a single so edge (and so is included in (wr ∪ so) + ). Now we prove our nal claim. For a history h = (T, so, wr) and biconnected component B of Comm(h), the projection of h over transactions in sessions of B is denoted by h ↓ B, i.e., h ↓ B = (T , so , wr ) where T is the set of transactions in sessions of B, so and wr are the projections of so and wr, respectively, on T .

Theorem . . . For any criterion C ∈ {RA, RC, CC, PC, SI, SER}, a history h satisfies

C i for every biconnected component B of Comm(h), h ↓ B satisfies C.
Proof. The "only-if" direction is obvious. For the "if" direction, we rst consider the cases C ∈ {RA, RC, CC, SER}. The proof concerning PC and SI is based on the reduction to SER outlined in Section . . and Section . . , respectively, and it is given afterwards. Let B 1 ,. . .,B n be the biconnected components of Comm(h).

Let C ∈ {RA, RC, CC, SER}, and let co i be the commit order that witnesses that h ↓ B i satis es C, for each 1 ≤ i ≤ n. The union i co i is acyclic since otherwise, any minimal cycle would be a minimal path between transactions of the same biconnected component B j , and, by Lemma . . , it will include only transactions of B j which is a contradiction to co j being a total order. We show that any linearization co of i co i along with h satis es the axioms of C. The axioms de ning RA, RC, CC, and SER involve transactions that write or read a common variable, which implies that they belong to the same biconnected component (we refer to the transactions t 1 , t 2 , and t 3 in Figure . ). Furthermore, by Lemma . . , minimal paths witnessing the dependencies in those axioms, e.g., (wr ∪ so) + for CC, are also formed of transactions included in the same biconnected component. Therefore, co satis es any of those axioms provided that each co i does.

We now consider the case where C = PC. Assume that each B i satis es PC. Based on the reduction in Section . . , h satis es PC i h R|W satis es SER. Moreover, since h R|W is obtained from h by splitting each transaction t into a read transaction R t and a write transaction W t while keeping all session order dependencies, each session in h corresponds to a session in h R|W that reads or writes exactly the same set of variables. Therefore, Comm(h) is isomorphic to Comm(h R|W ). Since B i satis es PC, we get that the corresponding biconnected component B i of Comm(h R|W ) satis es SER, for every i. Therefore, h R|W satis es SER, which implies that h satis es PC. The case of SI is proved in a similar way using the reduction to the serializability of h c R|W presented in Section . . (note that two transactions of h c R|W may read or write an additional common variable only if they were writing a common variable in the original history and therefore, Comm(h) is still isomorphic to Comm(h c R|W )). Since the decomposition of a graph into biconnected components can be done in linear time, Theorem . . implies that any of the criteria PC, SI, or SER can be checked in time O(size(h) bi-size(h) • size(h) 3 • bi-nb(h)) where bi-size(h) and bi-nb(h) are the maximum size of a biconnected component in Comm(h) and the number of biconnected components of Comm(h), respectively. The following corollary is a direct consequence of this observation.

Corollary . . . For an arbitrary but fixed constant k ∈ N and any criterion C ∈ {PC, SI, SER}, the problem of checking if a history h satisfies C is polynomial time, provided that the size of every biconnected component of Comm(h) is bounded by k.

E E

To demonstrate the practical value of the theory developed in the previous sections, we argue that our algorithms:

• are e cient and scalable,

• enable an e ective testing framework allowing to expose consistency violations in production databases.

We focus on three of the criteria introduced in Section . : serializability which is NP-complete in general and polynomial time when the number of sessions is considered to be a constant, snapshot isolation which can be reduced in linear time to serializability, and causal consistency which is polynomial time in general. As benchmark, we consider histories extracted from three distributed databases: CockroachDB [ ], Galera [ ], and AntidoteDB [ ]. Following the approach in Jepsen [ ], histories are generated with random clients. For the experiments described hereafter, the randomization process is parametrized by: ( ) the number of sessions (#sess), ( ) the number of transactions per session (#trs), ( ) the number of operations per transaction (#ops), and ( ) an upper bound on the number of used variables (#vars) . For any valuation of these parameters, half of the histories generated with CockroachDB and Galera are restricted such that the sets of variables written by any two sessions are disjoint (the sets of read variables are not constrained). This restriction is used to increase the frequency of valid histories.

In a rst experiment, we investigated the e ciency of our serializability-checking algorithm (Algorithm ) and we compared its performance with a direct SAT encoding of the serializability de nition in Section . (we used MiniSAT [ ] to solve the SAT queries). We used histories extracted from CockroachDB which claims to implement serializability, acknowledging however the possibility of anomalies [ ]. The sessions of a history are uniformly distributed among nodes of a single cluster. To evaluate scalability, we x a reference set of parameter values: #sess= , #trs= , #ops= , and #vars = × #sess, and vary only one parameter at a time. For instance, the number of sessions varies from to in increments of . We consider histories for each combination of parameter values. The experimental data is reported in Figure . . Our algorithm scales well even when increasing the number of sessions, which is not guaranteed by its

We ensure that every value is written at most once. For each ordered pair of transactions t1, t2 we add two propositional variables representing t1, t2 ∈ (wr ∪ so) + and t1, t2 ∈ co, respectively. Then we generate clauses corresponding to: ( ) singleton clauses de ning the relation wr ∪ so (extracted from the input history), ( ) t1, t2 ∈ wr ∪ so implies t1, t2 ∈ co, ( ) co being a total order, and ( ) the axioms corresponding to the considered consistency model. This is an optimization that does not encode wr and so separately, which is sound because of the shape of our axioms (and because these relations are xed apriori). worst-case complexity (in general, this is exponential in the number of sessions). Also, our algorithm is at least two orders of magnitude more e cient than the SAT encoding. While the performance of SAT solvers is known to be heavily a ected by the speci c encoding of the problem, we strove to make the SAT formula as succinct as possible and optimize its construction. We have xed a minutes timeout, a limit of GB of memory, and a limit of GB on the les containing the formulas to be passed to the SAT solver. The blue dots represent resource-exhausted instances. The SAT encoding reaches the le limit for out of histories with at least sessions ( We have found a large number of violations, whose frequency increases with the number of sessions, transactions per session, or operations per transaction, and decreases when allowing more variables. This is expected since increasing any of the former parameters increases the chance of interference between di erent transactions while increasing the latter has the opposite e ect. The second and third column of Table . give a more precise account of the kind of violations we found by identifying for each criterion X, the number of histories that violate X but no other criterion weaker than X, e.g., there is only one violation to SI that satis es PC.

The second experiment measures the scalability of the SI checking algorithm obtained by applying the reduction to SER described in Section . . followed by the SER checking algorithm in Algorithm , and its performance compared to a SAT encoding of SI. Actually, the reduction to SER is performed on-the-y, while traversing the history and checking for serializability (of the transformed history). The SAT encoding follows the same principles as in the case of serializability. We focus on its behavior when increasing the number of sessions (varying the other parameters leads to similar results). As benchmark, we used the same CockroachDB histories as in Figure . a and a number of histories extracted from Galera whose documentation contains contradicting claims about whether it implements snapshot isolation [ , ]. We use histories per combination of parameter values as in the previous experiment. The results are reported In order to increase the frequency of valid histories, all sessions are executed on a single node. . b. We observe the same behavior as in the case of SER. In particular, the SAT encoding reaches the le limit for out of histories with at least sessions in the case of the CockroachDB histories, and for out of histories with at least sessions in the case of the Galera histories. The last two columns in Table . classify the set of violations depending on the weakest criterion that they violate.

We also evaluated the performance of the CC checking algorithm in Section . when increasing the number of sessions, on histories extracted from AntidoteDB, which claims to implement causal consistency [ ]. The results are reported in Figure . c. In this case, the SAT encoding reaches the le limit for out of histories with at least sessions. All the histories considered in this experiment are valid. However, when experimenting with other parameter values, we have found several violations. The smallest parameter values for which we found violations were sessions, transactions per session, operations per transaction, and variables. The violations we found are also violations of Read Atomic. For instance, one of the violations contains two transactions t 1 and t 2 , each of them writing to two variables x 1 and x 2 , and another transaction t 3 that reads x 1 from t 1 and x 2 from t 2 (t 1 and t 2 are from di erent sessions while t 3 is an so successor of t 1 in the same session). These violations are novel and they were con rmed by the developers of AntidoteDB.

The re nement of the algorithms above based on communication graphs, described in Section . , did not have a signi cant impact on their performance. The histories we generated contained few biconnected components (many histories contained just a single biconnected component) which we believe is due to our proof of concept deployment of these databases on a single machine that did not allow to experiment with very large number of sessions and variables.

R W

[ ] give the rst formalization of the criteria we consider in this work, using the speci cation methodology of [ ]. This formalization uses two auxiliary relations, a visibility relation which represents the fact that a transaction "observes" the e ects of another transaction and a commit order, also called arbitration order, like in our case. Executions are abstracted using a notion of history that includes only a session order and the adherence to some consistency criterion is de ned as the existence of a visibility relation and a commit order satisfying certain axioms. Motivated by practical goals, our histories include a write-read relation, which enables more uniform and in our opinion, more intuitive, axioms to characterize consistency criteria. Our formalizations are however equivalent with those of [ ] (a formal proof of this equivalence is presented in the extended version of this paper [ ]). Moreover, [ ] do not investigate algorithmic issues as in our work.

[ ] showed that checking serializability of an execution is NP-complete. Moreover, it identies a stronger criterion called conflict serializability which is polynomial-time checkable. Con ict serializability assumes that histories are given as sequences of operations and requires that the commit order be consistent with a conflict-order between transactions de ned based on this sequence (roughly, a transaction t 1 is before a transaction t 2 in the con ict order if it accesses some variable x before t 2 does). This result is not applicable to distributed databases where deriving such a sequence between operations submitted to di erent nodes in a network is impossible.

[ ] showed that checking several variations of causal consistency on executions of a non-transactional distributed database is polynomial time (they also assume that every value is written at most once). Assuming singleton transactions, our notion of CC corresponds to the causal convergence criterion in [ ]. Therefore, our result concerning CC can be seen as an extension of this result concerning causal convergence to transactions.

There are some works that investigated the problem of checking consistency criteria like sequential consistency and linearizability in the case of shared-memory systems. [ ] showed that checking linearizability of the single-value register type is NP-complete in general, but polynomial time for executions where every value is written at most once. Using a reduction from serializabilty, they showed that checking sequential consistency is NP-complete even when every value is written at most once. [ ] extended the result concerning linearizability to a series of abstract data types called collections, that includes stacks, queues, key-value maps, etc. Sequential consistency reduces to serializability for histories with singleton transactions (i.e., formed of a single read or write operation). Therefore, our polynomial-time result for checking serializability of boundedwidth histories (Corollary . . ) implies that checking sequential consistency of histories with a bounded number of threads is polynomial time. The latter result has been established independently by [ ].

The notion of communication graph is inspired by the work of [ ], which investigates partialorder reduction (POR) techniques for multi-threaded programs. In general, the goal of partialorder reduction [ ] is to avoid exploring executions which are equivalent w.r.t. some suitable notion of equivalence, e.g., Mazurkiewicz trace equivalence [ ]. They use the acyclicity of communication graphs to de ne a class of programs for which their POR technique is optimal. The algorithmic issues they explore are di erent than ours and they don't investigate biconnected components of this graph as in our results.

C

In this chapter, we proposed novel logical characterizations of various consistency models of transactional systems such as Read Committed (RC) [ ], Read Atomic (RA) [ ], Causal Consistency (CC) [ ], Prefix Consistency (PC) [ ], Snapshot Isolation (SI) [ ] and Serializability (SER). This enables an investigation of algorithmic techniques for checking conformance of a given execu-tion. We establish the asymptotic complexity of this problem for each consistency model when the read-from relation is known apriori. We introduce polynomial-time algorithms for RC, RA, CC, and prove that checking conformance for PC, SI, and SER is NP-complete. In the latter case, we introduce conformance checking algorithms that are polynomial time when the number of biconnected components of the communication graph is bounded by a xed constant. Finally, we demonstrate a runtime performance analysis of an implementation of our algorithms based on histories from production databases. As benchmark, we consider histories extracted from three distributed databases: CockroachDB [ ], Galera [ ], and AntidoteDB [ ]. Using our implementation, we were able to nd bugs in all these distributed databases, which con rms their incorrect promises on strong guarantees (CockroachDB) or previously mentioned bugs (Galera) or novel bugs (AntidoteDB). We present MonkeyDB, a mock in-memory storage system meant for testing correctness of storagebacked applications. MonkeyDB supports common APIs for accessing data (key-value updates, as well as SQL queries), making it an easy substitute for an actual storage system. MonkeyDB can be con gured with one of several transaction isolation (consistency) levels.

MonkeyDB implements a centralized operational semantics for key-value stores, which is based on the axiomatic de nitions presented in Section . . Transactions are executed serially, one after another, the concurrency being simulated during the handling of read events. This semantics maintains a history that contains all the past events (from all transactions/sessions), and write events are simply added to the history. The value returned by a read event is established based on a non-deterministic choice of a write-read dependency (concerning this read event) that satis es the axioms of the considered consistency models. Depending on the weakness of the isolation level, this makes it possible to return values written in arbitrarily "old" transactions, and simulate any concurrent behavior.

We formally prove that this semantics does indeed simulate any concurrent behavior, by showing that it is equivalent to a semantics where transactions are allowed to interleave. In comparison with concrete implementations, this semantics makes it possible to handle a wide range of consistency models in a uniform way. It only has two sources of non-determinism: the order in which entire transactions are submitted, and the choice of write-read dependencies in read events. This enable better coverage of possible behaviors, the penalty in performance not being an issue in safety testing workloads which are usually small (see our evaluation).

We also extend our semantics to cover SQL queries as well, by compiling SQL queries down to transactions with multiple key-value reads/writes. A table in a relational database is represented using a set of primary key values (identifying uniquely the set of rows) and a set of keys, one for each cell in the table. The set of primary key values is represented using a set of Boolean keyvalue pairs that simulate its characteristic function (adding or removing an element corresponds to updating one of these keys to true or false). Then, SQL queries are compiled to read or write accesses to the keys representing a table. For instance, a SELECT query that retrieves the set of rows in a table that satisfy a WHERE condition is compiled to ( ) reading Boolean keys to identify the primary key values of the rows contained in the table, ( ) reading keys that represent columns used in the WHERE condition, and ( ) reading all the keys that represent cells in a row satisfying the WHERE condition. This rewriting contains the minimal set of accesses to the cells of a table that are needed to ensure the conventional speci cation of SQL. It makes it possible to "export" formalizations of key-value store consistency models to SQL transactions.

The remainder of this chapter is organized as follows: • Section . presents a programming language to represent storage-backed applications,

InstrSQL def = SELECT c 1 AS x FROM tab WHERE φ( c 2 ) | INSERT INTO tab VALUES x | DELETE FROM tab WHERE φ( c) | UPDATE tab SET c 1 = x WHERE φ( c 2 )
• Section . de nes an operational semantics for key-value stores under various consistency models, which simulates all concurrent behaviors with executions where transactions execute serially and which is based on the axiomatic de nitions in Section . ,

• Section . broadens the scope of the key-value store semantics to SQL transactions using a compiler that rewrites SQL queries to key-value accesses,

• Section . describes the implementation of MonkeyDB,

• Section . and Section . present an evaluation of MonkeyDB on several applications, showcasing its superior coverage of weak behaviors as well as bug-nding abilities.

Section . overviews related work, and Section . concludes.

P L

Figure . lists the de nition of two simple programming languages that we use to represent applications running on top of Key-Value or SQL stores, respectively. A program is a set of sessions running in parallel, each session being composed of a sequence of transactions. Each transaction is delimited by begin and commit instructions , and its body contains instructions that access the store, and manipulate a set of local variables Vars ranged over using x, y, . . ..

For simplicity, we assume that all the transactions in the program commit. Aborted transactions can be ignored when reasoning about safety because their e ects should be invisible to other transactions.

In case of a program running on top of a Key-Value store, the instructions can be reading the value of a key and storing it to a local variable x (x := read(k)) , writing the value of a local variable x to a key (write(k, x)), or an assignment to a local variable x. The set of values of keys or local variables is denoted by Vals. Assignments to local variables use expressions interpreted as values whose syntax is left unspeci ed. Each of these instructions can be guarded by a Boolean condition φ( x) over a set of local variables x (their syntax is not important). Other constructs like while loops can be de ned in a similar way. Let P KV denote the set of programs where a transaction body can contain only such instructions.

For programs running on top of SQL stores, the instructions include simpli ed versions of standard SQL instructions and assignments to local variables. These programs run in the context of a database schema which is a (partial) function S : T 2 C mapping table names in T to sets of column names in C. The SQL store is an instance of a database schema S, i.e., a function D : dom(S) → 2 R mapping each table tab in the domain of S to a set of rows of tab, i.e., functions r : S(tab) → Vals. We use R to denote the set of all rows. The SELECT instruction retrieves the columns c 1 from the set of rows of tab that satisfy φ( c 2 ) ( c 2 denotes the set of columns used in this Boolean expression), and stores them into a variable x. INSERT adds a new row to tab with values x, and DELETE deletes all rows from tab that satisfy a condition φ( c). The UPDATE instruction assigns the columns c 1 of all rows of tab that satisfy φ( c 2 ) with values in x. Let P SQL denote the set of programs where a transaction body can contain only such instructions.

O S P KV

We de ne a small-step operational semantics for Key-Value store programs, which is parametrized by a consistency model I. Transactions are executed serially one after another, and the values returned by read operations are decided using the axiomatic de nition of I. The semantics maintains a history of previously executed operations, and the value returned by a read is chosen nondeterministically as long as extending the current history with the corresponding write-read dependency satis es the axioms of I. We show that this semantics is sound and complete for any natural consistency model I, i.e., it generates precisely the same set of histories as a baseline semantics where transactions can interleave arbitrarily and the read operations can return arbitrary values as long as they can be proved to be correct at the end of the execution.

D O S

We use the program in Figure . a to give an overview of our semantics, assuming Causal Consistency. This program has two concurrent transactions whose reads can both return the initial value 0, which is not possible under Serializability.

Our semantics executes transactions in their entirety one after another (without interleaving them), maintaining a history that contains all the executed operations. We assume that the transaction on the left executes rst. Initially, the history contains a ctitious transaction log that writes the initial value to all keys, and that will precede all the transaction logs created during the execution in session order.

Executing a write instruction consists in simply appending the corresponding write operation to the log of the current transaction. For instance, executing the rst write (and begin) in our example results in adding a transaction log that contains a write operation (see Figure . b). The execution continues with the read instruction from the same transaction, and it cannot switch to the other transaction.

The execution of a read instruction consists in choosing non-deterministically a write-read dependency that validates Causal when added to the current history. In our example, executing read(k 2 ) results in adding a write-read dependency from the transaction log writing initial values, which determines the return value of the read (see Figure . c). This choice makes the obtained history satisfy Causal.

The second transaction executes in a similar manner. When executing its read instruction, the chosen write-read dependency is again related to the transaction log writing initial values (see Figure . d). This choice is valid under Causal. Since a read must not read from the preceding transaction, this semantics is able to simulate all the "anomalies" of a weak consistency model (this execution being an example).

Formally, the operational semantics is de ned as a transition relation ⇒ I between configurations, which are de ned as tuples containing the following:

• history h storing the operations executed in the past,

• identi er j of the current session,

• local variable valuation γ for the current transaction,

• code B that remains to be executed from the current transaction, and

• sessions/transactions P that remain to be executed from the original program.

For readability, we de ne a program as a partial function P : SessId Sess that associates session identi ers in SessId with concrete code as de ned in Figure . (i.e., sequences of transactions). Similarly, the session order so in a history is de ned as a partial function so : SessId Tlogs * that associates session identi ers with sequences of transaction logs. Two transaction logs are ordered by so if one occurs before the other in some sequence so(j) with j ∈ SessId.

Before presenting the de nition of ⇒ I , we introduce some notation. Let h be a history that contains a representation of so as above. We use h ⊕ j t, O, po to denote a history where t fresh P(j) = begin; Body; commit; S h, _, _, , P ⇒ I h ⊕ j t, ∅, ∅ , j, ∅, Body, P[j → S] ϕ( x)[x → γ(x) : x ∈ x] true h, j, γ, if(φ( x)){Instr}; B, P ⇒ I h, j, γ, Instr; B, P ϕ( x)[x → γ(x) : x ∈ x] false h, j, γ, if(φ( x)){Instr}; B, P ⇒ I h, j, γ, B, P v = γ(x) i fresh h, j, γ, write(k, x); B, P ⇒ I h ⊕ j write i (k, v), j, γ, B, P write(k, v) is the last write on k in t w.r.t. po i fresh h, j, γ, x := read(k); B, P ⇒ I h ⊕ j read i (k, v), j, γ[x → v], B, P h = (T, so, wr) t is the id of the last transaction log in so(j) write(k, v) ∈ writes(t ) with t ∈ T and t = t i fresh t, O, po is appended to so(j). Also, for an operation o, h ⊕ j o is the history obtained from h by adding o to the last transaction log in so(j) and as a last operation in the program order of this log (i.e., if so(j) = σ; t, O, po , then the session order so of h ⊕ j o is de ned by so (k) = so(k) for all k = j and so(j) = σ; t, O ∪ o, po ∪ {(o , o) : o ∈ O} ). Finally, for a history h = T, so, wr , h ⊕ wr(t, o) is the history obtained from h by adding (t, o) to the write-read relation. corresponds to a write instruction and consists in simply adding a write operation to the current history. and concern read instructions.

h = (h ⊕ j read i (k, v)) ⊕ wr(t , read i (k, v)) h satis es I h, j, γ, x := read(k); B, P ⇒ I h , j, γ[x → v], B, P
handles the case where the read follows a write on the same key k in the same transaction: the read returns the value written by the last write on k in the current transaction. Otherwise, corresponds to reading a value written in another transaction t (t is the id of the log of the current transaction). The transaction t is chosen non-deterministically t fresh P(j) = begin; Body; commit; S B(j) = h, γ, B, P ⇒ h ⊕ j t, ∅, ∅ , γ[j → ∅], B[j → Body], P[j → S] B(j) = x := read(k); B h = (T, so, wr) t is the id of the last transaction log in so(j) write(k, v) ∈ writes(t ) with t ∈ compTrans(h, B) and t = t i fresh

h = (h ⊕ j read i (k, v)) ⊕ wr(t , read i (k, v)) h, γ, B, P ⇒ h , γ[(j, x) → v], B[j → B], P Figure .
: A baseline operational semantics for P KV programs. Above, compTrans(h, B) denotes the set of transaction logs in h that excludes those corresponding to live transactions, i.e., transaction logs t ∈ T such that t is the last transaction log in some so(j ) and B(j ) = .

as long as extending the current history with the write-read dependency associated to this choice leads to a history that still satis es I . An initial con guration for program P contains the program P along with a history h = {t 0 }, ∅, ∅ , where t 0 is a transaction log containing only writes that write the initial values of all keys, and empty current transaction code (B = ). An execution of a program P under an consistency model I is a sequence of con gurations c 0 c 1 . . . c n where c 0 is an initial con guration for P, and c m ⇒ I c m+1 , for every 0 ≤ m < n. We say that c n is I-reachable from c 0 . The history of such an execution is the history h in the last con guration c n . A con guration is called final if it contains the empty program (P = ∅). Let hist I (P) denote the set of all histories of an execution of P under I that ends in a nal con guration.

C O S

We de ne the correctness of ⇒ I in relation to a baseline semantics where transactions can interleave arbitrarily, and the values returned by read operations are only constrained to come from committed transactions. This semantics is represented by a transition relation ⇒, which is de ned by a set of rules that are analogous to ⇒ I . Since it allows transactions to interleave, a con guration contains a history h, the sessions/transactions P that remain to be executed, and:

• a valuation map γ that records local variable values in the current transaction of each session ( γ associates identi ers of sessions that have live transactions with valuations of local variables),

• a map B that stores the code of each live transaction (associating session identi ers with code).

Figure . lists some rules de ning ⇒ (the others can be de ned in a similar manner). starts a new transaction in a session j provided that this session has no live transaction ( B(j) = ). Compared to in Figure . , this rule allows un nished transactions in other sessions. does not check conformance to I, but it allows a read to only return a value written in a completed (committed) transaction. In this work, we consider only consistency models A history which satis es the rst order formula ( . ) with the axiom de ned in gure . corresponding to I.

. Compiling SQL to Key-Value API satisfying this constraint. Executions, initial and nal con gurations are de ned as in the case of ⇒ I . The history of an execution is still de ned as the history in the last con guration. Let hist * (P) denote the set of all histories of an execution of P w.r.t. ⇒ that ends in a nal con guration.

Practical consistency models satisfy a "pre x-closure" property saying that if the axioms of I are satis ed by a pair h 2 , co 2 , then they are also satis ed by every prefix of h 2 , co 2 . A pre x of h 2 , co 2 contains a pre x of the sequence of transactions in h 2 when ordered according to co 2 , and the last transaction log in this pre x is possibly incomplete. In general, this pre x-closure property holds for consistency models I that are de ned by axioms as in ( . ), provided that the property φ(t 2 , α) is monotonic, i.e., the set of models in the context of a pair h 2 , co 2 is a superset of the set of models in the context of a pre x h 1 , co 1 of h 2 , co 2 . For instance, the property φ in the axiom de ning Causal is (t 2 , α) ∈ (wr ∪ so) + , which is clearly monotonic. In general, standard consistency models are de ned using a property α of the form (t 2 , α) ∈ R where R is an expression built from the relations po, so, wr, and co using (re exive and) transitive closure and composition of relations [ ]. Such properties are monotonic in general (they would not be if those expressions would use the negation/complement of a relation). An axiom as in ( . ) is called monotonic when the property φ is monotonic.

The following theorem shows that hist I (P) is precisely the set of histories under the baseline semantics, which satisfy I (the validity of the reads is checked at the end of an execution), provided that the axioms of I are monotonic.

Theorem . . . For any consistency model I defined by a set of monotonic axioms, hist I (P) = {h ∈ hist * (P) : h satisfies I}.

The ⊆ direction follows mostly from the fact that ⇒ I is more constrained than ⇒. For the opposite direction, given a history h that satis es I, i.e., there exists a commit order co such that h, co satis es the axioms of I, we can show that there exists an execution under ⇒ I with history h, where transactions execute serially in the order de ned by co. The pre x closure property is used to prove that transitions are enabled (these transitions get executed with a pre x of h). See the supplementary material for more details.

It can also be shown that ⇒ I is deadlock-free for every natural consistency model (e.g., Read Committed, Causal Consistency, Snapshot Isolation, and Serializability), i.e., every read can return some value satisfying the axioms of I at the time when it is executed (independently of previous choices).

C SQL K V API

We de ne an operational semantics for SQL programs (in P SQL ) based on a compiler that rewrites SQL queries to Key-Value read and write instructions. For presentation reasons, we use an intermediate representation where each table of a database instance is represented using a set variable that stores values of the primary key (identifying uniquely the rows in the table) and a set of keyvalue pairs, one for each cell in the table. In a second step, we de ne a rewriting of the API used to manipulate set variables into Key-Value read and write instructions.

For simplicity, we assume that primary keys correspond to a single column in the table.

I

R Let S : T 2 C be a database schema (recall that T and C are the set of table names and column names, resp.). For each table tab, let tab.pkey be the name of the primary key column. We represent an instance D : dom(S) → 2 R using:

• for each table tab, a set variable tab (with the same name) that contains the primary key value r(tab.pkey) of every row r ∈ D(tab),

• for each row r ∈ D(tab) with primary key value pkeyVal = r(tab.pkey), and each column c ∈ S(tab), a key tab.pkeyVal .c associated with the value r(c). . , where the primary key is defined by the Id column, is represented using a set variable A storing the set of values in the column Id, and one keyvalue pair for each cell in the table.

Example . . . The table A on the left of Figure

Figure . lists our rewriting of SQL queries over a database instance D to programs that manipulate the set variables and key-value pairs described above. This rewriting contains the minimal set of accesses to the cells of a table that are needed to implement an SQL query according to its conventional speci cation. To manipulate set variables, we use add and remove for adding and removing elements, respectively (returning true or false when the element is already present or deleted from the set, respectively), and elements that returns all of the elements in the input set .

SELECT, DELETE, and UPDATE start by reading the contents of the set variable storing primary key values and then, for every row, the columns in c 2 needed to check the Boolean condition φ (the keys corresponding to these columns). For every row satisfying this Boolean condition, SELECT continues by reading the keys associated to the columns that need to be returned, DELETE removes the primary key value associated to this row from the set tab, and UPDATE writes to the keys corresponding to the columns that need to be updated. In the case of UPDATE, we assume that the values of the variables in x are obtained from a valuation γ (this valuation would be maintained by the operational semantics of the underlying Key-Value store). INSERT adds a new primary key value to the set variable tab (the call to add checks whether this value is unique) and then writes to the keys representing columns of this new row.

M S V

Based on the standard representation of a set using its characteristic function, we implement each set variable tab using a set of keys tab.has.pkeyVal , one for add(s, e) and remove(s, e) add and remove the element e from s, respectively. elements(s) returns the content of s. MonkeyDB contains a SQL-To-KV compiler that parses an input query , builds its Abstract Syntax Tree (AST) and then applies the rewriting steps described in Section . to produce an equivalent sequence of KV API calls (read() and write()). It uses a hashing routine (hash) to generate unique keys corresponding to each cell in a table. For instance, in order to insert a value v for a column c in a particular row with primary key value pkeyVal , of a table tab, we invoke write(hash(tab, pkeyVal , c), v). We currently support only a subset of the standard SQL operators. For instance, nested queries or join operators are unsupported; these can be added in the future with more engineering e ort.

MonkeyDB schedules transactions from di erent sessions one after the other using a single global lock. Internally, it maintains execution state as a history consisting of a set of transaction logs, write-read relations and a partial session order (as discussed in § . ). On a read(), MonkeyDB rst collects a set of possible writes present in transaction log that can potentially form write-read (read-from) relationships, and then invokes the consistency checker (Figure . ) to con rm validity under the chosen consistency model. Finally, it randomly returns one of the values associated with valid writes. A user can optionally instruct MonkeyDB to only select from the set of latest valid write per session. This option helps limit weak behaviors for certain reads.

The implementation of our consistency checker is based on prior work [ ]. It maintains the write-read relation as a graph, and detects cycles (isolation-level violations) using DFS traversals on the graph. The consistency checker is an independent and pluggable module: we have one for Read Committed and one for Causal Consistency, and more can be added in the future.

We support the MySQL client-server protocol using https://github.com/jonhoo/msql-srv. We use https://github.com/ballista-compute/sqlparser-rs // Get user's tweets We consider a set of micro-benchmarks inspired from real-world applications ( § . . ) and evaluate the number of test iterations required to fail an invalid assertion ( § . . ). We also measure the coverage of weak behaviors provided by MonkeyDB ( § . . ). Each of these applications were implemented based on their speci cations described in prior work; they all use MonkeyDB as a library, via its KV interface.

A T This is based on a social-networking application that allows users to create a new account, follow, unfollow, tweet, browse the newsfeed (tweets from users you follow) and the timeline of any particular user. Figure . shows the pseudo code for two operations.

A user can access twitter from multiple clients (sessions), which could lead to unexpected behavior under weak consistency models. Consider the following scenario with two users, A and B where user A is accessing twitter from two di erent sessions, S 1 and S 2 . User A views the timeline of user B from one session (S 1 :Timeline(B)) and decides to follow B through another session (S 2 :Follow(A, B)). Now when user A visits their timeline or newsfeed (S 2 :NewsFeed(A)), they expect to see all the tweets of B that were visible via Timeline in session S 1 . But under weak consistency models, this does not always hold true and there could be missing tweets.

S C

This application allows a user to add, remove and change quantity of items from di erent sessions. It also allows the user to view all items present in the shopping cart. The pseudo code and an unexpected behavior under weak consistency models were discussed in § . , Figure . .

C

This is an application for managing students and courses, allowing students to register, de-register and enroll for courses. Courses can also be created or deleted. Courseware maintains the current status of students (registered, de-registered), courses (active, deleted) as well as enrollments. Enrollment can contain only registered students and active courses, subject to the capacity of the course.

Under weak isolation, it is possible that two di erent students, when trying to enroll concurrently, will both succeed even though only one spot was left in the course. Another example that breaks the application is when a student is trying to register for a course that is being concurrently removed: once the course is removed, no student should be seen as enrolled in that course. T S Treiber stack is a concurrent stack data structure that uses compare-andswap (CAS) instructions instead of locks for synchronization. This algorithm was ported to operate on a kv-store in prior work [ ] and we use that implementation. Essentially, the stack contents are placed in a kv-store, instead of using an in-memory linked data structure. Each row in the store contains a pair consisting of the stack element and the key of the next row down in the stack. A designated key "head" stores the key of the top of the stack. CAS is implemented as a transaction, but the pop and push operations do not use transactions, i.e., each read/write/CAS is its own transaction.

When two di erent clients try to pop from the stack concurrently, under serializability, each pop would return a unique value, assuming that each pushed value is unique. However, under causal consistency, concurrent pops can return the same value.

A C

We ran the above applications with MonkeyDB to nd out if assertions, capturing unexpected behavior, were violated under causal consistency. Table . summarizes the results. For each application, we used client threads and operations per thread. We ran each test with MonkeyDB for a total of , times; we refer to a run as an iteration. We report the average number of iterations (Iters) before an assertion failed, and the corresponding time taken (sec). All the assertions were violated within iterations, in half a second or less. In contrast, running with an actual database almost never produces an assertion violation. For this experiment, we randomly generated test harnesses; each harness spawns multiple threads that each execute a sequence of operations. In order to compute the absolute maximum of possible states, we had to limit the size of the tests: either or threads, each choosing between to operations.

Note that any program that concurrently executes operations against a store has two main sources of non-determinism: the rst is the interleaving of operations (i.e., the order in which operations are submitted to the store) and second is the choice of read-from (i.e., the value returned by the store under its con gured consistency model). MonkeyDB only controls the latter; it is up to the application to control the former. There are many tools that systematically enumerate interleavings (such as C [ ], C [ ]), but we use a simple trick instead to avoid imposing any burden on the application: we included an option in MonkeyDB to deliberately add a small random delay (sleep between 0 to 4 ms) before each transaction begins. This option was su cient in our experiments, as we show next.

We also implemented a special using the C tool [ ] to enumerate all sources of non-determinism, interleavings as well as read-from, in order to explore the entire state space of a test. We use this to compute the total number of states. Figure . shows the number of distinct states observed under di erent consistency models, averaged across multiple (50) test harnesses. For each of serializability and causal consistency, we show the max (as computed by C

) and versions with and without the delay option in MonkeyDB.

Each of these graphs show similar trends: the number of states with causal consistency are much higher than with serializability. Thus, testing with a store that is unable to generate weak behaviors will likely be ine ective. Furthermore, the "delay" versions of MonkeyDB are able to approach the maximum within a few thousand attempts, implying that MonkeyDB's strategy of per-read randomness is e ective for providing coverage to the application.

E OLTP W

OLTPBench [ ] is a benchmark suite of representative OLTP workloads for relational databases. We picked a subset of OLTPBench for which we had reasonable assertions. Table . lists basic information such as the number of database tables, the number of static transactions, how many of them are read-only, and the number of di erent assertions corresponding to system invariants for testing the benchmark. We modi ed OLTPBench by rewriting SQL join and aggregation operators into equivalent application-level loops, following a similar strategy as prior work [ ].

Except for this change, we ran OLTPBench unmodi ed.

For TPC-C, we obtained a set of 12 invariants from its speci cation document [ ]. For all other benchmarks, we manually identi ed invariants that the application should satisfy. We asserted these invariants by issuing a read-only transaction to MonkeyDB at the end of the execution of the benchmark. None of the assertions fail under serializability; they are indeed invariants un-Benchmark #Tables #Txns #Read-only #Assertions TPC-C SmallBank Voter Wikipedia Table . : OLTP benchmarks tested with MonkeyDB der serializability. When using weaker isolation, we con gured MonkeyDB to use latest reads only ( § . ) for the assertion-checking transactions in order to isolate the weak behavior to only the application.

We ran each benchmark 100 times and report, for each assertion, the number of runs in which it was violated. Note that OLTPBench runs in two phases. The rst is a loading phase that consists of a big initial transaction to populates tables with data, and then the execution phase issues multiple concurrent transactions. With the goal of testing correctness, we turn down the scale factor to generate a small load and limit the execution phase time to ten seconds with just two or three sessions. A smaller test setup has the advantage of making debugging easier. With MonkeyDB, there is no need to generate large workloads. TPC C TPC-C emulates a wholesale supplier transactional system that delivers orders for a warehouse company. This benchmark deals with customers, payments, orders, warehouses, deliveries, etc. We con gured OLTPBench to issue a higher proportion (> 85%) of update transactions, compared to read-only ones. Further, we considered a small input workload constituting of one warehouse, two districts per warehouse and three customers per district.

TPC-C has twelve assertions (A to A ) that check for consistency between the database tables. For example, A checks: for any customer, the sum of delivered order-line amounts must be equal to the sum of balance amount and YTD (Year-To-Date) payment amount of that customer.

Figure . shows the percentage of test runs in which an assertion failed. It shows that all the twelve assertions are violated under Read Committed consistency model. In fact, 9 out of the 12 assertions are violated in more than % of the test runs. In case of causal, all assertions are violated with three sessions, except for A and A . We manually inspected TPC-C and we believe that both these assertions are valid under causal consistency. For instance, A checks for consistency between two tables, both of which are only updated within the same transaction, thus causal consistency is enough to preserve consistency between them.

These results demonstrate the e ectiveness of MonkeyDB in breaking (invalid) assertions. Running with MySQL, under read committed, was unable to violate any assertion except for two (A and A ), even when increasing the number of sessions to 10. We used the same time limit of 10 seconds for the execution phase. We note that MySQL is much faster than MonkeyDB and ends up processing up to 50× more transactions in the same time limit, yet is unable to violate most assertions. Prior work [ ] attempted a more sophisticated test setup where TPC-C was executed on a Cassandra cluster, while running Jepsen [ ] for fault injection. This setup also was unable to violate all assertions, even when running without transactions, and on a weaker consistency We initially observed two assertions failing under serializability. Upon analyzing the code, we identi ed that the behavior is due to a bug in OLTPBench that we have reported to the authors (link ommitted).

S

B V W SmallBank is a standard nancial banking system, dealing with customers, saving and checking accounts, money transfers, etc. Voter emulates the voting system of a television show and allows users to vote for their favorite contestants. Wikipedia is based on the popular online encyclopedia. It deals with a complex database schema involving page revisions, page views, user accounts, logging, etc. It allows users to edit its pages and maintains a history of page edits and user actions.

We identi ed a set of ve assertions, A to A , that should be satis ed by these systems. For SmallBank, we check if the total money in the bank remains the same while it is transfered from one account to another (A ). Voter requires that the number of votes by a user is limited to a xed threshold (A ). For Wikipedia, we check if for a given user and for a given page, the number of edits recorded in the user information, history, and logging tables are consistent (A -A ). As before, we consider small work loads: ( ) ve customers for SmallBank, ( ) one user for Voter, and ( ) two pages and two users for Wikipedia.

Figure . shows the results. MonkeyDB detected that all the assertions are invalid under the chosen consistency models. Under causal, MonkeyDB could break an assertion in . % (geomean) runs given sessions and in . % (geo-mean) runs given sessions. Under read committed, the corresponding numbers are . % and . % for and sessions, respectively.

R W

There have been several directions of work addressing the correctness of database-backed applications. We directly build upon one line of work concerned with the logical formalization of consistency models or isolation levels [ , , , , ]. Our work relies on the axiomatic de nitions of consistency models or isolation levels, as given in [ ], which also investigated the problem of checking whether a given history satis es a certain isolation level. Our kv-store implementation relies on these algorithms to check the validity of the values returned by read operations. Working with a logical formalization allowed us to avoid implementing an actual database with replication or sophisticated synchronization.

Another line of work concentrates on the problem of nding "anomalies": behaviors that are not possible under serializability. This is typically done via a static analysis of the application code that builds a static dependency graph that over-approximates the data dependencies in all possible executions of the application [ , , , , , ]. Anomalies with respect to a given consistency model then corresponds to a particular class of cycles in this graph. Static dependency graphs turn out to be highly imprecise in representing feasible executions, leading to false positives. Another source of false positives is that an anomaly might not be a bug because the application may already be designed to handle the non-serializable behavior [ , ]. Recent work has tried to address these issues by using more precise logical encodings of the application, e.g. [ , ] or by using user-guided heuristics [ ].

Another approach consists of modeling the application logic and the consistency model in rstorder logic and relying on SMT solvers to search for anomalies [ , , ], or de ning specialized reductions to assertion checking [ , ]. The C tool [ ], for instance, uses a static analysis of the application to generate test cases with plausible anomalies, which are deployed in a concrete testing environment for generating actual executions.

Our approach, based on testing with MonkeyDB, has several practical advantages. There is no need for analyzing application code; we can work with any application. There are no false positives because we directly run the application and check for user-de ned assertions, instead of looking for application-agnostic anomalies. The limitation, of course, is the inherent incompleteness of testing.

Several works have looked at the problem of reasoning about the correctness of applications executing under weak isolation and introducing additional synchronization when necessary [ , , , ]. As in the previous case, our work based on testing has the advantage that it can scale to real sized applications (as opposed to these techniques which are based on static analysis or logical proof arguments), but it cannot prove that an application is correct. Moreover, the issue of repairing applications is orthogonal to our work.

From a technical perspective, our operational semantics based on recording past operations and certain data-ow and control-ow dependencies is similar to recent work on stateless model checking in the context of weak memory models, e.g. [ , ]. This work, however, does not consider transactions. Furthermore, their focus is on avoiding enumerating equivalent executions, which is beyond the scope of our work (but an interesting direction for future work).

C

Our goal is to enable developers to test the correctness of their storage-backed applications under weak consistency models. Such bugs are hard to catch because weak behaviors are rarely generated by real storage systems, but failure to address them can lead to loss of business [ ]. We present MonkeyDB, an easy-to-use mock storage system for weeding out such bugs. MonkeyDB uses a logical understanding of isolation levels to provide (randomized) coverage of all possible weak behaviors. Our evaluation reveals that using MonkeyDB is very e ective at breaking assertions that would otherwise hold under a strong consistency model.

C

In this thesis, we have investigated various algorithmic questions related to automated testing of weakly-consistent data storage systems and applications built on top of them. We have explored the issue of specifying such systems, and studied the theoretical limits of checking whether a given execution satis es the intended speci cation. The contributions of this thesis span several directions: ( ) new formalisms for specifying weakly-consistent behaviors which integrate data type abstractions like counters, registers, sets, lists, etc, or transactions with various degrees of isolation, ( ) new asymptotic complexity results that delineate the tractability of automated testing for data storage systems, and ( ) an e ective methodology for improving the test coverage of storagebacked applications.

In more detail, Chapter focused on CRDTs, an important class of replicated data types that o ers a suitable compromise between consistency and availability. We have introduced a new speci cation formalism that provides a seamless integration between a particular data type semantics and consistency properties related to the asynchronous propagation of updates. We have used this formalism to derive new complexity results concerning the problem of checking conformance for a given execution.

Chapter investigated the same issues, but in the case of transactional key-value stores. We propose new de nitions for established consistency models, which compared to previous approaches, are expressed by logical constraints that follow a common template and make it possible to better distill semantical di erences. We have also established interesting semantical relationships between weak consistency models like Pre x Consistency or Snapshot Isolation, and Serializability. These advancements were used to ultimately derive complexity results about checking correctness of transactional key-value store executions, and determine the limits of tractability.

Chapter uses the speci cation formalism presented in Chapter in order to design a mock in-memory storage system called MonkeyDB that makes it possible to improve coverage in testing applications built on top of transactional storage systems. MonkeyDB simulates the behaviors of a storage system satisfying a speci c consistency model by keeping a global history of previously executed operations and making uniform random choices on read operations. Our empirical evaluation shows that MonkeyDB makes it possible to uncover invariant violations in established OLTP benchmarks in a small number of attempts.

F W

The work in this thesis can be advanced along several directions:

• Chapter leaves open several questions related to the complexity of CRDT consistency checking: checking conformance to the counter CRDT when the number of replicas is bounded, or sets and ags when their sizes are also bounded. We believe that these problems remain polynomial time, but as we explained in that chapter, the algorithms introduced in our previous work [ ] are only sound.

• Our conformance checking algorithms are offline, in the sense, that they receive as input an entire execution. For future work, we want to explore online algorithms that process a given execution on the y. Designing such algorithms with a low resource footprint or small overhead is a highly challenging issue.

• While our algorithms can only be used to indicate whether an execution is correct or not, we would like to investigate the issue of root-causing violations. Some bugs are di cult to expose with small length executions. For instance, our tests on AntidoteDB exposed a bug in an execution with transactions, which has been con rmed by the developers, and which cannot be caught with smaller executions (up to our knowledge). In such cases, pin pointing the root cause becomes essential for developers being able to repair it.

• Modern data storage systems support operations/transactions at di erent levels of consistency. While our work has assumed that all operations/transactions behave under the same consistency model, extending it to such cases is an important research direction.

• Concerning the problem of testing applications, a frequent issue is the lack of precise specications when checking their correctness against a weak consistency model. An interesting direction for future work is trying to automatically synthesize application-level invariants that distinguish its behaviors under strong consistency versus weak consistency. These invariants could be used during the development process as a way of guiding the insertion of additional synchronization.

• More generally, an important issue is nding the weakest possible consistency model for which an application satis es the intended speci cation. This would help in improving the performance of a given application, since weaker consistency models boost concurrency and minimize the synchronization overhead.

Figure . :

 . Figure . : A non-linearizable OR-Set execution. Edges represent propagation of updates. Each replica is annotated with labels showing the evolution of the set object after each update.

Figure . :Figure

 . Figure . : The complexity of consistency checking for various replicated data types.

  Figure . : A simple shopping cart service.

Figure . :

 . Figure . : The axiomatic semantics of replicated data types. Quanti ed variables are implicitly distinct, and ∃!o denotes the existence of a unique operation o.

Figure . :

 . Figure . : Axioms used to de ne the semantics of RGA.

  then return false; lin ← hb; lin ← LinClosure(hb,L [T ]); if lin is cyclic then return false; return true; Algorithm : Consistency checking for RGA, LWW, and MVR. R [T ] refers to an axiom of T , or true when T lacks such an axiom. The relation R + denotes the transitive closure of R.

  seen and checkCounter(h, m , seen) then return true; seen ← seen ∪ {m }; return false; Algorithm : The procedure checkCounter, where ro 1 denotes immediate ro-successor, and f [a ← b] updates function f with mapping a → b.

Figure . :Figure . :

 .. Figure . : An admissible execution of replicated counter for which Algorithm returns false.

  seen and CheckAWSet(h, m , u , seen) then return true; seen ← seen ∪ { m , u }; return false; Algorithm : The procedure CheckAWSet for checking consistency of Add-Wins Set.

  Figure . : Examples of transactions used to justify our simplifying assumptions (each box represents a di erent transaction): (a) only the last written value is observable in other transactions, (b) reads following writes to the same variable return the last written value in the same transaction, and (c) values written in aborted transactions are not observable.

  Figure . a shows a history This monotonicity property corresponds to the fact that in the original formulation of R C [ ],

  Figure . : De nitions of consistency axioms. The re exive and transitive, resp., transitive, closure of a relation rel is denoted by rel * , resp., rel + . Also, • denotes the composition of two relations, i.e., rel 1 • rel 2 = { a, b |∃c. a, c ∈ rel 1 ∧ c, b ∈ rel 2 }.

  Serializability violation.

Figure . :

 . Figure . : Examples of histories used to explain the axioms in Figure . . For readability, the wr relation is de ned by the values written in comments with each read.

  Figure . h shows a Serializability violation.

  Figure . : Applying the RA and CC checking algorithms.

  Figure . a and Figure . b. Applying the axiom in Figure .

Figure . :

 . Figure . : Sub-histories included in h ϕ for each literal λ ij and variable x k .

  Figure . a shows the sub-history associated to a positive literal λ ij = x k while Figure . b shows the case of a negative literal λ ij = ¬x k . For a positive literal λ ij = x k (Figure . a), ( ) we enrich session order with the pairs y ij , a k and b k , w ij , ( ) we include writes to a variable v ij in the transactions y ij and z ij , and ( ) we make w ij read from z ij , i.e. z ij , w ij ∈ wr v ij . The case of a negative literal is similar, switching the roles of a k and b k .

  ij (Figure . a or Figure . b depending on the polarity of the literal).

  and y ij , z ij ∈ co for each λ ij = ¬x k . Looking at the sub-histories corresponding to literals λ ij (Figure . a or Figure . b), co goes in the same direction (upwards or downwards) on both sides.

  Figure . b pictures this search on the history in Figure . a. The right branch (containing blue edges) contains only valid extensions and it reaches a pre x that includes all the transactions in the history.

Figure . :

 . Figure . : Cycles with non-consecutive write transactions.

  Figure . a). The relations between these transactions of h R|W imply that the corresponding transactions of h are related as shown in Figure . b:

  Figure . : Reducing SI to SER.

  The communication graph and its decomposition in biconnected components.

Figure . :

 . Figure . : A history and its communication graph.

Figure . :

 . Figure . : Minimal paths between transactions in the same biconnected component.

  Figure . : Scalability of our algorithm for checking S (Algorithm ) with comparison to a SAT encoding. The x-axis represents the varying parameter while the y-axis represents the wall-clock time in logarithmic scale. The circular, resp., triangular, dots represent wallclock times of our algorithm, resp., the SAT encoding. The red, green, and blue dots represent invalid, valid and resource-exhausted instances, respectively.

  Figure . : Scalability of our algorithms for checking S (Section . . ) and C (Algorithm ) with comparison to a SAT encoding. The x-axis represents the varying parameter while the y-axis represents the wall-clock time in logarithmic scale. The circular, resp., triangular, dots represent wall-clock times of our algorithm, resp., the SAT encoding. The red, green, and blue dots represent invalid, valid and resource-exhausted instances, respectively.

  Figure . a) and for out of histories with transactions per session (Figure . b), the other parameters being xed as explained above.

k∈=

  Keys x ∈ Vars tab ∈ T c, c 1 , c 2 ∈ C * InstrKV | InstrSQL | x := e | if(φ( x)){Instr} InstrKV def = x := read(k) | write(k, x)

Figure . :

 . Figure . : Program syntax. The set of all keys is denoted by Keys, Vars denotes the set of local variables, Tthe set of table names, and C the set of column names. We use φ to denote Boolean expressions, and e to denote expressions interpreted as values. We use • to denote vectors of elements.

  Causal semantics on the program in (a), assuming that the transaction on the left is scheduled rst.

Figure . :

 . Figure . : Operational semantics for P KV programs under consistency model I. For a function f : A B, f [a → b] denotes the function f : A B de ned by f (c) = f (c), for every c = a in the domain of f , and f (a) = b.

Figure

  Figure . lists the rules de ning ⇒ I . The rule starts a new transaction, provided that there is no other live transaction (B = ). It adds an empty transaction log to the history and schedules the body of the transaction. and check the truth value of a Boolean condition of an if conditional.corresponds to a write instruction and consists in simply adding a write operation to the current history. and concern read instructions.handles the case where the read follows a write on the same key k in the same transaction: the read returns the value written by the last write on k in the current transaction. Otherwise, corresponds to reading a value written in another transaction t (t is the id of the log of the current transaction). The transaction t is chosen non-deterministically

Figure . :

 . Figure . : Representing tables with set variables and key-value pairs. We write a key-value pair as key:value.

  Figure . : Architecture of MonkeyDB

  Figure . : Example operations of the Twitter app

Figure . :

 . Figure . : State coverage obtained with MonkeyDB for various microbenchmarks

Figure . :

 . Figure . : Assertion checking: TPC-C

  Free Replicated Data Types . . . . . . . . . . . . . . . . . . . . . . . Transactional Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Applications Using Transactional Systems . . . . . . . . . . . . . . . . . . . . Thesis Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Reducing Snapshot Isolation to Serializability . . . . . . . . . . . . . . Communication graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Experimental Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

		r 1	add(b)	add(a)	remove(b)		contains(b)=true
			{b}	{a,b}	{a,b}		{a}	{a,b}		{a,b}	contains(a)=true
	C	r 2	{a}	{a,b}	{a,b}		{b}	{a,b}		{a,b}	contains(b)=true
			add(a)	add(b)	remove(a)		contains(a)=true
	I
	. Con ict-C C		C	F	R		D	T
	.
	T	A		T	U T			D	S
	.	Programming Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
										vii

A Logical Characterization of Replicated Data Types . . . . . . . . . . . . . . . . Replicated Sets and Flags . . . . . . . . . . . . . . . . . . . . . . . . . . Replicated Registers . . . . . . . . . . . . . . . . . . . . . . . . . . . . Replicated Counters . . . . . . . . . . . . . . . . . . . . . . . . . . . . Replicated Growable Array . . . . . . . . . . . . . . . . . . . . . . . . Intractability for Registers, Sets, Flags, and Counters . . . . . . . . . . . . . . . Polynomial-Time Algorithms . . . . . . . . . . . . . . . . . . . . . . . . . . . . Registers and Arrays . . . . . . . . . . . . . . . . . . . . . . . . . . . . Replicated Counters . . . . . . . . . . . . . . . . . . . . . . . . . . . . Sets and Flags . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . C T C . Consistency Criteria . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Histories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Axiomatic Framework . . . . . . . . . . . . . . . . . . . . . . . . . . Checking Consistency Criteria . . . . . . . . . . . . . . . . . . . . . . . . . . Checking Consistency of Bounded-Width Histories . . . . . . . . . . . . . . . . Checking Serializability . . . . . . . . . . . . . . . . . . . . . . . . . . . Reducing Pre x Consistency to Serializability . . . . . . . . . . . . . . .

  [ ]. The history of Add-Wins Set in Figure . is admissible while Algorithm returns false. The explanations are similar to the Counter example in Figure . . Many have considered consistency models applicable to CRDTs, including causal consistency [ ], sequential consistency [ ], linearizability [ ], session consistency [ ], eventual consistency [ ],and happens-before consistency [ ].Burckhardt et al. [ , ] propose a unifying framework to formalize these models. Many have also studied the complexity of verifying data-type agnostic notions of consistency, including serializability, sequential consistency, and linearizability[ , , , , , , ], as well as causal consistency [ ]. Our de nition of the replicated LWW register corresponds to the notion of causal convergence in [ ].

R W

Table . :

 . Consistency model de nitions

	Consistency model	Axioms
	R	C	(RC)	Read Committed
	R	A	(RA)	Read Atomic
	C		(CC) Causal
	P		(PC)	Prefix
	S		(SI)	Prefix ∧ Conflict
	S		(SER)	Serializability

  Input:A history h = T, so, wr Output: true i h satis es C

	if so ∪ wr is cyclic then
	return false;
	co ← so ∪ wr;
	foreach x ∈ vars(h) do
	foreach t1 = t2 ∈ T s.t. t1 and t2 write x do
	if ∃t3. t1, t3 ∈ wrx ∧ t2, t3 ∈ (so ∪ wr) + then
	co ← co ∪ { t2, t1 };
	if co is cyclic then
	return false;
	else
	return true;

  Input:A history h = (T, so, wr), a serializable pre x T of h Output: true i T * h The algorithm checkSER for checking serializabilty. seen is a global variable storing a set of pre xes of h (which are not serializable). It is initialized as the empty set.

	if T = T then
	return true;
	foreach t ∈ T s.t. ∀t ∈ T . t , t ∈ wr ∪ so do
	if T	T	{t} then
		continue;
	if T	{t} ∈ seen ∧ checkSER(h, T	{t}) then
		return true;
	seen ← seen ∪ {(T	{t})};
	return false;

Algorithm :

  h and h R|W have the same width.

							read(x); //	read(y); //
					read(x); //	read(y); //
							read(y); //	read(x); //
	read(x); //	read(y); //	read(x); //	read(x); //
	x = ;	y = ;	read(y); //	read(y); //	so	so	so	so
		(a) Long fork		x = ;	y = ;	// empty	// empty
					(b) Long fork (transformed)
					read(x); //	read(x); //
		read(x); //	read(x); //
		x = ;	x = ;
					x = ;	x = ;
		(c) Lost update

  Cycles in co 2 correspond to Prefix violations: (a) Minimal cycle in co 2 , (b) Prefix violation in h, co .

					t 2 writes x	co *	t 4
					co	wr ∪ so
					t 1	wr x	t 3
						(b)
	t 2 writes x Figure . : t 1 co	wr x co *	t 4	t 3 wr ∪ so	W t1 W t2 writes x co * wr x co co W t 4 R t3 wr ∪ so
		(a)				(b)

Figure . : Prefix violations correspond to cycles in co : (a) Prefix violation in h, co , (b) Cycle in co .

contains a dependency R t 3 , W t 2 ∈ RW(co 1 ) which implies the existence of a write transaction W t 1 in h R|W s.t. W t 1 , R t 3 ∈ wr x and W t 1 , W t 2 ∈ co 1 and W t 1 , W t 2 write on x (these dependencies are represented by the black edges in

Table . :

 . Violation statistics. The "disjoint writes" columns refer to histories where the set of variables written by any two sessions are disjoint.

		Serializability checking	Snapshot Isolation checking
	Weakest	CockroachDB	CockroachDB	Galera	Galera
	criterion violated	(disjoint writes) (no constraints) (disjoint writes) (no constraints)
	Read Committed
	Read Atomic
	Causal Consistency
	Pre x Consistency
	Snapshot Isolation
	Serializability
	Total number of violations	/	/	/	/
	in Figure . a and Figure

Table . :

 . Assertions checking results in microbenchmarks CThe previous section only checked for a particular set of assertions. As an additional measure of test robustness, we count the number of distinct client-observable states generated by a test. A client-observable state, for an execution, is the vector of values returned by read operations. For instance, a stack's state is de ned by return values of pop operations; a shopping cart's state is de ned by the return value of GetCart and so on.

	Application Assertion	Avg. time to fail
			(Iters)	(sec)
	Stack	Element popped more than once	.	.
	Courseware	Course registration over ow	.	.
	Courseware	Removed course registration	.	.
	Shopping	Item reappears after deletion	.	.
	Twitter	Missing tweets in feed	.	.

This is also used in Jepsen, e.g., checking dirty reads in Galera [ ].

each value pkeyVal ∈ Vals. These keys are associated with Boolean values, indicating whether pkeyVal is contained in tab. In a concrete implementation, this set of keys need not be xed apriori, but can grow during the execution with every new instance of an INSERT. Figure . lists the implementations of add/elements, which are self-explanatory (remove is analogous).

I

We implemented MonkeyDB to support an interface common to most storage systems. Operations can be either key-value (KV) updates (to access data as a KV map) or SQL queries (to access data as a relational database). MonkeyDB supports transactions as well; a transaction can include multiple operations. Figure . shows the architecture of MonkeyDB. A client can connect to .