001: package gov.nasa.jpf.mc;
002:
003: //
004: // Copyright (C) 2005 United States Government as represented by the
005: // Administrator of the National Aeronautics and Space Administration
006: // (NASA). All Rights Reserved.
007: //
008: // This software is distributed under the NASA Open Source Agreement
009: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
010: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
011: // directory tree for the complete NOSA document.
012: //
013: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
014: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
015: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
016: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
017: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
018: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
019: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
020: //
021:
022: /**
023: * This example shows a deadlock which occurs as a result of a missed signal.
024: * It also contains an assertion check that shows the race violation that is the
025: * cause for the missed signal (and ultimate deadlock)
026: * @author wvisser
027: */
028: public class oldclassic {
029: public static void main(String[] args) {
030: Event new_event1 = new Event();
031: Event new_event2 = new Event();
032:
033: FirstTask task1 = new FirstTask(new_event1, new_event2);
034: SecondTask task2 = new SecondTask(new_event1, new_event2);
035:
036: task1.start();
037: task2.start();
038: }
039: }
040:
041: /**
042: * DOCUMENT ME!
043: */
044: class Event {
045: int count = 0;
046:
047: public synchronized void signal_event() {
048: count = (count + 1) % 3;
049: notifyAll();
050: }
051:
052: public synchronized void wait_for_event() {
053: try {
054: wait();
055: } catch (InterruptedException e) {
056: }
057:
058: ;
059: }
060: }
061:
062: /**
063: * DOCUMENT ME!
064: */
065: class FirstTask extends java.lang.Thread {
066: Event event1;
067: Event event2;
068: int count = 0;
069:
070: public FirstTask(Event e1, Event e2) {
071: this .event1 = e1;
072: this .event2 = e2;
073: }
074:
075: public void run() {
076: count = event1.count;
077:
078: while (true) {
079: if (count == event1.count) {
080: assert (count == event1.count);
081: event1.wait_for_event();
082: }
083: count = event1.count;
084: event2.signal_event();
085: }
086: }
087: }
088:
089: /**
090: * DOCUMENT ME!
091: */
092: class SecondTask extends java.lang.Thread {
093: Event event1;
094: Event event2;
095: int count = 0;
096:
097: public SecondTask(Event e1, Event e2) {
098: this .event1 = e1;
099: this .event2 = e2;
100: }
101:
102: public void run() {
103: count = event2.count;
104:
105: while (true) {
106: event1.signal_event();
107: if (count == event2.count) {
108: assert (count == event2.count);
109: event2.wait_for_event();
110: }
111: count = event2.count;
112: }
113: }
114: }
|