Maximizing concurrency bug detection in multithreaded software programs

Patent metadata

Field	Value
Publication number	US-9792161-B2
Application number	US-201414553056-A
Country	US
Kind code	B2
Filing date	Nov 25, 2014
Priority date	Nov 25, 2014
Publication date	Oct 17, 2017
Grant date	Oct 17, 2017

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.

First claim

The invention claimed is:

1. 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.

2. The system of claim 1 , wherein the instructions are further executable by the hardware processor to:
order the order and branch variables in an order of execution according to the maximal causal model; and
repeat the generating the formula for a plurality of trace properties, thus enabling the constraint solver to detect multiple concurrency bugs.

3. The system of claim 1 , wherein the concurrency bug comprises a data race, and wherein the trace property comprises a conflicting operation pair of events from different threads being executed in succession.

4. The system of claim 3 , wherein the formula encodes all feasible traces corresponding to each respective of a plurality of data races.

5. The system of claim 4 , wherein the instructions, when executed by the hardware processor to generate the formula, further: generate a conjunction of sub-formulae over the order variables, the sub-formulae selected from at least one of: (i) must happen-before (MHB) constraints, (ii) lock mutual exclusion constraint, or (iii) race constraints.

6. The system of claim 5 , wherein the MHB constraints include: (i) a begin event, which can happen only as a first event in a first thread and only after the thread is forked by a second thread; and (ii) an end event, which can happen only after an end event of a joined thread of the first and second threads.

7. The system of claim 5 , wherein the lock mutual exclusion constraint requires that two sequences of events protected by an identified lock do not interleave, the sequences of events comprising acquire and release events.

8. The system of claim 5 , wherein the race constraints comprise: (i) that each conflicting operation pair of events are executed in succession; and (ii) a conjunction of two control flow constraints specifying data-abstract feasibility of the conflicting operation pair of events, wherein the data-abstract feasibility ensures each read event that must happen before any of the conflicting operation pairs of events satisfies a data-consistency constraint comprising that each read retrieves an identical value as the respective read retrieves within the input trace.

9. 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.

10. The method of claim 9 , wherein the branch events occur between the data events within the feasible traces through the program.

11. The method of claim 9 , wherein the maximal causal model incorporates a sequential consistency memory model, and wherein the formula encodes the concurrency and branch constraints as a set of first-order logical constraints.

12. The method of claim 9 , wherein the concurrency bug comprises a data race, and wherein the trace property comprises a conflicting operation pair of events being executed in succession, without intervening events.

13. The method of claim 12 , wherein assigning the order variables comprises assigning the order variables to only data events that stem from branch events leading to race-related op

Assignees

• Univ Illinois

Inventors

• Huang Jeff
• Rosu Grigore

Classifications

• G06F11/366 Primary

  using diagnostics (G06F11/0703 takes precedence) · CPC title

• G06F11/008

  Reliability or availability analysis · CPC title

• G06F9/524 Primary

  Deadlock detection or avoidance · CPC title