Sylvan: multi-core decision diagrams

Research output: ThesisPhD Thesis - Research UT, graduation UT

318 Downloads (Pure)

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 languageEnglish
Awarding Institution
  • University of Twente
Supervisors/Advisors
  • van de Pol, Jaco , Supervisor
Thesis sponsors
Award date13 Jul 2016
Place of PublicationEnschede
Publisher
Print ISBNs978-90-365-4160-2
DOIs
Publication statusPublished - 13 Jul 2016

Fingerprint

Dive into the research topics of 'Sylvan: multi-core decision diagrams'. Together they form a unique fingerprint.

Cite this