Maximizing concurrency bug detection in multithreaded software programs

Jeff Huang (Inventor), Grigore Rosu (Inventor)

Research output: Patent


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.
Original languageEnglish (US)
U.S. patent number9792161
Filing date11/25/14
StatePublished - Oct 17 2017


Dive into the research topics of 'Maximizing concurrency bug detection in multithreaded software programs'. Together they form a unique fingerprint.

Cite this