Preface |
|
ix | |
PART 1 Semantics of distributed protocols |
|
|
|
3 | (21) |
|
|
3 | (5) |
|
Examples of multi-sorted structures |
|
|
5 | (3) |
|
First-order languages and satisfaction |
|
|
8 | (7) |
|
|
10 | (2) |
|
|
12 | (1) |
|
Substructures and reducts |
|
|
12 | (1) |
|
|
13 | (2) |
|
An example: a mutual exclusion protocol |
|
|
15 | (9) |
|
Proof of the Mutual Exclusion property |
|
|
21 | (3) |
|
|
24 | (24) |
|
Time and interval orderings |
|
|
24 | (6) |
|
|
27 | (3) |
|
Definition of system executions |
|
|
30 | (2) |
|
|
30 | (1) |
|
Parallel composition of systems |
|
|
31 | (1) |
|
Higher and lower-level events |
|
|
32 | (2) |
|
|
34 | (1) |
|
Specification of registers and communication devices |
|
|
34 | (7) |
|
Specifying communication devices |
|
|
37 | (4) |
|
Achilles and the Tortoise |
|
|
41 | (7) |
|
|
44 | (2) |
|
|
46 | (2) |
|
Semantics of concurrent protocols |
|
|
48 | (21) |
|
A protocol language and its flowcharts |
|
|
49 | (8) |
|
Serial and concurrent procedures |
|
|
50 | (2) |
|
|
52 | (3) |
|
|
55 | (2) |
|
|
57 | (2) |
|
Histories and executions of flowcharts |
|
|
57 | (2) |
|
|
59 | (1) |
|
|
59 | (2) |
|
The Pitcher/Catcher example |
|
|
61 | (8) |
|
|
69 | (9) |
|
Mutual exclusion revisited |
|
|
69 | (9) |
|
|
78 | (33) |
|
Pitcher/Catcher revisited |
|
|
79 | (11) |
|
|
90 | (1) |
|
|
91 | (8) |
|
|
95 | (4) |
|
|
99 | (7) |
|
|
101 | (5) |
|
|
106 | (5) |
PART 2 Shared-variable communication |
|
|
On the Producer/Consumer problem: buffers and semaphores |
|
|
111 | (21) |
|
The Producer/Consumer problem |
|
|
111 | (3) |
|
|
114 | (1) |
|
|
115 | (11) |
|
The textbook specification |
|
|
117 | (5) |
|
Abstract specification of semaphores |
|
|
122 | (4) |
|
Load/unload with semaphores |
|
|
126 | (3) |
|
A Multiple Process Mutual Exclusion Protocol |
|
|
129 | (3) |
|
|
132 | (15) |
|
Unbounded sequence numbers |
|
|
132 | (10) |
|
|
136 | (4) |
|
|
140 | (1) |
|
|
141 | (1) |
|
|
142 | (5) |
PART 3 Message communication |
|
|
Specification of channels |
|
|
147 | (17) |
|
|
148 | (4) |
|
|
151 | (1) |
|
|
152 | (2) |
|
|
154 | (4) |
|
A Multiple Producer Protocol |
|
|
158 | (6) |
|
A Sliding window protocol |
|
|
164 | (25) |
|
Protocol analysis and definition and higher-level events |
|
|
170 | (14) |
|
|
177 | (7) |
|
The Sliding Window Axioms hold |
|
|
184 | (3) |
|
Complete Send/Receive/Ack events |
|
|
184 | (3) |
|
Correctness of the protocol |
|
|
187 | (2) |
|
Broadcasting and causal ordering |
|
|
189 | (14) |
|
Send/Receive Network Signature |
|
|
190 | (1) |
|
|
191 | (2) |
|
|
193 | (3) |
|
Causality preservation and deliveries |
|
|
196 | (3) |
|
|
198 | (1) |
|
|
199 | (4) |
|
Uniform delivery in group communication |
|
|
203 | (29) |
|
A generic Uniform Delivery Protocol |
|
|
203 | (10) |
|
The Time-Stamp Vector Axioms are satisfied |
|
|
207 | (2) |
|
|
209 | (3) |
|
|
212 | (1) |
|
Correctness of the generic protocol |
|
|
213 | (2) |
|
The Early Delivery Protocol |
|
|
215 | (6) |
|
|
221 | (11) |
Epilogue: Formal and informal correctness proofs |
|
232 | (2) |
References |
|
234 | (2) |
Index |
|
236 | |