Concurrency: State Models & Java Programs

Table of Contents
Back Cover
Concurrency—State Models & Java Programs, 2nd Edition
Preface
	Intended Readership
	Additional Resources
	Second Edition
Chapter 1: Introduction
	1.2 The Modeling Approach
	1.3 Practice
	1.4 Content Overview
	Summary
	Notes and Further Reading
Chapter 2: Processes and Threads
	2.2 Implementing Processes
	Summary
	Notes and Further Reading
	Exercises
Chapter 3: Concurrent Execution
	3.1 Modeling Concurrency
	3.2 Multi-Threaded Programs
	Summary
	Notes and Further Reading
	Exercises
Chapter 4: Shared Objects and Mutual Exclusion
	4.2 Mutual Exclusion in Java
	4.3 Modeling Mutual Exclusion
	Summary
	Notes and Further Reading
	Exercises
Chapter 5: Monitors and Condition Synchronization
	5.2 Semaphores
	5.3 Bounded Buffers
	5.4 Nested Monitors
	5.5 Monitor Invariants
	Summary
	Notes and Further Reading
	Exercises
Chapter 6: Deadlock
	6.1 Deadlock Analysis
	6.2 Dining Philosophers Problem
	Summary
	Notes and Further Reading
	Exercises
Chapter 7: Safety and Liveness Properties
	7.1 Safety
	7.2 Single-Lane Bridge Problem
	7.3 Liveness
	7.4 Liveness of the Single-Lane Bridge
	7.5 Readers–Writers Problem
	Summary
	Notes and Further Reading
	Exercises
Chapter 8: Model-Based Design
	8.1 From Requirements to Models
	8.2 From Models to Implementations
	Summary
	Notes and Further Reading
	Exercises
Chapter 9: Dynamic Systems
	9.1 Golf Club Program
	9.2 Golf Club Model
	9.3 Fair Allocation
	9.4 Revised Golf Ball Allocator
	9.5 Bounded Overtaking
	9.6 Bounded Overtaking Golf Ball Allocator
	9.7 Master–Slave Program
	9.8 Master–Slave Model
	Summary
	Notes and Further Reading
	Exercises
Chapter 10: Message Passing
	10.2 Asynchronous Message Passing
	10.3 Rendezvous
	Summary
	Notes and Further Reading
	Exercises
Chapter 11: Concurrent Architectures
	11.2 Supervisor – Worker
	11.3 Announcer – Listener
	Summary
	Notes and Further Reading
	Exercises
Chapter 12: Timed Systems
	12.1 Modeling Timed Systems
	12.2 Implementing Timed Systems
	12.3 Parcel Router Problem
	12.4 Space Invaders
	Summary
	Notes and Further Reading
	Exercises
Chapter 13: Program Verification
	13.1 Sequential Processes
	13.2 Modeling Condition Synchronization
	13.3 Modeling Variables and Synchronized Methods
	13.4 Bounded Buffer Example
	13.5 Readers – Writers Example
	Summary
	Notes and Further Reading
	Exercises
Chapter 14: Logical Properties
	14.1 Fluent Propositions
	14.2 Temporal Propositions
	14.3 Fluent Linear Temporal Logic (FLTL)
	14.4 Database Ring Problem
	Summary
	Notes and Further Reading
	Exercises
Appendix A: FSP Quick Reference
	A.2 Composite Processes
	A.3 Common Operators
	A.4 Properties
	A.5 Fluent Linear Temporal Logic (FLTL)
Appendix B: FSP Language Specification
	B.1 FSP Description
	B.2 Identifiers
	B.3 Action Labels
	B.4 Const, Range, Set
	B.5 Process Definition
	B.6 Composite Process
	B.7 Parameters
	B.8 Re-Labeling and Hiding
	B.9 Property, Progress and Menu
	B.10 Expression
	B.11 Basic FSP
	B.12 Fluent and Assert
Appendix C: FSP Semantics
	C.2 Processes
	C.3 Composite Processes
	C.4 Common Operators
	C.5 Safety Properties
	C.6 Semantic Equivalences
	C.7 Fluent Linear Temporal Logic (FLTL)
Appendix D: UML Class Diagrams
Bibliography
Index
	B
	C
	D
	E
	F
	G
	H
	I
	J
	K
	L
	M
	N
	O
	P
	R
	S
	T
	U
	V
	W
	Y
List of Figures
List of Tables
List of Programs