Modular Verification of Multithreaded Programs

Cormac Flanagan, Stephen N. Freund, Shaz Qadeer, and Sanjit A. Seshia. Modular Verification of Multithreaded Programs. Theoretical Computer Science, 338(1-3):153–183, 2005.

Download

[HTML] 

Abstract

Multithreaded software systems are prone to errors due to the difficulty of reasoning about multiple interleaved threads operating on shared data. Static checkers that analyze a program's behavior over all execution paths and all thread interleavings are a powerful approach to identifying bugs in such systems. In this paper, we present Calvin, a scalable and expressive static checker for multithreaded programs based on automatic theorem proving. To handle realistic programs, Calvin performs modular checking of each procedure called by a thread using specifications of other procedures and other threads. Our experience applying Calvin to several real-world programs indicates that Calvin has a moderate annotation overhead and can catch common defects in multithreaded programs, such as synchronization errors and violations of data invariants.

BibTeX

@article{FFQS05,
  author    = {Cormac Flanagan and
               Stephen N. Freund and
               Shaz Qadeer and
               Sanjit A. Seshia},
  title     = {Modular Verification of Multithreaded Programs},
  journal   = {Theoretical Computer Science},
  volume    = {338},
  number    = {1-3},
  year      = {2005},
  pages     = {153-183},
  abstract = {Multithreaded software systems are prone to errors due to the difficulty of reasoning about multiple interleaved threads operating on shared data. Static checkers that analyze a program's behavior over all execution paths and all thread interleavings are a powerful approach to identifying bugs in such systems. In this paper, we present Calvin, a scalable and expressive static checker for multithreaded programs based on automatic theorem proving. To handle realistic programs, Calvin performs modular checking of each procedure called by a thread using specifications of other procedures and other threads. Our experience applying Calvin to several real-world programs indicates that Calvin has a moderate annotation overhead and can catch common defects in multithreaded programs, such as synchronization errors and violations of data invariants.},
}