JINC [Elektronische Ressource] : a multi-threaded library for higher-order weighted decision diagram manipulation / vorgelegt von Jörn Ossowski

Sujets

• Informatik

Informations

• Publié par: rheinische_friedrich-wilhelms-universitat_bonn
• Publié le: 01 janvier 2010
• Nombre de lectures: 14
• Langue: English
• Poids de l'ouvrage: 2 Mo

Extrait

JINC { A Multi-Threaded Library for
Higher-Order Weighted Decision Diagram
Manipulation
Dissertation
zur
Erlangung des Doktorgrades (Dr. rer. nat.)
der
Mathematisch-Naturwissenschaftlichen Fakult at
der
Rheinischen Friedrich-Wilhelms-Universit at Bonn
vorgelegt von
J orn Ossowski
aus
Dusseldorf
Bonn 2009Angefertigt mit Genehmigung der Mathematisch-Naturwissenschaftlichen Fakult at
der Rheinischen Friedrich-Wilhelms-Universit at Bonn
Diese Dissertation ist auf dem Hochschulschriftenserver der ULB Bonn
http://hss.ulb.uni-bonn.de/diss_online
elektronisch publiziert.
1. Referent: Prof. Dr. Armin B. Cremers
2.t: Prof. Dr. Wolfgang Kuc hlin
Tag der Promotion: 1.10.2010
Erscheinungsjahr: 2010
iiJINC { A Multi-Threaded Library for Higher-Order
Weighted Decision Diagram Manipulation
J orn Ossowski
Abstract
Ordered Binary Decision Diagrams (OBDDs) have been proven to be an e cient
data structure for symbolic algorithms. The e ciency of the symbolic methods de-
pends on the underlying OBDD library. Available OBDD libraries are based on
the standard concepts and so far only di er in implementation details. This thesis
introduces new techniques to increase run-time and space-e ciency of an OBDD
library.
This thesis introduces the framework of Higher-Order Weighted Decision Diagrams
(HOWDDs) to combine the similarities of di erent OBDD variants. This frame-
work pioneers the basis for the new variant Toggling Algebraic Decision Diagrams
(TADDs) which has been shown to be a space-e cient HOWDD variant for sym-
bolic matrix representation. The concept of HOWDDs has been use to implement
the OBDD library JINC. This thesis also analyzes the usage of multi-threading
techniques to speed-up OBDD manipulations. A new reordering framework ap-
plies the advantages of multi-threading techniques to algorithms. This
approach uses an abstraction layer so that the original reordering algorithms are
not touched. The challenge that arise from a straight forward algorithm is that
the computed-tables and the garbage collection are not as e cient as in a single-
threaded environment. We resolve this problem by developing a new multi-operand
APPLY algorithm that eliminates the creation of temporary nodes which could occur
during computation and thus reduces the need for caching or garbage collection.
The HOWDD framework leads to an e cient library design which has been shown to
be more e cient than the established OBDD library CUDD. The HOWDD instance
TADD reduces the needed number of nodes by factor two compared to ordinary
ADDs. The new multi-threading approaches are more e cient than single-threading
approaches by several factors. In the case of the new reordering framework the speed-
up almost equals the theoretical optimal speed-up. The novel multi-operand APPLY
algorithm reduces the memory usage for the n-queens problem by factor 50 which
enables the calculation of bigger problem instances compared to the traditional
APPLY approach.
The new approaches improve the performance and reduce the memory footprint.
This leads to the conclusion that applications should be reviewed whether they
could bene t from the new multi-threading multi-operand approaches introduced
and discussed in this thesis.
Keywords: OBDD, TADD, HOWDD, multi-threading, reordering framework, multi-
operand APPLY, JINC
iiiDanksagung / Acknowledgements
This thesis has gone a long way. There are many people who helped to make
this work what it is today.
I would like to thank my supervisor Prof. Dr. Cremers for the encouragement to
explore the potential of multi-threading architectures, Prof. Dr. Kuc hlin for his
helpfulness by being the second examiner on short notice, Prof. Dr. Weber for his
endless support and guidance and Prof. Dr. Koepke for his aid.
I owe my special thanks to Daniel Frey for this assistance in all C++ and perfor-
mance related questions and his very helpful review comments. My thanks also go
to Dr. Christoph Vogelbusch, Tobias Blechmann and Dr. Rolf Bardeli for reviewing
this thesis.
Lastly, and most importantly, I would like to express my heart-felt gratitude to my
wife Claudia and my family.
ivThis thesis is dedicated in loving memory to
my father Hartmut Martin Ossowski.
vviContents
Chapter 1 Introduction 1
Chapter 2 Ordered Binary Decision Diagrams 5
2.1. Notations and De nitions . . . . . . . . . . . . . . . . . . . . . . . . 5
2.2. Shared Ordered Binary Decision Diagrams . . . . . . . . . . . . . . . 7
2.2.1. SOBDD with Negative Edges . . . . . . . . . . . . . . . . . . 7
2.2.2. Algebraic Decision Diagrams . . . . . . . . . . . . . . . . . . . 8
2.2.3. Edge-Valued Binary Decision Diagrams . . . . . . . . . . . . . 9
2.2.4. Factored Edge-Valued Binary Decision Diagrams . . . . . . . 10
2.2.4.1. Normalized Algebraic Decision . . . . . . . 10
2.3. Matrix Representation and Operations . . . . . . . . . . . . . . . . . 11
2.3.1. Direct methods . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.3.2. Iterative methods . . . . . . . . . . . . . . . . . . . . . . . . . 12
Chapter 3 Higher-Order Weighted Decision Diagrams 15
3.1. Output Weighted Decision Diagrams . . . . . . . . . . . . . . . . . . 15
3.1.1. De nition and Semantics . . . . . . . . . . . . . . . . . . . . . 15
3.1.2. Reducedness and Canonicity . . . . . . . . . . . . . . . . . . . 18
3.1.3. Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
3.2. Higher-Order Weighted Decision Diagrams . . . . . . . . . . . . . . . 24
3.2.1. De nition and Semantics . . . . . . . . . . . . . . . . . . . . . 24
3.2.2. Reducedness and Canonicity . . . . . . . . . . . . . . . . . . . 27
3.2.3. Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
Chapter 4 JINC { Basic Concept 35
4.1. Basic Concept . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
4.1.1. Data Structures . . . . . . . . . . . . . . . . . . . . . . . . . . 36
4.1.1.1. Nodes . . . . . . . . . . . . . . . . . . . . . . . . . . 36
4.1.1.2. Unique-table . . . . . . . . . . . . . . . . . . . . . . 37
4.1.1.3. Variable Ordering . . . . . . . . . . . . . . . . . . . 39
4.1.2. Algorithms . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
vii4.1.2.1. Computed-table . . . . . . . . . . . . . . . . . . . . 43
4.1.3. Iterators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
4.1.4. Memory Management . . . . . . . . . . . . . . . . . . . . . . . 46
4.1.4.1. Memory Fragmentation . . . . . . . . . . . . . . . . 47
4.1.4.2. Garbage collection . . . . . . . . . . . . . . . . . . . 47
4.1.5. Reordering . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
4.2. Further Details . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
4.2.1. Cube Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
4.2.2. Zero-suppressed Algebraic Decision Diagrams . . . . . . . . . 53
Chapter 5 JINC { Toggling Algebraic Decision Diagrams 57
5.1. De nition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
5.2. Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
5.2.1. FindOrAdd . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
5.2.2. Algorithms and Operators . . . . . . . . . . . . . . . . . . . . 62
5.2.3. Iterators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
5.2.3.1. Swap . . . . . . . . . . . . . . . . . . . . . . . . . . 64
5.3. Benchmarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
Chapter 6 JINC { Multi-Threading 69
6.1. Parallel Computing Concepts . . . . . . . . . . . . . . . . . . . . . . 69
6.1.1. Multi-Threading Challenges . . . . . . . . . . . . . . . . . . . 72
6.1.2. JINC’s Concept . . . . . . . . . . . . . . . . . . . . . . . . . . 74
6.2. Data Structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
6.2.1. Nodes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
6.2.2. Unique-table . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
6.2.3. Memory Pools . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
6.2.4. Computed-table . . . . . . . . . . . . . . . . . . . . . . . . . . 77
6.2.5. Variable Ordering . . . . . . . . . . . . . . . . . . . . . . . . . 77
6.3. Thread-pool . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
6.4. Futures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
6.5. Garbage Collection . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
6.6. Parallel Reordering . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
viii6.7. Generic Multi-Operand APPLY . . . . . . . . . . . . . . . . . . . . . . 87
6.7.1. Expression Templates . . . . . . . . . . . . . . . . . . . . . . . 88
6.7.2. Generic Multi-Operand APPLY algorithm . . . . . . . . . . . . 88
Chapter 7 Case Studies 93
7.1. Single-Threaded JINC . . . . . . . . . . . . . . . . . . . . . . . . . . 93
7.1.1. Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . 93
7.1.1.1. Leader Election Protocol . . . . . . . . . . . . . . . . 94
7.1.1.2. Kanban . . . . . . . . . . . . . . . . . . . . . . . . . 97
7.2. Multi-Threaded JINC . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
7.2.1. Parallel Node Allocation and Garbage Collection . . . . . . . 98
7.2.2. Parallel Reordering .