Paper Info
Title
Sylvan: Multi-Core Decision Diagrams.
Abstract
Decision diagrams such as binary decision diagrams and multi-valued decision diagrams play an important role in various fields, including symbolic model checking. An ongoing challenge is to develop datastructures and algorithms for modern multi-core architectures. The BDD package Sylvan provides one contribution by implementing parallelized BDD operations and thus allowing sequential algorithms to exploit the power of multi-core machines. We present several extensions to Sylvan. We implement parallel operations on list decision diagrams, a variant of multi-valued decision diagrams that is useful for symbolic model checking. We also substitute several core components of Sylvan by new designs, such as the work-stealing framework, the unique table and the operation cache. Furthermore, we combine parallel operations with parallelization on a higher level, by partitioning the transition relation. We show that this results in an improved speedup using the model checking toolset ltsmin. We also demonstrate that the parallelization of symbolic model checking for explicit-state modeling languages with an on-the-fly next-state function, as supported by ltsmin, scales well.
Year
DOI
Venue
2015
10.1007/978-3-662-46681-0_60
TACAS
Field
DocType
Citations 
Programming language,Model checking,Cache,Computer science,Binary decision diagram,Modeling language,Exploit,Theoretical computer science,Multi-core processor,Speedup,Hash table
Conference
11
PageRank 
References 
Authors
0.55
22
2
Name
Order
Citations
PageRank
Tom van Dijk1223.47
Jaco van de Pol2135.00