Elements of Distributed Algorithms: Modeling and Analysis with Petri Nets

Introduction......Page 12
Part A. Elementary System Models......Page 14
1 A First Look at Distributed Algorithms......Page 16
2 Basic Definitions: Nets......Page 25
3 Dynamics......Page 28
4 Interleaved Runs......Page 32
5 Concurrent Runs......Page 33
6 Progress......Page 38
7 Fairness......Page 41
8 Elementary System Nets......Page 42
9 Sequential and Parallel Buffers......Page 46
10 The Dining Philosophers......Page 49
11 An Asynchronous Stack......Page 55
12 Crosstalk Algorithms......Page 56
13 Mutual Exclusion......Page 61
14 Distributed Testing of Message Lines......Page 71
Part B. Advanced System Models......Page 74
15 Introductory Examples......Page 76
16 The Concept of System Nets......Page 84
17 Interleaved and Concurrent Runs......Page 86
18 Structures and Terms......Page 89
19 A Term Representation of System Nets......Page 91
20 Set-Valued Terms......Page 94
21 Transition Guards and System Schemata......Page 99
22 High-Level Extensions of Elementary Net Models......Page 102
23 Distributed Constraint Programming......Page 107
24 Exclusive Writing and Concurrent Reading......Page 111
25 Distributed Rearrangement......Page 113
26 Self Stabilizing Mutual Exclusion......Page 116
27 The Alternating Bit Protocol......Page 118
28 The Balanced Sliding Window Protocol......Page 123
29 Acknowledged Messages to Neighbors in Networks......Page 127
30 Distributed Master/Slave Agreement......Page 130
31 Principles of Network Algorithms......Page 134
32 Leader Election and Spanning Trees......Page 136
33 The Echo Algorithm......Page 138
34 Mutual Exclusion in Networks......Page 141
35 Consensus in Networks......Page 145
36 Phase Synchronization on Undirected Trees......Page 148
37 Distributed Self Stabilization......Page 151
Part C. Analysis of Elementary System Models......Page 154
38 Propositional State Properties......Page 156
39 Net Equations and Net Inequalities......Page 158
40 Place Invariants of es-nets......Page 161
41 Some Small Case Studies......Page 164
42 Traps......Page 167
43 Case Study: Mutex......Page 170
44 Progress on Interleaved Runs......Page 176
45 The Interleaved Pick-up Rule......Page 178
46 Proof Graphs for Interleaved Progress......Page 181
47 Standard Proof Graphs......Page 183
48 How to Pick Up Fairness......Page 187
49 Case Study: Evolution of Mutual Exclusion Algorithms......Page 189
50 Progress on Concurrent Runs......Page 198
51 The Concurrent Pick-up Rule......Page 199
52 Proof Graphs for Concurrent Progress......Page 201
53 Ground Formulas and Rounds......Page 202
54 Rounds of Sequential and Parallel Buffer Algorithms......Page 206
55 Rounds and Ground Formulas of Various Algorithms......Page 208
56 Ground Formulas of Mutex Algorithms......Page 211
Part D. Analysis of Advanced System Models......Page 216
X. State Properties of System Nets......Page 218
57 First-Order State Properties......Page 219
58 Multisets and Linear Functions......Page 220
59 Place Weights, System Equations, and System Inequalities......Page 221
60 Place Invariants of System Nets......Page 225
61 Traps of System Nets......Page 230
62 State Properties of Variants of the Philosopher System......Page 233
63 Progress on Interleaved Runs......Page 238
64 Interleaved Pick-up and Proof Graphs for System Nets......Page 239
65 Case Study: Producer/Consumer Systems......Page 241
66 How to Pick up Fairness......Page 242
67 Progress of Concurrent Runs......Page 244
68 The Concurrent Pick-up Rule......Page 245
69 Pick-up Patterns and Proof Graphs......Page 246
70 Ground Formulas and Rounds......Page 249
71 The Asynchronous Stack......Page 252
72 Exclusive Writing and Concurrent Reading......Page 255
73 Distributed Rearrangement......Page 260
74 Self-Stabilizing Mutual Exclusion......Page 264
75 Master/Slave Agreement......Page 266
76 Leader Election......Page 269
77 The Echo Algorithm......Page 271
78 Global Mutual Exclusion on Undirected Trees......Page 277
79 Local Mutual Exclusion......Page 280
80 Consensus in Networks......Page 290
81 Phase Synchronization on Undirected Trees......Page 296
82 Distributed Self-Stabilization......Page 302
References......Page 310