Checking Robustness Against Snapshot Isolation

TL;DR

This paper presents a method to verify if programs maintain correctness under snapshot isolation by reducing the problem to a state reachability analysis, enabling reuse of existing verification techniques.

Contribution

It introduces a polynomial-time reduction from robustness verification against snapshot isolation to state reachability, facilitating the application of classic verification methods.

Findings

Verification problem is polynomial-time reducible to state reachability.

Reduction enables reuse of classic verification techniques.

Proof technique based on Lipton's reduction theory for robustness.

Abstract

Transactional access to databases is an important abstraction allowing programmers to consider blocks of actions (transactions) as executing in isolation. The strongest consistency model is {\em serializability}, which ensures the atomicity abstraction of transactions executing over a sequentially consistent memory. Since ensuring serializability carries a significant penalty on availability, modern databases provide weaker consistency models, one of the most prominent being \emph{snapshot isolation}. In general, the correctness of a program relying on serializable transactions may be broken when using weaker models. However, certain programs may also be insensitive to consistency relaxations, i.e., all their properties holding under serializability are preserved even when they are executed over a weak consistent database and without additional synchronization. In this paper, we address the issue of verifying if a given program is {\em robust against snapshot isolation}, i.e., all its behaviors are serializable even if it is executed over a database ensuring snapshot isolation. We show that this verification problem is polynomial time reducible to a state reachability problem in transactional programs over a sequentially consistent shared memory. This reduction opens the door to the reuse of the classic verification technology for reasoning about weakly-consistent programs. In particular, we show that it can be used to derive a proof technique based on Lipton's reduction theory that allows to prove programs robust.

Tables

Table 1. Table 1 : An overview of the analysis results. CDG stands for commutativity dependency graph. The columns PO and PT show the number of proof obligations and proof time in second, respectively. T stands for trivial when the application has only read-only transactions.

Application	#Transactions	Robustness	Reachability Analysis		CDG Analysis
			PO	PT	PO	PT
Auction	4	✓	70	0.3	20	0.5
Courseware	5	✗	59	0.37	na	na
FusionTicket	4	✓	72	0.3	34	0.5
SmallBank	5	✗	48	0.28	na	na
TPC-C	5	✓	54	0.7	82	3.7
Cassieq-Core	8	✓	173	0.55	104	2.9
Currency-Exchange	6	✓	88	0.35	26	3.5
PlayList	14	✓	99	4.63	236	7.3
RoomStore	5	✓	85	0.3	22	0.5
Shopping-Cart	4	✓	58	0.25	T	T

Equations

$$\text{begin}(p_1,t_1)\text{ld}(p_1,t_1,y,0)\text{isu}(p_1,t_1,x,1)$$

$$\text{begin}(p_2,t_2)\text{ld}(p_2,t_2,x,0)\text{isu}(p_2,t_2,y,1)\text{com}(p_2,t_2)$$

$$\text{begin}(p_1,t_1)\text{ld}(p_1,t_1,y,0)\text{st}(p_1,t_1,r_x,1)$$

$$\text{begin}(p_2,t_2)\text{ld}(p_2,t_2,x,0)\text{isu}(p_2,t_2,y,1)\text{com}(p_2,t_2)$$

$$\text{begin}(p_1,t_1)\text{st}(p_1,t_1,r_x,1)$$

$$\text{begin}(p_2,t_2)\text{ld}(p_2,t_2,x,0)\text{isu}(p_2,t_2,y,1)\text{com}(p_2,t_2)$$

$$\mathbb{E}\text{v}=\{\text{begin}(p,t),\text{ld}(p,t,x,v),\text{isu}(p,t,x,v),\text{com}(p,t):p\in \mathbb{P},t\in {\mathbb{T}}^2,x\in \mathbb{V},v\in \mathbb{D}\}$$

$$[[{\text{l}}_1\text{lit}\ast :r:=x\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;]{]}_{\text{A}}=$$

$${\text{l}}_1\text{lit}\ast :\text{lit}\ast assume{a}_{{\text{tr}}_{\text{A}}}=\perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x1}\text{lit}\ast ;$$

$${\text{l}}_{x1}\text{lit}\ast :r:=x\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;$$

$${\text{l}}_1\text{lit}\ast :\text{lit}\ast assume{a}_{{\text{tr}}_{\text{A}}}\ne \perp \wedge p.a\ne \perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x2}\text{lit}\ast ;$$

$${\text{l}}_{x2}\text{lit}\ast :r:=x^{\prime }\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x3}\text{lit}\ast ;$$

$${\text{l}}_{x3}\text{lit}\ast :x.event:=\text{ld}\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x4}\text{lit}\ast ;$$

$${\text{l}}_{x4}\text{lit}\ast :\text{lit}\ast assume\mathsf{HB}=\perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x5}\text{lit}\ast ;$$

$${\text{l}}_{x5}\text{lit}\ast :\mathsf{HB}:=\mathsf{true}\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;$$

$${\text{l}}_{x4}\text{lit}\ast :\text{lit}\ast assume\mathsf{HB}\ne \perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;$$

$$[[{\text{l}}_1\text{lit}\ast :x:=e\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;]{]}_{\text{A}}=$$

$${\text{l}}_1\text{lit}\ast :\text{lit}\ast assume{a}_{{\text{tr}}_{\text{A}}}=\perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x1}\text{lit}\ast ;$$

$${\text{l}}_{x1}\text{lit}\ast :x:=e\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;$$

$${\text{l}}_1\text{lit}\ast :\text{lit}\ast assume{a}_{{\text{tr}}_{\text{A}}}\ne \perp \wedge p.a\ne \perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x2}\text{lit}\ast ;$$

$${\text{l}}_{x2}\text{lit}\ast :x^{\prime }:=e\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x3}\text{lit}\ast ;$$

$${\text{l}}_{x3}\text{lit}\ast :x.even{t}^{\prime }:=1\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;$$

$${\text{l}}_1\text{lit}\ast :\text{lit}\ast assume{a}_{{\text{st}}_{\text{A}}}=x.event=\perp \wedge a_{{\text{tr}}_{\text{A}}}\ne \perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x4}\text{lit}\ast ;$$

$${\text{l}}_{x4}\text{lit}\ast :x^{\prime }:=e\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x5}\text{lit}\ast ;$$

$${\text{l}}_{x5}\text{lit}\ast :a_{{\text{st}}_{\text{A}}}:=‘x‘\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x6}\text{lit}\ast ;$$

$${\text{l}}_{x8}\text{lit}\ast :x.even{t}^{\prime }:=1\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;$$

$$[[{\text{l}}_1\text{lit}\ast :r:=x\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;]{]}_{\text{HbH}}=$$

$${\text{l}}_1\text{lit}\ast :\text{lit}\ast assume\mathsf{HB}=\perp \wedge p.a=\perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x1}\text{lit}\ast ;$$

$${\text{l}}_{x1}\text{lit}\ast :r:=x\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;$$

$${\text{l}}_1\text{lit}\ast :\text{lit}\ast assume\mathsf{HB}\ne \perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x2}\text{lit}\ast ;$$

$${\text{l}}_{x2}\text{lit}\ast :r:=x\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x3}\text{lit}\ast ;$$

$${\text{l}}_{x3}\text{lit}\ast :\text{lit}\ast assumex.eventI=\text{st}\wedge p.hbh=\perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x4}\text{lit}\ast ;$$

$${\text{l}}_{x4}\text{lit}\ast :p.hbh:=\text{true}\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;$$

$${\text{l}}_{x3}\text{lit}\ast :\text{lit}\ast assumex.event=\perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x5}\text{lit}\ast ;$$

$${\text{l}}_{x5}\text{lit}\ast :x.event:=\text{ld}\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;$$

$${\text{l}}_{x3}\text{lit}\ast :\text{lit}\ast assumex.event\ne \perp \vee p.hbh\ne \perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;$$

$$[[{\text{l}}_1\text{lit}\ast :x:=e\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;]{]}_{\text{HbH}}=$$

$${\text{l}}_1\text{lit}\ast :\text{lit}\ast assume\mathsf{HB}=\perp \wedge a_{{\text{tr}}_{\text{A}}}=\perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x1}\text{lit}\ast ;$$

$${\text{l}}_{x1}\text{lit}\ast :x:=e\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;$$

$${\text{l}}_1\text{lit}\ast :\text{lit}\ast assume\mathsf{HB}\ne \perp \wedge p.a=\perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x2}\text{lit}\ast ;$$

$${\text{l}}_{x2}\text{lit}\ast :\text{lit}\ast assumex.even{t}^{\prime }\ne \perp \text{lit}\ast ;\text{lit}\ast assume\mathsf{false}\text{lit}\ast ;$$

$${\text{l}}_{x2}\text{lit}\ast :\text{lit}\ast assumex.even{t}^{\prime }=\perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x3}\text{lit}\ast ;$$

$${\text{l}}_{x3}\text{lit}\ast :x:=e\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x4}\text{lit}\ast ;$$

$${\text{l}}_{x4}\text{lit}\ast :x.event:=\text{st}\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x5}\text{lit}\ast ;$$

$${\text{l}}_{x5}\text{lit}\ast :\text{lit}\ast assumex.eventI\ne \perp \wedge p.hbh=\perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_{x6}\text{lit}\ast ;$$

$${\text{l}}_{x6}\text{lit}\ast :p.hbh:=\text{true}\text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;$$

$${\text{l}}_{x5}\text{lit}\ast :\text{lit}\ast assumex.eventI=\perp \vee p.hbh\ne \perp \text{lit}\ast ;\text{lit}\ast goto{\text{l}}_2\text{lit}\ast ;$$

$$\displaystyle\begin{array}[]{c}\dfrac{\text{$\displaystyle\text{$\displaystyle\mathtt{begin}$}\in{\textsf{inst}}(\textsf{ls}({p}).\textsf{pc})$\quad$\displaystyle\mathsf{img}(\textsf{ls}.\textsf{tstamp})<{t}.{st}$\quad$\displaystyle s=\textsf{ls}({p})[\textsf{log}\mapsto\epsilon,\textsf{store}\mapsto\textsf{Log},\textsf{pc}\mapsto\mathsf{next}(\textsf{pc})]$}}{\text{$\displaystyle(\textsf{ls},\textsf{tstamp},\textsf{Log},\textsf{lk})\xrightarrow{\text{\tiny$\displaystyle\textsf{begin}({p},{t})$}}(\textsf{ls}[{p}\mapsto s],\textsf{tstamp},\textsf{Log},\textsf{lk})$}}\\[16.00003pt] \dfrac{\displaystyle\begin{multlined}\text{$\displaystyle r:=x\in{\textsf{inst}}(\textsf{ls}({p}).\textsf{pc})$\quad$\displaystyle\textsf{ls}({p}).\textsf{store}[x]=v$ \quad$\displaystyle\mathit{rval}=\textsf{ls}({p}).\textsf{rval}[r\mapsto v]$}\\ \text{$\displaystyle s=\textsf{ls}({p})[\textsf{rval}\mapsto\mathit{rval},\textsf{pc}\mapsto\mathsf{next}(\textsf{pc})]$}\end{multlined}\text{$\displaystyle r:=x\in{\textsf{inst}}(\textsf{ls}({p}).\textsf{pc})$\quad$\displaystyle\textsf{ls}({p}).\textsf{store}[x]=v$ \quad$\displaystyle\mathit{rval}=\textsf{ls}({p}).\textsf{rval}[r\mapsto v]$}\\ \text{$\displaystyle s=\textsf{ls}({p})[\textsf{rval}\mapsto\mathit{rval},\textsf{pc}\mapsto\mathsf{next}(\textsf{pc})]$}}{\text{$\displaystyle(\textsf{ls},\textsf{tstamp},\textsf{Log},\textsf{lk})\xrightarrow{\text{\tiny$\displaystyle\textsf{ld}({p},{t},x,v)$}}(\textsf{ls}[{p}\mapsto s],\textsf{tstamp},\textsf{Log},\textsf{lk})$}}\\[22.76219pt] \dfrac{\begin{multlined}\text{$\displaystyle x:=v\in{\textsf{inst}}(\textsf{ls}({p}).\textsf{pc})$\quad$\displaystyle\mathit{log}=\textsf{ls}({p}).\textsf{log}[x\mapsto 1]$\quad$\displaystyle\mathit{store}=\textsf{ls}({p}).\textsf{store}[x\mapsto v]$}\\ \text{$\displaystyle s=\textsf{ls}({p})[\textsf{log}\mapsto\mathit{log},\textsf{store}\mapsto\mathit{store},\textsf{pc}\mapsto\mathsf{next}(\textsf{pc})]$}\end{multlined}\text{$\displaystyle x:=v\in{\textsf{inst}}(\textsf{ls}({p}).\textsf{pc})$\quad$\displaystyle\mathit{log}=\textsf{ls}({p}).\textsf{log}[x\mapsto 1]$\quad$\displaystyle\mathit{store}=\textsf{ls}({p}).\textsf{store}[x\mapsto v]$}\\ \text{$\displaystyle s=\textsf{ls}({p})[\textsf{log}\mapsto\mathit{log},\textsf{store}\mapsto\mathit{store},\textsf{pc}\mapsto\mathsf{next}(\textsf{pc})]$}}{\text{$\displaystyle(\textsf{ls},\textsf{tstamp},\textsf{Log},\textsf{lk})\xrightarrow{\text{\tiny$\displaystyle\textsf{isu}({p},{t},x,v)$}}(\textsf{ls}[{p}\mapsto s],\textsf{tstamp},\textsf{Log},\textsf{lk})$}}\\[22.76219pt] \dfrac{\begin{multlined}\begin{multlined}\text{$\displaystyle\text{$\displaystyle\mathtt{end}$}\in{\textsf{inst}}(\textsf{ls}({p}).\textsf{pc})$\quad$\displaystyle\forall x\in\mathbb{V}.\ \mathit{log}[x]=\bot\lor\textsf{tstamp}(x)<{t}.{st}$ \quad$\displaystyle\mathsf{img}(\textsf{ls}.\textsf{tstamp})<{t}.{ct}$}\\ \text{ $\displaystyle\mathit{Log}=\textsf{Log}[x\mapsto\textsf{store}[x]:x\in\mathbb{V},\mathit{log}[x]\neq\bot]$ }\end{multlined}\text{$\displaystyle\text{$\displaystyle\mathtt{end}$}\in{\textsf{inst}}(\textsf{ls}({p}).\textsf{pc})$\quad$\displaystyle\forall x\in\mathbb{V}.\ \mathit{log}[x]=\bot\lor\textsf{tstamp}(x)<{t}.{st}$ \quad$\displaystyle\mathsf{img}(\textsf{ls}.\textsf{tstamp})<{t}.{ct}$}\\ \text{ $\displaystyle\mathit{Log}=\textsf{Log}[x\mapsto\textsf{store}[x]:x\in\mathbb{V},\mathit{log}[x]\neq\bot]$ }\\ \text{$\displaystyle\mathit{tstamp}=\textsf{tstamp}[x\mapsto{st}.{ct}:x\in\mathbb{V},\mathit{log}[x]\neq\bot]$ \quad$\displaystyle s=\textsf{ls}({p})[\textsf{pc}\mapsto\mathsf{next}(\textsf{pc})]$}\end{multlined}\begin{multlined}\text{$\displaystyle\text{$\displaystyle\mathtt{end}$}\in{\textsf{inst}}(\textsf{ls}({p}).\textsf{pc})$\quad$\displaystyle\forall x\in\mathbb{V}.\ \mathit{log}[x]=\bot\lor\textsf{tstamp}(x)<{t}.{st}$ \quad$\displaystyle\mathsf{img}(\textsf{ls}.\textsf{tstamp})<{t}.{ct}$}\\ \text{ $\displaystyle\mathit{Log}=\textsf{Log}[x\mapsto\textsf{store}[x]:x\in\mathbb{V},\mathit{log}[x]\neq\bot]$ }\end{multlined}\text{$\displaystyle\text{$\displaystyle\mathtt{end}$}\in{\textsf{inst}}(\textsf{ls}({p}).\textsf{pc})$\quad$\displaystyle\forall x\in\mathbb{V}.\ \mathit{log}[x]=\bot\lor\textsf{tstamp}(x)<{t}.{st}$ \quad$\displaystyle\mathsf{img}(\textsf{ls}.\textsf{tstamp})<{t}.{ct}$}\\ \text{ $\displaystyle\mathit{Log}=\textsf{Log}[x\mapsto\textsf{store}[x]:x\in\mathbb{V},\mathit{log}[x]\neq\bot]$ }\\ \text{$\displaystyle\mathit{tstamp}=\textsf{tstamp}[x\mapsto{st}.{ct}:x\in\mathbb{V},\mathit{log}[x]\neq\bot]$ \quad$\displaystyle s=\textsf{ls}({p})[\textsf{pc}\mapsto\mathsf{next}(\textsf{pc})]$}}{\text{$\displaystyle(\textsf{ls},\textsf{tstamp},\textsf{Log},\textsf{lk})\xrightarrow{\text{\tiny$\displaystyle\textsf{com}({p},{t})$}}(\textsf{ls}[p\mapsto s],\textsf{Log}\mapsto\mathit{Log},\textsf{tstamp}\mapsto\mathit{tstamp},\textsf{lk})$}}\end{array}$$

$$\displaystyle\displaystyle\mathbb{E}\textsf{v}=\$$

$$c_i{\to }_{{\mathsf{HB}}^1}{c}_{i+1}\text{ for all }i\in [0,n]$$

Full text

In this paper, we address the issue of verifying if a given program is robust against snapshot isolation, i.e., all its behaviors are serializable even if it is executed over a database ensuring snapshot isolation. We show that this verification problem is polynomial time reducible to a state reachability problem in transactional programs over a sequentially consistent shared memory. This reduction opens the door to the reuse of the classic verification technology for reasoning about weakly-consistent programs. In particular, we show that it can be used to derive a proof technique based on Lipton’s reduction theory that allows to prove programs robust.

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 consistency level is achieved with serializable transactions [20] whose outcome in concurrent executions is the same as if the transactions were executed atomically in some order. Since serializability carries a significant penalty on availability, modern databases often provide weaker consistency models, one of the most prominent being snapshot isolation (SI) [4]. Then, an important issue is to ensure that the level of consistency needed by a given program coincides with the one that is guaranteed by its infrastructure, i.e., the database it uses. One way to tackle this issue is to investigate the problem of checking robustness of programs against consistency relaxations: Given a program $\displaystyle P$ and two consistency models $\displaystyle S$ and $\displaystyle W$ such that $\displaystyle S$ is stronger than $\displaystyle W$, we say that $\displaystyle P$ is robust for $\displaystyle S$ against $\displaystyle W$ if for every two implementations $\displaystyle I_{S}$ and $\displaystyle I_{W}$ of $\displaystyle S$ and $\displaystyle W$ respectively, the set of computations of $\displaystyle P$ when running with $\displaystyle I_{S}$ is the same as its set of computations when running with $\displaystyle I_{W}$. This means that $\displaystyle P$ is not sensitive to the consistency relaxation from $\displaystyle S$ to $\displaystyle W$, and therefore it is possible to reason about the behaviors of $\displaystyle P$ assuming that it is running over $\displaystyle S$, and no additional synchronization is required when $\displaystyle P$ runs over the weak model $\displaystyle W$ such that it maintains all its properties satisfied with $\displaystyle S$.

In this paper, we address the problem of verifying robustness of transactional programs for serializability, against snapshot isolation. Under snapshot isolation, any transaction $\displaystyle t$ reads values from a snapshot of the database taken at its start and $\displaystyle t$ can commit only if no other committed transaction has written to a location that $\displaystyle t$ wrote to, since $\displaystyle t$ started. Robustness is a form of program equivalence between two versions of the same program, obtained using two semantics, one more permissive than the other. It ensures that this permissiveness has no effect on the program under consideration. The difficulty in checking robustness is to apprehend the extra behaviors due to the relaxed model w.r.t. the strong model. This requires a priori reasoning about complex order constraints between operations in arbitrarily long computations, which may need maintaining unbounded ordered structures, and make robustness checking hard or even undecidable.

Our first contribution is to show that verifying robustness of transactional programs against snapshot isolation can be reduced in polynomial time to the reachability problem in concurrent programs under sequential consistency (SC). This allows (1) to avoid explicit handling of the snapshots from where transactions read along computations (since this may imply memorizing unbounded information), and (2) to leverage available tools for verifying invariants/reachability problems on concurrent programs. This also implies that the robustness problem is decidable for finite-state programs, PSPACE-complete when the number of sites is fixed, and EXPSPACE-complete otherwise. This is the first result on the decidability and complexity of the problem of verifying robustness in the context of transactional programs. The problem of verifying robustness has been considered in the literature for several models, including eventual and causal consistency [5, 9, 10, 11, 19]. These works provide (over- or under-)approximate analyses for checking robustness, but none of them provides precise (sound and complete) algorithmic verification methods for solving this problem.

Based on this reduction, our second contribution is a proof methodology for establishing robustness which builds on Lipton’s reduction theory [17]. We use the theory of movers to establish whether the relaxations allowed by SI are harmless, i.e., they don’t introduce new behaviors compared to serializability.

We applied the proposed verification techniques on 10 challenging applications extracted from previous work [10, 23, 2, 15, 5, 13, 18]. These techniques were enough for proving or disproving the robustness of these applications.

2 Overview

In this section, we give an overview of our approach for checking robustness against snapshot isolation. While serializability enforces that transactions are atomic and conflicting transactions, i.e., which read or write to a common location, cannot commit concurrently, SI [4] allows that conflicting transactions commit in parallel as long as they don’t contain a write-write conflict, i.e., write on a common location. Moreover, under SI, each transaction reads from a snapshot of the database taken at its start. These relaxations permit the “anomaly” known as Write Skew (WS) shown in Figure 1(a), where an anomaly is a program execution which is allowed by SI, but not by serializability. The execution of Write Skew under SI allows the reads of $\displaystyle{\tt x}$ and $\displaystyle{\tt y}$ to return $\displaystyle 0$ although this cannot happen under serializability. These values are possible since each transaction is executed locally (starting from the initial snapshot) without observing the writes of the other transaction.

Execution trace. Our notion of program robustness is based on an abstract representation of executions called trace. Informally, an execution trace is a set of events, i.e., accesses to shared variables and transaction begin/commit events, along with several standard dependency relations between events recording the data-flow. The transitive closure of the union of all these dependency relations is called happens-before. An execution is an anomaly if the happens-before of its trace is cyclic. Figure 1(b) shows the happens-before of the Write Skew anomaly. Notice that the happens-before order is cyclic in both cases.

Semantically, every transaction execution involves two main events, the issue and the commit. The issue event corresponds to a sequence of reads and/or writes where the writes are visible only to the current transaction. We interpret it as a single event since a transaction starts with a database snapshot that it updates in isolation, without observing other concurrently executing transactions. The commit event is where the writes are propagated and made visible to all processes. Under serializability, the two events coincide, i.e., they are adjacent in the execution. Under SI, this is not the case and in between the issue and the commit of the same transaction, we may have issue/commit events from concurrent transactions. When a transaction commit does not occur immediately after its issue, we say that the underlying transaction is delayed. For example, the following execution of WS corresponds to the happens-before cycle in Figure 1(b) where the write to $\displaystyle x$ was committed after $\displaystyle{t}_{2}$ finished, hence, $\displaystyle{t}_{1}$ was delayed:

[TABLE]

Above, $\displaystyle\textsf{begin}({p}_{1},{t}_{1})$ stands for starting a new transaction $\displaystyle{t}_{1}$ by process $\displaystyle{p}_{1}$, ld represents read (load) actions, while isu denotes write actions that are visible only to the current transaction (not yet committed). The writes performed during $\displaystyle{t}_{1}$ become visible to all processes once the commit event $\displaystyle\textsf{com}({p}_{1},{t}_{1})$ takes place.

Reducing robustness to SC reachability. The above SI execution can be mimicked by an execution of the same program under serializability modulo an instrumentation that simulates the delayed transaction. The local writes in the issue event are simulated by writes to auxiliary registers and the commit event is replaced by copying the values from the auxiliary registers to the shared variables (actually, it is not necessary to simulate the commit event; we include it here for presentation reasons). The auxiliary registers are visible only to the delayed transaction. In order that the execution be an anomaly (i.e., not possible under serializability without the instrumentation) it is required that the issue and the commit events of the delayed transaction are linked by a chain of happens-before dependencies. For instance, the above execution for WS can be simulated by:

[TABLE]

The write to $\displaystyle x$ was delayed by storing the value in the auxiliary register $\displaystyle r_{x}$ and the happens-before chain exists because the read on $\displaystyle y$ that was done by $\displaystyle{t}_{1}$ is conflicting with the write on $\displaystyle y$ from $\displaystyle{t}_{2}$ and the read on $\displaystyle x$ by $\displaystyle{t}_{2}$ is conflicting with the write of $\displaystyle x$ in the simulation of $\displaystyle t_{1}$’s commit event. On the other hand, the following execution of Write-Skew without the read on $\displaystyle y$ in $\displaystyle{t}_{1}$:

[TABLE]

misses the conflict (happens-before dependency) between the issue event of $\displaystyle{t}_{1}$ and $\displaystyle{t}_{2}$. Therefore, the events of $\displaystyle{t}_{2}$ can be reordered to the left of $\displaystyle{t}_{1}$ and obtain an equivalent execution where $\displaystyle\textsf{st}({p}_{1},{t}_{1},x,r_{x})$ occurs immediately after $\displaystyle\textsf{st}({p}_{1},{t}_{1},r_{x},1)$. In this case, $\displaystyle{t}_{1}$ is not anymore delayed and this execution is possible under serializability (without the instrumentation).

If the number of transactions to be delayed in order to expose an anomaly is unbounded, the instrumentation described above may need an unbounded number of auxiliary registers. This would make the verification problem hard or even undecidable. However, we show that it is actually enough to delay a single transaction, i.e., a program admits an anomaly under SI iff it admits an anomaly containing a single delayed transaction. This result implies that the number of auxiliary registers needed by the instrumentation is bounded by the number of program variables, and that checking robustness against SI can be reduced in linear time to a reachability problem under serializability (the reachability problem encodes the existence of the chain of happens-before dependencies mentioned above). The proof of this reduction relies on a non-trivial characterization of anomalies.

Proving robustness using commutativity dependency graphs. Based on the reduction above, we also devise an approximated method for checking robustness based on the concept of mover in Lipton’s reduction theory [17]. An event is a left (resp., right) mover if it commutes to the left (resp., right) of another event (from a different process) while preserving the computation. We use the notion of mover to characterize happens-before dependencies between transactions. Roughly, there exists a happens-before dependency between two transactions in some execution if one doesn’t commute to the left/right of the other one. We define a commutativity dependency graph which summarizes the happens-before dependencies in all executions of a given program between transactions $\displaystyle{t}$ as they appear in the program, transactions $\displaystyle{t}\setminus\{w\}$ where the writes of $\displaystyle{t}$ are

deactivated (i.e., their effects are not visible outside the transaction), and transactions $\displaystyle{t}\setminus\{r\}$ where the reads of $\displaystyle{t}$ obtain non-deterministic values. The transactions $\displaystyle{t}\setminus\{w\}$ are used to simulate issue events of delayed transactions (where writes are not yet visible) while the transactions $\displaystyle{t}\setminus\{r\}$ are used to simulate commit events of delayed transactions (which only write to the shared memory). Two transactions $\displaystyle a$ and $\displaystyle b$ are linked by an edge iff $\displaystyle a$ cannot move to the right of $\displaystyle b$ (or $\displaystyle b$ cannot move to the left of $\displaystyle a$), or if they are related by the program order (i.e., issued in some order in the same process). Then a program is robust if for every transaction $\displaystyle{t}$, this graph doesn’t contain a path from $\displaystyle{t}\setminus\{w\}$ to $\displaystyle{t}\setminus\{r\}$ formed of transactions that don’t write to a variable that $\displaystyle{t}$ writes to (the latter condition is enforced by SI since two concurrent transactions cannot commit at the same time when they write to a common variable). For example, Figure 2 shows the commutativity dependency graph of the modified WS program where the read of $\displaystyle y$ is removed from $\displaystyle{t}_{1}$. The fact that it doesn’t contain any path like above implies that it is robust.

3 Programs

A program is parallel composition of processes distinguished using a set of identifiers $\displaystyle\mathbb{P}$. Each process is a sequence of transactions and each transaction is a sequence of labeled instructions. Each transaction starts with a $\displaystyle\mathtt{begin}$ instruction and finishes with a $\displaystyle\mathtt{commit}$ instruction. Each other instruction is either an assignment to a process-local register from a set $\displaystyle\mathbb{R}$ or to a shared variable from a set $\displaystyle\mathbb{V}$, or an $\displaystyle\mathtt{assume}$ statement. The read/write assignments use values from a data domain $\displaystyle\mathbb{D}$. An assignment to a register $\displaystyle\langle reg\rangle:=\langle var\rangle$ is called a read of the shared-variable $\displaystyle\langle var\rangle$ and an assignment to a shared variable $\displaystyle\langle var\rangle:=\langle reg\text{-}expr\rangle$ is called a write to $\displaystyle\langle var\rangle$ ($\displaystyle\langle reg\text{-}expr\rangle$ is an expression over registers whose syntax we leave unspecified since it is irrelevant for our development). The $\displaystyle\mathtt{assume}$ $\displaystyle\langle bexpr\rangle$ blocks the process if the Boolean expression $\displaystyle\langle bexpr\rangle$ over registers is false. They are used to model conditionals as usual. We use $\displaystyle\mathtt{goto}$ statements to model an arbitrary control-flow where the same label can be assigned to multiple instructions and multiple $\displaystyle\mathtt{goto}$ statements can direct the control to the same label which allows to mimic imperative constructs like loops and conditionals. To simplify the technical exposition, our syntax includes simple read/write instructions. However, our results apply as well to instructions that include SQL (select/update) queries. The experiments reported in Section 7 consider programs with SQL based transactions.

The semantics of a program under SI is defined as follows. The shared variables are stored in a central memory and each process keeps a replicated copy of the central memory. A process starts a transaction by discarding its local copy and fetching the values of the shared variables from the central memory. When a process commits a transaction, it merges its local copy of the shared variables with the one stored in the central memory in order to make its updates visible to all processes. During the execution of a transaction, the process stores the writes to shared variables only in its local copy and reads only from its local copy. When a process merges its local copy with the centralized one, it is required that there were no concurrent updates that occurred after the last fetch from the central memory to a shared variable that was updated by the current transaction. Otherwise, the transaction is aborted and its effects discarded.

More precisely, the semantics of a program $\displaystyle\mathcal{P}$ under SI is defined as a labeled transition system $\displaystyle[\mathcal{P}]_{{\tt SI}{}}$ where transactions are labeled by the set of events

[TABLE]

where begin and com label transitions corresponding to the start and the commit of a transaction, respectively. isu and ld label transitions corresponding to writing, resp., reading, a shared variable during some transaction.

An execution of program $\displaystyle\mathcal{P}$, under snapshot isolation, is a sequence of events $\displaystyle\mathit{ev}_{1}\cdot\mathit{ev}_{2}\cdot\ldots$ corresponding to a run of $\displaystyle[\mathcal{P}]_{{\tt CM}{}}$. The set of executions of $\displaystyle\mathcal{P}$ under SI is denoted by $\displaystyle\mathbb{E}\textsf{x}_{{\tt SI}{}}(\mathcal{P})$.

4 Robustness Against SI

A trace abstracts the order in which shared-variables are accessed inside a transaction and the order between transactions accessing different variables. Formally, the trace of an execution $\displaystyle\rho$ is obtained by (1) replacing each sub-sequence of transitions in $\displaystyle\rho$ corresponding to the same transaction, but excluding the com transition, with a single “macro-event” $\displaystyle\textsf{isu}({p},{t})$, and (2) adding several standard relations between these macro-events $\displaystyle\textsf{isu}({p},{t})$ and commit events $\displaystyle\textsf{com}({p},{t})$ to record the data-flow in $\displaystyle\rho$, e.g. which transaction wrote the value read by another transaction. The sequence of $\displaystyle\textsf{isu}({p},{t})$ and $\displaystyle\textsf{com}({p},{t})$ events obtained in the first step is called a summary of $\displaystyle\rho$. We say that a transaction $\displaystyle{t}$ in $\displaystyle\rho$ performs an external read of a variable $\displaystyle x$ if $\displaystyle\rho$ contains an event $\displaystyle\textsf{ld}({p},{t},x,v)$ which is not preceded by a write on $\displaystyle x$ of $\displaystyle{t}$, i.e., an event $\displaystyle\textsf{isu}({p},{t},x,v)$. Also, we say that a transaction $\displaystyle{t}$ writes a variable $\displaystyle x$ if $\displaystyle\rho$ contains an event $\displaystyle\textsf{isu}({p},{t},x,v)$, for some $\displaystyle v$.

The trace $\displaystyle\mathsf{tr}(\rho)=(\tau,{\mathsf{PO}},{\mathsf{WR}},{\mathsf{WW}},{\mathsf{RW}},{\mathsf{STO}})$ of an execution $\displaystyle\rho$ consists of the summary $\displaystyle\tau$ of $\displaystyle\rho$ along with the program order $\displaystyle{\mathsf{PO}}$, which relates any two issue events $\displaystyle\textsf{isu}({p},{t})$ and $\displaystyle\textsf{isu}({p},{t}^{\prime})$ that occur in this order in $\displaystyle\tau$, write-read relation $\displaystyle{\mathsf{WR}}$ (also called read-from), which relates any two events $\displaystyle\textsf{com}({p},{t})$ and $\displaystyle\textsf{isu}({p}^{\prime},{t}^{\prime})$ that occur in this order in $\displaystyle\tau$ such that $\displaystyle{t}^{\prime}$ performs an external read of $\displaystyle x$, and $\displaystyle\textsf{com}({p},{t})$ is the last event in $\displaystyle\tau$ before $\displaystyle\textsf{isu}({p}^{\prime},{t}^{\prime})$ that writes to $\displaystyle x$ (to mark the variable $\displaystyle x$, we may use $\displaystyle{\mathsf{WR}}(x)$), the write-write order $\displaystyle{\mathsf{WW}}$ (also called store-order), which relates any two store events $\displaystyle\textsf{com}({p},{t})$ and $\displaystyle\textsf{com}({p}^{\prime},{t}^{\prime})$ that occur in this order in $\displaystyle\tau$ and write to the same variable $\displaystyle x$ (to mark the variable $\displaystyle x$, we may use $\displaystyle{\mathsf{WW}}(x)$), the read-write relation $\displaystyle{\mathsf{RW}}$ (also called conflict), which relates any two events $\displaystyle\textsf{isu}({p},{t})$ and $\displaystyle\textsf{com}({p}^{\prime},{t}^{\prime})$ that occur in this order in $\displaystyle\tau$ such that $\displaystyle{t}$ reads a value that is overwritten by $\displaystyle{t}^{\prime}$, and the same-transaction relation $\displaystyle{\mathsf{STO}}$, which relates the issue event with the commit event of the same transaction. The read-write relation $\displaystyle{\mathsf{RW}}$ is formally defined as $\displaystyle{\mathsf{RW}}(x)={\mathsf{WR}}^{-1}(x);{\mathsf{WW}}(x)$ (we use ; to denote the standard composition of relations) and $\displaystyle{\mathsf{RW}}=\bigcup_{x\in\mathbb{V}}{\mathsf{RW}}(x)$. If a transaction $\displaystyle{t}$ reads the initial value of $\displaystyle x$ then $\displaystyle{\mathsf{RW}}(x)$ relates $\displaystyle\textsf{isu}({p},{t})$ to $\displaystyle\textsf{com}({p}^{\prime},{t}^{\prime})$ of any other transaction $\displaystyle{t}^{\prime}$ which writes to $\displaystyle x$ (i.e., $\displaystyle(\textsf{isu}({p},{t}),\textsf{com}({p}^{\prime},{t}^{\prime}))\in{\mathsf{RW}}(x)$) (note that in the above relations, $\displaystyle{p}$ and $\displaystyle{p}^{\prime}$ might designate the same process).

Since we reason about only one trace at a time, to simplify the writing, we may say that a trace is simply a sequence $\displaystyle\tau$ as above, keeping the relations $\displaystyle{\mathsf{PO}}$, $\displaystyle{\mathsf{WR}}$, $\displaystyle{\mathsf{WW}}$, $\displaystyle{\mathsf{RW}}$, and $\displaystyle{\mathsf{STO}}$ implicit. The set of traces of executions of a program $\displaystyle\mathcal{P}$ under SI is denoted by $\displaystyle\mathbb{T}\textsf{r}(\mathcal{P})_{{\tt SI}{}}$.

Serializability semantics. The semantics of a program under serializability can be defined using a transition system where the configurations keep a single shared-variable valuation (accessed by all processes) with the standard interpretation of read and write statements. Each transaction executes in isolation. Alternatively, the serializability semantics can be defined as a restriction of $\displaystyle[\mathcal{P}]_{{\tt SI}{}}$ to the set of executions where each transaction is immediately delivered when it starts, i.e., the start and commit time of transaction coincide $\displaystyle{t}.{st}={t}.{ct}$. Such executions are called serializable and the set of serializable executions of a program $\displaystyle\mathcal{P}$ is denoted by $\displaystyle\mathbb{E}\textsf{x}_{{\tt SER}{}}(\mathcal{P})$. The latter definition is easier to reason about when relating executions under snapshot isolation and serializability, respectively.

Serializable trace. A trace $\displaystyle\mathit{tr}$ is called serializable if it is the trace of a serializable execution. Let $\displaystyle\mathbb{T}\textsf{r}_{{\tt SER}{}}(\mathcal{P})$ denote the set of serializable traces. Given a serializable trace $\displaystyle\mathit{tr}=(\tau,{\mathsf{PO}},{\mathsf{WR}},{\mathsf{WW}},{\mathsf{RW}},{\mathsf{STO}})$ we have that every event $\displaystyle\textsf{isu}({p},{t})$ in $\displaystyle\tau$ is immediately followed by the corresponding $\displaystyle\textsf{com}({p},{t})$ event.

Happens before order. Since multiple executions may have the same trace, it is possible that an execution $\displaystyle\rho$ produced by snapshot isolation has a serializable trace $\displaystyle\mathsf{tr}(\rho)$ even though $\displaystyle\textsf{isu}({p},{t})$ events may not be immediately followed by $\displaystyle\textsf{com}({p},{t})$ actions. However, $\displaystyle\rho$ would be equivalent, up to reordering of “independent” (or commutative) transitions, to a serializable execution. To check whether the trace of an execution is serializable, we introduce the happens-before relation on the events of a given trace as the transitive closure of the union of all the relations in the trace, i.e., $\displaystyle{\mathsf{HB}}=({\mathsf{PO}}\cup{\mathsf{WW}}\cup{\mathsf{WR}}\cup{\mathsf{RW}}\cup{\mathsf{STO}})^{+}$.

Finally, the happens-before relation between events is extended to transactions as follows: a transaction $\displaystyle{t}_{1}$ happens-before another transaction $\displaystyle{t}_{2}\neq{t}_{1}$ if the trace $\displaystyle\mathit{tr}$ contains an event of transaction $\displaystyle{t}_{1}$ which happens-before an event of $\displaystyle{t}_{2}$. The happens-before relation between transactions is denoted by $\displaystyle{\mathsf{HB}}_{t}$ and called transactional happens-before. The following characterizes serializable traces.

Theorem 4.1 ([1, 22])

A trace $\displaystyle\mathit{tr}$ is serializable iff $\displaystyle{\mathsf{HB}}_{t}$ is acyclic.

A program is called robust if it produces the same set of traces as the serializability semantics.

Definition 1

A program $\displaystyle\mathcal{P}$ is called robust against SI iff $\displaystyle\mathbb{T}\textsf{r}_{\textsf{{\tt SI}{}}}(\mathcal{P})=\mathbb{T}\textsf{r}_{{\tt SER}{}}(\mathcal{P})$.

Since $\displaystyle\mathbb{T}\textsf{r}_{{\tt SER}{}}(\mathcal{P})\subseteq\mathbb{T}\textsf{r}_{\textsf{X}}(\mathcal{P})$, the problem of checking robustness of a program $\displaystyle\mathcal{P}$ is reduced to checking whether there exists a trace $\displaystyle\mathit{tr}\in\mathbb{T}\textsf{r}_{{\tt SI}{}}(\mathcal{P})\setminus\mathbb{T}\textsf{r}_{{\tt SER}{}}(\mathcal{P}).$

5 Reducing Robustness against SI to SC Reachability

A trace which is not serializable must contain at least an issue and a commit event of the same transaction that don’t occur one after the other even after reordering of “independent” events. Thus, there must exist an event that occur between the two which is related to both events via the happens-before relation, forbidding the issue and commit to be adjacent. Otherwise, we can build another trace with the same happens-before where events are reordered such that the issue is immediately followed by the corresponding commit. The latter is a serializable trace which contradicts the initial assumption. We define a program instrumentation which mimics the delay of transactions by doing the writes on auxiliary variables which are not visible to other transactions. After the delay of a transaction, we track happens-before dependencies until we execute a transaction that does a “read” on one of the variables that the delayed transaction writes to (this would expose a read-write dependency to the commit event of the delayed transaction). While tracking happens-before dependencies we cannot execute a transaction that writes to a variable that the delayed transaction writes to since SI forbids write-write conflicts between concurrent transactions.

Concretely, given a program $\displaystyle\mathcal{P}$, we define an instrumentation of $\displaystyle\mathcal{P}$ such that $\displaystyle\mathcal{P}$ is not robust against SI iff the instrumentation reaches an error state under serializability. The instrumentation uses auxiliary variables in order to simulate a single delayed transaction which we prove that it is enough for deciding robustness. Let $\displaystyle\textsf{isu}({p},{t})$ be the issue event of the only delayed transaction. The process $\displaystyle{p}$ that delayed $\displaystyle{t}$ is called the Attacker. When the attacker finishes executing the delayed transaction it stops. Other processes that execute transactions afterwards are called Happens-Before Helpers.

The instrumentation uses two copies of the set of shared variables in the original program to simulate the delayed transaction. We use primed variables $\displaystyle x^{\prime}$ to denote the second copy. Thus, when a process becomes the attacker, it will only write to the second copy that is not visible to other processes including the happens-before helpers. The writes made by the other processes including the happens-before helpers are made visible to all processes.

When the attacker delays the transaction $\displaystyle{t}$, it keeps track of the variables it accessed, in particular, it stores the name of one of the variables it writes to, $\displaystyle x$, it tracks every variable $\displaystyle y$ that it reads from and every variable $\displaystyle z$ that it writes to. When the attacker finishes executing $\displaystyle{t}$, and some other process wants to execute some other transaction, the underlying transaction must contain a write to a variable $\displaystyle y$ that the attacker reads from. Also, the underlying transaction must not write to a variable that $\displaystyle{t}$ writes to. We say that this process has joined happens-before helpers through the underlying transaction. While executing this transaction, we keep track of each variable that was accessed and the type of operation, wheather it is a read or write. Afterward, in order for some other transaction to “join” the happens-before path, it must not write to a variable that $\displaystyle{t}$ writes to so it does not violate the fact that SI forbids write-write conflicts, and it has to satisfy one of the following conditions in order to ensure the continuity of the happens-before dependencies: (1) the transaction is issued by a process that has already another transaction in the happens-before dependency (program order dependency), (2) the transaction is reading from a shared variable that was updated by a previous transaction in the happens-before dependency (write-read dependency), (3) the transaction writes to a shared variable that was read by a previous transaction in the happens-before dependency (read-write dependency), or (4) the transaction writes to a shared variable that was updated by a previous transaction in the happens-before dependency (write-write dependency). We introduce a flag for each shared variable to mark the fact that the variable was read or written by a previous transaction.

Processes continue executing transactions as part of the chain of happens-before dependencies, until a transaction does a read on the variable $\displaystyle x$ that $\displaystyle{t}$ wrote to. In this case, we reached an error state which signals that we found a cycle in the transactional happens-before relation.

The instrumentation uses four varieties of flags: a) global flags (i.e., $\displaystyle\mathsf{HB}$, $\displaystyle a_{\textsf{tr}_{\textsf{A}}}$, $\displaystyle a_{\textsf{st}_{\textsf{A}}}$), b) flags local to a process (i.e., $\displaystyle p.a$ and $\displaystyle p.hbh$), and c) flags per shared variable (i.e., $\displaystyle x.event$, $\displaystyle x.event^{\prime}$, and $\displaystyle x.eventI$). We will explain the meaning of these flags along with the instrumentation. At the start of the execution, all flags are initialized to null ($\displaystyle\perp$).

Whether a process is an attacker or happens-before helper is not enforced syntactically by the instrumentation. It is set non-deterministically during the execution using some additional process-local flags. Each process chooses to set to $\displaystyle\mathsf{true}$ at most one of the flags $\displaystyle p.a$ and $\displaystyle p.hbh$, implying that the process becomes an attacker or happens-before helper, respectively. At most one process can be an attacker, i.e., set $\displaystyle p.a$ to $\displaystyle\mathsf{true}$. In the following, we detail the instrumentation for read and write instructions of the attacker and happens-before helpers.

5.1 Instrumentation of the Attacker

Figure 3 lists the instrumentation of the write and read instructions of the attacker. Each process passes through an initial phase where it executes transactions that are visible immediately to all the other processes (i.e., they are not delayed), and then non-deterministically it can choose to delay a transaction at which point it sets the flag $\displaystyle a_{\textsf{tr}_{\textsf{A}}}$ to $\displaystyle\mathsf{true}$. During the delayed transaction it chooses non-deterministically a write instruction to a variable $\displaystyle x$ and stores the name of this variable in the flag $\displaystyle a_{\textsf{st}_{\textsf{A}}}$ (line (5)). The values written during the delayed transaction are stored in the primed variables and are visible only to the current transaction, in case the transaction reads its own writes. For example, given a variable $\displaystyle z$, all writes to $\displaystyle z$ from the original program are transformed into writes to the primed version $\displaystyle z^{\prime}$ (line (3)). Each time, the attacker writes to $\displaystyle z$, it sets the flag $\displaystyle z.event^{\prime}=1$. This flag is used later by transactions from happens-before helpers to avoid writing to variables that the delayed transaction writes to.

A read on a variable, $\displaystyle y$, in the delayed transaction takes her value from the primed version, $\displaystyle y^{\prime}$. In every read in the delayed transaction, we set the flag $\displaystyle y.event$ to ld (line (1)) to be used latter in order for a process to join the happens-before helpers. Afterward, the attacker starts the happens-before path, and it sets the variable $\displaystyle\mathsf{HB}$ to $\displaystyle\mathsf{true}$ (line (2)) to mark the start of the happens. When the flag $\displaystyle\mathsf{HB}$ is set to $\displaystyle\mathsf{true}$ the attacker stops executing new transactions.

5.2 Instrumentation of the Happens-Before Helpers

The remaining processes, which are not the attacker, can become a happens-before helper. Figure 4 lists the instrumentation of write and read instructions of a happens-before helper. In a first phase, each process executes the original code until the flag $\displaystyle a_{\textsf{tr}_{\textsf{A}}}$ is set to $\displaystyle\mathsf{true}$ by the attacker. This flag signals the “creation” of the secondary copy of the shared-variables, which can be observed only by the attacker. At this point, the flag $\displaystyle\mathsf{HB}$ is set to $\displaystyle\mathsf{true}$, and the happens-before helper process chooses non-deterministically a first transaction through which it wants to join the set of happens-before helpers, i.e., continue the happens-before dependency created by the existing happens-before helpers. When a process chooses a transaction, it makes a pledge (while executing the $\displaystyle\mathtt{begin}$ instruction) that during this transaction it will either read from a variable that was written to by another happens-before helper, write to a variable that was accessed (read or written) by another happens-before helper, or write to a variable that was read from in the delayed transaction. When the pledge is met, the process sets the flag $\displaystyle p.hbh$ to true (lines (7) and (11)). The execution is blocked if a process does not keep its pledge (i.e., the flag $\displaystyle p.hbh$ is null) at the end of the transaction. Note that the first process to join the happens-before helper has to execute a transaction $\displaystyle{t}$ which writes to a variable that was read from in the delayed transaction since this is the only way to build a happens-before between $\displaystyle{t}$, and the delayed transaction ($\displaystyle{\mathsf{PO}}$ is not possible since $\displaystyle{t}$ is not from the attacker, $\displaystyle{\mathsf{WR}}$ is not possible since $\displaystyle{t}$ does not see the writes of the delayed transaction, and $\displaystyle{\mathsf{WW}}$ is not possible since $\displaystyle{t}$ cannot write to a variable that the delayed transaction writes to). We use a flag $\displaystyle x.event$ for each variable $\displaystyle x$ to record the type (read ld or write st) of the last access made by a happens-before helper (lines (8) and (10)). During the execution of a transaction that is part of the happens-before dependency, we must ensure that the transaction does not write to variable $\displaystyle y$ where $\displaystyle y.even^{\prime}$ is set to $\displaystyle 1$. Otherwise, the execution is blocked (line 9).

The happens-before helpers continue executing their instructions, until one of them reads from the shared variable $\displaystyle x$ whose name was stored in $\displaystyle a_{\textsf{st}_{\textsf{A}}}$. This establishes a happens-before dependency between the delayed transaction and a “fictitious” store event corresponding to the delayed transaction that could be executed just after this read of $\displaystyle x$. The execution doesn’t have to contain this store event explicitly since it is always enabled. Therefore, at the end of every transaction, the instrumentation checks whether the transaction read $\displaystyle x$. If it is the case, then the execution stops and goes to an error state to indicate that this is a robustness violation. Notice that after the attacker stops, the only processes that are executing transactions are happens-before helpers, which is justified since when a process is not from a happens-before helper it implies that we cannot construct a happens-before dependency between a transaction of this process and the delayed transaction which means that the two transactions commute which in turn implies that this process’s transactions can be executed before executing the delayed transaction of the attacker.

5.3 Correctness

The role of a process in an execution is chosen non-deterministically at runtime. Therefore, the final instrumentation of a given program $\displaystyle\mathcal{P}$, denoted by $\displaystyle[\![\mathcal{P}]\!]$, is obtained by replacing each labeled instruction $\displaystyle\langle linst\rangle$ with the concatenation of the instrumentations corresponding to the attacker and the happens-before helpers, i.e., $\displaystyle\ \ \ [\![\langle linst\rangle]\!]::=[\![\langle linst\rangle]\!]_{\textsf{A}}\hskip 4.83691pt[\![\langle linst\rangle]\!]_{\textsf{HbH}}$

The following theorem states the correctness of the instrumentation.

Theorem 5.1

$\displaystyle\mathcal{P}$ is not robust against SI iff $\displaystyle[\![\mathcal{P}]\!]$ reaches the error state.**

If a program is not robust, this implies that the execution of the program under SI results in a trace where the happens-before is cyclic. Which is possible only if the program contains at least one delayed transaction. In the proof of this theorem, we show that is sufficient to search for executions that contain a single delayed transaction.

Notice that in the instrumentation of the attacker, the delayed transaction must contain a read and write instructions on different variables. Also, the transactions of the happens-before helpers must not contain a write to a variable that the delayed transaction writes to. The following corollary states the complexity of checking robustness for finite-state programs 111Programs with a bounded number of variables taking values from a bounded domain. against snapshot isolation. It is a direct consequence of Theorem 5.1 and of previous results concerning the reachability problem in concurrent programs running over a sequentially-consistent memory, with a fixed [16] or parametric number of processes [21].

Corollary 1

*Checking robustness of finite-state programs against snapshot isolation is PSPACE-complete when the number of processes is fixed and

EXPSPACE-complete, otherwise.*

The instrumentation can be extended to SQL (select/update) queries where a statement may include expressions over a finite/infinite set of variables, e.g., by manipulating a set of flags x.event for each statement instead of only one.

6 Proving Program Robustness

As a more pragmatic alternative to the reduction in the previous section, we define an approximated method for proving robustness which is inspired by Lipton’s reduction theory [17].

Movers. Given an execution $\displaystyle\tau=\mathit{ev}_{1}\cdot\ldots\cdot\mathit{ev}_{n}$ of a program $\displaystyle\mathcal{P}$ under serializability (where each event $\displaystyle\mathit{ev}_{i}$ corresponds to executing an entire transaction), we say that the event $\displaystyle\mathit{ev}_{i}$ moves right (resp., left) in $\displaystyle\tau$ if $\displaystyle\mathit{ev}_{1}\cdot\ldots\cdot\mathit{ev}_{i-1}\cdot\mathit{ev}_{i+1}\cdot\mathit{ev}_{i}\cdot\mathit{ev}_{i+2}\cdot\ldots\cdot\mathit{ev}_{n}$ (resp., $\displaystyle\mathit{ev}_{1}\cdot\ldots\cdot\mathit{ev}_{i-2}\cdot\mathit{ev}_{i}\cdot\mathit{ev}_{i-1}\cdot\mathit{ev}_{i+1}\cdot\ldots\cdot\mathit{ev}_{n}$) is also a valid execution of $\displaystyle\mathcal{P}$, the process of $\displaystyle\mathit{ev}_{i}$ is different from the process of $\displaystyle\mathit{ev}_{i+1}$ (resp., $\displaystyle\mathit{ev}_{i-1}$), and both executions reach to the same end state $\displaystyle\sigma_{n}$. For an execution $\displaystyle\tau$, let $\displaystyle\mathsf{instOf}_{\tau}(\mathit{ev}_{i})$ denote the transaction that generated the event $\displaystyle\mathit{ev}_{i}$. A transaction $\displaystyle{t}$ of a program $\displaystyle\mathcal{P}$ is a right (resp., left) mover if for all executions $\displaystyle\tau$ of $\displaystyle\mathcal{P}$ under serializability, the event $\displaystyle\mathit{ev}_{i}$ with $\displaystyle\mathsf{instOf}(\mathit{ev}_{i})={t}$ moves right (resp., left) in $\displaystyle\tau$.

If a transaction $\displaystyle{t}$ is not a right mover, then there must exist an execution $\displaystyle\tau$ of $\displaystyle\mathcal{P}$ under serializability and an event $\displaystyle\mathit{ev}_{i}$ of $\displaystyle\tau$ with $\displaystyle\mathsf{instOf}(\mathit{ev}_{i})={t}$ that does not move right. This implies that there must exist another $\displaystyle\mathit{ev}_{i+1}$ of $\displaystyle\tau$ which caused $\displaystyle\mathit{ev}_{i}$ to not be a right mover. Since $\displaystyle\mathit{ev}_{i}$ and $\displaystyle\mathit{ev}_{i+1}$ do not commute, then this must be because of either a write-read, write-write, or a read-write dependency. If $\displaystyle{t}^{\prime}=\mathsf{instOf}(\mathit{ev}_{i+1})$, we say that $\displaystyle{t}$ is not a right mover because of $\displaystyle{t}^{\prime}$ and some dependency that is either write-read, write-write, or read-write. Notice that when $\displaystyle{t}$ is not a right mover because of $\displaystyle{t}^{\prime}$ then $\displaystyle{t}^{\prime}$ is not a left mover because of $\displaystyle{t}$.

We define $\displaystyle{\mathsf{M_{WR}}}$ as a binary relation between transactions such that $\displaystyle({t},{t}^{\prime})\in{\mathsf{M_{WR}}}$ when $\displaystyle{t}$ is not a right mover because of $\displaystyle{t}^{\prime}$ and a write-read dependency. We define the relations $\displaystyle{\mathsf{M_{WW}}}$ and $\displaystyle{\mathsf{M_{RW}}}$ corresponding to write-write and read-write dependencies in a similar way.

Read/Write-free transactions. Given a transaction $\displaystyle{t}$, we define $\displaystyle{t}\setminus\{r\}$ as a variation of $\displaystyle{t}$ where all the reads from shared variables are replaced with non-deterministic reads, i.e., $\displaystyle\langle reg\rangle:=\langle var\rangle$ statements are replaced with $\displaystyle\langle reg\rangle:=\star$ where $\displaystyle\star$ denotes non-deterministic choice. We also define $\displaystyle{t}\setminus\{w\}$ as a variation of $\displaystyle{t}$ where all the writes to shared variables in $\displaystyle{t}$ are disabled. Intuitively, recalling the reduction to SC reachability in Section 5, $\displaystyle{t}\setminus\{w\}$ simulates the delay of a transaction by the Attacker, i.e., the writes are not made visible to other processes, and $\displaystyle{t}\setminus\{r\}$ approximates the commit of the delayed transaction which only applies a set of writes.

Commutativity dependency graph. Given a program $\displaystyle\mathcal{P}$, we define the commutativity dependency graph as a graph where vertices represent transactions and their read/write-free variations. Two vertices which correspond to the original transactions in $\displaystyle\mathcal{P}$ are related by a program order edge, if they belong to the same process. The other edges in this graph represent the “non-mover” relations $\displaystyle{\mathsf{M_{WR}}}$, $\displaystyle{\mathsf{M_{WW}}}$, and $\displaystyle{\mathsf{M_{RW}}}$.

Given a program $\displaystyle\mathcal{P}$, we say that the commutativity dependency graph of $\displaystyle\mathcal{P}$ contains a non-mover cycle if there exist a set of transactions $\displaystyle{t}_{0},{t}_{1},\ldots,{t}_{n}$ of $\displaystyle\mathcal{P}$ such that the following hold:

1. (a)

$\displaystyle({t}^{\prime\prime}_{0},{t}_{1})\in{\mathsf{M_{RW}}}$ where $\displaystyle{t}^{\prime\prime}_{0}$ is the write-free variation of $\displaystyle{t}_{0}$ and $\displaystyle{t}_{1}$ does not write to a variable that $\displaystyle{t}_{0}$ writes to; 2. (b)

for all $\displaystyle i\in[1,n]$, $\displaystyle({t}_{i},{t}_{i+1})\in({\mathsf{PO}}\cup{\mathsf{M_{WR}}}\cup{\mathsf{M_{WW}}}\cup{\mathsf{M_{RW}}})$, $\displaystyle{t}_{i}$ and $\displaystyle{t}_{i+1}$ do not write to a shared variable that $\displaystyle{t}_{0}$ writes to; 3. (c)

$\displaystyle({t}_{n},{t}^{\prime}_{0})\in{\mathsf{M_{RW}}}$ where $\displaystyle{t}^{\prime}_{0}$ is the read-free variation of $\displaystyle{t}_{0}$ and $\displaystyle{t}_{n}$ does not write to a variable that $\displaystyle{t}_{0}$ writes to.

A non-mover cycle approximates an execution of the instrumentation defined in Section 5 in between the moment that the Attacker delays a transaction $\displaystyle{t}_{0}$ (which here corresponds to the write-free variation $\displaystyle{t}^{\prime\prime}_{0}$) and the moment where $\displaystyle{t}_{0}$ gets committed (the read-free variation $\displaystyle{t}^{\prime}_{0}$).

The following theorem shows that the acyclicity of the commutativity dependency graph of a program implies the robustness of the program. Actually, the notion of robustness in this theorem relies on a slightly different notion of trace where store-order and write-order dependencies take into account values, i.e., store-order relates only writes writing different values and the write-order relates a read to the oldest write (w.r.t. execution order) writing its value. This relaxation helps in avoiding some harmless robustness violations due to for instance, two transactions writing the same value to some variable.

Theorem 6.1

For a program $\displaystyle\mathcal{P}$, if the commutativity dependency graph of $\displaystyle\mathcal{P}$ does not contain non-mover cycles, then $\displaystyle\mathcal{P}$ is robust.

7 Experiments

To test the applicability of our robustness checking algorithms, we have considered a benchmark of 10 applications extracted from the literature related to weakly consistent databases in general. A first set of applications are open source projects that were implemented to be run over the Cassandra database, extracted from [10]. The second set of applications is composed of: TPC-C [23], an on-line transaction processing benchmark widely used in the database community, SmallBank, a simplified representation of a banking application [2], FusionTicket, a movie ticketing application [15], Auction, an online auction application [5], and Courseware, a course registration service extracted from [13, 18].

A first experiment concerns the reduction of robustness checking to SC reachability. For each application, we have constructed a client (i.e., a program composed of transactions defined within that application) with a fixed number of processes (at most 3) and a fixed number of transactions (between 3 and 7 transactions per process). We have encoded the instrumentation of this client, defined in Section 5, in the Boogie programming language [3] and used the Civl verifier [14] in order to check whether the assertions introduced by the instrumentation are violated (which would represent a robustness violation). Note that since clients are of fixed size, this requires no additional assertions/invariants (it is an instance of bounded model checking). The results are reported in Table 1. We have found two of the applications, Courseware and SmallBank, to not be robust against snapshot isolation. The violation in Courseware is caused by transactions RemoveCourse and EnrollStudent that execute concurrently, RemoveCourse removing a course that has no registered student and EnrollStudent registering a new student to the same course. We get an invalid state where a student is registered for a course that was removed. SmallBank’s violation contains transactions Balance, TransactSaving, and WriteCheck. One process executes WriteCheck where it withdraws an amount from the checking account after checking that the sum of the checking and savings accounts is bigger than this amount. Concurrently, a second process executes TransactSaving where it withdraws an amount from the saving account after checking that it is smaller than the amount in the savings account. Afterwards, the second process checks the contents of both the checking and saving accounts. We get an invalid state where the sum of the checking and savings accounts is negative.

Since in the first experiment we consider fixed clients, the lack of assertion violations doesn’t imply that the application is robust (this instantiation of our reduction can only be used to reveal robustness violations). Thus, a second experiment concerns the robustness proof method based on commutativity dependency graphs (Section 6). For the applications that were not identified as non-robust by the previous method, we have used Civl to construct their commutativity dependency graphs, i.e., identify the “non-mover” relations $\displaystyle{\mathsf{M_{WR}}}$, $\displaystyle{\mathsf{M_{WW}}}$, and $\displaystyle{\mathsf{M_{RW}}}$ (Civl allows to check whether some code fragment is a left/right mover). In all cases, the graph didn’t contain non-mover cycles, which allows to conclude that the applications are robust.

The experiments show that our results can be used for finding violations and proving robustness, and that they apply to a large set of interesting examples. Note that the reduction to SC and the proof method based on commutativity dependency graphs are valid for programs with SQL (select/update) queries.

8 Related Work

Decidability and complexity of robustness has been investigated in the context of relaxed memory models such as TSO and Power [8, 6, 12]. Our work borrows some high-level principles from [6] which addresses the robustness against TSO. We reuse the high-level methodology of characterizing minimal violations according to some measure and defining reductions to SC reachability using a program instrumentation. Instantiating this methodology in our context is however very different, several fundamental differences being:

1. –

SI and TSO admit different sets of relaxations and SI is a model of transactional databases. 2. –

We use a different notion of measure: the measure in [6] counts the number of events between a write issue and a write commit while our notion of measure counts the number of delayed transactions. This is a first reason for which the proof techniques in [6] don’t extend to our context. 3. –

Transactions induce more complex traces: two transactions might be related by several dependency relations since each transaction may contain multiple reads and writes to different locations. In TSO, each action is a read or a write to some location, and two events are related by a single dependency relation. Also, the number of dependencies between two transactions depends on the execution since the set of reads/writes in a transaction evolves dynamically.

Other works [8, 12] define decision procedures which are based on the theory of regular languages and do not extend to infinite-state programs like in our case.

As far as we know, our work provides the first results concerning the decidability and the complexity of robustness checking in the context of transactions. The existing work on the verification of robustness for transactional programs provide either over- or under-approximate analyses. Our commutativity dependency graphs are similar to the static dependency graphs used in [5, 9, 10, 11], but they are more precise, i.e., reducing the number of false alarms. The static dependency graphs record happens-before dependencies between transactions based on a syntactic approximation of the variables accessed by a transaction. For example, our techniques are able to prove that the program in Figure 5 is robust, while this is not possible using static dependency graphs. The latter would contain a dependency from transaction $\displaystyle{t}_{1}$ to $\displaystyle{t}_{2}$ and one from $\displaystyle{t}_{2}$ to $\displaystyle{t}_{1}$ just because syntactically, each of the two transactions reads both variables and may write to one of them. Our dependency graphs take into account the semantics of these transactions and do not include this happens-before cycle. Other over- and under-approximate analyses have been proposed in [19]. They are based on encoding executions into first order logic, bounded-model checking for the under-approximate analysis, and a sound check for proving a cut-off bound on the size of the happens-before cycles possible in the executions of a program, for the over-approximate analysis. The latter is strictly less precise than our method based on commutativity dependency graphs. For instance, extending the TPC-C application with additional transactions will make the method in [19] fail while our method will succeed in proving robustness (the three transactions are for adding a new product, adding a new warehouse based on the number of customers and warehouses, and adding a new customer, respectively).

Finally, the idea of using Lipton’s reduction theory for checking robustness has been also used in the context of the TSO memory model [7], but the techniques are completely different, e.g., the TSO technique considers each update in isolation and doesn’t consider non-mover cycles like in our commutativity dependency graphs.

Appendix 0.A Programs

0.A.1 Program Syntax

We consider a simple programming language grammar which is defined in Figure 6. A program is parallel composition of processes distinguished using a set of identifiers $\displaystyle\mathbb{P}$. Each process is a sequence of transactions and each transaction is a sequence of labeled instructions. Each transaction starts with a $\displaystyle\mathtt{begin}$ instruction and finishes with a $\displaystyle\mathtt{commit}$ instruction. Each other instruction is either an assignment to a process-local register from a set $\displaystyle\mathbb{R}$ or to a shared variable from a set $\displaystyle\mathbb{V}$, or an $\displaystyle\mathtt{assume}$ statement. The read/write assignments use values from a data domain $\displaystyle\mathbb{D}$. An assignment to a register $\displaystyle\langle reg\rangle:=\langle var\rangle$ is called a read of $\displaystyle\langle var\rangle$ and an assignment to a shared variable $\displaystyle\langle var\rangle:=\langle reg\text{-}expr\rangle$ is called a write to $\displaystyle\langle var\rangle$ ($\displaystyle\langle reg\text{-}expr\rangle$ is an expression over registers whose syntax we leave unspecified since it is irrelevant for our development). The $\displaystyle\mathtt{assume}$ $\displaystyle\langle bexpr\rangle$ blocks the process if the Boolean expression $\displaystyle\langle bexpr\rangle$ over registers is false.

0.A.2 Program Semantics Under SnapShot Isolation

The semantics of a program under SI is defined as follows. The shared variables are stored in a central memory and each process keeps a replicated copy of the central memory. A process starts a transaction by discarding its local copy and fetching the values of the shared variables from the central memory. When a process commits a transaction, it merges its local copy of the shared variables with the one stored in the central memory in order to make its updates visible to all processes. During the execution of a transaction, the process stores the writes to shared variables only in its local copy and reads only from its local copy. When a process merges its local copy with the centralized one, it is required that there were no concurrent updates that occurred after the last fetch from the central memory to a shared variable that was updated by the current transaction. Otherwise, the transaction is aborted and its effects discarded.

Thus, a program configuration is a tuple $\displaystyle\textsf{gs}=(\textsf{ls},\textsf{tstamp},\textsf{Log})$ where $\displaystyle\textsf{ls}:\mathbb{P}\rightarrow\mathbb{S}$ associates a local state in $\displaystyle\mathbb{S}$ to each process in $\displaystyle\mathbb{P}$, $\displaystyle\textsf{tstamp}:\mathbb{V}\rightarrow\mathbb{T}$ stores the largest timestamp for each shared variable, and $\displaystyle\textsf{Log}:\mathbb{V}\rightarrow\mathbb{D}$ holds the global valuation of shared variables. A local state is a tuple $\displaystyle\left\langle\textsf{pc},\textsf{store},\textsf{log},\textsf{rval}\right\rangle$ where $\displaystyle\textsf{pc}\in\mathbb{L}\textsf{ab}$ is the program counter, i.e., the label of the next instruction to be executed, $\displaystyle\textsf{store}:\mathbb{V}\rightarrow\mathbb{D}$ is the local valuation of the shared variables, $\displaystyle\textsf{log}:\mathbb{V}\rightarrow\{\bot,1\}$ is a local log which marks shared variables which were updated in a transaction, and $\displaystyle\textsf{rval}:\mathbb{R}\rightarrow\mathbb{D}$ is the valuation of the local registers. For a local state $\displaystyle s$, we use $\displaystyle s.\textsf{pc}$ to denote the program counter component of $\displaystyle s$, and similarly for all the other components of $\displaystyle s$. Given a transaction $\displaystyle{t}\in\mathbb{T}\times\mathbb{T}$, we use $\displaystyle{t}.{st}$ to denote the start time of transaction $\displaystyle{t}$ and $\displaystyle{t}.{ct}$ to denote the commit time of $\displaystyle{t}$. Before merging store with Log, after executing a transaction $\displaystyle{t}$, we check that for every variable $\displaystyle x$ that $\displaystyle{t}$ writes to ($\displaystyle\textsf{log}(x)\neq\bot$) we have that $\displaystyle\textsf{tstamp}(x)<{t}.{st}$ (i.e., there were no concurrent write to $\displaystyle x$). Then, we store the value of $\displaystyle\textsf{store}(x)$ for every variable $\displaystyle x$ that $\displaystyle{t}$ writes to ($\displaystyle\textsf{log}(x)\neq\bot$) in $\displaystyle\textsf{Log}(x)$. Also, for every variable $\displaystyle x$ that $\displaystyle{t}$ writes to, we store $\displaystyle{t}.{ct}$ in $\displaystyle\textsf{tstamp}(x)$.

Then, the semantics of a program $\displaystyle\mathcal{P}$ under snapshot isolation consistency model is defined using a labeled transition system (LTS) $\displaystyle[\mathcal{P}]_{{\tt SI}{}}=(\mathbb{C},\mathbb{E}\textsf{v},\textsf{gs}_{0},\rightarrow)$ where $\displaystyle\mathbb{C}$ is the set of program configurations, $\displaystyle\mathbb{E}\textsf{v}$ is a set of transition labels called events, $\displaystyle\textsf{gs}_{0}$ is the initial program configuration, and $\displaystyle\rightarrow\subseteq\mathbb{C}\times\mathbb{E}\textsf{v}\times\mathbb{C}$ is the transition relation. The set of events under SI is defined as follow.

[TABLE]

where begin and com label transitions corresponding to the start and the commit of a transaction, respectively. isu and ld label transitions corresponding to writing, resp., reading, a shared variable during some transaction.

The transition relation $\displaystyle\rightarrow$ is defined in Figure 7. For readability, the events labeling a transition are written on top of $\displaystyle\rightarrow$. A begin transition resets the local valuation of the shared variables and fetches their values from the central memory. A com transition applies the writes performed in a transaction to the central memory by merging the contents of the local copy store with the central memory Log. An ld transition reads the value of a shared-variable from the local copy store while an isu transition applies a new write to the local copy store.

An execution of program $\displaystyle\mathcal{P}$, under snapshot isolation, is a sequence of events $\displaystyle\mathit{ev}_{1}\cdot\mathit{ev}_{2}\cdot\ldots$ labeling the transitions, such that there exists a sequence of configurations $\displaystyle\textsf{gs}_{0}\cdot\textsf{gs}_{1}\cdot\ldots$ where $\displaystyle\textsf{gs}_{0}$ is the initial configuration before $\displaystyle\mathcal{P}$ starts execution and $\displaystyle\textsf{gs}_{i-1}\xrightarrow{\mathit{ev}_{i}}\textsf{gs}_{i}$ is a valid transition for $\displaystyle i>1$. of transitions. The set of executions of $\displaystyle\mathcal{P}$ under SI is denoted by $\displaystyle\mathbb{E}\textsf{x}_{{\tt SI}{}}(\mathcal{P})$.

Appendix 0.B Proofs of Section 5: Characterizations of SI Trace-Robustness

In this section, we describe the proof of Theorem 5.1. We first reduce the robustness of a program $\displaystyle\mathcal{P}$ against SI to the existence of some execution trace $\displaystyle\mathit{tr}\in\mathbb{T}\textsf{r}_{{\tt SI}{}}(\mathcal{P})\setminus\mathbb{T}\textsf{r}_{{\tt SER}{}}(\mathcal{P})$ that has a specific shape. We call a trace $\displaystyle\mathit{tr}\in\mathbb{T}\textsf{r}_{{\tt SI}{}}(\mathcal{P})\setminus\mathbb{T}\textsf{r}_{{\tt SER}{}}(\mathcal{P})$, an anomaly. Then, we show that of the anomaly of a particular shape is equivalent to an execution of the instrumented program reaching an error state.

First, we give an auxiliary lemma about the happens-before relation (between events). In the remaining of this section, we use $\displaystyle{\mathsf{HB}}^{1}$ to denote the happens-before without the transitive closure, i.e., $\displaystyle{\mathsf{HB}}^{1}=({\mathsf{PO}}\cup{\mathsf{WW}}\cup{\mathsf{WR}}\cup{\mathsf{RW}}\cup{\mathsf{STO}})$. To decide if two events in a trace are “independent” (or commutative) we use the information about the existence of a happens-before relation between the events. If two events are not related by happens-before then they can be swapped while preserving the same happens-before. Thus, we extend the happens-before relation to obtain the happens-before through relation as follows:

Definition 2 ([6])

Let $\displaystyle\tau=\alpha\cdot a\cdot\beta\cdot b\cdot\gamma$ be a trace where $\displaystyle a$ and $\displaystyle b$ are events (or atomic macro events), and $\displaystyle\alpha$, $\displaystyle\beta$, and $\displaystyle\gamma$ are sequences of events (or atomic macro events) under a semantics $\displaystyle{\tt SI}{}$. We say that $\displaystyle a$ happens-before $\displaystyle b$ through $\displaystyle\beta$ if there is a non empty sub-sequence $\displaystyle c_{1}\cdots c_{n}$ of $\displaystyle\beta$ that satisfies:

[TABLE]

where $\displaystyle c_{0}=a$, $\displaystyle c_{n+1}=b$.

We deduce from the definition of serializable traces, that a anomaly trace must contain at least an issue and a commit events of the same transaction that are related via the happens-before through relation. Otherwise, we can build another trace with the same happens-before where events are reordered such that every issue $\displaystyle\textsf{isu}({p},{t})$ is immediately followed by the corresponding commit $\displaystyle\textsf{com}({p},{t})$. The latter is a serializable trace which contradicts the initial assumption.

Lemma 1

Given an anomaly $\displaystyle\tau$, there must exist a transaction $\displaystyle{t}$ such that $\displaystyle\tau=\alpha\cdot\textsf{isu}({p},{t})\cdot\beta\cdot\textsf{com}({p},{t})\cdot\gamma$ and $\displaystyle\textsf{isu}({p},{t})$ happens before $\displaystyle\textsf{com}({p},{t})$ through $\displaystyle\beta$.

Given an anomaly of the from $\displaystyle\tau=\alpha\cdot\textsf{isu}({p},{t})\cdot\beta\cdot\textsf{com}({p},{t})\cdot\gamma$, we call $\displaystyle{t}$ a delayed transaction in the trace $\displaystyle\tau$ when $\displaystyle\textsf{isu}({p},{t})$ happens before $\displaystyle\textsf{com}({p},{t})$ through $\displaystyle\beta$.

For an anomaly $\displaystyle\tau$, the number of delays, denoted by $\displaystyle\#(\tau)$, in $\displaystyle\tau$ is the total number of delayed transactions in the trace.

[TABLE]

Definition 3 (Minimal anomaly)

An anomaly $\displaystyle\tau$ is called minimal if it has the least number of delays among all possible anomalies (for a given program $\displaystyle\mathcal{P}$).

Given an anomaly $\displaystyle\tau=\alpha\cdot\textsf{isu}({p},{t})\cdot\beta\cdot\textsf{com}({p},{t})\cdot\gamma$, and assuming that $\displaystyle{t}$ is the first delayed transaction in $\displaystyle\tau$ (w.r.t. the order between issue events of delayed transactions) and that $\displaystyle\tau$ is a minimal anomaly, the following lemma shows that we can assume w.l.o.g. that $\displaystyle\gamma$ is empty.

Lemma 2

Let $\displaystyle\tau=\alpha\cdot\textsf{isu}({p},{t})\cdot\beta\cdot\textsf{com}({p},{t})\cdot\gamma$ be a minimal anomaly such that $\displaystyle\textsf{isu}({p},{t})$ happens-before $\displaystyle\textsf{com}({p},{t})$ through $\displaystyle\beta$. Then, $\displaystyle\tau^{\prime}=\alpha\cdot\textsf{isu}({p},{t})\cdot\beta\cdot\textsf{com}({p},{t})$ is also a minimal anomaly.

Proof

We can notice that after executing the event $\displaystyle\textsf{com}({p},{t})$, we obtain a cycle in the $\displaystyle{\mathsf{HB}}_{t}$ relation. Thus, $\displaystyle\tau^{\prime}$ is already an anomaly not serializable.

The following result relates SI robustness problem to finding certain anomaly trace which is a minimal anomaly where only a single transaction is delayed.

Theorem 0.B.1

A program $\displaystyle\mathcal{P}$ is not robust under SI iff there exists an anomaly $\displaystyle\tau$ under SI such that the following must hold:

[TABLE]

1. (a)

$\displaystyle\textsf{isu}({p},{t})$* is the issue of the only delayed transaction in $\displaystyle\tau$; (Lemmas 6 and 5);* 2. (b)

$\displaystyle\textsf{isu}({p},{t})$* happens before $\displaystyle\textsf{com}({p},{t})$ through $\displaystyle\beta$ (Lemma 6);* 3. (c)

for any event $\displaystyle a\in\beta$, we have that $\displaystyle(\textsf{isu}({p},{t}),a)\in{\mathsf{HB}}$ and $\displaystyle(a,\textsf{com}({p},{t}))\in{\mathsf{HB}}$ (Lemma 6); 4. (d)

there exist events $\displaystyle a$ and $\displaystyle b$ in $\displaystyle\beta$ such that $\displaystyle(\textsf{isu}({p},{t}),a)\in{\mathsf{RW}}(x)$ and $\displaystyle(b,\textsf{com}({p},{t}))\in{\mathsf{RW}}(y)$ with $\displaystyle x\neq y$ (Lemma 6); 5. (e)

all delayed transactions in $\displaystyle\beta$ don’t write to shared variables that $\displaystyle{t}$ writes to (Lemma 3).

Note that in certain cases the events $\displaystyle a$ and $\displaystyle b$ can be identical and $\displaystyle\beta=a$. Figure 8 shows two examples of anomalies of the form given in Theorem 0.B.1.

In the following, we give the lemmas that constitute Theorem 0.B.1.

An important property in SI semantics is that of conflict-free, and since the event $\displaystyle\textsf{com}({p},{t})$ is successfully executed only if there are no concurrent writes that were committed after $\displaystyle\textsf{isu}({p},{t})$. Thus, for every event $\displaystyle\textsf{com}({p}_{0},{t}_{0})$ in $\displaystyle\beta$, $\displaystyle\textsf{com}({p}_{0},{t}_{0})$ don’t write to a shared variable that $\displaystyle\textsf{com}({p},{t})$ writes to.

Lemma 3

Let $\displaystyle\tau=\alpha\cdot\textsf{isu}({p},{t})\cdot\beta\cdot\textsf{com}({p},{t})$ be a minimal anomaly such that $\displaystyle\textsf{isu}({p},{t})$ happens-before $\displaystyle\textsf{com}({p},{t})$ through $\displaystyle\beta$. Then, for every $\displaystyle a\in\beta$, $\displaystyle a$ does not write to a shared variable that $\displaystyle\textsf{com}({p},{t})$ writes to.

The following lemma shows that we must have an event $\displaystyle\textsf{isu}({p}^{\prime},{t}^{\prime})\in\beta$ such that $\displaystyle\textsf{isu}({p}^{\prime},{t}^{\prime})$ happens before $\displaystyle\textsf{com}({p},{t})$.

Lemma 4

Let $\displaystyle\tau=\alpha\cdot\textsf{isu}({p},{t})\cdot\beta\cdot\textsf{com}({p},{t})$ be a minimal anomaly such that $\displaystyle\textsf{isu}({p},{t})$ happens-before $\displaystyle\textsf{com}({p},{t})$ through $\displaystyle\beta$. Then, there must exist an event $\displaystyle\textsf{isu}({p}^{\prime},{t}^{\prime})\in\beta$ such that $\displaystyle\textsf{isu}({p}^{\prime},{t}^{\prime})$ happens before $\displaystyle\textsf{com}({p},{t})$, i.e., $\displaystyle(\textsf{isu}({p}^{\prime},{t}^{\prime}),\textsf{com}({p},{t}))\in{\mathsf{HB}}$.

Proof

Suppose by contradiction that $\displaystyle\beta$ does not contain an event $\displaystyle\textsf{isu}({p}^{\prime},{t}^{\prime})$ such that $\displaystyle\textsf{isu}({p}^{\prime},{t}^{\prime})$ happens before $\displaystyle\textsf{com}({p},{t})$. Then, $\displaystyle\textsf{com}({p},{t})$ can be swapped with every $\displaystyle\textsf{isu}({p}^{\prime},{t}^{\prime})$ event in $\displaystyle\beta$. Thus, we obtain that the two events $\displaystyle\textsf{isu}({p},{t})$ and $\displaystyle\textsf{com}({p},{t})$ are adjacent which means that $\displaystyle{t}$ is no longer a delayed transaction which is a contradiction. Therefore, $\displaystyle\beta$ does contain an event $\displaystyle\textsf{isu}({p}^{\prime},{t}^{\prime})$ such that $\displaystyle(\textsf{isu}({p}^{\prime},{t}^{\prime}),\textsf{com}({p},{t}))\in{\mathsf{HB}}$.

Next lemma shows that we can always obtain a minimal anomaly trace $\displaystyle\tau=\alpha\cdot\textsf{isu}({p},{t})\cdot\beta\cdot\textsf{com}({p},{t})$ where $\displaystyle\beta$ contains no delayed transaction. We show that if it were to have a delayed transaction $\displaystyle{t}_{0}$ in $\displaystyle\beta$, then it is possible to obtain a new anomaly where either $\displaystyle{t}$ is not delayed or $\displaystyle{t}_{0}$ is not delayed, and obtain a new anomaly with a smaller number of delayed transactions which contradicts the minimality assumption.

Lemma 5

Let $\displaystyle\tau=\alpha\cdot\textsf{isu}({p},{t})\cdot\beta\cdot\textsf{com}({p},{t})$ be a minimal anomaly. Then, $\displaystyle\beta$ does not contain delayed transactions.

Proof

We suppose by contradiction that $\displaystyle\beta$ contains a delayed transaction $\displaystyle{t}_{0}$ issued by a process $\displaystyle{p}_{0}$.

It is important to notice that there must exist $\displaystyle\beta^{\prime}\subset\beta$ and $\displaystyle\textsf{com}({p}_{0},{t}_{0})\in\beta$ such that $\displaystyle\textsf{isu}({p}_{0},{t}_{0})$ happens before $\displaystyle\textsf{com}({p}_{0},{t}_{0})$ through $\displaystyle\beta$. Otherwise, we can commute the events until $\displaystyle\textsf{com}({p}_{0},{t}_{0})$ occurs just after $\displaystyle\textsf{isu}({p}_{0},{t}_{0})$ and in this case transaction $\displaystyle{t}_{0}$ is not delayed by $\displaystyle{p}_{0}$. Thus, $\displaystyle\tau$ is of the form $\displaystyle\tau=\alpha\cdot\textsf{isu}({p},{t})\cdot\beta_{1}\cdot\textsf{isu}({p}_{0},{t}_{0})\cdot\beta^{\prime}\cdot\textsf{com}({p}_{0},{t}_{0})\cdot\beta_{2}\cdot\textsf{com}({p},{t})$.

Notice that we can build happens-before cycle from $\displaystyle\textsf{isu}({p}_{0},{t}_{0})$ to $\displaystyle\textsf{com}({p}_{0},{t}_{0})$. Also, since in $\displaystyle\beta_{1}\cdot\textsf{isu}({p}_{0},{t}_{0})\cdot\beta^{\prime}\cdot\textsf{com}({p}_{0},{t}_{0})\cdot\beta_{2}$ no transaction depends on $\displaystyle\textsf{isu}({p},{t})$. Thus, we can safely remove $\displaystyle\textsf{isu}({p},{t})$ and its associated commit event $\displaystyle\textsf{com}({p},{t})$ and obtains: $\displaystyle\tau^{\prime}=\alpha\cdot\beta_{1}\cdot\textsf{isu}({p}_{0},{t}_{0})\cdot\beta^{\prime}\cdot\textsf{com}({p}_{0},{t}_{0})\cdot\beta_{2}$. which is an anomaly because of the cycle formed as $\displaystyle\textsf{isu}({p}_{0},{t}_{0})$ happens-before $\displaystyle\textsf{com}({p}_{0},{t}_{0})$ through $\displaystyle\beta^{\prime}$. In $\displaystyle\tau^{\prime}$, transaction $\displaystyle{t}$ was not delayed, therefore, $\displaystyle\tau^{\prime}$ has less number of delays than $\displaystyle\tau$. Thus, $\displaystyle\tau$ is not a minimal anomaly, a contradiction to our hypothesis.

The next lemma characterizes the relation between the first delayed transaction and the commit of the underlying transaction. It shows the type of the first and last happens-before relations in the happens-before path between the issue of the only delayed transaction and its corresponding commit.

Lemma 6

Let $\displaystyle\tau=\alpha\cdot\textsf{isu}({p},{t})\cdot\beta\cdot\textsf{com}({p},{t})$ be a minimal anomaly under SI. Then, the following must hold: There exist $\displaystyle({p}_{0},{t}_{0}),\ ({p}_{1},{t}_{1})\in\beta$ where $\displaystyle(\textsf{isu}({p},{t}),({p}_{0},{t}_{0}))\in{\mathsf{RW}}$, and $\displaystyle(({p}_{1},{t}_{1}),\textsf{com}({p},{t}))\in{\mathsf{RW}}$.

Proof

We have that since $\displaystyle\textsf{isu}({p},{t})$ happens-before $\displaystyle\textsf{com}({p},{t})$ through $\displaystyle\beta$ and $\displaystyle\beta$ does not contain a delayed transaction. Then, there must exist $\displaystyle({p}_{0},{t}_{0})$ and $\displaystyle({p}_{1},{t}_{1})$ in $\displaystyle\beta$ such that $\displaystyle(\textsf{isu}({p},{t}),({p}_{0},{t}_{0}))\in{\mathsf{HB}}^{1}$, $\displaystyle(({p}_{1},{t}_{1}),\textsf{com}({p},{t}))\in{\mathsf{HB}}^{1}$, and $\displaystyle(({p}_{0},{t}_{0}),({p}_{1},{t}_{1}))\in{\mathsf{HB}}$. It is important to note that $\displaystyle({p}_{0},{t}_{0})$ and $\displaystyle({p}_{1},{t}_{1})$ might be identical in which case $\displaystyle\beta=({p}_{0},{t}_{0})$.

Notice that every event in $\displaystyle\beta$ (including $\displaystyle({p}_{0},{t}_{0})$ and $\displaystyle({p}_{1},{t}_{1})$) cannot write to a variable that $\displaystyle({p},{t})$ writes to under SI semantics, thus store order relation is not possible. Also, since $\displaystyle({p},{t})$ is not visible to any event in $\displaystyle\beta$ thus the read-from and program order are not possible. Thus, the only possibility is that $\displaystyle(\textsf{isu}({p},{t}),({p}_{0},{t}_{0}))\in{\mathsf{RW}}$, and $\displaystyle(({p}_{1},{t}_{1}),\textsf{com}({p},{t}))\in{\mathsf{RW}}$.

Appendix 0.C Proofs of Section 5: The Complete Instrumentation

In this section, we present the instrumentation for the remaining instructions which are, begin and commit for the attacker and happens-before helper.

0.C.1 Instrumentation of the Attacker

We provide in Figure 9, the instrumentation of the code for the attacker process. When the attacker randomly chooses a transaction to delay, it sets the flag $\displaystyle a_{\textsf{tr}_{\textsf{A}}}$ to $\displaystyle\mathsf{true}$ in the instruction begin (line (15)). Then, it sets the flag $\displaystyle p.a$ to 1 to indicate that the current process is the attacker. It copies the values from every variable $\displaystyle x$ to its primed version $\displaystyle x^{\prime}$.

In the case the attacker starts the happens-before chain, it has to set the variable $\displaystyle\mathsf{HB}$ to $\displaystyle\mathsf{true}$ to mark the start of the happens-before chain and the end of the visibility chain and set the flag $\displaystyle x.event$ to ld (line (2) in Figure 3). We can notice that when the $\displaystyle\mathsf{HB}$ is set to $\displaystyle\mathsf{true}$, we can no longer execute new transactions from the attacker (all conditions in lines (13) and (14) become $\displaystyle\mathsf{false}$).

0.C.2 Instrumentation of the Happens-Before Helpers

In Figure 10, we provide the instrumentation of the remaining instructions of a happens-before helper.

When the flag $\displaystyle{\mathsf{HB}}$ is set to $\displaystyle\mathsf{true}$, a process (which cannot be the attacker, i.e., the flag $\displaystyle p.a$ is null) starts the attempts to join the set of happens-before helpers. Thus, it randomly chooses a first transaction (the begin of this transaction is shown in line (16)) through which the process will join the set of happens-before helpers. When a process chose the transaction to join happens-before helpers, that means it has made pledge that during this transaction it will either do read from a variable that was updated by a another delayed transaction from some other process in happens-before helpers or write to a variable that was accessed with a read or write from another process in happens-before helpers. When either one of these criteria are satisfied the flag $\displaystyle p.hbh$ will be set to true. If a process does not keep its pledge (the flag $\displaystyle p.hbh$ is null) then before executing the com instruction of the first transaction we block the execution (line (20)).

The happens-before helpers processes continue executing their instructions, until one of them executes a load that reads from the shared variable $\displaystyle x$ that was stored in $\displaystyle a_{\textsf{st}_{\textsf{A}}}$ which implies the existence of a happens-before cycle. When executing the instruction com at the end of every transaction, we have a conditional check to detect if we have a load or a write accessing the variable $\displaystyle x$ (lines (17), (18), and (19)). When the check detects that the variable $\displaystyle x$ was accessed, the execution goes to the error state (line (19)) to indicate that the execution has produced an anomaly and we denote the reached state of the instrumented program’s execution, the error state.

As a direct consequence of Theorem 5.1, the next corollary states that some programs which have certain characteristics are robust against SI.

Corollary 2

Given a program $\displaystyle\mathcal{P}$, if one of the following holds:

1. (a)

every transaction of $\displaystyle\mathcal{P}$ contains a single instruction either a read or a write; 2. (b)

every transaction of $\displaystyle\mathcal{P}$ contains only read/write events that access a single variable (different transactions might read/write to different variables); 3. (c)

given a variable $\displaystyle x$, every transaction of $\displaystyle\mathcal{P}$ contains a write to the variable $\displaystyle x$.

then $\displaystyle\mathcal{P}$ is robust under SI.

Appendix 0.D Proofs of Section 5: Soundness and Completeness of the Instrumentation

The aim of the instrumentation procedure is to reduce the problem of checking the existence of the anomaly described in Theorem 0.B.1 to reachability under serialisability of en error state by the instrumented version of a program. The instrumentation procedure is considered sound and complete iff if an error state is reachable, then we can reconstruct an anomaly, and every anomaly ensures that the error state is reachable by the instrumented version of the program.

Theorem 0.D.1 (Soundness and Completeness)

A program $\displaystyle\mathcal{P}$ is not robust iff the instrumented version of it, $\displaystyle\mathcal{P}^{\prime}$, reaches an error state under SER.

Proof

Soundness. Suppose that the instrumented program reaches an error state. Then, the execution’s trace of the instrumented program is of the form:

[TABLE]

The last transaction, $\displaystyle({p}^{\prime},{t}^{\prime})$ performed by a process $\displaystyle{p}^{\prime\prime}$ that has a read accessing the variable $\displaystyle x=a_{\textsf{st}_{\textsf{A}}}$ and is part of the happens-before helpers. Because the conditional check can be performed only by a process ($\displaystyle{p}_{HbH1}$) that is one of the happens-before helpers and is currently executing.

In order for $\displaystyle{p}_{HbH1}$, to join the set of happens-before helpers, it must have found that the valuation of the flag $\displaystyle\mathsf{HB}$ is not null which means there exists some process $\displaystyle{p}$ that is the attacker that sets the flag $\displaystyle\mathsf{HB}$ to $\displaystyle\mathsf{true}$. In $\displaystyle\tau_{1}$, the attacker, happens-before helpers, and other processes start executing the original instructions without setting any flags or delaying any transactions. Afterwards, the attacker issues the delayed transaction $\displaystyle\textsf{isu}({p},{t})$ and it starts populating the primed variables $\displaystyle x^{\prime}$ and reading from them and setting the flags $\displaystyle x.event^{\prime}$ to $\displaystyle 1$ for every variable $\displaystyle x$ that it writes to and $\displaystyle y.event$ to ld for every variable $\displaystyle y$ that it reads from. During the execution of $\displaystyle{t}$, the attacker sets the flag $\displaystyle\mathsf{HB}$ to $\displaystyle\mathsf{true}$. Hence, the happens-before helpers start checking at every instruction whether the flags $\displaystyle x.event$ are set to either st or ld. If so, they start populating the flags $\displaystyle x.event$ and $\displaystyle l.event$ as well. When $\displaystyle\mathsf{HB}$ is set to $\displaystyle\mathsf{true}$, the attacker stop issuing new transactions. Therefore, all transaction in $\displaystyle\tau_{2}$ are from the happens-before helpers.

We now transform $\displaystyle\tau_{\star}$ into the following execution trace:

[TABLE]

Here, $\displaystyle\tau_{1}^{\prime}$ is the subsequence of all $\displaystyle\tau_{1}$ events that are produced by instructions from $\displaystyle\mathcal{P}$ without the conditionals checking (i.e., the assume statements). The transaction $\displaystyle{t}$ which is executed by the attacker represents the delayed transactions in $\displaystyle\tau$ with the removal of the conditionals checking and the flags setting. $\displaystyle\tau_{2}^{\prime}$ is the subsequence of all events of $\displaystyle\tau_{2}$ produced by transactions from $\displaystyle\mathcal{P}$ which are executed only by the happens-before helpers except the conditionals checking and the flags setting. We add the commit of transaction $\displaystyle\textsf{com}({p}_{0},{t})$ to describe the commit of the delayed transaction that was delayed by the attacker. $\displaystyle\tau$ is a possible execution’s trace of the program $\displaystyle\mathcal{P}$ because $\displaystyle\tau_{\star}$ is result of an execution of the instrumented version of $\displaystyle\mathcal{P}$ and we have removed from $\displaystyle\tau$ all the effects of the instrumentation, and replaced the stores to auxiliary variables by issues of stores without changing the dependency between all the events in the execution.

All transactions in $\displaystyle\tau_{2}^{\prime}$ are from the happens-before helpers. Transactions in $\displaystyle\tau_{2}^{\prime}$ form a happens-before path between $\displaystyle\textsf{isu}({p},{t})$ and $\displaystyle\textsf{com}({p},{t})$. Also, we have $\displaystyle a,\ b=({p}^{\prime},{t}^{\prime})\in\tau_{2}^{\prime}$ such that $\displaystyle(\textsf{isu}({p},{t}),a)\in{\mathsf{RW}}(y)$ and $\displaystyle(b,\textsf{com}({p},{t}))\in{\mathsf{RW}}(x)$. No transaction in $\displaystyle\tau_{2}^{\prime}$ writes to a variable that $\displaystyle{t}$ writes to. Hence, $\displaystyle\tau$ indeed holds all the properties of the anomaly described in Theorem 0.B.1.

Completeness. Suppose we have an anomaly of a given program $\displaystyle\mathcal{P}$:

[TABLE]

such that $\displaystyle\tau$ maintains all the properties given in Theorem 0.B.1. We demonstrate that there is a possible serializable execution based on $\displaystyle\tau$ of the instrumented version of the program $\displaystyle\mathcal{P}$ that reaches the error state. Next, we show how to build the instrumented program execution.

At the start of the execution, $\displaystyle\tau_{1}$, the attacker, happens-before helpers, and other processes execute the original transactions with just conditional checks.

Afterwards, the attacker delays the transaction $\displaystyle\textsf{isu}({p},{t})$ and starts populating the flags. In $\displaystyle\textsf{isu}({p},{t})$, the attacker issues a store to the shared variable $\displaystyle`x`=a_{\textsf{st}_{\textsf{A}}}$ and $\displaystyle\exists\ b\in\tau_{2}$ such that $\displaystyle(b,\textsf{com}({p},{t}))\in{\mathsf{RW}}(x)$. All writes that were executed in $\displaystyle{t}$ by the attacker are invisible to the remaining processes which includes the happens-before helpers. While executing $\displaystyle{t}$, the attacker sets the content of the flag $\displaystyle y.event$ to ld for every variable $\displaystyle y$ that it reads from and it sets the flag $\displaystyle{\mathsf{HB}}{}$ to $\displaystyle\mathsf{true}$.

On the other hand, the processes which are executing their transactions without delaying them will attempt to join the happens-before helpers by checking if the flag $\displaystyle{\mathsf{HB}}{}$ is set to $\displaystyle\mathsf{true}$. If so, they start the attempt of joining the happens-before helpers and when it succeed they joining the happens-before helpers and start executing their transactions which constitute $\displaystyle\tau_{2}$. The first executed transaction by the happens-before helpers is $\displaystyle a$ described above which signals the start of $\displaystyle\tau_{2}$ and the happen before dependency. Thus, in $\displaystyle\tau_{2}$, we have only transactions form the happens-before helpers (because the attacker stop when the flag $\displaystyle{\mathsf{HB}}{}$ is set to $\displaystyle\mathsf{true}$) such that they are related by the happen before dependency that started from $\displaystyle\textsf{isu}({p},{t})$ until it reaches $\displaystyle\textsf{com}({p},{t})$ through $\displaystyle\tau_{2}$. We know that there must exist $\displaystyle b\in\tau_{2}$ such that $\displaystyle(b,\textsf{com}({p},{t}))\in{\mathsf{RW}}(`x`=a_{\textsf{st}_{\textsf{A}}})$. $\displaystyle b$ is equivalent to the last executed transaction by the happens-before helpers that accesses the shared variable $\displaystyle x$. Thus, the underlying happens-before helper will set the content of the flag $\displaystyle x.event$ to ld. Hence, when the underlying process executes the com instruction of this transaction, it will go to the error state (lines (17), (18), and (19)) and in this case the instrumented version of the program $\displaystyle\mathcal{P}$ has reached the desired error state.

Appendix 0.E Proofs of Section 6

The following theorem shows that the acyclicity of the commutativity dependency graph of a program implies the robustness of the program. Actually, the notion of robustness in this theorem relies on a slightly different notion of trace where store-order and write-order dependencies take into account values, i.e., store-order relates only transactions writing different values and the write-order relates a reading transaction to the oldest transaction (w.r.t. execution order) writing its value. In more details, we assume that two transactions are $\displaystyle{\mathsf{WW}}$-related iff they write different values. Notice that since $\displaystyle{\mathsf{RW}}$ is defined using $\displaystyle{\mathsf{WW}}$ then when two transactions are $\displaystyle{\mathsf{WW}}$-related iff they write different values then when two transactions are $\displaystyle{\mathsf{RW}}$-related this implies that the value that is read is different than the one that is written. For example, in Figure 11(a), if we don’t have this weakening of $\displaystyle{\mathsf{WW}}$ we get an execution trace, where the happens-before is cyclic, of the form $\displaystyle\tau=\textsf{isu}({p}_{1},{t}_{1})\cdot({p}_{2},{t}_{2})\cdot({p}_{3},{t}_{3})\cdot\textsf{com}({p}_{1},{t}_{1})$ because of the $\displaystyle{\mathsf{WW}}$ relation that links $\displaystyle({p}_{2},{t}_{2})$ and $\displaystyle({p}_{3},{t}_{3})$. However, with our weakening of $\displaystyle{\mathsf{WW}}$ there will be no $\displaystyle{\mathsf{WW}}$ relation between $\displaystyle({p}_{2},{t}_{2})$ and $\displaystyle({p}_{3},{t}_{3})$ and this the above execution can be equivalently rewritten as $\displaystyle\tau=({p}_{3},{t}_{3})\cdot\textsf{isu}({p}_{1},{t}_{1})\textsf{com}({p}_{1},{t}_{1})\cdot({p}_{2},{t}_{2})$ which is serializable. Similarly, we assume that two transactions $\displaystyle{t}_{1}$ and $\displaystyle{t}_{2}$ are related by $\displaystyle{\mathsf{WR}}$ iff when we swap the two transactions $\displaystyle{t}_{2}$ does not read the same value that $\displaystyle{t}_{1}$ is writing. For instance, in Figure 11(b), if we don’t have this assumption we get an execution trace, where the happens-before is cyclic, of the form $\displaystyle\tau=\textsf{isu}({p}_{1},{t}_{1})\cdot({p}_{2},{t}_{2})\cdot({p}_{3},{t}_{3})\cdot\textsf{com}({p}_{1},{t}_{1})$ because of the $\displaystyle{\mathsf{WR}}$ relation that links $\displaystyle({p}_{2},{t}_{2})$ and $\displaystyle({p}_{3},{t}_{3})$. However, with our assumption on $\displaystyle{\mathsf{WR}}$ there will be no $\displaystyle{\mathsf{WR}}$ relation between $\displaystyle({p}_{2},{t}_{2})$ and $\displaystyle({p}_{3},{t}_{3})$ and this the above execution can be equivalently rewritten as $\displaystyle\tau=({p}_{3},{t}_{3})\cdot\textsf{isu}({p}_{1},{t}_{1})\textsf{com}({p}_{1},{t}_{1})\cdot({p}_{2},{t}_{2})$ which is serializable. This approach helps in avoiding some of the harmless anomalies, where the happens before cycle might be caused by a write-write dependency between two transactions that writes the same values.

Theorem 0.E.1

For a program $\displaystyle\mathcal{P}$, if (1) the commutativity dependency graph of $\displaystyle\mathcal{P}$ does not contain non-mover cycles, then (2) $\displaystyle\mathcal{P}$ is robust.

Proof

We prove the contrapositive, i.e., $\displaystyle\neg(2)\Rightarrow\neg(1)$. For the proof, we use the result of Theorem 5.1.

Assuming that the program $\displaystyle\mathcal{P}$ is not robust. Then, based on Theorem 5.1 there must exist an execution of the instrumentation of $\displaystyle\mathcal{P}$ that reaches the error state. We suppose that $\displaystyle{t}$ is the delayed transaction, $\displaystyle{t}_{ins}$ is the instrumentation of $\displaystyle{t}$ (writes are stored in auxiliary registers), and $\displaystyle{p}$ is the attacker process. Therefore, the execution of the instrumentation of $\displaystyle\mathcal{P}$ that reaches the error state is of the form $\displaystyle\tau=\alpha\cdot({p},{t}_{ins})\cdot a\cdot\beta\cdot b$ where $\displaystyle a$ writes to a variable that $\displaystyle{t}$ reads from and $\displaystyle b$ reads from a variable that $\displaystyle{t}$ writes to. We assume that $\displaystyle b$ is the first event that does read that accesses a variable that $\displaystyle{t}$ writes to. In the following we show that the commutativity dependency graph of $\displaystyle\mathcal{P}$ contains a non-mover cycle where $\displaystyle{t}$ is $\displaystyle{t}_{0}$. We consider two cases, first case when $\displaystyle a=b$ and $\displaystyle\beta=\epsilon$, and second case is when $\displaystyle a\neq b$.

First case: $\displaystyle\tau=\alpha\cdot({p},{t}_{ins})\cdot a$ where $\displaystyle a$ writes to a variable that $\displaystyle{t}$ reads from, reads from a variable that $\displaystyle{t}$ writes to, and does not write to a variable that $\displaystyle{t}$ writes to. Assume that $\displaystyle a=({p}_{1},{t}_{1})$. Thus, we can safely obtain $\displaystyle\tau_{0}=\alpha\cdot({p}_{1},{t}_{1})\cdot({p},{t}^{\prime})$ a serializable execution trace of $\displaystyle\mathcal{P}$ where $\displaystyle{t}^{\prime}$ is the reads free instantiation of $\displaystyle{t}$. Since $\displaystyle(({p}_{1},{t}_{1}),\textsf{com}({p},{t}))\in{\mathsf{RW}}$ then $\displaystyle{t}_{1}$ reads a value that $\displaystyle{t}^{\prime}$ is overwriting with a different value. Therefore, $\displaystyle\tau^{\prime}_{0}=\alpha\cdot({p},{t}^{\prime})\cdot({p}_{1},{t}_{1})$ is either a serializable execution with a different end state than $\displaystyle\tau_{0}$ has or it is not an serializable execution. Thus, $\displaystyle({t}_{1},{t}^{\prime})\in{\mathsf{M_{RW}}}$ and $\displaystyle{t}_{1}$ does not write to a variable that $\displaystyle{t}$ writes to. Similarly, we can safely obtain $\displaystyle\tau_{n}=\alpha\cdot({p},{t}^{\prime\prime})\cdot({p}_{1},{t}_{1})$ a serializable execution trace of $\displaystyle\mathcal{P}$ where $\displaystyle{t}^{\prime\prime}$ is the writes free instantiation of $\displaystyle{t}$. Since $\displaystyle(\textsf{isu}({p},{t}),({p}_{1},{t}_{1}))\in{\mathsf{RW}}$ then $\displaystyle{t}^{\prime\prime}$ reads a value that $\displaystyle{t}_{1}$ is overwriting with a different value. Therefore, $\displaystyle\tau^{\prime}_{n}=\alpha\cdot({p}_{1},{t}_{1})\cdot({p},{t}^{\prime\prime})$ is either a serializable execution with a different end state than $\displaystyle\tau_{n}$ has or it is not an serializable execution. Thus, $\displaystyle({t}^{\prime\prime},{t}_{1})\in{\mathsf{M_{RW}}}$ and $\displaystyle{t}_{1}$ does not write to a variable that $\displaystyle{t}$ writes to.

Second case: $\displaystyle\tau=\alpha\cdot({p},{t}_{ins})\cdot a\cdot\beta\cdot b$ where $\displaystyle a$ writes to a variable that $\displaystyle{t}$ reads from, $\displaystyle b$ reads from a variable that $\displaystyle{t}$ writes to, and every transaction in $\displaystyle a\cdot\beta\cdot b$ does not write to a variable that $\displaystyle{t}$ writes to. Assume that $\displaystyle a=({p}_{1},{t}_{1})$ and $\displaystyle b=({p}_{n},{t}_{n})$. Since the transactions in $\displaystyle({p}_{1},{t}_{1})\cdot\beta\cdot({p}_{n},{t}_{n})$ constitute the happens-before path in the execution trace $\displaystyle\tau$. Then, for every $\displaystyle({p}_{i},{t}_{i}),\ ({p}_{i+1},{t}_{i+1})\in({p}_{1},{t}_{1})\cdot\beta\cdot({p}_{n},{t}_{n})$ we have that $\displaystyle(({p}_{i},{t}_{i}),({p}_{i+1},{t}_{i+1}))\in({\mathsf{PO}}\cup{\mathsf{WR}}\cup{\mathsf{WW}}\cup{\mathsf{RW}})$. In the case $\displaystyle(({p}_{i},{t}_{i}),({p}_{i+1},{t}_{i+1}))\in({\mathsf{WR}}\cup{\mathsf{WW}}\cup{\mathsf{RW}})$, we can safely obtain $\displaystyle\tau_{i}=\alpha\cdot\gamma\cdot({p}_{i},{t}_{i})\cdot({p}_{i+1},{t}_{i+1})$ which is a serializable execution trace of $\displaystyle\mathcal{P}$ where $\displaystyle\gamma$ either empty (i.e., $\displaystyle\epsilon$) or $\displaystyle\gamma=({p}_{1},{t}_{1})\cdot\cdots\cdot({p}_{i-1},{t}_{i-1})$. Since, $\displaystyle(({p}_{i},{t}_{i}),({p}_{i+1},{t}_{i+1}))\in({\mathsf{WR}}\cup{\mathsf{WW}}\cup{\mathsf{RW}})$, then swapping $\displaystyle{t}_{i}$ and $\displaystyle{t}_{i}+1$ will result in either reordering of writes or write overwrites a read, or read obtains a different value. Therefore, $\displaystyle\tau^{\prime}_{i}=\alpha\cdot\gamma\cdot({p}_{i+1},{t}_{i+1})\cdot({p}_{i},{t}_{i})$ is either a serializable execution trace with a different end state than $\displaystyle\tau_{i}$ has or it is not an serializable execution trace. Thus, $\displaystyle({t}_{i},{t}_{i+1})\in{\mathsf{M_{RW}}}$. Also, we have that $\displaystyle{t}_{i}$ and $\displaystyle{t}_{i+1}$ do not write to a variable that $\displaystyle{t}$ writes to. Similar to the first case, we can safely obtain $\displaystyle\tau_{0}=\alpha\cdot({p}_{1},{t}_{1})\cdot\beta\cdot({p}_{n},{t}_{n})\cdot({p},{t}^{\prime})$ a serializable execution trace of $\displaystyle\mathcal{P}$ where $\displaystyle{t}^{\prime}$ is the reads free instantiation of $\displaystyle{t}$. Since $\displaystyle(({p}_{n},{t}_{n}),\textsf{com}({p},{t}))\in{\mathsf{RW}}$ then $\displaystyle{t}_{n}$ reads a value that $\displaystyle{t}^{\prime}$ is overwriting with a different one. Therefore, $\displaystyle\tau^{\prime}_{0}=\alpha\cdot({p}_{1},{t}_{1})\cdot\beta\cdot({p},{t}^{\prime})\cdot({p}_{n},{t}_{n})$ is either a serializable execution with a different end state than $\displaystyle\tau_{0}$ has or it is not an serializable execution trace. Thus, $\displaystyle({t}_{n},{t}^{\prime})\in{\mathsf{M_{RW}}}$ and $\displaystyle{t}_{n}$ does not write to a variable that $\displaystyle{t}$ writes to. Furthermore, we can safely obtain $\displaystyle\tau_{n}=\alpha\cdot({p},{t}^{\prime\prime})\cdot({p}_{1},{t}_{1})$ a serializable execution trace of $\displaystyle\mathcal{P}$ where $\displaystyle{t}^{\prime\prime}$ is the writes free instantiation of $\displaystyle{t}$. Since $\displaystyle(\textsf{isu}({p},{t}),({p}_{1},{t}_{1}))\in{\mathsf{RW}}$ then $\displaystyle{t}^{\prime\prime}$ reads a value that $\displaystyle{t}_{1}$ is overwriting with a different one. Then, $\displaystyle\tau^{\prime}_{n}=\alpha\cdot({p}_{1},{t}_{1})\cdot({p},{t}^{\prime\prime})$ is either a serializable execution trace with a different end state than $\displaystyle\tau_{n}$ has or it is not an serializable execution trace. Thus, $\displaystyle({t}^{\prime\prime},{t}_{1})\in{\mathsf{M_{RW}}}$ and $\displaystyle{t}_{1}$ does not write to a variable that $\displaystyle{t}$ writes to.

Appendix 0.F Experiments Appendix

In this section we describe the applications we used to evaluate our techniques. For every table in the original application program, we added a boolean annotation in our formalization of the table in Boogie, in order, to inspect whether a given record does exist in the table or not. For instance, if we consider the following table Customer(CustomerId, CustomerName), in Boogie, we formalize the table as two maps: CustomerAlive which takes a CustomerId and returns true if there is a customer with underlying id and else otherwise, CustomerTable which takes a CustomerId and returns the corresponding CustomerName. Also, in certain cases we formalize a Table as multiple maps. Below, we describe each application.

Auction [5]: Which has five transactions that manipulate three tables: BIDS, ITEMS, and USERS. Transaction RegBid is for placing a bid on an item. Transaction RegUser is for registration a user. Transaction ViewItem is for viewing the number of bids for an item. Transaction ViewUser is for looking at a user name. Transaction ViewUsers is for looking at all registered users.

Cassieq-Core222https://github.com/paradoxical-io/cassieq: A core unit of a distributed queue. It has eight transactions that manipulate a single table: USERACCOUNTS. Transaction AddNewAccount is for adding a new account in USERACCOUNTS. Transaction DeleteAnAccount is for deleting an account from USERACCOUNTS. Transaction AddNewKey is for adding a new key to an existing account in USERACCOUNTS. Transaction DeleteAKey is removing a key from an existing account in USERACCOUNTS. Transaction GetAnAccount is to check whether there exist an account with a given id in the table USERACCOUNTS. Transaction GetAccounts is to return all existing accounts in USERACCOUNTS. Transaction GetAccountKeys is for getting all the keys of certain account in USERACCOUNTS. Transaction GetAccountKey is to check whether a certain account does hold a certain key in USERACCOUNTS.

Courseware [13, 18]: Which has five transactions that manipulate three tables: STUDENT, COURSE, and ENROLED. Transaction RegisterStudent is for registering a new student in the table STUDENT. Transaction AddCourse is for adding a new course in the table COURSE. Transaction EnrollStudent is for enrolling a given registered student in a given course. Transaction RemoveCourse is for removing a given course from the table COURSE. Transaction QueryCourses is for inspecting courses in the table COURSE.

Currency-Exchange333https://github.com/Haiyan2/Trade: A trading service. It has six transactions that manipulate a single table: TRADES. Transaction SaveTrade is for registering a new trade. Transaction ViewListTrades is for viewing the trades that occurred before a given instance of time. Transaction ViewTrade is for inspecting a given trade. Transaction ViewTradeUser is for looking for a user who carried out a given trade. Transaction GetNbTrades is for inspecting the number of trades. Transaction GetTradeTimeStamp is for looking for the time stamp of a given trade.

FusionTicket [15]: Which has four transactions that manipulate a single table: EVENTS. Transaction AddEvent is adding new event in some given venue. Transaction ViewEvent is for looking at given a event and the number of tickets available at this event. Transaction Browse is for looking at events that are planned in some given venue. Transaction Purchase is for buying a ticket at a certain event.

Shopping-Cart444https://github.com/nikhilswagle/Shopping_Cart_Angular_Cassandra: An on-line shop service implemented over Cassandra. It has four transactions that query two tables: USERS and PRODUCTS. Transaction GetUser is for querying the existence of a user in the table USERS. Transaction GetProductsByCategory is for finding products that are in a given category. Transaction GetProductByUPC is for finding a product through its UPC. Transaction GetCategories is for finding the categories.

Playlist555https://github.com/DataStaxDocs/playlist: An on-line music service. It has fourteen transactions that manipulate three tables: USERS, TRACKS, and ARTISTS. Transaction AddTrack is for adding a new track in the table TRACKS. Transaction GetTrack is for getting a certain track from the table TRACKS. Transaction AddUser is for adding a new user in the table USERS. Transaction GetUser is for looking for a certain user in the table USERS. Transaction CreatePlayList is for creating a playlist of certain user in the table USERS. Transaction ListArtistByLetter is for listing artists by their first letters of their names. Transaction ListSongsByArtist is for listing tracks produced by certain artist. Transaction ListSongsByGenre is for listing tracks of certain genre type. Transaction AddTrackToPlaylist is for adding an existing track (in TRACKS) to an existing user play list in the table USERS. Transaction DeleteTrackFromPlaylist is for removing a track from user play list in the table USERS. Transaction GetPlaylistForUser is for getting the contents of certain play list of certain user. Transaction GetPlaylistNames is for getting all the play lists of certain user. Transaction DeletePlayListForUser is for deleting a certain user’s play list. Transaction DeleteUser is deleting a user from the table USERS.

RoomStore666https://github.com/mebigfatguy/roomstore: A messages bot service. It has five transactions that manipulate a single table: MESSAGES. Transaction AddMessage is for adding a new message to the table MESSAGES. Transaction GetLastMessage is for getting the messages of given user. Transaction GetMessages is for looking for messages that were added in a certain date. Transaction GetSpecificMessage is for getting specific message that was added in a certain date and time. Transaction GetTopicMessages is for getting messages that are of certain topic.

SmallBank [2]: Which has five transactions that manipulate three tables: ACCOUNT, SAVING, and CHECKING. Transaction Balance is for looking at both the saving and checking balances of a given user account. Transaction DepositChecking is for depositing a certain amount into the checking balance. Transaction TransactSaving is for depositing or withdrawing into/form the saving balance. Transaction Amalgamate (Amg) is for moving the saving and checking balances of an account to another account checking balance and resetting the saving and checking balances of the first account to zero. Transaction WriteCheck is for withdrawing from a given account’s checking balance.

TPC-C [23]: Which has five transactions that manipulate nine tables: WAREHOUSE, DISTRICT, STOCK, ITEMS, CUSTOMERS, HISTORY, ORDER, NEWORDER, and ORDERLINE. Transaction NewOrder is for placing a new order on a set of items. Transaction Delivery is for delivering a withstanding order at certain warehouse. Transaction Payment is for a given customer paying a withstanding amount of credit. Transaction OrderStatus is for inspecting certain orders and the associated order lines. Transaction StockLevel is for inspecting stocks at certain warehouse and the withstanding orders at this warehouse.