Advanced STG decomposition [Elektronische Ressource] / vorgelegt von Mark Schäfer

Informations

• Publié par: universitat_augsburg
• Publié le: 01 janvier 2009
• Nombre de lectures: 14
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Advanced
STG
Decomposition
Dissertation zur Erlangung des Grades eines
Doktors der Naturwissenschaften (Dr. rer. nat)
der Fakult¨at fu¨r Angewandte Informatik
der Universit¨at Augsburg
Vorgelegt von
Mark Sch¨aferGutachter
Erstgutachter: Prof. Dr. Walter Vogler
Zweitgutachter: Prof. Dr. Bernhard M¨oller
Mu¨ndliche Pru¨fung
28. Februar 2008To my wife Maren and my daughter Charlotte
I would like to thank everybody who supported and entertained me
during this four years and all the years before.
Thank you all!
Brina, as ever — Elmar, for explaining objects — Frank, for pizza
Gabriele, for all that libraries — Heinz, for bed and breakfast — Hilli, for smoking
Jan & Thomas, for ma¨a¨a¨a¨a¨a¨h — Jonathan & Victor, for many discussions
Ju¨rgen, for da brainz — Minna, for math — Peter, for the games
Stephan, for the ketchup — Ute, for the fun — Walter, for being sensei
Werner, for showing the way — Willi, for weldingAdvanced STG DecompositionAdvanced
STG
Decomposition
Mark Schaefer
University of AugsburgBibliografische Information der Deutschen Nationalbibliothek
Die Deutsche Nationalbibliothek verzeichnet diese Publikation in der
DeutschenNationalbibliografie; detaillierte bibliografische Datensindim
Internet ub¨ er http://dnb.d-nb.de abrufbar.
?c 2008 Mark Schaefer
[e-mail]
Herstellung und Verlag
Books on Demand GmbH, Norderstedt
ISBN: 978-3-8370-4604-5CONTENTS
Contents
1 Introduction 11
1.1 Scope . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.3 Contribution and Organisation . . . . . . . . . . . . . . . . . . . . . . 13
2 Asynchronous Circuits 15
2.1 Digital Circuits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.1.1 Sequential Circuits . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.1.2 Synchronous Circuits . . . . . . . . . . . . . . . . . . . . . . . . 18
2.2 Asynchronous Circuits . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.2.1 Timing Assumptions . . . . . . . . . . . . . . . . . . . . . . . . 24
2.2.2 Operating Modes . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.2.3 Handshake Circuits. . . . . . . . . . . . . . . . . . . . . . . . . 27
3 Basic Definitions 31
3.1 Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.1.1 Labelled Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . 35
3.1.2 Implicit and Redundant Places . . . . . . . . . . . . . . . . . . 38
3.1.3 Unfoldings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3.2 Signal Transition Graphs . . . . . . . . . . . . . . . . . . . . . . . . . 40
3.2.1 State Graph and Complete State Coding . . . . . . . . . . . . 43
3.2.2 Parallel Composition, Renaming and Hiding . . . . . . . . . . . 47
3.3 Decomposition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
3.3.1 Purpose . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
3.3.2 Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
3.4 Properties of Transition Contractions . . . . . . . . . . . . . . . . . . . 65
3.5 Some Considerations about Consistency . . . . . . . . . . . . . . . . . 70
74 Determinate Decomposition 75
4.1 Redundant Places in Marked Graphs . . . . . . . . . . . . . . . . . . . 76
4.2 Determinacy of Petri Net Operations . . . . . . . . . . . . . . . . . . . 81
4.2.1 Decomposition as Reduction System . . . . . . . . . . . . . . . 81
4.2.2 Reduction is Locally Confluent . . . . . . . . . . . . . . . . . . 83
5 Internal Signals 95
5.1 Extended Correctness Definition . . . . . . . . . . . . . . . . . . . . . 96
5.2 Hierarchical Decomposition . . . . . . . . . . . . . . . . . . . . . . . . 100
5.3 CSC Solving. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
5.4 Comparison with other Approaches . . . . . . . . . . . . . . . . . . . . 114
5.5 Other Implementation Relations . . . . . . . . . . . . . . . . . . . . . 116
5.5.1 Conformance . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117
5.5.2 I/O-Compatibility . . . . . . . . . . . . . . . . . . . . . . . . . 119
5.5.3 Strictness of Inclusions . . . . . . . . . . . . . . . . . . . . . . . 121
6 Advanced Decomposition Strategies 123
6.1 Correctness of New Strategies . . . . . . . . . . . . . . . . . . . . . . . 124
6.2 Reordering Transition Contractions . . . . . . . . . . . . . . . . . . . . 125
6.3 Lazy Backtracking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125
6.4 Tree Decomposition . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130
6.4.1 Component Aggregation . . . . . . . . . . . . . . . . . . . . . . 134
6.5 Undo Stack and Self-Triggering . . . . . . . . . . . . . . . . . . . . . . 135
6.6 CSC-Aware Decomposition . . . . . . . . . . . . . . . . . . . . . . . . 135
6.6.1 CSC-Aware Decomposition . . . . . . . . . . . . . . . . . . . . 137
6.6.2 Safeness-Preserving Contractions . . . . . . . . . . . . . . . . . 141
6.6.3 Implicit Places and Dynamic Auto-Conflicts . . . . . . . . . . . 146
6.7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147
6.7.1 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147
6.7.2 Application to other Decomposition Approaches . . . . . . . . 157
6.7.3 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158
7 Output-Determinacy 161
7.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 163
7.1.1 Output-Determinacy . . . . . . . . . . . . . . . . . . . . . . . . 165
7.2 Decomposition into Output-Determinate Comp. . . . . . . . . . . . . . 169
7.2.1 Valid STG transformations . . . . . . . . . . . . . . . . . . . . 173
7.2.2 New Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . 181
7.3 Output-Determinacy and Internal Signals . . . . . . . . . . . . . . . . 185
7.4 Results. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 188