Advertisement

Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation

  • Orna Grumberg
  • Tamir Heyman
  • Nili Ifergan
  • Assaf Schuster
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)

Abstract

This paper presents a novel BDD-based distributed algorithm for reachability analysis which is completely asynchronous. Previous BDD-based distributed schemes are synchronous: they consist of interleaved rounds of computation and communication, in which the fastest machine (or one which is lightly loaded) must wait for the slowest one at the end of each round.

We make two major contributions. First, the algorithm performs image computation and message transfer concurrently, employing non-blocking protocols in several layers of the communication and the computation infrastructures. As a result, regardless of the scale and type of the underlying platform, the maximal amount of resources can be utilized efficiently. Second, the algorithm incorporates an adaptive mechanism which splits the workload, taking into account the availability of free computational power. In this way, the computation can progress more quickly because, when more CPUs are available to join the computation, less work is assigned to each of them. Less load implies additional important benefits, such as better locality of reference, less overhead in compaction activities (such as reorder), and faster and better workload splitting.

We implemented the new approach by extending a symbolic model checker from Intel. The effectiveness of the resulting scheme is demonstrated on a number of large industrial designs as well as public benchmark circuits, all known to be hard for reachability analysis. Our results show that the asynchronous algorithm enables efficient utilization of higher levels of parallelism. High speedups are reported, up to an order of magnitude, for computing reachability for models with higher memory requirements than was previously possible.

Keywords

Model Check Reachable State Reachability Analysis Symbolic Model Check Free Worker 
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.

References

  1. 1.
    Barnat, J., Brim, L., Stribrna, J.: Distributed LTL model-checking in SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 200–216. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  2. 2.
    Beer, I., Ben-David, S., Landver, A.: On-The-Fly Model Checking of RCTL Formulas. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 184–194. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  3. 3.
    Biere, A., Artho, C., Schuppan, V.: Liveness Checking as Safety Checking. In: Proceedings of the 7th International ERCIM Workshop, FMICS 2002. Electronic Notes in Theoretical Computer Science, vol. 66(2). Elsevier, Amsterdam (2002)Google Scholar
  4. 4.
    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zue, Y.: Bounded Model Checking. Advances in Computers, vol. 58. Academic Press, London (2003)Google Scholar
  5. 5.
    Braberman, V.A., Olivero, A., Schapachnik, F.: Issues in distributed timed model checking: Building Zeus. STTT 7(1), 4–18 (2005)CrossRefGoogle Scholar
  6. 6.
    Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic Model Checking with Partitioned Transition Relations. In: Proceedings of Internation Conference on Very Large Integration, pp. 45–58 (1991)Google Scholar
  7. 7.
    Cabodi, G., Camurati, P., Quer, S.: Improved Reachability Analysis of Large FSM. In: Proceedings of the IEEE International Conference on CAD, pp. 354–360 (1996)Google Scholar
  8. 8.
    Chauhan, P., Clarke, E.M., Kroening, D.: Using SAT based Image Computation for Reachability Analysis. Technical report, Carnegie Mellon University, School of Computer Science (2003)Google Scholar
  9. 9.
    Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  10. 10.
    Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (1999)Google Scholar
  11. 11.
    Dijkstra, E.W., Feijen, W.H.J., van Gasteren, A.J.M.: Derivation of a Termination Detection Algorithm for Distributed Computations. Information Processing Letters, 217–219 (1983)Google Scholar
  12. 12.
    Dijkstra, E.W., Scholten, C.S.: Termination Detection for Diffusing Computations. Information Processing Letters, 1–4 (1980)Google Scholar
  13. 13.
    Fraer, R., Kamhi, G., Barukh, Z., Vardi, M.Y., Fix, L.: Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  14. 14.
    Grumberg, O., Heyman, A., Heyman, T., Schuster, A.: Division System: A General Platform for Distributed Symbolic Model Checking Research (2003)Google Scholar
  15. 15.
    Grumberg, O., Heyman, T., Schuster, A.: A Work-Efficient Distributed Algorithm for Reachability Analysis. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 54–66. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  16. 16.
    Grumberg, O., Schuster, A., Yadgar, A.: Memory Efficient All-Solutions SAT Solver and its Application for Reachability Analysis. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 275–289. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    Gupta, A., Gupta, A., Yang, Z., Ashar, P.: Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation. In: DAC, pp. 536–541. ACM Press, New York (2001)Google Scholar
  18. 18.
    Gupta, A., Yang, Z., Ashar, P., Zhang, L., Malik, S.: Partition-Based Decision Heuristics for Image Computation using SAT and BDDs. In: ICCAD, pp. 286–292. IEEE Press, Los Alamitos (2001)Google Scholar
  19. 19.
    Gupta, A., Yang, Z., Ashar, P., Gupta, A.: SAT-Based Image Computation with Application in Reachability Analysis. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 354–371. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  20. 20.
    Heyman, T., Geist, D., Grumberg, O., Schuster, A.: A Scalable Parallel Algorithm for Reachability Analysis of Very Large Circuits. Formal Methods in System Design, 317–338 (2002)Google Scholar
  21. 21.
    Kang, H., Park, I.: SAT-based Unbounded Symbolic Model Checking. In: DAC (2003)Google Scholar
  22. 22.
    Lerda, F., Sisto, R.: Distributed-Memory Model Checking with SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 22–39. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  23. 23.
    McMillan, K.L.: Applying SAT Methods in Unbounded Symbolic Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  24. 24.
    Milvang-Jensen, K., Hu, A.J.: BDDNOW: A Parallel BDD Package. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 501–507. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  25. 25.
    Narayan, A., Isles, A., Jain, J., Brayton, R., Sangiovanni-Vincentelli, A.L.: Reachability Analysis Using Partitioned-ROBDDs. In: Proceedings of the IEEE International Conference on Computer Aided Design, pp. 388–393 (1997)Google Scholar
  26. 26.
    Narayan, A.A., Jawahar, J., Fujita, M., Sangiovanni-Vincenteli, A.: Partitioned-ROBDDs. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 547–554. Springer, Heidelberg (1996)Google Scholar
  27. 27.
    Nicol, D.M., Ciardo, G.: Automated Parallelization of Discrete State-Space Generation. J. Parallel Distrib. Comput. 47(2), 153–167 (1997)CrossRefGoogle Scholar
  28. 28.
    Prasad, M.R., Biere, A., Gupta, A.: A Survey of Recent Advances in SAT-Based Verification. To appear in STTT 2005 (2005)Google Scholar
  29. 29.
    Stern, U., Dill, D.L.: Parallelizing the Murϕ Verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 256–278. Springer, Heidelberg (1997)Google Scholar
  30. 30.
    Stornetta, T., Brewer, F.: Implementation of an Efficient Parallel BDD Package. In: 33rd Design Automation Conference (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Orna Grumberg
    • 1
  • Tamir Heyman
    • 1
  • Nili Ifergan
    • 1
  • Assaf Schuster
    • 1
  1. 1.Computer Science DepartmentTechnionHaifaIsrael

Personalised recommendations