Distributed Binary Decision Diagrams for Symbolic Reachability

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2 Citations

Abstract

Decision diagrams are used in symbolic verification to concisely represent state spaces. A crucial symbolic verification algorithm is reachability: systematically exploring all reachable system states. Although both parallel and distributed reachability algorithms exist, a combined solution is relatively unexplored. This paper contributes BDD-based reachability algorithms targeting compute clusters: high-performance networks of multi-core machines. The proposed algorithms may use the entire memory of every machine, allowing larger models to be processed while increasing performance by using all available computational power. To do this effectively, a distributed hash table, cluster-based work stealing algorithms, and several caching structures have been designed that all utilise the newest networking technology. The approach is evaluated extensively on a large collection of models, thereby demonstrating speedups up to 51,1x with 32 machines. The proposed algorithms not only benefit from the large amounts of available memory on compute clusters, but also from all available computational resources.
LanguageEnglish
Title of host publicationSPIN 2017 Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software
PublisherAssociation for Computing Machinery
Pages21-30
Number of pages10
ISBN (Print)978-1-4503-5077-8
DOIs
StatePublished - Jul 2017
Event24th International SPIN Symposium 2017 - University of California, Santa Barbara, United States
Duration: 13 Jul 201714 Jul 2017
Conference number: 24
http://conf.researchr.org/home/spin-2017

Conference

Conference24th International SPIN Symposium 2017
Abbreviated titleSPIN 2017
CountryUnited States
CitySanta Barbara
Period13/07/1714/07/17
Internet address

Fingerprint

Binary decision diagrams
Data storage equipment
Network performance
Parallel algorithms

Keywords

  • Symbolic model checking
  • parallel computing
  • distributed computing
  • high-performance computing
  • reachability analysis

Cite this

Oortwijn, W., van Dijk, T., & van de Pol, J. (2017). Distributed Binary Decision Diagrams for Symbolic Reachability. In SPIN 2017 Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software (pp. 21-30). Association for Computing Machinery. DOI: 10.1145/3092282.3092284
Oortwijn, Wytse ; van Dijk, Tom ; van de Pol, Jaco. / Distributed Binary Decision Diagrams for Symbolic Reachability. SPIN 2017 Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software. Association for Computing Machinery, 2017. pp. 21-30
@inproceedings{1c7dd725328c47f4b4cd99f5a5ccdc52,
title = "Distributed Binary Decision Diagrams for Symbolic Reachability",
abstract = "Decision diagrams are used in symbolic verification to concisely represent state spaces. A crucial symbolic verification algorithm is reachability: systematically exploring all reachable system states. Although both parallel and distributed reachability algorithms exist, a combined solution is relatively unexplored. This paper contributes BDD-based reachability algorithms targeting compute clusters: high-performance networks of multi-core machines. The proposed algorithms may use the entire memory of every machine, allowing larger models to be processed while increasing performance by using all available computational power. To do this effectively, a distributed hash table, cluster-based work stealing algorithms, and several caching structures have been designed that all utilise the newest networking technology. The approach is evaluated extensively on a large collection of models, thereby demonstrating speedups up to 51,1x with 32 machines. The proposed algorithms not only benefit from the large amounts of available memory on compute clusters, but also from all available computational resources.",
keywords = "Symbolic model checking, parallel computing, distributed computing, high-performance computing, reachability analysis",
author = "Wytse Oortwijn and {van Dijk}, Tom and {van de Pol}, Jaco",
year = "2017",
month = "7",
doi = "10.1145/3092282.3092284",
language = "English",
isbn = "978-1-4503-5077-8",
pages = "21--30",
booktitle = "SPIN 2017 Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software",
publisher = "Association for Computing Machinery",
address = "United States",

}

Oortwijn, W, van Dijk, T & van de Pol, J 2017, Distributed Binary Decision Diagrams for Symbolic Reachability. in SPIN 2017 Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software. Association for Computing Machinery, pp. 21-30, 24th International SPIN Symposium 2017, Santa Barbara, United States, 13/07/17. DOI: 10.1145/3092282.3092284

Distributed Binary Decision Diagrams for Symbolic Reachability. / Oortwijn, Wytse; van Dijk, Tom; van de Pol, Jaco.

SPIN 2017 Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software. Association for Computing Machinery, 2017. p. 21-30.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Distributed Binary Decision Diagrams for Symbolic Reachability

AU - Oortwijn,Wytse

AU - van Dijk,Tom

AU - van de Pol,Jaco

PY - 2017/7

Y1 - 2017/7

N2 - Decision diagrams are used in symbolic verification to concisely represent state spaces. A crucial symbolic verification algorithm is reachability: systematically exploring all reachable system states. Although both parallel and distributed reachability algorithms exist, a combined solution is relatively unexplored. This paper contributes BDD-based reachability algorithms targeting compute clusters: high-performance networks of multi-core machines. The proposed algorithms may use the entire memory of every machine, allowing larger models to be processed while increasing performance by using all available computational power. To do this effectively, a distributed hash table, cluster-based work stealing algorithms, and several caching structures have been designed that all utilise the newest networking technology. The approach is evaluated extensively on a large collection of models, thereby demonstrating speedups up to 51,1x with 32 machines. The proposed algorithms not only benefit from the large amounts of available memory on compute clusters, but also from all available computational resources.

AB - Decision diagrams are used in symbolic verification to concisely represent state spaces. A crucial symbolic verification algorithm is reachability: systematically exploring all reachable system states. Although both parallel and distributed reachability algorithms exist, a combined solution is relatively unexplored. This paper contributes BDD-based reachability algorithms targeting compute clusters: high-performance networks of multi-core machines. The proposed algorithms may use the entire memory of every machine, allowing larger models to be processed while increasing performance by using all available computational power. To do this effectively, a distributed hash table, cluster-based work stealing algorithms, and several caching structures have been designed that all utilise the newest networking technology. The approach is evaluated extensively on a large collection of models, thereby demonstrating speedups up to 51,1x with 32 machines. The proposed algorithms not only benefit from the large amounts of available memory on compute clusters, but also from all available computational resources.

KW - Symbolic model checking

KW - parallel computing

KW - distributed computing

KW - high-performance computing

KW - reachability analysis

U2 - 10.1145/3092282.3092284

DO - 10.1145/3092282.3092284

M3 - Conference contribution

SN - 978-1-4503-5077-8

SP - 21

EP - 30

BT - SPIN 2017 Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software

PB - Association for Computing Machinery

ER -

Oortwijn W, van Dijk T, van de Pol J. Distributed Binary Decision Diagrams for Symbolic Reachability. In SPIN 2017 Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software. Association for Computing Machinery. 2017. p. 21-30. Available from, DOI: 10.1145/3092282.3092284