Verifying reference counting implementations. (English) Zbl 1234.68254
Kowalewski, Stefan (ed.) et al., Tools and algorithms for the construction and analysis of systems. 15th international conference, TACAS 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22–29, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-00767-5/pbk). Lecture Notes in Computer Science 5505, 352-367 (2009).
Summary: Reference counting is a widely-used resource management idiom which maintains a count of references to each resource by incrementing the count upon an acquisition, and decrementing upon a release; resources whose counts fall to zero may be recycled. We present an algorithm to verify the correctness of reference counting with minimal user interaction. Our algorithm performs compositional verification through the combination of symbolic temporal case splitting and predicate abstraction-based reachability. Temporal case splitting reduces the verification of an unbounded number of processes and resources to verification of a finite number through the use of Skolem variables. The finite state instances are discharged by symbolic model checking, with an auxiliary invariant correlating reference counts with the number of held references. We have implemented our algorithm in Referee, a reference counting analysis tool for C programs, and applied Referee to two real programs: the memory allocator of an OS kernel and the file interface of the Yaffs file system. In both cases our algorithm proves correct the use of reference counts in less than one minute.
For the entire collection see [Zbl 1157.68007].
For the entire collection see [Zbl 1157.68007].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
References:
| [1] | Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL (2002) · doi:10.1145/503272.503274 |
| [2] | Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005) · doi:10.1007/978-3-540-30569-9_3 |
| [3] | Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006) · doi:10.1007/11804192_6 |
| [4] | Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: The blast query language for software verification. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 2–18. Springer, Heidelberg (2004) · Zbl 1104.68408 · doi:10.1007/978-3-540-27864-1_2 |
| [5] | 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. Springer, Heidelberg (2000) · Zbl 0974.68517 · doi:10.1007/10722167_15 |
| [6] | Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: POPL (1977) · Zbl 1149.68389 · doi:10.1145/512950.512973 |
| [7] | Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: FMCAD (2002) · Zbl 1019.68620 · doi:10.1007/3-540-36126-X_2 |
| [8] | Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI (2002) · doi:10.1145/512529.512558 |
| [9] | Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL (2002) · Zbl 1323.68371 · doi:10.1145/503272.503291 |
| [10] | Gopan, D., Reps, T.W., Sagiv, S.: A framework for numeric analysis of array operations. In: POPL (2005) · Zbl 1369.68138 · doi:10.1145/1040305.1040333 |
| [11] | Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997) · doi:10.1007/3-540-63166-6_10 |
| [12] | Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL (2004) · Zbl 1325.68147 · doi:10.1145/964001.964021 |
| [13] | Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002) · Zbl 1323.68374 · doi:10.1145/503272.503279 |
| [14] | Jain, H., Ivančić, F., Gupta, A., Shlyakhter, I., Wang, C.: Using statically computed invariants inside the predicate abstraction and refinement loop. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 137–151. Springer, Heidelberg (2006) · doi:10.1007/11817963_15 |
| [15] | Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 39–51. Springer, Heidelberg (2005) · Zbl 1081.68622 · doi:10.1007/11513988_6 |
| [16] | Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 193–206. Springer, Heidelberg (2007) · Zbl 1135.68474 · doi:10.1007/978-3-540-73368-3_23 |
| [17] | Jos, J.: An operating system kernel, http://pdos.csail.mit.edu/6.828/2005/overview.html |
| [18] | Kuncak, V., Lam, P., Zee, K., Rinard, M.C.: Modular pluggable analyses for data structure consistency. IEEE Trans. Software Eng. 32(12), 988–1005 (2006) · doi:10.1109/TSE.2006.125 |
| [19] | Lahiri, S.K., Bryant, R.E.: Constructing quantified invariants via predicate abstraction. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 267–281. Springer, Heidelberg (2004) · Zbl 1202.68251 · doi:10.1007/978-3-540-24622-0_22 |
| [20] | Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 135–147. Springer, Heidelberg (2004) · Zbl 1103.68627 · doi:10.1007/978-3-540-27813-9_11 |
| [21] | Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995) · Zbl 1288.68169 · doi:10.1007/978-1-4612-4222-2 |
| [22] | McMillan, K.L.: A methodology for hardware verification using compositional model checking. Sci. Comput. Program. 37, 279–309 (2000) · Zbl 0954.68005 · doi:10.1016/S0167-6423(99)00030-1 |
| [23] | One, A.: Yaffs file system, http://www.yaffs.net/ |
| [24] | Qadeer, S., Wu, D.: KISS: Keep it simple, sequential. In: PLDI (2004) |
| [25] | Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS (2002) |
| [26] | Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: POPL (1999) · Zbl 1103.68635 · doi:10.1145/292540.292552 |
| [27] | Shankar, N.: Combining theorem proving and model checking through symbolic analysis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, p. 1. Springer, Heidelberg (2000) · Zbl 0999.68523 · doi:10.1007/3-540-44618-4_1 |
| [28] | van Rossum, G.: Debugging reference count problems, http://www.python.org/doc/essays/refcnt/ |
| [29] | Yahav, E.: Verifying safety properties of concurrent java programs using 3-valued logic. In: POPL (2001) · Zbl 1323.68183 · doi:10.1145/360204.360206 |
| [30] | Yahav, E., Ramalingam, G.: Verifying safety properties using separation and heterogeneous abstractions. In: PLDI (2004) · doi:10.1145/996841.996846 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
