Shaz Qadeer, Microsoft Research
Debugging concurrent programs by context-bounded analysis
Designing concurrent programs is difficult. The nondeterministic interaction between concurrently executing threads of a concurrent program results in programming errors that are notoriously difficult to reproduce and fix. Automated program analysis techniques for finding such errors are invaluable as a debugging and programming aid. In this talk, I will present a novel static analysis technique for concurrent software based on the idea of context-bounded model checking.
An execution of a concurrent program is a sequence of contexts, where each context consists of transitions performed by a single thread. Our work is motivated by the belief that many subtle errors in a concurrent program are manifested by executions with few contexts.
I will first present KISS (Keep It Simple and Sequential), a technique for transforming a concurrent program P into a sequential program Q that encodes all executions of P with a small number of contexts. We used KISS to convert SDV (Static Driver Verifier), a model checker for sequential C programs, into a model checker for concurrent C programs. We have used the combination of KISS and SDV to find a number of subtle concurrency errors in Windows device drivers.
Next, I will present a new theoretical result that illustrates that bounding the number of contexts significantly reduces the complexity of verifying concurrent programs. It is well-known that the problem of verifying assertions in a concurrent boolean program is undecidable. I will show that if analysis is limited to executions with a fixed but arbitrary context-bound, the problem becomes decidable, even in the presence of unbounded dynamic thread creation.