Multi-core Decision Diagrams

Chapter

Abstract

Decision diagrams are fundamental data structures that revolutionized fields such as model checking, automated reasoning and decision processes. As performance gains in the current era mostly come from parallel processing, an ongoing challenge is to develop data structures and algorithms for modern multicore architectures. This chapter describes the parallelization of decision diagram operations as implemented in the parallel decision diagram package Sylvan, which allows sequential algorithms that use decision diagrams to exploit the power of multi-core machines.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    Magdy S. Abadir and Hassan K. Reghbati. Functional Test Generation for Digital Circuits Described Using Binary Decision Diagrams. IEEE Trans. Computers, 35(4):375–379, 1986.Google Scholar
  2. [2]
    Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Scheduling parallel programs by work stealing with private deques. In PPOPP, pages 219–228. ACM, 2013.Google Scholar
  3. [3]
    S.B. Akers. Binary Decision Diagrams. IEEE Trans. Computers, C-27(6):509–516, 6 1978.Google Scholar
  4. [4]
    Prakash Arunachalam, Craig M. Chase, and Dinos Moundanos. Distributed binary decision diagrams for verification of large circuit. In ICCD, pages 365–370, 1996.Google Scholar
  5. [5]
    R. Iris Bahar, Erica A. Frohm, Charles M. Gaona, Gary D. Hachtel, Enrico Macii, Abelardo Pardo, and Fabio Somenzi. Algebraic decision diagrams and their applications. In ICCAD 1993, pages 188–191, 1993.Google Scholar
  6. [6]
    Debashis Bhattacharya, Prathima Agrawal, and Vishwani D. Agrawal. Test Generation for Path Delay Faults Using Binary Decision Diagrams. IEEE Trans. Computers, 44(3):434–447, 1995.Google Scholar
  7. [7]
    F. Bianchi, Fulvio Corno, Maurizio Rebaudengo, Matteo Sonza Reorda, and Roberto Ansaloni. Boolean function manipulation on a parallel system using BDDs. In HPCN Europe, pages 916–928, 1997.Google Scholar
  8. [8]
    Stefan Blom and Simona Orzan. Distributed Branching Bisimulation Reduction of State Spaces. ENTCS, 89(1):99–113, 2003.Google Scholar
  9. [9]
    Stefan Blom, Jaco van de Pol, and Michael Weber. LTSmin: Distributed and Symbolic Reachability. In CAV, volume 6174 of LNCS, pages 354–359. Springer, 2010.Google Scholar
  10. [10]
    Robert D. Blumofe. Scheduling multithreaded computations by work stealing. In FOCS, pages 356–368. IEEE Computer Society, 1994.Google Scholar
  11. [11]
    Robert D. Blumofe, Christopher F. Joerg, Bradley C. Kuszmaul, Charles E. Leiserson, Keith H. Randall, and Yuli Zhou. Cilk: An Efficient Multithreaded Runtime System. J. Parallel Distrib. Comput., 37(1):55–69, 1996.Google Scholar
  12. [12]
    Marco Bozzano, Alessandro Cimatti, and Francesco Tapparo. Symbolic fault tree analysis for reactive systems. In ATVA 2007, volume 4762 of LNCS, pages 162–176. Springer, 2007.Google Scholar
  13. [13]
    Karl S. Brace, Richard L. Rudell, and Randal E. Bryant. Efficient implementation of a BDD package. In DAC, pages 40–45, 1990.Google Scholar
  14. [14]
    Randal E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers, C-35(8):677–691, 8 1986.Google Scholar
  15. [15]
    Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L. J. Hwang. Symbolic model checking: 10ˆ20 states and beyond. Inf. Comput., 98(2):142–170, 1992.Google Scholar
  16. [16]
    J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, and D.L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4):401–424, 4 1994.Google Scholar
  17. [17]
    G.P. Cabodi, S. Gai, and M. Sonza Reorda. Boolean function manipulation on massively parallel computers. In Proc. of 4th Symp. on Frontiers of Massively Parallel Computation, pages 508–509. IEEE, 10 1992.Google Scholar
  18. [18]
    Jer-Sheng Chen and P. Banerjee. Parallel construction algorithms for BDDs. In ISCAS 1999, pages 318–322. IEEE, 1999.Google Scholar
  19. [19]
    Ming-Ying Chung and Gianfranco Ciardo. Saturation NOW. In QEST, pages 272–281. IEEE Computer Society, 2004.Google Scholar
  20. [20]
    Gianfranco Ciardo, Gerald Lüttgen, and Radu Siminiceanu. Saturation: An Efficient Iteration Strategy for Symbolic State-Space Generation. In TACAS, volume 2031 of LNCS, pages 328–342, 2001.Google Scholar
  21. [21]
    Gianfranco Ciardo, Yang Zhao, and Xiaoqing Jin. Parallel symbolic state-space exploration is difficult, but what is the alternative? In PDMC, pages 1–17, 2009.Google Scholar
  22. [22]
    Edmund M. Clarke, Kenneth L. McMillan, Xudong Zhao, Masahiro Fujita, and J. Yang. Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. In DAC, pages 54–60, 1993.Google Scholar
  23. [23]
    Jonathan Ezekiel, Gerald Lüttgen, and Gianfranco Ciardo. Parallelising symbolic state-space generators. In CAV, volume 4590 of LNCS, pages 268–280, 2007.Google Scholar
  24. [24]
    Karl-Filip Faxén. Wool–A work stealing library. SIGARCH Computer Architecture News, 36(5):93–100, 2008.Google Scholar
  25. [25]
    Karl-Filip Faxén. Efficient work stealing for fine grained parallelism. In ICPP 2010, pages 313–322. IEEE Computer Society, 2010.Google Scholar
  26. [26]
    Kathi Fisler, Shriram Krishnamurthi, Leo A. Meyerovich, and Michael Carl Tschantz. Verification and change-impact analysis of access-control policies. In ICSE 2005, pages 196–205. ACM, 2005.Google Scholar
  27. [27]
    Matteo Frigo, Charles E. Leiserson, and Keith H. Randall. The Implementation of the Cilk-5 Multithreaded Language. In PLDI, pages 212–223. ACM, 1998.Google Scholar
  28. [28]
    S. Gai, M. Rebaudengo, and M. Sonza Reorda. An improved data parallel algorithm for Boolean function manipulation using BDDs. In Proc. Euromicro Workshop on Par. and Distrib. Processing, pages 33–39. IEEE, 1 1995.Google Scholar
  29. [29]
    Orna Grumberg, Tamir Heyman, and Assaf Schuster. A work-efficient distributed algorithm for reachability analysis. Formal Methods in System Design, 29(2):157–175, 2006.Google Scholar
  30. [30]
    Ernst Moritz Hahn, Yi Li, Sven Schewe, Andrea Turrini, and Lijun Zhang. iscasmc: A web-based probabilistic model checker. In FM, volume 8442 of LNCS, pages 312–317. Springer, 2014.Google Scholar
  31. [31]
    Tamir Heyman, Danny Geist, Orna Grumberg, and Assaf Schuster. Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. In Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 20–35. Springer Berlin / Heidelberg, 2000.Google Scholar
  32. [32]
    Masakazu Ishihata, Taisuke Sato, and Shin-ichi Minato. Compiling Bayesian networks for parameter learning based on shared BDDs. In AI 2011, volume 7106 of Lecture Notes in Computer Science, pages 203–212. Springer, 2011.Google Scholar
  33. [33]
    Gijs Kant, Alfons Laarman, Jeroen Meijer, Jaco van de Pol, Stefan Blom, and Tom van Dijk. LTSmin: High-Performance Language-Independent Model Checking. In TACAS 2015, volume 9035 of LNCS, pages 692–707. Springer, 2015.Google Scholar
  34. [34]
    S. Kimura and E.M. Clarke. A parallel algorithm for constructing binary decision diagrams. In Proc. of IC on Computer Design: VLSI in Computers and Processors ICCD, pages 220–223, 9 1990.Google Scholar
  35. [35]
    S. Kimura, T. Igaki, and H. Haneda. Parallel Binary Decision Diagram Manipulation. IEICE Transactions on Fundamentals of Electronics, Communications and Computer Science, E75-A(10):1255–62, 10 1992.Google Scholar
  36. [36]
    Alfons Laarman, Jaco van de Pol, and Michael Weber. Boosting multi-core reachability performance with shared hash tables. In FMCAD 2010, pages 247–255. IEEE, 2010.Google Scholar
  37. [37]
    Alfons W. Laarman, Jaco van de Pol, and Michael Weber. Multi-Core LTSmin: Marrying Modularity and Scalability. In NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings, volume 6617 of LNCS, pages 506–511. Springer, 2011.Google Scholar
  38. [38]
    Elsa Loekito and James Bailey. Fast mining of high dimensional expressive contrast patterns using zero-suppressed binary decision diagrams. In SIGKDD 2006, pages 307–316. ACM, 2006.Google Scholar
  39. [39]
    Alberto Lovato, Damiano Macedonio, and Fausto Spoto. A Thread-Safe Library for Binary Decision Diagrams. In SEFM, volume 8702 of LNCS, pages 35–49. Springer, 2014.Google Scholar
  40. [40]
    Sharad Malik, Albert R. Wang, Robert K. Brayton, and Alberto L. Sangiovanni-Vincentelli. Logic verification using binary decision diagrams in a logic synthesis environment. In ICCAD 1998, pages 6–9, 1988.Google Scholar
  41. [41]
    Yusuke Matsunaga and Masahiro Fujita. Multi-level logic optimization using binary decision diagrams. In ICCAD 1989, pages 556–559. IEEE, 1989.Google Scholar
  42. [42]
    Jeroen Meijer, Gijs Kant, Stefan Blom, and Jaco van de Pol. Read, Write and Copy Dependencies for Symbolic Model Checking. In Eran Yahav, editor, HVC, volume 8855 of Lecture Notes in Computer Science, pages 204–219. Springer, 2014.Google Scholar
  43. [43]
    Kim Milvang-Jensen and Alan J. Hu. BDDNOW: A parallel BDD package. In FMCAD, pages 501–507, 1998.Google Scholar
  44. [44]
    Shin-ichi Minato. Techniques of BDD/ZDD: Brief History and Recent Activity. IEICE Transactions, 96-D(7):1419–1429, 2013.Google Scholar
  45. [45]
    Shin-ichi Minato, Ken Satoh, and Taisuke Sato. Compiling Bayesian networks by symbolic probability calculation based on zero-suppressed BDDs. In IJCAI 2007, pages 2550–2555, 2007.Google Scholar
  46. [46]
    Hiroyuki Ochi, Nagisa Ishiura, and Shuzo Yajima. Breadth-first manipulation of SBDD of Boolean functions for vector processing. In DAC, pages 413–416, 1991.Google Scholar
  47. [47]
    Wytse Oortwijn. Distributed Symbolic Reachability Analysis. Master’s thesis, University of Twente, Dept. of C.S., 2015.Google Scholar
  48. [48]
    Wytse Oortwijn, Tom van Dijk, and Jaco van de Pol. Distributed Binary Decision Diagrams for Symbolic Reachability. In SPIN, pages 21–30. ACM, 2017.Google Scholar
  49. [49]
    Jörn Ossowski. JINC – A Multi-Threaded Library for Higher-Order Weighted Decision Diagram Manipulation. PhD thesis, Rheinische Friedrich-Wilhelms-Universität Bonn, 10 2010.Google Scholar
  50. [50]
    Yegnashankar Parasuram, Edward P. Stabler, and Shiu-Kai Chin. Parallel implementation of BDD algorithms using a distributed shared memory. In HICSS (1), pages 16–25, 1994.Google Scholar
  51. [51]
    Radek Pelánek. BEEM: benchmarks for explicit model checkers. In SPIN, pages 263–267, Berlin, Heidelberg, 2007. Springer-Verlag.Google Scholar
  52. [52]
    Karen A. Reay and John D. Andrews. A fault tree analysis strategy using binary decision diagrams. Rel. Eng. & Sys. Safety, 78(1):45–56, 2002.Google Scholar
  53. [53]
    Yuko Sakurai, Suguru Ueda, Atsushi Iwasaki, Shin-ichi Minato, and Makoto Yokoo. A compact representation scheme of coalitional games based on multiterminal zero-suppressed binary decision diagrams. In PRIMA 2011, volume 7047 of Lecture Notes in Computer Science, pages 4–18. Springer, 2011.Google Scholar
  54. [54]
    Jagesh V. Sanghavi, Rajeev K. Ranjan, Robert K. Brayton, and Alberto L. Sangiovanni-Vincentelli. High performance BDD package by exploiting memory hiercharchy. In DAC, pages 635–640, 1996.Google Scholar
  55. [55]
    Mathias Soeken, Laura Tague, Gerhard W. Dueck, and Rolf Drechsler. Ancillafree synthesis of large reversible functions using binary decision diagrams. J. Symb. Comput., 73:1–26, 2016.Google Scholar
  56. [56]
    Fabio Somenzi. Efficient manipulation of decision diagrams. STTT, 3(2):171–181, 2001.Google Scholar
  57. [57]
    Fabio Somenzi. CUDD: CU decision diagram package release 3.0.0. http://vlsi.colorado.edu/~fabio/CUDD/, 2015.
  58. [58]
    Tony Stornetta and Forrest Brewer. Implementation of an efficient parallel BDD package. In DAC, pages 641–644, 1996.Google Scholar
  59. [59]
    Tom van Dijk. Sylvan: Multi-core Decision Diagrams. PhD thesis, University of Twente, 7 2016.Google Scholar
  60. [60]
    Tom van Dijk, Ernst Moritz Hahn, David N. Jansen, Yong Li, Thomas Neele, Mariëlle Stoelinga, Andrea Turrini, and Lijun Zhang. A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. In SETTA, volume 9409 of LNCS, pages 35–51. Springer, 2015.Google Scholar
  61. [61]
    Tom van Dijk, Alfons Laarman, and Jaco van de Pol. Multi-core BDD operations for symbolic reachability. ENTCS, 296:127–143, 2013.Google Scholar
  62. [62]
    Tom van Dijk, Alfons W. Laarman, and Jaco van de Pol. Multi-core and/or Symbolic Model Checking. ECEASST, 53, 2012.Google Scholar
  63. [63]
    Tom van Dijk and Jaco van de Pol. Lace: Non-blocking Split Deque for Work-Stealing. In MuCoCoS, volume 8806 of LNCS, pages 206–217. Springer, 2014.Google Scholar
  64. [64]
    Tom van Dijk and Jaco van de Pol. Sylvan: Multi-Core Decision Diagrams. In TACAS, volume 9035 of LNCS, pages 677–691. Springer, 2015.Google Scholar
  65. [65]
    Tom van Dijk and Jaco van de Pol. Multi-Core Symbolic Bisimulation Minimisation. In TACAS, volume 9636 of LNCS, pages 332–348. Springer, 2016.Google Scholar
  66. [66]
    Tom van Dijk and Jaco van de Pol. Sylvan: multi-core framework for decision diagrams. International Journal on Software Tools for Technology Transfer, 19(6) pp 675–696, 2017.Google Scholar
  67. [67]
    Tom van Dijk and Jaco van de Pol. Multi-core symbolic bisimulation minimisation. International Journal on Software Tools for Technology Transfer, 2017. Published online, August 2017.Google Scholar
  68. [68]
    Miroslav N. Velev and Ping Gao. Efficient parallel GPU algorithms for BDD manipulation. In ASP-DAC, pages 750–755. IEEE, 2014.Google Scholar
  69. [69]
    David B. Wagner and Brad Calder. Leapfrogging: A portable technique for implementing efficient futures. In PPOPP, pages 208–217. ACM, 1993.Google Scholar
  70. [70]
    Ralf Wimmer, Marc Herbstritt, Holger Hermanns, Kelley Strampp, and Bernd Becker. Sigref – A Symbolic Bisimulation Tool Box. In ATVA, volume 4218 of LNCS, pages 477–492. Springer, 2006.Google Scholar
  71. [71]
    Bwolen Yang and David R. O’Hallaron. Parallel breadth-first BDD construction. In PPOPP, pages 145–156, 1997.Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Institute for Formal Methods and VerificationJohannes Kepler UniversityLinzAustria
  2. 2.Formal Methods and ToolsUniversity of TwenteEnschedeThe Netherlands

Personalised recommendations