On Concurrent Programming

Pirmais vāks
Springer Science & Business Media, 1997. gada 6. maijs - 473 lappuses
Concurrent computing is gaining ground in interest as it becomes increasingly feasible to implement distributed computing across networks of workstations. This book, by one of the subject's leading figures, provides a comprehensive survey of the subject beginning with proposotional logic and concluding with concurrent programming. It is based on graduate courses taught at Cornell University and is designed to be used as a graduate text. There are exercises at the end of each chapter to extend and illustrate the main themes covered. Professor Schneier emphasizes the use of formal methods and assertional reasoning using notation and paradigms drawn from programming to drive the exposition. As a result, all those interested in studying concurrent computing will find this to be an invaluable approach to the subject.
 

Atlasītās lappuses

Saturs

Chapter 1 Introduction
1
12 Communication and Synchronization
2
14 A Preview
5
Exercises
6
Formal Logic
9
22 Propositional Logic
13
23 A Predicate Logic
23
24 Safety and Liveness Revisited
42
74 Developing Programs for Historical Safety Properties
213
75 Auxiliary Variables
218
76 Some Cautions
228
Exercises
230
Verifying Arbitrary Temporal Logic Properties
239
82 Unless Properties and Derivatives
247
83 Fairness Assumptions
249
84 Reasoning from Fairness Assumptions
257

Historical Notes
48
Exercises
49
Temporal Logic
55
32 Syntax and Meaning of Formulas
57
33 Axioms and Inference Rules
60
34 Temporal Logic Applications
74
35 About Modal Logics
79
Historical Notes
82
Exercises
83
Notation and Logic for Sequential Programming
91
42 Reasoning About Program States
95
43 Proof Outline Logic
99
44 Assignment to Composite Variables
109
45 A Predicate Transformer
113
Historical Notes
122
Exercises
123
Concurrency and Interference
135
52 Control Predicate Axioms
136
53 Interference Freedom
137
54 Hiding Control Predicates in Derived Terms
148
55 Synchronously Altered and Shared Assertions
152
56 Specifying Synchronization
155
57 Synchronization and Interference
158
Historical Notes
166
Exercises
168
Safety Properties Invariance
175
62 Verifying Invariance Properties
176
63 Exclusion of Configurations
180
64 Direct Use of Proof Outlines
182
65 Developing Programs for Invariance Properties
184
Historical Notes
197
Exercises
198
Safety Properties with Past Terms
205
72 Past Extensions to Predicate Logic
206
73 Verifying Historical Safety Properties
211
85 Helpful Actions and Eventualities
260
86 Liveness for Mutual Exclusion
269
Historical Notes
275
Exercises
277
Programming with FineGrained Atomic Actions
283
92 TranslationIndependent Reasoning
292
93 Implementing Condition Synchronization
297
94 Programming with the Subset
300
95 Synchronization and Interference Revisited
308
96 Interlock Instructions
315
Barrier Synchronization
319
Historical Notes
326
Exercises
327
Semaphores Locks and Conditional Critical Regions
337
102 Change of Variable to use Semaphores
342
103 Binary Semaphores and Locks
346
104 Split Binary Semaphore Method
349
105 Conditional Critical Regions
360
Historical Notes
367
Exercises
370
Message Passing and Distributed Programming
377
112 Synchronous MessagePassing
382
113 Derivation of Distributed Programs
400
114 SharedVariable Representations
405
Historical Notes
413
Exercises
416
Putting It Together
427
122 Principles for Verifying Safety and Liveness Properties
429
123 Proofs Only Increase Confidence
431
124 A Tool and Applications
433
Historical Notes
434
References
435
Index
451
Autortiesības

Citi izdevumi - Skatīt visu

Bieži izmantoti vārdi un frāzes

Populāri fragmenti

436. lappuse - KR Apt and E.-R. Olderog, Verification of Sequential and Concurrent Programs, Springer- Verlag, New York, 1991.
436. lappuse - Letters 18 (1984) 215-220 [BNl] LBoasson. M.Nivat Adherences of languages JCSS 20 (1980) 285309 [Bui] JRBuchi On a decision method in restricted second order arithmetic Logic. Methodology and Philosophy of Science; Proc.

Bibliogrāfiskā informācija