Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems

  • Published:
Annals of Mathematics and Artificial Intelligence Aims and scope Submit manuscript

Abstract

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 asinglediagram 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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

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)

    Article  MathSciNet  Google Scholar 

  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)

  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)

  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)

  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)

  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)

  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)

    Article  Google Scholar 

  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)

  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)

  11. Brookes, S.D.: A Semantics for Concurrent Separation Logic. In: Proceedings of CONCUR’04, LNCS, vol. 3170, pp 16–34. Springer (2004)

  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)

  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)

  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)

  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)

  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)

  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)

    MATH  Google Scholar 

  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)

  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)

  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)

  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)

  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)

  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)

  27. Herlihy, M., Shavit, N.: The art of multiprocessor programming. Morgan-Kaufmann (2008)

  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)

  29. Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19(7), 371–384 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  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)

  31. Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Commun. ACM 17(8), 453–455 (1974)

    Article  MathSciNet  MATH  Google Scholar 

  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)

  33. Manna, Z., Pnueli, A.: Temporal verification of reactive systems: Safety. springer (1995)

  34. Manna, Z., Sipma, H.: Verification of Parameterized Systems by Dynamic Induction on Diagrams. In: Proceedings of CAV’99, LNCS, vol. 1633. Springer (1999)

  35. Marco Bozzano, G.D.: Beyond Parameterized Verification. In: Proceedings of TACAS’02, LNCS, vol. 2280, pp 221–235. Springer (2002)

  36. Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. Theor. Comput. Sci. 32, 321–330 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  37. O’Hearn, P.W.: Resources, Concurrency and Local Reasoning. In: Proceedings of CONCUR’04, LNCS, vol. 3170, pp 49–67. Springer (2004)

  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)

  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)

  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)

  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)

  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)

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

  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)

  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)

  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)

    Article  MathSciNet  MATH  Google Scholar 

  57. Zhang, S.J.: Scalable Automatic Linearizability Checking. In: Proceedings of ICSE’11, vol. 5578, pp 1185–1187. ACM (2011)

Download references

Author information

Authors and Affiliations

  1. IMDEA Software Institute, Madrid, Spain

    Alejandro Sánchez & César Sánchez

Authors
  1. Alejandro Sánchez
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. César Sánchez
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alejandro Sánchez.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Sánchez, A., Sánchez, C. Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems. Ann Math Artif Intell 80, 249–282 (2017). https://doi.org/10.1007/s10472-016-9531-9

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10472-016-9531-9

Keywords

Search

Navigation