On a Method of Multiprogramming

1. Front Matter

   Pages i-xx

   PDF

2. On Our Computational Model

   • W. H. J. Feijen, A. J. M. van Gasteren

   Pages 1-5

3. Our Program Notation and Its Semantics

   • W. H. J. Feijen, A. J. M. van Gasteren

   Pages 7-22

4. The Core of the Owicki/Gries Theory

   • W. H. J. Feijen, A. J. M. van Gasteren

   Pages 23-33

5. Two Disturbing Divergences

   • W. H. J. Feijen, A. J. M. van Gasteren

   Pages 35-39

6. Bridling the Complexity

   • W. H. J. Feijen, A. J. M. van Gasteren

   Pages 41-53

7. Co-assertions and Strengthening the Annotation

   • W. H. J. Feijen, A. J. M. van Gasteren

   Pages 55-60

8. Three Theorems and Two Examples

   • W. H. J. Feijen, A. J. M. van Gasteren

   Pages 61-74

9. Synchronization and Total Deadlock

   • W. H. J. Feijen, A. J. M. van Gasteren

   Pages 75-88

10. Individual Progress and the Multibound

    • W. H. J. Feijen, A. J. M. van Gasteren

    Pages 89-96

11. Concurrent Vector Writing: A First Exercise in Program Development

    • W. H. J. Feijen, A. J. M. van Gasteren

    Pages 97-110

12. More Theorems and More Examples

    • W. H. J. Feijen, A. J. M. van Gasteren

    Pages 111-121

13. The Yellow Pages

    • W. H. J. Feijen, A. J. M. van Gasteren

    Pages 123-151

14. The Safe Sluice: A Synthesis Emerging

    • W. H. J. Feijen, A. J. M. van Gasteren

    Pages 153-161

15. Peterson’s Two-Component Mutual Exclusion Algorithm

    • W. H. J. Feijen, A. J. M. van Gasteren

    Pages 163-169

16. Re-inventing a Great Idea

    • W. H. J. Feijen, A. J. M. van Gasteren

    Pages 171-176

17. On Handshake Protocols

    • W. H. J. Feijen, A. J. M. van Gasteren

    Pages 177-186

18. Phase Synchronization for Two Machines

    • W. H. J. Feijen, A. J. M. van Gasteren

    Pages 187-199

19. The Parallel Linear Search

    • W. H. J. Feijen, A. J. M. van Gasteren

    Pages 201-206

20. The Initialization Protocol

    • W. H. J. Feijen, A. J. M. van Gasteren

    Pages 207-217

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.

• Annotation
• algorithm
• algorithms
• complexity
• design
• development
• parallelism
• programming
• semantics

• Department of Computing Science, Eindhoven University of Technology, Eindhoven, The Netherlands

  W. H. J. Feijen, A. J. M. Gasteren

Policies and ethics