US 9,792,161 B2Granted

Maximizing concurrency bug detection in multithreaded software programs

AssigneeThe Board of Trustees of the University of Illinois

InventorsJeff Huang, Grigore Rosu

Life of this patent

Estimating the term…

Loading patent…

Abstract

Disclosed systems and methods incorporate a sound and maximal causal model with control flow information for maximum concurrency error detection in general multithreaded programs. The maximal causal model may be based on or integrated with the sequential consistency model, and form the basis for a formula including branch and order variables as first-order logical constraints solvable by an SMT solver for detection or prediction of concurrency errors. The disclosed systems and methods also relate to predictive trace analysis (PTA) for predicting generic concurrency properties using local traces (as opposed to a global trace) through the threads of a multithreaded program. By uniformly modeling violations of concurrency properties and the thread causality as constraints over events, and using an SMT solver, the systems and methods predict property violations allowed by the causal model.

Claims21

Dependent claims

A system comprising:

a hardware processor;
a constraint solver executable by the hardware processor;
non-transitory computer-readable medium storing instructions executable by the hardware processor to maximize detection of concurrency bugs in different threads of a multithreaded software program (“program”), the instructions and the program executable by the hardware processor to:
formulate detection as a constraint-solving problem by:
assigning an order variable to each of a plurality of events in an input trace of the program;
ordering the order variables to corresponding events in an order of execution according to a maximal causal model, which captures a set of feasible traces that can be generated by a thread of a multithreaded program capable of generating the input trace and by a second input trace, wherein the input trace and the second input trace are thread-local traces;
defining the maximal causal model with multiple axioms comprising prefix closedness and local determinism, wherein prefix closedness is that prefixes of a feasible trace are also feasible, and local determinism is that threads of the program behave deterministically;
further defining local determinism to include:
data-abstract equivalence of the input trace and the second input trace of the program, where the input trace and the second input trace are equal except for data values in read events and write events of the plurality of events;
and
a branch axiom, in relation to a first branch event of the plurality of events and using the data-abstract equivalence, comprising when read events in the input trace for the thread equal the read events in the second input trace for the thread, the first branch event in the second input trace is feasible;
and
generating a formula over the order variables and over a plurality of branch variables corresponding to branch events, including the first branch event, that captures the maximal causal model, control flow, and a trace property whose violation corresponds to a concurrency bug;
and
solve the formula with the constraint solver to determine whether the trace property is violated due to the concurrency bug, wherein employment of thread-local traces enables concurrency bug detection in multiple of the different threads in parallel, reducing runtime computation overhead of the hardware processor by at least ten percent.

12 more elements

A method comprising:

formulating, using a hardware processor of at least one computing device having non-transitory computer-readable medium for storing data and instructions, detection of a concurrency bug within different threads of a multithreaded software program (“program”) as a constraint-solving problem by:
assigning an order variable to each of a plurality of data events in an input trace of the program as concurrency constraints;
assigning a branch variable to each of a plurality of branch events of the input trace of the program as control flow constraints;
ordering the order variables and the branch variables in an order of execution according to a maximal causal model defining a maximal set of feasible traces inferred from the input trace and from a second input trace, which are executable by the program, wherein the input trace and the second input trace are thread-local traces;
defining the maximal causal model with multiple axioms comprising prefix closedness and local determinism, wherein prefix closedness is that prefixes of a feasible trace are also feasible, and local determinism is that threads of the program behave deterministically;
further defining local determinism to include:
data-abstract equivalence of the input trace and the second input trace of the program, where the input trace and the second input trace are equal except for data values in read events and write events of the plurality of events;
and
a branch axiom, in relation to a first branch event of the plurality of events and using the data-abstract equivalence, comprising when read events in the input trace for the thread equal the read events in the second input trace for the thread, the first branch event in the second input trace is feasible;
and
generating a formula over the order and branch variables that captures the maximal causal model, control dependency from the control flow, and a trace property whose violation corresponds to the concurrency bug, and
solving, using the hardware processor, the formula with a constraint solver to determine whether the trace property is violated due to the concurrency bug, wherein employment of thread-local traces enables concurrency bug detection in multiple of the different threads in parallel, reducing runtime computation overhead of the hardware processor by at least ten percent.

9 more elements

A non-transitory computer-readable storage medium storing instructions thereon that, when executed by a hardware processor, cause a computer system to perform a plurality of operations comprising:

formulating detection of a concurrency bug of different threads of a multithreaded software program (“program”) as a constraint-solving problem by:
assigning an order variable to each of a plurality of data events in an input trace of the program, as executed on the hardware processor, as concurrency constraints;
assigning a branch variable to each of a plurality of branch events of the input trace of the program as control flow constraints;
ordering the order variables in an order of execution according to a maximal causal model, which captures a set of feasible traces that can be generated by a thread of a multithreaded program capable of generating the input trace and by a second input trace, wherein the input trace and the second input trace are thread-local traces;
defining the maximal causal model with multiple axioms comprising prefix closedness and local determinism, wherein prefix closedness is that prefixes of a feasible trace are also feasible, and local determinism is that threads of the program behave deterministically;
further defining local determinism to include:
data-abstract equivalence of the input trace and the second input trace of the program, where the input trace and the second input trace are equal except for data values in read events and write events of the plurality of events;
and
a branch axiom, in relation to a first branch event of the plurality of events and using the data-abstract equivalence, comprising when read events in the input trace for the thread equal the read events in the second input trace for the thread, the first branch event in the second input trace is feasible;
and
generating a formula over the order and branch variables that captures the maximal causal model, control dependency from the control flow, and a trace property whose violation corresponds to the concurrency bug;
and
solving, using the hardware processor, the formula with a constraint solver to determine whether the property is violated due to the concurrency bug, wherein employment of thread-local traces enables concurrency bug detection in multiple of the different threads in parallel, reducing runtime computation overhead of the hardware processor by at least ten percent.

10 more elements

Dependencies are inferred from the claim text.