Download Dynamic Invariant Generation for Multithreaded

Dynamic Invariant Generation for Multithreaded Programs
Arijit Chattopadhyay
(ABSTRACT)
We propose a fully automated and dynamic method for generating likely invariants from multithreaded programs and then leveraging these invariants to infer atomic regions and diagnose concurrency errors in the software code. Although existing methods for dynamic invariant generation
perform reasonably well on sequential programs, for multithreaded programs, their effectiveness
often reduces dramatically in terms of both the number of invariants that they can generate and the
likelihood of them being true invariants. We solve this problem by developing a new dynamic invariant generator, which consists of a new LLVM based code instrumentation tool, an Inspect based
thread interleaving explorer, and a customized inference engine inside Daikon. We have evaluated
the resulting system on public domain multithreaded C/C++ benchmarks. Our experiments show
that the new method is effective in generating high-quality invariants. Furthermore, the state and
transition invariants generated by our new method have been proved useful in applications such as
error diagnosis and inferring atomic regions in the concurrent software code.