Advertisement

Parallelizing a Symbolic Compositional Model-Checking Algorithm

  • Ariel Cohen
  • Kedar S. Namjoshi
  • Yaniv Sa’ar
  • Lenore D. Zuck
  • Katya I. Kisyova
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6504)

Abstract

We describe a parallel, symbolic, model-checking algorithm, built around a compositional reasoning method. The method constructs a collection of per-process (i.e., local) invariants, which together imply a desired global safety property. The local invariant computation is a simultaneous fixpoint evaluation, which easily lends itself to parallelization. Moreover, locality of reasoning helps limit both the frequency and the amount of cross-thread synchronization, leading to good parallel performance. Experimental results show that the parallelized computation can achieve substantial speed-up, with reasonably small memory overhead.

Keywords

Model Check Shared Variable Mutual Exclusion Reachable State Cache Line 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221–234. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  2. 2.
    Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transistion relations. In: VLSI (1991)Google Scholar
  3. 3.
    Cabodi, G., Camurati, P., Lioy, A., Poncino, M., Quer, S.: A parallel approach to symbolic traversal based on set partitioning. In: CHARME, pp. 167–184 (1997)Google Scholar
  4. 4.
    Cabodi, G., Camurati, P., Quer, S.: Improved reachability analysis of large finite state machines. In: ICCAD, pp. 354–360 (1996)Google Scholar
  5. 5.
    Cho, H., Hachtel, G.D., Macii, E., Plessier, B., Somenzi, F.: Algorithms for approximate fsm traversal based on state space decomposition. IEEE Trans. on CAD of Integrated Circuits and Systems 15(12), 1465–1478 (1996)CrossRefGoogle Scholar
  6. 6.
    Cohen, A., Namjoshi, K.S.: Local proofs for global safety properties. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 55–67. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. 7.
    Cohen, A., Namjoshi, K.S.: Local proofs for linear-time properties of concurrent programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 149–161. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  8. 8.
    Cohen, A., Namjoshi, K.S., Sa’ar, Y.: A dash of fairness for compositional reasoning. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 543–557. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  9. 9.
    Cohen, A., Namjoshi, K.S., Sa’ar, Y.: Split: A compositional LTL verifier. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 558–561. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  10. 10.
    Cohen, A., Namjoshi, K.S., Sa’ar, Y., Zuck, L.D., Kisyova, K.I.: Model checking in bits and pieces. In: EC2 Workshop, CAV (2010), http://split.ysaar.net/data/EC2.pdf
  11. 11.
    Cousot, P.: Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice. Res. rep. R.R. 88, Laboratoire IMAG, Université scientifique et médicale de Grenoble, Grenoble, France (September 1977)Google Scholar
  12. 12.
    Cousot, P., Cousot, R.: Automatic synthesis of optimal invariant assertions: mathematical foundations. In: ACM Symposium on Artificial Intelligence & Programming Languages, vol. 12(8), pp. 1–12. ACM SIGPLAN Not, Rochester, NY (August 1977)Google Scholar
  13. 13.
    Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)CrossRefzbMATHGoogle Scholar
  14. 14.
    Ezekiel, J., Lüttgen, G., Ciardo, G.: Parallelising symbolic state-space generators. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 268–280. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  15. 15.
    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)CrossRefGoogle Scholar
  16. 16.
    German, S., Janssen, G.: A tutorial example of a cache memory protocol and RTL implementation. Technical Report RC23958 (W0605-092), IBM, 5 (2006)Google Scholar
  17. 17.
    Govindaraju, S.G., Dill, D.L., Hu, A.J., Horowitz, M.: Approximate reachability with bdds using overlapping projections. In: DAC, pp. 451–456 (1998)Google Scholar
  18. 18.
    Grumberg, O., Heyman, T., Ifergan, N., Schuster, A.: Achieving speedups in distributed symbolic reachability analysis through asynchronous computation. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 129–145. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  19. 19.
    Grumberg, O., Heyman, T., Schuster, A.: A work-efficient distributed algorithm for reachability analysis. Formal Methods in System Design 29(2), 157–175 (2006)CrossRefzbMATHGoogle Scholar
  20. 20.
    Holzmann, G.J., Bosnacki, D.: The design of a multicore extension of the SPIN model checker. IEEE Trans. Software Eng. 33(10), 659–674 (2007)CrossRefGoogle Scholar
  21. 21.
    Holzmann, G.J., Bosnacki, D.: Multi-core model checking with SPIN. In: IPDPS, pp. 1–8. IEEE, Los Alamitos (2007)Google Scholar
  22. 22.
    Hu, A.J., Dill, D.L.: Efficient verification with bdds using implicitly conjoined invariants. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 3–14. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  23. 23.
    Iyer, S.K., Sahoo, D., Emerson, E.A., Jain, J.: On partitioning and symbolic model checking. IEEE Trans. on CAD of Integrated Circuits and Systems 25(5), 780–788 (2006)CrossRefzbMATHGoogle Scholar
  24. 24.
    Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng. 3(2) (1977)Google Scholar
  25. 25.
    Lüttgen, G.: Parallelising Symbolic State-Space Generators: Frustration & Hope. Seminar on Distributed Verification and Grid Computing. Schloss Dagstuhl, Germany (August 2008), http://www-users.cs.york.ac.uk/~luettgen/presentations
  26. 26.
    Moon, I.-H., Kukula, J.H., Shiple, T.R., Somenzi, F.: Least fixpoint approximations for reachability analysis. In: ICCAD, pp. 41–44 (1999)Google Scholar
  27. 27.
    Namjoshi, K.S.: Symmetry and completeness in the analysis of parameterized systems. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 299–313. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  28. 28.
    Narayan, A., Isles, A.J., Jain, J., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: Reachability analysis using partitioned-robdds. In: ICCAD, pp. 388–393 (1997)Google Scholar
  29. 29.
    Owicki, S.S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. ACM Commun. 19(5), 279–285 (1976)MathSciNetCrossRefzbMATHGoogle Scholar
  30. 30.
    Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981)CrossRefzbMATHGoogle Scholar
  31. 31.
    Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82–97. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  32. 32.
    Pnueli, A., Sa’ar, Y., Zuck, L.D.: jtlv: A framework for developing verification algorithms. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 171–174. Springer, Heidelberg (2010), http://jtlv.sourceforge.net/ CrossRefGoogle Scholar
  33. 33.
    Ravi, K., Somenzi, F.: High-density reachability analysis. In: ICCAD, pp. 154–158 (1995)Google Scholar
  34. 34.
    Sahoo, D., Jain, J., Iyer, S.K., Dill, D.L.: A new reachability algorithm for symmetric multi-processor architecture. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 26–38. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  35. 35.
    Sahoo, D., Jain, J., Iyer, S.K., Dill, D.L., Emerson, E.A.: Multi-threaded reachability. In: DAC, pp. 467–470. ACM, New York (2005)Google Scholar
  36. 36.
    Stern, U., Dill, D.L.: Parallelizing the Murϕ verifier. Formal Methods in System Design 18(2), 117–129 (2001)CrossRefzbMATHGoogle Scholar
  37. 37.
    Szymanski, B.K.: A simple solution to Lamport’s concurrent programming problem with linear wait. In: Proc. 1988 International Conference on Supercomputing Systems, pp. 621–626. St. Malo, France (1988)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Ariel Cohen
    • 1
  • Kedar S. Namjoshi
    • 1
  • Yaniv Sa’ar
    • 2
  • Lenore D. Zuck
    • 3
  • Katya I. Kisyova
    • 3
  1. 1.Bell LabsAlcatel-LucentMurray HillUSA
  2. 2.Weizmann Institute of ScienceRehovotIsrael
  3. 3.University of Illinois at ChicagoChicagoUSA

Personalised recommendations