Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers

Share

Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric. 21st International Conference on Computer Aided Verification (CAV 2009), Grenoble, France.
[pdf] [bib]

Abstract: Context-bounded analysis is an attractive approach to verification of concurrent programs. Bounding the number of contexts executed per thread not only reduces the asymptotic complexity, but also the complexity increases gradually from checking a purely sequential program.
Lal and Reps provided a method for reducing the context-bounded verification of a concurrent boolean program to the verification of a sequential boolean program, thereby allowing sequential reasoning to be employed for verifying concurrent programs. In this work, we adapt the encoding to work for systems programs written in C with the heap and accompanying low-level operations such as pointer arithmetic and casts. Our approach is completely automatic: we use a verification condition generator and SMT solvers, instead of a boolean model checker, in order to avoid manual extraction of boolean programs and false alarms introduced by the abstraction.We demonstrate the use of field slicing for improving the scalability and (in some cases) coverage of our checking.We evaluate our tool STORM on a set of real-world Windows device drivers, and has discovered a bug that could not be detected by extensive application of previous tools.

Bibtex:

@inproceedings{cav2009-lqr,
  author = {Shuvendu K. Lahiri and Shaz Qadeer and
    Zvonimir Rakamari\'c},
  title = {Static and Precise Detection of Concurrency Errors in
    Systems Code Using {SMT} Solvers},
  booktitle = {Proceedings of the 21st International Conference on
    Computer Aided Verification (CAV 2009)},
  series = {Lecture Notes in Computer Science},
  volume = {5643},
  publisher = {Springer},
  editor = {Ahmed Bouajjani and Oded Maler},
  year = {2009},
  pages = {509--524},
}