A Discipline of Multiprogramming: Programming Theory for Distributed Applications

Front Cover
Springer Science & Business Media, Jun 26, 2001 - Computers - 420 pages
This 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
References
397
Index
410
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information