src/examples/oldclassic.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   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
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  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.
  17  */
  18
  19 /**
  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().
  22  *
  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()').
  27  *
  28  * The resulting race is typical for unsafe optimizations that try to
  29  * avoid expensive blocking calls by means of local caches
  30  *
  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
  33  * in:
  34  *
  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
  39  *
  40  * @author wvisser
  41  */
  42
  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();
  48
  49     FirstTask  task1 = new FirstTask(new_event1, new_event2);
  50     SecondTask task2 = new SecondTask(new_event1, new_event2);
  51
  52     task1.start();
  53     task2.start();
  54   }
  55 }
  56
  57 //------- shared objects implemented as monitors
  58 class Event {
  59   int count = 0;
  60
  61   public synchronized void signal_event () {
  62
  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)
  69     // works just fine
  70     count = (count + 1) % 3;
  71     //count++;  // requires "+cg.randomize_choices=true" for DFSearch policy
  72
  73     notifyAll();
  74   }
  75
  76   public synchronized void wait_for_event () {
  77     try {
  78       wait();
  79     } catch (InterruptedException e) {
  80     }
  81   }
  82 }
  83
  84 //------- the two concurrent threads using the monitors
  85 class FirstTask extends Thread {
  86   Event event1;
  87   Event event2;
  88   int   count = 0;  // bad optimization - local cache of event1 internals
  89
  90   public FirstTask (Event e1, Event e2) {
  91     this.event1 = e1;
  92     this.event2 = e2;
  93   }
  94
  95   @Override
  96   public void run () {
  97     count = event1.count;          // <race> violates event1 monitor encapsulation
  98
  99     while (true) {
 100       System.out.println("1");
 101
 102       if (count == event1.count) { // <race> ditto
 103         event1.wait_for_event();
 104       }
 105
 106       count = event1.count;        // <race> ditto
 107       event2.signal_event();       // updates event2.count
 108     }
 109   }
 110 }
 111
 112 class SecondTask extends Thread {
 113   Event event1;
 114   Event event2;
 115   int   count = 0;  // bad optimization - local cache of event2 internals
 116
 117   public SecondTask (Event e1, Event e2) {
 118     this.event1 = e1;
 119     this.event2 = e2;
 120   }
 121
 122   @Override
 123   public void run () {
 124     count = event2.count;          // <race> violates event2 monitor encapsulation
 125
 126     while (true) {
 127       System.out.println("  2");
 128       event1.signal_event();       // updates event1.count
 129
 130       if (count == event2.count) { // <race> ditto
 131         event2.wait_for_event();
 132       }
 133
 134       count = event2.count;        // <race> ditto
 135     }
 136   }
 137 }