Skip Navigation



Journal of Logic and Computation Advance Access published online on February 12, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp006
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 Ezekiel, J.
Right arrow Articles by Siminiceanu, R.
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

To Parallelize or to Optimize?

Jonathan Ezekiel

Department of Computing, Imperial College, London, UK.
E-mail: jezekiel{at}doc.ic.ac.uk

Gerald Lüttgen

Department of Computer Science, University of York, Heslington, York YO10 5DD, UK.
E-mail: gerald.luettgen{at}cs.york.ac.uk

Radu Siminiceanu

National Institute of Aerospace, Hampton, Virginia, USA.
E-mail: radu{at}nianet.org

Received 29 February 2008.

Model checking is a popular and successful technique for verifying complex digital systems. Carrying this technique—and its underlying state-space generation algorithms—beyond its current limitations presents itself with a number of alternatives. Our focus is on parallelization which is made attractive by the current trend in hardware architectures towards multi-core, multi-processor systems. The main obstacle in this endeavour is that, in particular, symbolic state-space generation algorithms are notoriously hard to parallelize. In this article, we describe the process of taking a sequential symbolic state-space generation algorithm, namely a generic, symbolic BFS algorithm, through a sequence of optimizations that leads up to the Saturation algorithm and follow the impact these sequential algorithms have on their parallel counterparts. In particular, we develop a parallel version of Saturation, discuss the challenges faced in its design and conduct extensive experimental studies of its implementation. We employ rigorous analysis tools and techniques for measuring and evaluating parallel overheads and the quality of the parallelization. The outcome of these studies is that the performance of a parallel symbolic state-space generation algorithm is almost impossible to predict and highly dependent on the model to which it is applied. In most situations, perceivable speed-ups are hard to achieve, but real-world applications where our technique produces significant improvements do exist. Nevertheless, it appears that time is better invested in optimizing sequential symbolic model checking algorithms rather than parallelizing them.

Keywords: Symbolic state-space generation; Saturation; parallelisation; benchmarking



References

  1. Agrawal K, He Y, Leiserson CE. Adaptive work stealing with parallelism feedback. In: Principles and Practice of Parallel Programming (2007) ACM. 112–120.
  2. Barnat J, Rockai P. Shared hash tables in parallel model checking. In: Proceedings of the Parallel and Distributed Methods in verifiCation’07, Electronic Notes in Theoritical Computer Science (2008) 198. Elsevier. 79–91.
  3. Behrmann G, Hune T, Vaandrager FW. Distributing timed model checking: how the search order matters. In: Proceedings of the Computer AidedVerification’00 (2000) Springer. 216–231. Vol. 1855 of Lecture Notes in Computer Science.
  4. Blumofe RD, Joerg CF, Kuszmaul BC, Leiserson CE, Randall KH, Zhou Y. Cilk: an efficient multithreaded runtime system. Parallel and Distributed Computing (1996) 37:55–69.[CrossRef]
  5. Blumofe RD, Papadopoulos D. The performance of work stealing in multiprogrammed environments. In: Measurement and Modeling of Computer Systems—Leutenegger S, ed. (1998) ACM. 266–267.
  6. Bollig B, Leucker M, Weber M. Local parallel model checking for the alternation-free µ-calculus. In: Proceedings of the International SPINWorkshop’02 (2002) Springer. 128–147. Vol. 2318 of Lecture Notes in Computer Science.
  7. Bryant RE. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers (1986) 35:677–691.[CrossRef][Web of Science]
  8. Butenhof DR. Programming with POSIX threads (1997) Addison-Wesley.
  9. Chung M-Y, Ciardo G. A dynamic firing speculation to speedup distributed symbolic state-space generation. In: Proceedings of the International Parallel & Distributed Processing Symposium’03 (2003) IEEE. 10.
  10. Chung M-Y, Ciardo G. Saturation NOW. In: Proceedings of the Quantitative Evaluation of Systems’04 (2004) IEEE. 272–281.
  11. Chung M-Y, Ciardo G, Yu AJ. A fine-grained fullness-guided chaining heuristic for symbolic reachability analysis. In: Proceedings of the Automated Technology for Verification and Analysis’06 (2006) Springer. 51–66. Vol. 4218 of Lecture Notes in Computer Science.
  12. Ciardo G, Jones RL, Miner AS, Siminiceanu R. Logical and stochastic modeling with SMART. Performance Evaluation (2006) 63:578–608.[CrossRef][Web of Science]
  13. Ciardo G, Lan Y. Faster discrete-event simulation through structural caching. In: Performability Modeling of Computer and Communication Systems—Bobbio A, Deavours D, Ma Y, eds. (2003) IEEE. 11–14.
  14. Ciardo G, Lüttgen G, Miner AS. Exploiting interleaving semantics in symbolic state-space generation. Formal Methods in System Design (2007) 31:63–100.[CrossRef][Web of Science]
  15. Ciardo G, Lüttgen G, Siminiceanu R. Efficient symbolic state–space construction for asynchronous systems. (2000) Springer. 103–122. In Proceedings of the Application and Theory of Petri Nets, 21st International Conference’00. Vol. 1839 of Lecture Notes in Computer Science.
  16. Ciardo G, Lüttgen G, Siminiceanu R. Saturation: an efficient iteration strategy for symbolic state-space generation. In: Proceedinigs of the Tools and Algorithms for the Construction and Analysis of Systems’01 (2001) Springer. 328–348. Vol. 2031 of Lecture Notes in Computer Science.
  17. Ciardo G, Marmorstein RM, Siminiceanu R. Saturation unbound. In: Proceedinigs of the Tools and Algorithms for the Construction and Analysis of Systems’03 (2003) Springer. 379–393. Vol. 2619 of Lecture Notes in Computer Science.
  18. Cimatti A, Clarke EM, Giunchiglia F, Roveri M. NuSMV: a new symbolic model checker. Software Tools for Technology Transfer (2000) 2:410–425.[CrossRef]
  19. Clarke EM, Emerson EA, Sistla AP. Automatic verification of finite-state concurrent sys tems using temporal logic specifications. Transactions on Programming Languages and Systems (1986) 8:244–263.[CrossRef]
  20. Clarke EM, Grumberg O, Peled DA. Model Checking (1999) MIT Press.
  21. Ezekiel J. Parallelising Symbolic State-Space Generation Algorithms on Shared-Memory Architectures (2007) UK: University of York. PhD Thesis.
  22. Ezekiel J, Lüttgen G, Ciardo G. Parallelising symbolic state-space generators. In: Proceedings of the Computer Aided Verification’07 (2007) Springer. 268–280. Vol. 4590 of Lecture Notes in Computer Science.
  23. Ezekiel J, Lüttgen G, Siminiceanu R. Can Saturation be parallelised? On the parallelisation of a symbolic state-space generator. In: Proceedings of the Parallel and Distributed Methods in Verification’06 (2007) Springer. 331–346. Vol. 4346 of Lecture Notes in Computer Science.
  24. Fernandes P, Plateau B, Stewart WJ. Efficient descriptor vector multiplications in stochastic automata networks. Assoication for Computing Machinery (1998) 45:381–414.
  25. Garavel H, Mateescu R, Smarandache I. Parallel state space construction for modelchecking. In. In: Proceedings of the SPIN’01 (2001) Springer. 217–234. Vol. 2057 of Lecture Notes in Computer Science.
  26. Gautier T, Roch J-L, Villard G. Regular versus irregular problems and algorithms. In: Proceedings of the IRREGULAR’95 (1995) Springer. 1–25. Vol. 980 of Lecture Notes in Computer Science.
  27. Graf S, Steffen B, Lüttgen G. Compositional minimisation of finite state systems using interface specifications. Formal Aspects of Computing (1996) 8:607–616.[CrossRef]
  28. Graham SL, Kessler PB, McKusick MK. gprof: a call graph execution profiler. ACM SIGPLAN Notices (2004) 39:49–57.
  29. Grumberg O, Heyman T, Ifergan N, Schuster A. Achieving speedups in distributed symbolic reachability analysis through asynchronous computation. In: Proceedings of the Correct Hardware Design and Verification Methods’05 (2005) Springer. 129–145. Vol. 3725 of Lecture Notes in Computer Science.
  30. Grumberg O, Heyman T, Schuster A. A work-efficient distributed algorithm for reachability analysis. Formal Methods in System Design (2006) 29:157–175.[CrossRef][Web of Science]
  31. Gupta A, Tucker A, Urushibara S. The impact of operating system scheduling policies and synchronization methods of performance of parallel applications. ACM SIGMETRICS Performance Evaluation Review (1991) 19:120–132.[CrossRef]
  32. Heyman T, Geist D, Grumberg O, Schuster A. Achieving scalability in parallel reachability analysis of very large circuits. In: Proceedings of the Computer Aided Verification’00 (2000) Springer. 20–35. Vol. 1855 of Lecture Notes in Computer Science.
  33. Inggs CP. Parallel Model Checking On Shared Memory Architectures (2004) UK: University of Manchester. PhD Thesis.
  34. Inggs CP, Barringer H. Effective state exploration for model checking on a shared memory architecture. In: Proceedings of the Parallel and Distributed Methods in verifiCation’02 (2002) Vol. 68 of Electronic Notes in Theoritical Computer Sciencec.
  35. Inggs CP, Barringer H. CTL* model checking on a shared-memory architecture. Formal Methods in System Design (2006) 29:135–155.[CrossRef][Web of Science]
  36. Itai A, Rodeh M. Symmetry breaking in distributed networks. Information and Computation (1990) 88:60–87.[CrossRef][Web of Science]
  37. Kam T, Villa T, Brayton RK, Sangiovanni-Vincentelli AL. Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic (1998) 4:9–62.[Medline]
  38. Knottenbelt WJ, Harrison PG, Mestern MA, Kritzinger PS. A probabilistic dynamic technique for the distributed generation of very large state spaces. Performance Evaluation (2000) 39:127–148.[CrossRef][Web of Science]
  39. Lerda F, Sisto R. Distributed-memory model checking with SPIN. In: Proceedings of the SPIN’99 (1999) Springer. 22–39. Vol. 1680 of Lecture Notes in Computer Science.
  40. Lucco S. A dynamic scheduling method for irregular parallel programs. In: Proceedings of the Programming Language Design and Implementation’92 (1992) ACM. 200–211.
  41. McMillan K. Symbolic Model Checking (1993) Kluwer.
  42. Milvang-Jensen K, Hu AJ. BDDNOW: a parallel BDD package. In: Proceedings of the Formal Methods in Computer-Aided Design’98 (1998) Springer. 501–507. Vol. 1522 of Lecture Notes in Computer Science.
  43. Miner AS, Ciardo G. Efficient reachability set generation and storage using decision diagrams. (1999) Springer. 6–25. In Proceedings of the Application and Theory of Petri Nets, 21st International Conference’99. Vol. 1639 of Lecture Notes in Computer Science.
  44. Pastor E, Roig O, Cortadella J, Badia RM. Petri net analysis using boolean manipulation. In: Proceedings of the Petri Nets and Performance Models’94 (1994) Springer. 416–435. Vol. 815 of Lecture Notes in Computer Science.
  45. Prechelt L, Hanssgen SU. Efficient parallel execution of irregular recursive programs. IEEE Transanctions on Parallel and Distributed Systems (2002) 13:167–178.[CrossRef]
  46. Queille JP, Sifakis J. Specification and verification of concurrent systems in CESAR. (1982) Springer. 337–351. In Proceedings of the 5th International Symposium on Programming. Vol. 137 of Lecture Notes in Computer Science.
  47. Siminiceanu RI, Ciardo G. Formal verification of the NASA runway safety monitor. Software Tools for Technology Transfer (2007) 9:63–76.[CrossRef]
  48. Solé M, Pastor E. Traversal techniques for concurrent systems. In: Proceedings of the Formal Methods in Computer-Aided Design’02 (2002) Springer. 220–237. Vol. 2517 of Lecture Notes in Computer Science.
  49. Stern U, Dill DL. Parallelizing the Mur{varphi} verifier. Formal Methods in System Design (2001) 18:117–129.[CrossRef][Web of Science]
  50. Stornetta T, Brewer F. Implementation of an efficient parallel BDD package. (1996) ACM. 641–644. Proceedings of the Conference on Design Automation’96.
  51. Tilgner M, Takahashi Y, Ciardo G. SNS 1.0: synchronized network solver. (1996) 215–234. In Proceedings of the Application and Theory of Petri Nets, 21st International Conference’96.
  52. Yang T, Fu C. Space/time-efficient scheduling and execution of parallel irregular computations. ACM Transaction on Programming Languages and Systems (1998) 20:1195–1222.[CrossRef]

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 Ezekiel, J.
Right arrow Articles by Siminiceanu, R.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?