Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation
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.
KeywordsModel Check Reachable State Reachability Analysis Symbolic Model Check Free Worker
- 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.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
- 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.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.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
- 10.Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (1999)Google Scholar
- 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.Dijkstra, E.W., Scholten, C.S.: Termination Detection for Diffusing Computations. Information Processing Letters, 1–4 (1980)Google Scholar
- 14.Grumberg, O., Heyman, A., Heyman, T., Schuster, A.: Division System: A General Platform for Distributed Symbolic Model Checking Research (2003)Google Scholar
- 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.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
- 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.Kang, H., Park, I.: SAT-based Unbounded Symbolic Model Checking. In: DAC (2003)Google Scholar
- 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.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
- 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.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.Stornetta, T., Brewer, F.: Implementation of an Efficient Parallel BDD Package. In: 33rd Design Automation Conference (1996)Google Scholar