On Concurrent ProgrammingSpringer 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. |
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 |
435 | |
451 | |
Citi izdevumi - Skatīt visu
Bieži izmantoti vārdi un frāzes
after(door after(S anchored sequence assignment statement at(S at(T₁ atomic statement auxiliary variable axiomatization B₁ blocked channel action cobegin coend concurrent program Condition Synchronization conditional atomic action conditional critical conjunct control point critical regions critical section defe defined derived term entry Etern example execution exit fairness assumption false falsify GEval guard evaluation action Helpful Actions holds Hs-valid implementation implies in(CS in(S inference rules Init interference freedom invariance property Ipo(s Lamport liveness property modal logic Modus Ponens operational semantics operations outline of Figure postcondition precondition Predicate Logic premise primitive assertion program of Figure Proof Outline Logic Propositional Logic protocol prove receive statements replaced rigid variable S-Temporal S₁ S₂ safety property satisfies skip split binary semaphore synchronous message-passing T₁ Temporal Logic formula terminates Textual Substitution theorem of Proof tion true truthifies valid proof outline Virtual Circuit well-founded set
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.
Atsauces uz šo grāmatu
Logics for Databases and Information Systems Jan Chomicki,Gunter Saake Ierobežota priekšskatīšana - 1998 |