Shuvendu Lahiri, Alexander Malkis, and Shaz Qadeer
Verification of large multithreaded programs is challenging.
Automatic approaches cannot overcome the state explosion in the number
of threads; semi-automatic methods require expensive human time
for finding global inductive invariants. Ideally, automatic methods should
not deal with the composition of the original threads and a human should
not supply a global invariant. We provide such an approach. In our approach,
a human supplies a specification of each thread in the program.
Here he has the freedom to ignore or to use the knowledge about the
other threads. The checks whether specifications of threads are sound
as well as whether the composition of the specifications is error-free are
handed over to the off-the-shelf verifiers. We show how to apply this
divide-and-conquer approach for the interleaving semantics with shared
variables communication where specifications are targeted to real-world
programmers: a specification of a thread is simply another thread. The
new approach extends thread-modular reasoning by relaxing the structure
of the transition relation of a specification. We demonstrate the
feasibility of our approach by verifying two protocols governing the teardown
of important data structures in Windows device drivers.
|Published in||Conference on Verification, Model Checking, and Abstract Interpretation|
All copyrights reserved by Springer 2007.