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.
Original languageEnglish
Title of host publicationSPIN 2017 Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software
PublisherACM
Pages21-30
Number of pages10
ISBN (Print)978-1-4503-5077-8
DOIs
StatePublished - Jul 2017
Event24th International SPIN Symposium 2017 - Santa Barbara, United States

Conference

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

Fingerprint

Binary decision diagrams
Network performance
Parallel algorithms

Keywords

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

Cite this

Oortwijn, W., Dijk, T. V., & Pol, J. V. D. (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). ACM. DOI: 10.1145/3092282.3092284

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

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

Research output: Scientific - peer-reviewConference contribution

@inbook{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 Dijk, {Tom van} and Pol, {Jaco van de}",
year = "2017",
month = "7",
doi = "10.1145/3092282.3092284",
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 = "ACM",

}

Oortwijn, W, Dijk, TV & Pol, JVD 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. ACM, pp. 21-30, 24th International SPIN Symposium 2017, Santa Barbara, United States, 13-14 July. DOI: 10.1145/3092282.3092284

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

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

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Distributed Binary Decision Diagrams for Symbolic Reachability

AU - Oortwijn,Wytse

AU - Dijk,Tom van

AU - Pol,Jaco van de

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 - ACM

ER -

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