Abstract
We present an algorithm called Tar (“Thread-modular Abstraction Refinement”) for model checking safety properties of concurrent software. The Tar algorithm uses thread-modular assume-guarantee reasoning to overcome the exponential complexity in the control state of multithreaded programs. Thread modularity means that Tar explores the state space of one thread at a time, making assumptions about how the environment can interfere. The Tar algorithm uses counterexample-guided predicate-abstraction refinement to overcome the usually infinite complexity in the data state of C programs. A successive approximation scheme automatically infers the necessary precision on data variables as well as suitable environment assumptions. The scheme is novel in that transition relations are approximated from above, while at the same time environment assumptions are approximated from below. In our software verification tool Blast we have implemented a fully automatic race checker for multithreaded C programs which is based on the Tar algorithm. This tool has verified a wide variety of commonly used locking idioms, including locking schemes that are not amenable to existing dynamic and static race checkers such as Eraser or Warlock.
This work was supported in part by the NSF grants CCR-0085949 and CCR-0234690, the DARPA grant F33615-00-C-1693, and the MARCO grant 98-DT-660.
Chapter PDF
References
Abadi, M., Lamport, L.: Conjoining specifications. ACM TOPLAS 17, 507–534 (1995)
Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods in System Design 15, 7–48 (1999)
Alur, R., Itai, A., Kurshan, R.P., Yannakakis, M.: Timing verification by successive approximation. Information and Computation 118, 142–157 (1995)
Ball, T., Rajamani, S.K.: The slam project: debugging system software via static analysis. In: Proc. POPL, pp. 1–3. ACM, New York (2002)
Boyapati, C., Rinard, M.: A parameterized type system for race-free Java programs. In: Proc. OOPSLA, pp. 56–69 (2001)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Laubach, R.S., Zheng, H.: Bandera: extracting finite-state models from Java source code. In: Proc. ICSE, pp. 439–448. IEEE Computer Society Press, Los Alamitos (2000)
Flanagan, C., Freund, S.N.: Detecting race conditions in large programs. In: Proc. PASTE, pp. 90–96. ACM, New York (2001)
Flanagan, C., Freund, S.N., Qadeer, S.: Thread-modular verification for shared-memory programs. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 262–277. Springer, Heidelberg (2002)
Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 213–224. Springer, Heidelberg (2003)
Flanagan, C., Qadeer, S., Seshia, S.A.: A modular checker for multithreaded programs. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 180–194. Springer, Heidelberg (2002)
Graf, S., Saïdi, H.: Construction of abstract state graphs with Pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Havelund, K., Pressburger, T.: Model checking Java programs using Java Pathfinder. Software Tools for Technology Transfer 2, 72–84 (2000)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. POPL, pp. 58–70. ACM, New York (2002)
Holzmann, G.J.: The spin model checker. IEEE TSE 23, 279–295 (1997)
Holzmann, G.J.: Logic verification of ANSI-C code with spin. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 131–147. Springer, Heidelberg (2000)
Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM TOPLAS 5, 596–619 (1983)
Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica 6, 319–340 (1976)
Savage, S., Burrows, M., Nelson, C.G., Sobalvarro, P., Anderson, T.: Eraser: a dynamic data race detector for multithreaded programs. ACM TOCS 15, 391–411 (1997)
Sterling, N.: Warlock: a static data race analysis tool. In: Proc. USENIX Technical Conference, pp. 97–106 (1993)
Yahav, E.: Verifying safety properties of concurrent Java programs using threevalued logic. In: Proc. POPL, pp. 27–40. ACM, New York (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Henzinger, T.A., Jhala, R., Majumdar, R., Qadeer, S. (2003). Thread-Modular Abstraction Refinement. In: Hunt, W.A., Somenzi, F. (eds) Computer Aided Verification. CAV 2003. Lecture Notes in Computer Science, vol 2725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45069-6_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-45069-6_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40524-5
Online ISBN: 978-3-540-45069-6
eBook Packages: Springer Book Archive