Here, one of the leading figures in the field provides a comprehensive survey of the subject, beginning with prepositional logic and concluding with concurrent programming. It is based on graduate courses taught at Cornell University and is designed for use as a graduate text. Professor Schneier emphasises the use of formal methods and assertional reasoning using notation and paradigms drawn from programming to drive the exposition, while exercises at the end of each chapter extend and illustrate the main themes covered. As a result, all those interested in studying concurrent computing will find this an invaluable approach to the subject.
Author(s): Fred B. Schneider
Series: Graduate Texts in Computer Science
Publisher: Springer
Year: 1997
Language: English
Pages: 492
Cover......Page __sk_0000.djvu
Copyright......Page __sk_0002.djvu
Contents......Page __sk_0011.djvu
Preface......Page __sk_0005.djvu
List of Figures......Page __sk_0015.djvu
1.1 Concurrent Programs......Page __sk_0019.djvu
1.3 Understanding Concurrent Programs......Page __sk_0020.djvu
Historical Notes......Page __sk_0023.djvu
Exercises......Page __sk_0024.djvu
2.1 Formal Logical Systems......Page __sk_0027.djvu
2.2 Propositional Logic......Page __sk_0031.djvu
2.3 A Predicate Logic......Page __sk_0041.djvu
2.4 Safety and Liveness Revisited......Page __sk_0060.djvu
Historical Notes......Page __sk_0066.djvu
Exercises......Page __sk_0067.djvu
3.1 Informal Preview......Page __sk_0073.djvu
3.2 Syntax and Meaning of Formulas......Page __sk_0075.djvu
3.3 Axioms and Inference Rules......Page __sk_0078.djvu
3.4 Temporal Logic Applications......Page __sk_0092.djvu
3.5 About Modal Logics......Page __sk_0097.djvu
Historical Notes......Page __sk_0100.djvu
Exercises......Page __sk_0101.djvu
4.1 Notation for Sequential Programs......Page __sk_0109.djvu
4.2 Reasoning About Program States......Page __sk_0113.djvu
4.3 Proof Outline Logic......Page __sk_0117.djvu
4.4 Assignment to Composite Variables......Page __sk_0127.djvu
4.5 A Predicate Transformer......Page __sk_0131.djvu
Historical Notes......Page __sk_0140.djvu
Exercises......Page __sk_0141.djvu
5.1 Specifying Concurrency......Page __sk_0153.djvu
5.2 Control Predicate Axioms......Page __sk_0154.djvu
5.3 Interference Freedom......Page __sk_0155.djvu
5.4 Hiding Control Predicates in Derived Terms......Page __sk_0166.djvu
5.5 Synchronously Altered and Shared Assertions......Page __sk_0170.djvu
5.6 Specifying Synchronization......Page __sk_0173.djvu
5.7 Synchronization and Interference......Page __sk_0176.djvu
Historical Notes......Page __sk_0184.djvu
Exercises......Page __sk_0186.djvu
6.1 Invariance Properties......Page __sk_0193.djvu
6.2 Verifying Invariance Properties......Page __sk_0194.djvu
6.3 Exclusion of Configurations......Page __sk_0198.djvu
6.4 Direct Use of Proof Outlines......Page __sk_0200.djvu
6.5 Developing Programs for Invariance Properties......Page __sk_0202.djvu
Historical Notes......Page __sk_0215.djvu
Exercises......Page __sk_0216.djvu
7.1 Historical Safety Properties......Page __sk_0223.djvu
7.2 Past Extensions to Predicate ogic......Page __sk_0224.djvu
7.3 Verifying Historical Safety Properties......Page __sk_0229.djvu
7.4 Developing Programs for Historical Safety Properties......Page __sk_0231.djvu
7.5 Auxiliary Variables......Page __sk_0236.djvu
Historical Notes......Page __sk_0246.djvu
Exercises......Page __sk_0248.djvu
8.1 S-Temporal Logic Revisited......Page __sk_0257.djvu
8.2 Unless Properties and Derivatives......Page __sk_0265.djvu
8.3 Fairness Assumptions......Page __sk_0267.djvu
8.4 Reasoning from Fairness Assumptions......Page __sk_0275.djvu
8.5 Helpful Actions and Eventualities......Page __sk_0278.djvu
8.6 Liveness for Mutual Exclusion......Page __sk_0287.djvu
Historical Notes......Page __sk_0293.djvu
Exercises......Page __sk_0295.djvu
9.1 Pretending Atomicity......Page __sk_0301.djvu
9.2 Translation-Independent Reasoning......Page __sk_0310.djvu
9.3 Implementing Condition Synchronization......Page __sk_0315.djvu
9.4 Programming with the Subset......Page __sk_0318.djvu
9.5 Synchronization and Interference Revisited......Page __sk_0326.djvu
9.6 Interlock Instructions......Page __sk_0333.djvu
9.7 Example: Barrier Synchronization......Page __sk_0337.djvu
Historical Notes......Page __sk_0344.djvu
Exercises......Page __sk_0345.djvu
10.1 Semaphores......Page __sk_0355.djvu
10.2 Change of Variable to use Semaphores......Page __sk_0360.djvu
10.3 Binary Semaphores and Locks......Page __sk_0364.djvu
10.4 Split Binary Semaphore Method......Page __sk_0367.djvu
10.5 Conditional Critical Regions......Page __sk_0378.djvu
Historical Notes......Page __sk_0385.djvu
Exercises......Page __sk_0388.djvu
11.1 Asynchronous Message-Passing......Page __sk_0395.djvu
11.2 Synchronous Message-Passing......Page __sk_0400.djvu
11.3 Derivation of Distributed Programs......Page __sk_0418.djvu
11.4 Shared-Variable Representations......Page __sk_0423.djvu
Historical Notes......Page __sk_0431.djvu
Exercises......Page __sk_0434.djvu
12.1 On Languages......Page __sk_0445.djvu
12.2 Principles for Verifying Safety and Liveness Properties......Page __sk_0447.djvu
12.3 Proofs Only Increase Confidence......Page __sk_0449.djvu
12.4 A Tool and Applications......Page __sk_0451.djvu
Historical Notes......Page __sk_0452.djvu
References......Page __sk_0453.djvu
Index......Page __sk_0469.djvu
