On the Complexity of Checking Transactional Consistency

TL;DR

This paper analyzes the computational complexity of verifying whether transactional database executions meet various consistency models, revealing some are polynomial-time checkable while others are NP-complete, with practical algorithms for the latter.

Contribution

It provides a complexity classification for checking different transactional consistency models and introduces fixed-parameter algorithms for NP-complete cases, with empirical evaluation.

Findings

Read committed, read atomic, and causal consistency are polynomial-time checkable.

Prefix consistency and snapshot isolation are NP-complete to verify in general.

Algorithms with fixed parameters perform well on real-world databases.

Abstract

Transactions simplify concurrent programming by enabling computations on shared data that are isolated from other concurrent computations and are resilient to failures. Modern databases provide different consistency models for transactions corresponding to different tradeoffs between consistency and availability. In this work, we investigate the problem of checking whether a given execution of a transactional database adheres to some consistency model. We show that consistency models like read committed, read atomic, and causal consistency are polynomial time checkable while prefix consistency and snapshot isolation are NP-complete in general. These results complement a previous NP-completeness result concerning serializability. Moreover, in the context of NP-complete consistency models, we devise algorithms that are polynomial time assuming that certain parameters in the input executions, e.g., the number of sessions, are fixed. We evaluate the scalability of these algorithms in the context of several production databases.

Tables

Table 1. Table 1 . Consistency model definitions

Consistency model	Axioms
Read Committed (RC)	$\mathrm{𝖱𝖾𝖺𝖽}\mathrm{𝖢𝗈𝗆𝗆𝗂𝗍𝗍𝖾𝖽}$
Read Atomic (RA)	$\mathrm{𝖱𝖾𝖺𝖽}\mathrm{𝖠𝗍𝗈𝗆𝗂𝖼}$
Causal consistency (CC)	$\mathrm{𝖢𝖺𝗎𝗌𝖺𝗅}$
Prefix consistency (PC)	$\mathrm{𝖯𝗋𝖾𝖿𝗂𝗑}$
Snapshot isolation (SI)	$\mathrm{𝖯𝗋𝖾𝖿𝗂𝗑}\wedge \mathrm{𝖢𝗈𝗇𝖿𝗅𝗂𝖼𝗍}$
Serializability (SER)	$\mathrm{𝖲𝖾𝗋𝗂𝖺𝗅𝗂𝗓𝖺𝖻𝗂𝗅𝗂𝗍𝗒}$

Table 2. Table 2. 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			19	50
Read Atomic	180	547	91	139
Causal Consistency	339	382	88	43
Prefix Consistency	2	7
Snapshot Isolation		1		1
Serializability	25
Total number of violations	546/1000	937/1000	198/250	233/250

Table 3. Table 3 . Consistency axioms for a history h 𝗌𝗈 = ⟨ T , 𝗌𝗈 ⟩ subscript ℎ 𝗌𝗈 𝑇 𝗌𝗈 {h}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}}={\left\langle{T,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}}\right\rangle} , visibility relation vis , and commit order co .

$\forall (O,\text{po})\in t,\forall o\in O,o=read(x,n)\wedge$ $\{o^{\prime }\in {\text{po}}^{-1}\left(o\right)\mid o^{\prime }=\_(x,\_)\}\ne \varnothing \Rightarrow$ $ma{x}_{\text{po}}\left(\{o^{\prime }\in {\text{po}}^{-1}\left(o\right)\mid o^{\prime }=\_(x,\_)\}\right)=\_(x,n)$			(Int)
$\forall t=(O,\text{po})\in t,\forall x,t\vDash \text{read}(x,n)\Rightarrow$ $\left(\left({\text{vis}}^{-1}\left(t\right)\cap {\text{Write}}_x\right)=\varnothing \wedge n=0\right)\vee$ $\left(ma{x}_{\text{co}}\left({\text{vis}}^{-1}\left(t\right)\cap {\text{Write}}_x\right)\vDash \text{write}(x,n)\right)$			(Ext)
$\text{so}\subseteq \text{vis}$	(Session)	visis transitive	(TransVis)
$\text{co};\text{vis}\subseteq \text{vis}$	(Prefix)	$\text{vis}=\text{co}$	(TotalVis)
$\forall t,t^{\prime }\in T,\forall x,\left(t,t^{\prime }\in {\text{Write}}_x\wedge t\ne t^{\prime }\right)$ $\Rightarrow \left(t\stackrel{\text{vis}}{\to }{t}^{\prime }\vee t^{\prime }\stackrel{\text{vis}}{\to }t\right)$			(NoConflict)

Table 4. Table 4 . Consistency model definitions in Cerone et al . ( 2015 ) .

Consistency model	Axioms
Read atomic	Int $\wedge$ Ext $\wedge$ Session
Causal consistency	Int $\wedge$ Ext $\wedge$ Session $\wedge$ TransVis
Prefix consistency	Int $\wedge$ Ext $\wedge$ Session $\wedge$ Prefix
Snapshot isolation	Int $\wedge$ Ext $\wedge$ Session $\wedge$ Prefix $\wedge$ NoConflict
Serializability	Int $\wedge$ Ext $\wedge$ TotalVis

Equations

$$\mathsf{Op}=\{{\text{read}}_i(x,v),{\text{write}}_i(x,v):i\in \mathsf{OpId},x\in \mathsf{Var},v\in \mathsf{Val}\}$$

$$\displaystyle\forall{x},\ \forall{t}_{1},{t}_{2},\ \forall\alpha.\ {t}_{1}\neq{t}_{2}\land{\left\langle{{t}_{1},\alpha}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}\land{{t}_{2}}\ \mathsf{writes}\ {{x}}\land\phi({t}_{2},\alpha)\Rightarrow{\left\langle{{t}_{2},{t}_{1}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}$$

$$\mathsf{Causal}\Rightarrow \mathsf{Read}\mathsf{Atomic}\Rightarrow \mathsf{Read}\mathsf{Committed}$$

$$\mathsf{Prefix}\Rightarrow \mathsf{Causal}$$

$$\mathsf{Serializability}\Rightarrow \mathsf{Prefix}\wedge \mathsf{Conflict}$$

$$\displaystyle{\left\langle{{t}_{2},{t}_{1}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}\text{ :- }{t}_{1}\neq{t}_{2},{\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}},{\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}})^{+}$$

$${\left\langle{a_{k},b_{k}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}$$

$$\displaystyle\mbox{${\left\langle{a_{k},b_{k}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}$ iff ${\left\langle{z_{ij},y_{ij}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}$ when $\lambda_{ij}=\neg x_{k}$}.$$

$$\displaystyle{\left\langle{b_{k},a_{k}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}\land{\left\langle{y_{ij},z_{ij}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}$$

$$\displaystyle\{{\left\langle{a_{k^{\prime}},b_{k^{\prime}}}\right\rangle},{\left\langle{b_{k^{\prime}},a_{k^{\prime}}}\right\rangle}|1\leq k^{\prime}\leq n\}\cup\{{\left\langle{y_{i^{\prime}j^{\prime}},z_{i^{\prime}j^{\prime}}}\right\rangle},{\left\langle{z_{i^{\prime}j^{\prime}},y_{i^{\prime}j^{\prime}}}\right\rangle}|\text{for each }i^{\prime},j^{\prime}\}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}.$$

$$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}^{\prime}=\{{\left\langle{R_{t},W_{t}}\right\rangle}|{t}\in T\}\cup\{{\left\langle{R_{{t}_{1}},R_{{t}_{2}}}\right\rangle},{\left\langle{R_{{t}_{1}},W_{{t}_{2}}}\right\rangle},{\left\langle{W_{{t}_{1}},R_{{t}_{2}}}\right\rangle},{\left\langle{W_{{t}_{1}},W_{{t}_{2}}}\right\rangle}|{\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\}$$

$$\displaystyle\forall{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}.\ \exists{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}.\ {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle}\models\mathsf{Prefix}\Rightarrow{\left\langle{{h}_{R|W},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}}\right\rangle}\models\mathsf{Serializability}$$

$$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}=\{{\left\langle{R_{{t}},W_{{t}}}\right\rangle}|{t}\in T\}\cup\{{\left\langle{W_{{t}_{1}},W_{{t}_{2}}}\right\rangle}|{\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}\}\ \cup\{{\left\langle{W_{{t}_{1}},R_{{t}_{2}}}\right\rangle}|{\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\}$$

$$\displaystyle\mathsf{RW}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1})=\{{\left\langle{{t}_{3},{t}_{2}}\right\rangle}|\exists{x}\in\mathsf{vars}({h}).\ \exists{t}_{1}\in T^{\prime}.\ {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}^{\prime},{\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1},{{t}_{2}}\ \mathsf{writes}\ {{x}}\}$$

$$\mathsf{Causal}\Rightarrow \mathsf{Read}\mathsf{Atomic}\Rightarrow \mathsf{Read}\mathsf{Committed}$$

$$\mathsf{Prefix}\Rightarrow \mathsf{Causal}$$

$$\mathsf{Serializability}\Rightarrow \mathsf{Prefix}\wedge \mathsf{Conflict}$$

$$\displaystyle\exists{x},\ \exists{t}_{1},{t}_{2},\ \exists\alpha,\beta.\ {\left\langle{{t}_{1},\alpha}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}\land{{t}_{2}}\ \mathsf{writes}\ {{x}}\ \land{\left\langle{{t}_{2},\beta}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\land{\left\langle{\beta,\alpha}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{po}}\land{\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}.$$

$$\displaystyle\exists{x},\exists{t}_{1},{t}_{2},{t}_{3}.\ {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}\land{{t}_{2}}\ \mathsf{writes}\ {{x}}\ \land{\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\land{\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}.$$

$$\displaystyle\exists{x},\exists{t}_{1},{t}_{2},{t}_{3}.\ {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}\land{{t}_{2}}\ \mathsf{writes}\ {{x}}\ \land{\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+}\land{\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}.$$

$$\displaystyle\exists{x},\exists{t}_{1},{t}_{2},{t}_{3},{t}_{4}.\ {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}\land{{t}_{2}}\ \mathsf{writes}\ {{x}}\ \land{\left\langle{{t}_{2},{t}_{4}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*}\land{\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}$$

$$\displaystyle\mathsf{WR}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1})=\{{\left\langle{W_{{t}_{1}},R_{{t}_{2}}}\right\rangle}|$$

$$\displaystyle{\left\langle{R_{{t}_{2}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}_{2,1}}}^{\prime},$$

$$\displaystyle{\left\langle{W_{{t}_{1}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1},{W_{{t}_{1}}}\ \mathsf{writes}\ {{x}_{2,1}}\}$$

Full text

††conference: ACM SIGPLAN Conference on Programming Languages; January 01–03, 2018; New York, NY, USA††journalyear: 2018††doi: ††copyright: none††ccs: Software and its engineering General programming languages††ccs: Social and professional topics History of programming languages

1. Introduction

Transactions simplify concurrent programming by enabling computations on shared data that are isolated from other concurrent computations and resilient to failures. Modern databases provide transactions in various forms corresponding to different tradeoffs between consistency and availability. The strongest level of consistency is achieved with serializable transactions (Papadimitriou, 1979) whose outcome in concurrent executions is the same as if the transactions were executed atomically in some order. Unfortunately, serializability carries a significant penalty on the availability of the system assuming, for instance, that the database is accessed over a network that can suffer from partitions or failures. For this reason, modern databases often provide weaker guarantees about transactions, formalized by weak consistency models, e.g., causal consistency (Lamport, 1978) and snapshot isolation (Berenson et al., 1995).

Implementations of large-scale databases providing transactions are difficult 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 difficult to design and reason about. The black-box testing framework Jepsen (jep, [n. d.]a) found a remarkably large number of subtle problems in many production distributed databases.

Testing a transactional database raises two issues: (1) deriving a suitable set of testing scenarios, e.g., faults to inject into the system and the set of transactions to be executed, and (2) deriving efficient algorithms for checking whether a given execution satisfies the considered consistency model. The Jepsen framework aims to address the first issue by using randomization, e.g., introducing faults at random and choosing the operations in a transaction randomly. The effectiveness of this approach has been proved formally in recent work (Ozkan et al., 2018). The second issue is, however, largely unexplored. Jepsen checks consistency in a rather ad-hoc way, focusing on specific classes of violations to a given consistency model, e.g., dirty reads (reading values from aborted transactions). This problem is challenging because the consistency specifications 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 (Papadimitriou, 1979), and checking causal consistency in a non-transactional context is known to be polynomial time (Bouajjani et al., 2017). In this work, we try to fill this gap by investigating the complexity of this problem w.r.t. several consistency models and, in case of NP-completeness, devising algorithms that are polynomial time assuming fixed 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) (Berenson et al., 1995), requires that every value read in a transaction is written by a committed transaction. Read Atomic (RA) (Cerone et al., 2015) requires that successive reads of the same variable in a transaction return the same value (also known as Repeatable Reads (Berenson et al., 1995)), 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 (Terry et al., 1994), an abstraction of the sequence of transactions performed during the execution of an application. Causal Consistency (CC) (Lamport, 1978) requires that if a transaction ${t}_{1}$ “affects” 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) (Burckhardt et al., 2015) requires that there exists a total commit order between all the transactions such that each transaction observes a prefix of this sequence. Snapshot Isolation (SI) (Berenson et al., 1995) further requires that two different transactions observe different prefixes if they both write to a common variable. Finally, we also provide new results concerning the problem of checking serializability (SER) that complement the known result about its NP-completeness.

The algorithmic issues we explore in this paper have led to a new specification 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 defined effectively. 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 identifiers (e.g., a local counter that is incremented with every new write coupled with a client/session identifier)111This is also used in Jepsen, e.g., checking dirty reads in Galera (jep, [n. d.]b).. Since practical database implementations are data-independent (Wolper, 1986), 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 (Bouajjani et al., 2017; Burckhardt et al., 2014; Cerone et al., 2015) has formalized such consistency models using two auxiliary relations: a visibility relation defining for each transaction the set of transactions it observes, and a commit order defining the order in which transactions are committed to the “global” memory. An execution satisfying some consistency model is defined 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 simplification allows us to state a series of axioms defining these consistency models, which have a common shape. Intuitively, they define 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 differences between these consistency models, these axioms are essential for the algorithmic issues we investigate afterwards.

We establish that checking whether an execution satisfies 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 verification problem becomes polynomial time provided that, roughly speaking, the number of sessions in the input executions is considered to be fixed (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 fixed. (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 (Chalupa et al., 2018). 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 fixed size.

We provide an experimental evaluation of our algorithms on executions of CockroachDB (coc, [n. d.]a), which claims to implement serializability (coc, [n. d.]b) acknowledging however the possibility of anomalies, Galera (gal, [n. d.]a), whose documentation contains contradicting claims about whether it implements snapshot isolation (gal, [n. d.]b, [n. d.]c), and AntidoteDB (ant, [n. d.]a), which claims to implement causal consistency (ant, [n. d.]b). Our implementation reports violations of these criteria in all cases. The consistency violations we found for AntidoteDB are novel and have been confirmed by its developers. We show that our algorithms are efficient 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.

To summarize, the contributions of this work are fourfold:

• •

We develop a new specification framework for describing common transactional-consistency criteria (§2);

• •

We show that checking RC, RA, and CC is polynomial time while checking PC and SI is NP-complete (§3);

• •

We show that PC, SI, and SER are polynomial-time checkable assuming that the communication graph of the input execution has fixed-size biconnected components (§4 and §5);

• •

We perform an empirical evaluation of our algorithms on executions generated by production databases (§6);

Combined, these contributions form an effective algorithmic framework for the verification of transactional-consistency models. To the best of our knowledge, we are the first to investigate the asymptotic complexity for most of these consistency models, despite their prevalence in practice.

2. Consistency Criteria

2.1. Histories

We consider a transactional database storing a set of variables $\mathsf{Var}=\{{x},{y},\ldots\}$. Clients interact with the database by issuing transactions formed of read and write operations. Assuming an unspecified set of values $\mathsf{Val}$ and a set of operation identifiers $\mathsf{OpId}$, we let

[TABLE]

be the set of operations reading a value ${v}$ or writing a value ${v}$ to a variable ${x}$. We omit operation identifiers when they are not important.

Definition 2.1.

A transaction {\left\langle{O,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{po}}}\right\rangle} is a finite set of operations $O$ along with a strict total order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{po}} on $O$, called program order.

We use ${t}$, ${t}_{1}$, ${t}_{2}$, $\ldots$ to range over transactions. The set of read, resp., write, operations in a transaction ${t}$ is denoted by $\mathsf{reads}({{t}})$, resp., $\mathsf{writes}({{t}})$. The extension to sets of transactions is defined as usual. Also, we say that a transaction ${t}$ writes a variable ${x}$, denoted by ${{t}}\ \mathsf{writes}\ {{x}}$, when $\textsf{write}_{{i}}({{x}},{{v}})\in\mathsf{writes}({{t}})$ for some ${i}$ and ${v}$. Similarly, a transaction ${t}$ reads a variable ${x}$ when $\textsf{read}_{{i}}({{x}},{{v}})\in\mathsf{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 ${x}$ 222That is, for every transaction ${t}$, and every $\textsf{write}({{x}},{{v}}),\textsf{write}({{y}},{{v}^{\prime}})\in\mathsf{writes}({{t}})$, we have that ${x}\neq{y}$., and that a read of a variable ${x}$ cannot be preceded by a write to ${x}$ in the same transaction333That is, for every transaction {t}={\left\langle{O,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{po}}}\right\rangle}, if $\textsf{write}({{x}},{{v}})\in\mathsf{writes}({{t}})$ and there exists $\textsf{read}({{x}},{{v}})\in\mathsf{reads}({{t}})$, then we have that {\left\langle{\textsf{read}({{x}},{{v}}),\textsf{write}({{x}},{{v}})}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{po}}. 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 1(a) should not return 1 because this is not the last value written to x by the other transaction. It can return the initial value or 2. 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 1(b) can only return 2 (assuming that there are no other writes on x in the same transaction). These two properties can be verified 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 effect of aborted transactions should not be visible to other transactions, and therefore, they can be ignored. For instance, the read(x) in Figure 1(c) should not return the value 1 written by the aborted transaction. The transactions are ordered according to a (partial) session order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} which represents ordering constraints imposed by the applications using the database. Most often, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} is a union of sequences, each sequence being called a session. We assume that the history includes a write-read relation that identifies 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 (Wolper, 1986), 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.

Definition 2.2.

A history {\left\langle{T,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}}\right\rangle} is a set of transactions $T$ along with a strict partial order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} called session order, and a relation {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\subseteq T\times\mathsf{reads}({T}) called write-read relation, s.t.

• •

the inverse of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}} is a total function, and if ({t},\textsf{read}({{x}},{{v}}))\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}, then $\textsf{write}({{x}},{{v}})\in{t}$, and

• •

{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{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 {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}. We use ${h}$, ${h}_{1}$, ${h}_{2}$, $\ldots$ to range over histories.

We say that the read operation $\textsf{read}({{x}},{{v}})$ reads value ${v}$ from variable ${x}$ written by ${t}$ when ({t},\textsf{read}({{x}},{{v}}))\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}. For a given variable ${x}$, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} denotes the restriction of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}} to reads of variable ${x}$, i.e., , {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cap(T\times\{\textsf{read}({{x}},{{v}})\mid{v}\in\mathsf{Val}\}). Moreover, we extend the relations {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}} and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} to pairs of transactions as follows: {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}, resp., {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}, iff there exists a read operation $\textsf{read}({{x}},{{v}})\in\mathsf{reads}({{t}_{2}})$ such that {\left\langle{{t}_{1},\textsf{read}({{x}},{{v}})}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}, resp., {\left\langle{{t}_{1},\textsf{read}({{x}},{{v}})}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}. We say that the transaction ${t}_{1}$ is read by the transaction ${t}_{2}$ when {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}, and that it is read when it is read by some transaction ${t}_{2}$.

2.2. Axiomatic Framework

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 satisfies a certain criterion if there exists a strict total order on its transactions, called commit order and denoted by {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, which extends the write-read relation and the session order, and which satisfies 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 define mandatory {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} predecessors ${t}_{2}$ of a transaction ${t}_{1}$ that is read in the history. For instance, the criterion called Read Committed (RC) (Berenson et al., 1995) 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 past444This monotonicity property corresponds to the fact that in the original formulation of Read Committed (Berenson et al., 1995), every write is guarded by the acquisition of a lock on the written variable, that is held until the end of the transaction.. While the first condition holds for any history (because of the surjectivity of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}), the second condition is expressed by the axiom $\mathsf{Read\ Committed}$ in Figure 2(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, Figure 3(a) shows a history and a (partial) commit order that does not satisfy this axiom because ${\tt read(x)}$ returns the value written in a transaction “older” than the transaction read in the previous ${\tt read(y)}$. An example of a history and commit order satisfying this axiom is given in Figure 3(b).

More precisely, the axioms are first-order formulas555These formulas are interpreted on tuples {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} of a history ${h}$ and a commit order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} on the transactions in ${h}$ as usual. of the following form:

[TABLE]

where $\phi$ is a property relating ${t}_{2}$ and $\alpha$ (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 $\alpha$ to read specifically $t_{1}$’s write on $x$, it must be the case that every $t_{2}$ that also writes $x$ and satisfies $\phi(t_{2},\alpha)$ was committed before $t_{1}$. Note that in all cases we consider, $\phi(t_{2},\alpha)$ already ensures that $t_{2}$ is committed before the read $\alpha$, so this axiom schema ensures that $t_{2}$ is furthermore committed before $t_{1}$’s write.

The axioms used throughout the paper are given in Figure 2. The property $\phi$ relates ${t}_{2}$ and $\alpha$ 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 defining them. Read Atomic (RA) (Cerone et al., 2015) is a strengthening of Read Committed defined by the axiom $\mathsf{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 {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}} or {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} predecessors of ${t}_{3}$ writing ${x}$ must precede ${t}_{1}$ in commit order. The case of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}} predecessors corresponds to the Repeatable Read criterion in (Berenson et al., 1995) which requires that successive reads of the same variable in the same transaction return the same value, Figure 3(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}^{\prime}$ (w.r.t. the commit order) that is read by ${t}$, Figure 3(d) showing a violation (for any commit order between the transactions on the left, either ${\tt read(x)}$ or ${\tt read(y)}$ will return a value not written by the maximal transaction). The case of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} predecessors corresponds to the “read-my-writes” guarantee (Terry et al., 1994) concerning sessions, which states that a transaction ${t}$ must observe previous writes in the same session. For instance, read(y) returning 1 in Figure 3(c) shows that the last transaction on the right does not satisfy this guarantee: the transaction writing 1 to y was already visible to that session before it wrote 2 to y, and therefore the value 2 should have been read. $\mathsf{Read\ Atomic}$ requires that the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} predecessor of the transaction reading y be ordered in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} before the transaction writing 1 to y, which makes the union {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}} cyclic.

The following lemma shows that for histories satisfying $\mathsf{Read\ Atomic}$, the inverse of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} extended to transactions is a total function (see Appendix A for the proof).

Lemma 2.3.

Let {h}={\left\langle{T,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}}\right\rangle} be a history. If {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} satisfies $\mathsf{Read\ Atomic}$, then for every transaction ${t}$ and two reads $\textsf{read}_{{i}_{1}}({{x}},{{v}_{1}}),\textsf{read}_{{i}_{2}}({{x}},{{v}_{2}})\in\mathsf{reads}({{t}})$, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}^{-1}(\textsf{read}_{{i}_{1}}({{x}},{{v}_{1}}))={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}^{-1}(\textsf{read}_{{i}_{2}}({{x}},{{v}_{2}})) and ${v}_{1}={v}_{2}$.

Causal Consistency (CC) (Lamport, 1978) is defined by the axiom $\mathsf{Causal}$, which states that for any transaction ${t}_{1}$ writing a variable ${x}$ that is read in a transaction ${t}_{3}$, the set of ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+} predecessors of ${t}_{3}$ writing ${x}$ must precede ${t}_{1}$ in commit order (({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+} is usually called the causal order). A violation of this axiom can be found in Figure 3(e): the transaction ${t}_{2}$ writing 2 to x is a ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+} predecessor of the transaction ${t}_{3}$ reading 1 from x because the transaction ${t}_{4}$, writing 1 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 1 to x, which again, is inconsistent with the write-read relation (${t}_{2}$ reads from ${t}_{1}$).

Prefix consistency (PC) (Burckhardt et al., 2015) is a strengthening of CC, which requires that every transaction observes a prefix of a commit order between all the transactions. With the intuition that the observed transactions are {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} predecessors, the axiom $\mathsf{Prefix}$ defining PC, states that for any transaction ${t}_{1}$ writing a variable ${x}$ that is read in a transaction ${t}_{3}$, the set of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*} predecessors of transactions observed by ${t}_{3}$ writing ${x}$ must precede ${t}_{1}$ in commit order (we use {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*} to say that even the transactions observed by ${t}_{3}$ must precede ${t}_{1}$). This ensures the prefix property stated above. An example of a PC violation can be found in Figure 3(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=1, y=2 or x=2, y=1 cannot be produced at the end of a prefix in this serialization.

Snapshot Isolation (SI) (Berenson et al., 1995) is a strengthening of PC that disallows two transactions to observe the same prefix of a commit order if they conflict, i.e., write to a common variable. It is defined by the conjunction of $\mathsf{Prefix}$ and another axiom called $\mathsf{Conflict}$, which requires that for any transaction ${t}_{1}$ writing a variable ${x}$ that is read in a transaction ${t}_{3}$, the set of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*} predecessors writing ${x}$ of transactions conflicting with ${t}_{3}$ and before ${t}_{3}$ in commit order, must precede ${t}_{1}$ in commit order. Figure 3(g) shows a $\mathsf{Conflict}$ violation.

Finally, Serializability (SER) (Papadimitriou, 1979) is defined 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 {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} predecessors of ${t}_{3}$ writing ${x}$ must precede ${t}_{1}$ in commit order. This ensures that each transaction observes the effects of all the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} predecessors. Figure 3(h) shows a $\mathsf{Serializability}$ violation.

Lemma 2.4.

The following entailments hold:

[TABLE]

Definition 2.5.

Given a set of axioms $X$ defining a criterion $C$ like in Table 1, a history {h}={\left\langle{T,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}}\right\rangle} satisfies $C$ iff there exists a strict total order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} such that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} and {\left\langle{h,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} satisfies $X$.

Definition 2.5 and Lemma 2.4 imply that each consistency criterion in Table 1 is stronger than its predecessors (reading them from top to bottom), e.g., CC is stronger than RA and RC. This relation is strict, e.g., RA is not stronger than CC. These definitions are equivalent with previous formalizations by Cerone et al. (2015) (see Appendix E).

3. Checking Consistency Criteria

This section establishes the complexity of checking the different consistency criteria in Table 1 for a given history. More precisely, we show that Read Committed, Read Atomic, and Causal Consistency 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 defining those consistency criteria do not contain the commit order ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{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 Figure 4(a) and Figure 4(b). Applying the axiom in Figure 2(b) on the first history, since the transaction on the right reads 2 from ${y}$, we get that its {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} predecessor (i.e., the first transaction on the left) must precede the transaction writing 2 to ${y}$ in commit order (the red edge). This holds because the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} predecessor writes on ${y}$. Similarly, since the same transaction reads 1 from ${x}$, we get that its {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{y}}} predecessor must precede the transaction writing 1 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 4(b), all the axiom instantiations are vacuous, i.e., the left part of the entailment is false, and therefore, it satisfies RA. Checking CC on the history in Figure 4(c) requires a single saturation step: since the transaction on the bottom right reads 1 from ${x}$, its {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}\mathop{;}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{y}}} predecessor that writes on ${x}$ (the transaction on the bottom left) must precede in commit order the transaction writing 1 to ${x}$. Since this is already inconsistent with the session order, we get that this history violates CC.

Algorithm 1 lists our procedure for checking CC. As explained above, co is initially set to {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}, and then, it is saturated with other ordering constraints implied by non-vacuous instantiations of the axiom $\mathsf{Causal}$ (where the left-hand side of the implication evaluates to true). The algorithms concerning RC and RA are defined in a similar way by essentially changing the test at line 6 so that it corresponds to the left-hand side of the implication in the corresponding axiom. Algorithm 1 can be rewritten as a Datalog program containing straightforward Datalog rules for computing transitive closures and relation composition, and a rule of the form666We write Datalog rules using a standard notation $\mathit{head}\text{ :- }\mathit{body}$ where $\mathit{head}$ is a relational atom (written as ${\left\langle{a,b}\right\rangle}\in R$ where $a$, $b$ are elements and $R$ a binary relation) and $\mathit{body}$ is a list of relational atoms.

[TABLE]

to represent the $\mathsf{Causal}$ axiom. The following is a consequence of the fact that these algorithms run in polynomial time (or equivalently, the Datalog programs can be evaluated in polynomial time over a database that contains the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}} and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} relations in a given history).

Theorem 3.1.

For any criterion $C\in\{\emph{{Read Committed}},\emph{{Read Atomic}},\emph{{Causal consistency}}\}$, 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 satisfiability (SAT) that covers uniformly all the three cases. In the case of SER, it provides a new proof of the NP-completeness result by Papadimitriou (1979) which uses a reduction from the so-called non-circular SAT and which cannot be extended to PC and SI.

Theorem 3.2.

For any criterion $C\in\{\emph{{Prefix Consistency}},\emph{{Snapshot Isolation}},\emph{{Serializability}}\}$ 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 satisfies the corresponding axioms. This shows that the problem is in NP.

To show NP-hardness, we define a reduction from boolean satisfiability. Therefore, let $\varphi=D_{1}\land\ldots\land D_{m}$ be a CNF formula over the boolean variables $x_{1},\ldots,x_{n}$ where each $D_{i}$ is a disjunctive clause with $m_{i}$ literals. Let $\lambda_{ij}$ denote the $j$-th literal of $D_{i}$.

We construct a history $h_{\varphi}$ such that $\varphi$ is satisfiable if and only if $h_{\varphi}$ satisfies PC, SI, or SER. Since $SER\Rightarrow SI\Rightarrow PC$, we show that (1) if $h_{\varphi}$ satisfies PC, then $\varphi$ is satisfiable, and (2) if $\varphi$ is satisfiable, then $h_{\varphi}$ satisfies SER.

The main idea of the construction is to represent truth values of each of the variables and literals in $\varphi$ with the polarity of the commit order between corresponding transaction pairs. For each variable $x_{k}$, $h_{\varphi}$ contains a pair of transactions $a_{k}$ and $b_{k}$, and for each literal $\lambda_{ij}$, $h_{\varphi}$ contains a set of transactions $w_{ij}$, $y_{ij}$ and $z_{ij}$ 777We assume that the transactions $a_{k}$ and $b_{k}$ associated to a variable $x_{k}$ are distinct and different from the transactions associated to another variable $x_{k^{\prime}}\neq x_{k}$ or to a literal $\lambda_{ij}$. Similarly, for the transactions $w_{ij}$, $y_{ij}$ and $z_{ij}$ associated to a literal $\lambda_{ij}$.. We want to have that $x_{k}$ is false if and only if {\left\langle{a_{k},b_{k}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}, and $\lambda_{ij}$ is false if and only if {\left\langle{y_{ij},z_{ij}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{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_{\varphi}$ should ensure that the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} ordering constraints corresponding to an assignment that falsifies the formula (i.e., one of its clauses) form a cycle. To achieve that, we add all pairs ${\left\langle{z_{ij},y_{i,(j+1)\%m_{i}}}\right\rangle}$ in the session order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}. An unsatisfied clause $D_{i}$, i.e., every $\lambda_{ij}$ is false, leads to a cycle of the form y_{i1}\xrightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}}z_{i1}\xrightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}}y_{i2}\xrightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}z_{i2}\cdots z_{im_{i}}\xrightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}}y_{i1}.

The most complicated part of the construction is to ensure the consistency between the truth value of the literals and the truth value of the variables, e.g., $\lambda_{ij}=x_{k}$ is false iff $x_{k}$ is false. We use special sub-histories to enforce that if history $h_{\varphi}$ satisfies PC (i.e., the axiom $\mathsf{Prefix}$), then there exists a commit order co such that {\left\langle{h_{\varphi},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} satisfies $\mathsf{Prefix}$ (Figure 2(d)) and:

[TABLE]

Figure 5(a) shows the sub-history associated to a positive literal $\lambda_{ij}=x_{k}$ while Figure 5(b) shows the case of a negative literal $\lambda_{ij}=\neg x_{k}$.

For a positive literal $\lambda_{ij}=x_{k}$ (Figure 5(a)), (1) we enrich session order with the pairs ${\left\langle{y_{ij},a_{k}}\right\rangle}$ and ${\left\langle{b_{k},w_{ij}}\right\rangle}$, (2) we include writes to a variable $v_{ij}$ in the transactions $y_{ij}$ and $z_{ij}$, and (3) we make $w_{ij}$ read from $z_{ij}$, $i.e.,$ {\left\langle{z_{ij},w_{ij}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}_{v_{ij}}. The case of a negative literal is similar, switching the roles of $a_{k}$ and $b_{k}$.

This construction ensures that if the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} goes downwards on the right-hand side ({\left\langle{a_{k},b_{k}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} in the case of a positive literal, and {\left\langle{b_{k},a_{k}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} in the case of a negative literal), then it must also go downwards on the left-hand side ({\left\langle{y_{ij},z_{ij}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}) to satisfy $\mathsf{Prefix}$. For instance, in the case of a positive literal, note that if {\left\langle{a_{k},b_{k}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, then {\left\langle{y_{ij},w_{ij}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\mathop{;}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}\mathop{;}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}. Therefore, for every commit order co such that {\left\langle{h_{\varphi},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} satisfies $\mathsf{Prefix}$, {\left\langle{a_{k},b_{k}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}} implies {\left\langle{y_{ij},z_{ij}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. Indeed, if {\left\langle{a_{k},b_{k}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}, instantiating the $\mathsf{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 {\left\langle{y_{ij},z_{ij}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}.

In contrast, when the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} goes upwards on the right-hand side ({\left\langle{b_{k},a_{k}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} in the case of a positive literal, and {\left\langle{a_{k},b_{k}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} in the case of a negative literal) then it imposes no constraint on the direction of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} on the left-hand side. Therefore, any commit order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} satisfying $\mathsf{Prefix}$ that goes upwards on the right-hand side (e.g., {\left\langle{b_{k},a_{k}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} in the case of a positive literal) and downwards on the left-hand side ({\left\langle{y_{ij},z_{ij}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}) in some sub-history (associated to some literal), thereby contradicting Property (1), can be modified into another commit order satisfying $\mathsf{Prefix}$ that goes upwards on the left-hand side as well. Formally, let co be a commit order such that {\left\langle{h_{\varphi},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} satisfies $\mathsf{Prefix}$ and

[TABLE]

for some literal $\lambda_{ij}=x_{k}$ (the case of negative literals can be handled in a similar manner). Let {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}_{1} be the restriction of co on the set of tuples

[TABLE]

Since {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}_{1}\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}, we have that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}_{1} is acyclic. Let {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}_{2} be a relation obtained from {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}_{1} by flipping the order between $y_{ij}$ and $z_{ij}$ (i.e., {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}_{2}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}_{1}\setminus\{{\left\langle{y_{ij},z_{ij}}\right\rangle}\}\cup\{{\left\langle{z_{ij},y_{ij}}\right\rangle}\}). This flipping does not introduce any cycle because {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}_{2} contains no path ending in $z_{ij}$ (see Fig 5(a)). Also, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}_{2} still satisfies the $\mathsf{Prefix}$ axiom (since {\left\langle{b_{k},a_{k}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}_{2} there is no path from $y_{ij}$ to $w_{ij}$ satisfying the constraints in the $\mathsf{Prefix}$ axiom). Since {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}_{2} is acyclic, it can be extended to a total commit order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}_{3} that satisfies $\mathsf{Prefix}$. This is a consequence of the following lemma whose proof follows easily from definitions (the part of this lemma concerning $\mathsf{Serializability}$ will be used later).

Lemma 3.3.

Let {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} be an acyclic relation that includes {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}, ${\left\langle{a_{k},b_{k}}\right\rangle}$ or ${\left\langle{b_{k},a_{k}}\right\rangle}$, for each $k$, and ${\left\langle{y_{ij},z_{ij}}\right\rangle}$ or ${\left\langle{z_{ij},y_{ij}}\right\rangle}$, for each $i$, $j$. For each axiom $A\in\{\mathsf{Prefix},\mathsf{Serializability}\}$, if {\left\langle{h_{\varphi},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} satisfies $A$, then there exists a total commit order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} such that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} and {\left\langle{h_{\varphi},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}}\right\rangle} satisfies $A$.

Therefore, {\left\langle{h_{\varphi},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{3}}\right\rangle} satisfies $\mathsf{Prefix}$, and {\left\langle{b_{k},a_{k}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}_{3}\land{\left\langle{z_{ij},y_{ij}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}_{3} ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{3} goes upwards on both sides of a sub-history like in Figure 5(a)). This transformation can be applied iteratively until obtaining a commit order that satisfies both $\mathsf{Prefix}$ and Property (1).

Next, we complete the correctness proof of this reduction. For the “if” direction, if $h_{\varphi}$ satisfies PC, then there exists a total commit order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} between the transactions described above, which together with $h_{\varphi}$ satisfies $\mathsf{Prefix}$. The assignment of the variables $x_{k}$ explained above (defined by the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} order between $a_{k}$ and $b_{k}$, for each $k$) satisfies the formula $\varphi$ since there exists no cycle between the transactions $y_{ij}$ and $z_{ij}$, which implies that for each clause $D_{i}$, there exists a $j$ such that {\left\langle{y_{ij},z_{ij}}\right\rangle}\not\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}} which means that $\lambda_{ij}$ is satisfied. For the “only-if” direction, let $\gamma$ be a satisfying assignment for $\varphi$. Also, let {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{\prime} be a binary relation that includes {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}} such that if $\gamma(x_{k})=\mathit{false}$, then {\left\langle{a_{k},b_{k}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{\prime}, {\left\langle{y_{ij},z_{ij}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{\prime} for each $\lambda_{ij}=x_{k}$, and {\left\langle{z_{ij},y_{ij}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{\prime} for each $\lambda_{ij}=\neg x_{k}$, and if $\gamma(x_{k})=\mathit{true}$, then {\left\langle{b_{k},a_{k}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{\prime}, {\left\langle{z_{ij},y_{ij}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{\prime} for each $\lambda_{ij}=x_{k}$, and {\left\langle{y_{ij},z_{ij}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{\prime} for each $\lambda_{ij}=\neg x_{k}$. Note that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{\prime} is acyclic: no cycle can contain $w_{ij}$ because $w_{ij}$ has no “outgoing” dependency (i.e., {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{\prime} contains no pair with $w_{ij}$ as a first 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}\neq 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}\neq i_{2}$ since these are disconnected as well, and finally, there is no cycle including only transactions $y_{ij}$ and $z_{ij}$, for a fixed $i$, because $\varphi$ is satisfiable. By Lemma 3.3, the acyclic relation {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} can be extended to a total commit order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} which together with $h_{\varphi}$ satisfies the $\mathsf{Serializability}$ axiom. Therefore, $h_{\varphi}$ satisfies SER. ∎

4. Checking Consistency of Bounded-Width Histories

In this section, we show that checking prefix 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 fixed constant. If we consider the standard case where the session order is a union of transaction sequences (modulo the fictitious 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 which is polynomial time when the width is bounded by a fixed constant. In general, the asymptotic complexity of this algorithm is exponential in the width of the history, but this worst-case behavior is not exercised in practice as shown in Section 6. Then, we prove that checking prefix consistency and snapshot isolation can be reduced in polynomial time to the problem of checking serializability.

4.1. Checking Serializability

We present an algorithm for checking serializability of a given history which constructs a valid commit order (satisfying $\mathsf{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. {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}), and the next transaction to linearize is chosen among the immediate {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{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 $\mathsf{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 {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} antichains. If the width of the history is bounded (by a fixed constant), then the number of possible {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{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}={\left\langle{T,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}}\right\rangle} is a set of transactions $T^{\prime}\subseteq T$ such that all the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} predecessors of transactions in $T^{\prime}$ are also in $T^{\prime}$, i.e., \forall{t}\in T.\ {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}^{-1}({t})\in T. A prefix $T^{\prime}$ is uniquely determined by the set of transactions in $T^{\prime}$ which are maximal w.r.t. {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}. This set of transactions forms an antichain of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}, i.e., any two elements in this set are incomparable w.r.t. {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}. Given an antichain $\{{t}_{1},\ldots,{t}_{n}\}$ of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}, we say that $\{{t}_{1},\ldots,{t}_{n}\}$ is the boundary of the prefix T^{\prime}=\{t:\exists i.\ {\left\langle{t,t_{i}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\lor t=t_{i}\}. For instance, given the history in Figure 6(a), the set of transactions $\{{t}_{0},{t}_{1},{t}_{2}\}$ is a prefix with boundary $\{{t}_{1},{t}_{2}\}$ (the latter is an antichain of the session order).

A prefix $T^{\prime}$ of a history ${h}$ is called serializable iff there exists a partial commit order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} on the transactions in ${h}$ such that the following hold:

• •

{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} does not contradict the session order and the write-read relation in ${h}$, i.e., {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is acyclic,

• •

{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is a total order on transactions in $T^{\prime}$,

• •

{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} orders transactions in $T^{\prime}$ before transactions in $T\setminus T^{\prime}$, i.e., {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} for every ${t}_{1}\in T^{\prime}$ and ${t}_{2}\in T\setminus T^{\prime}$,

• •

{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} does not order any two transactions ${t}_{1},{t}_{2}\not\in T^{\prime}$

• •

the history ${h}$ along with the commit order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} satisfies the axiom defining serializability, i.e., {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle}\models\mathsf{Serialization}.

For the history in Figure 6(a), the prefix $\{{t}_{0},{t}_{1},{t}_{2}\}$ is serializable since there exists a partial commit order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} which 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 $\mathsf{Serialization}$ is satisfied trivially, since the prefix contains a single transaction writing ${x}$ and all the transactions outside of the prefix do not read ${x}$.

A prefix $T^{\prime}\uplus\{{t}\}$ of ${h}$ is called a valid extension of a serializable prefix $T^{\prime}$ of ${h}$ 888We assume that ${t}\not\in T^{\prime}$ which is implied by the use of the disjoint union $\uplus$., denoted by $T^{\prime}\vartriangleright T^{\prime}\uplus\{{t}\}$if:

• •

${t}$ does not read from a transaction outside of $T^{\prime}$, i.e., for every ${t}^{\prime}\in T\setminus T^{\prime}$, {\left\langle{{t}^{\prime},{t}}\right\rangle}\not\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}, and

• •

for every variable ${x}$ written by ${t}$, there exists no transaction ${t}_{2}\neq{t}$ outside of $T^{\prime}$ which reads a value of ${x}$ written by a transaction ${t}_{1}$ in $T^{\prime}$, i.e., for every ${x}$ written by ${t}$ and every ${t}_{1}\in T^{\prime}$ and ${t}_{2}\in T\setminus(T^{\prime}\uplus\{{t}\})$, {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\not\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}.

For the history in Figure 6(a), we have $\{{t}_{0},{t}_{1}\}\vartriangleright\{{t}_{0},{t}_{1}\}\uplus\{{t}_{2}\}$ because ${t}_{2}$ reads from ${t}_{0}$ and it does not write any variable. On the other hand $\{{t}_{0},{t}_{1}\}\not\vartriangleright\{{t}_{0},{t}_{1}\}\uplus\{{t}_{3}\}$ because ${t}_{3}$ writes ${x}$ and the transaction ${t}_{2}$, outside of this prefix, reads from the transaction ${t}_{0}$ included in the prefix.

Let $\vartriangleright^{*}$ denote the reflexive and transitive closure of $\vartriangleright$.

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

Lemma 4.1.

For a serializable prefix $T^{\prime}$ of a history $h$, a prefix $T^{\prime}\uplus\{{t}\}$ is serializable if it is a valid extension of $T^{\prime}$.

Proof.

Let {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} be the partial commit order for $T^{\prime}$ which satisfies the serializable prefix conditions. We extend {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} to a partial order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}\cup\{{\left\langle{{t},{t}^{\prime}}\right\rangle}|{t}^{\prime}\not\in T^{\prime}\uplus\{{t}^{\prime}\}\}. We show that {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle}\models\mathsf{Serialization}. The other conditions for $T^{\prime}\uplus\{t\}$ being a serializable prefix are satisfied trivially by {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}.

Assume by contradiction that {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} does not satisfy the axiom $\mathsf{Serialization}$. Then, there exists ${t}_{1},{t}_{2},{t}_{3}$, ${x}\in\mathsf{vars}({{h}})$ s.t. {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} and ${t}_{2}$ writes on ${x}$ and {\left\langle{{t}_{1},{t}_{2}}\right\rangle},{\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. Since {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}}\right\rangle} satisfies this axiom, at least one of these two {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} ordering constraints are of the form ${\left\langle{{t},{t}^{\prime}}\right\rangle}$ where ${t}^{\prime}\not\in T^{\prime}\uplus\{{t}\}$:

• •

the case ${t}_{1}={t}$ and ${t}_{2}\not\in T^{\prime}\uplus\{{t}\}$ is not possible because {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} contains no pair of the form {\left\langle{{t}^{\prime},\_}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} with ${t}^{\prime}\not\in T^{\prime}$ (recall that ${\left\langle{{t}_{2},{t}_{3}}\right\rangle}$ should be also included in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}).

• •

If ${t}_{2}={t}$ then, {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} and ${\left\langle{{t}_{2},{t}_{3}}\right\rangle}$ for some ${t}_{3}\not\in T^{\prime}\uplus\{{t}\}$. But, by the definition of valid extension, for all variables ${x}$ written by ${t}$, there exists no transaction ${t}_{3}\not\in T^{\prime}\uplus\{{t}\}$ such that it reads ${x}$ from ${t}_{1}\in T^{\prime}$. Therefore, this is also a contradiction. $\Box$

∎

Algorithm 2 lists our algorithm for checking serializability. It is defined as a recursive procedure that searches for a sequence of valid extensions of a given prefix (initially, this prefix is empty) until covering the whole history. Figure 6(b) pictures this search on the history in Figure 6(a). The right branch (containing blue edges) contains only valid extensions and it reaches a prefix that includes all the transactions in the history.

Theorem 4.2.

A history ${h}$ is serializable iff $\mathsf{checkSER}({h},\emptyset,\emptyset)$ returns true.

Proof.

The “if” direction is a direct consequence of Lemma 4.1. For the reverse, assume that {h}={\left\langle{T,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}}\right\rangle} is serializable with a (total) commit order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. Let {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{i} be the set of transactions in the prefix of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} of length $i$. Since {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is consistent with {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}, we have that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{i} is a prefix of ${h}$, for any $i$. We show by induction that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{i+1} is a valid extension of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{i}. The base case is trivial. For the induction step, let ${t}$ be the last transaction in the prefix of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} of length $i+1$. Then,

• •

${t}$ cannot read from a transaction outside of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{i} because {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is consistent with the write-read relation {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}},

• •

also, for every variable ${x}$ written by ${t}$, there exists no transaction ${t}_{2}\neq{t}$ outside of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{i} which reads a value of ${x}$ written by a transaction {t}_{1}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{i}. Otherwise, {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}, {\left\langle{{t},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, and {\left\langle{{t}_{1},{t}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} which implies that {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} does not satisfy $\mathsf{Serializability}$.

This implies that $\mathsf{checkSER}({h},\emptyset,\emptyset)$ returns true. ∎

By definition, the size of each antichain of a history ${h}$ is smaller than the width of ${h}$. Therefore, the number of possible antichains of a history ${h}$ is $O(\mathsf{size}(h)^{\mathsf{width}(h)})$ where $\mathsf{size}(h)$, resp., $\mathsf{width}(h)$, is the number of transactions, resp., the width, of ${h}$. Since the valid extension property can be checked in quadratic time, the asymptotic time complexity of the algorithm defined by $\mathsf{checkSER}$ is upper bounded by $O(\mathsf{size}(h)^{\mathsf{width}(h)}\cdot\mathsf{size}(h)^{3})$. The following corollary is a direct consequence of this observation.

Corollary 4.3.

For an arbitrary but fixed constant $k\in\mathbb{N}$, the problem of checking serializability for histories of width at most $k$ is polynomial time.

4.2. Reducing Prefix Consistency to Serializability

We describe a polynomial time reduction of checking prefix consistency of bounded-width histories to the analogous problem for serializability. Intuitively, as opposed to serializability, prefix 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 prefix consistency, we define 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 satisfies prefix consistency, and vice-versa. For instance, Figure 7 shows this transformation on the two histories in Figure 7(a) and Figure 7(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 4.3, implies that checking prefix consistency of bounded-width histories is polynomial time.

Thus, given a history {h}={\left\langle{T,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}}\right\rangle}, we define the history {h}_{R|W}={\left\langle{T^{\prime},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}^{\prime},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}^{\prime}}\right\rangle} as follows:

• •

$T^{\prime}$ 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^{\prime}=\{R_{t}|{t}\in T\}\cup\{W_{t}|{t}\in 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}$ iff ${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}$, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}^{\prime}=\{{\left\langle{W_{{t}_{1}},R_{{t}_{2}}}\right\rangle}|{\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{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.,

[TABLE]

The following lemma is a straightforward consequence of the definitions (see Appendix C).

Lemma 4.4.

The histories ${h}$ and ${h}_{R|W}$ have the same width.

Next, we show that ${h}_{R|W}$ is serializable if ${h}$ is prefix consistent. Formally, we show that

[TABLE]

Thus, let {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} be a commit (total) order on transactions of ${h}$ which together with ${h}$ satisfies the prefix consistency axiom. We define two partial commit orders {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2}, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2} a strengthening of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}, which we prove that they are acyclic and that any linearization {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2} is a valid witness for ${h}_{R|W}$ satisfying serializability.

Thus, let {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} be a partial commit order on transactions of ${h}_{R|W}$ defined as follows:

[TABLE]

We show that if {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{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 4.5.

The relation {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} is acyclic.

Proof. We first show that if {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{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 {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} is cyclic. Then,

• •

Since {\left\langle{W_{{t}_{1}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} implies {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, for every ${t}_{1}$ and ${t}_{2}$, a cycle in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} cannot contain only write transactions. Otherwise, it will imply a cycle in the original commit order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. Therefore, a cycle in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} must contain at least one read transaction.

• •

Assume that a cycle in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} contains two write transactions $W_{{t}_{1}}$ and $W_{{t}_{2}}$ which are not consecutive, like in Figure 8. Since either {\left\langle{W_{{t}_{1}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} or {\left\langle{W_{{t}_{1}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}, there exists a smaller cycle in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} where these two write transactions are consecutive. If {\left\langle{W_{{t}_{1}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}, then {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} contains the smaller cycle on the lower part of the original cycle (Figure 8(a)), and if {\left\langle{W_{{t}_{2}},W_{{t}_{1}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}, then {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} contains the cycle on the upper part of the original cycle (Figure 8(b)). Thus, all the write transactions in a minimal cycle of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{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 {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{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 {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{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 2, then it contains two transactions $W_{{t}_{1}}$ and $R_{{t}_{2}}$ such that {\left\langle{W_{{t}_{1}},R_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} and {\left\langle{R_{{t}_{2}},W_{{t}_{1}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}. Since all the ${\left\langle{R_{\_},W_{\_}}\right\rangle}$ dependencies in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} are of the form ${\left\langle{R_{t},W_{t}}\right\rangle}$, it follows that ${t}_{1}={t}_{2}$. Then, we have {\left\langle{W_{{t}_{1}},R_{{t}_{1}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} which implies {\left\langle{{t}_{1},{t}_{1}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}, a contradiction.

• •

if the cycle is of size 3, then it contains three transactions $W_{{t}_{1}}$, $W_{{t}_{2}}$, and $R_{{t}_{3}}$ such that {\left\langle{W_{{t}_{1}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}, {\left\langle{W_{{t}_{2}},R_{{t}_{3}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}, and {\left\langle{R_{{t}_{3}},W_{{t}_{1}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}. Using a similar argument as in the previous case, {\left\langle{R_{{t}_{3}},W_{{t}_{1}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} implies ${t}_{3}={t}_{1}$. Therefore, {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} and {\left\langle{{t}_{2},{t}_{1}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}, which contradicts the fact that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. $\Box$

We define a strengthening of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{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, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}\cup\mathsf{RW}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}) where

[TABLE]

It can be shown that any cycle in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2} would correspond to a $\mathsf{Prefix}$ violation in the original history. Therefore,

Lemma 4.6.

The relation {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2} is acyclic.

Proof. Assume that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2} is cyclic. Any minimal cycle in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2} still satisfies the properties of minimal cycles of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} proved in Lemma 4.5 (because all write transactions are still totally ordered and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2} doesn’t relate directly read transactions). So, a minimal cycle in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2} contains a read transaction and a write transaction, and at most one more write transaction.

Since {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} is acyclic, a cycle in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2}, and in particular a minimal one, must necessarily contain a dependency from \mathsf{RW}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{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 9(a) show a minimal cycle of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2} satisfying all the properties mentioned above. This cycle contains a dependency {\left\langle{R_{{t}_{3}},W_{{t}_{2}}}\right\rangle}\in\mathsf{RW}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}) which implies the existence of a write transaction $W_{{t}_{1}}$ in ${h}_{R|W}$ s.t. {\left\langle{W_{{t}_{1}},R_{{t}_{3}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}^{\prime} and {\left\langle{W_{{t}_{1}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} and $W_{{t}_{1}},W_{{t}_{2}}$ write on ${x}$ (these dependencies are represented by the black edges in Figure 9(a)). The relations between these transactions of ${h}_{R|W}$ imply that the corresponding transactions of ${h}$ are related as shown in Figure 9(b): {\left\langle{W_{{t}_{1}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} and {\left\langle{W_{{t}_{2}},W_{{t}_{4}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime*}_{1} imply {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} and {\left\langle{{t}_{2},{t}_{4}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*}, respectively, {\left\langle{W_{{t}_{1}},W_{{t}_{3}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}^{\prime} implies {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}, and {\left\langle{W_{{t}_{4}},R_{{t}_{3}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} implies {\left\langle{{t}_{4},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}. This implies that {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} doesn’t satisfy the $\mathsf{Prefix}$ axiom, a contradiction. $\Box$

Lemma 4.7.

If a history ${h}$ satisfies prefix consistency, then ${h}_{R|W}$ is serializable.

Proof.

Let {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} be any total order consistent with {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2}. Assume by contradiction that {\left\langle{{h}_{R|W},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}}\right\rangle} doesn’t satisfy $\mathsf{Serializability}$. Then, there exist ${t}^{\prime}_{1},{t}^{\prime}_{2},{t}^{\prime}_{3}\in T^{\prime}$ such that {\left\langle{{t}^{\prime}_{1},{t}^{\prime}_{2}}\right\rangle},{\left\langle{{t}^{\prime}_{2},{t}^{\prime}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} and ${t}^{\prime}_{1},{t}^{\prime}_{2}$ write on some variable ${x}$ and {\left\langle{{t}^{\prime}_{1},{t}^{\prime}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}^{\prime}. But then ${t}^{\prime}_{1},{t}^{\prime}_{2}$ are write transactions and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} must contain ${\left\langle{{t}^{\prime}_{1},{t}^{\prime}_{2}}\right\rangle}$. Therefore, \mathsf{RW}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}) and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2} should contain ${\left\langle{{t}^{\prime}_{3},{t}^{\prime}_{2}}\right\rangle}$, a contradiction with {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} being consistent with {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2}. ∎

Finally, it can be proved that any linearization {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2} satisfies $\mathsf{Serializability}$ (together with ${h}_{R|W}$). Moreover, it can also be shown that the serializability of ${h}_{R|W}$ implies that ${h}$ satisfies PC. Therefore,

Theorem 4.8.

A history ${h}$ satisfies prefix consistency iff ${h}_{R|W}$ is serializable.

Proof. The “only-if” direction is proven by Lemma 4.7. For the reverse, we show that

\forall{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}.\ \exists{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}.\ {\left\langle{{h}_{R|W},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}}\right\rangle}\models\mathsf{Serializability}

\Rightarrow{\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle}\models\mathsf{Prefix}

Thus, let {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} be a commit (total) order on transactions of ${h}_{R|W}$ which together with ${h}_{R|W}$ satisfies the serializability axiom. Let {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} be a commit order on transactions of ${h}$ defined by {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}=\{{\left\langle{{t}_{1},{t}_{2}}\right\rangle}|{\left\langle{W_{{t}_{1}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}\} ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is clearly a total order). If {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} were not to be consistent with {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}, then there would exist transactions ${t}_{1}$ and ${t}_{2}$ such that {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} and {\left\langle{{t}_{2},{t}_{1}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, which would imply that {\left\langle{W_{{t}_{1}},R_{{t}_{2}}}\right\rangle},{\left\langle{R_{{t}_{2}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} and {\left\langle{W_{{t}_{2}},W_{{t}_{1}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}, which violates the acylicity of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}. We show that {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} satisfies $\mathsf{Prefix}$. Assume by contradiction that there exists a $\mathsf{Prefix}$ violation between ${t}_{1}$, ${t}_{2}$, ${t}_{3}$, ${t}_{4}$ (shown in Figure 10(a)), i.e., for some ${x}\in\mathsf{vars}({{h}})$, {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} and ${{t}_{2}}\ \mathsf{writes}\ {{x}}$, {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, {\left\langle{{t}_{2},{t}_{4}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*} and {\left\langle{{t}_{4},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{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: {\left\langle{W_{{t}_{1}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} and {\left\langle{W_{{t}_{1}},R_{{t}_{3}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}^{\prime} because {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} and {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. Since {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} satisfies $\mathsf{Serializability}$, then {\left\langle{R_{{t}_{3}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}. But {\left\langle{{t}_{2},{t}_{4}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*} and {\left\langle{{t}_{4},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} imply that {\left\langle{W_{{t}_{2}},W_{{t}_{4}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime*} and {\left\langle{W_{{t}_{4}},R_{{t}_{3}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}^{\prime}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}^{\prime}, which show that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} is cyclic (the red cycle in Figure 10(b)), a contradiction. $\Box$

Since the history ${h}_{R|W}$ can be constructed in linear time, Lemma 4.4, Theorem 4.8, and Corollary 4.3 imply the following result.

Corollary 4.9.

For an arbitrary but fixed constant $k\in\mathbb{N}$, the problem of checking prefix consistency for histories of width at most $k$ is polynomial time.

4.3. Reducing Snapshot Isolation to Serializability

We extend the reduction of prefix consistency to serializability to the case of snapshot isolation. Compared to prefix 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 $\mathsf{Conflict}$ axiom). More precisely, for any pair of transactions ${t}_{1}$ and ${t}_{2}$ writing to a common variable, ${t}_{1}$ must observe the effects of ${t}_{2}$ or vice-versa. We refine the definition of ${h}_{R|W}$ such that any “serialization” (i.e.., commit order satisfying $\mathsf{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 11 shows this transformation on the two histories in Figure 11(a) and Figure 11(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 x12 which 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}={\left\langle{T,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}}\right\rangle}, the history {h}_{R|W}^{c}={\left\langle{T^{\prime},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}^{\prime},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}^{\prime}}\right\rangle} is defined as ${h}_{R|W}$ with the following additional construction: for every two transactions ${t}_{1}$ and ${t}_{2}\in 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\neq j\in\{1,2\}$, i.e., {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}_{1,2}}}=\{{\left\langle{R_{{t}_{1}},W_{{t}_{1}}}\right\rangle}\} and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}_{2,1}}}=\{{\left\langle{R_{{t}_{2}},W_{{t}_{2}}}\right\rangle}\}.

Note that ${h}_{R|W}$ and ${h}_{R|W}^{c}$ have the same width (the session order is defined exactly in the same way), which implies, by Lemma 4.4, that ${h}$ and ${h}_{R|W}^{c}$ have the same width.

The following result can be proved using similar reasoning as in the case of prefix consistency (see Appendix D).

Theorem 4.10.

A history ${h}$ satisfies snapshot isolation iff ${h}_{R|W}^{c}$ is serializable.

Note that ${h}_{R|W}^{c}$ and ${h}$ have the same width, and that ${h}_{R|W}^{c}$ can be constructed in linear time. Therefore, Theorem 4.10, and Corollary 4.3 imply the following result.

Corollary 4.11.

For an arbitrary but fixed constant $k\in\mathbb{N}$, the problem of checking snapshot isolation for histories of width at most $k$ is polynomial time.

5. Communication graphs

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 different 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 fictitious transaction writing the initial values), i.e., each transaction sequence corresponding to the standard notion of session 999The results can be extended to arbitrary session orders by considering maximal transaction sequences in session order instead of sessions.. We represent the sharing of variables between different sessions using an undirected graph called a communication graph. For instance, the communication graph of the history in Figure 12(a) is given in Figure 12(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 fixed constant. This is stronger than the results in Section 4 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 12(b) shows the decomposition in biconnected components of a communication graph. This graph contains 5 sessions while every biconnected component is of size at most 3. Intuitively, any potential cycle in the commit order associated to a history will contain a cycle that passes only through sessions in the same biconnected component. 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 12(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 $\mathsf{Comm}({h})=(V,E)$ where the set of vertices $V$ is the set of sessions in ${h}$ 101010The transaction writing the initial values is considered as a distinguished session., and $(v,v^{\prime})\in E$ iff the sessions $v$ and $v^{\prime}$ contain two transactions ${t}_{1}$ and ${t}_{2}$, respectively, such that ${t}_{1}$ and ${t}_{2}$ read or write a common variable ${x}$.

Lemma 5.1.

Let $C_{1}$,$\ldots$,$C_{n}$ be the biconnected components of $\mathsf{Comm}({h})$ for a history {h}={\left\langle{T,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}}\right\rangle}. Let $P_{A}$ be a path of the form of type $A$ connecting two transactions of $C_{i}$ 111111That is, transactions that are included in the sessions in $C_{i}$. Then, there is a path $P_{B}$ of the form of type $B$ connecting the same two transactions and $P_{B}$ never leaves $C_{i}$.

Proof. Type $A$ and $B$ are both of the form {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{+}. Consider a minimal path $\pi={t}_{0},\ldots,{t}_{n}$ in \bigcup_{i}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{i} between two transactions ${t}_{0}$ and ${t}_{n}$ of the same biconnected component $C$ of $\mathsf{Comm}({h})$ (i.e., from sessions in $C$). We define a path $\pi_{s}=v_{0},\ldots,v_{m}$ between sessions, i.e., vertices of $\mathsf{Comm}({h})$, which contains an edge $(v_{j},v_{j+1})$ iff $\pi$ 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}\neq v_{j}$. Since any graph decomposes to a forest of biconnected components, this path must necessarily leave and enter some biconnected component $C_{1}$ to and from the same biconnected component $C_{2}$, i.e., $\pi_{s}$ must contain two vertices $v_{j_{1}}$ and $v_{j_{2}}$ in $C_{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 $C_{2}$. Let ${t}_{1}$, ${t}_{2}$, ${t}_{3}$, ${t}_{4}$ be the transactions in the path $\pi$ 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

• •

if {\left\langle{{t}_{3},{t}_{4}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}, then there exists a smaller path between ${t}_{0}$ and ${t}_{1}$ that uses the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} relation between ${\left\langle{{t}_{3},{t}_{4}}\right\rangle}$ (we recall that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\subseteq\bigcup_{i}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{i}) instead of the transactions in $C_{2}$, pictured in Figure 13(a), which is a contradiction to the minimality of $\pi$,

• •

if {\left\langle{{t}_{4},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}, then, we have a cycle in \bigcup_{i}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{i}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}, pictured in Figure 13(b), which is also a contradiction.

Type $A$ and $B$ are of the form ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+}. “shortening” a bigger ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+} path (they are also a path in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{+} since ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+}\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}) will introduce only {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} dependencies. So a minimal ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+} never leaves a bicomponent.

Type $A$ and $B$ are of the form {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{*}\mathop{;}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}). Similar to last the case, “shortening” a bigger path will introduce only {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} dependencies. If the new {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} is at the end of the path then the new path is still of the form {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{*}\mathop{;}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}). Else, we can replace {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} with co to make a path of the form {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{*}\mathop{;}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}). So a minimal {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{*}\mathop{;}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}) never leaves a bicomponent.

Type $A$ is of the form {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{*}\mathop{;}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}} where the last co dependency is between two transactions writing on same variable and type $B$ is of the same form of type $A$ or {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{*}\mathop{;}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}. Similar to the previous cases, “shortening” a bigger path will introduce only {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} dependencies. If the new {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} is at the end, then it becomes of the form of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{*}\mathop{;}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}. Else, we can replace {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} with co to make a path of the form {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{*}\mathop{;}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}} where the last co dependency is the one from the original path. So a minimal path of type $A$ never leaves a bicomponent or it can be “shortened” to a minimal path of the form {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{*}\mathop{;}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} which never leaves a bicomponent. $\Box$

For a history {h}=(T,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}) and biconnected component $C$ of $\mathsf{Comm}({h})$, the projection of ${h}$ over transactions in sessions of $C$ is denoted by $h\downarrow C$, i.e., h\downarrow C=(T^{\prime},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}^{\prime},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}^{\prime}) where $T^{\prime}$ is the set of transactions in sessions of $C$, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}^{\prime} and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}^{\prime} are the projections of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}, respectively, on $T^{\prime}$.

Theorem 5.2.

For any criterion $X\in\{\text{RA},\text{RC},\text{CC},\text{PC},\text{SI},\text{SER}\}$, a history $h$ satisfies $X$ iff for every biconnected component $C$ of $\mathsf{Comm}({h})$, $h\downarrow C$ satisfies $X$.

Proof.

The “only-if” direction is obvious. For the “if” direction, let $C_{1}$,$\ldots$,$C_{n}$ be the biconnected components of $\mathsf{Comm}({h})$. Also, let {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{i} be the commit order that witnesses that $h\downarrow C_{i}$ satisfies $X$, for each $1\leq i\leq n$. The union \bigcup_{i}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{i} is acyclic since otherwise, any minimal cycle would be a minimal path between transactions of the same biconnected component $C_{j}$, and, by Lemma 5.1, it will include only transactions of $C_{j}$ which is a contradiction to {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{j} being a total order. We show that any linearization {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} of \bigcup_{i}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{i} along with $h$ satisfies the axioms of $X$, for every consistency model $X$.

The axioms defining RA, RC, CC, PC, and SER involve transactions that write or read a common variable, which implies that they belong to the same biconnected component. For CC, resp., PC, SER using the result from Lemma 5.1, a minimal ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+}, resp., {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{*}\mathop{;}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+}, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} path from ${t}_{2}$ to ${t}_{3}$ in Figure 2(c), resp., Figure 2(d), Figure 2(f) will include transactions in the same biconnected component as ${t}_{2}$ and ${t}_{3}$, since “shortening” a bigger path will introduce only {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} dependencies. Therefore, they must be satisfied by {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}.

For SI, it’s only necessary to discuss the axiom $\mathsf{Conflict}$ (the satisfaction of $\mathsf{Prefix}$ is proved as for PC). Following Figure 2(e) and Lemma 5.1, any {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{*}\mathop{;}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}} path connecting ${t}_{2}$, and ${t}_{3}$ where the last co dependency is between two transactions writing on same variables, has either a minimal path of the same form that never leaves the same bicomponent as ${t}_{2},{t}_{3}$, or a minimal path of the form {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}^{*}\mathop{;}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}. Since the bicomponent satisfies SI or particularly $\mathsf{Prefix}$ and $\mathsf{Conflict}$, for all possible ${t}_{1}$, ${t}_{1},{t}_{2},{t}_{3}$, it must satisfy $\mathsf{Conflict}$. Note that ${t}_{3}$ cannot be the first transaction in its session because a path from ${t}_{2}$ to ${t}_{3}$ passing through ${t}_{4}$ (which belongs to a different biconnected component) will necessarily have to pass twice through ${t}_{3}$ which would imply that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is cyclic. Thus, $\mathsf{Conflict}$ must be satisfied by {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. ∎

Since the decomposition of a graph into biconnected components can be done in linear time, Theorem 5.2 implies that any of the criteria PC, SI, or SER can be checked in time $O(\mathsf{size}(h)^{\mathsf{bi\text{-}size}(h)}\cdot\mathsf{size}(h)^{3}\cdot\mathsf{bi\text{-}nb}(h))$ where $\mathsf{bi\text{-}size}(h)$ and $\mathsf{bi\text{-}nb}(h)$ are the maximum size of a biconnected component in $\mathsf{Comm}({h})$ and the number of biconnected components of $\mathsf{Comm}({h})$, respectively. The following corollary is a direct consequence of this observation.

Corollary 5.3.

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

6. Experimental Evaluation

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

• •

are efficient and scalable, and they outperform a SAT encoding of the axioms in Section 2,

• •

enable an effective testing framework allowing to expose consistency violations in production databases.

The SAT encoding we considered is based on the axioms we presented on this paper. We represent each binary relation with a propositional variable and encode the axioms using clauses to create a 3-SAT formula, which is passed to a SAT solver.

For each ordered pair of transactions ${t}_{1}$, ${t}_{2}$ we add two propositional variables representing {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+} and {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}, respectively. Then we generate clauses corresponding to:

• •

Singleton clauses defining the relation {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} (extracted from the input history),

• •

{\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} implies {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{co}}.

• •

co being a total order.

• •

The axioms corresponding to the considered consistency model.

This is an optimization that does not encode {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}} and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} separately, which is sound because of the shape of our axioms (and because these relations are fixed apriori).

As for the implementation of our algorithms, we used standard programming optimizations, e.g., efficient data structures, to avoid unnecessary runtime and memory usage. Few examples include:

• •

using efficient hashsets for searching in a set,

• •

grouping transactions which access the same variable (because our algorithms usually iterate over transactions accessing the same variable).

• •

reducing PCSI to SER on-the-fly while traversing the history.

We focus on three of the criteria introduced in Section 2: 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 on-the-fly to serializability, and causal consistency which is polynomial-time in general 121212Our implementation is publicly available. URL omitted to maintain anonymity.. As benchmark, we consider histories extracted from three distributed databases: CockroachDB (coc, [n. d.]a), Galera (gal, [n. d.]a), and AntidoteDB (ant, [n. d.]a). Following the approach in Jepsen (jep, [n. d.]a), histories are generated with random clients. For the experiments described hereafter, the randomization process is parametrized by: (1) the number of sessions (#sess), (2) the number of transactions per session (#trs), (3) the number of operations per transaction (#ops), and (4) an upper bound on the number of used variables (#vars) 131313We ensure that every value is written at most once.. 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 first experiment, we investigated the efficiency of our serializability checking algorithm (Section 4.1) and we compared its performance with a direct SAT encoding of the serializability definition in Section 2 (we used MiniSAT (Eén and Sörensson, 2003) to solve the SAT queries). We used histories extracted from CockroachDB which claims to implement serializability, acknowledging however the possibility of anomalies (coc, [n. d.]b). The sessions of a history are uniformly distributed among 3 nodes of a single cluster. To evaluate scalability, we fix a reference set of parameter values: #sess=6, #trs=30, #ops=20, and #vars = 60 $\times$ #sess, and vary only one parameter at a time. For instance, the number of sessions varies from 3 to 15 in increments of 3. We consider 100 histories for each combination of parameter values. The experimental data is reported in Figure 14. Our algorithm scales well even when increasing the number of sessions, which is not guaranteed by its worst-case complexity (in general, this is exponential in the number of sessions). Also, our algorithm is at least two orders of magnitude more efficient than the SAT encoding. We have fixed a 10 minutes timeout, a limit of 10GB of memory, and a limit of 10GB on the files containing the formulas to be passed to the SAT solver. The blue dots represent resource exhausted instances. The SAT encoding reaches the file limit for 148 out of 200 histories with at least 12 sessions (Figure 14(a)) and for 50 out of 100 histories with 60 transactions per session (Figure 14(b)), the other parameters being fixed as explained above.

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 different transactions while increasing the latter has the opposite effect. The second and third column of Table 2 give a more precise account of the kind of violations we found by identifying for each criterion X, the number of histories which violate X but no other criterion weaker than X, e.g., there is only one violation to SI which satisfies PC.

The second experiment measures the scalability of the SI checking algorithm obtained by applying the reduction to SER described in Section 4.3 followed by the SER checking algorithm in Section 4.1, and its performance compared to a SAT encoding of SI. 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 14(a) and a number of histories extracted from Galera141414In order to increase the frequency of valid histories, all sessions are executed on a single node. whose documentation contains contradicting claims about whether it implements snapshot isolation (gal, [n. d.]b, [n. d.]c). We use 100 histories per combination of parameter values as in the previous experiment. The results are reported in Figure 15(a) and Figure 15(b). We observe the same behavior as in the case of SER. In particular, the SAT encoding reaches the file limit for 150 out of 200 histories with at least 12 sessions in the case of the CockroachDB histories, and for 162 out of 300 histories with at least 9 sessions in the case of the Galera histories. The last two columns in Table 2 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 3 when increasing the number of sessions, on histories extracted from AntidoteDB, which claims to implement causal consistency (ant, [n. d.]b). The results are reported in Figure 15(c). In this case, the SAT encoding reaches the file limit for 150 out of 300 histories with at least 9 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 3 sessions, 14 transactions per session, 14 operations per transaction, and 5 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}$ which reads $x_{1}$ from ${t}_{1}$ and $x_{2}$ from ${t}_{2}$ (${t}_{1}$ and ${t}_{2}$ are from different sessions while ${t}_{3}$ is an {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} successor of ${t}_{1}$ in the same session). These violations are novel and they were confirmed by the developers of AntidoteDB.

The refinement of the algorithms above based on communication graphs, described in Section 5, did not have a significant 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.

7. Related Work

Cerone et al. (2015) give the first formalization of the criteria we consider in this paper, using the specification methodology of Burckhardt et al. (2014). This formalization uses two auxiliary relations, a visibility relation which represents the fact that a transaction “observes” the effects 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 defined 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. Moreover, Cerone et al. (2015) do not investigate algorithmic issues as in our paper.

Papadimitriou (1979) showed that checking serializability of an execution is NP-complete. Moreover, it identifies a stronger criterion called conflict serializability which is polynomial time checkable. Conflict serializability assumes that histories are given as sequences of operations and requires that the commit order be consistent with a conflict-order between transactions defined based on this sequence (roughly, a transaction ${t}_{1}$ is before a transaction ${t}_{2}$ in the conflict 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 different nodes in a network is impossible.

Bouajjani et al. (2017) 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 Bouajjani et al. (2017). 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. Gibbons and Korach (1997) 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. Emmi and Enea (2018) extended the result concerning linearizability to a series of abstract data types called collections, that includes stacks, queues, key-value maps, etc. sequential consistency is g serializability

The notion of communication graph is inspired by the work of Chalupa et al. (2018) which investigates partial-order reduction (POR) techniques for multi-threaded programs. In general, the goal of partial-order reduction (Flanagan and Godefroid, 2005) is to avoid exploring executions which are equivalent w.r.t. some suitable notion of equivalence, e.g., Mazurkiewicz trace equivalence (Mazurkiewicz, 1986). They use the acyclicity of communication graphs to define a class of programs for which their POR technique is optimal. The algorithmic issues they explore are different than ours and they don’t investigate biconnected components of this graph as in our results.

8. Conclusions

Our results provide an effective means of checking the correctness of transactional databases with respect to a wide range of consistency criteria, in an efficient way. We devise a new specification framework for these criteria, which besides enabling efficient verification algorithms, provide a novel understanding of the differences between them in terms of set of transactions that must be committed before a transaction which is read during the execution. These algorithms are shown to be scalable and orders of magnitude more efficient than standard SAT encodings of these criteria (as defined in our framework). While the algorithms are quite simple to understand and implement, the proof of their correctness is non-trivial and benefits heavily from the new specification framework. One important venue for future work is identifying root causes for a given violation. The fact that we are able to deal with a wide range of criteria is already helpful in identifying the weakest criterion that is violated in a given execution. Then, in the case of RC, RA, and CC, where inconsistencies correspond to cycles in the commit order, the root cause could be attributed to a minimal cycle in this relation. We did this in our communication with the Antidote developers to simplify the violation we found which contained 42 transactions. In the case of PC, SI, and SER, it could be possible to implement a search procedure similar to CDCL in SAT solvers, in order to compute the root-cause as a SAT solver would compute an unsatisfiability core.

Appendix A Proofs of Section 2

Lemma A.1.

Let {h}={\left\langle{T,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}}\right\rangle} be a history. If {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} satisfies $\mathsf{Read\ Atomic}$, then for every transaction ${t}$ and two reads $\textsf{read}_{{i}_{1}}({{x}},{{v}_{1}}),\textsf{read}_{{i}_{2}}({{x}},{{v}_{2}})\in\mathsf{reads}({{t}})$, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}^{-1}(\textsf{read}_{{i}_{1}}({{x}},{{v}_{1}}))={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}^{-1}(\textsf{read}_{{i}_{2}}({{x}},{{v}_{2}})) and ${v}_{1}={v}_{2}$.

Proof.

Let {\left\langle{{t}_{1},\textsf{read}_{{i}_{1}}({{x}},{{v}_{1}})}\right\rangle},{\left\langle{{t}_{2},\textsf{read}_{{i}_{2}}({{x}},{{v}_{2}})}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}. Then ${t}_{1},{t}_{2}$ write to ${x}$. Let us assume by contradiction, that ${t}_{1}\neq{t}_{2}$. By Read Atomic, {\left\langle{{t}_{2},{t}_{1}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} because {\left\langle{{t}_{1},\textsf{read}_{{i}_{1}}({{x}},{{v}_{1}})}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} and ${t}_{2}$ writes to ${x}$. Similarly, we can also show that {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. This contradicts the fact that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{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}$. ∎

Lemma A.2.

The following entailments hold:

[TABLE]

Proof.

We will show the contrapositive of each implication:

• •

If {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} does not satisfy Read Committed, then

[TABLE]

Let ${t}_{3}$ the transaction containing $\alpha$ and $\beta$. We have that {\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}. But then we have ${t}_{1},{t}_{2},{t}_{3}$ such that {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} and {\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}} and ${{t}_{2}}\ \mathsf{writes}\ {{x}}$. So by Read Atomic, {\left\langle{{t}_{2},{t}_{1}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. This contradicts the fact that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is a strict total order. Therefore, {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} does not satisfy Read Atomic.

• •

If {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} does not satisfy Read Atomic, then

[TABLE]

Then {\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+}. Then, by Causal, we have {\left\langle{{t}_{2},{t}_{1}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, which contradicts the fact that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is a strict total order. Therefore, {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} does not satisfy Causal.

• •

If {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} does not satisfy Causal, then

[TABLE]

But, ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+}=({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{*}\mathop{;}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*}\mathop{;}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}). Therefore, {\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*}\mathop{;}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}). Then, by Prefix, we have {\left\langle{{t}_{2},{t}_{1}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, which contradicts the fact that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is a strict total order. Therefore, {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} does not satisfy Prefix.

• •

If {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} does not satisfy Prefix or Conflict, then

[TABLE]

and

• –

{\left\langle{{t}_{4},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}\land{{t}_{3}}\ \mathsf{writes}\ {{y}}\ \land{{t}_{3}}\ \mathsf{writes}\ {{y}} if it violates Conflict.

• –

{\left\langle{{t}_{4},{t}_{3}}\right\rangle}\in({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}) if it violates Prefix.

In both cases, we have that {\left\langle{{t}_{4},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. Because {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is transitive, {\left\langle{{t}_{2},{t}_{4}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*} and {\left\langle{{t}_{4},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} imply that {\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. Then by Serializability, we have {\left\langle{{t}_{2},{t}_{1}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, which contradicts the fact that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is a strict total order. Therefore, {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\right\rangle} does not satisfy Serializability.

∎

Appendix B Proofs of Section 3

Theorem B.1.

The problem of checking whether a history satisfies Read Committed, Read Atomic, or Causal consistency is polynomial time.

Proof.

We first consider the case of Read Committed. Algorithm 3 finds all the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} relations that are implied by the $\mathsf{ReadCommitted}$ axiom (fig. 2(a)) i.e., for all ${t}_{1},{t}_{2}$ and for all $\alpha,\beta$ if we have, {\left\langle{{t}_{1},\alpha}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} and {\left\langle{{t}_{2},\beta}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}} and {\left\langle{\beta,\alpha}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{po}} and ${{t}_{2}}\ \mathsf{writes}\ {{x}}$(from figure 2(a)), then we add {\left\langle{{t}_{2},{t}_{1}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. Quantification can be done in cubic iteration over the transactions for each variable. Now, we claim ${h}$ is Read Committed if and only if {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, the union of these found relations is acyclic.

First we prove that if {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is acyclic, then ${h}$ satisfies Read Committed. {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is acyclic, hence consider a topological order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. If {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}}\right\rangle} does not satisfies Read Committed, there exists ${t}_{1},{t}_{2}$ and $\alpha,\beta$ such that, {\left\langle{{t}_{1},\alpha}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} and {\left\langle{{t}_{2},\beta}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}} and {\left\langle{\alpha,\beta}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{po}} and ${{t}_{2}}\ \mathsf{writes}\ {{x}}$ and {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}. But with the same ${t}_{1},{t}_{2},\alpha,\beta$ and variable ${x}$, we must have added ${\left\langle{{t}_{2},{t}_{1}}\right\rangle}$ in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} which implies any topological order of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} can not have ${\left\langle{{t}_{1},{t}_{2}}\right\rangle}$ which contradicts that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} contains ${\left\langle{{t}_{1},{t}_{2}}\right\rangle}$.

Now we prove, if {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is not acyclic, then ${h}$ does not satisfie Read Committed. If the history is Read Committed, there must be a commit order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} for ${h}$, for which {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}}\right\rangle} satisfies Read Committed. {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} must be acyclic. Now, take any cycle in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, {t}_{1}\xrightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}{t}_{2}\xrightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}\cdots\xrightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}{t}_{k}\xrightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}}{t}_{1}. Now along these, if for all $i,j$ {t}_{i}\xrightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}}{t}_{j} then, it becomes a cycle in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}. Therefore, there must be atleast one pair, where {\left\langle{{t}_{i},{t}_{j}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, but {\left\langle{{t}_{i},{t}_{j}}\right\rangle}\not\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} or {\left\langle{{t}_{j},{t}_{i}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} since {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} is total.

But {\left\langle{{t}_{i},{t}_{j}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} must have been added because there exists $\alpha,\beta$ such that {\left\langle{{t}_{i},\beta}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}, {\left\langle{\beta,\alpha}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{po}} and {\left\langle{{t}_{j},\alpha}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} and ${{t}_{i}}\ \mathsf{writes}\ {{x}}$. But {\left\langle{{t}_{j},{t}_{i}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}, so {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} violates Read Commmitted for ${t}_{i},{t}_{j},\alpha,\beta$. Therefore, if {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} has a cyclic, ${h}$ does not satisfy Read Committed.

The case of Read Atomic and Causal Consistency is similar. If the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} at the end of the algorithm is acyclic, then if a topological order extending it does not satisfy resp. consistency model, then it contains ${\left\langle{{t}_{1},{t}_{2}}\right\rangle}$ with the quantified transactions, variables and operations for resp. consistency model. But, then for same quantified transactions, variables and operations, we must have added {\left\langle{{t}_{2},{t}_{1}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} in the algorithm. It contradicts the topological order contains ${\left\langle{{t}_{1},{t}_{2}}\right\rangle}$. For the other direction, if the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} at the end of the algorithm has cycle, we show there exists {\left\langle{{t}_{i},{t}_{j}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, like the case of Read Committed, yet it is not in a commit order satisfying the resp. consistency models. Then the commit order must have ${\left\langle{{t}_{j},{t}_{i}}\right\rangle}$ which violates the resp. consistency models for the exact same quantified transactions, variables and operations for which ${\left\langle{{t}_{i},{t}_{j}}\right\rangle}$ was added in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} at first. ∎

Appendix C Proofs of Section 4.2

Lemma C.1.

The histories ${h}$ and ${h}_{R|W}$ have the same width.

Proof.

We show that if ${h}$ is of width $k$, then the session order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}^{\prime} of ${h}_{R|W}$ cannot contain an antichain of size $k+1$. Let $\{X^{1}_{{t}_{1}},X^{2}_{{t}_{2}},\ldots X^{k}_{{t}_{k}},X^{k+1}_{{t}_{k+1}}\}$ with $X^{i}\in\{R,W\}$, for all $1\leq i\leq k+1$, be a set of $k+1$ transactions in ${h}_{R|W}$. Then,

• •

if ${t}_{i}={t}_{j}={t}$ for some $i\neq j$, then $X^{i}_{{t}_{i}}=R_{{t}}$ and $X^{j}_{{t}_{j}}=W_{t}$ or vice-versa. Since {\left\langle{R_{{t}},W_{{t}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}^{\prime}, this set cannot be an antichain of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}^{\prime}.

• •

otherwise, by hypothesis, the set $\{{t}_{1},{t}_{2},\ldots,{t}_{k},{t}_{k+1}\}$ is not an antichain of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}. Thus, there exists $i,j$ such that {\left\langle{{t}_{i},{t}_{j}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}. By the definition of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}^{\prime}, {\left\langle{X^{i}_{{t}_{i}},X^{j}_{{t}_{j}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}^{\prime}, which implies that this set is not an antichain of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}^{\prime}.

∎

Appendix D Proofs of Section 4.3

Theorem D.1.

A history ${h}$ satisfies snapshot isolation iff ${h}_{R|W}^{c}$ is serializable.

Proof.

For the “only-if” direction, we define partial commit orders {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{1}^{\prime} and \mathsf{RW}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{1}^{\prime}) as in the case of prefix consistency. Along with them, we define a partial commit order \mathsf{WR}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{1}^{\prime})

[TABLE]

which intuitively, enforces that the read part $R_{{t}_{2}}$ of a transaction ${t}_{2}$ observes the effects of the write part $W_{{t}_{1}}$ of a transaction ${t}_{1}$ when ${t}_{1}$ and ${t}_{2}$ write on a common variable and the commit order in ${h}$ orders ${t}_{1}$ before ${t}_{2}$ (which implies that the corresponding write transactions are ordered in the same way in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}). We define {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{2}^{\prime}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{1}^{\prime}\cup\mathsf{RW}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{1}^{\prime})\cup\mathsf{WR}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}).

The characterization of minimal cycles of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{1}^{\prime} and ultimately, the fact that it is acyclic can be proved as in Lemma 4.5. The proof that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{2}^{\prime} is acyclic goes as follows. As for PC, since {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1} is acyclic, a cycle in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2}, and in particular a minimal one, must necessarily contain a dependency from \mathsf{RW}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}) or \mathsf{WR}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}). Note that a minimal cycle cannot contain two dependencies in either \mathsf{RW}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}) or \mathsf{WR}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}) since this would imply that it contains two non-consecutive write transactions. Differently from the previous case, the cycle in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{2}^{\prime} here can also contains the dependencies in \mathsf{WR}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}) which are from write transactions to read transactions. The case of minimal cycles in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{2} that contain only a dependency from \mathsf{RW}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}), and no dependencies from \mathsf{WR}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}), can be dealt with as in the case of PC.

Consider a minimal cycle of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}_{2}^{\prime} that contains a dependency ${\left\langle{W_{{t}_{4}},R_{{t}_{3}}}\right\rangle}$ in \mathsf{WR}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}), which implies that $W_{{t}_{4}},W_{{t}_{3}}$ must write on some common variable $y$. Because the minimal cycle contains at most two write transactions and one read transaction, it must also contain a dependency from read transactions to write transactions. Note that such a dependency can come only from \mathsf{RW}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}). The red edges in Figure 16(a) show such a cycle. By the definition of ${h}_{R|W}^{c}$, we have that $W_{{t}_{4}}$ and $R_{{t}_{3}}$ write on a variable ${x}_{3,4}$ and {\left\langle{R_{{t}_{3}},W_{{t}_{3}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}_{3,4}}}^{\prime}. Since {\left\langle{R_{{t}_{3}},W_{{t}_{2}}}\right\rangle}\in\mathsf{RW}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}), we have that there exists a write transaction $W_{{t}_{1}}$ s.t. {\left\langle{W_{{t}_{1}},R_{{t}_{3}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}^{\prime}[{x}], for some ${x}$, and {\left\langle{W_{{t}_{1}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}_{1}. The relations between these transactions of ${h}_{R|W}^{c}$ imply that the corresponding transactions of ${h}$ are related as shown in Figure 16(b), which implies a violation of $\mathsf{Conflict}$, a contradiction of the hypothesis.

For the “if” direction, let {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} be a commit (total) order on transactions of ${h}_{R|W}^{c}$ which satisfies the serializability axiom. Let {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} be a commit order on transactions of ${h}$ defined by {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}=\{{\left\langle{{t}_{1},{t}_{2}}\right\rangle}|{\left\langle{W_{{t}_{1}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}\} ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is clearly a total order). Showing that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is an extension of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} and that it doesn’t expose a $\mathsf{Prefix}$ violation can be done as for prefix consistency. Now, assume by contradiction that there exists a $\mathsf{Conflict}$ violation between ${t}_{1}$, ${t}_{2}$, ${t}_{3}$, ${t}_{4}$ (shown in Figure 17(a)). Then, the corresponding transactions $W_{{t}_{1}},W_{{t}_{2}},W_{{t}_{4}},R_{{t}_{3}},W_{{t}_{3}}$ in ${h}_{R|W}^{c}$, shown in Figure 17(b), would be related as follows: (1) since {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} and {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, we have that {\left\langle{W_{{t}_{1}},R_{{t}_{3}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}^{\prime} and {\left\langle{W_{{t}_{1}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}, (2) since {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} satisfies $\mathsf{Serializability}$, then {\left\langle{R_{{t}_{3}},W_{{t}_{2}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}, (3) {\left\langle{{t}_{2},{t}_{4}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*} implies {\left\langle{W_{{t}_{2}},W_{{t}_{4}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime*}, (4) {\left\langle{{t}_{4},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} and ${t}_{4},{t}_{3}$ write on a common variable $y$ implies that {\left\langle{W_{{t}_{4}},W_{{t}_{3}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}, {\left\langle{R_{{t}_{3}},W_{{t}_{3}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}^{\prime}[{x}_{3,4}], and $W_{{t}_{4}}$ writes the variable ${x}_{3,4}$, which by the serializability axiom, implies {\left\langle{W_{{t}_{4}},R_{{t}_{3}}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime}. Therefore, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{\prime} contains a cycle, a contradiction to the hypthesis. ∎

Appendix E Equivalence between our definitions and the formalization in (Cerone

et al., 2015)

Cerone et al. (2015) define the criteria RA, CC, PC, SI, and SER using a notion of history that contains only the session order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}. Such a history satisfies one of these criteria in their formalization if there exists a visibility relation vis between transactions, and a commit order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} extending the visibility relation that satisfy certain axioms.

The axioms used by Cerone et al. (2015) are given in Table 3.

Int is an axiom which enforces that if there is a read operation $O$ on variable ${x}$ in a transaction and there is a read or write operation on ${x}$ before $O$ i.e., $\left\{o^{\prime}\in\textsf{po}^{-1}(o)\mid o^{\prime}=\_(x,\_)\right\}\neq\emptyset$, then the latest operation on ${x}$ before $O$ must read or write the value read by $O$ i.e., $max_{\textsf{po}}\left(\left\{o^{\prime}\in\textsf{po}^{-1}(o)\mid o^{\prime}=\_(x,\_)\right\}\right)=\_(x,n)$.

Ext is an axiom which enforces that if a transaction ${t}$ has a operation $O$ which reads a variable ${x}$ and which is not preceded by a write on ${x}$, denoted by ${t}\models\texttt{read}(x,n)$, then either:

• •

it read the initial value 0, and there is no transaction writing on ${x}$ visible to ${t}$, i.e., {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{vis}}^{-1}({t})\cap\textsf{Write}_{x}=\emptyset, or

• •

it read from a write of another transaction ${t}^{\prime}$ which writes to variable ${x}$ and ${t}^{\prime}$ is the last one in the commit order in the visibility set of ${t}$, i.e., {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textsf{vis}}^{-1}({t}), that writes on ${x}$.

Since, the writes in our history have unique values, this is equivalent to, for all ${t}_{1},{t}_{3}$ if ${t}_{1}\models write({x},n)$ and ${t}_{3}\models read({x},n)$, then for any {t}_{2}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}^{-1}({t}_{3}) where ${t}_{2}\neq{t}_{1}$ and ${t}_{2}\models write({x},\_)$, ${t}_{2}$ can not be after ${t}_{1}$ in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} order (i.e., {\left\langle{{t}_{2},{t}_{1}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} since {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is total), because ${t}_{1}$ must be the maximal among the transactions that wrote ${x}$. We illustrated the axiom in Figure 18(a), which is very similar to our definition in Figure 2.

The definitions for Session, TransVis, Prefix, TotalVis are straightforward. NoConflict enforces {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} to totally order the transactions those write on same variable.

We will show in our axioms definition figures, the path between ${t}_{2}$ and ${t}_{3}$ is essentially a {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} relation in {h}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}}.

The definitions of RA, CC, PC, SI, and SER in Cerone et al. (2015) are given in Table 4. Next, we show the equivalence between these definitions and our definitions in Figure 2 on histories where every value is written at most once. For a history {h}={\left\langle{T,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}}\right\rangle} as in our framework, {h}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}}={\left\langle{T,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}}\right\rangle}.

• •

We show that Int $\land$ Ext $\land$ Session $\equiv$ Read Atomic

• –

For a history {h}={\left\langle{T,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}}\right\rangle}, if {h}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}} satisfies Int $\land$ Ext $\land$ Session for some {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, we show that ${h}$ satisfies Read Atomic for the same {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. If it does not, then, there exists ${t}_{1},{t}_{2},{t}_{3}$ such that {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}, ${t}_{2}$ writes on ${x}$, {\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} and {\left\langle{{t}_{3},{t}_{1}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. But, since {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} satisfies Int $\land$ Ext $\land$ Session, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}\supseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}. Hence, {\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}. Therefore, {\left\langle{{h},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}}\right\rangle} violates the definition in figure 18(a), which contradicts the fact {\left\langle{{h}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}}\right\rangle} satisfies Int $\land$ Ext.

• –

For the other direction, we have a commit order {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} for ${h}$ which satisfies Read Atomic. We show that there exists a visibility relation {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} which together with the same {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} and {h}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}} satisfies Int $\land$ Ext $\land$ Session. Let {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}=\{{\left\langle{{t}_{1},{t}_{2}}\right\rangle}|{\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\}.

First of all, by definition, the internal reads in our transactions are consistent to the last read or write before them. Only thing is left, to show that the first reads of a variable ${x}$ before a write to ${x}$ inside a variable is also reading from a unique transaction.

• *

If $o_{1},o_{1}$ are two reads on ${x}$ and ${\left\langle{{t}_{1},o_{1}}\right\rangle}$, ${\left\langle{{t}_{2},o_{2}}\right\rangle}$ $\in$ {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}, then by Read Atomic axiom, we have ${\left\langle{{t}_{1},{t}_{2}}\right\rangle}$, ${\left\langle{{t}_{2},{t}_{1}}\right\rangle}$ \in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. Therefore, the reads to ${x}$ in a transaction before the first write to ${x}$ are from same transaction.

• *

We can not have a violation of Int and Ext because we defined {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} as \{{\left\langle{{t}_{1},{t}_{2}}\right\rangle}|{\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\}. So any violation of Ext will be a violation of Read Atomic

• *

{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} satisfy Session, since {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}

• •

We show that Int $\land$ Ext $\land$ Session $\land$ TransVis $\equiv$ Causal Consistency.

• –

If ${h}$ satisfies Causal Consistency, there exists a {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} for ${h}$. We define {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}=({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+}. {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}\supseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}, therefore as previous case, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} satisfies Int $\land$ Ext $\land$ Session and by construction of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} it is a transitive closure therefore it also satisfies TransVis. If there is any Int and Ext violation then there exist ${t}_{1},{t}_{2},{t}_{3}$ such that {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}, ${t}_{2}$ writes on ${x}$, {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} and {\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}=({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+} which is a violation of Casual Consistency. This is a contradiction.

• –

If there exists a {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} for {h}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}} which satisfies Int $\land$ Ext $\land$ Session $\land$ TransVis, we show, the same {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} satisfies Causal Consistency. If it does not, we have ${t}_{1},{t}_{2},{t}_{3}$ such that {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} ${t}_{2}$ writes on ${x}$ and {\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+} and {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. But, by Int $\land$ Ext, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} and by Session {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} and by TransVis we have {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}^{+}\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} which implies ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})^{+}\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}. There fore {\left\langle{{t}_{2},tr_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}. So ${t}_{1},{t}_{2},{t}_{3}$ violates Int and Ext axiom for {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, which is a contradiction.

• •

We show that Int $\land$ Ext $\land$ Session $\land$ Prefix $\equiv$ Prefix consistency.

• –

If ${h}$ satisfies Prefix consistency, there exists a {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} for ${h}$. We define {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*}\mathop{;}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}). {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}\supseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}} therefore as previous case, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} satisfies Int $\land$ Ext $\land$ Session. Assume {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}\mathop{;}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}. Then there exists ${t}_{3}$ such that {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} and {\left\langle{{t}_{3},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*}\mathop{;}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}). Therefore, there exists ${t}_{4}$ such that either ${t}_{3}={t}_{4}$ or {\left\langle{{t}_{3},{t}_{4}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} and {\left\langle{{t}_{4},{t}_{2}}\right\rangle}\in({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}). Since, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is a total order, then {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} and either ${t}_{3}={t}_{4}$ or ${\left\langle{{t}_{3},{t}_{4}}\right\rangle}$ imply {\left\langle{{t}_{1},{t}_{4}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. We have {\left\langle{{t}_{4},{t}_{2}}\right\rangle}\in({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}). Therefore, {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}\mathop{;}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}. Therefore, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}\mathop{;}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} which is Prefix axiom.

• –

If {h}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}} satisfies Int $\land$ Ext $\land$ Session $\land$ Prefix, then there exists a {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} for which the axioms satisfy. The same {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} will satisfy Read Atomic axiom for ${h}$. So if we have a violation in Prefix consistency, then there exist ${t}_{1},{t}_{2},{t}_{3}$ such that {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}, ${t}_{2}$ writes on ${x}$ and {\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*}\mathop{;}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}) and {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. If {\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}), then it is violation in Read Atomic, therefore, {\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{+}\mathop{;}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}\mathop{;}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}) because {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is transitive. But by Int $\land$ Ext $\land$ Session, ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}, therefore {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}\mathop{;}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}})\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}\mathop{;}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}. Then ${t}_{1},{t}_{2},{t}_{3}$ violates Ext.

• •

We have to show, Int $\land$ Ext $\land$ Session $\land$ Prefix $\land$ NoConflict $\equiv$ Snapshot isolation.

• –

If ${h}$ satisfies Snapshot isolation, it also satisfies Prefix consistency. We define {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}=({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*}\mathop{;}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}}\cup{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}))\cup({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*}\mathop{;}\{{\left\langle{{t}_{1},{t}_{2}}\right\rangle}|{\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}},\exists{x}.{t}_{1},{t}_{2}\text{write on }{x}\}. Clearly, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} contains the the relations for Int $\land$ Ext $\land$ Session $\land$ Prefix proof, therefore, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} satisfies them. Also, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} satisfies NoConflict by definition since {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is a total order. Any violation in Int and Ext will imply there is a ${t}_{1},{t}_{2},{t}_{3}$ such that {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}}, ${t}_{2}$ writes on ${x}$ and {\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} and {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. But by definition of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} we will have violations in either Prefix or Conflict axioms of Snapshot isolation model.

• –

If {h}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}} satisfies Int $\land$ Ext $\land$ Session $\land$ Prefix $\land$ NoConflict, then there exists a {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} for which the axioms satisfy. The same {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} will satisfy Prefix Consistency axiom for ${h}$. So if we have a violation in Snapshot isolation, it is a violation of Conflict axiom, i.e., there exist ${t}_{1},{t}_{2},{t}_{3}$ such that {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} ${t}_{2}$ writes on ${x}$ and {\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}^{*}\mathop{;}\{{\left\langle{{t}_{1},{t}_{2}}\right\rangle}|\exists{x},{t}_{1},{t}_{2}\text{write on }{x}\} and {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. But \{{\left\langle{{t}_{1},{t}_{2}}\right\rangle}|\exists{x},{t}_{1},{t}_{2}\text{write on }{x}\}\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} by NoConflict and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}\mathop{;}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}\subseteq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} by Prefix. Hence, {\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}. Then ${t}_{1},{t}_{2},{t}_{3}$ violates Ext.

• •

We show that Int $\land$ Ext $\land$ TotalVis $\equiv$ Serialization.

• –

If ${h}$ satisfies Serialization, there exists {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} for ${h}$ that satisfy Serialization. We define {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. Clearly it satisfies TotalVis because {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} is total. We have any violation in Int and Ext, that will imply we have ${t}_{1},{t}_{2},{t}_{3}$ such that ${t}_{1},{t}_{2},{t}_{3}$ such that {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}} ${t}_{2}$ writes on ${x}$ and {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. But since {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, ${t}_{1},{t}_{2},{t}_{3}$ will violate Serialization axiom, which is a contradiction.

• –

If {h}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}} satisfies Int $\land$ Ext $\land$ TotalVis, then there exists a {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} for which the axioms satisfy. If for same {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}, we have a violation of Serialization, then there exist ${t}_{1},{t}_{2},{t}_{3}$ such that {\left\langle{{t}_{1},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{wr}_{{x}}} ${t}_{2}$ writes on ${x}$ and {\left\langle{{t}_{2},{t}_{3}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}} and {\left\langle{{t}_{1},{t}_{2}}\right\rangle}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}. But {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{co}}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{vis}}, so then we have a Int and Ext violation in {h}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{so}}} for ${t}_{1},{t}_{2},{t}_{3}$