×

zbMATH — the first resource for mathematics

Context-aware counter abstraction. (English) Zbl 1213.68362
Summary: The trend towards multi-core computing has made concurrent software an important target of computer-aided verification. Unfortunately, Model Checkers for such software suffer tremendously from combinatorial state space explosion. We show how to apply counter abstraction to real-world concurrent programs to factor out redundancy due to thread replication. The traditional global state representation as a vector of local states is replaced by a vector of thread counters, one per local state. In practice, straightforward implementations of this idea are unfavorably sensitive to the number of local states. We present a novel symbolic exploration algorithm that avoids this problem by carefully scheduling which counters to track at any moment during the search. We have carried out experiments on Boolean programs, an abstraction promoted by the success of the Slam project. The experiments give evidence of the applicability of our method to realistic programs, and of the often huge savings obtained in comparison to plain symbolic state space exploration, and to exploration optimized by partial-order methods. To our knowledge, our tool marks the first implementation of counter abstraction to programs with non-trivial local state spaces, resulting in a Model Checker for concurrent Boolean programs that promises true scalability.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ball T, Rajamani SK (2000) Bebop: a symbolic model checker for Boolean programs. In: SPIN, pp 113–130 · Zbl 0976.68540
[2] Ball T, Rajamani SK (2002) The SLAM project: debugging system software via static analysis. In: POPL, pp 1–3
[3] Ball T, Chaki S, Rajamani SK (2001) Parameterized verification of multithreaded software libraries. In: TACAS, pp 158–173 · Zbl 0978.68679
[4] Ball T, Bounimova E, Cook B, Levin V, Lichtenberg J, McGarvey C, Ondrusek B, Rajamani SK, Ustuner A (2006) Thorough static analysis of device drivers. In: EuroSys, pp 73–85
[5] Barner S, Grumberg O (2005) Combining symmetry reduction and under-approximation for symbolic Model Checking. Form Methods Syst Des 27(1–2):29–66 · Zbl 1085.68086 · doi:10.1007/s10703-005-2246-x
[6] Basler G, Mazzucchi M, Wahl T, Kroening D (2009) Symbolic counter abstraction for concurrent software. In: CAV, pp 64–78 · Zbl 1242.68055
[7] Bosnacki D, Dams D, Holenderski L (2002) Symmetric spin. Int J Softw Tools Technol Transf 4(1):92–106 · Zbl 02178179 · doi:10.1007/s100090200074
[8] Clarke EM, Jha S, Enders R, Filkorn T (1996) Exploiting symmetry in temporal logic Model Checking. Form Methods Syst Des 9(1/2):77–104 · Zbl 05475431 · doi:10.1007/BF00625969
[9] Clarke EM, Kroening D, Sharygina N, Yorav K (2005) SATABS: SAT-based predicate abstraction for ANSI-C. In: TACAS, pp 570–574 · Zbl 1087.68586
[10] Cook B, Kroening D, Sharygina N (2005) Symbolic Model Checking for asynchronous Boolean programs. In: SPIN, pp 75–90 · Zbl 1151.68367
[11] Cook B, Kroening D, Sharygina N (2007) Verification of Boolean programs with unbounded thread creation. Theor Comput Sci 388(13):227–242 · Zbl 1143.68043
[12] Delzanno G (2000) Automatic verification of parameterized cache coherence protocols. In: CAV, pp 53–68 · Zbl 0974.68500
[13] Donaldson AF, Miller A (2006) Exact and approximate strategies for symmetry reduction in model checking. In: FM, pp 541–556
[14] Donaldson AF, Miller A (2006) Symmetry reduction for probabilistic Model Checking using generic representatives. In: ATVA, pp 9–23 · Zbl 1161.68564
[15] Donaldson A, Miller A, Parker D (2009) Language-level symmetry reduction for probabilistic Model Checking. In: QEST, pp 289–298
[16] Emerson EA, Sistla AP (1996) Symmetry and Model Checking. Form Methods Syst Des 9(1/2):105–131 · Zbl 05475432 · doi:10.1007/BF00625970
[17] Emerson EA, Trefler RJ (1999) From asymmetry to full symmetry: new techniques for symmetry reduction in Model Checking. In: CHARME, pp 142–156 · Zbl 0957.68067
[18] Emerson EA, Wahl T (2005) Dynamic symmetry reduction. In: TACAS, pp 382–396 · Zbl 1087.68587
[19] Emerson EA, Wahl T (2005) Efficient reduction techniques for systems with many components. Electron Notes Theor Comput Sci 130:379–399 · Zbl 05415260 · doi:10.1016/j.entcs.2005.03.019
[20] Emerson EA, Jha S, Peled D (1997) Combining partial order and symmetry reductions. In: TACAS, pp 19–34
[21] Emerson EA, Havlicek J, Trefler RJ (2000) Virtual symmetry reduction. In: LICS, pp 121–131
[22] Flanagan C, Godefroid P (2005) Dynamic partial-order reduction for Model Checking software. In: POPL, pp 110–121 · Zbl 1369.68135
[23] Graf S, Saïdi H (1997) Construction of abstract state graphs with PVS. In: CAV, pp 72–83
[24] Henzinger TA, Jhala R, Majumdar R (2004) Race checking by context inference. In: PLDI, pp 1–13
[25] Holzmann GJ, Peled D (1994) An improvement in formal verification. In: FORTE, pp 197–211
[26] Kurshan RP (1994) Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press, Princeton
[27] Lahiri SK, Bryant RE, Cook B (2003) A symbolic approach to predicate abstraction. In: CAV, pp 141–153 · Zbl 1278.68181
[28] Lubachevsky BD (1984) An approach to automating the verification of compact parallel coordination programs I. Acta Inform 21:125–169 · Zbl 0534.68017 · doi:10.1007/BF00289237
[29] Manevich R, Lev-Ami T, Sagiv M, Ramalingam G, Berdine J (2008) Heap decomposition for concurrent shape analysis. In: SAS, pp 363–377 · Zbl 1149.68358
[30] Melton R, Dill D Mur\(\phi\) annotated reference manual, rel. 3.1. http://verify.stanford.edu/dill/murphi.html
[31] Pnueli A, Xu J, Zuck LD (2002) Liveness with (0,1,-counter abstraction. In: CAV, pp 107–122 · Zbl 1010.68095
[32] Pong F, Dubois M (1995) A new approach for the verification of cache coherence protocols. IEEE Trans Parallel Distrib Syst 6(8):773–787 · Zbl 05107536 · doi:10.1109/71.406955
[33] Somenzi F The CU decision diagram package, release 2.3.1. University of Colorado at Boulder. http://vlsi.colorado.edu/\(\sim\)fabio/CUDD/
[34] Suwimonteerabuth D, Esparza J, Schwoon S (2008) Symbolic context-bounded analysis of multithreaded java programs. In: SPIN, pp 270–287
[35] Wahl T, Blanc N, Emerson EA (2008) SVISS: symbolic verification of symmetric systems. In: TACAS, pp 459–462
[36] Wei O, Gurfinkel A, Chechik M (2005) Identification and counter abstraction for full virtual symmetry. In: CHARME, pp 285–300 · Zbl 1159.68345
[37] Witkowski T, Blanc N, Kroening D, Weissenbacher G (2007) Model Checking concurrent Linux device drivers. In: ASE, pp 501–504
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.