Synthesizing Precise and Useful Commutativity Conditions

Abstract

Reasoning about commutativity between data-structure operations is an important problem with many applications. In the sequential setting, commutativity can be used to reason about the correctness of refactoring, compiler transformations, and identify instances of non-determinism. In parallel contexts, commutativity dates back to the database (Weihl in IEEE Trans Comput 37(12):1488–1505, 1988) and compilers (Rinard and Diniz in ACM Trans Program Lang Syst 19(6):942–991, 1997) communities and, more recently, appears in optimistic parallelization (Herlihy and Koskinen in Proceedings of the 13th ACM SIGPLAN symposium on principles and practice of parallel programming, 2008), dynamic concurrency (Tripp et al. in Proceedings of the 33rd ACM SIGPLAN conference on programming language design and implementation, PLDI ’12, New York, NY, USA, ACM, pp 145–156, 2012; Dimitrov et al. in Proceedings of the 35th ACM SIGPLAN conference on programming language design and implementation, 2014), scalable systems (Clements et al. in ACM Trans Comput Syst 32(4):10, 2015) and even smart contracts (Dickerson et al. in Proceedings of the ACM symposium on principles of distributed computing, PODC ’17, New York, NY, USA, ACM, pp 303–312, 2017). There have been research results on automatic generation of commutativity conditions, yet we are unaware of any fully automated technique to generate conditions that are both sound and effective. We have designed such a technique, driven by an algorithm that iteratively refines a conservative approximation of the commutativity (and non-commutativity) condition for a pair of methods into an increasingly precise version. The algorithm terminates if/when the entire state space has been considered, and can be aborted at any time to obtain a partial yet sound commutativity condition. We have generalized our work to left-/right-movers (Lipton in Commun ACM 8(12):717–721, 1975) and proved relative completeness. We describe aspects of our technique that lead to useful commutativity conditions, including how predicates are selected during refinement and heuristics that impact the output shape of the condition. We have implemented our technique in a prototype open-source tool Servois. Our algorithm produces quantifier-free queries that are dispatched to a back-end SMT solver. We evaluate Servois first by synthesizing commutativity conditions for a range of data structures including Set, HashTable, Accumulator, Counter, and Stack. We then show several applications of our work including reasoning about memories and locks, finding vulnerabilities in Ethereum smart contracts, improving transactional memory performance, distributed applications, code refactoring, verification, and synthesis.

1 Introduction

Reasoning about the conditions under which data-structure operations commute is an important problem. The ability to derive sound yet effective commutativity conditions can improve correctness of sequential programs, eg in validating refactoring transformations like code motion [16], and further unlocks the potential of multicore architectures, including parallelizing compilers [31, 38], speculative execution (e.g. transactional memory [19]), peephole partial-order reduction [41], futures, etc. In recent years, another important application domain has emerged: Ethereum [15] smart contracts. Efficient execution of such contracts hinges on exploiting their commutativity [11] and block-wise concurrency can lead to vulnerabilities [32]. Intuitively, commutativity is an important property because linearizable data-structure operations that commute can be executed concurrently: their effects do not interfere with each other in an observable way. When using a linearizable HashTable, for example, knowledge that put(x,‘a’) commutes with get(y) provided that $\texttt {x}\ne \texttt {y}$ enables significant parallelization opportunities. Indeed, it’s important for the commutativity condition to be sufficiently granular so that parallelism can be exploited effectively [9]. At the same time, to make safe use of a commutativity condition, it must be sound [24, 25]. Achieving both of these goals using manual reasoning is burdensome and error prone.

In light of that, researchers have investigated ways of verifying user-provided commutativity conditions [23] as well as synthesizing such conditions automatically, e.g. based on random interpretation [2], profiling [37] or sampling [18]. None of these approaches, however, meet the goal of computing a commutativity condition that is both sound and granular in a fully automated manner.

In this paper, we present a refinement-based technique for synthesizing commutativity conditions. Our technique builds on well-known

descriptions and representations of abstract data types (ADTs) in terms of logical specifications [6, 14, 17, 20, 27, 29] denoted $({ Pre}_{m},{ Post}_{m})$ for each method m. Our algorithm iteratively relaxes under-approximations of the commutativity and non-commutativity conditions of methods m and n, starting from false, into increasingly precise versions. At each step, we conjunctively subdivide the symbolic state space into regions, searching for areas where m and n commute and where they don’t. Counterexamples to both the positive side and the negative side are used in the next symbolic subdivision. Throughout this recursive process, we accumulate the commutativity condition as a growing disjunction of these regions. The output of our procedure is a logical formula $\varphi _m^n$ which specifies when method m commutes with method n. We have proven that the algorithm is sound, and can also be aborted at any time to obtain a partial, yet useful [19, 37], commutativity condition. We show that, under certain conditions, termination is guaranteed (relative completeness).

We address several challenges that arise in using an iterative refinement approach to generating precise and useful commutativity conditions. First, we show how to pose the commutativity question in a way that does not introduce additional quantifiers. We also show how to generate the predicate vocabulary for expressing the condition $\varphi _m^n$, as well as how to choose the predicates throughout the refinement loop. A further question that we address is how predicate selection impacts the conciseness and readability of the generated commutativity conditions. We next show that our algorithm can be generalized to left-/right-movers [28], a more precise version of commutativity.

We have implemented our approach as the Servois tool, whose code and documentation are available online [33]. Servois is built on top of the CVC4 SMT solver [7]. We first evaluate Servois through by generating commutativity conditions for a collection of popular data structures, including Set, HashTable, Accumulator, Counter, and Stack. The conditions typically combine multiple theories, such as sets, integers, arrays, etc. We show the conditions to be comparable in granularity to manually specified conditions [23].

We then explore a range of applications of how the commutativity conditions we use can be employed in numerous contexts. We consider reasoning about memories and locks. We also consider BlockKing [32], an Ethereum smart contract, with its known vulnerability. We demonstrate how a developer can be guided by Servois to create a more robust implementation. Furthermore, we describe how Servois can aid transactional memory, distributed systems, code refactoring, verification and synthesis.

Contributions In summary, this paper makes the following contributions:

• The first sound and precise technique to automatically generate commutativity conditions (Sect. 5).

• Proofs of soundness and relative completeness (Sect. 5).

• A generalization to left- and right-movers (Sect. 6).

• An implementation that takes an abstract code specification and automatically generates commutativity conditions using an SMT solver (Sect. 7).

• A novel technique for selecting refinement predicates that improves scalability and the simplicity of the generated formulae (Sect. 7).

• Demonstrated efficacy for several key data structures (Sect. 8).

• Application of our work to a variety of contexts (Sect. 9).

An earlier version of this work was previously published. [3].

Related Work The closest to our contribution in this paper is a recent technique by Gehr et al. [18] for learning, or inference, of commutativity conditions based on black-box sampling. They draw concrete arguments, extract relevant predicates from the sampled set of examples, and then search for a formula over the predicates. There are no soundness or completeness guarantees.

Both Aleen and Clark [2] and Tripp et al. [37] identify sequences of actions that commute (via random interpretation and dynamic analysis, respectively). However, neither technique yields an explicit commutativity condition. Kulkarni et al. [26] point out that varying degrees of commutativity specification precision are useful. Kim and Rinard [23] use Jahob to verify manually specified commutativity conditions of several different linked data structures. Commutativity is also of interest in the feature-oriented programming commutativity. Chechik et al. [8] discuss how to identify non-commutativity by examining so-called feature trees. If two operations in this tree may write to the same shared variables, the authors conservatively conclude that these operations are non-commutative. Commutativity specifications are also found in dynamic analysis techniques [12]. More distantly related is work on synthesis of programs [35] and of synchronization [39, 40].

2 Example

Specifying commutativity conditions is generally nontrivial and it is easy to miss subtle corner cases. Additionally, it has to be done pairwise for all methods. For ease of illustration, we will focus on the relatively simple Set ADT, whose state consists of a single set $S$ that stores an unordered collection of unique elements. Let us consider one pair of operations: (i) contains($x$)/bool, a side-effect-free check whether the element $x$ is in $S$; and (ii) add($y$)/bool adds $y$ to $S$ if it is not already there and returns true, or otherwise returns false. add and contains clearly commute if they refer to different elements in the set. There is another case that is less obvious: add and contains commute if they refer to the same element e, as long as in the pre-state $e \in S$. In this case, under both orders of execution, add and contains leave the set unmodified and return false and true, respectively. The algorithm we describe in this paper completes within a few seconds, producing a precise logical formula $\varphi$ that captures this commutativity condition, i.e. the disjunction of the two cases above: $\varphi \equiv x\ne y\vee (x= y\wedge x\in S)$. The algorithm also generates the conditions under which the methods do not commute: $\tilde{\varphi }\equiv x=y\wedge x\notin S$. These are precise, since $\varphi$ is the negation of $\tilde{\varphi }$.

A more complicated commutativity condition is generated by our tool Servoisin 1.4s for Ethereum smart contract BlockKing. This contract has a method called enter($\textsf {val}_{1},\textsf {sendr}_{1},\textsf {bk}_{1}$...) (Fig. 5, Sect. 8) which does not commute with itself enter($\textsf {val}_{2},\textsf {sendr}_{2},\textsf {bk}_{2}$...) iff:

$$\begin{aligned} \begin{array}{c} \bigvee \left\{ \begin{array}{l} \textsf {val}_{1}\ge 50 \wedge \textsf {val}_{2}\ge 50 \wedge \textsf {sendr}_{1}\ne \textsf {sendr}_{2}\\ \textsf {val}_{1}\ge 50 \wedge \textsf {val}_{2}\ge 50 \wedge \textsf {sendr}_{1}= \textsf {sendr}_{2}\wedge \textsf {val}_{1}\ne \textsf {val}_{2}\\ \textsf {val}_{1}\ge 50 \wedge \textsf {val}_{2}\ge 50 \wedge \textsf {sendr}_{1}= \textsf {sendr}_{2}\wedge \textsf {val}_{1}= \textsf {val}_{2}\wedge \textsf {bk}_{1}\ne \textsf {bk}_{2}\\ \end{array} \right. \end{array} \end{aligned}$$

This disjunction enumerates the non-commutativity cases and, as discussed in Sect. 8, directly identifies a vulnerability.

Capturing precise conditions such as these by hand, and doing so for many pairs of operations, is tedious and error prone. This paper instead presents a way to automate this. Our algorithm recursively subdivides the state space via predicates until, at the base case, regions are found that are either entirely commutative or else entirely non-commutative. Returning to our Set example, the conditions we incrementally generate are denoted $\varphi$ and $\tilde{\varphi }$, respectively. The following diagram illustrates how our algorithm proceeds to generate the commutativity conditions for add and contains (abbreviated as m and n).

In this diagram, each subsequent panel depicts a partitioning of the state space into regions of commutativity ($\varphi$) or non-commutativity ($\tilde{\varphi }$). The counterexamples $\chi _\text {c},\chi _\text {nc}$ give values for the arguments x, y and the current state $S$.

We denote by H the logical formula that describes the current state space at a given recursive call. We begin with $H_0=\textsf {true}$, $\varphi =\textsf {false}$, and $\tilde{\varphi }=\textsf {false}$. There are three cases for a given H: (i) H describes a precondition for m and n in which they always commute; (ii) H describes a precondition for m and n in which they never commute; or (iii) neither of the above. The latter case drives the algorithm to subdivide the region by choosing a new predicate.

We now detail the run of this refinement loop on our earlier Set example. We elaborate on the other challenges that arise in later sections. At each step of the algorithm, we determine which case we are in via carefully designed validity queries to an SMT solver (Sect. 4).

For $H_0$, it returns the commutativity counterexample: $\chi _\text {c}= \{ x=0,y=0,S=\emptyset \}$ as well as the non-commutativity counterexample $\chi _\text {nc}= \{ x=0,y=1,S=\{0\} \}$. Since, therefore, $H_0=\textsf {true}$ is neither a commutativity nor a non-commutativity condition, we must refine $H_0$ into regions (or stronger conditions). In particular, we would like to perform a useful subdivision: Divide $H_0$ into an $H_1$ that allows $\chi _\text {c}$ but disallows $\chi _\text {nc}$, and an $H'_1$ that allows $\chi _\text {nc}$ but not $\chi _\text {c}$. So we must choose a predicate p (from a suitable set of predicates $\mathcal{P}$, discussed later), such that $H_0 \wedge p \Rightarrow \chi _\text {c}$ while $H_0 \wedge \lnot p \Rightarrow \chi _\text {nc}$ (or vice versa).

The predicate $x=y$ satisfies this property. The algorithm then makes the next two recursive calls, adding p as a conjunct to H, as shown in the second column of the diagram above: one with $H_1 \equiv \textsf {true}\wedge x=y$ and one with $H'_1 \equiv \textsf {true}\wedge x\ne y$.

Taking the $H'_1$ case, our algorithm makes another SMT query and finds that $x\ne y$ implies that add always commutes with contains. At this point, it can update the commutativity condition $\varphi$, letting $\varphi {:}{=} \varphi \vee H'_1$, adding this $H'_1$ region to the growing disjunction.

On the other hand, $H_1$ is neither a sufficient commutativity nor a sufficient non-commutativity condition, and so our algorithm, again, produces the respective counterexamples: $\chi _\text {c}= \{ x=0,y=0,S=\emptyset \}$ and $\chi _\text {nc}= \{ x=0,y=0,S=\{0\} \}$. In this case, our algorithm selects the predicate $x\in S$, and makes two further recursive calls: one with $H_2 \equiv x=y\wedge x\in S$ and another with $H'_2 \equiv x=y\wedge x\notin S$. It now finds that $H_2$ is a sufficiently strong precondition for commutativity, while $H'_2$ is a strong enough precondition for non-commutativity. Consequently, $H_2$ is added as a new conjunct to $\varphi$, yielding $\varphi \equiv x\ne y \vee (x=y\wedge x\in S)$. Similarly, $\tilde{\varphi }$ is updated to be: $\tilde{\varphi }\equiv (x=y\wedge x\notin S)$.

No further recursive calls are made so the algorithm terminates and we have obtained a precise (complete) commutativity/non-commutativity specification: $\varphi \vee \tilde{\varphi }$ is valid (Lemma 1).

Challenges and Outline While the algorithm outlined so far is a relatively standard refinement, the above generated conditions were not immediate. We now discuss challenges involved in generating sound and useful conditions.

(Section 4) A first question is how to pose the underlying commutativity queries for each subsequent H in a way that avoids the introduction of additional quantifiers, so that we can remain in fragments for which the solver has complete decision procedures. Thus, if the data structure can be encoded using theories that are decidable, then the queries we pose to the SMT solver are guaranteed to be decidable as well. ${ Pre}_{m}/{ Post}_{m}$ specifications that are partial would introduce quantifier alternation, but we show how this can be avoided by, instead, transforming them into total specifications.

(Section 5) We have proved that our algorithm is sound even if aborted or the ADT description involves undecidable theories. We further show that termination implies completeness, and specify broad conditions that imply termination.

(Section 6) We have generalized our theory and algorithm to be able to synthesis conditions for left- and right-movers [28], an asymmetric version of commutativity.

(Section 7) Another challenge is to prioritize predicates during the refinement loop. This choice impacts not only the algorithm’s performance, but also the quality/conciseness of the resulting conditions. Our choice of next predicate p is governed by two requirements. First, for progress, p/$\lnot p$ must eliminate the counterexamples to commutativity/non-commutativity due to the last iteration . This may still leave multiple choices, and we propose two heuristics—called simple and poke—with different trade-offs to break ties.

(Section 8) We next provide an evaluation on a range of popular data structures including a Counter, Stack, HashTable, Accumulator, and Set.

(Section 9) We show several applications of our work, including memories and lock-based synchronization, a case study on the security of an Ethereum smart contract, and examples of how Servois commutativity conditions can be employed in transactional memory, distributed systems, code refactoring, verification, and code synthesis.

3 Preliminaries

States, Actions, Methods We will work with a state space $\Sigma$, with decidable equality and a set of actions A. For each $\alpha \in A$, we have a transition function . We denote a single transition as $\sigma \xrightarrow {\alpha }\sigma '$. We assume that each such action arc completes in finite time. Let . We say that two actions $\alpha _1$ and $\alpha _2$commute [12], denoted $\alpha _1 \bowtie \alpha _2$, provided that . Note that $\bowtie$ is with respect to . Our formalism, implementation, and evaluation all extend to a more fine-grained notion of commutativity: an asymmetric version called left-movers and right-movers [28], where a method commutes in one direction and not the other. We return to this in Sect. 6. Also, in our evaluation (Sect. 8) we show left-/right-mover conditions that were generated by our implementation.

An action $\alpha \in A$ is of the form $m(\bar{x})/\bar{r}$, where m, $\bar{x}$ and $\bar{r}$ are called a method, arguments and return values respectively. As a convention, for actions corresponding to a method n, we use $\bar{y}$ for arguments and $\bar{s}$ for return values. The set of methods will be finite, inducing a finite partitioning of A. We refer to an action, say $m(\bar{a})/\bar{v}$, as corresponding to method m (where $\bar{a}$ and $\bar{v}$ are vectors of values). The set of actions corresponding to a method m, denoted $A_m$, might be infinite as arguments and return values may be from an infinite domain.

Definition 1

Methods m and n commute, denoted $m\ \bowtie \ n$ provided that $\forall \bar{x}\ \bar{y}\ \bar{r}\ \bar{s}.\;\; m(\bar{x})/\bar{r}\bowtie n(\bar{y})/\bar{s}$.

The quantification $\forall \bar{x}\bar{r}$ above means $\forall m(\bar{x})/\bar{r}\in A_m$, i.e., all vectors of arguments and return values that constitute an action in $A_m$.

Abstract Specifications We symbolically describe the actions of a method m as pre-condition ${ Pre}_{m}$ and post-condition ${ Post}_{m}$. Pre-conditions are logical formulae over method arguments and the initial state: $[\![ { Pre}_{m} ]\!] : \bar{x}\rightarrow \Sigma \rightarrow \mathbb {B}$. Post-conditions are over method arguments, and return values, initial state and final state: $[\![ { Post}_{m} ]\!] : \bar{x}\rightarrow \bar{r}\rightarrow \Sigma \rightarrow \Sigma \rightarrow \mathbb {B}$. Given $({ Pre}_{m},{ Post}_{m})$ for every method m, we define a transition system such that $\sigma \xrightarrow {m(\bar{a})/\bar{v}} \sigma '$iff $[\![ { Pre}_{m} ]\!]\ \bar{a}\ \sigma$ and $[\![ { Post}_{m} ]\!]\ \bar{a}\ \bar{v}\ \sigma \ \sigma '$.

Since our approach works on deterministic transition systems, we have implemented an SMT-based check (Sect. 8) that ensures the input transition system is deterministic. Deterministic specifications were sufficient in our examples. This is unsurprising given the inherent difficulty of creating efficient concurrent implementations of nondeterministic operations, whose effects are hard to characterize. Reducing nondeterministic data-structure methods to deterministic ones through symbolic partial determinization [1, 10] is left as future work.

Logical Commutativity Formulae We will generate a commutativity condition for methods m and n as logical formulae over initial states and the arguments/return values of the methods. We denote a logical commutativity formula as $\varphi$ and assume a decidable interpretation of formulae, i.e. that $[\![ \varphi ]\!] : (\sigma ,\bar{x},\bar{y},\bar{r},\bar{s}) \rightarrow \mathbb {B}$. (We tuple the arguments for brevity.) The first argument is the initial state. Commutativity post- and mid-conditions can also be written [23] but here, for simplicity, we focus on commutativity pre-conditions. We may write $[\![ \varphi ]\!]$ as $\varphi$ when it is clear from context that $\varphi$ is meant to be interpreted.

We say that $\varphi _m^n$ is a sound commutativity condition, and $\hat{\varphi }_m^n$ a sound non-commutativity condition resp., for m and n provided that

$$\begin{aligned} \begin{array}{l} \forall \sigma \bar{x}\bar{y}\bar{r}\bar{s}.\ [\![ \varphi _m^n ]\!]\ \sigma \ \bar{x}\ \bar{y}\ \bar{r}\ \bar{s}\Rightarrow m(\bar{x})/\bar{r}\ \bowtie \ n(\bar{y})/\bar{s}, \text { and}\\ \forall \sigma \bar{x}\bar{y}\bar{r}\bar{s}.\ [\![ \hat{\varphi }_m^n ]\!]\ \sigma \ \bar{x}\ \bar{y}\ \bar{r}\ \bar{s}\Rightarrow \lnot (m(\bar{x})/\bar{r}\ \bowtie \ n(\bar{y})/\bar{s}), \text { resp.} \end{array} \end{aligned}$$

4 Commutativity Without Quantifier Alternation

Definition 1 requires showing equivalence between different compositions of potentially partial functions. That is, if and only if:

Even when the transition relation can be expressed in a decidable theory, because of $\forall \exists$ quantifier alternation in the above encoding (which is undecidable in general), any procedure requiring such a check would be incomplete. SMT solvers are particularly poor at handling such constraints.

We observe that when the transition system is specified as $Pre_m$ and $Post_m$ conditions, and the $Post_m$ condition is consistent with $Pre_m$, then it is possible to avoid quantifier alternation. By consistent we mean that whenever $Pre_m$ holds, there is always some state and return value for which $Post_m$ holds (i.e. for which the procedure does not abort).

$$\begin{aligned} \forall \bar{a}\ \sigma .\;\;\; { Pre}_{m}(\bar{a},\sigma ) = \textsf {true}\;\Rightarrow \; \exists \sigma '\ \bar{r}.\ { Post}_{m}(\bar{a},\bar{r},\sigma ,\sigma '). \end{aligned}$$

That is, the procedure terminates for every ${ Pre}_{m}$, which holds in particular for all of the specifications in the examples we considered (see Sect. 8). This allows us to perform a simple transformation on transition systems to a lifted domain, and enforce a definition of commutativity in the lifted domain $m\ \hat{\bowtie }\ n$ that is equivalent to Definition 1. This new definition (inspired by “type lifting”) requires only universal quantification, and as such, is better suited to SMT-backed algorithms (Sect. 5).

Definition 2

(Lifted transition function) For , we lift $\mathfrak {T}$ to where $\hat{\Sigma }= \Sigma \cup \{ \textsf {err}{} \}$, $\textsf {err}{} \notin \Sigma$, and , as:

Intuitively, wraps so that $\textsf {err}{}$ loops back to $\textsf {err}{}$, and the (potentially partial) is made to be total by mapping elements to $\textsf {err}{}$ when they are undefined in . It is not necessary to lift the actions (or, indeed, the methods), but only the states and transition function. Once lifted, for a given state $\hat{\sigma }_0$, the question of some successor state becomes equivalent to all successor states because there is exactly one successor state.

Abstraction Pre-/post-conditions $({ Pre}_{m},{ Post}_{m})$ are suitable for specifications of potentially partial transition systems. One can translate these into a new pair $(\widehat{{ Pre}}_{m},\widehat{{ Post}}_{m})$ that induces a corresponding lifted transition system that is total and remains deterministic. These lifted specifications have types over lifted state spaces: $[\![ \widehat{{ Pre}}_{m} ]\!] : \bar{x}\rightarrow \hat{\Sigma }\rightarrow \mathbb {B}$ and $[\![ \widehat{{ Post}}_{m} ]\!] : \bar{x}\rightarrow \bar{r}\rightarrow \hat{\Sigma }\rightarrow \hat{\Sigma }\rightarrow \mathbb {B}$. Our implementation performs this lifting via translation denoted Lift from $({ Pre}_{m},{ Post}_{m})$ to:

$$\begin{aligned} \begin{array}{rl} \widehat{{ Pre}}_{m}(\bar{x},\hat{\sigma }) &{}\equiv \;\;\textsf {true}\\ \widehat{{ Post}}_{m}(\bar{x},\bar{r},\hat{\sigma },\hat{\sigma }') &{}\equiv \;\bigvee {\left\{ \begin{array}{ll} \hat{\sigma }=\textsf {err}{} \wedge \hat{\sigma }'=\textsf {err}{}\\ \hat{\sigma }\ne \textsf {err}{} \wedge { Pre}_{m}(\bar{x},\hat{\sigma }) \wedge \hat{\sigma }'\ne \textsf {err}{} \wedge { Post}_{m}(\bar{x},\bar{r},\hat{\sigma },\hat{\sigma }')\\ \hat{\sigma }\ne \textsf {err}{} \wedge \lnot { Pre}_{m}(\bar{x},\hat{\sigma }) \wedge \hat{\sigma }'=\textsf {err}{} \end{array}\right. } \end{array} \end{aligned}$$

(For simplicity of presentation, we abuse notation, giving $\hat{\sigma }$ as an argument to ${ Pre}_{m}$, etc.) It is easy to see that the lifted transition system induced by this translation () is of the form given in Definition 2. Later, we show that our tool transforms a counter specification (Fig. 2) into an an equivalent lifted version that is total (Fig. 3).

We use the notation $\hat{\bowtie }$ to mean $\bowtie$ but over lifted transition system $\hat{\mathfrak {T}}$. Since $\hat{\bowtie }$ is over total, determinsitic transition functions, $\alpha _1\ \hat{\bowtie }\ \alpha _2$ is equivalent to:

(1)

The equivalence above is in terms of state equality. Importantly, this is a universally quantified formula that translates to a ground satisfiability check in an SMT solver (modulo the theories used to model the data structure). In our refinement algorithm (Sect. 5), we will use this format to check whether candidate logical formulae describe commutative subregions.

5 Iterative Refinement

We now present an iterative refinement strategy that, when given a lifted abstract transition system, generates the conditions for commutativity and non-commutativity. We then discuss soundness and relative completeness and, in Sects. 7 and 8, challenges in generating precise and useful commutativity conditions.

The refinement algorithm symbolically searches the state space for regions where the operations commute (or do not commute) in a conjunctive manner, adding on one predicate at a time. We add each subregion H (described conjunctively) in which commutativity always holds to a growing disjunctive description of the commutativity condition $\varphi$, and each subregion H in which commutativity never holds to a growing disjunctive description of the non-commutativity condition $\tilde{\varphi }$.

Fig. 1

Algorithm for generating commutativity $\varphi$ and non-commutativity $\tilde{\varphi }$

The algorithm in Fig. 1 begins by setting $\varphi =\textsf {false}$ and $\tilde{\varphi }=\textsf {false}$. Refine begins a symbolic binary search through the state space H, starting from the entire state: $H=\textsf {true}$. It also may use a collection of predicates $\mathcal{P}$ (discussed later). At each iteration, Refine checks whether the current H represents a region of space for which m and n always commute: $H \Rightarrow m\ \hat{\bowtie }\ n$ (described below). If so, H can be disjunctively added to $\varphi$. It may, instead be the case that H represents a region of space for which m and n never commute: . If so, H can be disjunctively added to $\tilde{\varphi }$. If neither of these cases hold, we have two counterexamples. $\chi _\text {c}$ is the counterexample to commutativity, returned if the validity check on Line 2 fails. $\chi _\text {nc}$ is the counterexample to non-commutativity, returned if the validity check on Line 4 fails.

We now need to subdivide H into two regions. This is accomplished by selecting a new predicate p via the Choose method. For now, let the method Choose and the choice of predicate vocabulary $\mathcal{P}$ be parametric. Refine is sound regardless of the behavior of Choose. Below we give the conditions on Choose that ensure relative completeness, and in Sect. 8 we discuss our particular strategy. Regardless of what p is returned by Choose, two recursive calls are made to Refine, one with argument $H \wedge p$, and the other with argument $H\wedge \lnot p$. Since we branch on each predicate, the algorithm is exponential in the number of predicates in the worst case. In Sect. 7 we discuss prioritizing predicates to make this practical in practice.

The refinement algorithm generates commutativity conditions in disjunctive normal form. Hence, any finite logical formula can be represented. This logical language is more expressive than previous commutativity logics that, because they were designed for run-time purposes, were restricted to conjunctions of inequalities [26] and boolean combinations of predicates over finite domains [12].

Checking a Candidate $H_m^n$. Our algorithm involves checking whether $(H_m^n \Rightarrow m\ \hat{\bowtie }\ n)$ or . As shown in Sect. 4, we can check whether $H_m^n$ specifies conditions under which $m\ \bowtie \ n$ via an SMT query that does not introduce quantifier alternation. For brevity, we define:

$$\begin{aligned} \begin{array}{l}\textsf {valid}(H_m^n \;\Rightarrow \;m\ \hat{\bowtie }\ n) \,\equiv \, \textsf {valid} \left( \begin{array}{l} \forall \hat{\sigma }_0\ \bar{x}\ \bar{y}\ \bar{r}\ \bar{s}.\;\;\; H_m^n(\hat{\sigma }_0,\bar{x},\bar{y},\bar{r},\bar{s}) \;\Rightarrow \; \\ \;\;\;\;\; m(\bar{x})/\bar{r}\;\;n(\bar{y})/\bar{s}\;\;\hat{\sigma }_0 = n(\bar{y})/\bar{s}\;\;m(\bar{x})/\bar{r}\;\;\hat{\sigma }_0 \end{array} \right) \end{array} \end{aligned}$$

Above we assume as a black box an SMT solver providing valid. Here we have lifted the universal quantification within $\hat{\bowtie }$ outside the implication.

We can similarly check whether $H_m^n$ is a condition under which m and n do not commute. First, we define negative analogs of commutativity:

We thus define a check for when $\varphi _m^n$ is a non-commutativity condition with:

Theorem 1

(Soundness) For each $\text {Refine}^m_n$ iteration: $\varphi \Rightarrow m\ \hat{\bowtie }\ n$ and .

Proof

We focus on the commutativity condition $\varphi$ case; $\tilde{\varphi }$ is analogous. Initially, $\varphi =\textsf {false}$ is a sound condition for when commutativity holds. The $\text {Refine}^m_n$ algorithm proceeds by iteratively updating $\varphi$, constructing a DNF formula of the following shape:

$$\begin{aligned} \varphi = \begin{array}{l} \textsf {false}\vee (p^0_0 \wedge \cdots \wedge p_{N_0}^0) \vee \cdots \vee (p^M_0 \wedge \cdots \wedge p_{N_M}^M) \end{array} \end{aligned}$$

where there are some M disjuncts, each consisting of some $N_i$ (for $i\in [1,M]$) predicate conjuncts. For soundness, it suffices to show that each disjunct’s conjunction is a valid commutativity condition. Fix one such conjunction $H=p_0\wedge \cdots \wedge p_{N_i}$. This conjunction is accumulated as the first parameter on the $\text {Refine}^m_n$ call stack, in the recursive call made on Lines 9 and 10. $\varphi$ is only updated on Line 3 and it does so by adding this new conjunction H. However, the addition of H is guarded by $\textsf {valid}(H \Rightarrow m\ \hat{\bowtie }\ n)$ on Line 2 and thus each H must be a sound commutativity condition. $\square$

Because all additions to the (non)commutativity conditions are immediately proceeded by a valid check, soundness depends only on simple local condition rather than a complicated invariant. Note also that soundness holds regardless of what Choose returns and even when the theories used to model the underlying data-structure are incomplete. Next we show termination implies completeness:

Lemma 1

If Refine$^m_n$ terminates, then $\varphi \vee \tilde{\varphi }$.

Proof

The recursive calls of the Refine algorithm induce a binary tree T, where nodes are labeled by the conjunction of predicates. If Refine terminates, then T is finite, and each node is labeled with a finite conjunction $p_0 \wedge \cdots \wedge p_n$.

Claim The disjunction of all leaf node labels is valid. Proof By induction on the tree. Base case: a single-node tree has label $\textsf {true}$. Inductive case: for every new node created, labeled with a new conjunct $\ldots \wedge p$, there is a sibling node with label $\ldots \wedge \lnot p$.

Each leaf node of tree T, labeled with conjunction $\gamma$, arises from Refine reaching a base case where, by construction, the conjunction $\gamma$ is disjunctively added to either $\varphi$ or $\tilde{\varphi }$. Since Refine terminates, all conjunctions are added to either $\varphi$ or $\tilde{\varphi }$, and thus $\varphi \vee \tilde{\varphi }$ must be valid. $\square$

Theorem 2

(Conditions for termination) Refine$^m_n$ terminates if 1. (expressiveness) the state space $\Sigma$ is partitionable into a finite set of regions $\Sigma _1,\ldots ,\Sigma _N$, each described by a finite conjunction of predicates $\psi _i$, such that either $\psi _i\Rightarrow m\ \hat{\bowtie }\ n$ or ; and 2. (fairness) for every $p\in \mathcal{P}$, Choose eventually picks p (note that this does not imply that $\mathcal{P}$ is finite),

Proof

By contradiction. As in the proof for Lemma 1, we represent the algorithm’s execution as a binary tree T, induced by the recursive Refine calls, whose nodes are labeled by the conjunction of predicates (Lines 9 and 10 in Algorithm 1). Assume there exists an infinite path along T, and let its respective labels be $\pi = p_0, p_0\wedge p_1, p_0\wedge p_1\wedge p_2,\ldots$.

Claim There is no finite prefix of $\pi$ that contains all the predicates $\psi _i$. Proof Had there been such a prefix $\varpi$, by the expressiveness assumption the running condition H would satisfy one of the validity checks at lines 2 and 4 within, or immediately after, $\varpi$. This is because H would be equal to, or stronger than, the conjunction of the predicates $\psi _i$. This would have made $\pi$ finite, as $\pi$ is extended only if both of the validity checks fail, where we assume $\pi$ is infinite.

By the above claim, at least one of the predicates $\psi _i$ is not contained in any finite prefix of $\pi$. This contradicts the fairness assumption, whereby any predicate $p \in \mathcal{P}$ is chosen after finitely many Choose invocations (provided the algorithm hasn’t terminated). $\square$

Note that while these conditions ensure termination, the bound on the number of iterations depends on the predicate language and behavior of Choose.

6 Right-/Left-Movers

We now describe how the formalism and algorithm presented thus far can be extend to a more fine-grained notion of commutativity: an asymmetric version called left-movers and right-movers [28], where a method commutes in one direction and not the other.

Definition 3

(Right-mover [28]) We say that an action $\alpha _1$moves to the right of action $\alpha _2$ commute, denoted $\alpha _1 \triangleright \alpha _2$, provided that . For methods m and n,

$$\begin{aligned} m\ \triangleright \ n \;\;\equiv \;\; \forall \bar{x}\ \bar{y}\ \bar{r}\ \bar{s}.\;\; m(\bar{x})/\bar{r}\triangleright n(\bar{y})/\bar{s}\end{aligned}$$

Left-movers can be defined as right-movers, but with arguments swapped. A logical right-mover condition denoted ${\Psi }_m^n$ has the same type as a commutativity condition and, again $[\![ {\Psi }_m^n ]\!]$ denotes interpretations of ${\Psi }_m^n$. Moreover, we say that ${\Psi }_m^n$ is a right-mover condition for m and n provided that $\forall \sigma _0\ \bar{x}\ \bar{y}\ \bar{r}\ \bar{s}.\ [\![ {\Psi }_m^n ]\!]\ \sigma _0\ (m(\bar{x})/\bar{r})\ (n(\bar{y})/\bar{s}) = \textsf {true}\Rightarrow m\ \triangleright \ n$ and similar for a non-right-mover condition denoted $\tilde{{\Psi }}_m^n$.

We also extend right-movers to lifted transition systems, as in Sect. 4. We use $\hat{\triangleright }$ to mean $\triangleright$ but over lifted transition systems $\hat{\mathfrak {T}}$.

Checking whether ${{\Psi }_m^n} \Rightarrow m\ \hat{\triangleright }\ n$. After performing the lifting transformation, we again are able to reduce the question of whether a formula ${\Psi }_m^n$ is a right-mover condition to a validity check that does not introduce quantifier alternation.

Notice that this is a generalization of the validity check for commutativity.

Lemma 2

If $\textsf {valid}(H_m^n \Rightarrow m\ \hat{\triangleright }\ n)$ and $\textsf {valid}(H_m^n \Rightarrow n\ \hat{\triangleright }\ m)$ then $\textsf {valid}(H_m^n \Rightarrow m\ \bowtie \ n)$.

We define $\;^{\hat{\triangleright }}\!\text {Refine}^m_n$ to be the same algorithm as in Fig. 1, except that $\textsf {valid}(H_m^n \Rightarrow m\ \hat{\bowtie }\ n)$ is replaced with $\textsf {valid}(H_m^n \Rightarrow m\ \hat{\triangleright }\ n)$. Then,

Theorem 3

(Left-mover soundness) For each $\;^{\hat{\triangleright }}\!\text {Refine}^m_n$ iteration: ${\Psi }_m^n\Rightarrow m\ \hat{\triangleright }\ n$, and .

Proof

Similar to Theorem 1. $\square$

6.1 The Full Lay of the Land

Recall that commutativity implies both-moverness while non-commutativity implies either non-left-, non-right- or non-both-moverness. We use the following notation for the three subcases of a non-commutativity condition $\tilde{\varphi }$:

In some cases it may be helpful to distinguish these cases. Therefore, we now describe how to combine the $\;^{\hat{\triangleright }}\!\text {Refine}^m_n$ and $\;^{\hat{\triangleleft }}\!\text {Refine}^m_n$ algorithms so that we can fully identify all cases. Let us denote $\;^{\hat{\triangleright }}\!\text {Refine}_n^m(H,\mathcal{P})$ to be the algorithms above, starting from state space H and constructing/returning right-moverness/non-right-moverness pair $(\psi ,\psi ')$.

The above calls to Refine divide the state space into four quadrants. Properties and are all defined via conjunction. Meanwhile, the weaker non-commutativity $\tilde{\varphi }$ is defined with disjunction. While $\tilde{\varphi }$ maintains DNF form, the other formulas have lost it. This can be rectified through formula manipulation. Alternatively, one could explore modifications to the original Refine algorithm that query the state space at this more precise granularity. We leave this to future work.

7 The Servois Tool and Practical Considerations

We have developed the open-source tool Servois [34]. Servois uses CVC4 [7] as a backend SMT solver. It begins by parsing an input ADT specification and performing some pre-processing, discussed below. It subsequently implements Refine, Lift, predicate generation, and a method for selecting predicates (Choose) discussed below.

Input We use an input specification language building on YAML (which has parser and printer support for many programming languages) with SMTLIB as the logical language. This can be automatically generated relatively easily, thus enabling the integration with other tools [6, 14, 17, 20, 27, 29]. Specifically, the input is specified by the following:

• name: name of the object being modeled.

• state: a list of name, type where name is name of the fields, and type the SMTLIB type being used to model the corresponding field.

• states_equal: a SMT formula denoting when two states should be considered equal.

• methods: specification of the methods as pre and post conditions. Specifically, following things need to be specified for a method:

  • args: a list of name, type where name is name of an argument, and type the SMTLIB type being used to model the corresponding argument.

  • return: a list of name, type where name is name of a return value, and type the SMTLIB type being used to model the corresponding return value.

  • requires: a SMT formula denoting the precondition of the method.

  • ensures: a SMT formula denoting the postcondition of the method.

  • terms: optionally, terms that should be used to generate predicates.

Fig. 2

An example of the input ADT specification for Counter

An example input for the Counter ADT specification can be seen in Fig. 2. It was derived from the ${ Pre}_{}$ and ${ Post}_{}$ conditions used in earlier work [23]. The states of a transition system describing an ADT are encoded as list of variables (each as a name/type pair), and each method specification requires a list of argument types, return type, and ${ Pre}_{}$/${ Post}_{}$ conditions. Notice that the Counter specification (Fig. 2) involves methods that have preconditions (e.g. increment) and therefore, the specification is not total. Servois performs the Lift transformation¹ as described in Sect. 4. An example of Lift applied to Counter is in Fig. 3. Notice that the state space has been augmented with err and post-conditions of all methods now account for err. Moreover, states_equal has also been amended.

Fig. 3

An example of the ADT specification after lifting has been performed. (terms have been elided for lack of space.)

Predicate Generation (PGen) Next, Servois automatically generates the predicate language in addition to user-provided hints. If the predicate vocabulary is not sufficiently expressive, then the algorithm would not be able to converge on precise commutativity and non-commutativity conditions (Sect. 5). We generate predicates by using terms and operators that appear in the specification, and generating well-typed atoms not trivially true or false. For example, if size, 1, (size+1) are terms of sort $\mathbb {Z}$ that appear in the formula along with the predicates = and $\ge$, then we generate $(\texttt {size}=1), (\texttt {size} \ge 1)$, etc (a total of 18 predicates in this case). We filter out those that are trivial. As we demonstrate in Sect. 8, our predicate generation strategy works well in practice. Intuitively, ${ Pre}_{}$ and ${ Post}_{}$ formulas suffice to express the footprint of an operation. So the atoms comprising them are an effective vocabulary to express when operations do or do not interfere.

Predicate Selection (Choose) Even though the number of computed predicates is relatively small, since our algorithm is exponential in number of predicates it is essential to be able to identify relevant predicates for the algorithm. To this end, in addition to filtering trivial predicates, we prioritize predicates based on the two counterexamples generated by the validity checks in Refine. Predicates that distinguish between the given counter examples are tried first (call these distinguishing predicates). Choose must return a predicate such that $\chi _\text {c}\Rightarrow \; H \wedge p$ and $\chi _\text {nc}\Rightarrow \; H \wedge \lnot p$. This guarantees progress on both recursive calls. When combined with a heuristic to favor less complex atoms, this ensured timely termination on our examples. We refer to this as the simple heuristic.

Though this produced precise conditions, they were not always very concise, which is desirable for human understanding and the inspection purposes. We thus introduced a new heuristic which significantly improves the qualitative aspect of our algorithm. We found that doing a lookahead (recurse on each predicate one level deep) and computing the number of distinguishing predicates for the two branches as a good indicator of importance of the predicate. More precisely, we pick the predicate with lowest sum of remaining number of distinguishing predicates by the two calls. We call this strategy “poke.” As an aside, those familiar with decision tree learning might see a connection with the notion of entropy gain. This requires more calls to the SMT solver at each step, but it cuts down the total number of branches to be explored. Also, all individual queries were relatively simple for CVC4. The heuristic converges much faster to the relevant predicates, and produces smaller, concise conditions.

8 Evaluation

We applied Servois to Set, HashTable, Accumulator, Counter, and Stack. The generated commutativity conditions for these data structures typically combine multiple theories, such as sets, integers and arrays. We now discuss how we represented each of the data structures. All evaluation data is available on the Servois homepage [33].

• 1. Counter The Counter involves typical operations: increment, decrement, zero test and reset. The counter can be thought of as an integer that can take only non-negative values (the state is modeled in our language as one variable of sort Int, and non-negativity is enforced using preconditions). In particular, this breaks the assumption that a successor state always exists doesn’t hold (Axiom 1). We get around this assumption in our encoding by introducing an Err state as described in Sect. 3. Our abstract definition encodes this as pair of variables, one of sort Int (for contents), and other sort Bool (for Err ).

• 2. Accumulator This is a simple data structure which holds a natural number, initially zero. There are only two methods: add(int x), which increments internal state by x; and read(), which returns the internal value. We represent the internal state using a single variable of sort Int.

• 3. Set This is a Set data structure with four operations: add, remove, contains and getsize. We encode the state in SMT using a two variables with Set sort [4] and size as Int sort. The elements of the Set are of an uninterpreted sort. The operations are straightforward. add and remove each take one argument and return true or false. The return value is true if and only if the data structure is modified (e.g., add(x) returns true if x is not in the data structure before the call). contains and getsize do not modify the state of the data structure.

• 4. Hashtable We use the SMTLIB theories of arrays and finite sets to encode a Hashtable. The state is represented as a tuple $(\texttt {keys}, \texttt {H})$. $\texttt {keys}$ keeps track of the set of keys on which the Hashtable is currently defined, this is encoded as a set of an uninterpreted sort: $\text {(Set E)}$. The values corresponding to keys in the Hashtable is encoded using the array theory: H is an array from E to another uninterpreted sort for the values. $\texttt {get}$ takes a single argument of sort E, if it is not in keys it goes to an error state. Otherwise, it returns the value in the Hashtable. $\texttt {put}$ takes two arguments: a (key,value) pair and updates the Hashtable. Similar to Set, it returns true (resp. false) if the data structure is modified (resp. not modified). $\texttt {remove}$ takes a single argument, the key to be removed if it exists. Other methods are self-explanatory.

• 5. Stack We use an abstraction which tracks only the top two values and the size. We observe that stack operations push and pop only modify the top element. Thus for the purposes of commutativity conditions we are looking at the value of only top two elements are of importance, other that we check that size is the same. A subtle point here though is that even though top two values can be modified, we need to track up to four values since two pop calls can cause the third from top value to become part of the top two values.

Depending on the pair of methods, the number of predicates generated by PGen were as follows:

ADT	Predicates	After filtering
Counter	25–25	12–12
Accumulator	1–20	0–20
Set	17–55	17–34
HashTable	18–36	6–36
Stack	41–61	41–42

We did not provide any hints to the algorithm for this case study. On all our examples, the simple heuristic terminated with precise commutativity conditions. In Fig. 4, we give the number of solver queries and total time (in paren.) consumed by this heuristic. The experiments were run on a 2.53 GHz Intel Core 2 Duo machine with 8 GB RAM. The conditions in Fig. 4 are those generated by the poke heuristic, and interested reader may compare them with the simple heuristic in [5]. On the theoretical side, our Choose implementation is fair (satisfies condition 2 of Theorem 2, as Lines 9–10 of the algorithm remove from $\mathcal {P}$ the predicate being tried). From our experiments we conclude that our choice of predicates satisfies condition 1 of Theorem 2.

Evaluation of Various Abstract Data Structures Although our algorithm is sound, we manually validated the implementation of Servois by examining its output and comparing the generated commutativity conditions with those reported by prior studies. In the case of Accumulator and Counter, our commutativity conditions were identical to those given in [23]. For the Set data structure, the work of [23] used a less precise Set abstraction, so we instead validated against the conditions of [26]. As for HashTable, we validated that our conditions match those by Dimitrov et al. [12].

Fig. 4

Automatically generated commutativity conditions ($\varphi ^m_n$). Right-moverness ($\rhd$) conditions identical for a pair of methods denoted by $\bowtie$. Qs denotes number of SMT queries. Running time in seconds. Longer conditions have been truncated, see [5]

9 Applications

Commutativity has played a central role in a number of application domains. In this section we discuss use cases that emerge from our automated reasoning about commutativity, as performed by Servois.

9.1 Memory, Locks and Commutativity

We now apply Servois to the setting of memories and locks. We work with a set of variables $Vars$ (of uninterpreted sort) and a memory $\texttt {mem}: Vars \rightarrow \mathbb {Z}$. First, we consider the simple setting where there are two operations: $\texttt {read}(x)/v$ and $\texttt {write}(y)/w$, similar to a Hashtable but with fewer methods. Not surprisingly, Servois generated the commutativity conditions including the fact that write operations on the same variable commute provided that the value being written is the same.

Next, we introduce locks and mix them with memory. Let $\mathcal {L}_\bot$ be the type of locks. We use $\tau _{}$ to represent a lock value (e.g. a thread IDs) with a special distinct lock $\bot$ to indicate unlocked. Finally, we maintain a mapping $\texttt {locked}: Vars \rightarrow \mathcal {L}_\bot$ to indicate whether a given memory location is locked and, if so, by whom.

To represent these types and methods in Servois, we exploited the underlying SMT solver’s ability to declare sorts and to declare datatypes such as a Pair. Technically, $\texttt {locked}$ maps variables to a Pair, consisting of a boolean flag (for $\bot$) and a sort for thread IDs. We define methods $\texttt {lock}(\tau _{i},x)$ and $\texttt {unlock}(\tau _{i},x)$ which, respectively, represent thread $\tau _{i}$ locking and unlocking the variable x, following the usual semantics of locks. We then further define $\texttt {tryread}(\tau _{i},x)$ which attempts to read the value of x but can only do so if $\tau _{i}$ holds the lock and returns -1 otherwise. We similarly define $\texttt {trywrite}(\tau _{i},x,v)$.

For commutativity in this context, there are many different cases to consider. For example, when considering only $\texttt {tryread}$ and $\texttt {trywrite}$, Servois generated a commutativity condition that had 11 different cases. This cases include:

• 1. $\texttt {tryread} \bowtie \texttt {trywrite}$ when operating on different variables.

• 2. $\texttt {tryread} \bowtie \texttt {trywrite}$ when the value being written is the same as what’s already there.

• 3. $\texttt {tryread} \bowtie \texttt {trywrite}$ when it is the same thread, same variable, but the lock is not held. (In this case both the read and write will fail.)

• 4. $\texttt {tryread} \bowtie \texttt {trywrite}$ when they are different threads.

Running Servois, we also obtained commutativity conditions such as:

Method pair	Example commutativity case
$\texttt {tryread}\bowtie \texttt {tryread}$	always
$\texttt {trywrite}(x,\tau _{i}) \bowtie \texttt {lock}(y,\tau _{j})$	when $x \ne y$ and the lock for y is not held.
$\texttt {lock}(x,\tau _{i}) \bowtie \texttt {lock}(y,\tau _{j})$	whenever $x \ne y$.
$\texttt {lock}(x,\tau _{i}) \bowtie \texttt {lock}(y,\tau _{j})$	whenever $x=y$ and the lock is held by anyone, including a third party.
$\texttt {lock}(x,\tau _{i}) \bowtie \texttt {lock}(y,\tau _{j})$	whenever $x=y$ and the lock is unheld, but $\tau _{i}=\tau _{j}$.
$\texttt {lock}(x,\tau _{i}) \bowtie \texttt {unlock}(y,\tau _{j})$	whenever $x \ne y$.
$\texttt {lock}(x,\tau _{i}) \bowtie \texttt {unlock}(y,\tau _{j})$	whenever $\tau _{i}=\tau _{j}$ and $x = y$, but the lock is held by someone else.
$\texttt {lock}(x,\tau _{i}) \bowtie \texttt {unlock}(y,\tau _{j})$	for different threads with $x=y$, but it is already locked by $\tau _{i}$.
$\texttt {lock}(x,\tau _{i}) \bowtie \texttt {unlock}(y,\tau _{j})$	for different threads with $x=y$, but locked by a third party.

9.2 Ethereum Smart Contracts and BlockKing

We further validated our approach by examining a real-world situation in which non-commutativity opens the door for attacks that exploit interleavings. We examined “smart contracts”, which are programs written in the Solidity programming language [36] and executed on the Ethereum blockchain [15]. Eliding many details, smart contracts are like objects, and blockchain participants can invoke methods on these objects. Although the initial intuition is that smart contracts are executed sequentially, practitioners and academics [32] are increasingly realizing that the blockchain is a concurrent environment due to the fact the execution of one actor’s smart contract can be split across multiple blocks, with other actors’ smart contracts interleaved. Therefore, the execution model of the blockchain has been compared to that of concurrent objects [32]. Unfortunately, many smart contracts are not written with this in mind, and attackers can exploit interleavings to their benefit.

As an example, we study the BlockKing smart contract. Figure 5 provides a simplification of its description, as discussed in [32]. This is a simple game in which the players—each identified by an address $\textsf {sendr}_{}$—participate by making calls to BlockKing.enter(), sending money $\textsf {val}_{}$ to the contract. (The grey variables are external input that we have lifted to be parameters. $\textsf {bk}_{}$ reflects the caller’s current block number and $\textsf {rnd}_{}$ is the outcome of a random number generation, described shortly.) The variables on Line 1 are globals, writable in any call to enter. On Line 3 there is a trivial case when the caller hasn’t put enough value into the game, and the money is simply returned. Otherwise, the caller stores their address and value into the shared state. A random number is then generated and, since this requires complex algorithms, it is done via a remote procedure call to a third-party on Line 5, with a callback method provided on Line 7. If the randomly generated number is equal to a modulus of the current block number, then the caller is the winner, and warrior’s (caller’s) details are stored to king and kingBlock on Line 10.

Fig. 5

Simplified code for BlockKing in a C-like language

Since random number generation is done via an RPC, players’ invocations of enter can be interleaved. Moreover, these calls all write $\textsf {sendr}_{}$ and $\textsf {val}_{}$ to shared variables, so the RPC callback will always roll the dice for whomever most recently wrote to warriorBlock. An attacker can use this to leverage other players’ investments to increase his/her own chance to win.

We now explore how Servois can aid a programmer in developing a more secure implementation. We observe that, as in traditional parallel programming contexts, if smart contracts are commutative then these interleavings are not problematic. Otherwise, there is cause for concern. To this end, we translated the BlockKing game into Servois format (see Servois source code [34]). Servois took 1.4s (on machine with 2.4 GHz Intel Core i5 processor and 8 GB RAM) and yielded the following non-commutativity condition for two calls to enter:

This disjunction effectively enumerates cases under which they contract calls do not commute. Of particular note is the first disjunct. From this first disjunct, whenever $\textsf {sendr}_{1}\ne \textsf {sendr}_{2}$, the calls will not commute. Since in practice $\textsf {sendr}_{1}$ will always be different from $\textsf {sendr}_{2}$ (two different callers) and $\textsf {val}_{1}\ge 50 \wedge \textsf {val}_{2}\ge 50$ is the non-trivial case, the operations will almost never commute. This should be immediate cause for concern to the developer.

Fig. 6

Our fixed version of BlockKing in a C-like language

Fixed version of BlockKing. A commutative version of BlockKing would mean that there are no interleavings to be concerned about. Indeed, a simple way to improve commutativity is for each player to write their respective $\textsf {sendr}_{}$ and $\textsf {val}_{}$ to distinct shared state, perhaps via a hashtable keyed on $\textsf {sendr}_{}$. To this end, we created a new version enter_fixed, shown in Fig. 6. (YML versions of these two programs, blockking.yml and blockking_fixed.yml, can be found in our source code repository [34].) Servois generated the following non-commutativity condition after 3.5s.

In the above non-commutativity condition, $\textsf {md}$ is shorthand for modFun. In the first two disjuncts above, $\textsf {sendr}_{1}=\textsf {sendr}_{2}$ which is, again, a case that will not occur in practice. All that remains is the third disjunct where $\textsf {md}(\textsf {bk}_{2}) = \textsf {rnd}_{2}$ and $\textsf {md}(\textsf {bk}_{1}) = \textsf {rnd}_{1}$. This corresponds to the case where both players have won. In this case, it is acceptable for the operations to not commute, because whomever won more recently will store their address/block to the shared king/kingBlock.

In summary, if we assume that $\textsf {sendr}_{1}\ne \textsf {sendr}_{2}$, the non-commutativity of the original version is $\textsf {val}_{1}\ge 50 \vee \textsf {val}_{2}\ge 50$ (very strong). By contrast, the non-commutativity of the fixed version is $\textsf {val}_{1}\ge 50 \wedge \textsf {val}_{2}\ge 50 \wedge \textsf {md}(\textsf {bk}_{2}) = \textsf {rnd}_{2}\wedge \textsf {md}(\textsf {bk}_{1}) = \textsf {rnd}_{1}$. We have thus demonstrated that the commutativity (and non-commutativity) conditions generated by Servois can help developers understand the model of interference between two concurrent calls.

9.3 Transactional Memory

The output of Servois can be used for speculative concurrent execution, e.g. transactional memory. Specifically, transactional boosting [19] is a form of transactional memory in which transactions consist of operations on shared highly-concurrent objects rather than directly on a shared memory. This strategy permits conflict to be defined—based on commutativity—at the level of abstract data types rather than at the overly conservative level of memory read/write operations. It has been shown to improve performance [19]. Here is an example of an execution of two boosted transactions:

$$\begin{aligned} \begin{array}{l|llllll} \text {Thread 1}: &{} \texttt {begin} &{} v = sk.\textsf {pop}(); &{} &{} ht.\textsf {put}(5, v); &{} &{} \texttt {commit} \\ \hline \text {Thread 2}: &{} \texttt {begin} &{} &{} w = ht.\textsf {get}(6); &{} &{} \texttt {commit} \\ \end{array} \end{aligned}$$

The above transactions perform operations on a shared Stack sk and Hashtable ht, which each must be implemented as linearizable objects with no shared state beyond the state of the objects. Even though these are concurrent transactions, the boosting methodology permits concurrent operations on the same objects, provided that the operations commute. As we have seen in Sect. 8, these hashtable methods indeed commute because they are operating on distinct keys.

The impact of boosting on the performance of transactional memory critically depends on the quality and completeness of the specification, which controls the extent to which spurious rollbacks are avoided. Servois is unique among availably synthesis tools in its ability to (i) always generate commutativity conditions, even if not fully precise, for arbitrary data structures, and (ii) ensure the soundness of the generated conditions, so that none of the guarantees of the underlying transactional memory system is lost.

9.4 Testing for Interactions Between Code Blocks

The importance of representing concurrent data structures according to their guarantees has already been established by past studies, eg in the context of exposing impediments to loop parallelization [38]. Again here, as with transactional memory, there is the challenge of automatically coming up with a commutativity specification. The HawkEye approach is to emulate concrete-level reads and writes w.r.t. the abstract representation of a concurrent ADT implementation. This yields approximate commutativity conditions, whereas Servois enables an alternative that is more precise while still practical (see discussion above). As an illustrative example, consider concurrent calls to Counter’s decrement method. Servois is able to establish that these always commute, as show in Sect. 8, yet writing to the value field of the counter to decrement it would trigger a spurious conflict by HawkEye.

To show this, we extended our implementation of the Counter, to further support a write(v) operation, which directly wrote to the counter. Re-running Servois, we found that:

• $\textsf {incr} \bowtie \textsf {decr}$ as long as the counter was not 0 (as in the original Counter).

• $\textsf {incr} \bowtie \textsf {incr}$ in all cases (as in the original Counter).

• $\textsf {incr} \bowtie \textsf {write}$never.

• $\textsf {decr} \bowtie \textsf {write}$never.

• $\textsf {write} \bowtie \textsf {write}$ when both are writing the same value (as in a Memory).

9.5 Parallel and Distributed Systems

As the BlockKing example (Sect. 9.2) illustrates, a major aspect of reasoning about the correctness of parallel and distributed programs concerns the conditions under which concurrent execution of the code is safe. As long as these conditions meet the intentions of the developer, and are enforced at the implementation level via appropriate synchronization, concurrent execution is safe. From a formal standpoint, this amounts to commutativity checking.

Servois exposes a convenient interface for this type of reasoning. The ability to focus on operations of interest, using custom logical vocabularies, enables granular yet accurate reasoning about their interactions. Here is an example, adapted from Xiao et al. [43]:

Given two instances of the body of the foreach loop, Servois is able to report that commutativity is not generally guaranteed. Indeed, while simply searching for the maximal value is an operation that can be evaluated in a distributed fashion, using that value (x) to extract another column value (y) yields deterministic output only if that other value is the same across rows the share the maximal value.

9.6 Refactoring

A common use case in code maintenance and refactoring is to move statements [16]. That occurs, for example, when trying to increase reuse via method extraction; hoisting statements outside a loop structure for improved performance; or changing the order of statements to organize the code better. In all of these cases, there is the danger of introducing unintended side effects because of latent interactions between statements that have changed their relative position.

IDE-integrated refactoring tools often take care of the change itself, but without being able to (fully) reason about the correctness of the transformation. Ultimately it is up to the developer to approve the change (eg via a dialog that presents the before and after versions of the code).

An example follows:

It is safe to hoist Data x = map.get("x"); outside the loop given the knowledge that $\forall \texttt {e} \in \texttt {input}. \texttt {"X"} \ne \texttt {e}$. However, this is beyond what a standard compiler or refactoring tool is able to establish. Within this use case, Servois could suggest that $\texttt {"X"} \ne e$ is a sufficient condition for the hoisting operation, which the developer can then review and approve.

Servois is well positioned to integrate with IDE refactoring tools, in that it’s feasible to create reusable vocabularies of predicates for popular languages, libraries and data structures, and with these, have Servois perform resource-bounded reasoning when a refactoring request is made. The unique advantage of Servois, beyond features already mentioned above, is in its ability to always generate sound commutativity conditions, even if stopped before reaching a stable solution.

9.7 Verification and Test Case Generation

Testing and verification are yet another opportunity to apply Servois. Specifically, given an encoding of a data structure and its associated operations, the conditions that Servois computes for commutativity become a correctness checking objective. As a concrete example, Servois can integrate with dynamic analysis tools to guide checking of the implementation both under conditions where method calls are expected to commute and where they are expected to interfere.

Here is an illustrative example:

Per specification, two calls to PutIfAbsent commute either if the Maps are different or if the Entrys differ in their Key field or if the Values are the same. With this information given by Servois, a testing tool can check for the behavior when PutIfAbsent calls interfere. That would uncover a bug, whereby

yields a state where k is mapped to v2 rather than v1.

Integrations of this sort bridge the step down from specification to implementation. Servois synthesizes commutativity conditions at the specification level, which are discharged to a concrete-level checking tool for testing or verification against the implementation. Again in this use case, the ability to generate conditions within a limited time budget, and while reusing predicate vocabularies across verification tasks, makes Servois a practical alternative that is easy to integrate with algorithms for verification or testing.

9.8 Code Synthesis

An analogous use case to correctness checking with Servois operating at the specification level is code synthesis. In this scenario, the conditions computed by Servois are become the specification for synchronization synthesis.

Consider the following program:

The second part of this program (from Line 4 onward) is attempting to exploit the commutativity of put and put operating on different keys, represented by commutativity condition $\varphi _m^n$ used as a precondition. The synthesis question becomes: what implementation of placement ensures that $\texttt {k}_1 \ne \texttt {k}_2$?

Synthesis algorithms like that by Itzhaky et al. [22] can then be used to generate an admissible implementation of placement.

Synchronization synthesis need to be fully optimal, but (i) the synthesis algorithm should be reasonably efficient (not taking too long to complete), (ii) the synthesized synchronization should be sound, and finally (iii) the algorithm should be (close to) complete, not failing too often to synthesize synchronization. The Servois design, and guarantees, meet all three of these requirements.

10 Conclusions and Future Work

This paper demonstrates that it is possible to automatically generate sound and effective commutativity conditions, a task that has so far been done manually or without soundness. Our commutativity conditions are applicable in a variety of contexts including transactional boosting [19], open nested transactions [30], and other non-transactional concurrency paradigms such as race detection [12], parallelizing compilers [31, 38], and, as we show, robustness of Ethereum smart contracts [32]. It has been shown that understanding the commutativity of data-structure operations provides a key avenue to improved performance [9] or ease of verification [24, 25].

This work opens several avenues of future research. For instance, leveraging the internal state of the SMT solver (beyond counterexamples) in order to generate new predicates [21]; automatically building abstract representation or making inferences such as one we made for the stack example; and exploring strategies to compute commutativity conditions directly from the program’s code, without the need for an intermediate abstract representation [38]. Finally, it may be worth exploring how our approach of ensuring totality applies to other properties such as safety and liveness.