Abstract
Decision diagrams such as binary decision diagrams and multi-valued decision diagrams play an important role in various fields, including symbolic model checking. An ongoing challenge is to develop datastructures and algorithms for modern multi-core architectures. The BDD package Sylvan provides one contribution by implementing parallelized BDD operations and thus allowing sequential algorithms to exploit the power of multi-core machines.
We present several extensions to Sylvan. We implement parallel operations on list decision diagrams, a variant of multi-valued decision diagrams that is useful for symbolic model checking. We also substitute several core components of Sylvan by new designs, such as the work-stealing framework, the unique table and the operation cache. Furthermore, we combine parallel operations with parallelization on a higher level, by partitioning the transition relation. We show that this results in an improved speedup using the model checking toolset ltsmin. We also demonstrate that the parallelization of symbolic model checking for explicit-state modeling languages with an on-the-fly next-state function, as supported by ltsmin, scales well.
Chapter PDF
Similar content being viewed by others
Keywords
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
Akers, S.: Binary Decision Diagrams. IEEE Trans. Computers C-27(6), 509–516 (1978)
Blom, S., van de Pol, J.: Symbolic Reachability for Process Algebras with Recursive Data Types. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 81–95. Springer, Heidelberg (2008)
Blom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354–359. Springer, Heidelberg (2010)
Blumofe, R.D.: Scheduling multithreaded computations by work stealing. In: FOCS, pp. 356–368. IEEE Computer Society (1994)
Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers C-35(8), 677–691 (1986)
Burch, J.R., Clarke, E.M., Long, D.E., McMillan, K.L., Dill, D.L.: Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 13(4), 401–424 (1994)
Chung, M.Y., Ciardo, G.: Saturation NOW. In: QEST, pp. 272–281. IEEE Computer Society (2004)
Ciardo, G., Marmorstein, R.M., Siminiceanu, R.: Saturation Unbound. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 379–393. Springer, Heidelberg (2003)
van Dijk, T.: The Parallelization of Binary Decision Diagram operations for model checking. Master’s thesis, University of Twente, Dept. of C.S (April 2012)
van Dijk, T., Laarman, A.W., van de Pol, J.C.: Multi-core and/or Symbolic Model Checking. ECEASST 53 (2012)
van Dijk, T., Laarman, A.W., van de Pol, J.C.: Multi-Core BDD Operations for Symbolic Reachability. In: 11th International Workshop on Parallel and Distributed Methods in verification. ENTCS. Elsevier (2012)
van Dijk, T., van de Pol, J.C.: Lace: non-blocking split deque for work-stealing. In: Lopes, L., et al. (eds.) Euro-Par 2014, Part II. LNCS, vol. 8806, pp. 206–217. Springer, Heidelberg (2014)
Ezekiel, J., Lüttgen, G., Ciardo, G.: Parallelising symbolic state-space generators. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 268–280. Springer, Heidelberg (2007)
Faxén, K.F.: Efficient work stealing for fine grained parallelism. In: 39th International Conference on Parallel Processing (ICPP), pp. 313–322. IEEE Computer Society, Los Alamitos (2010)
Grumberg, O., Heyman, T., Schuster, A.: A work-efficient distributed algorithm for reachability analysis. Formal Methods in System Design 29(2), 157–175 (2006)
Kam, T., Villa, T., Brayton, R.K., Sangiovanni-vincentelli, A.L.: Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic 4(1), 9–62 (1998)
Kant, G., Laarman, A.W., Meijer, J., van de Pol, J.C., Blom, S., van Dijk, T.: LTSmin: High-Performance Language-Independent Model Checking. In: TACAS 2015 (2015)
Kimura, S., Igaki, T., Haneda, H.: Parallel Binary Decision Diagram Manipulation. IEICE Transactions on Fundamentals of Electronics, Communications and Computer Science E75-A(10), 1255–1262 (1992)
Laarman, A.W., van de Pol, J.C., Weber, M.: Boosting multi-core reachability performance with shared hash tables. In: Formal Methods in Computer-Aided Design, pp. 247–255. IEEE (October 2010)
Laarman, A.W., van de Pol, J.C., Weber, M.: Multi-Core LTSmin: Marrying Modularity and Scalability. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 506–511. Springer, Heidelberg (2011)
Lovato, A., Macedonio, D., Spoto, F.: A Thread-Safe Library for Binary Decision Diagrams. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 35–49. Springer, Heidelberg (2014)
Miller, D.M., Drechsler, R.: On the Construction of Multiple-Valued Decision Diagrams. In: 32nd IEEE International Symposium on Multiple-Valued Logic (ISMVL 2002), pp. 245–253. IEEE Computer Society (2002)
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)
Ossowski, J.: JINC – A Multi-Threaded Library for Higher-Order Weighted Decision Diagram Manipulation. Ph.D. thesis, Rheinischen Friedrich-Wilhelms-Universität Bonn (October 2010)
Pelánek, R.: BEEM: benchmarks for explicit model checkers. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263–267. Springer, Heidelberg (2007)
Sahoo, D., Jain, J., Iyer, S.K., Dill, D.L., Emerson, E.A.: Multi-threaded reachability. In: Proceedings of the 42nd Annual Design Automation Conference, DAC 2005, pp. 467–470. ACM, New York (2005)
Stornetta, T., Brewer, F.: Implementation of an efficient parallel BDD package. In: Proceedings of the 33rd Annual Design Automation Conference, DAC 1996, pp. 641–644. ACM, New York (1996)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Dijk, T., van de Pol, J. (2015). Sylvan: Multi-Core Decision Diagrams. In: Baier, C., Tinelli, C. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2015. Lecture Notes in Computer Science(), vol 9035. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46681-0_60
Download citation
DOI: https://doi.org/10.1007/978-3-662-46681-0_60
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46680-3
Online ISBN: 978-3-662-46681-0
eBook Packages: Computer ScienceComputer Science (R0)