## A Discipline of Multiprogramming: Programming Theory for Distributed ApplicationsThis volume presents a programming model, similar to object-oriented programming, that imposes a strict discipline on the form of the constituent objects and interactions among them. Concurrency considerations have been eliminated from the model itself and are introduced only during implementation, thereby freeing programmers from dealing with concurrency explicitly. Moreover, the resulting software designs are typically more modular and easier to analyze than the more traditional ones. Numerous examples illustrate various aspects of the model and reveal that a few simple, integrated features are adequate for designing complex applications. Topics and features: * Presents a simple, easy-to-understand multiprogramming model * Provides extensive development of the underlying theory * Emphasizes program composition, thereby making possible programming of large systems through modular designs * Eliminates explicit concurrency considerations during program design * Supplies efficient implementation schemes for distributed platforms. This book addresses the problem of developing complex distributed applications on wide-area networks, such as the Internet and World Wide Web, by using effective program design principles. Computer scientists, computer engineers, and software engineers will find the book an authoritative guide to large-scale multiprogramming. |

### What people are saying - Write a review

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

### Contents

A Discipline of Multiprogramming | 1 |

Planning a Meeting | 4 |

122 Program development | 5 |

123 Correctness and performance of plan | 6 |

13 Issues in Multiprogram Design | 7 |

132 Structuring through objects not processes | 8 |

133 Implementation for efficient execution | 9 |

134 Transformational and reactive procedures | 10 |

663 The role of the disjunction rule | 192 |

67 Concluding Remarks | 193 |

68 Bibliographic Notes | 194 |

69 Exercises | 195 |

610 Solutions to Exercises | 201 |

Maximality Properties | 215 |

72 Notion of Maximality | 217 |

721 Definition of maximality | 218 |

14 Concluding Remarks | 11 |

15 Bibliographic Notes | 12 |

Action Systems | 13 |

21 An Informal View of Action Systems | 14 |

22 Syntax and Semantics of Action Systems | 15 |

23 Properties of Action Systems | 16 |

232 fixed point | 17 |

24 Examples | 18 |

242 Odometer | 20 |

243 Greatest common divisor | 22 |

244 Merging sorted sequences | 23 |

245 Mutual exclusion | 25 |

246 Shortest path | 31 |

25 Concluding Remarks | 37 |

An ObjectOriented View of Action Systems | 39 |

32 Seuss Syntax | 41 |

322 Procedure | 42 |

323 Procedure body | 43 |

324 Multiple alternatives | 44 |

325 Examples of alternatives Use of positive alternatives | 45 |

326 Constraints on programs | 48 |

331 Tight execution | 49 |

34 Discussion | 51 |

342 Tight vs loose execution | 53 |

344 Partial order on boxes | 54 |

35 Concluding Remarks | 55 |

36 Bibliographic Notes | 56 |

Small Examples | 57 |

41 Channels | 58 |

412 Bounded fifo channel | 59 |

413 Unordered channel | 61 |

414 Task dispatcher | 62 |

415 Disk head scheduler | 63 |

416 Faulty channel | 64 |

42 A Simple Database | 65 |

Lazy Caching | 68 |

44 RealTime Controller DiscreteEvent Simulation | 69 |

441 Discreteevent simulation | 71 |

46 Broadcast | 73 |

47 Barrier Synchronization | 74 |

48 Readers and Writers | 75 |

481 Guaranteed progress for writers | 76 |

483 Starvationfreedom for writers | 77 |

49 Semaphore | 78 |

491 Weak semaphore | 79 |

492 Strong semaphore | 81 |

493 Snoopy semaphore | 83 |

410 Multiple Resource Allocation | 85 |

4101 A deadlockfree solution | 86 |

4102 A starvationfree solution | 87 |

411 Concluding Remarks | 89 |

Safety Properties | 91 |

52 The Meaning of co | 92 |

53 Special Cases of co | 97 |

532 Fixed point | 98 |

54 Derived Rules | 100 |

542 Rules for the special cases | 101 |

543 Substitution axiom | 102 |

544 Elimination theorem | 103 |

545 Distinction between properties and predicates | 104 |

55 Applications | 105 |

552 Common meeting time | 107 |

token ring | 110 |

554 From program texts to properties | 111 |

555 Finite state systems | 114 |

556 Auxiliary variables | 117 |

557 Deadlock | 118 |

558 Axiomatization of a communication network | 120 |

559 Coordinated attack | 122 |

5510 Dynamic graphs | 124 |

5511 A treatment of real time | 126 |

5512 A realtime mutual exclusion algorithm | 129 |

56 Theoretical Results | 134 |

563 Fixed point | 135 |

57 Concluding Remarks | 136 |

58 Bibliographic Notes | 137 |

59 Exercises | 139 |

510 Solutions to Exercises | 143 |

Progress Properties | 155 |

62 Fairness | 156 |

621 Minimal progress | 157 |

623 Strong fairness | 158 |

63 Transient Predicate | 159 |

631 Minimal progress | 160 |

632 Weak fairness | 161 |

633 Strong fairness | 162 |

635 Derived rules | 163 |

636 Discussion | 164 |

642 leadsto | 165 |

643 Examples of specifications with leadsto | 166 |

644 Derived rules | 168 |

645 Proofs of the derived rules | 170 |

646 Corollaries of the derived rules | 174 |

65 Applications | 176 |

652 Common meeting time | 177 |

653 Token ring | 178 |

654 Unordered channel | 180 |

655 Shared counter | 181 |

656 Dynamic graphs | 182 |

657 Treatment of strong fairness | 184 |

66 Theoretical Issues | 188 |

662 A fixpoint characterization of wit | 191 |

73 Proving Maximality | 219 |

732 Proving maximality | 222 |

733 Justification for the proof rules | 223 |

74 Random Assignment | 225 |

75 Fair Unordered Channel | 227 |

751 Maximal solution for fair unordered channel | 228 |

752 The constrained program | 229 |

invariants | 230 |

754 Correctness of implementation of random assignments We have to show | 231 |

755 Proof of chronicle and execution correspondence Proof of chronicle correspondence | 232 |

77 Concluding Remarks | 233 |

Program Composition | 235 |

82 Composition by Union | 237 |

822 Hierarchical program structures | 239 |

823 Union theorem | 240 |

824 Proof of the union theorem and its corollaries | 241 |

825 Locality axiom | 243 |

826 Union theorem for progress | 245 |

83 Examples of Program Union | 246 |

831 Parallel search | 247 |

832 Handshake protocol | 250 |

833 Semaphore | 252 |

834 Vending machine | 259 |

835 Message communication | 263 |

84 Substitution Axiom under Union | 266 |

852 A definition of refinement | 267 |

853 Alternative definition of refinement | 269 |

86 Concluding Remarks | 270 |

87 Bibliographic Notes | 271 |

89 Solutions to Exercises | 274 |

Conditional and Closure Properties | 281 |

92 Conditional Properties | 282 |

922 Linear network | 283 |

producer consumer | 284 |

factorial network | 287 |

concurrent bag | 288 |

93 Closure Properties | 295 |

931 Types of global variables | 296 |

932 Definitions of closure properties | 299 |

934 Derived rules | 302 |

handshake protocol | 304 |

concurrent bag | 306 |

token ring | 309 |

94 Combining Closure and Conditional Properties | 313 |

96 Bibliographic Notes | 314 |

Reduction Theorem | 315 |

102 A Model of Seuss Programs | 317 |

1022 Justification of the model | 318 |

1023 Partial order on boxes | 320 |

1024 Procedures as relations | 322 |

103 Compatibility | 323 |

1031 Examples of compatibility Semaphore | 324 |

1032 Semicommutativity of compatible procedures | 326 |

104 Loose Execution | 328 |

1041 Box condition | 329 |

1042 Execution tree | 330 |

105 Reduction Theorem and Its Proof | 331 |

106 A Variation of the Reduction Theorem | 334 |

107 Concluding Remarks | 335 |

108 Bibliographic Notes | 336 |

Distributed Implementation | 339 |

112 Outline of the Implementation Strategy | 340 |

113 Design of the Scheduler | 341 |

1132 Specification | 342 |

1134 Correctness of the scheduling strategy | 343 |

114 Proof of Maximality of the Scheduler | 345 |

1141 Invariants of the constrained program | 346 |

1142 Correctness of random assignment implementation The random assignment | 348 |

1143 Proof of chronicle and execution correspondence Proof of chronicle correspondence | 349 |

1152 Distributed scheduler | 350 |

116 Designs of the Processors | 351 |

117 Optimizations | 352 |

1171 Data structures for optimization | 353 |

1172 Operation of the scheduler | 354 |

1173 Maintaining the shadow invariant | 355 |

1174 Notes on the optimization scheme | 357 |

118 Concluding Remarks | 359 |

A Logic for Seuss | 361 |

122 Specifications of Simple Procedures | 362 |

1221 readerswriters with progress for writers | 365 |

1222 readerswriters with progress for both | 368 |

123 Specifications of General Procedures | 370 |

1231 Derived rules | 371 |

1232 Simplifications of the derived rules | 372 |

124 Persistence and Relative Stability | 373 |

1242 Relative stability | 374 |

125 Strong Semaphore | 376 |

1252 Proof of the specification | 377 |

126 Starvation Freedom in a Resource Allocation Algorithm | 379 |

1261 The resource allocation program | 380 |

1262 Proof of absence of starvation | 381 |

127 Concluding Remarks | 384 |

128 Bibliographic Notes | 385 |

In Retrospect | 387 |

Elementary Logic and Algebra | 389 |

A2 Predicate Calculus | 391 |

A23 Universal and Existential quantification | 392 |

A3 Proof Format | 393 |

A42 Weakest preconditions | 394 |

397 | |

410 | |

### Other editions - View all

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

A Discipline of Multiprogramming: Programming Theory for Distributed ... Jayadev Misra No preview available - 2012 |

### Common terms and phrases

action systems algorithm assignment binary relation caller channel chapter components computation concurrent programming condition conjunction constrained program corollary critical section deduce defined definition denote dining philosophers problem disjunction elimination theorem endif eventually example F and G false fifo finite fixed point free variable given global variable guarantee holds idle implementation induction inference rules infinitely initially integer invariant leads-to loose execution maximal minimal progress natural number node nonterminal odometer operation partial action partial method partial order partial procedure pre-condition predicate calculus premise processor program text progress properties prove q in F q Proof queue rejected resource safety properties scheduler semaphore program sequence Seuss solution specification ss.p stable strategy strengthen lhs strong semaphore substitution axiom terminal terminal symbol total method total procedure transient transition true union theorem weak fairness weaken rhs wlt.q wltq