2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
10 * http://www.apache.org/licenses/LICENSE-2.0.
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
20 * This example shows a deadlock that occurs as a result of a missed signal,
21 * i.e. a wait() that happens after the corresponding notify().
23 * The defect is caused by a violated monitor encapsulation, i.e. directly
24 * accessing monitor internal data ('Event.count') from concurrent clients
25 * ('FirstTask', 'SecondTask'), without synchronization with the
26 * corresponding monitor operations ('wait_for-Event()' and 'signalEvent()').
28 * The resulting race is typical for unsafe optimizations that try to
29 * avoid expensive blocking calls by means of local caches
31 * This example was inspired by a defect found in the "Remote Agent"
32 * spacecraft controller that flew on board of "Deep Space 1", as described
35 * Model Checking Programs
36 * W. Visser, K. Havelund, G. Brat, S. Park and F. Lerda
37 * Automated Software Engineering Journal
38 * Volume 10, Number 2, April 2003
43 //------- the test driver
44 public class oldclassic {
45 public static void main (String[] args) {
46 Event new_event1 = new Event();
47 Event new_event2 = new Event();
49 FirstTask task1 = new FirstTask(new_event1, new_event2);
50 SecondTask task2 = new SecondTask(new_event1, new_event2);
57 //------- shared objects implemented as monitors
61 public synchronized void signal_event () {
63 // NOTE: this abstraction is not strictly required - even if the state space would
64 // be unbound, JPF could still find the error at a reasonable search depth,
65 // unless it's left-most branch in the search tree is unbound. If it is,
66 // there are two ways to work around: (1) use a different search strategy
67 // (e.g. HeuristicSearch with BFSHeuristic), or (2) set a random choice
68 // enumeration order ("+cg.randomize_choices=true"). In this example, (2)
70 count = (count + 1) % 3;
71 //count++; // requires "+cg.randomize_choices=true" for DFSearch policy
76 public synchronized void wait_for_event () {
79 } catch (InterruptedException e) {
84 //------- the two concurrent threads using the monitors
85 class FirstTask extends Thread {
88 int count = 0; // bad optimization - local cache of event1 internals
90 public FirstTask (Event e1, Event e2) {
97 count = event1.count; // <race> violates event1 monitor encapsulation
100 System.out.println("1");
102 if (count == event1.count) { // <race> ditto
103 event1.wait_for_event();
106 count = event1.count; // <race> ditto
107 event2.signal_event(); // updates event2.count
112 class SecondTask extends Thread {
115 int count = 0; // bad optimization - local cache of event2 internals
117 public SecondTask (Event e1, Event e2) {
124 count = event2.count; // <race> violates event2 monitor encapsulation
127 System.out.println(" 2");
128 event1.signal_event(); // updates event1.count
130 if (count == event2.count) { // <race> ditto
131 event2.wait_for_event();
134 count = event2.count; // <race> ditto