Sylvan: multi-core decision diagrams

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    196 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

    Keywords

    • IR-100676
    • METIS-317253

    Cite this