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. 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 Much software today is structured as concurrent programs. This graduate-level text offers a self-contained and in-depth treatment of the subject. Formal methods and assertional reasoning drive the exposition. Not only are derivation and reasoning about concurrent programs discussed, but the assertional approach provides a compelling way to motivate and understand the more traditional concerns in concurrent programming: synchronization and communication mechanisms; protocols to solve key concurrent programming problems. As befits an introductory text, readers are provided with a good account of the basics: propositional and predicate logic, temporal logic, and a Hoare-style logic for sequential programs. Exercises at the end of each chapter extend and illustrate the main themes. The result is a book that should be invaluable to those interested in concurrent programming.
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.
Concurrent computing is gaining popularity as it becomes increasingly feasible to implement distributed computing across networks of workstations. Written by one of the subject's leading figures, this is a comprehensive survey of the subject beginning with prepositional logic and concluding with concurrent programming. The book emphasizes the use of formal methods and assertional reasoning using notation and paradigms drawn from programming. Exercises are included at the end of each chapter, making the book an invaluable approach to the subject.
