t if act

Ar en
t * Co m p let e
*

A ECDo
*
st
PoPP *

We
* P se * Consi

ll
*
cu m
eu
Production-guided Concurrency Debugging

Ev
e
R nt
ed
* Easy t o
alu d
at e

Nuno Machado Brandon Lucia Luı́s Rodrigues

INESC-ID, Instituto Superior Técnico, Carnegie Mellon University, USA INESC-ID, Instituto Superior Técnico,
Universidade de Lisboa, Portugal blucia@[Link] Universidade de Lisboa, Portugal
[Link]@[Link] ler@[Link]

Abstract different execution paths. Since this huge search space makes com-
Concurrency bugs that stem from schedule-dependent branches are plete exhaustive testing infeasible, some failures will likely mani-
hard to understand and debug, because their root causes imply not fest in deployment.
only different event orderings, but also changes in the control-flow This work aims at exposing failures that may include schedule-
between failing and non-failing executions. We present Cortex: a dependent branches, without ever needing to observe a failing ex-
system that helps exposing and understanding concurrency bugs ecution. We leverage the observation that a failing schedule typi-
that result from schedule-dependent branches, without relying on cally deviates in only a few critical ways from a non-failing sched-
information from failing executions. Cortex preemptively exposes ule [33]. Our main insight is to expose new failing schedules by per-
failing executions by perturbing the order of events and control- turbing the order of events and certain branch outcomes in a non-
flow behavior in non-failing schedules from production runs of failing schedule. We further leverage abundant production runs of a
a program. By leveraging this information from production runs, program on deployed systems to guide our search of the enormous
Cortex synthesizes executions to guide the search for failing sched- space of possible execution schedules [5]: our production-guided
ules. Production-guided search helps cope with the large execution search for a failing schedule targets schedules very similar to a non-
search space by targeting failing executions that are similar to ob- failing schedule observed in production.
served non-failing executions. Evaluation on popular benchmarks We present Cortex1 , a system that helps exposing and under-
shows that Cortex is able to expose failing schedules with only a standing concurrency bugs using traces from normal, non-failing
few perturbations to non-failing executions, and takes a practical production executions. Figure 3 depicts an overview of our system.
amount of time. Cortex starts by collecting a set of per-thread path profiles from one
or more production runs. Each profile is used to guide a symbolic
execution of the program producing a symbolic event trace for each
1. Introduction thread that is compatible with the original execution’s control-flow.
Concurrent programming has hit the mainstream, because it en- Cortex combines an execution’s per-thread symbolic traces to im-
ables software to take advantage of parallelism in pervasive mul- plement production-guided search for a new, failing execution –
ticore computer architectures. Unfortunately, expressing concur- one that may depend on both schedule and path conditions.
rency in multi-threaded code is more challenging than writing Cortex’s production-guided search is a novel approach to select-
sequential code. The reason is that multi-threaded programs of- ing a path and schedule. Starting from the computed symbolic ex-
ten permit many different schedules of operations from different ecution, Cortex systematically reorders events in the schedule and
threads. Hence, a program’s outcome may vary from run to run, inverts the outcome of certain branches, with a preference for ex-
depending on the executed schedule. Many schedules are correct, ecutions that are most similar to the original. Cortex determines
but some failing schedules result in misbehavior, like a crash or if a perturbed execution is feasible using a constraint system for a
data corruption. Satisfiability Modulo Theories (SMT) solver. The constraint system
A large body of research has focused on exposing failing sched- encodes synchronization, data-flow, event ordering, and the occur-
ules and exhaustively testing for failures [12, 15, 17, 47]. To find a rence of a failure. If the SMT formulation is satisfiable, the exe-
failing schedule is a challenging problem: the subset of thread or- cution that Cortex generated is feasible and the system reports the
derings that lead to the failure often corresponds to a tiny portion new failure. If the SMT formulation is infeasible, Cortex moves on
of the space of possible execution schedules and those few failing to a different perturbation of the execution’s schedule and branch-
schedules may manifest rarely. Furthermore, the variation in the ing behavior. Cortex favors executions that vary only slightly from
schedule in a failing execution may cause a variation in the execu- the original, observed execution, putting its focus on failures that
tion’s data flow, and subsequently, its control-flow. Such schedule- very nearly manifested in a previous execution.
dependent branches further complicate the task of exposing failing In this paper, we consider failures to be violations of assertions
schedules, because one has to explore not only the space of possible in the code. We argue that it is common for developers to ship
thread schedules for a given execution path, but also the space of code with assertions. For instance, Google pervasively uses trac-
ing and assertions throughout live, production datacenter code via
Dapper [45]. Also, recent work showed that invariants can often
be derived automatically [24], which broadens the applicability of
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without Cortex.
fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice
and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be
honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to
lists, requires prior specific permission and/or a fee. Request permissions from permissions@[Link] or Publications
1 We have named our system Cortex after the cerebral cortex, which is a part
Dept., ACM, Inc., fax +1 (212) 869-0481.
of the human brain that receives and processes information from neurons to
PPoPP ’16, March 12-16, 2016, Barcelona, Spain
Copyright c 2016 ACM 978-1-4503-4092-2/16/03. . . $15.00 control several functions of the human body. Likewise, our system leverages
DOI: [Link] information from multiple production runs to expose concurrency bugs.
 In addition to exposing failing schedules, Cortex is also able (initially x = 0)
to isolate the failure’s root cause. The root cause of a failure is the
minimum sequence of events in the schedule that cause the program T1 T2
to fail. A failing schedule may contain many events and the failure’s 1: x++ 3: x = 0
root cause could be anywhere in the schedule, which makes debug-
ging a complex task. Failures resulting from schedule-dependent 2: assert(x > 0)
branches further exacerbate this problem, because the programmer Figure 1: Example of a multithreaded program with a schedule-
must reason about different events in a failing execution and in a dependent bug.
non-failing one.
Cortex leverages production-guided search to extend previous
work on differential schedule projections [33] and compute differ- The example is an atomicity violation, because the block of oper-
ential path-schedule projections (DPSPs). DPSPs zero in on the ations in T1 should execute atomically, without being interleaved
root cause of failures that stem from schedule-dependent branches by operations from T2, but the code fails to enforce the atomicity.
by reporting the differences between a failing and a non-failing Atomicity violations and other types of concurrency bugs (e.g. or-
schedule, including variations in their event orderings, data-flow dering violations and data-races) have been studied extensively in
behavior, and control-flow decisions. the literature [9, 14, 27–31, 38, 43, 53, 54] and we defer to prior
Our evaluation in Section 6 shows that Cortex is able to find work for a more thorough background on concurrency bug types.
failing schedules in concurrent programs by perturbing very few Regardless of the type, some concurrency bugs are strictly
branch conditions. Moreover, we show that Cortex’s production- schedule-dependent. The error in Figure 1 is an example of a
guided search reduces the number of attempts to expose concur- strictly schedule-dependent bug: threads in both the failing and
rency bugs by up to three orders of magnitude with respect to pre- non-failing schedules execute the same sequence of instructions,
vious state-of-the-art concurrency testing techniques [12, 17]. but the schedules differ in the threads’ operations interleaving.
In summary, this paper makes the following contributions: Unlike the bug in Figure 1, not all concurrency bugs are strictly
i) A cooperative scheme to collect and analyze thread path- schedule-dependent. Some concurrency bugs are path and schedule
profiles from production runs. dependent, instead, like the example in Figure 2. In the example, T1
ii) A novel, production-guided approach to exposing path and and T2 access four shared variables (x, y, w, and z). The program
schedule dependent failures by exploring variations in schedule and fails when it executes the schedule 8-1-2-3-4-9-10-5-6-7, which
control-flow behavior in non-failing executions. causes the value of x at line 7 to be 0 and violate the assertion. All
iii) A technique to synthesize new executions similar to ob- non-failing schedules for this program exhibit a different control-
served ones leveraging traces collected from production, as well flow path than the failing schedule, because the code must not
as symbolic execution. execute line 6, to guarantee that x > 0 at line 7. The key distinction
iv) An implementation of Cortex for Java and an evaluation, between this example and the example in Figure 1 is that the failing
with widely used benchmarks and real-world applications, showing execution requires a variation from the correct execution in both
that Cortex is efficient and effective for exposing and debugging the order of events (i.e., the schedule) and in the control-flow path
hard concurrency bugs. executed. The next section discusses the challenges of path and
The rest of the paper is organized as follows. Section 2 overviews schedule dependent bugs.
the background concepts most related to our work. Section 3
describes the Cortex system, namely its architecture and the (initially x = y = w = z = 0)
production-guided search used to find failing schedules. Section 4
provides a concrete example that illustrates how Cortex employs T1 T2
the production-guided search to expose a concurrency bug that
depends on schedule-sensitive branches. Section 5 discusses the 1: if(z > 0) 8: z = 1
implementation details. Section 6 presents the experimental eval- 2: w++ 9: if(w > 0)
uation results and discuss the main findings. Finally, Section 7 3: x=1 10: y=0
reviews the related work. 4: y=1
5: if(y == 0)
2. Motivation and Background
6: x--
Cortex exposes new concurrency bugs and helps their diagnosis.
7: assert(x > 0)
This section overviews concurrency bugs and debugging, as well
as techniques from prior work that form the foundation of Cortex. Figure 2: Example of a multithreaded program with a path and
schedule dependent bug.
2.1 Concurrency Bugs
Concurrency bugs are errors in code that permit operations from
different threads to execute in an order that causes the program 2.2 Challenges of Path and Schedule Dependent Bugs
to fail — concurrency bugs permit failing execution schedules. Testing for and debugging path and schedule dependent bugs is
Concurrency bugs include omitted and misused synchronization more complex and challenging than for strictly schedule-dependent
and inter-thread communication. For example, consider the mul- bugs. The reason for the difference is that path and schedule depen-
tithreaded program in Figure 1. This program has two threads (T1 dent bugs require searching not only for an inter-thread operation
and T2), which access a shared variable x. T1 increments the value order, but also for a new execution path that is compatible with such
of x (which is initially set to 0) and then checks whether this value a failing schedule.
is greater than 0. In turn, T2 simply writes 0 to x.
This program has two possible outcomes: it either validates or Testing. Stateless model checking systems like con2colic test-
violates the assertion at line 2, depending on the order in which ing [11] and MCR [17] leverage SMT constraint solving to expose
threads execute their operations. The program fails for the sched- concurrency bugs. By encoding the possible thread schedules for a
ule 1-3-2 and ends correctly for the schedules 3-1-2 and 1-2-3. given execution path as a constraint system, these systems are able
to check properties and search for failures in a set of schedules, for Therefore, for a given execution control-flow, the constraint
a given single execution path. Other systematic concurrency testing system can be used to obtain an execution schedule that either fails
techniques systematically exercise many different schedules for the or ends successfully, depending on whether the failure condition
same control-flow path [16, 34]. Systematic schedule search works is satisfied or not, respectively. In the following, we describe each
for strictly schedule-dependent bugs, but path and schedule depen- sub-formula in more detail.
dent bugs require a tool to simultaneously explore all control-flow
Path Constraint φpath is a conjunction of all threads’ path con-
paths to find a path and schedule that leads to the failure. This
requirement illustrates an important challenge: the space of paths ditions (i.e., branch outcomes), recorded during symbolic execu-
and schedules explodes with an execution’s length and quickly be- tion [4, 51]. For instance, a possible path constraint for an execu-
comes unwieldy and infeasible to search. In this work, we address tion of the program in Figure 2 would be [z > 0] ∧ [¬(y==0)] for
search space explosion using the local, production-guided search T1 and [w > 0] for T2.
technique that we describe in Section 3.3. Synchronization Constraints. φsync is divided into partial order
constraints and locking constraints.
Debugging. Debugging tools like CLAP [20] and Symbiosis [33] The former encode the happens-before relation [25] between or-
use symbolic execution and SMT constraint solving for automatic dering synchronization operations (e.g., signal, wait, join, fork). For
debugging. Both systems use per-thread path profiles from a con- instance, the constraints state that i) one thread’s start/join event
crete failing execution to generate and replay a failing schedule. happens after another thread’s fork/exit event. Locking constraints
While CLAP is only focused on reproducing failures, Symbiosis encode mutual exclusion of code protected by a lock. These con-
is able to diagnose them as well, by systematically reordering op- straints match a thread’s unlock operations to a preceding unlock in
erations in a failing schedule to produce an alternate schedule that that thread.
does not trigger the failure. Symbiosis uses a differential analysis
of the alternate and the original schedule to isolate a failure’s cause Read-Write Constraints. φrw encodes the ordering and result of
and produce a differential schedule projection [33]. shared memory read and write operations. The read-write con-
Symbiosis and CLAP do not handle path and schedule depen- straints express the fact that a read from a variable returns the sym-
dent bugs: CLAP only computes failing schedules and Symbiosis’ bolic value written by the last write to that variable.
alternate schedules are required to adhere to the original control- For example, in Figure 2, if T1 reads the value 1 for the variable
flow of the original execution. Furthermore, both Symbiosis and z at line 1, then the most recent write to z must be the one at line 8
CLAP need a trace from a failing execution to work, which may be by T2 and, consequently, line 8 must execute before line 1.
hard to obtain. For instance, we ran the program in Figure 2 10,000
Memory Order Constraints. φmo determines the order in which
times and it did not fail a single time.
operations occur in a specific thread. In Cortex, we consider that
In this work, Cortex couples its production-guided search with
operations execute in program order, i.e. following a sequencial
symbolic execution and SMT solving ideas from Symbiosis and
consistent memory model. However, it is possible to express more
CLAP to address schedule and path dependent bugs without the
relaxed memory consistency models using slightly different con-
need to observe a failing execution. Section 7 provides a more
straints [20].
thorough comparison between Cortex and Symbiosis.
Failure Constraint. φassert corresponds to the condition that, if
2.3 Computing Schedules with Symbolic Execution and unsatisfied, indicates that an execution failed. For a failing execu-
Constraint Solving tion, Φfail , the failure condition must be violated (i.e., ¬φassert
Cortex leverages the multithreaded trace generation technique de- must hold). On the other hand, for a correct execution Φok , φassert
veloped in CLAP [20] and refined in Symbiosis [33]. The technique must be true. In Figure 2, ¬φassert corresponds to [x≤0] and
uses concrete, per-thread path profiles to guide a symbolic execu- φassert corresponds to [x>0].
tion of the program and generate per-thread symbolic traces (see
Section 3.2). The technique then builds an SMT constraint formu- 3. Cortex
lation that is based on the per-thread symbolic traces. When solved Cortex is an automated system for exposing and debugging path
by an off-the-shelf SMT solver, the formulation yields a failing, and schedule dependent failures in multithreaded programs. In
multi-threaded schedule. We defer a full discussion of this formu- contrast with other systems, Cortex does not need to observe a
lation to its original work [20], but provide background here. failed execution to isolate a failure. Instead, Cortex starts from
The constraint formulation has two kinds of variables: value a concrete, non-failing execution and explores alternative execu-
variables, which represent symbolic values returned by read opera- tions with only minor variations in their schedule and path from
tions, and order variables, which represent the order of operations the non-failing schedule. Using an initial, non-failing execution
in a schedule. The constraint system, Φfail , is a conjunction of five from production turns Cortex’s execution space exploration into a
sub-formulae: production-guided search for new failures. The exposed failures
Φfail = φpath ∧ φsync ∧ φrw ∧ φmo ∧ ¬φassert represent behavior that nearly happened in the observed execution,
and is, thus, more likely to happen in some future execution. Cortex
Briefly, φpath encodes the path conditions corresponding to the summarizes only the differences between the exposed failing exe-
path executed by each thread; φsync encodes inter-thread ordering cution and the original non-failing execution to clearly isolate the
imposed by synchronization; φrw encodes inter-thread ordering im- root cause of the failure to the developer.
plied by accesses to shared memory; φmo encodes possible opera- Cortex operates in four main steps: static analysis, trace col-
tion reorderings permitted by the memory consistency model; and lection, production-guided search, and root cause isolation. These
¬φassert encodes the failure constraint, which corresponds to an steps are illustrated in Figure 3 and described in the following sec-
assertion failure. tions.
Symbiosis [33] observed that a similar constraint formulation,
Φok , yields a non-failing schedule, without the failure condition 3.1 Static Analysis
negated:
Cortex starts by performing a static program analysis with two
Φok = φpath ∧ φsync ∧ φrw ∧ φmo ∧ φassert goals. The first goal is to instrument the beginning of each basic
 instrumented
program 01001
10011
10100
Static failing schedule
Analysis T1 T2
thread path profiles 1
... shared
variables
x@12
y@15
…
Wz@20
Rx@12
Ww@22
Wy@15=1
… Production-guided Root Cause
T1 T2 T1 T2
…
Schedule Search T1 T2 Isolation
thread symbolic
traces
3 4
... differential path-schedule
projection (DPSP)
Trace non-failing schedule
Collection
2

production runs Cortex

Figure 3: Overview of Cortex. 1) Cortex starts by instrumenting the program in order to allow capturing per-thread path profiles at runtime.
2) Cortex uses the path profiles, collected from multiple production runs, to guide a symbolic execution of the program and produce per-thread
symbolic event traces that adhere to the original executions’ control-flow. 3) Cortex leverages symbolic traces and SMT constraint solving to
conduct a production-guided search for a new failing execution that may depend on both schedule and path conditions. 4) Whenever Cortex
successfully uncovers a new failing schedule, it computes a differential path-schedule projection (using the uncovered failing schedule and a
non-failing schedule) to isolate the underlying bug.

thread symbolic
block in the program to trace the control-flow path followed in a traces
concrete execution. The second goal is to identify shared variables. Constraint
Schedule Wz@2 Constraint
Φfail
Rx@12
0
Wy@15=1
Model
Non-private (i.e., shared) variables and local variables derived from Exploration
Generation failing
Solving
those variables are marked as symbolic. Marking shared variables 1 2 constraint 3
model
as symbolic is a pre-requisite to Cortex’s symbolic trace collection thread Wz@20
Rx@12
Ww@22 branch
satisfiable
symbolic Wy@18=2
…
and generation mechanism (described next). traces
… flip
T1 T2

unsatisfiable
3.2 Trace Collection Execution
Synthesis
Given the infeasibility of exhaustively exploring all possible exe- 4 failing schedule

cutions of a program, Cortex narrows the exploration to favor those

paths that are most like those observed in production. Figure 4: Detail of production-guided schedule search.

Concrete Trace Collection. The version of the program instru-

mented by Cortex collects per-thread path profiles [20, 33]. A path- exploring all control-flow paths, as in a conventional symbolic ex-
profile is a sequence of basic blocks (i.e., control-flow outcomes) ecution, the symbolic execution in Cortex only follows branches
that was followed by the thread at runtime. taken in the original run. Cortex, thus generates per-thread sym-
Note that traces collected at this stage do not have any infor- bolic traces containing the same control-flow, synchronization, and
mation concerning thread scheduling, nor regarding which events shared memory accesses as the original, production run.
were executed during the production run. The reason is because Cortex maintains a database of per-thread symbolic traces gen-
recording the precise thread interleaving incurs heavy runtime erated from any set of observed, per-thread concrete traces. Cortex
overhead [19]. Hence, as previous work [20], we opt for a more organizes the traces in its database to facilitate its downstream
lightweight logging approach to capture runtime information. search, using the executions’ control-flow. Like symbolic execu-
Production runs with the same control-flow output identical tion tools [4, 48, 51], Cortex denotes a branch outcome as a binary
traces. However, paths with different control-flow may execute in value, with a 1 for branches taken and a 0 for branches not taken.
production. Cortex can collect a variety of paths from multiple, An execution path is, thus, uniquely defined by a string of bits.
different executions, potentially from distinct machines and execu- For example, consider a symbolic trace for thread T1 in Fig-
tion environments. This form of cooperative path collection enables ure 2 with path id 10. This path id indicates that the thread fol-
Cortex to leverage the execution diversity in multiple deployments lowed an execution path corresponding to the conditions [z>0] and
to gather a representative collection of traces. [¬(y==0)]. Note that the 0 in the path id means that the corre-
Symbolic Trace Generation. Cortex uses symbolic execution to sponding path condition evaluates false during the execution, hence
generate per-thread, symbolic traces from the collected, per-thread, the negation symbol in the condition [¬(y==0)].
concrete traces. Cortex augments the collected, per-thread path
traces offline with information about shared variables from its static 3.3 Production-Guided Search
analysis. Cortex marks as symbolic all shared variables and lo- After gathering the path profiles from production runs and generat-
cal variables that depend on shared variables. These symbolic an- ing their corresponding per-thread symbolic traces, Cortex starts its
notations mean that later, when Cortex does symbolic execution, search for alternate, failing executions. Figure 4 illustrates Cortex’s
reads and writes to these variables manipulate symbolic expres- search procedure.
sions, rather than concrete values. Cortex’s search is guided by production in two ways. The first
Cortex performs a symbolic execution of the program, guiding way is schedule exploration, during which Cortex searches multi-
each thread’s symbolic execution by its path trace. In other words, threaded executions compatible with the set of per-thread symbolic
the symbolic execution proceeds solely across the execution path traces from some observed execution. If schedule exploration fails
indicated by its corresponding path profile. As a result, instead of to surface any new failures, for any traces in Cortex’s database,
Cortex uses execution synthesis as a second form of production- T1
T1 T2
guided search. Cortex synthesizes new multi-threaded executions B 1
by modifying the control-flow behavior in one or more of the B 1
0
C
0 1
threads’ traces. Cortex then performs schedule exploration on the 0 A 1
new synthesized execution. 0
schedule A
3.3.1 Schedule Exploration 1 assert
T1 T2 0
Given a combination of per-thread, symbolic path traces — from ... b) flip branch A
either a production run or a synthesized execution — Cortex checks ... C
assert
if any interleaving of operations that make up those paths leads to a B T1 T2
...
failure. First, Cortex selects an assertion from the trace at random. A T2 B 1 C
Next, Cortex builds a Φfail constraint model (from Section 2.3) ... 0 0 1

with the symbolic information contained in the traces and the assert //ok C A 1
condition in the assertion. 0 1
0
Cortex uses an SMT solver to check the satisfiability of the gen-
assert
erated constraints. If the model is satisfiable, then the solver outputs
the failing schedule. If the constraints are unsatisfiable, then there a) initial non-failing schedule c) flip branches B and C
is no schedule that leads to a failure of the selected assertion for
the given control-flow trace. Cortex applies this schedule explo- Figure 6: Branch condition flipping. Arrows and dashed arrows
ration procedure to each execution in its database, reporting newly represent conditional and unconditional control-flow, respectively.
exposed failures as they manifest. Thicker arrows represent the execution path followed by the thread.
Note that only performing schedule exploration on execu-
tions observed in production will only expose strictly schedule- tic continues considering complexes of increasingly many branch
dependent failures. However, Cortex is not limited to these failures inversions up to the configurable threshold number D.
only, because it goes beyond schedule exploration with its execu- Figure 6a) illustrates Cortex’s path synthesis heuristic. There
tion synthesis technique. are two threads, T1 and T2, and three branch conditions ( A and
3.3.2 Execution Synthesis B belong to T1, and C belongs to T2). According to the non-
failing schedule in Figure 6a), the closest branch to the assertion
Execution synthesis generates new per-thread control-flow traces is A , followed by B and C . The figure also shows that the path
corresponding to entirely novel executions by making small pertur- conditions in the threads’ symbolic traces are 10 (i.e., taken, not
bations in the control-flow observed in production runs. By synthe- taken) and 1 (i.e., taken), respectively for T1 and T2.
sizing new executions with control-flow variations, and then apply- Figure 6b) depicts the first branch condition that Cortex at-
ing schedule exploration to those synthesized executions, Cortex tempts to flip, namely A . As a result, Cortex generates a new
can expose new failures that are schedule and path dependent. control-flow path for T1 containing 11, while the trace for T2
Synthesizing executions presents two main challenges: i) how to remains the same. Later, the path synthesis heuristic may gener-
decide which alternate execution to synthesize, and ii) how to ob- ate another control-flow path by flipping the outcome of multiple
tain per-thread symbolic traces for the alternate execution to be syn- branches. Figure 6c) illustrates a case where Cortex simultaneously
thesized. Cortex addresses the first challenge with a novel heuristic flips branches B and C , resulting in a path for T1 containing 00
denoted branch condition flipping. The heuristic perturbs the orig- and a path for T2 containing 0.
inal control-flow observed during some production run, generating After synthesizing a new control-flow path, Cortex needs a new
one or more new per-thread traces. Cortex addresses the second symbolic trace for the newly synthesized path. Cortex can either
challenge using a combination of its trace database and symbolic find an existing symbolic trace, or synthesize a new symbolic trace.
execution. If Cortex has already observed some execution in which
a thread followed the perturbed control-flow path, Cortex uses the Finding a Symbolic Trace. The easiest way for Cortex to obtain a
per-thread symbolic trace for that path that is in its database. If symbolic trace that is compatible with a newly synthesized control-
Cortex has not observed the perturbed path in some prior execu- flow path is to look for one in its database of traces collected
tion, Cortex synthesizes a new symbolic path trace by running a from any prior, production execution. A compatible trace from the
symbolic execution, guided by the perturbed control-flow trace. database must have an identical prefix of branch outcomes as the
original, unperturbed trace, but must have the opposite outcome for
Synthesizing a Control-flow Path. Cortex’s synthesizes a new
the branch or branches flipped by the path synthesis heuristic.
control-flow path by inverting path conditions on an existing path
When there is more than one compatible, symbolic trace in the
that are within a given distance from the selected assertion.
database, Cortex considers each of them in turn, up to a maximum
To identify the path conditions corresponding to the branches
of N possible traces, and in ascending order of their path length.
closest to the assertion, Cortex selects an execution from its
The tuple (D, N ) allows tuning the search in terms of the number
database and generates a non-failing, multi-threaded schedule us-
of different branches conditions flipped and the number of possible
ing the Φok constraint model (from Section 2.3). Cortex examines
traces that are attempted for each branch flip. A high D means that
the resulting schedule and selects the D branches closest to the
Cortex flips path conditions far from the assertion, and a high N
assertion as candidates for inversion.
indicates that Cortex explores many paths with a common prefix.
Cortex’s path synthesis heuristic generates paths that are most
similar to the original path trace first, generating new paths in order Synthesizing a Symbolic Trace. When there is no trace in the
of deviation from the original. The first paths that the heuristic gen- database that matches a newly synthesized control-flow path,
erates are ones with a single branch outcome flipped, and Cortex Cortex synthesizes a compatible trace using guided symbolic ex-
gives priority to paths in which the flipped branch is closer to the ecution. Cortex uses the newly synthesized control-flow path to
assertion. Next, the heuristic generates new paths with two branch guide a symbolic execution of the thread up to, and including the
flips, again, prioritizing new paths with lower total distance be- flipped branch or branches. After reaching the flipped branch in
tween branch flips and the assertion. Cortex’s path synthesis heuris- the symbolic execution, Cortex has no information about which
a) T1 T2 b) c) T1

8: z = 1 Symbolic Traces Symbolic Traces Symbolic Traces -

1: [z > 0]
1 (Production Run 1) (Production Run 2) (Production Run 3)
9: [w > 0]
0 2: w++ 1 0 1
0 T11: 10 T21: 1 T12: 10 T22: 0 T13: 00 T23: 0
3: x = 1 10: y=0 1: [z > 0] 8: z = 1 1: [z > 0] 8: z = 1 1: [¬(z > 0)] 8: z = 1 0 0
4: y = 1 2: w++ 9: [w > 0] 2: w++ 9: [¬(w > 0)] 3: x = 1 9: [¬(w > 0)]
EXIT 3: x = 1 10: y = 0 3: x = 1 4: y = 1 T13 T11, T12
5: [y == 0]
1 4: y = 1 4: y = 1 5: [¬(y == 0)]
0 5: [¬(y == 0)] 5: [¬(y == 0)] 7: assert(x > 0) //ok T2
6: x-- 7: assert(x > 0) //ok 7: assert(x > 0) //ok
-
7: assert(x > 0)
0 1
EXIT T22, T23 T21

d.1) initial non-failing schedule: d.2) Run 4: T1:11 is synthesized, d.3) Run 5: T1:00 and T2:0 from d.4) Run 6: T1:10 and T2:1 from d.5) Run 7: T1:01 is synthesized, d.6) Run 8: T1:11 is synthesized,
T1:10 and T2:0 from trace DB T2:0 from trace DB trace DB trace DB T2:0 from trace DB T2:1 from trace DB
T1 T2 T1 T2 T1 T2 T1 T2 T1 T2
T1 T2 - - - - - - - - - -
Trace DB

Trace DB

Trace DB

Trace DB

Trace DB
Trace DB

- -
0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1
0 1 0 1 T22 T22 T21 T22
0 0 1 0 0 1 0 0 1 0 1 0 1 0 0 1 T21
T22
0 0 SST T13 T12 SST SST
T12
T1 T2 T1 T2 T1 T2 T1 T2 T1 T2
T1 T2 8: z = 1 1: [¬(z > 0)] B 8: z = 1 1: [¬(z > 0)] B 8: z = 1
8: z = 1 9: [¬(w > 0)] C 8: z = 1 1: [z > 0] B 8: z = 1 1: [z > 0] B
9: [¬(w > 0)] C
1: [z > 0] B 9: [¬(w > 0)] C 2: w++ 9: [¬(w > 0)] C 2: w++
1: [z > 0] B 2: w++ 3: x=1 9: [w > 0] C 3: x = 1 3: x = 1
2: w++ 3: x=1 4: y=1 10: y=0 4: y = 1 4: y = 1
3: x=1 4: y=1 5: [¬(y == 0)] A 3: x = 1 5: [y == 0] A //infeasible 9: [w > 0] C
4: y=1 5: [y == 0] A //infeasible 7: 4: y = 1
¬ assert(x > 0) //infeasible 10: y=0
5: [¬(y == 0)] A 5: [¬(y == 0)] A 5: [y == 0] A
7: assert(x > 0) 7: ¬ assert(x > 0) //infeasible 6: x--
example of possible infeasible schedules explored by the SMT solver 7: ¬ assert(x > 0) //feasible!

Figure 5: a) Schematic view of the program in Figure 2: boxes represent basic blocks, arrows depict conditional jumps (0 means false and 1
means true), dashed arrows depict unconditional jumps, round shapes represent program’s exit points, and [z > 0] represents a path condition;
b) Per-thread symbolic traces path for three different correct production runs. T11 :10 indicates that the trace for thread T1 from production
run 1 has path id 10; c) Trace database, with per-thread path ids organized into prefix trees. The node label “-” indicates the root of the prefix
tree. d) Production-guided schedule search employed by Cortex to find the failing schedule. SST stands for synthesized symbolic trace.

control-flow path to follow. Cortex allows the symbolic execution common to both the failing and non-failing schedule. Cortex then
to run freely, exploring all paths, as in classical symbolic execu- examines data-flow in both traces and reports only data-flow edges
tion [4, 23, 51]. We heuristically stop the symbolic execution when that exist in one trace, but not the other. Control-flow variations are
it reaches the assertion or program exit along any path. We also highlighted as data-flow variations involving operations that only
stop symbolic execution after a configurable threshold timeout, to executed in one trace, but not the other. DPSPs are helpful for de-
prevent the path explosion problem from hindering Cortex. bugging, because they allow developers to see only a very small
As an example, consider the scenario where Cortex has to syn- number of relevant operations and data movement events, rather
thesize the symbolic trace for T1 required in Figure 6b). Cortex than forcing them to pore over a full execution schedule. Further-
would run the program symbolically, forcing T1 to take the branch more, DPSPs illustrate the failure alongside a very similar, but non-
1 for the path condition B , as well as for path condition A . As T1’s failing execution. The side-by-side comparison helps understand
execution ends with the assertion right after A , Cortex would out- the failure and aids in debugging.
put a symbolic trace for T1 that is compatible with the previously
unobserved control-flow path 11. 4. Running Example
This section synthesizes the entire Cortex debugging workflow
3.4 Root Cause Isolation using a detailed running example. Figure 5 shows how Cortex
Like prior systems on systematic concurrency testing [12, 17], automatically computes the root cause of the failure in Figure 2.
Cortex is able to report a newly exposed failing schedule, but unlike
Static analysis. Cortex’s static analysis identifies and instruments
prior systems, Cortex also reports a concise summary of the fail-
basic blocks and shared variables. Figure 5a shows the program’s
ure’s root cause. To summarize a failure’s root cause, Cortex com-
control-flow graph. In the example code, z, w, y, and x are marked
putes and reports a differential path-schedule projection (DPSP).
as symbolic.
DPSPs are an extension of differential schedule projections, devel-
oped in Symbiosis [33]. Cortex computes DPSPs by analyzing an Symbolic trace collection. The program executes in production,
exposed failing execution and the original, non-failing execution potentially many times, and a path profile for each thread is col-
that it was derived from. A DPSP reports the salient differences lected from each execution. From the path profiles, Cortex pro-
between the failing and non-failing schedule, including variation duces symbolic traces. Using symbolic execution, Cortex identi-
in their event orderings, data-flow behavior, and control-flow deci- fies each branch condition evaluated by each thread (depicted in
sions. The key difference between DPSPs in this work and DSPs in square brackets in Figure 5a) and symbolic execution follows those
prior work is that DSPs do not incorporate differences in control- branches according to the path profile. The symbolic execution pro-
flow between a failing and a non-failing execution, while, critically, duces a corresponding symbolic trace file; Figure 5b shows the
DPSPs include those differences. per-thread symbolic traces for three non-failing, production runs
Cortex produces the DPSP by computing a “diff” of the fail- with different execution paths. For instance, T11 :10 indicates that
ing schedule against the non-failing schedule. To compute a DPSP, the trace for thread T1 of production run 1 followed the control-
Cortex first compares the traces and prunes a prefix of operations flow path 10 (i.e., taken, not taken). After producing the per-thread,
symbolic traces, Cortex stores them in its trace database, depicted Non-failing schedule Failing schedule
in Figure 5c as a prefix tree.
T1 T2 T1 T2
Production-guided search. Figures 5d.1-d.6 illustrate how Cortex init: w = 0 2: w++
uses production-guided search to expose a failing schedule from the 9: [¬(w > 0)] 3: x = 1
non-failing, production schedules in its trace database. 2: w++ 4: y = 1
First, Cortex tries to obtain a failing schedule by exploring the 3: x=1 9: [w > 0]
4: y=1 10: y=0
schedules that are compatible with per-thread traces from produc-
5: [¬(y == 0)] 5: [y == 0]
tion runs that are in the trace database. Cortex applies its schedule 7: assert(x > 0) 6: x--
exploration algorithm (see Section 3.3.1) to production runs 1, 2 7: assert(x > 0)
and 3. In this example, there is no failing schedule that simply in-
terleaves the per-thread traces from any execution. Instead, Cortex Figure 7: Differential path-schedule projection.
needs to explore alternate executions that it derives from the ob-
served executions via execution synthesis.
Cortex begins its search by arbitrarily selecting production run schedule and on the right is the failing schedule. The DPSP does
2, which includes traces T12 and T22 . Using the traces from this not show operations that the two schedules have in common, in-
execution, Cortex generates a non-failing schedule by calling out stead highlighting only the parts of the execution trace that are dif-
to the SMT solver (Figure 5d.1). Cortex examines the non-failing ferent. The DPSP illustrates (in the bold lines) which control-flow
schedule to identify the branches that are closest to the assertion. outcomes differ between the schedules. The arrows in the figure
In the example, these branches are A , B (from trace T12 ) and C indicate data-flow edges that exist in one schedule, but not in the
(from T22 ). other. Together these properties of the DPSP show the root cause of
In Figure 5d.2, Cortex explores a different execution path by the failure: the failure is attributable to a change in the order of op-
flipping the branch condition A . The resulting path prefix is thus erations in the schedule, the data-flow changes resulting from those
obtained by inverting the second bit in the path of trace T12 , i.e., ordering changes, and the control-flow changes stemming from the
by changing the path condition 10 to the path condition 11. Cortex changes in data-flow.
checks its database for a symbolic trace for T1 with the path prefix In particular, the example shows that the branch condition
11, but, in this example, there is no such path in the database. [w>0], which evaluates false in the non-failing schedule, becomes
Consequently, Cortex needs to synthesize a new symbolic trace for true in the failing schedule, because w at line 9 reads the value
T1 with that prefix using symbolic trace synthesis. 1 (written by T1 at line 2) rather than the initial value 0. Conse-
Symbolic trace synthesis produces a symbolic trace T1:11. quently, T2 executes line 10 and sets y to 0, allowing the [y==0] to
Cortex uses the generated trace, together with T22 , to synthesize a be true at line 5. In contrast, in the non-failing schedule, T1 takes
new execution that we refer to as “run 4”. Cortex performs sched- the branch outcome corresponding to the condition ¬[y==0], be-
ule exploration on run 4, checking for interleavings of its threads’ cause y at line 5 necessarily reads the value 1 written at line 4.
operations that lead to a failure. The solver, however, yields unsatis- Finally, the DPSP shows that the assertion failure in the failing
fiable when evaluating the constraint system that encodes schedule schedule is due to the value of x being decremented by T1 at
exploration. The execution is infeasible because there is no feasible line 6. Conversely, the execution ends successfully in the non-
data-flow that allows the value of y at line 5 to be 0. failing schedule because the read of x at line 7 returns the value
To continue its search for a feasible schedule, Cortex again 1, previously written at line 3.
applies its path synthesis heuristic to generate a new control-flow Note that previous work in Symbiosis [33] simply reorders
path to explore (Figure 5d.3). The next branch to flip is B from events in the failing schedule to obtain an alternate, non-failing
trace T12 :10, which corresponds to the path 00. Cortex finds that its schedule and produce a differential schedule projection. As such,
trace database for T1 already contains a trace with that path prefix Symbiosis would not be able to generate a DPSP like the one of
(namely T13 ). Cortex uses the trace that it found to synthesize a Figure 7, because the failing schedule and the non-failing schedule
new execution (“run 5”), containing the newly synthesized trace for for this case comprise not only sequences of different events, but
T1 and trace T22 . Cortex then performs schedule exploration on run also differing path conditions.
5, continuing its search for a feasible, failing alternate schedule.
Cortex proceeds according to this approach. When schedule 5. Implementation
exploration yields no failing schedule, Cortex synthesizes a new
path, finds or synthesizes a new symbolic trace, creates a new We implemented a prototype of Cortex for Java programs. We use
execution, and re-applies schedule exploration. Figure 5d.4 and Soot [49] to perform the static analysis of Java bytecode, namely
Figure 5d.5 show subsequent applications of the approach, which to inject probes at the beginning of each basic block that allow
consist of runs 6 and 7, respectively. Note that, in Figure 5d.5, recording the path profile at runtime. Moreover, we leverage Soot’s
Cortex inverts the outcome of two branches, instead of a single thread-local objects (TLO) escape analysis to compute a sound
branch because, at this point in its search, it has exhausted all over-approximation of the set of shared variables in Java programs.
options involving only a single branch inversion. For each access on a shared variable we log an entry into a trace file
In Figure 5d.6, Cortex identifies a feasible, failing schedule for a containing the variable’s reference and the source code line. Cortex
newly synthesized execution that includes a synthesized symbolic consults the trace file during symbolic execution to identify which
trace for T1 (previously generated in run 4), and T21 . The traces operations should to treat symbolically.
for T1 and T2 in the execution for which there is a failing schedule Cortex’s production-guided schedule search and DPSP genera-
are the result of inverting the outcome of both branches A and C . tion were implemented in around 1,200 lines of C and C++ code
Note that without Cortex’s unique ability to explore both schedule that extended the publicly available version of Symbiosis [33]. We
and path variations, this failure would not have been exposed. extended Symbiosis to i) efficiently store symbolic traces from
multiple production runs, ii) expose strictly schedule dependent,
Root cause isolation. With the failing and non-failing schedules as well as path and schedule dependent concurrency bugs using
that are the result of production-guided search, Cortex generates traces from non-failing executions, and iii) perform symbolic trace
the DPSP depicted in Figure 7. On the left side is the non-failing synthesis during multiple path exploration.
 Cortex organizes its database of per-thread path traces, repre- Table 1: Benchmarks and performance. (LOC, #Threads, #Branches and
sented as bit strings, into tries (i.e., prefix trees). Tries are typically #Shared stand for lines of code, number of threads, number of branches, and
used for string retrieval and contain one node for every common number of shared variable accesses in each benchmark).
Profiling Log Symb. #Shared
prefix of stored strings. In Cortex’s implementation, if strings rep- Program LOC #Threads
Overhead Size Exec.
#Branches
Events
resenting two different traces share a prefix of n bits, the corre- Account 373 5 18.1% 1KB 0.6s 1 244
sponding executions followed the same path until the nth branch Critical 76 3 17.3% 260B 0.59s 4 36
decision. Cortex’s use of a trie to store traces minimizes the storage ExMCR 95 3 17.1% 170B 0.42s 4 56
required for large numbers of traces collected from production. PingPong 388 6 18.9% 226B 0.47s 5 66
Cortex uses Java PathFinder (JPF) [51] for symbolic execution Piper 280 5 18.6% 470B 1.11s 12 182
Airline 136 8 9.1% 252B 2.53s 15 77
and Z3 [7] to solve SMT constraints. We modified Java PathFinder Garage 554 7 6.7% 105KB 56.50s 22 284
to integrate it with the other parts of Cortex. First, when generating BubbleSort 376 6 13.4% 1KB 0.59s 24 161
symbolic traces for the production run per-thread path profiles, we Manager 219 5 16.4% 1.4KB 0.79s 56 331
ignore states that do not conform with execution path traced at run- Loader 146 11 2.4% 4KB 0.91s 56 386
time. This allows guiding the symbolic execution along the origi- StringBuf 1339 3 19.9% 1KB 1.13s 65 331
TicketOrder 246 4 9.5% 892B 0.85s 69 354
nal paths only. Second, when synthesizing new symbolic traces, we
BufWriter 272 5 20.4% 4.8KB 4.84s 89 1245
force JPF to follow original path solely up to the branch condition
Pool 10K 3 2.5% 960B 1.4s 21 198
flip point. After that, JPF switches to the traditional mode, where Cache4j (S) 2.3K 4 18.4% 3KB 1.02s 51 541
it explores all branches for each condition on symbolic variables, Cache4j (M) 2.3K 4 20% 15KB 2.01s 233 2364
using a breadth-first search heuristic. In this mode, we also set a Cache4j (L) 2.3K 4 21.7% 21KB 3.47s 309 3105
timeout to the exploration, in order to cope with path explosion.
Our Cortex prototype assumes that bugs in programs are ex-
pressed in the code as assertion invariants. Assuming that produc- We modeled the data collection of a production environment
tion software contains assertions is reasonable, as many major in- by executing each program 100 times and ensuring that none of
dustrial environments use production assertions and tracing [45]. the 100 executions triggered the bug. From these production runs,
In our experiments, we added these assertions when they were not we generated non-failing, symbolic traces and applied production-
initially present. For cases where the error had the following form guided search to expose a failing schedule for each benchmark.
on the left, we inject the assertion as indicated on the right: For Cache4j, we have experimented with different workloads to
if(cond){ if(cond){ assess the scalability of the constraint solving phase, as done in
//error assert(false) previous work [33]. Concretely, we re-ran this test case by varying
} //error the worker thread’s update loop to have 1 (small), 5 (medium), and
else{ } 10 (large) iterations.
... else{ The experiments were conducted on an 8-core, 3.5Ghz machine
} assert(true) with 32GB of memory, running Ubuntu 10.04.4.
...
} 6.1 Cortex is Practical and Efficient
Since JPF does not support arrays of symbolic length, we have The most important result is that for all of the benchmarks that
also modified these cases in our experiments to have a constant size, we considered, Cortex exposed a new failing execution based on
without affecting the original buggy behavior of the program. a small handful of observed, non-failing schedules, and did so in
The Cortex prototype is publicly available at [Link] a practical amount of time. Table 1 reports the time and storage
com/nunomachado/cortex-tool. overhead imposed by Cortex on production runs to capture path
profiles, as well as the time required to compute symbolic trace
collection. We report average time values across all executions
6. Evaluation (concrete and symbolic) for each benchmark.
Our evaluation of Cortex focuses on answering the following three Cortex’s path profiling overhead ranges from from 2.4% in
questions: Loader to 21.7% in Cache4j (L). The overhead is tolerable, even
for production, and similar to other prior work in this area [20, 33].
1. How efficient is Cortex in collecting symbolic traces from pro- Better software path profiling [3] or hardware support [50] are
duction runs? (§6.1) orthogonal techniques that would reduce this overhead.
Regarding space overhead, Cortex produces traces with sizes
2. How effective is Cortex’s production-guided search in finding
ranging from 170B in ExMCR to 105KB in Garage. The symbolic
concurrency bugs? (§6.2 and §6.3)
execution time is typically low as well: JPF produced a symbolic
3. How effective is Cortex in isolating the root cause of concur- trace in less than one minute for all programs. The programs with
rency bugs? (§6.4) larger path profiles are also the ones with more shared symbolic
events (e.g. BufWriter and Garage). Garage has a long traces and
We evaluated Cortex on the wide variety of multithreaded symbolic executions time because it uses busy waiting.
benchmarks shown in Table 1. These benchmarks have been used
in prior work on concurrency debugging [10, 13, 17, 18]. We used 6.2 Cortex Exposes Failures
11 programs from the IBM ConTest benchmark suite [10]; String-
Table 2 reports experimental results that allow assessing Cortex’s
Buf, a test driver of a bug in the Java JDK1.4 [17]; ExMCR, a
efficacy in finding failing schedules. Columns 3 and 4 of the table
micro-benchmark used by J. Huang et al. [17] to illustrate the ben-
together show that Cortex was able to find a failing schedule for all
efits of MCR against other stateless model checking techniques.
programs, including ones with failures dependent on both the path
We have also tested with two real-world application bugs, namely
and schedule (“ branch dependent ”). We now characterize Cortex’s
Pool (which consists of a data race in Apache Commons Pool) and
ability to expose new failures.
Cache4j (uncaught exception due to a data race). When present-
ing results, we sort test cases by “difficulty”, i.e, benchmarks with Strictly schedule dependent bugs. Column 3 of Table 2 shows
fewer branches and smaller search spaces appear first in the tables. that schedule exploration alone works for only 8 out of the
Table 2: Bug Finding Results. Column 2 shows the number of different binations of branch inversions. Note that the number of attempts is
correct production runs observed; Column 3 marks bug found by schedule actually greater than the product of the search parameters (D, N )
exploration only; Columns 4-8 provide details of production-guided search; for ExMCR, because Cortex needed to flip a combination of two
Last column depicts the average time to solve the corresponding satisfiable
branches simultaneously in order to trigger this failure2 . Garage
SMT system.
#Diff. Schedule Branch Dependent SMT required fewer attempts than D × N . The reason is that Cortex
Program Prod. Depend. #Branches #Synth. Solving selected traces for some paths that included redundant execution
Tries (D,N)
Runs Only Flipped Traces Time paths. Cortex discarded the redundant paths and found a failing
Account 1 3 29s schedule using the 4th trace for the 6th combination of branch flips.
Critical 23 3 6 (2,3) 2 4 <1s For BubbleSort and Loader, Cortex experimented with only one
ExMCR 1 3 6 (4,1) 6 6 <1s
trace per branch inversion, but it searched through 4 and 11 branch
PingPong 39 3 <1s
Piper 33 3 1 (1,1) 1 1 1s inversions, respectively, to compute the failing schedule. Pool, in
Airline 3 3 <1s turn, was the program for which Cortex required more tries and
Garage 2 3 9 (3,4) 6 6 2s flips of branch conditions to expose the failure. This is because
BubbleSort 26 3 4 (4,1) 4 4 <1s the only combination of branch inversions that allowed finding the
Manager 39 3 1 (1,1) 1 0 9s
failing schedule corresponded to flipping simultaneously the 4th
Loader 1 3 11 (11,1) 11 10 25s
StringBuf 12 3 9s and 5th branches closest to the assertion.
TicketOrder 47 3 1 (1,1) 1 0 1s In conclusion, these results show that search parameters (D, N )
BufWriter 57 3 2h56m affect significantly the number of attempts that production-guided
Pool 59 3 17 (5,4) 15 8 1s schedule search requires to expose the concurrency bug.
Cache4j (S) 11 3 5s
Cache4j (M) 29 3 1h30m Solving Time. The last column of Table 2 reports the average
Cache4j (L) 37 3 2h8m amount of time that the SMT solver took to solve the constraint
system (this value comprises only the case when the solver yielded
satisfiable, because reporting unsatisfiable took at most 3 seconds
17 benchmarks, namely Account, PingPong, Airline, StringBuf, for our test cases). The data shows that solving time is low for
BufWriter, and the three Cache4j scenarios. The reason schedule most cases, i.e., a couple of seconds. The exception are benchmarks
search alone is adequate for these benchmarks is that these eight BufWriter, Cache4j (M), and Cache4j (L). Once more, this is due to
cases include assertions of the form if(cond){assert(false)} the higher number of shared events in these programs. In particular,
else{assert(true)}. Cortex finds the failing schedule via the solver took almost 3 hours for BufWriter, because the SMT con-
schedule exploration alone because the failures are dependent only straint formulation for this program contains more than 920K read-
on strictly schedule dependent data flow to cond. write constraints and more than 6.5K locking constraints, which
have a big impact in the solving time for this kind of constraint
Efficiency of production-guided search. Column 4 in Table 2 systems [20, 33].
shows that production-guided search finds a failing schedule for
our path and schedule dependent bugs. Column 5 shows the num- 6.3 Cortex Compares Favorably to Systematic Testing
ber of branch outcome inversions Cortex performed to expose each
Unlike Cortex, systematic testing techniques search by fully ex-
failure. 3 out of 9 cases required inverting only the single clos-
ploring the space of possible executions. We directly compared
est branch to the assertion. This outcome supports our observation
Cortex to two state-of-the-art systematic testing techniques, namely
that failing executions are lurking in production, and that perturb-
MCR [17] and iterative context bounding with dynamic partial or-
ing production executions is an effective search strategy for these
der reduction (ICB-DPOR) [12]. Similarly to Cortex, MCR uses
otherwise elusive failures. The need for branch inversions, even in
an SMT constraint-based approach to efficiently explore the space
our production-guided search reinforces the fact that schedule ex-
of possible schedules of a multithreaded execution in search for
ploration alone is insufficient.
concurrency bugs. In particular, MCR starts from a concrete seed
Production run diversity. Collecting a diversity of production ex- interleaving and builds a maximal causal model that allows check-
ecutions expedites Cortex’s search for failures because it populates ing correctness properties on all execution schedules equivalent to
the trace database with traces, obviating the more costly execution that seed interleaving. To further explore the state space, MCR it-
synthesis step. Column 2 of Table 2 shows how many distinct non- eratively generates new non-redundant schedules by enforcing read
failing executions Cortex observed during 100 runs of each bench- operations to return different values. MCR then uses the newly gen-
mark. For all benchmarks except BufWriter and Pool, less than 50% erated schedules as seed interleavings for subsequent iterations.
of the collected executions are distinct. The data suggest that, even On the other hand, ICB-DPOR simply bounds the number of
in small numbers of runs, executions are diverse and Cortex can thread preemptions that can occur when systematically exercising
leverage a large trace database in a large deployment. different execution schedules, thus not accounting for redundant
interleavings (i.e. interleavings that produce the same values for
Search parameters. The column labelled as (D, N ) character- read operations).
izes parameters used during Cortex’s search for failures. Programs Our goal is to show that Cortex examines fewer executions
for which Cortex finds the failure with a single branch flip exhibit before exposing a failure than other approaches. We reproduce
the pair (1,1) for (D, N ). For those programs, Cortex exposed a results for MCR and ICB-DPOR reported by Huang et al. [17]
bug by inverting the outcome of the single branch that was closest for the subset of benchmarks that have been used with all three
to the assertion. systems. Table 3 reports the comparison.
In contrast, in Critical, ExMCR, Garage, BubbleSort, Loader, The data show that, for most cases, Cortex searches orders of
and Pool the optimal value for (D, N ) varies significantly. For Crit- magnitude fewer executions than ICB-DPOR, and considerably
ical, Cortex found the failing schedule after inverting two branch fewer than MCR. The standout is ExMCR; ExMCR is a micro-
conditions (the two closest to the assertion) and performed sched- benchmark that was designed to be adversarial to systematic con-
ule exploration using three different symbolic traces for each one
of the two paths. For ExMCR, Cortex was able to find the failing 2 We note that there are 2D − 1 different combinations of branch condition
execution in 6 attempts, but in this case it required 6 different com- flips that can be attempted for a given search parameter D.
Table 3: Comparison between Cortex and other systematic concur- Table 4: DPSP conciseness. Reduction achieved by Cortex in terms of
rency testing techniques. Data for MCR and ICB-DPOR as reported by number of data-flows and events with respect to full failing schedules (“*”
J. Huang et al. [17] (“*” indicates bugs that are schedule-dependent only). indicates bugs that are schedule-dependent only).
Shaded cells indicate the cases where Cortex outperforms the other systems. Program
#Data-flows #Data-flows #Events #Events
#Attempts to find failing schedule Full DPSP (%Red.) Full DPSP (%Red.)
Program
Cortex MCR ICB-DPOR Account* 139 6 (↓96%) 244 58 (↓76%)
Account* 1 2 20 Critical 13 7 (↓46%) 36 13 (↓64%)
ExMCR 16 8 (↓50%) 56 39 (↓30%)
ExMCR 6 46 3782
PingPong* 16 1 (↓94%) 66 5 (↓92%)
PingPong* 1 2 37 Piper 57 2 (↓96%) 182 51 (↓72%)
Airline* 1 9 19 Airline* 29 3 (↓90%) 77 18 (↓77%)
BubbleSort 4 4 400 Garage 139 26 (↓81%) 284 235 (↓17%)
StringBuf* 1 2 10 BubbleSort 69 15 (↓78%) 161 144 (↓11%)
Pool 17 3 6 Manager 142 32 (↓77%) 331 220 (↓34%)
Loader 179 21 (↓88%) 386 281 (↓27%)
StringBuf* 115 1 (↓99%) 331 40 (↓88%)
TicketOrder 183 45 (↓75%) 354 290 (↓18%)
currency testing systems. Cortex exposes the bug after searching BufWriter* 745 95 (↓87%) 1245 1216 (↓2%)
just 6 executions, substantially outperforming both other systems. Pool 73 34 (↓53%) 198 123 (↓38%)
The only benchmark where Cortex required more attempts to Cache4j (S)* 211 1 (↓99.5%) 541 11 (↓98%)
find the failing schedule than the other approaches was Pool. As Cache4j (M)* 862 3 (↓99.7%) 2364 1371 (↓42%)
mentioned before, for this program, Cortex was only able to trigger Cache4j (L)* 1139 3 (↓99.7%) 3105 1094 (↓65%)
the failure after inverting the 4th and 5th branches at the same time.
Hence, Cortex ended up spending time exploring combinations
of branch flips that, despite being closer to the assertion, were sider that the execution control-flow is only affected by thread inter-
ineffective to expose the failing schedule. leavings. Exposing concurrency bugs considering variable input in
We believe the aforementioned scenario to be infrequent in addition to schedule non-determinism is substantially more chal-
practice, as shown by the outcomes of the other benchmarks. There- lenging, because the search space now grows along two different
fore, we argue that the results in Table 3 further support our obser- dimensions: input and schedules.
vation production-guided search is effective. A possible way to address input non-determinism is to extend
Cortex to record the input during production runs, in addition to
6.4 DPSPs are Concise and Informative threads’ execution path. This way, symbolic traces could then be
aggregated in subsets according to their execution path and input.
We computed DPSPs for all of our benchmarks, using observed
Another approach is to mark as symbolic the variables that are
(and synthesized) non-failing schedules and corresponding failing
affected by the inputs of the program, in order to force Cortex to
schedules exposed by Cortex. We evaluated DPSPs by comparing
explore the space of possible inputs during symbolic execution.
the number of data-flows and events in the DPSPs to those in full
schedules. Table 4 summarizes our results. Long Executions. As shown in our experiments, when the execu-
The data show that DPSPs are simpler than full, failing sched- tion has a large number of shared events, the SMT solver can take
ules. DPSPs include only the salient differences between the fail- a long time to solve the constraint system. For long executions, this
ing and the correct executions, directing the developer’s attention problem is exacerbated and it can become hard to expose a failing
towards the most relevant events and the data-flows involved in schedule in a reasonable amount of time.
the root cause of the failure. On average, Cortex produced DPSPs To improve the scalability of Cortex’s constraint solving phase,
with 83% fewer data-flows and 50% fewer events than full sched- one could apply record-and-replay techniques [32, 37, 55] to cap-
ules. Considering benchmarks with path and schedule dependent ture lightweight information regarding the thread orderings ob-
bugs alone, the average reduction values are 72% and 35%, re- served at runtime. This data could then be used to prune the con-
spectively for data-flows and events. These results provide evidence straint model (by fixing some read-write linkages), without com-
that DPSPs are a useful asset for root cause diagnosis, not only for promising the ability to expose failing schedules.
schedule-dependent only failures, but also for schedule and path Alternatively, Cortex could leverage interference abstractions [46]
dependent failures. to make the constraint analysis more tractable. Interference abstrac-
tions allow computing under- and over-approximations of thread
6.5 Discussion interferences in a concurrent program. Moreover, interference ab-
The experimental results presented in the previous sections clearly stractions can be gradually refined to reduce the space of possible
demonstrate the benefits of Cortex in exposing and isolating path schedules when checking for properties [46].
and schedule dependent bugs. Nevertheless, there are still a few
challenges that need to be addressed in order to further improve 7. Related Work
Cortex’s applicability and scalability. We enumerate these chal-
A large body of prior work has studied debugging and testing of
lenges below and discuss possible research lines to address them
concurrent programs. In this section, we we reiterate some of the
in the future.
solutions discussed in Section 2.2 and overview other prior efforts
Non-Assertion Bugs. Our current Cortex prototype assumes that that are most related to Cortex.
failures manifest as assertion violations. Although assertions are
Cortex vs Symbiosis. Symbiosis [33] is a system that helps devel-
commonly placed in code during development, concurrency bugs
opers to understand and diagnose concurrency failures by comput-
might not always be expressed as invariant failures.
ing a differential schedule projection (DSP). DSPs are useful for
One can address this issue by extending Cortex’s constraint
debugging because they highlight the variations in data-flow be-
model to check for other type of concurrency bugs (e.g. data
tween a failing schedule and a non-failing schedule, which allows
races [17] or deadlocks) in addition to assertion violations.
isolating the bug’s root cause.
Input Non-determinism. In this paper, we assume that all pro- As referred in Section 2.2, Cortex and Symbiosis leverage sev-
duction runs are captured with a fixed input. Consequently, we con- eral similar techniques, namely guided symbolic execution, SMT
constraint solving, and differential analysis to isolate bugs. How- All of these techniques output a failing schedule and expose new
ever, we argue that these two systems are fundamentally different. concurrency bugs, but do not concisely summarize a failure’s root
A fundamental distinction of Cortex is that Symbiosis starts from cause, like Cortex.
a single failing execution and produces a single non-failing one. Another approach to testing multithreaded programs is test syn-
Symbiosis is, therefore, predicated on having evidence about the thesis. Test synthesis receives a suite of sequential tests as in-
existence of a bug and its location. In contrast, Cortex synthesizes put, and analyzes the traces from these sequential executions in
a failing execution from a set of failure-free executions. As such, order to generate bug-inducing multithreaded tests. Omen [40],
Cortex must explore a much larger search space of executions. Fur- Narada [42], and Intruder [41] use this approach to automatically
thermore, this space includes both branch and schedule variations: synthesize tests aimed at exposing deadlocks, races, and atomicity
another key distinction from Symbiosis, which is not able to handle violations, respectively. Note, however, that test synthesis tech-
path variations. niques still require multithreaded tests to be executed and analyzed
Finally, as Symbiosis cannot isolate path and schedule depen- with dynamic detectors [14, 35, 38] to find the concurrency bugs.
dent bugs like Cortex, we can say the DPSPs computed by Cortex
are more broadly applicable than the DSPs produced by Symbiosis. Symbolic execution and SMT constraints Symbolic execution
and SMT constraint solving form the core of Cortex’s sched-
ule search. Prior work has also used a combination of sym-
Cooperative tracing of production runs. Cortex’s cooperative bolic execution and SMT constraint formulations to determinis-
approach is inspired by prior work on cooperative tracing and de- tically replay concurrency failures [20], test multithreaded pro-
bugging. CBI [26], CCI [21], and Gist [22] log events (e.g., branch grams [11, 17], find atomicity violations [52] and identify schedule-
frequency, return values) from multiple production runs and use sensitive branches [18].
statistical predictors to isolate the bug’s root cause. LBR/LCR [2], However, none of the techniques above use cooperative trace
in turn, uses on low-overhead hardware extensions to maintain a collection and production-guided search.
short-term log of hardware events that are useful for production
run failure diagnosis. CoopREP [32] records partial logs from mul-
tiple user instances running a multithreaded program and combines 8. Conclusions and Future Work
that information to deterministically replay a concurrency error. We have presented Cortex, a system that is not only able to find
Aviso [29] uses statistical analysis of production-run event traces, concurrency bugs in programs, but also helps the programmer in
but with the orthogonal goal of avoiding failures, rather than expos- identifying their root cause. For this, Cortex generates differential
ing them. path-schedule projections (DPSPs) that capture the differences be-
Cortex benefits from information collected in production as tween non-failing and failing executions, even when threads follow
well. However, Cortex has more immediately exposed failures than different paths in each execution. These DPSPs have from 46% to
other cooperative techniques because it does not need the amount of 99% less data-flows than full failing executions, strongly simpli-
data required by statistical approaches. Cortex has also the advan- fying the task of identifying the branches that are involved in the
tage of being able to synthesize new execution traces as necessary. bug.
Moreover, most other cooperative systems require first observing a Contrary to most previous work, Cortex does not require a
failing execution, rather than exposing new ones. failure to be observed in production to avoid exploring the full
space of possible executions. Instead, it is able to use non-failing
Testing for concurrency bugs. Systematic concurrency testing executions from production runs as a starting point for exploration,
(SCT) is one approach to testing multithreaded programs. The two generating synthetic executions that are likely to expose a bug
most widely adopted SCT techniques are partial order reduction (when it exists). Interestingly, with the benchmarks used in the
(POR) and schedule bounding. POR [15] reduces the number of paper, Cortex was able to generate failing executions after a few
schedules that need to be explored without false negatives, by (more, precisely, from just 1 to 15) cleverly guided branch flips.
exploring only one of each group of partial-order-equivalent set In its current version, Cortex stops when a failing execution and
of executions. Dynamic POR techniques aim at improving the the corresponding DPSP are produced. In future versions, we plan
efficiency and effectiveness of POR by computing a persistent to search for, and compare, multiple failing executions, to enrich
set [6], sleep set [12], and source set [1] during systematic search. the information provided to the programmer.
Schedule bounding techniques strive to limit the set of sched-
ules examined during testing [8, 34, 39]. For instance, preemption Acknowledgements
bounding [34, 39] limits the number of preemptive context switches We would like to thank our shepherd Murali Ramanathan and the
that are allowed in a schedule. Delay bounding [8], in turn, bounds anonymous reviewers for their invaluable feedback. This work was
the amount of times a schedule can deviate from the scheduling partially supported by Fundação para a Ciência e a Tecnologia
defined by a given deterministic scheduler. (FCT), under project UID/CEC/50021/2013, and by a 2015 Google
CTrigger [36] attempts to reduce the interleaving space in ex- Faculty Research Award.
ploration by focusing the testing on unserializable interleavings,
which are interleavings that usually correspond to atomicity vio-
lations and have low probability of occurring outside a controlled References
environment. In turn, AtomFuzzer [35] relies on annotations pro- [1] P. Abdulla, S. Aronis, B. Jonsson, and K. Sagonas. Optimal dynamic
vided by developers to dynamically check for atomicity violations partial order reduction. In POPL’14, 2014.
in multithreaded programs. AtomFuzzer uses a random scheduler [2] J. Arulraj, G. Jin, and S. Lu. Leveraging the short-term memory
to choose an arbitrary thread to run at every program state, favoring of hardware to diagnose production-run software failures. In ASP-
interleavings that correspond to atomicity violation execution pat- LOS’14, 2014.
terns. RaceFuzzer [44] also employs random testing, but with the [3] T. Ball and J. R. Larus. Optimally profiling and tracing programs.
goal of finding data races. Similarly to AtomFuzzer, RaceFuzzer ACM Trans. Program. Lang. Syst., 16(4), July 1994.
combines a random scheduler with race detection techniques, in [4] C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic
order to guide an execution schedule towards potential racing pairs generation of high-coverage tests for complex systems programs. In
of statements. OSDI’08, 2008.
 [5] G. Candea. Exterminating bugs via collective information recycling. [33] N. Machado, B. Lucia, and L. Rodrigues. Concurrency debugging
In HotDep’11, 2011. with differential schedule projections. In PLDI’15, 2015.
[6] E. M. Clarke, O. Grumberg, M. Minea, and D. Peled. State space [34] M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar, and
reduction using partial order techniques. In STTT’98, 1998. I. Neamtiu. Finding and reproducing heisenbugs in concurrent pro-
[7] L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In grams. In OSDI’08, 2008.
TACAS’08/ETAPS’08, 2008. [35] C.-S. Park and K. Sen. Randomized active atomicity violation detec-
[8] M. Emmi, S. Qadeer, and Z. Rakamarić. Delay-bounded scheduling. tion in concurrent programs. In FSE’08, 2008.
In POPL’11, 2011. [36] S. Park, S. Lu, and Y. Zhou. Ctrigger: Exposing atomicity violation
bugs from their hiding places. In ASPLOS XIV, 2009.
[9] D. Engler and K. Ashcraft. RacerX: Effective, static detection of race
conditions and deadlocks. In SOSP’03, 2003. [37] S. Park, Y. Zhou, W. Xiong, Z. Yin, R. Kaushik, K. H. Lee, and S. Lu.
PRES: Probabilistic replay with execution sketching on multiproces-
[10] E. Farchi, Y. Nir, and S. Ur. Concurrent bug patterns and how to test
sors. In SOSP’09, 2009.
them. In IPDPS’03, 2003.
[38] S. Park, R. W. Vuduc, and M. J. Harrold. Falcon: Fault localization in
[11] A. Farzan, A. Holzer, N. Razavi, and H. Veith. Con2colic testing. In
concurrent programs. In ICSE ’10, 2010.
ESEC/FSE’13, 2013.
[39] S. Qadeer. Partial-order reduction for context-bounded state explo-
[12] C. Flanagan and P. Godefroid. Dynamic partial-order reduction for
ration. Technical Report MSR- TR-2007-12, Microsoft Research,
model checking software. In POPL’05, 2005.
2007.
[13] C. Flanagan and S. Qadeer. A type and effect system for atomicity. In [40] M. Samak and M. K. Ramanathan. Multithreaded test synthesis for
PLDI’03, 2003. deadlock detection. In OOPSLA ’14, 2014.
[14] C. Flanagan, S. N. Freund, and J. Yi. Velodrome: A sound and [41] M. Samak and M. K. Ramanathan. Synthesizing tests for detecting
complete dynamic atomicity checker for multithreaded programs. In atomicity violations. In ESEC/FSE 2015, 2015.
PLDI’08, 2008.
[42] M. Samak, M. K. Ramanathan, and S. Jagannathan. Synthesizing racy
[15] P. Godefroid. Partial-Order Methods for the Verification of Concur- tests. In PLDI 2015, 2015.
rent Systems: An Approach to the State-Explosion Problem. Springer-
Verlag, 1996. [43] S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson.
Eraser: A dynamic data race detector for multithreaded programs.
[16] P. Godefroid. Model checking for programming languages using ACM Trans. Comput. Syst., 15(4), Nov. 1997. ISSN 0734-2071.
verisoft. In POPL’97, 1997.
[44] K. Sen. Race directed random testing of concurrent programs. In
[17] J. Huang. Stateless model checking concurrent programs with maxi- PLDI’08, 2008.
mal causality reduction. In PLDI’15, 2015.
[45] B. H. Sigelman, L. A. Barroso, M. Burrows, P. Stephenson, M. Plakal,
[18] J. Huang and L. Rauchwerger. Finding schedule-sensitive branches. D. Beaver, S. Jaspan, and C. Shanbhag. Dapper, a large-scale dis-
In ESEC/FSE’15, 2015. tributed systems tracing infrastructure. Technical report, Google, Inc.,
[19] J. Huang, P. Liu, and C. Zhang. LEAP: Lightweight deterministic 2010.
multi-processor replay of concurrent java programs. In FSE’10, 2010. [46] N. Sinha and C. Wang. On interference abstractions. In POPL ’11,
[20] J. Huang, C. Zhang, and J. Dolby. Clap: Recording local executions 2011.
to reproduce concurrency failures. In PLDI’13, 2013. [47] P. Thomson, A. F. Donaldson, and A. Betts. Concurrency testing using
[21] G. Jin, A. Thakur, B. Liblit, and S. Lu. Instrumentation and sampling schedule bounding: An empirical study. In PPoPP’14, 2014.
strategies for cooperative concurrency bug isolation. In OOPSLA’10, [48] N. Tillmann and J. De Halleux. Pex: White box test generation for
2010. .net. In TAP’08, 2008.
[22] B. Kasikci, B. Schubert, C. Pereira, G. Pokam, and G. Candea. Failure [49] R. Vallée-Rai, P. Co, E. Gagnon, L. Hendren, P. Lam, and V. Sundare-
sketching: A technique for automated root cause diagnosis of in- san. Soot - a java bytecode optimization framework. In CASCON’99,
production failures. In SOSP’15, 2015. 1999.
[23] J. C. King. Symbolic execution and program testing. Commun. ACM, [50] K. Vaswani, M. J. Thazhuthaveetil, and Y. N. Srikant. A pro-
19(7), July 1976. grammable hardware path profiler. In CGO’05, 2005.
[24] M. Kusano, A. Chattopadhyay, and C. Wang. Dynamic generation of [51] W. Visser, C. S. Pǎsǎreanu, and S. Khurshid. Test input generation
likely invariants for multithreaded programs. In ICSE ’15, 2015. with java pathfinder. In ISSTA’04, 2004.
[25] L. Lamport. Time, clocks, and the ordering of events in a distributed [52] C. Wang, R. Limaye, M. Ganai, and A. Gupta. Trace-based symbolic
system. Commun. ACM, 21(7), July 1978. analysis for atomicity violations. In TACAS’10, 2010.
[26] B. Liblit, A. Aiken, A. Zheng, and M. Jordan. Bug isolation via remote [53] W. Zhang, C. Sun, and S. Lu. ConMem: Detecting severe concurrency
program sampling. In PLDI’03, 2003. bugs through an effect-oriented approach. In ASPLOS XV, 2010.
[27] S. Lu, J. Tucek, F. Qin, and Y. Zhou. AVIO: Detecting atomicity [54] W. Zhang, J. Lim, R. Olichandran, J. Scherpelz, G. Jin, S. Lu, and
violations via access interleaving invariants. In ASPLOS XII, 2006. T. Reps. Conseq: Detecting concurrency bugs through sequential
[28] S. Lu, S. Park, E. Seo, and Y. Zhou. Learning from mistakes: A errors. In ASPLOS XVI, 2011.
comprehensive study on real world concurrency bug characteristics. [55] J. Zhou, X. Xiao, and C. Zhang. Stride: Search-based deterministic
In ASPLOS XIII, 2008. replay in polynomial time via bounded linkage. In ICSE’12, 2012.
[29] B. Lucia and L. Ceze. Cooperative empirical failure avoidance for
multithreaded programs. In ASPLOS’13, 2013.
[30] B. Lucia, L. Ceze, and K. Strauss. ColorSafe: Architectural support
for debugging and dynamically avoiding multi-variable atomicity vio-
lations. In ISCA’10, 2010.
[31] B. Lucia, B. P. Wood, and L. Ceze. Isolating and understanding con-
currency errors using reconstructed execution fragments. In PLDI’11,
2011.
[32] N. Machado, P. Romano, and L. Rodrigues. Lightweight cooperative
logging for fault replication in concurrent programs. In DSN’12, 2012.