Concurrency: State Models and Java Programs

Concurrency: State Models and Java Programs

by Jeff Magee, Jeff Kramer
Released July 2006
Publisher(s): Wiley
ISBN: 9780470093559

Read it now on the O’Reilly learning platform with a 10-day free trial.

O’Reilly members get unlimited access to books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.

Start your free trial

Book description

Concurrency provides a thoroughly updated approach to the basic concepts and techniques behind concurrent programming. Concurrent programming is complex and demands a much more formal approach than sequential programming. In order to develop a thorough understanding of the topic Magee and Kramer present concepts, techniques and problems through a variety of forms: informal descriptions, illustrative examples, abstract models and concrete Java examples. These combine to provide problem patterns and associated solution techniques which enable students to recognise problems and arrive at solutions.

New features include:

  • New chapters covering program verification and logical properties.

  • More student exercises.

  • Supporting website contains an updated version of the LTSA tool for modelling concurrency, model animation, and model checking.

  • Website also includes the full set of state models, java examples, and demonstration programs and a comprehensive set of overhead slides for course presentation.

Table of contents

  1. Copyright
  2. Preface
    1. What Can Readers Expect from this Book?
    2. Intended Readership
    3. Additional Resources
    4. Second Edition
  3. Acknowledgments
  4. 1. Introduction
    1. 1.1. Concurrent Programs
    2. 1.2. The Modeling Approach
    3. 1.3. Practice
    4. 1.4. Content Overview
    5. 1.5. Summary
    6. 1.6. Notes and Further Reading
  5. 2. Processes and Threads
    1. 2.1. Modeling Processes
      1. 2.1.1. Action Prefix
      2. 2.1.2. Choice
        1. 2.1.2.1. Non-Deterministic Choice
      3. 2.1.3. Indexed Processes and Actions
      4. 2.1.4. Process Parameters
      5. 2.1.5. Guarded Actions
      6. 2.1.6. Process Alphabets
    2. 2.2. Implementing Processes
      1. 2.2.1. Operating System Processes
      2. 2.2.2. Threads in Java
      3. 2.2.3. Thread Life Cycle
      4. 2.2.4. Countdown Timer Example
    3. 2.3. Summary
    4. 2.4. Notes and Further Reading
    5. 2.5. Exercises
  6. 3. Concurrent Execution
    1. 3.1. Modeling Concurrency
      1. 3.1.1. Parallel Composition
      2. 3.1.2. Shared Actions
      3. 3.1.3. Process Labeling
      4. 3.1.4. Relabeling
      5. 3.1.5. Hiding
      6. 3.1.6. Structure Diagrams
    2. 3.2. Multi-Threaded Programs
      1. 3.2.1. ThreadDemo Example – Model
      2. 3.2.2. ThreadDemo Example – Implementation
    3. 3.3. Summary
    4. 3.4. Notes and Further Reading
    5. 3.5. Exercises
  7. 4. Shared Objects and Mutual Exclusion
    1. 4.1. Interference
      1. 4.1.1. Ornamental Garden Problem
      2. 4.1.2. Ornamental Garden Model
    2. 4.2. Mutual Exclusion in Java
    3. 4.3. Modeling Mutual Exclusion
    4. 4.4. Summary
    5. 4.5. Notes and Further Reading
    6. 4.6. Exercises
  8. 5. Monitors and Condition Synchronization
    1. 5.1. Condition Synchronization
      1. 5.1.1. Car Park Model
      2. 5.1.2. Car Park Program
      3. 5.1.3. Condition Synchronization in Java
    2. 5.2. Semaphores
      1. 5.2.1. Modeling Semaphores
      2. 5.2.2. Semaphores in Java
    3. 5.3. Bounded Buffers
      1. 5.3.1. Bounded Buffer Model
      2. 5.3.2. Bounded Buffer Program
    4. 5.4. Nested Monitors
    5. 5.5. Monitor Invariants
    6. 5.6. Summary
    7. 5.7. Notes and Further Reading
    8. 5.8. Exercises
  9. 6. Deadlock
    1. 6.1. Deadlock Analysis
    2. 6.2. Dining Philosophers Problem
      1. 6.2.1. Dining Philosophers Implementation
      2. 6.2.2. Deadlock-Free Philosophers
    3. 6.3. Summary
    4. 6.4. Notes and Further Reading
    5. 6.5. Exercises
  10. 7. Safety and Liveness Properties
    1. 7.1. Safety
      1. 7.1.1. Safety Properties
      2. 7.1.2. Safety Property for Mutual Exclusion
    2. 7.2. Single-Lane Bridge Problem
      1. 7.2.1. Single-Lane Bridge Model
      2. 7.2.2. Single-Lane Bridge Implementation
    3. 7.3. Liveness
      1. 7.3.1. Progress Properties
      2. 7.3.2. Progress Analysis
      3. 7.3.3. Action Priority
        1. 7.3.3.1. High Priority Operator ("≪")
        2. 7.3.3.2. Low Priority Operator ("≫")
    4. 7.4. Liveness of the Single-Lane Bridge
      1. 7.4.1. Revised Single-Lane Bridge Model
      2. 7.4.2. Revised Single-Lane Bridge Implementation
    5. 7.5. Readers–Writers Problem
      1. 7.5.1. Readers–Writers Model
        1. 7.5.1.1. Safety Property
        2. 7.5.1.2. Progress Property
      2. 7.5.2. Readers–Writers Implementation
      3. 7.5.3. Revised Readers–Writers Model and Implementation
    6. 7.6. Summary
    7. 7.7. Notes and Further Reading
    8. 7.8. Exercises
  11. 8. Model-Based Design
    1. 8.1. From Requirements to Models
      1. 8.1.1. A Cruise Control System
      2. 8.1.2. Structure of the Model
      3. 8.1.3. Model Elaboration
      4. 8.1.4. Safety Properties
      5. 8.1.5. Revising the Model
      6. 8.1.6. Progress Properties
    2. 8.2. From Models to Implementations
    3. 8.3. Summary
    4. 8.4. Notes and Further Reading
    5. 8.5. Exercises
  12. 9. Dynamic Systems
    1. 9.1. Golf Club Program
    2. 9.2. Golf Club Model
    3. 9.3. Fair Allocation
    4. 9.4. Revised Golf Ball Allocator
    5. 9.5. Bounded Overtaking
    6. 9.6. Bounded Overtaking Golf Ball Allocator
    7. 9.7. Master–Slave Program
    8. 9.8. Master–Slave Model
    9. 9.9. Summary
    10. 9.10. Notes and Further Reading
    11. 9.11. Exercises
  13. 10. Message Passing
    1. 10.1. Synchronous Message Passing
      1. 10.1.1. Selective Receive
      2. 10.1.2. Synchronous Message Passing in Java
      3. 10.1.3. Modeling Synchronous Message Passing
      4. 10.1.4. Modeling and Implementing Selective Receive
    2. 10.2. Asynchronous Message Passing
      1. 10.2.1. Asynchronous Message Passing in Java
      2. 10.2.2. Modeling Asynchronous Message Passing
    3. 10.3. Rendezvous
      1. 10.3.1. Rendezvous in Java
      2. 10.3.2. Modeling Rendezvous
      3. 10.3.3. Rendezvous and Monitor Method Invocation
    4. 10.4. Summary
    5. 10.5. Notes and Further Reading
    6. 10.6. Exercises
  14. 11. Concurrent Architectures
    1. 11.1. Filter Pipeline
      1. 11.1.1. Primes Sieve Model
        1. 11.1.1.1. Unbuffered Pipes
        2. 11.1.1.2. Abstracting from Application Detail
        3. 11.1.1.3. Architectural Property Analysis
      2. 11.1.2. Primes Sieve Implementation
        1. 11.1.2.1. Why Use Buffering?
    2. 11.2. Supervisor–Worker
      1. 11.2.1. Linda Tuple Space
        1. 11.2.1.1. Tuple Space Model
        2. 11.2.1.2. Tuple Space Implementation
      2. 11.2.2. Supervisor–Worker Model
        1. 11.2.2.1. Analysis
      3. 11.2.3. Supervisor–Worker Implementation
        1. 11.2.3.1. Speedup and Efficiency
    3. 11.3. Announcer–Listener
      1. 11.3.1. Announcer–Listener Model
        1. 11.3.1.1. Analysis
      2. 11.3.2. Announcer – Listener Implementation
    4. 11.4. Summary
    5. 11.5. Notes and Further Reading
    6. 11.6. Exercises
  15. 12. Timed Systems
    1. 12.1. Modeling Timed Systems
      1. 12.1.1. Timing Consistency
      2. 12.1.2. Maximal Progress
      3. 12.1.3. Modeling Techniques
        1. 12.1.3.1. Output in an Interval
        2. 12.1.3.2. Jitter
        3. 12.1.3.3. Timeout
    2. 12.2. Implementing Timed Systems
      1. 12.2.1. Timed Objects
        1. 12.2.1.1. CountDown Timer
        2. 12.2.1.2. Timed Producer–Consumer
        3. 12.2.1.3. The Two-Phase Clock
      2. 12.2.2. Time Manager
    3. 12.3. Parcel Router Problem
      1. 12.3.1. Parcel Router Model
        1. 12.3.1.1. GEN
        2. 12.3.1.2. BIN
        3. 12.3.1.3. STAGE
        4. 12.3.1.4. CHUTE
        5. 12.3.1.5. SENSORCONTROLLER
        6. 12.3.1.6. SWITCH
        7. 12.3.1.7. Analysis
      2. 12.3.2. Parcel Router Implementation
    4. 12.4. Space Invaders
      1. 12.4.1. Space Invaders Model
        1. 12.4.1.1. Sprite
        2. 12.4.1.2. Alien
        3. 12.4.1.3. Missile
        4. 12.4.1.4. Spaceship
        5. 12.4.1.5. Collision Detection
        6. 12.4.1.6. Space Invaders
        7. 12.4.1.7. Analysis
      2. 12.4.2. Space Invaders Implementation
        1. 12.4.2.1. Sprite and SpriteCanvas
        2. 12.4.2.2. CollisionDetector
        3. 12.4.2.3. SpaceInvaders
    5. 12.5. Summary
    6. 12.6. Notes and Further Reading
    7. 12.7. Exercises
  16. 13. Program Verification
    1. 13.1. Sequential Processes
      1. 13.1.1. Local Process END
      2. 13.1.2. Sequential Composition;
      3. 13.1.3. Parallel Composition and Sequential Processes
      4. 13.1.4. Sequential Processes and Analysis
    2. 13.2. Modeling Condition Synchronization
      1. 13.2.1. Wait, Notify and NotifyAll
    3. 13.3. Modeling Variables and Synchronized Methods
      1. 13.3.1. Variables
      2. 13.3.2. Monitor Exit and Entry
      3. 13.3.3. Synchronized Methods
    4. 13.4. Bounded Buffer Example
      1. 13.4.1. put() and get() Methods
      2. 13.4.2. Producer and Consumer Threads
      3. 13.4.3. Analysis
    5. 13.5. Readers–Writers Example
      1. 13.5.1. ReadWritePriority Methods
        1. 13.5.1.1. READER and WRITER Processes
      2. 13.5.2. Analysis
        1. 13.5.2.1. Progress Analysis
    6. 13.6. Summary
    7. 13.7. Notes and Further Reading
    8. 13.8. Exercises
  17. 14. Logical Properties
    1. 14.1. Fluent Propositions
      1. 14.1.1. Fluents
        1. 14.1.1.1. Action Fluents
      2. 14.1.2. Fluent Expressions
    2. 14.2. Temporal Propositions
      1. 14.2.1. Safety Properties
        1. 14.2.1.1. Single-Lane Bridge Safety Property
      2. 14.2.2. Liveness Properties
        1. 14.2.2.1. Response Properties
    3. 14.3. Fluent Linear Temporal Logic (FLTL)
      1. 14.3.1. Until
      2. 14.3.2. Weak Until
        1. 14.3.2.1. Definitions
      3. 14.3.3. Next Time
    4. 14.4. Database Ring Problem
      1. 14.4.1. Database Ring Model
      2. 14.4.2. Database Ring Properties
        1. 14.4.2.1. Witness Executions
        2. 14.4.2.2. Finite Executions
    5. 14.5. Summary
    6. 14.6. Notes and Further Reading
    7. 14.7. Exercises
  18. A. FSP Quick Reference
    1. A.1. Processes
      1. A.1.1. Example
    2. A.2. Composite Processes
      1. A.2.1. Example
    3. A.3. Common Operators
    4. A.4. Properties
    5. A.5. Fluent Linear Temporal Logic (FLTL)
  19. B. FSP Language Specification
    1. B.1. FSP Description
    2. B.2. Identifiers
    3. B.3. Action Labels
      1. B.3.1. Examples
      2. B.3.2. Examples
      3. B.3.3. Examples
    4. B.4. const, range, set
      1. B.4.1. Examples
    5. B.5. Process Definition
      1. B.5.1. Examples
      2. B.5.2. Example
      3. B.5.3. Examples
    6. B.6. Composite Process
      1. B.6.1. Examples
      2. B.6.2. Example
    7. B.7. Parameters
      1. B.7.1. Example
    8. B.8. Re-Labeling and Hiding
      1. B.8.1. Examples
      2. B.8.2. Prefix Matching
    9. B.9. property, progress and menu
      1. B.9.1. Example
    10. B.10. Expression
    11. B.11. Basic FSP
    12. B.12. fluent and assert
      1. B.12.1. Example
  20. C. FSP Semantics
    1. C.1. Labeled Transition System (LTS)
    2. C.2. Processes
    3. C.3. Composite Processes
      1. C.3.1. LTS Composition
      2. C.3.2. LTS Priority
      3. C.3.3. FSP Composition and Priority
    4. C.4. Common Operators
      1. C.4.1. Re-Labeling
      2. C.4.2. Hiding
      3. C.4.3. FSP Re-Labeling, Hiding and Interface
    5. C.5. Safety Properties
    6. C.6. Semantic Equivalences
      1. C.6.1. Strong Equivalence
      2. C.6.2. Weak Equivalence
    7. C.7. Fluent Linear Temporal Logic (FLTL)
      1. C.7.1. Linear Temporal Logic
      2. C.7.2. Fluents
  21. D. UML Class Diagrams
  22. Bibliography

Product information

  • Title: Concurrency: State Models and Java Programs
  • Author(s): Jeff Magee, Jeff Kramer
  • Release date: July 2006
  • Publisher(s): Wiley
  • ISBN: 9780470093559