Coping with Multi-thread Schedules for Detecting Concurrency Bugs
Event details
| Date | 22.06.2011 |
| Hour | 10:15 |
| Speaker | Dr Aarti Gupta, NEC Laboratories America |
| Location | |
| Category | Conferences - Seminars |
Verification of multi-threaded programs has to grapple with the core
problem of handling an explosive number of thread schedules. In this talk,I will describe three main approaches we have proposed to cope with this problem, spanning a range of static and dynamic analyses.
- The first is a static analysis framework for semantic reduction of
thread interleavings, where we iteratively refine a transaction graph
that captures the interleavings, by deriving sound invariants using
abstract interpretation. For data race detection, this framework serves
to reduce the number of false warnings captured by an initial lockset
analysis, and enables the use of model checking on the remaining warnings to generate concrete error traces.
- The second approach combines dynamic testing with predictive analysis. Given a test execution of the multi-threaded program, we derive a symbolic predictive model to explore all (or some) alternative thread schedules over the same events, and use an SMT solver to find violations.
- The third approach is based on systematic testing, where we propose a
coverage-based metric to choose which interleavings to explore during
stateless model checking. Although unsound in principle, the metric works well in practice to catch many bugs, while significantly improving performance in comparison to other methods such as dynamic partial order reduction and preemptive context bounding.
Dr Gupta's homepage
Practical information
- General public
- Free