Optimal Concolic Dynamic Partial Order Reduction

Systematic state space exploration for concurrent software involves exploring both concurrency nondeterminism and data nondeterminism. Concurrency nondeterminism arises out of the possible orders in which threads or processes can be scheduled or messages delivered; data nondeterminism arises out of the possible values that variables may take. Both sources are important in finding bugs.

There are orthogonal techniques to handle each source in the context of dynamic (or stateless) model checking. Dynamic partial order reduction (DPOR) [29, 30, 6, 48, 45] handles concurrency nondeterminism efficiently by maintaining scheduling constraints along an execution, and exploring distinct schedules if and only if the corresponding constraints lead to non-equivalent executions. Modern DPOR tools explore the concurrency space optimally [6, 45] and also account for errors caused by compiler/CPU reorderings [8, 5, 48, 56].

Symbolic execution handles data nondeterminism by maintaining symbolic constraints on data along an execution, and exploring distinct execution paths if and only if the symbolic constraints along these paths are mutually disjoint. Tools based on dynamic symbolic execution (also called concolic testing, CT) [31, 61, 19, 23], maintain the symbolic constraints dynamically, and efficiently manage the backtracking symbolic search.

Despite their many individual successes, few tools handle both concurrency and data nondeterminism simultaneously and optimally. Current approaches ignore either partial orderings [59, 19, 23] or data nondeterminism [55, 6, 56, 40, 45] or optimality [58, 60].

In this paper, we present ConDpor, a systematic exploration algorithm that combines DPOR with CT. ConDpor does so by maintaining symbolic constraints in the trace constructed by a DPOR algorithm (specifically, TruSt [45]), and backtracking both on scheduling constraints and on symbolic constraints.

But why tackle both issues at the same time in the first place? At a first glance, data- and concurrency bugs seem orthogonal, as many concurrent programs are otherwise deterministic. However, popular concurrent data structures argue otherwise: algorithms like timestamped stack [26] or elimination-backoff stack [37] use timestamps or random identifiers to achieve better efficiency, and thus fundamentally require reasoning about both concurrency- and data nondeterminism. Moreover, concurrency APIs also often require supporting data nondeterminism, as their primitives may fail with multiple error values, each one leading to a different control-flow path. In a nutshell, handling concurrency and data together amplifies stateless model checking to unbounded state spaces.

An interesting aspect of ConDpor lies in how symbolic constraints are generated and manipulated in the context of DPOR. Indeed, as we later show, ConDpor only needs to know when symbolic values are generated, and when symbolic constraints are evaluated. As such, instead of using a dedicated runtime to manipulate the symbolic path constraint according to the executed instructions, ConDpor offloads the manipulation of symbolic expressions to the underlying programming language (similarly to [20, 63, 60]). Specifically, ConDpor provides dedicated datatypes for symbolic types (available to users) that “carry” the symbolic path constraint of the execution. Arithmetic operations on symbolic variables manipulate the path constraint before performing the respective operation, while logical operations record an event in the current trace at which ConDpor can later backtrack.

ConDpor is sound (i.e., explores no false positives), complete (i.e., explores all program behaviors), optimal (i.e., does not explore traces that only differ in the execution of DPOR-independent instructions or in the model satisfying the symbolic constraints), and parametric in the choice of the memory model (i.e., can find bugs due to compiler/CPU reorderings). As our implementation of ConDpor for concurrent Java programs demonstrates, ConDpor is also efficient: its overhead over standard DPOR is proportional to the amount of data nondeterminism in a given program, and ConDpor is able to fully explore challenging concurrent data structures within seconds.

In summary, we make the following contributions.

• $\mathrm{■}$

  We present ConDpor, a combination of optimal DPOR and concolic execution, and prove it sound, complete, and optimal.

• $\mathrm{■}$

  We implement ConDpor in a tool for programs running on the JVM.

• $\mathrm{■}$

  We empirically show that ConDpor can systematically explore concurrent programs involving both data and concurrency nondeterminism efficiently, with only a small memory overhead.

In this section, we provide a motivating example, followed by an informal description of ConDpor, along with some algorithmic and engineering challenges we faced.

We now formally describe execution graphs, the data structure behind ConDpor’s partial order semantics. We begin by defining events.

Block and error labels are generated by assume and assert statements, respectively. An $\text{assume}(b)$ statement is modeled as $\text{if}(!b)\text{block()}$, while an $\text{assert}(b)$ statement is modeled as $\text{if}(!b)\text{error()}$. The block() and error() statements generate the respective labels, while $b\in \mathrm{𝖵𝖺𝗅}$ is a boolean value.

Having defined events, we define execution graphs as follows.

We write $G.𝙴$, $G.\mathrm{𝚛𝚏}$, $G.\mathrm{𝚌𝚘}$, and ${\le }_G$ to project the various components of an execution graph, and use ${G|}_E$ to denote the restriction of an execution graph $G$ to a set of events $E$. We assume that $\mathrm{𝚒𝚗𝚒𝚝}\in 𝚆$, and use the functions $\mathrm{𝚝𝚒𝚍}$, $\mathrm{𝚒𝚍𝚡}$, $\mathrm{𝚕𝚘𝚌}$, $\mathrm{𝚟𝚊𝚕}$ and $\mathrm{𝚏𝚘𝚛𝚖𝚞𝚕𝚊}$ to get (when applicable) the thread identifier, index, location, value and formula of an event, respectively. We write $G.\mathsf{\Phi }\triangleq {\bigwedge }_{s\in G.𝙲}\mathrm{𝚏𝚘𝚛𝚖𝚞𝚕𝚊}(s)$ for the conjunction of all symbolic constraints of the graph, $G.𝚆$ for $G.𝙴\cap 𝚆$ (and similarly for other sets), and use subscripts to further restrict these sets (e.g., ). Finally, given two events $e_1,e_2\in G.𝙴$, we write if $e_1{\le }_G{e}_2$ and $e_1\ne e_2$.

As defined above, execution graphs do not have an explicit program order ($\mathrm{𝚙𝚘}$) component. We thus induce $\mathrm{𝚙𝚘}$ based on our event representation as follows:

We write for the graph’s causal dependency relation.

Finally, we define the semantics of a program $P$ under a model M as the set of execution graphs corresponding to $P$ that satisfy M’s consistency predicate. In this paper, we assume a memory model M providing a consistency predicate ${\mathrm{𝖼𝗈𝗇𝗌𝗂𝗌𝗍𝖾𝗇𝗍}}_{\text{M}}(G)$, determining whether a graph $G$ is consistent, as well as an error predicate ${\text{IsErroneous}}_{\text{M}}(G)$, determining whether $G$ contains an error (e.g., a data race) according to M. We further assume that ${\mathrm{𝖼𝗈𝗇𝗌𝗂𝗌𝗍𝖾𝗇𝗍}}_{\text{M}}(\cdot )$ is extensible, prefix-closed, and implies RMW atomicity and $\mathrm{𝚙𝚘}\mathrm{𝚛𝚏}$ acyclicity (see [45]), and that ${\text{IsErroneous}}_{\text{M}}(\cdot )$ is monotone (if a prefix-closed subset of a graph $G$ contains an error, then so does $G$). Models satisfying these assumptions include SC [51], TSO [57] and RC11 [50] under shared-memory consistency, as well as asynchronous communication, peer-to-peer, and mailbox under message-passing consistency [25].

Given such an underlying memory consistency model M, we then define a new memory model ${\text{M}}_S$, with ${\mathrm{𝖼𝗈𝗇𝗌𝗂𝗌𝗍𝖾𝗇𝗍}}_{{\text{M}}_{𝖲}}(G)\triangleq {\mathrm{𝖼𝗈𝗇𝗌𝗂𝗌𝗍𝖾𝗇𝗍}}_{\text{M}}(G)\wedge \text{SAT}(G.\mathsf{\Phi })$ and ${\text{IsErroneous}}_{{\text{M}}_S}(G)\triangleq {\text{IsErroneous}}_{\text{M}}(G)$, where $\text{SAT}(\cdot )$ is a predicate denoting whether a symbolic constraint is satisfiable. Intuitively, ${\text{M}}_S$ extends the underlying communication semantics to also require that all symbolic constraints in a graph are satisfiable. It is easy to show that ${\text{M}}_S$ satisfies the memory-model properties stated above.

Let us now present ConDpor in detail (cf. Algorithm 1). Although our algorithm works both under the Shasha-Snir and the reads-from equivalence partitioning, here we only provide the (more straightforward) Shasha-Snir version [62], the generalization of Mazurkiewicz equivalence partitioning for relaxed memory models such as TSO and PSO. Symbolic reasoning does not affect the choice of partitioning, and the required changes can be adapted from [45].

Given a program $P$, ConDpor explores all of its consistent execution graphs under a model M by calling ${\text{Visit}}_{P,{\text{M}}_S}(G_{\mathrm{\varnothing }})$, where $G_{\mathrm{\varnothing }}$ is the initial graph containing only the initialization event $\mathrm{𝚒𝚗𝚒𝚝}$. In turn, Visit constructs the execution graphs of $P$ one at a time and incrementally, while also recording the event addition order in the graph’s $\le$ component.

Let us now examine Visit more closely. As a first step, Visit checks whether $G$ contains an error (line 2); errors include safety violations (which manifest with an ${\mathrm{𝚎𝚛𝚛𝚘𝚛}}^{}$ label), as well as memory-model-specific errors such as data races.

After ensuring that the graph is error-free, Visit extends the current graph with the next program event (line 3) with the help of Add and next. next returns an event from a thread that is not blocked or finished, and Add adds it to the graph in place, and then returns the new event. If there are no events to add (in which case Add/next returns $\perp$), a full execution of $P$ has been explored, and Visit returns (line 4).

If $a$ is a read, we recursively explore all consistent $\mathrm{𝚛𝚏}$ options for it (line 7). (We assume that $\text{SetRF}(G,r,w)$ returns a new graph $G^{\prime }$ that only differs from $G$ in $\mathrm{𝚛𝚏}$: $G^{\prime }.\mathrm{𝚛𝚏}(r)=w$.)

If $a$ is a constraint-evaluation event, ConDpor has to examine whether the newly added event (and its negation) renders $G.\mathsf{\Phi }$ satisfiable. To do that, Visit calls VisitIfConsistent twice: once with $a$’s constraint as is, and another time with $a$’s expression negated. In order to set $a$’s symbolic constraint, Visit employs the $\text{SetSYM}(G,a,\varphi )$ function, which returns a new graph $G^{\prime }$ that is identical to $G$, apart from the constraint of event $a$, which is set to $\varphi$. Observe that if $G^{\prime }.\mathsf{\Phi }$ is unsatisfiable, then the execution subsequently be dropped by VisitIfConsistent as inconsistent.

If $a$ is a write, ConDpor examines both the non-revisit- and the revisit case. In the non-revisit case, ConDpor explores all consistent $\mathrm{𝚌𝚘}$ options for $a$ via VisitCOs (line 12). Analogously to SetRF, $\text{SetCO}(G,w_p,w)$ returns a new graph $G^{\prime }$ that only differs from $G$ in that the $\mathrm{𝚌𝚘}$-predecessor of $w$ is $w_p$.

In the revisit case, Visit examines previously-added reads as revisit candidates. Concretely, Visit only revisits same-location reads that are not $\mathrm{𝚙𝚘}\mathrm{𝚛𝚏}$-before $a$ (as revisiting those would create $\mathrm{𝚙𝚘}\mathrm{𝚛𝚏}$ cycles), assuming that the events deleted from the revisit have been added maximally (lines 13-14). The maximal-addition definition closely follows the one of Kokologiannakis et al. [46]: ConDpor backward-revisits $r$ from $a$ if all deleted events are added $\mathrm{𝚌𝚘}$-maximally (if non-symbolic), or in a unique fashion (if symbolic). Formally, we write $G_1\stackrel{𝑒}{\rightsquigarrow }{G}_2$ if $G_2=\text{Add}(G_1,e)$ and:
$G_2.\mathrm{𝚛𝚏}=G_1.\mathrm{𝚛𝚏}\cup \{⟨{\mathrm{𝗆𝖺𝗑}}_{G_1.{\mathrm{𝚌𝚘}}_e},e⟩\}$ $G_2.\mathrm{𝚌𝚘}=G_1.\mathrm{𝚌𝚘}$ $G_2.\mathsf{\Phi }=G_1.\mathsf{\Phi }$ $\text{if }e\in 𝚁$ $G_2.\mathrm{𝚛𝚏}=G_1.\mathrm{𝚛𝚏}$ $G_2.\mathrm{𝚌𝚘}=G_1.\mathrm{𝚌𝚘}\cup (G_1.{𝚆}_e\times \{e\})$ $G_2.\mathsf{\Phi }=G_1.\mathsf{\Phi }$ $\text{if }e\in 𝚆$ $G_2.\mathrm{𝚛𝚏}=G_1.\mathrm{𝚛𝚏}$ $G_2.\mathrm{𝚌𝚘}=G_1.\mathrm{𝚌𝚘}$ $G_2.\mathsf{\Phi }=\text{ST}(G_1.\mathsf{\Phi },e)$ $\text{if }e\in 𝙲$ $G_2.\mathrm{𝚛𝚏}=G_1.\mathrm{𝚛𝚏}$ $G_2.\mathrm{𝚌𝚘}=G_1.\mathrm{𝚌𝚘}$ $G_2.\mathsf{\Phi }=G_1.\mathsf{\Phi }$ otherwise
Above, the $\text{ST}(\cdot )$ function acts as a tiebraker if both cases of a constraint-evaluation event are feasible. If both $\mathrm{𝚏𝚘𝚛𝚖𝚞𝚕𝚊}(e)$ and $\neg \mathrm{𝚏𝚘𝚛𝚖𝚞𝚕𝚊}(e)$ are feasible, it (arbitrarily) returns $G_1.\mathsf{\Phi }\wedge \mathrm{𝚏𝚘𝚛𝚖𝚞𝚕𝚊}(e)$, while if only $\mathrm{𝚏𝚘𝚛𝚖𝚞𝚕𝚊}(e)$ (resp. $\neg \mathrm{𝚏𝚘𝚛𝚖𝚞𝚕𝚊}(e)$) is feasible, it returns $G_1.\mathsf{\Phi }\wedge \mathrm{𝚏𝚘𝚛𝚖𝚞𝚕𝚊}(e)$ (resp. $G_1.\mathsf{\Phi }\wedge \neg \mathrm{𝚏𝚘𝚛𝚖𝚞𝚕𝚊}(e)$).

We implemented ConDpor as a tool for concurrent Java programs⁵⁵5https://github.com/mpi-sws-rse/jmc. Our tool supports commonly used Java synchronization primitives such as locks, monitors, synchronized blocks, as well as thread creation and joining.

ConDpor can operate in two modes: a verification mode, and a “random mode” in which ConDpor samples executions from the program state space. The latter mode is useful for finding bugs faster, as random sampling does not involve backtracking.

Verifying a program with ConDpor involves three steps:

1. (1)

   compiling it into Java bytecode,

2. (2)

   instrumenting the bytecode so that we can intercept operations of interest, and

3. (3)

   running the instrumented bytecode under a special runtime that implements ConDpor to systematically explore all program behaviors.

Even though our algorithm is parametric in the choice of the memory model, our implementation currently only works under SC [51].

To instrument the bytecode, we used the ASM library [1], and inserted yield calls to ConDpor at points of interest. For example, whenever a thread acquires or releases a lock, the instrumented bytecode yields control to ConDpor, which then updates the execution graph and schedules threads appropriately. ConDpor controls thread scheduling by employing a shared mutex between the native Java Thread and the scheduler thread. We implement the yield method as Object.wait over this shared mutex, effectively imposing a cooperative multithreading semantics on top of the Java runtime.

To return appropriate values during constraint evaluation, ConDpor uses the JavaSMT library [13] to query an SMT solver for satisfiability. Although JavaSMT can interface with multiple solvers, we have only experimented with Z3 [3]. Similarly to TruSt [45], ConDpor copies the graph whenever a write revisits a read, meaning that a new solver instance has to be created as well. We found that creating new instances is expensive, and implemented a shared solver pool with a fixed number of instantiated solvers to allow solver reuse. Each solver instance also leverages incremental solving, which turned out to be very beneficial.

Finally, note that users must utilize our symbolic API to capture all sources of data nondeterminism manually: in practice, this involves subclassing some input types to their symbolic counterparts. Note that some existing symbolic (or concolic) execution engines, like EXE [20], employ source-to-source translation, where the instrumentation is written in the same programming language as the program under test. While a source-to-source translation is also possible for Java, we decided to implement ConDpor using bytecode instrumentation and by encoding symbolic objects directly in the language, so as to avoid maintaining a Java compiler infrastructure.

We now proceed with ConDpor’s evaluation, which aims to answer the following questions:

§​ 6.1

How does symbolic handling of data nondeterminism fare against an explicit one?

§​ 6.2

Can ConDpor handle real-world programs that employ data nondeterminism?

To answer these questions, we conduct two case studies. To showcase the differences between explicit and symbolic handling of data nondeterminism, we evaluate ConDpor on a set of synthetic benchmarks designed to juxtapose the two approaches. To see how well ConDpor scales in realistic code, we use a diverse set of concurrent data structures that rely on randomness (modeled as data nondeterminism). In both studies, we compare ConDpor against a baseline DPOR implementation ExEn that handles data nondeterminism explicitly by exhaustively enumerating all possible values in the input domain, and repeatedly running vanilla DPOR for each value. To ensure a fair comparison, we restrict the data domain to $\{0,1,2\}$, making explicit enumeration feasible.

Our evaluation demonstrates that ConDpor’s handling of nondeterminism is exponentially better than ExEn’s, and that ConDpor is able to completely explore clients of data-nondeterministic concurrent data structures. Moreover, ConDpor’s overhead over vanilla DPOR is proportional to the amount of data nondeterminism in the input program.

As far as handling data nondeterminism is concerned, a lot of research has focused around symbolic execution (e.g., [16, 68, 61]), which uses a symbolic interpreter to examine many program paths at once [43]. As symbolic execution is a static technique and the number of symbolic paths to explore explodes, recent work [31, 19, 32, 21, 53, 66] has focused on dynamic symbolic execution (aka concolic testing), where certain symbolic variables are concretized in order to reduce the state-space size. Despite their success, most symbolic tools do not reason about concurrency and weak memory consistency.

For scheduling nondeterminism, most automated tools are based on either testing or model checking. Testing tools (e.g., [41, 49, 52, 17, 2, 18, 71]) randomly sample the state space of a program in order to detect concurrency bugs, but they do not provide completeness guarantees, nor do they handle data-nondeterminism. Model checkers (e.g., [39, 35]), on the other hand, do guarantee completeness, as they exhaustively enumerate the state space of a program (up to a bound). In order not to store all the visited program states, model checking is often done “on the fly” (a.k.a. stateless model checking) [55, 30], while also employing partial order reduction [29, 7, 56, 45, 27, 47, 33, 4, 9]. While model checkers can handle data nondeterminism explicitly, explicit enumeration quickly blows up the state space (see § 6).

There has been work aiming to handle both scheduling and data nondeterminism (e.g., [28, 65, 70]), either by adding concurrency reasoning to concolic testing, or the other way around. Con2Colic [28] extends CT by introducing interference scenarios to encode the scheduling constraints that lead to new execution paths. Similarly, Guo et al. [34] encode program assertions as symbolic constraints to develop sound methods that prune out redundant executions. Tools like cmbc [24] encode the program into an SAT formula, and offload all symbolic reasoning to an SMT solver. JPF has been extended to incorporate symbolic execution [12]. None of these tools perform optimal partial order reduction for general memory consistency models. Finally, there are several works that attempt to efficiently combine DPOR with symbolically encoded partial-order constraints to reduce redundant exploration (e.g.,  [11, 42]). Unlike our approach, however, these do not tackle the problem of data nondeterminism within concurrent programs.

Another approach to addressing both scheduling and data non-determinism is maximal path causality (MPC) [69]. MPC uses a coarser equivalence partitioning than ConDpor, as it packs all combinations of schedules and data that reach the same path into a single equivalence class. Upon obtaining a random program interleaving, MPC collects constraints that would lead to the exploration of an unseen path, and explores them by re-running the program.

Apart from not being able to handle weak memory consistency models, MPC is not optimal w.r.t. its partitioning. As an example, consider the program on the right. Assuming MPC first obtains the interleaving ${𝙲}^{}(a>0)\cdot {𝚆}^{}(x,1)\cdot {𝚁}^{}(x)$, it will then generate the constraint $a\le 0\wedge \mathrm{𝚟𝚊𝚕}({𝚁}^{}(x))=2$, aiming to uncover the assertion violation. While this constraint (and all paths stemming from it) are infeasible, MPC cannot drop it, as some of the paths under the “else” branch could have been writing $x:=\mathrm{\hspace{0.33em}2}$.

The closest works to ConDpor are those that aim to combine DPOR and CT. One of the such attempts was jCUTE [60]. Unlike ConDpor, jCUTE uses a non-optimal DPOR (and therefore explores redundant executions), and does not support weak memory consistency. Another work is that of Schemmel et al. [58], who combine quasi-optimal partial order reduction with CT. However, the resulting algorithm (PorSe) is not optimal, does not support weak memory consistency, has exponential memory requirements, and, since it does not use concrete execution, incurs a costly and unnecessary extra query to the SMT solver upon each symbol constraint evaluation. In our extended version [44] (App. A.5), we present a comparison between ConDpor and PorSe using the SV-COMP benchmarks. This comparison shows that, on average, ConDpor reduces the number of explored executions by $72\%$ compared to PorSe across SV-COMP benchmarks.

We presented ConDpor, a sound, complete and optimal algorithm that integrates concolic execution into dynamic partial order reduction. ConDpor uses execution graphs for backtracking on both scheduling and symbolic constraints, and offloads all manipulation of symbolic expressions to the underlying language’s runtime. ConDpor significantly outperforms DPOR approaches that explicitly enumerate the values of a data domain (even with that domain is small), and can verify challenging concurrent data structures.