Skip Navigation



Journal of Logic and Computation Advance Access published online on February 20, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp005
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Chung, M.-Y.
Right arrow Articles by Ciardo, G.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Papers

Speculative Image Computation for Distributed Symbolic Reachability Analysis

Ming-Ying Chung

Verification Group, Synopsys Inc. Mountain View, CA 94085, USA.
E-mail: mychung{at}synopsys.com

Gianfranco Ciardo

Department of Computer Science and Engineering, University of California, Riverside, Riverside, CA 92521, USA.
E-mail: ciardo{at}cs.ucr.edu

Received 29 February 2008.

The Saturation-style fixpoint iteration strategy for symbolic reachability analysis is particularly effective for globally asynchronous locally synchronous discrete-state systems. However, its inherently sequential nature makes it difficult to parallelize Saturation on a network workstations (NOW). We then propose the idea of using idle workstation time to perform speculative image computations. Since an unrestrained prediction may make excessive use of computational resources, we introduce a history-based approach to dynamically recognize image computation (event firing) patterns and explore only firings that conform to these patterns. In addition, we employ an implicit encoding for the patterns, so that the actual image computation history can be efficiently preserved. Experiments not only show that image speculation works on a realistic model, but also indicate that the use of an implicit encoding together with two heuristics results in a better informed speculation.

Keywords: Reachability analysis; decision diagrams; image computation; distributed computing



References

  1. Bell A, Haverkort BR. Sequential and distributed model checking of Petri nets. Software Tools for Technology Transfer (2005) 7:43–60.[CrossRef]
  2. Bryant RE. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers (1986) 35:677–691.[CrossRef][Web of Science]
  3. Buchholz P, Ciardo G, Donatelli S, Kemper P. Complexity of memory-efficient Kronecker operations with applications to the solution of Markov models. INFORMS Journal on Computing (2000) 12:203–222.[Abstract/Free Full Text]
  4. Burch JR, Clarke EM, Long DE. Symbolic model checking with partitioned transition relations. Halaas A, Denyer PB, eds. (1991) Edinburgh, Scotland, North-Holland: IFIP Transactions. 49–58. In International Conference on Very Large Scale Integration.
  5. Chung M-Y, Ciardo G. Saturation NOW. In. In: Proceedings of the Quantitative Evaluation of SysTems (QEST)—Franceschinis G, Katoen J-P, Woodside M, eds. (2004) IEEE Comp. Soc. Press. 272–281.
  6. Chung M-Y, Ciardo G. A pattern recognition approach for speculative firing prediction in distributed saturation state-space generation. In. In: Workshop on Parallel and Distributed Model Checking (PDMC), ENTCS—Martin L, van de Pol J, eds. (2005) Elsevier. 65–79.
  7. Chung M-Y, Ciardo G. A dynamic firing speculation to speedup distributed symbolic state-space generation. Rosenberg AL, ed. (2006) IEEE Comp. Soc. Press. (electronic proceeding). In Proceedings of the International Parallel & Distributed Processing Symposium (IPDPS).
  8. Ciardo G, Jones RL, Miner AS, Siminiceanu R. Logical and stochastic modeling with SMART. Performance Evaluation (2006) 63:578–608.[CrossRef][Web of Science]
  9. Ciardo G, Lan Y. Faster discrete-event simulation through structural caching. In. In: Proceedings of the Sixth International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS-6) (2003) Monticello. 11–14.
  10. Ciardo G, Lüttgen G, Siminiceanu R. Efficient symbolic state-space construction for asynchronous systems. Nielsen M, Simpson D, eds. (2000) Springer. 103–122. In Proceedings of the 21th International Conference on Applications and Theory of Petri Nets, Vol. 1825 of Lecture Notes in Computer Science.
  11. Ciardo G, Lüttgen G, Siminiceanu R. Saturation: an efficient iteration strategy for symbolic state space generation—Margaria T, Yi W, eds. (2001) Springer. 328–342. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Vol. 2031 of Lecture Notes in Computer Science.
  12. Ciardo G, Marmorstein R, Siminiceanu R. Saturation unbound—Garavel H, Hatcliff J, eds. (2003) Springer. 379–393. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Vol. 2619 of Lecture Notes in Computer Science.
  13. Ciardo G, Siminiceanu R. Structural symbolic CTL model checking of asynchronous systems. Hunt W Jr, Somenzi F, eds. (2003) Springer. 40–53. In Computer Aided Verification (CAV’03), Vol. 2725 of Lecture Notes in Computer Science.
  14. Clarke EM, Grumberg O, Peled DA. Model Checking (1999) MIT Press.
  15. Ganai MK, Gupta A, Yang Z, Ashar P. Efficient distributed sat and sat-based distributed bounded model checking. Geist D, Tronci E, eds. (2003) Springer. 207–221. In Proceedings of the Correct Hardware Design and Verification Methods (CHARME), Vol. 2860 of Lecture Notes in Computer Science.
  16. Graf S, Steffen B, Lüttgen G. Compositional minimisation of finite state systems using interface specifications. Journal of Formal Aspects of Computing (1996) 8:607–616.[CrossRef]
  17. Grumberg O, Heyman T, Ifergan N, Schuster A. Achieving speedups in distributed symbolic reachability analysis through asynchronous computation. Borrione D, Paul W, eds. (2005) Springer. 129–145. In Proceedings of the Correct Hardware Design and Verification Methods (CHARME), Vol. 3725 of Lecture Notes in Computer Science.
  18. Grumberg O, Heyman T, Schuster A. A work-efficient distributed algorithm for reachability analysis. In: Computer Aided Verification (CAV)—Hunt WA Jr, Somenzi F, eds. (2003) Springer. 54–66.
  19. Heyman T, Geist D, Grumberg O, Schuster A. Achieving scalability in parallel reachability analysis of very large circuits. Allen Emerson E, Prasad Sistla A, eds. (2000) Springer. 20–35. In Computer-Aided Verification, 12th International Conference (CAV’00), Vol. 1855 of Lecture Notes in Computer Science.
  20. Kam T, Villa T, Brayton RK, Sangiovanni-Vincentelli A. Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic (1998) 4:9–62.[Medline]
  21. Milvang-Jensen K, Hu AJ. BDDNOW: a parallel bdd package. Gopalakrishnan G, Windley PJ, eds. (1998) Springer. 501–507. In Proceedings of the International Confrence on Formal Methods in Computer-Aided Design (FMCAD), Vol. 1522 of Lecture Notes in Computer Science.
  22. Miner AS, Ciardo G. Efficient reachability set generation and storage using decision diagrams—Kleijn HCM, Donatelli S, eds. (1999) Springer. 6–25. In Proceedings of the 20th International Conference on Applications and Theory of Petri Nets, Vol. 1639 of Lecture Notes in Computer Science.
  23. Narayan A, Isles AJ, Jain J, Fujita M, Sangiovanni-Vincentelli AL. Reachability analysis using partitioned-ROBDDs. Yasuura H, ed. (1997) ACM and IEEE Computer Society Press. 388–393. In Proceedings of the International Conference on Computer-Aided Design (ICCAD).
  24. Nicol D, Ciardo G. Automated parallelization of discrete state-space generation. Journal of Parallel and Distributed Computing (1997) 47:153–167.[CrossRef][Web of Science]
  25. Pastor E, Roig O, Cortadella J, Badia RM. Petri net analysis using Boolean manipulation. Valette R, ed. (1994) Springer. 416–435. In Proceedings of the International Conference on Applications and Theory of Petri Nets (ICATPN), Vol. 815 of Lecture Notes in Computer Science.
  26. Siminiceanu R, Ciardo G. Formal verification of the NASA Runway Safety Monitor. Huth M, ed. (2004) Elsevier. 179–194. In Proceedings of the International Workshop on Automated Verification of Critical Systems (AVoCS), Vol. 128(6) of ENTCS.
  27. Stern U, Dill DL. Parallelizing the mur{phi} verifier. Grumberg O, ed. (1997) Springer. 256–278. In Proceedings of the International Conference on Computer Aided Verification (CAV), Vol. 1254 of Lecture Notes in Computer Science.
  28. Stornetta AL. Implementation of an Efficient Parallel BDD Package (1995) Santa Barbara: University of California. Master's Thesis.
  29. Stornetta AL, Brewer F. Implementation of an efficient parallel BDD package. (1996) ACM Press. 641–644. In Proceedings of the Design Automation Conference (DAC).

Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Chung, M.-Y.
Right arrow Articles by Ciardo, G.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?