On a method of multiprogramming / W.H.J. Feijen, A.J.M. van Gasteran.

Format:

Book

Author/Creator:

Feijen, W. H. J.

Contributor:

Gasteran, A.J.M. (Antonetta J. M.), 1952-

Series:

Monographs in computer science

Language:

English

Subjects (All):

Multiprogramming (Electronic computers).

Physical Description:

xx, 370 pages ; 25 cm.

Place of Publication:

New York : Springer, [1999]

Summary:

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.

Contents:

1 On Our Computational Model 1

2 Our Program Notation and Its Semantics 7

2.0 The notation 7

2.1 Hoare-triples and the wlp 9

2.2 Properties of Hoare-triples and the wlp 10

2.3 Definition of the wlp's 11

2.3.0 The skip, the assignment, and the composition 12

2.3.1 The alternative construct 14

2.3.2 The repetitive construct 18

2.4 On our choice of formalism 19

3 The Core of the Owicki/Gries Theory 23

3.0 Annotating a multiprogram 24

3.1 Two examples 28

3.2 Postconditions 32

4 Two Disturbing Divergences 35

5 Bridling the Complexity 41

5.0 Private variables and orthogonality 42

5.1 System Invariants 45

5.2 Mutual Exclusion 50

6 Co-assertions and Strengthening the Annotation 55

7 Three Theorems and Two Examples 61

8 Synchronization and Total Deadlock 75

8.0 Guarded Statements 76

8.1 Progress issues 77

8.2 Some examples 80

8.3 Total Deadlock 82

8.4 More examples 83

9 Individual Progress and the Multibound 89

10 Concurrent Vector Writing 97

11 More Theorems and More Examples 111

12 The Yellow Pages 123

12.0.0 Predicate Calculus 124

12.0.1 Our computational model 125

12.0.2 Annotation 125

12.0.3 The Core of the Owicki/Gries theory 126

12.0.4 Variables 127

12.0.5 Atomicity 127

12.0.6 Progress 128

12.0.7 Rules and Lemmata 129

13 The Safe Sluice 153

14 Peterson's Two-Component Mutual Exclusion Algorithm 163

15 Re-inventing a Great Idea 171

16 On Handshake Protocols 177

17 Phase Synchronization for Two Machines 187

18 The Parallel Linear Search 201

19 The Initialization Protocol 207

20 Co-components 219

21 The Initialization Protocol Revisited 229

22 The Non-Blocking Write Protocol 237

23 Mutual Inclusion and Synchronous Communication 243

24 A Simple Election Algorithm 257

25 Peterson's General Mutual Exclusion Algorithm 265

26 Monitored Phase Synchronization 281

27 Distributed Liberal Phase Synchronization 287

28 Distributed Computation of a Spanning Tree 299

29 Shmuel Safra's Termination Detection Algorithm 313

30 The Alternating Bit Protocol 333

31 Peterson's Mutual Exclusion Algorithm Revisited 347.

Notes:

Includes bibliographical references (pages [361]-366).

ISBN:

038798870X

OCLC:

41165238