Sylvan: multi-core decision diagrams

Tom van Dijk

Research output: ThesisPhD Thesis - Research UT, graduation UT

Abstract

This thesis studies the parallelization of decision diagrams, a fundamental data-structure with applications in many fields, in particular symbolic model checking. Research into parallel processing is essential, as multi-core and many-core computers are ubiquitous. Graph algorithms such as decision diagram operations are known to be difficult to parallelize, as well as difficult to reason about. This is one of the reasons why parallelizing symbolic model checking is difficult. The main result of this research is the multi-core decision diagram package Sylvan. We investigate scalable hash tables, load balancing via work stealing, using Sylvan for symbolic state space exploration and for symbolic bisimulation minimization. The experimental results show high parallel speedup of up to 38x for benchmarks on a 48-core computer. Experiments that compare Sylvan to non-parallel decision diagram packages show that Sylvan is competitive when run with a single core, and faster when run with multiple cores.
LanguageEnglish
Awarding Institution
  • University of Twente
Supervisors/Advisors
  • van de Pol, Jan Cornelis, Supervisor
Thesis sponsors
Award date13 Jul 2016
Place of PublicationEnschede
Publisher
Print ISBNs978-90-365-4160-2
DOIs
StatePublished - 13 Jul 2016

Fingerprint

Model checking
Resource allocation
Data structures
Processing
Experiments

Keywords

  • IR-100676
  • METIS-317253

Cite this

van Dijk, T. (2016). Sylvan: multi-core decision diagrams Enschede: Universiteit Twente DOI: 10.3990/1.9789036541602
van Dijk, Tom. / Sylvan : multi-core decision diagrams. Enschede : Universiteit Twente, 2016. 154 p.
@phdthesis{b8ef8a430b7b4955a0bdf00e07ab55d2,
title = "Sylvan: multi-core decision diagrams",
abstract = "This thesis studies the parallelization of decision diagrams, a fundamental data-structure with applications in many fields, in particular symbolic model checking. Research into parallel processing is essential, as multi-core and many-core computers are ubiquitous. Graph algorithms such as decision diagram operations are known to be difficult to parallelize, as well as difficult to reason about. This is one of the reasons why parallelizing symbolic model checking is difficult. The main result of this research is the multi-core decision diagram package Sylvan. We investigate scalable hash tables, load balancing via work stealing, using Sylvan for symbolic state space exploration and for symbolic bisimulation minimization. The experimental results show high parallel speedup of up to 38x for benchmarks on a 48-core computer. Experiments that compare Sylvan to non-parallel decision diagram packages show that Sylvan is competitive when run with a single core, and faster when run with multiple cores.",
keywords = "IR-100676, METIS-317253",
author = "{van Dijk}, Tom",
note = "CTIT Ph.D. thesis series no. 16-398 IPA dissertation series no. 2016-09",
year = "2016",
month = "7",
day = "13",
doi = "10.3990/1.9789036541602",
language = "English",
isbn = "978-90-365-4160-2",
publisher = "Universiteit Twente",
school = "University of Twente",

}

van Dijk, T 2016, 'Sylvan: multi-core decision diagrams', University of Twente, Enschede. DOI: 10.3990/1.9789036541602

Sylvan : multi-core decision diagrams. / van Dijk, Tom.

Enschede : Universiteit Twente, 2016. 154 p.

Research output: ThesisPhD Thesis - Research UT, graduation UT

TY - THES

T1 - Sylvan

T2 - multi-core decision diagrams

AU - van Dijk,Tom

N1 - CTIT Ph.D. thesis series no. 16-398 IPA dissertation series no. 2016-09

PY - 2016/7/13

Y1 - 2016/7/13

N2 - This thesis studies the parallelization of decision diagrams, a fundamental data-structure with applications in many fields, in particular symbolic model checking. Research into parallel processing is essential, as multi-core and many-core computers are ubiquitous. Graph algorithms such as decision diagram operations are known to be difficult to parallelize, as well as difficult to reason about. This is one of the reasons why parallelizing symbolic model checking is difficult. The main result of this research is the multi-core decision diagram package Sylvan. We investigate scalable hash tables, load balancing via work stealing, using Sylvan for symbolic state space exploration and for symbolic bisimulation minimization. The experimental results show high parallel speedup of up to 38x for benchmarks on a 48-core computer. Experiments that compare Sylvan to non-parallel decision diagram packages show that Sylvan is competitive when run with a single core, and faster when run with multiple cores.

AB - This thesis studies the parallelization of decision diagrams, a fundamental data-structure with applications in many fields, in particular symbolic model checking. Research into parallel processing is essential, as multi-core and many-core computers are ubiquitous. Graph algorithms such as decision diagram operations are known to be difficult to parallelize, as well as difficult to reason about. This is one of the reasons why parallelizing symbolic model checking is difficult. The main result of this research is the multi-core decision diagram package Sylvan. We investigate scalable hash tables, load balancing via work stealing, using Sylvan for symbolic state space exploration and for symbolic bisimulation minimization. The experimental results show high parallel speedup of up to 38x for benchmarks on a 48-core computer. Experiments that compare Sylvan to non-parallel decision diagram packages show that Sylvan is competitive when run with a single core, and faster when run with multiple cores.

KW - IR-100676

KW - METIS-317253

U2 - 10.3990/1.9789036541602

DO - 10.3990/1.9789036541602

M3 - PhD Thesis - Research UT, graduation UT

SN - 978-90-365-4160-2

PB - Universiteit Twente

CY - Enschede

ER -

van Dijk T. Sylvan: multi-core decision diagrams. Enschede: Universiteit Twente, 2016. 154 p. Available from, DOI: 10.3990/1.9789036541602