×

Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems. (English) Zbl 1419.68064

Summary: This paper studies the problem of verifying temporal properties (including liveness properties) of parametrized concurrent systems executed by an unbounded number of threads. To solve this problem we introduce parametrized verification diagrams (PVDs), that extend the so-called generalized verification diagrams (GVDs) adding support for parametrized verification. Even though GVDs are known to be a sound and complete proof system for non-parametrized systems, the application of GVDs to parametrized systems requires using quantification or finding a potentially different diagram for each instantiation of the parameter (number of threads). As a consequence, the use of GVDs in parametrized verification requires discharging and proving either quantified formulas or an unbounded collection of verification conditions. Parametrized verification diagrams enable the use of a single diagram to represent the proof that all possible instances of the parametrized concurrent system satisfy the given temporal specification. Checking the proof represented by a PVD requires proving only a finite collection of quantifier-free verification conditions. The PVDs we present here assume that the parametrized systems are symmetric, which covers a large class of concurrent and distributed systems, including concurrent data types. Our second contribution is an implementation of PVDs and its integration into Leap, our prototype theorem prover. Finally, we illustrate empirically, using Leap, the practical applicability of PVDs by building and checking proofs of liveness properties of mutual exclusion protocols and concurrent data structures. To the best of our knowledge, these are the first machine-checkable proofs of liveness properties of these concurrent data types.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

AProVE
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Proc. Letters 22(6), 307-309 (1986) · doi:10.1016/0020-0190(86)90071-2
[2] Banerjee, A., Naumann, D.A., Rosenberg, S.: Regional Logic for Local Reasoning about Global Invariants. In: Proceedings of ECOOP’08, pp 387-411. Springer (2008)
[3] Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Handbook of Satisfiability, chap. Satisfiability Modulo Theories. IOS Press (2008) · Zbl 1329.68171
[4] Baukus, K., Bensalem, S., Lakhnech, Y., Stahl, K.: Abstracting WS1S Systems to Verify Parameterized Networks. In: Proceedings of TACAS’00, LNCS, vol. 1785, pp 188-203. Springer (2000) · Zbl 0964.68096
[5] Baukus, K., Lakhnech, Y., Stahl, K.: Verifying Universal Properties of Parameterized Networks. In: Proceedings of FTRTFT’00, LNCS, vol. 1926, pp 291-303. Springer (2000) · Zbl 0986.68062
[6] Baukus, K., Lakhnech, Y., Stahl, K.: Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness. In: Proceedings of VMCAI’02, LNCS, vol. 2294, pp 317-330. Springer (2002) · Zbl 1057.68620
[7] Berdine, J., Lev-ami, T., Manevich, R., RaMalingam, G., Sagiv, S.: Thread Quantification for Concurrent Shape Analysis. In: Proceedings of CAV’08, LNCS, vol. 5123, pp 399-413. Springer (2008) · Zbl 1155.68360
[8] Bjørner, N., Browne, A., Colón, M., Finkbeiner, B., Manna, Z., Sipma, H., Uribe, T.E.: Verifying temporal properties of reactive systems: A STeP tutorial. Form. Meth. in Sys. Design 16(3), 227-270 (2000) · doi:10.1023/A:1008700623084
[9] Bouajjani, A., Dragoi, C., Enea, C., Sighireanu, M.: A Logic-Based Framework for Reasoning about Composite Data Structures. In: Proceedings of CONCUR’09, pp 178-195. Springer (2009) · Zbl 1254.68146
[10] Bradley, A.R., Manna, Z., Sipma, H.B.: What’S Decidable about Arrays?. In: Proceedings of VMCAI’06, LNCS, vol. 3855, pp 427-442. Springer (2006) · Zbl 1176.68116
[11] Brookes, S.D.: A Semantics for Concurrent Separation Logic. In: Proceedings of CONCUR’04, LNCS, vol. 3170, pp 16-34. Springer (2004) · Zbl 1099.68650
[12] Browne, A., Manna, Z., Sipma, H.B.: Generalized Temporal Verification Diagrams. In: Proceedings of FSTTCS’95, LNCS, vol. 1206, pp 484-498. Springer (1995) · Zbl 1354.68171
[13] Bultan, T., Gerber, R., Pugh, W.: Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic. In: Proceedings of CAV’97, LNCS, vol. 1254, pp 400-411. Springer (1997) · Zbl 0664.68048
[14] Cerný, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., Alur, R.: Model Checking of Linearizability of Concurrent List Implementations. In: Proceedings of CAV’10, LNCS, vol. 6174, pp 465-479. Springer (2010)
[15] Clarke, E.M., Grumberg, O.: Avoiding the State Explosion Problem in Temporal Logic Model Checking. In: Proceedings of PODC’87, pp 294-303. ACM (1987)
[16] Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about Networks with Many Identical Finite-State Processes. In: Proceedings of PODC’86, pp 240-248. ACM (1986) · Zbl 0709.68610
[17] Clarke, E.M., Talupur, M., Veith, H.: Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems. In: Proceedings of TACAS’08, LNCS, vol. 4963, pp 33-47. Springer (2008) · Zbl 1134.68403
[18] Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that Programs Eventually Do Something Good. In: Proceedings of POPL’07, pp 265-276. ACM (2007) · Zbl 1295.68083
[19] Dershowitz, N., Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering. Communication and Computing 12(1/2), 117-156 (2001) · Zbl 0977.68052
[20] Emerson, E.A., Kahlon, V.: Reducing Model Checking of the Many to the Few. In: Proceedings of CADE’00, LNAI, vol. 1831, pp 236-254. Springer (2000) · Zbl 0963.68109
[21] Emerson, E.A., Kahlon, V.: Model Checking Large-Scale and Parameterized Resource Allocation Systems. In: TACAS, LNCS, vol. 2280, pp 251-265. Springer (2002) · Zbl 1043.68569
[22] Farzan, A., Kincaid, Z.: Verification of Parameterized Concurrent Programs by Modular Reasoning about Data and Control. In: Proceedings of POPL’12, pp 297-308. ACM (2012) · Zbl 1321.68192
[23] Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Plücker, M., Schneider-kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Proving Termination of Programs Automatically with AProVE. In: Proceedings of IJCAR’14, LNCS, vol. 8562, pp 184-191. Springer (2014) · Zbl 1409.68256
[24] Goel, A., Krstic, S., Leslie, R., Tuttle, M.R.: SMT-Based System Verification with DVF. In: Proceedings of SMT’12, Easychair, EPiC Series, vol. 20, pp 32-43 (2012)
[25] Gotsman, A., Cook, B., Parkinson, M.J., Vafeiadis, V.: Proving that Non-Blocking Algorithms Don’t Block. In: Shao, Z., Pierce, B.C. (eds.) Proceedings of POPL’09, pp 16-28. ACM (2009) · Zbl 1315.68093
[26] Groves, L.: Verifying Michael and Scott’s Lock-Free Queue Algorithm Using Trace Reduction. In: CATS, CRPIT, vol. 77, pp 133-142. Australian Computer Society (2008) · Zbl 1121.03040
[27] Herlihy, M., Shavit, N.: The art of multiprocessor programming. Morgan-Kaufmann (2008) · Zbl 1329.68171
[28] Hobor, A., Appel, A.W., Nardelli, F.Z.: Oracle Semantics for Concurrent Separation Logic. In: Proceedings of ESOP’08, LNCS, vol. 4960, pp 353-367. Springer (2008) · Zbl 1133.68371
[29] Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19(7), 371-384 (1976) · Zbl 0329.68016 · doi:10.1145/360248.360251
[30] Lahiri, S.K., Qadeer, S.: Back to the Future: Revisiting Precise Program Verification Using Smt Solvers. In: Proceedings of POPL’08, pp 171-182. ACM (2008) · Zbl 1295.68087
[31] Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Commun. ACM 17(8), 453-455 (1974) · Zbl 0281.68004 · doi:10.1145/361082.361093
[32] Manna, Z., Browne, A., Sipma, H., Uribe, T.E.: Visual Abstractions for Temporal Verification. In: Proceedings of AMAST’98, LNCS, vol. 1548, pp 28-41. Springer (1998) · Zbl 0281.68004
[33] Manna, Z., Pnueli, A.: Temporal verification of reactive systems: Safety. springer (1995) · Zbl 1288.68169
[34] Manna, Z., Sipma, H.: Verification of Parameterized Systems by Dynamic Induction on Diagrams. In: Proceedings of CAV’99, LNCS, vol. 1633. Springer (1999) · Zbl 1046.68601
[35] Marco Bozzano, G.D.: Beyond Parameterized Verification. In: Proceedings of TACAS’02, LNCS, vol. 2280, pp 221-235. Springer (2002) · Zbl 1043.68565
[36] Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. Theor. Comput. Sci. 32, 321-330 (1984) · Zbl 0544.68042 · doi:10.1016/0304-3975(84)90049-5
[37] O’Hearn, P.W.: Resources, Concurrency and Local Reasoning. In: Proceedings of CONCUR’04, LNCS, vol. 3170, pp 49-67. Springer (2004) · Zbl 1099.68588
[38] O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local Reasoning about Programs that Alter Data Structures. In: Proceedings of CSL’01, LNCS, vol. 2142, pp 1-19. Springer (2001) · Zbl 0999.68045
[39] Pnueli, A.: The Temporal Logic of Programs. In: Proceedings of FOCS’77, pp 46-57. IEEE Computer Society Press (1977)
[40] Pnueli, A., Shahar, E.: Liveness and Acceleration in Parameterized Verification. In: Proceedings of CAV’00, vol. 1855, pp 328-343. Springer (2000) · Zbl 0974.68521
[41] Podelsky, A., Rybalchenko, A.: Transition Invariants. In: Proceedings of LICS’04, pp 32-41. IEEE Computer Society Press (2004)
[42] Reynolds, J.C.: Separation Logic: a Logic for Shared Mutable Data Structures. In: Proceedings of LICS’02, pp 55-74. IEEE Computer Society Press (2002)
[43] Sánchez, A., Sánchez, C.: Decision Procedures for the Temporal Verification of Concurrent Lists. In: Proceedings of ICFEM’10, LNCS, vol. 6447, pp 74-89. Springer (2010) · Zbl 0664.68048
[44] Sánchez, A., Sánchez, C.: A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes. In: Proceedings of NFM’11, LNCS, vol. 6617, pp 343-358. Springer (2011) · Zbl 0544.68042
[45] Sánchez, A., Sánchez, C.: Formal Verification of Skiplists with Arbitrary Many Levels. In: Proceedings of ATVA’14, vol. 8837, pp 314-329. Springer (2014) · Zbl 1448.68317
[46] Sánchez, A., Sánchez, C.: LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes. In: Proceedings of CAV’14, vol. 8559, pp 620-627. Springer (2014)
[47] Sánchez, A., Sánchez, C.: Parametrized Verification Diagrams. In: Proceedings of TIME’14, pp 132-141. IEEE Computer Society (2014)
[48] Sánchez, A., Sánchez, C.: Parametrized invariance for infinite state processes. Acta Inf. 52(6), 525-557 (2015) · Zbl 1329.68171 · doi:10.1007/s00236-015-0222-5
[49] Sethi, D., Talupur, M., Schwartz-Narbonne, D., Malik, S.: Parameterized Model Checking of Fine Grained Concurrency. In: Proceedings of SPIN’12, pp 208-226. Springer (2012) · Zbl 1329.68171
[50] Sipma, H.B.: Diagram-Based Verification of Discrete, Real-Time and Hybrid Systems. Ph.D. thesis, Stanford University (1999)
[51] Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Proc. Letters 28, 213-214 (1988) · Zbl 0664.68048 · doi:10.1016/0020-0190(88)90211-6
[52] Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving Correctness of Highly-Concurrent Linearisable Objects. In: Proceedings of PPOPP’06, pp 129-136. ACM (2006)
[53] Vechev, M.T., Yahav, E., Yorsh, G.: Experience with Model Checking Linearizability. In: Proceedings of SPIN’09, LNCS, vol. 5578, pp 261-278. Springer (2009) · Zbl 0329.68016
[54] Wies, T., Piskac, R., Kuncak, V.: Combining Theories with Shared Set Operations. In: Proceedings of FROCOS’09, LNCS, vol. 5749, pp 366-382. Springer (2009) · Zbl 1193.03030
[55] Yorsh, G., Rabinovich, A.M., Sagiv, M., Meyer, A., Bouajjani, A.: A Logic of Reachable Patterns in Linked Data-Structures. In: Proceedings of FOSSACS’06, pp 94-110 (2006) · Zbl 1180.68131
[56] Yorsh, G., Rabinovich, A.M., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data-structures. J. Log. Algebr. Program. 73(1-2), 111-142 (2007) · Zbl 1121.03040 · doi:10.1016/j.jlap.2006.12.001
[57] Zhang, S.J.: Scalable Automatic Linearizability Checking. In: Proceedings of ICSE’11, vol. 5578, pp 1185-1187. ACM (2011)
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.