On Concurrent Programming

by Schneider, Fred B.

• ISBN13: 9780387949420
• ISBN10: 0387949429
• Format: Hardcover
• Copyright: 1997-05-01
• Publisher: Springer-Verlag New York Inc

Summary

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.

Table of Contents

Preface	vii	(10)
List of Figures	xvii
1 Introduction	1	(8)
1.1 Concurrent Programs	1	(1)
1.2 Communication and Synochronization	2	(1)
1.3 Understanding Concurrent Programs	2	(3)
1.4 A Preview	5	(1)
Historical Notes for Chapter 1	5	(1)
Exercises for Chapter 1	6	(3)
2 Formal Logic	9	(46)
2.1 Formal Logical Systems	9	(4)
2.2 Propositional Logic	13	(10)
2.3 A Predicate Logic	23	(19)
2.4 Safety and Liveness Revisited	42	(6)
Historical Notes for Chapter 2	48	(1)
Exercises for Chapter 2	49	(6)
3 Temporal Logic	55	(36)
3.1 Informal Preview	55	(2)
3.2 Syntax and Meaning of Formulas	57	(3)
3.3 Axioms and Inference Rules	60	(14)
3.4 Temporal Logic Applications	74	(5)
3.5 About Modal Logics	79	(3)
Historical Notes for Chapter 3	82	(1)
Exercises for Chapter 3	83	(8)
4 Notation and Logic for Sequential Programming	91	(44)
4.1 Notation for Sequential Programs	91	(4)
4.2 Reasoning About Program States	95	(4)
4.3 Proof Outline Logic	99	(10)
4.4 Assignment to Composite Variables	109	(4)
4.5 A Predicate Transformer	113	(9)
Historical Notes for Chapter 4	122	(1)
Exercises for Chapter 4	123	(12)
5 Concurrency and Interference	135	(40)
5.1 Specifying Concurrency	135	(1)
5.2 Control Predicate Axioms	136	(1)
5.3 Interference Freedom	137	(11)
5.4 Hiding Control Predicates in Derived Terms	148	(4)
5.5 Synchronously Altered and Shared Assertions	152	(3)
5.6 Specifying Synchronization	155	(3)
5.7 Synchronization and Interference	158	(8)
Historical Notes for Chapter 5	166	(2)
Exercises for Chapter 5	168	(7)
6 Safety Properties: Invariance	175	(30)
6.1 Invariance Properties	175	(1)
6.2 Verifying Invariance Properties	176	(4)
6.3 Exclusion of Configurations	180	(2)
6.4 Direct Use of Proof Outlines	182	(2)
6.5 Developing Programs for Invariance Properties	184	(13)
Historical Notes for Chapter 6	197	(1)
Exercises for Chapter 6	198	(7)
7 Safety Properties with Past Terms	205	(34)
7.1 Historical Safety Properties	205	(1)
7.2 Past Extensions to Predicate Logic	206	(5)
7.3 Verifying Historical Safety Properties	211	(2)
7.4 Developing Programs for Historical Safety Properties	213	(5)
7.5 Auxiliary Variables	218	(10)
7.6 Some Cautions	228	(1)
Historical Notes for Chapter 7	228	(2)
Exercises for Chapter 7	230	(9)
8 Verifying Arbitrary Temporal Logic Properties	239	(44)
8.1 S-Temporal Logic Revisited	239	(8)
8.2 Unless Properties and Derivatives	247	(2)
8.3 Fairness Assumptions	249	(8)
8.4 Reasoning from Fairness Assumptions	257	(3)
8.5 Helpful Actions and Eventualities	260	(9)
8.6 Liveness for Mutual Exclusion	269	(6)
Historical Notes for Chapter 8	275	(2)
Exercises for Chapter 8	277	(6)
9 Programming with Fine-Grained Atomic Actions	283	(54)
9.1 Pretending Atomicity	283	(9)
9.2 Translation-Independent Reasoning	292	(5)
9.3 Implementing Condition Synchronization	297	(3)
9.4 Programming with the Subset	300	(8)
9.5 Synchronization and Interference Revisited	308	(7)
9.6 Interlook Instructions	315	(4)
9.7 Example: Barrier Synchronization	319	(7)
Historical Notes for Chapter 9	326	(1)
Exercises for Chapter 9	327	(10)
10 Semaphores, Locks, and Conditional Critical Regions	337	(40)
10.1 Semaphores	337	(5)
10.2 Change of Variables to use Semaphores	342	(4)
10.3 Binary Semaphores and Locks	346	(3)
10.4 Split Binary Semaphore Method	349	(11)
10.5 Conditional Critical Regions	360	(7)
Historical Notes for Chapter 10	367	(3)
Exercises for Chapter 10	370	(7)
11 Message Passing and Distributed Programming	377	(50)
11.1 Asynchronous Message-Passing	377	(5)
11.2 Synchronous Message-Passing	382	(18)
11.3 Derivation of Distributed Programs	400	(5)
11.4 Shared-Variable Representations	405	(8)
Historical Notes for Chapter 11	413	(3)
Exercises for Chapter 11	416	(11)
12 Putting It Together	427	(8)
12.1 On Languages	427	(2)
12.2 Principles for Verifying Safety and Liveness Properties	429	(2)
12.3 Proofs Only Increase Confidence	431	(2)
12.4 A Tool and Applications	433	(1)
Historical Notes for Chapter 12	434	(1)
References	435	(16)
Index	451