MAXIMIZING CONCURRENCY BUG DETECTION IN MULTITHREADED SOFTWARE PROGRAMS

摘要

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.

主权项

1. A system comprising:
at least one processor; a constraint solver executable by the at least one processor; non-transitory computer-readable medium storing instructions executable by the at least one processor to maximize detection of concurrency bugs in a multithreaded software program (“program”), the instructions executable by the at least one 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 multithreaded program capable of generating the input trace; andgenerating a formula over the plurality of order variables and over a plurality of branch variables corresponding to branch events that captures the maximal causal model, control flow, and a trace property whose violation corresponds to a concurrency bug; andsolve the formula with a constraint solver to determine whether the property is violated due to the concurrency bug.