## On a Method of MultiprogrammingAmong 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 |

361 | |

367 | |

### Other editions - View all

### Common terms and phrases

absence of total Alternating Bit Protocol atomic statements become boolean boolean domain C-fragments calculate chapter co-assertion co-components Comp.p CompF computation proper conclude concurrent conjunct correctness of assertion cs.p derivation End of Remark example execution Exercise false final finite number formal global correctness guaranteed Guard Strengthening guarded skip guarded statement Handshake Protocol Hoare-triple individual progress initial InitX introduce Lemma linear search loop invariant Message Receipt Modus Ponens multibound mutual exclusion algorithm ncs.p node notation number of steps operational Owicki/Gries theory partial correctness Peterson's Peterson's algorithm Phase Synchronization post-assertion postcondition precondition predicate calculus predicate transformer semantics private variables problem program fragment program text proof obligations prove reader Rule Safe Sluice satisfying Section.k sequential programs skip fi solution specification stably true Strengthening the Annotation symmetric system invariant target assertion theorem Topology total deadlock transformation two-component multiprogram Version wlp.S.P

### References to this book

A Discipline of Multiprogramming: Programming Theory for Distributed ... Jayadev Misra Limited preview - 2001 |

Process Algebra for Parallel and Distributed Processing Michael Alexander,William Gardner Limited preview - 2008 |