book

Concurrency: State Models and Java Programs

Name: Concurrency: State Models and Java Programs
ISBN: 9780470093559

by Jeff Magee, Jeff Kramer

July 2006

Intermediate to advanced

434 pages

9h 24m

English

Wiley

Read now

Unlock full access

Copyright
Preface
What Can Readers Expect from this Book?Intended ReadershipAdditional ResourcesSecond Edition
Acknowledgments
1. Introduction
1.1. Concurrent Programs1.2. The Modeling Approach1.3. Practice1.4. Content Overview1.5. Summary1.6. Notes and Further Reading
2. Processes and Threads
2.1. Modeling Processes2.1.1. Action Prefix2.1.2. Choice2.1.2.1. Non-Deterministic Choice2.1.3. Indexed Processes and Actions2.1.4. Process Parameters2.1.5. Guarded Actions2.1.6. Process Alphabets2.2. Implementing Processes2.2.1. Operating System Processes2.2.2. Threads in Java2.2.3. Thread Life Cycle2.2.4. Countdown Timer Example2.3. Summary2.4. Notes and Further Reading2.5. Exercises
3. Concurrent Execution
3.1. Modeling Concurrency3.1.1. Parallel Composition3.1.2. Shared Actions3.1.3. Process Labeling3.1.4. Relabeling3.1.5. Hiding3.1.6. Structure Diagrams3.2. Multi-Threaded Programs3.2.1. ThreadDemo Example – Model3.2.2. ThreadDemo Example – Implementation3.3. Summary3.4. Notes and Further Reading3.5. Exercises
4. Shared Objects and Mutual Exclusion
4.1. Interference4.1.1. Ornamental Garden Problem4.1.2. Ornamental Garden Model4.2. Mutual Exclusion in Java4.3. Modeling Mutual Exclusion4.4. Summary4.5. Notes and Further Reading4.6. Exercises
5. Monitors and Condition Synchronization
5.1. Condition Synchronization5.1.1. Car Park Model5.1.2. Car Park Program5.1.3. Condition Synchronization in Java5.2. Semaphores5.2.1. Modeling Semaphores5.2.2. Semaphores in Java5.3. Bounded Buffers5.3.1. Bounded Buffer Model5.3.2. Bounded Buffer Program5.4. Nested Monitors5.5. Monitor Invariants5.6. Summary5.7. Notes and Further Reading5.8. Exercises
6. Deadlock
6.1. Deadlock Analysis6.2. Dining Philosophers Problem6.2.1. Dining Philosophers Implementation6.2.2. Deadlock-Free Philosophers6.3. Summary6.4. Notes and Further Reading6.5. Exercises
7. Safety and Liveness Properties
7.1. Safety7.1.1. Safety Properties7.1.2. Safety Property for Mutual Exclusion7.2. Single-Lane Bridge Problem7.2.1. Single-Lane Bridge Model7.2.2. Single-Lane Bridge Implementation7.3. Liveness7.3.1. Progress Properties7.3.2. Progress Analysis7.3.3. Action Priority7.3.3.1. High Priority Operator ("≪")7.3.3.2. Low Priority Operator ("≫")7.4. Liveness of the Single-Lane Bridge7.4.1. Revised Single-Lane Bridge Model7.4.2. Revised Single-Lane Bridge Implementation7.5. Readers–Writers Problem7.5.1. Readers–Writers Model7.5.1.1. Safety Property7.5.1.2. Progress Property7.5.2. Readers–Writers Implementation7.5.3. Revised Readers–Writers Model and Implementation7.6. Summary7.7. Notes and Further Reading7.8. Exercises

8. Model-Based Design
8.1. From Requirements to Models8.1.1. A Cruise Control System8.1.2. Structure of the Model8.1.3. Model Elaboration8.1.4. Safety Properties8.1.5. Revising the Model8.1.6. Progress Properties8.2. From Models to Implementations8.3. Summary8.4. Notes and Further Reading8.5. Exercises
9. Dynamic Systems
9.1. Golf Club Program9.2. Golf Club Model9.3. Fair Allocation9.4. Revised Golf Ball Allocator9.5. Bounded Overtaking9.6. Bounded Overtaking Golf Ball Allocator9.7. Master–Slave Program9.8. Master–Slave Model9.9. Summary9.10. Notes and Further Reading9.11. Exercises
10. Message Passing
10.1. Synchronous Message Passing10.1.1. Selective Receive10.1.2. Synchronous Message Passing in Java10.1.3. Modeling Synchronous Message Passing10.1.4. Modeling and Implementing Selective Receive10.2. Asynchronous Message Passing10.2.1. Asynchronous Message Passing in Java10.2.2. Modeling Asynchronous Message Passing10.3. Rendezvous10.3.1. Rendezvous in Java10.3.2. Modeling Rendezvous10.3.3. Rendezvous and Monitor Method Invocation10.4. Summary10.5. Notes and Further Reading10.6. Exercises
11. Concurrent Architectures
11.1. Filter Pipeline11.1.1. Primes Sieve Model11.1.1.1. Unbuffered Pipes11.1.1.2. Abstracting from Application Detail11.1.1.3. Architectural Property Analysis11.1.2. Primes Sieve Implementation11.1.2.1. Why Use Buffering?11.2. Supervisor–Worker11.2.1. Linda Tuple Space11.2.1.1. Tuple Space Model11.2.1.2. Tuple Space Implementation11.2.2. Supervisor–Worker Model11.2.2.1. Analysis11.2.3. Supervisor–Worker Implementation11.2.3.1. Speedup and Efficiency11.3. Announcer–Listener11.3.1. Announcer–Listener Model11.3.1.1. Analysis11.3.2. Announcer – Listener Implementation11.4. Summary11.5. Notes and Further Reading11.6. Exercises
12. Timed Systems
12.1. Modeling Timed Systems12.1.1. Timing Consistency12.1.2. Maximal Progress12.1.3. Modeling Techniques12.1.3.1. Output in an Interval12.1.3.2. Jitter12.1.3.3. Timeout12.2. Implementing Timed Systems12.2.1. Timed Objects12.2.1.1. CountDown Timer12.2.1.2. Timed Producer–Consumer12.2.1.3. The Two-Phase Clock12.2.2. Time Manager12.3. Parcel Router Problem12.3.1. Parcel Router Model12.3.1.1. GEN12.3.1.2. BIN12.3.1.3. STAGE12.3.1.4. CHUTE12.3.1.5. SENSORCONTROLLER12.3.1.6. SWITCH12.3.1.7. Analysis12.3.2. Parcel Router Implementation12.4. Space Invaders12.4.1. Space Invaders Model12.4.1.1. Sprite12.4.1.2. Alien12.4.1.3. Missile12.4.1.4. Spaceship12.4.1.5. Collision Detection12.4.1.6. Space Invaders12.4.1.7. Analysis12.4.2. Space Invaders Implementation12.4.2.1. Sprite and SpriteCanvas12.4.2.2. CollisionDetector12.4.2.3. SpaceInvaders12.5. Summary12.6. Notes and Further Reading12.7. Exercises
13. Program Verification
13.1. Sequential Processes13.1.1. Local Process END13.1.2. Sequential Composition;13.1.3. Parallel Composition and Sequential Processes13.1.4. Sequential Processes and Analysis13.2. Modeling Condition Synchronization13.2.1. Wait, Notify and NotifyAll13.3. Modeling Variables and Synchronized Methods13.3.1. Variables13.3.2. Monitor Exit and Entry13.3.3. Synchronized Methods13.4. Bounded Buffer Example13.4.1. put() and get() Methods13.4.2. Producer and Consumer Threads13.4.3. Analysis13.5. Readers–Writers Example13.5.1. ReadWritePriority Methods13.5.1.1. READER and WRITER Processes13.5.2. Analysis13.5.2.1. Progress Analysis13.6. Summary13.7. Notes and Further Reading13.8. Exercises
14. Logical Properties
14.1. Fluent Propositions14.1.1. Fluents14.1.1.1. Action Fluents14.1.2. Fluent Expressions14.2. Temporal Propositions14.2.1. Safety Properties14.2.1.1. Single-Lane Bridge Safety Property14.2.2. Liveness Properties14.2.2.1. Response Properties14.3. Fluent Linear Temporal Logic (FLTL)14.3.1. Until14.3.2. Weak Until14.3.2.1. Definitions14.3.3. Next Time14.4. Database Ring Problem14.4.1. Database Ring Model14.4.2. Database Ring Properties14.4.2.1. Witness Executions14.4.2.2. Finite Executions14.5. Summary14.6. Notes and Further Reading14.7. Exercises
A. FSP Quick Reference
A.1. ProcessesA.1.1. ExampleA.2. Composite ProcessesA.2.1. ExampleA.3. Common OperatorsA.4. PropertiesA.5. Fluent Linear Temporal Logic (FLTL)
B. FSP Language Specification
B.1. FSP DescriptionB.2. IdentifiersB.3. Action LabelsB.3.1. ExamplesB.3.2. ExamplesB.3.3. ExamplesB.4. const, range, setB.4.1. ExamplesB.5. Process DefinitionB.5.1. ExamplesB.5.2. ExampleB.5.3. ExamplesB.6. Composite ProcessB.6.1. ExamplesB.6.2. ExampleB.7. ParametersB.7.1. ExampleB.8. Re-Labeling and HidingB.8.1. ExamplesB.8.2. Prefix MatchingB.9. property, progress and menuB.9.1. ExampleB.10. ExpressionB.11. Basic FSPB.12. fluent and assertB.12.1. Example
C. FSP Semantics
C.1. Labeled Transition System (LTS)C.2. ProcessesC.3. Composite ProcessesC.3.1. LTS CompositionC.3.2. LTS PriorityC.3.3. FSP Composition and PriorityC.4. Common OperatorsC.4.1. Re-LabelingC.4.2. HidingC.4.3. FSP Re-Labeling, Hiding and InterfaceC.5. Safety PropertiesC.6. Semantic EquivalencesC.6.1. Strong EquivalenceC.6.2. Weak EquivalenceC.7. Fluent Linear Temporal Logic (FLTL)C.7.1. Linear Temporal LogicC.7.2. Fluents
D. UML Class Diagrams
Bibliography

Content preview from Concurrency: State Models and Java Programs

Chapter 13. Program Verification

Up to this point, we have taken a modeling approach to the design of concurrent programs. Models are constructed, so that we can focus on actions, interaction and concurrency before proceeding to implementation and adding the details concerned with data representation, resource usage and user interface. We use the model as a basis for program construction by identifying a mapping from model processes to Java threads and monitor objects. However, we do not demonstrate other than by testing and observation that the behavior of the implementation corresponds to the behavior predicted by the model. Essentially, we rely on a systematic translation of the model into Java to ensure that the program satisfies the same safety and progress properties as the model.

In this chapter, we address the problem of verifying implementations, using FSP and its supporting LTSA tool. In doing verification, we translate Java programs into a set of FSP processes and show that the resulting FSP implementation model satisfies the same safety and progress properties that the design model satisfied. In this way, we can show that the program is a satisfactory implementation of its design model.

Chapter 4 of the book took exactly this approach of translating a Java program into an FSP model to investigate the problem of interference. To perform verification, we need to model the Java program at the level of variables, monitor locks and condition synchronization. In Chapter 4, we ...

Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.

Read now

Unlock full access

More than 5,000 organizations count on O’Reilly

O’Reilly covers everything we've got, with content to help us build a world-class technology community, upgrade the capabilities and competencies of our teams, and improve overall team performance as well as their engagement.

Julian F.

Head of Cybersecurity

I wanted to learn C and C++, but it didn't click for me until I picked up an O'Reilly book. When I went on the O’Reilly platform, I was astonished to find all the books there, plus live events and sandboxes so you could play around with the technology.

Addison B.

Field Engineer

I’ve been on the O’Reilly platform for more than eight years. I use a couple of learning platforms, but I'm on O'Reilly more than anybody else. When you're there, you start learning. I'm never disappointed.

Amir M.

Data Platform Tech Lead

I'm always learning. So when I got on to O'Reilly, I was like a kid in a candy store. There are playlists. There are answers. There's on-demand training. It's worth its weight in gold, in terms of what it allows me to do.

Mark W.

Embedded Software Engineer

Mastering Concurrency Programming with Java 8

Publisher Resources

ISBN: 9780470093559Purchase book

Cloud Computing

Data Engineering

Data Science

AI & ML

Programming Languages

Software Architecture

IT/Ops

Security

Design

Business

Soft Skills

Concurrency: State Models and Java Programs

by Jeff Magee, Jeff Kramer

Chapter 13. Program Verification

Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.