On a Method of Multiprogramming

Front Cover
Springer Science & Business Media, Jun 11, 1999 - Computers - 370 pages
Among all the interests in parallelism, there is an essential and fundamental one that has remained largely unexplored, namely the question of how to design parallel programs from their specification. And that is what this book is about. It proposes a method for the formal development of parallel programs - multiprograms as we have preferred to call them -, and it does so with a minimum of formal gear, viz. with the predicate calculus and with the meanwhile well-established theory of Owicki and Gries. The fact that one can get away with just this theory will probably not convey anything to the uninitiated, but it may all the more come as a surprise to those who were exposed earlier to correctness of multiprograms. Contrary to common belief, the Owicki/Gries theory can indeed be effectively put to work for the formal development of multiprograms, regardless of whether these algorithms are distributed or not. That is what we intend to exemplify with this book.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

On Our Computational Model
1
Our Program Notation and Its Semantics
7
21 Hoaretriples and the wlp
9
22 Properties of Hoaretriples and the wlp
10
23 Definition of the wlps
11
230 The skip the assignment and the composition
12
231 The alternative construct
14
232 The repetitive construct
18
120 A Summary
124
1201 Our computational model
125
1203 The Core of the OwickiGries theory cf Chapters 3 6
126
1204 Variables
127
1206 Progress cf Chapters 8 9
128
1207 Rules and Lemmata
129
121 Exereises
130
The Safe Sluice A Synthesis Emerging
153

24 On our choice of formalism
19
The Core of the OwickiGries Theory
23
30 Annotating a multiprogram
24
31 Two examples
28
32 Postconditions
32
Two Disturbing Divergences
35
Bridling the Complexity
41
50 Private variables and orthogonality
42
51 System Invariants
45
52 Mutual Exclusion
50
Coassertions and Strengthening the Annotation
55
Three Theorems and Two Examples
61
Synchronization and Total Deadlock
75
80 Guarded Statements
76
81 Progress issues
77
82 Some examples
80
83 Total Deadlock
82
84 More examples
83
Individual Progress and the Multibound
89
Concurrent Vector Writing A First Exercise in Program Development
97
More Theorems and More Examples
111
The Yellow Pages
123
Petersons TwoComponent Mutual Exclusion Algorithm
163
Reinventing a Great Idea
171
On Handshake Protocols
177
Phase Synchronization for Two Machines
187
The Parallel Linear Seareh
201
The Initialization Protocol
207
Cocomponents
219
The Initialization Protocol Revisited
229
The NonBlocking Write Protocol
237
Mutual Inclusion and Synchronous Communication
243
A Simple Election Algorithm
257
Petersons General Mutual Exclusion Algorithm
265
Monitored Phase Synchronization
281
Distributed Liberal Phase Synchronization
287
Distributed Computation of a Spanning Tree
299
Shmuel Safras Termination Detection Algorithm
313
The Alternating Bit Protocol
333
Petersons Mutual Exclusion Algorithm Revisited
347
Epilogue
357
References
361
Index
367
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information