Monitoring Weak Consistency

Programming software applications that can deal with multiple clients at the same time, and possibly, with clients that connect at different sites in a network, relies on optimized concurrent or distributed objects which encapsulate lock-free shared memory access or message passing protocols into high-level abstract data types. Given the potentially-enormous amount of software that relies on these objects, it is important to maintain precise specifications and ensure that implementations adhere to their specifications.

One of the standard correctness criteria used in this context is linearizability (or strong consistency) [22], which ensures that the results of concurrently-executed invocations match the results of some serial execution of those same invocations. Ensuring such a criterion in a distributed context (when data is replicated at different sites in a network) is practically infeasible or even impossible [17, 19]. Therefore, various weak consistency criteria have been proposed like eventual consistency [23, 36], “session guarantees” like read-my-writes or monotonic-reads [35], causal consistency [25, 28], etc.

An axiomatic framework for formalizing such criteria has been proposed by Burckhardt et al. [9, 11]. Essentially, this extends the linearizability-based specification methodology with a dynamic visibility relation among operations, in addition to the standard dynamic happens-before and linearization relations. Permitting weaker visibility relations models outcomes in which an operation may not observe the effects of concurrent operations that are linearized before it.

In this work, we propose an online monitoring algorithm that checks whether an execution of a concurrent (or distributed) object satisfies a consistency model defined in this axiomatic framework. This algorithm constructs a linearization and visibility relation satisfying the axioms of the consistency model gradually as the execution extends with more operations. It is possible that the linearization and visibility constructed until some point in time are invalidated as more operations get executed, which requires the algorithm to backtrack and search for different candidates. This exponential blow-up is unavoidable since even the problem of checking linearizability is NP-hard in general [18].

The main difficulty in devising such an algorithm is coming up with efficient strategies for enumerating linearizations and visibility relations which minimize the number of candidates needed to be explored and the number of times the algorithm has to backtrack. We build on previous works that propose such strategies for enumerating linearizations [29, 38] in the context of linearizability checking. Roughly, the linearizations are extended iteratively by appending operations which are minimal in the happens-before order (among non-linearized operations). The choice of the minimal operations to append varies from one approach to the other. Our work focuses on combining such strategies with an efficient enumeration of visibility relations which are compatible with a given linearization.

Rather than specializing our results to one single consistency model, we consider a general class of consistency models from Burckhardt et al.’s axiomatic framework [9, 11] in which the visibility relation among operations is constrained to be contained in the linearization relation. That class includes, for instance, time-stamp based models employed in distributed object implementations, in which time stamps serve to resolve conflicts by effectively linearizing concurrent operations. We show that within this class of consistency models, it is not necessary to enumerate the set of all possible visibility relations (included in the linearization) in order to check consistency of an execution. More precisely, we develop an algorithm for enumerating visibility relations that traverses operations in linearization order and chooses for each operation o, a minimal set of operations visible to o that conforms to the consistency axioms (up to the linearization prefix that includes o). In general there may exist multiple such minimal sets of operations, and each of them must be explored. When the visibility relation cannot be extended, the algorithm needs to backtrack and choose different minimal visibility sets for previous operations. However, when all the minimal candidates have been explored, the algorithm can soundly report that the execution is not consistent, without resorting to the exploration of non-minimal visibility relations.

Besides demonstrating the soundness of minimal-visibility consistency checking, we also demonstrate its empirical impact by applying our algorithm to concurrent traces of Java concurrent data structures. We find that our algorithm consistently outperforms the baseline naïve approach to enumerating visibilities, which considers also non-minimal visibility relations. Furthermore, we demonstrate that minimal-visibility checking adds only modest overhead (roughly 2\(\times \)) to the baseline linearizability checking algorithm, which does not enumerate visibilities. This suggests that small sets of minimal visibilities typically suffice in practice, and that the additional exponential enumeration of visibilities, atop the exponential enumeration of linearizations, may be avoidable in practice. Our implementation and experiments are open source, and publicly available on GitHub.¹

In summary, this work makes the following contributions:

To the best of our knowledge, our algorithm is the first completely automatic algorithm for checking weak-consistency of arbitrary abstract data type implementations which avoids the naïve enumeration of all possible visibility relations.

The rest of this paper is organized as follows. Section 2 elaborates a formalization of Burckhardt et al.’s axiomatic consistency framework [9, 11], and Sect. 3 develops a formal argument to the soundness of considering only minimal visibility relations. Section 4 describes our overall consistency checking algorithms, and Sect. 5 describes our implementation and empirical evaluation. Section 6 describes related work, and finally Sect. 7 concludes.

We describe a formal model for concurrent (distributed) object implementations. Clients interact with an object by making invocations from a set \(\mathbb {I}\) and receiving returns from a set \(\mathbb {R}\) (parameters of invocations, if any, are part of the invocation name). An operation is an invocation \(i \in I\) paired with a return \(r\in R\); we denote such an operation by \(i \Rightarrow r\). We denote individual operations by o. The invocation, resp., the return, in an operation o is denoted by \( inv (o)\), resp., \( ret (o)\).

The interaction between a client and an object is represented by a history \({\left\langle { po , hb }\right\rangle }\) over a set of operations O which consists of

The program order is enforced by the client, e.g., by invoking a set of operations within the same thread or process, while the happens-before order represents the order in which the operations finished, i.e., \((o_1,o_2)\in hb \) iff operation \(o_1\) finished before \(o_2\) started. We assume that the program order is included in the happens-before order.

The axiomatic specifications of concurrent objects we consider are based on the following abstract representation of executions: an abstract execution over operations O is a tuple \({\left\langle { po , hb , lin , vis }\right\rangle }\) that consists of a history \({\left\langle { po , hb }\right\rangle }\) over O,

Intuitively, the visibility relation represents the inter-thread communication, how effects of operations are visible to other threads, while the linearization order models the “conflict resolution policy”, how the effects of concurrent operations are ordered when they become visible to other threads.

We say that an operation \(o_1\) such that \({\left\langle {o_1, o_2}\right\rangle } \in vis \) is visible to \(o_2\), and that \(o_2\) sees \(o_1\). Also, the set of operations visible to \(o_2\) is called the visibility set of \(o_2\). The extensions of \( inv \) and \( ret \) to partial orders on O are defined component-wise as usual.

A consistency criterion for concurrent objects is defined by a set of axioms over the relations in an abstract execution. These axioms relate abstract executions to a sequential semantics of the operations, which is defined by a function \( Spec :\mathbb {I}^*\times \mathbb {I}\rightarrow \mathbb {R}\) that determines the return value of an invocation given the sequence of invocations previously executed on the object³.

The domain \({{\mathrm{dom}}}(R)\) of a relation R is the set of elements x such that \({\left\langle {x,y}\right\rangle } \in R\) for some y; the codomain \({{\mathrm{codom}}}(R)\) is the set of elements y such that \({\left\langle {x,y}\right\rangle } \in R\) for some x. By an abuse of notation, if x is an individual element, \(x\in R\) denotes the fact that \(x\in {{\mathrm{dom}}}(R)\cup {{\mathrm{codom}}}(R)\). The (left) composition \(R_1 \circ R_2\) of two binary relations \(R_1\) and \(R_2\) is the set of pairs \({\left\langle {x,z}\right\rangle }\) such that \({\left\langle {x,y}\right\rangle } \in R_1\) and \({\left\langle {y,z}\right\rangle } \in R_2\) for some y. We denote the identity binary relation \({\{{ {\left\langle {x,x}\right\rangle } : x \in X }\}}\) on a set X by [X], and we write [x] to denote \([{\{{x}\}}]\).

Return-value consistency [9], a variant of eventual consistency without liveness guarantees, states that the return r of every operation \(i\Rightarrow r\) can be obtained from a sequential execution of i that follows the invocations visible to o (in the linearization order). This constraint will be formalized as an axiom called \(\mathsf {Ret}\). The visibility relation can be chosen arbitrarily. Standard “session guarantees” can be described in the same framework by adding constraints on the visibility relation: for instance, read my writes, i.e., operations previously executed in the same thread remain visible, can be stated as \(\mathsf {vis}\supseteq \mathsf {po}\) and monotonic reads, i.e., the set of visible operations to some thread grows monotonically over time, can be stated as \(\mathsf {vis}\supseteq \mathsf {vis}\circ \mathsf {po}\). Then, a version of causal consistency [7, 9], called causal convergence, is defined by the following set of axioms:which state that the visibility relation is transitive, it includes program order, and it is included in the linearization order. Finally, linearizability is defined by the set of axioms \(\mathsf {lin}\supseteq \mathsf {hb}\), \(\mathsf {vis}=\mathsf {lin}\), and \(\mathsf {Ret}\).

To state our results in a general context that concerns multiple consistency criteria defined in the literature (including the ones mentioned above) and variations there of, we consider a language of consistency axioms \(\phi \) defined by the grammar in Fig. 2. A consistency model \(\varPhi \) is a set \({\{{ \phi _1, \phi _2, \ldots }\}}\) of consistency axioms.

In the following, we assume that every consistency model is stronger than return-value consistency, and also, that the linearization order is consistent with the visibility and happens-before relations. The assumptions concerning the linearization order correspond to the fact that for instance, concurrent operations are ordered using timestamps that correspond to real-time. Formally, we assume that every consistency model contains the axiomsFigure 3 defines the precise semantics of consistency axioms on abstract executions: the context of an operation o according to a linearization \( lin \) and visibility \( vis \), denoted \( ctxt ( lin , vis , o)\) is the restriction \(([O_o] \circ lin \circ [O_o])\) of \( lin \) to the operations \(O_o = {{\mathrm{dom}}}( vis \circ [o])\) visible to o. For instance, for the abstract execution in Fig. 1(b), \( ctxt ( lin , vis , \mathtt{contains}(0)\Rightarrow \mathtt{false})\) is the sequence of operations \(\mathtt{put}(1,0)\Rightarrow \mathtt{null}; \mathtt{get}(1)\Rightarrow 0; \mathtt{put}(1,1)\Rightarrow 0\).

We extend this semantics to consistency models as \(e \models \varPhi \) iff \(e \models \phi \) for all \(\phi \in \varPhi \) and to histories as:

Checking whether a given history satisfies a consistency model is intractable in general. This essentially follows from the fact that checking linearizability is NP-hard in general [18]. While the main issue in checking linearizability is enumerating the exponentially many linearizations, checking weaker criteria like causal convergence requires also an enumeration of the exponentially many visibility relations (included in a given linearization). We prove in this section that it is enough to enumerate only minimal visibility relations (w.r.t. set inclusion), included in a given linearization, in order to conclude whether a given history and linearization satisfy a consistency model.

A linearized history \(\sigma ={\left\langle { po , hb , lin }\right\rangle }\) consists of a history and a linearization \( lin \) such that \( lin \supseteq hb \). The extension of \(\models \) to linearized histories is defined as:The i-th element of a sequence s is denoted by s[i] and the prefix of s of length i is denoted by \(s_i\). The projection of a linearized history \(\sigma ={\left\langle { po , hb , lin }\right\rangle }\) to a prefix \( lin _i\) of \( lin \) is denoted by \(\sigma _i\). Formally, \(O_i={{\mathrm{dom}}}( lin _i)\cup {{\mathrm{codom}}}( lin_i )\) and \(\sigma _i = {\left\langle { po \cap (O_i\times O_i), hb \cap (O_i\times O_i), lin _i}\right\rangle }\).

For a linearized history \({\left\langle { po , hb , lin }\right\rangle }\) and a consistency model \(\varPhi \), a visibility relation \( vis _i\) on operations from a prefix \( lin _i\) of \( lin \) is called \(\varPhi \)-extensible when there exists a visibility relation \( vis \supseteq vis _i\) such that \({\left\langle { po , hb , lin , vis }\right\rangle }\models \varPhi \). The relation \( vis \) is called a \(\varPhi \)-extension of \( vis _i\) up to \( lin \). By extrapolation, a \(\varPhi \)-extension of \( vis _i\) up to \( lin_j \) is a visibility relation \( vis _j\) such that \({\left\langle {\sigma _j, vis _j}\right\rangle }\models \varPhi \), for any \(i< j\). Such an extension is called minimal when for every other \(\varPhi \)-extension \( vis _j'\) of \( vis _i\) up to \( lin _j\), we have that \( vis _j'\not \subseteq vis _j\).

The next lemma shows that minimizing the visibility sets of operations in a linearization prefix, while preserving the truth of the axioms on that prefix, doesn’t exclude visibility choices for future operations (occurring beyond that prefix). In more precise terms, the \(\varPhi \)-extensibility status is not affected by choosing smaller visibility sets for operations in a linearization prefix. For instance, since the visibility \( vis _3\) in Example 5 is extensible (for causal convergence), the smaller visibility relation in which \(\mathtt{put}(0,0)\Rightarrow \mathtt{null}\) doesn’t see any operation, is also extensible. This result relies on the specific form of the axioms, which ensure that smaller visibility sets impose fewer constraints on the visibility sets of future operations. For instance, the axiom \( vis \supseteq vis \circ vis \) enforces that \( vis \) contains \(\{{\left\langle {o,o_2}\right\rangle }: {\left\langle {o,o_1}\right\rangle }\in vis \}\) whenever a pair \({\left\langle {o_1,o_2}\right\rangle }\) is added to \( vis \). Minimizing the visibility set of \(o_1\) will minimize the set of operations that must be seen by \(o_2\), thus making the choice of the operations visible to \(o_2\) more liberal.

The main result of this section shows that a visibility enumeration strategy that considers operations in the linearization order and computes minimal extensions iteratively, possibly backtracking to another choice of minimal extension if necessary, is complete in general (it finds a visibility relation satisfying the consistency axioms \(\varPhi \) iff the input linearized history satisfies \(\varPhi \)). Backtracking is necessary since in general, there may exist multiple minimal extensions and all of them should be explored. For a given linearized history \(\sigma \) and visibility relation \( vis \) on operations of \(\sigma \), \( vis _i= vis \circ [O_i]\) denotes the restriction of \( vis \) to operations from the prefix \( lin _i\).

We describe an algorithm for checking whether a given history satisfies a consistency model, which combines linearization enumeration strategies proposed in [29, 38] with the visibility enumeration strategy proposed in Sect. 3.

The algorithm is defined by the procedure checkConsistency listed in Fig. 4. This recursive procedure searches for extensions of the input linearization and visibility (initially, checkConsistency will be called with \( lin = vis =\emptyset \)) which witness that the input history h satisfies \(\varPhi \). It assumes that the inputs \( lin \) and \( vis \) satisfy the axioms of the consistency model \(\varPhi \) when the input history is projected on the linearized operations (the operations in \( lin \)). This projection is denoted by \(h_{ lin }\). Formally, the precondition of this procedure is that \({\left\langle {h_{ lin }, lin , vis }\right\rangle }\models \varPhi \).

The extensions of \( lin \) and \( vis \) are built in successive steps. At each step, the linearization is extended according to the procedure linExtensions and the visibility according to the procedure visExtensions.

The abstract implementation of linExtensions, presented in Fig. 4, chooses a set of non-linearized operations O which are minimal among non-linearized operations w.r.t. happens-before, i.e., returned by \(\mathtt{minimals}(h, lin )\), and appends any linearization of the operations in O to the input linearization \( lin \). Formally, \(O\subseteq \{o:o\not \in lin \text{ and } \forall o'.\ o'\not \in lin \Rightarrow \lnot o' \prec o\}\), where \(\prec \) denotes the happens-before relation. The fact that the operations in O are minimal among non-linearized operations ensures that the returned linearizations are consistent with the happens-before order.

Two linearization enumeration strategies proposed in the literature can be seen as instances of linExtensions. The strategy in [38] corresponds to the case where O contains exactly one minimal operation. For instance, for the history in Fig. 1(a), this strategy will start by picking a minimal element in the happens-before relation, say \(\mathtt{put}(1,0)\Rightarrow \mathtt{null}\), then, a minimal operation among the rest, say \(\mathtt{get}(1)\Rightarrow 0\), and so on.

The strategy proposed in [29] is slightly more involved (and according to experimental results, more efficient), but it relies on a presentation of histories h as sequences of call and return actions (an operation spanning the time interval between its call and return action). The happens-before order is extracted as usual: an operation \(o_1\) happens before an operation \(o_2\) if its return occurs before the call of \(o_2\). This strategy defines O as the first non-linearized operation o that returned in h together with a set of non-linearized operations \(O'\) that are concurrent with o (i.e., are not ordered after o in the happens-before order). The operation o is linearized last in the returned extensions. For instance, consider the history h in Fig. 5 represented as a sequence of call/return actions (small boxes at the begin, resp., end, of an interval denote call actions, resp., return actions). The first linearization extension (when \( lin =\emptyset \)) includes \(\mathtt{put}(1,0)\Rightarrow \mathtt{null}\) (the first operation to return) after some sequence of operations concurrent with it, for instance the empty sequence. Next, the current linearization \(\mathtt{put}(1,0)\Rightarrow \mathtt{null}\) can be extended by adding \(\mathtt{put}(0,0)\Rightarrow \mathtt{null}\) (the first operation to return, if we exclude \(\mathtt{put}(1,0)\Rightarrow \mathtt{null}\) which is already linearized) and possibly \(\mathtt{get}(1)\Rightarrow 0\) before it. Suppose that we choose \(\mathtt{put}(1,0)\Rightarrow \mathtt{null}; \mathtt{get}(1)\Rightarrow 0; \mathtt{put}(0,0)\Rightarrow \mathtt{null}\). Then, the extension will include \(\mathtt{put}(1,1)\Rightarrow 0\) and possibly \(\mathtt{contains}(0)\Rightarrow \mathtt{true}\) or \(\mathtt{contains}(0)\Rightarrow \mathtt{false}\), and so on. Compared to the previous strategy, an extension step can add multiple operations.

The extensions of the visibility relation (returned by visExtensions) are minimal \(\varPhi \)-extensions of \( vis \) up to the input linearization. They can be constructed iteratively by considering the newly linearized operations one by one and each time compute a minimal extension of the visibility. For instance, the linearization construction explained in the previous paragraph can be expanded with a visibility enumeration as follows:

The procedure \(\mathtt{checkConsistency}\) backtracks to a different extension when the current one cannot be completed to include all the operations in the input history (checked by the recursive call). The correctness of the algorithm is stated in the following theorem.

While our minimal-visibility consistency checking algorithm is applicable to a wide class of distributed and multicore shared object implementations, here we demonstrate its efficacy on histories recorded from executions of Java Development Kit (JDK) Standard Edition concurrent data structures. Recent work demonstrates that JDK concurrent data structures regularly admit non-atomic behaviors, often by design [14]; these weakly-consistent behaviors span many methods of the java.util.concurrent package, including the ConcurrentHashMap, ConcurrentSkipListMap, ConcurrentSkipListSet, ConcurrentLinkedQueue, and the ConcurrentLinkedDeque, for instance, including the contains method described in Example 3.

We subject each client program to 1 s of stress testing⁴ to record histories. The return value of each invocation is stored in a different thread-local variable which is read at the end of the execution. Recording the happens-before order between invocations without affecting implementation behavior significantly (e.g., without influencing the memory orderings between shared-memory accesses) is challenging. For instance, we found the use of high-precision timers to be unsuitable, since the response-time of System.nanoTime calls is much higher than calls to the implementations under test; invoking such timers between each invocation of implementation methods would prevent implementation methods from overlapping in time, and thus hide any possible inconsistent behaviors. Similarly, the use of atomic operations and volatile variables would impose additional synchronization constraints and prevent many weak-memory reorderings.

Essentially, our solution is to introduce a shared variable per thread storing its program counter – in our context, the program counter stores the number of call and return events thus far executed. A thread’s program counter is read by every other thread before and after each invocation. Figure 6 demonstrates a simplified version⁵ of our encoding for a program with two threads each invoking two methods. The program counter variables \(\mathtt{pc0}\) and \(\mathtt{pc1}\) are not declared volatile, which, in principle, provides stronger guarantees concerning the derived happens-before relation; such declarations would interfere with implementation weak-memory effects. The program counter values read by each thread allows us to extract a happens-before order between invocations which is sound in the sense that the actual happens-before may order more operations, but not fewer – assuming that shared-memory accesses satisfy at least the total-store order (TSO) semantics in which writes are guaranteed to be performed according to program order. For instance, when \(\mathtt{pcs[0][0]} > 2\) in the second thread (\(\mathtt{thread1}\)), the first invocation in the other thread (\(\mathtt{thread0}\)) happens-before the first invocation in this thread. Otherwise, if \(\mathtt{pcs[0][0]} < 2\), then the two invocations are overlapping in time. The latter may not be true in the real happens-before due to the delay in incrementing and reading the program counter variables. Although some loss of precision is possible, we are unaware of other methods for tracking happens-before which avoid significant interference with the implementation under test.

Based on the encoding described above, we generate histories as sequences of call and return actions which serve as input to our consistency checking algorithms. For simplicity, we have considered just two consistency models, linearizability and a weak consistency model defined by \({\{{\mathsf {Ret}, \mathsf {lin} \supseteq \mathsf {vis}, \mathsf {lin} \supseteq \mathsf {hb}, \mathsf {vis}\supseteq \mathsf {hb}}\}}\) – see Sect. 2. We consider linearizability in order to measure the overhead of checking weak consistency due to visibility enumeration; the second model is simply the easiest weak-consistency model to support with our implementation; the choice among possible weak-consistency models appears fairly arbitrary, since the enumeration of visibility relations is common to all.

We consider several measurements, the results of which are listed in Figs. 7 and 8; all times are measured in milliseconds on logarithmic scale on a 2.7 GHz Intel Core i5 MacBook Pro with Oracle–s Java SE runtime version 9; and timeouts are set to 1000 ms. We note that while accurate and recording of operation timings within an execution without interference is challenging, timing the validation of each recorded history, which we report here, is accomplished accurately, without interference, by computing the clock difference just before and after validation.

Our first measurements establish the baseline linearizability and weak-consistency checking algorithms. On the left side of Fig. 7 we consider the time required to check linearizability for each history by our own implementations of Wing and Gong’s standard enumerative approach [38], along with Lowe’s “just-in-time linearizability” algorithm [29] – see Sect. 4. We resolve the nondeterminism in these algorithms (e.g., in choosing which pending operation to attempt linearizing first) arbitrarily (e.g., first called), finding no clear winner: each algorithm performs better on some histories. Since these subtleties are outside the scope of our work, we avoid further investigation and choose Wing and Gong’s algorithm as our baseline linearizability-checking algorithm.

Our second measurement exposes the overhead of enumerating visibility relations for checking weak consistency. On the right side of Fig. 7 we consider the time required to check weak consistency of a given history versus the time required to check its linearizability.⁶ We observe an overhead of approximately 10\(\times \) due to visibility enumeration and validation. Our naïve implementation enumerates candidate visibilities in size-decreasing order since we expect visibility-loss to be the exception rather than the rule; for instance, atomic operations observe all linearized-before operations. We omit the analogous comparison between weak-consistency checking and just-in-time linearizability checking to avoid redundancy, since the just-in-time optimization is a seemingly-insignificant factor in our experiments: the results are nearly identical.

Our third measurement demonstrates the impact of our minimal-visibility consistency checking optimization. On the left side of Fig. 8 we consider the time required to check weak consistency without and with our optimization. The difference is dramatic, with our optimized algorithm consistently outperforming, sometimes up to multiple orders of magnitude: the leftmost 1000 ms timeout of the naïve algorithm is matched by a roughly 18 ms positive identification. Finally, our fourth measurement, on the right side of Fig. 8, demonstrates that the overhead of our minimal-visibility checking algorithm over linearizability checking is quite modest: we observe roughly a 2\(\times \) overhead, compared with the observed 10\(\times \) overhead without optimization.

While our experiments clearly demonstrate the efficacy of our minimal-visibility consistency checking algorithm, we will continue to evaluate this optimization across a wide range of concurrent objects, consistency models, and client programs, e.g., including many more concurrent threads. While we do expect the performance of linearizability- and weak-consistency checking to vary with thread count, we expect the performance gains of minimal-visibility consistency checking to continue to hold.

Herlihy and Wing [22] described linearizability, which is the standard consistency criterion for shared-memory concurrent objects. Motivated by replication-based distributed systems, Burckhardt et al. [9, 11] describe a more general axiomatic framework for specifying weaker consistencies like eventual consistency [36] and causal consistency [2]. Our weak consistency checking algorithm applies to consistency models described in this framework.

While several static techniques have been developed to prove linearizability [1, 4, 6, 12, 13, 21, 22, 24, 26, 27, 30‐34, 37, 39], few have addressed dynamic techniques such as testing and runtime verification. The works in [29, 38] describe monitors for checking linearizability that construct linearizations of a given history incrementally, in an online fashion. Line-Up [10] performs systematic concurrency testing via schedule enumeration, and offline linearizability checking via linearization enumeration. Our weak consistency checking algorithm combines these approaches with an efficient enumeration of visibility relations. The works in [15, 16] propose a symbolic enumeration of linearizations based on a SAT solver. Although more efficient in practice, this approach applies only to certain ADTs. In this work, we propose a generic approach that assumes no constraints on the sequential semantics of the concurrent objects.

Bouajjani et al. [7] consider the problem of verifying causal consistency. They propose an algorithm for checking whether a given execution satisfies causal consistency, but only for the key-value map ADT with simple \(\mathtt{put}\) and \(\mathtt{get}\) operations. Our work proposes a generic algorithm that can deal with various weak consistency criteria and ADTs.

From the complexity standpoint, Gibbons and Korach [18] showed that monitoring even the single-value register type for linearizability is np-hard. Alur et al. [3] showed that checking linearizability of all executions of a given implementation is in expspace when the number of concurrent operations is bounded, and then Hamza [20] established expspace-completeness. Bouajjani et al. [5] showed that the problem becomes undecidable once the number of concurrent operations is unbounded. Also, Bouajjani et al. [7, 8] investigate various ADTs for which the problems of checking eventual and causal consistency are decidable.

We have developed the first completely-automatic algorithm for checking weak consistency of arbitrary concurrent object implementations which avoids the naïve enumeration of all possible visibility relations. While methodologies for constructing reliable yet weakly-consistent implementations are relatively immature, we believe that such implementations will continue to be important for the development of distributed and multicore software systems. Likewise, automation for testing and verifying such implementations is, and will increasingly be, important. Besides improving state-of-the-art verification algorithms, our results represent an important step for future research which may find other ways to exploit the soundness of considering only minimal visibilities, on which our optimized algorithm relies.