Sylvan - Multi-core decision diagrams

Tom van Dijk

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.
Original languageUndefined
Supervisors/Advisors
  • van de Pol, Jan Cornelis, Supervisor
Sponsors
Date of Award13 Jul 2016
Place of PublicationEnschede
Publisher
Print ISBNs978-90-365-4160-2
DOIs
StatePublished - 13 Jul 2016

Fingerprint

Model checking
Resource allocation
Data structures
Experiments

Keywords

  • EWI-27576

Cite this

van Dijk, T. (2016). Sylvan - Multi-core decision diagrams Enschede: Centre for Telematics and Information Technology (CTIT) DOI: 10.3990/1.9789036541602
van Dijk, Tom. / Sylvan - Multi-core decision diagrams. Enschede : Centre for Telematics and Information Technology (CTIT), 2016. 172 p.
@misc{6321e0ea2efe4efea62d87ca5b158200,
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 = "EWI-27576",
author = "{van Dijk}, Tom",
year = "2016",
month = "7",
doi = "10.3990/1.9789036541602",
isbn = "978-90-365-4160-2",
publisher = "Centre for Telematics and Information Technology (CTIT)",
address = "Netherlands",

}

Sylvan - Multi-core decision diagrams. / van Dijk, Tom.

Enschede : Centre for Telematics and Information Technology (CTIT), 2016. 172 p.

Research output: ScientificPhD Thesis - Research UT, graduation UT

TY - THES

T1 - Sylvan - Multi-core decision diagrams

AU - van Dijk,Tom

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 - EWI-27576

U2 - 10.3990/1.9789036541602

DO - 10.3990/1.9789036541602

M3 - PhD Thesis - Research UT, graduation UT

SN - 978-90-365-4160-2

PB - Centre for Telematics and Information Technology (CTIT)

ER -

van Dijk T. Sylvan - Multi-core decision diagrams. Enschede: Centre for Telematics and Information Technology (CTIT), 2016. 172 p. Available from, DOI: 10.3990/1.9789036541602