KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > Bakery_original


1 //
2 // Copyright (C) 2005 United States Government as represented by the
3 // Administrator of the National Aeronautics and Space Administration
4 // (NASA). All Rights Reserved.
5 //
6 // This software is distributed under the NASA Open Source Agreement
7 // (NOSA), version 1.3. The NOSA has been approved by the Open Source
8 // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
9 // directory tree for the complete NOSA document.
10 //
11 // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12 // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13 // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14 // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15 // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16 // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17 // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18 //
19
20 /**
21  * This example shows how the use of the default <CODE>atomic-lines</CODE>
22  * option could result in JPF reporting the existence of a bogus livelock. JPF
23  * reports the livelock at:
24  * <PRE>
25  * ...
26  * while (p2.y2 != 0 && y1 >= p2.y2);
27  * ...
28  * </PRE>
29  * The reason is obvious. By using the default option we have told JPF to run
30  * the whole while loop atomically with no possibility of the other thread
31  * changing the outcome of the evaluation of the while loop's condition. To
32  * solve this you have two choices: You can use the <CODE>-no-atomic-lines
33  * </CODE> option when you run JPF or alternatively add a dummy body to the
34  * while loop, in effect making it a statement over multiple lines.
35  */
36 class Property {
37   static boolean flag = true;
38 }
39
40 /**
41  * DOCUMENT ME!
42  */
43 class Process1 extends Thread JavaDoc {
44   public int y1 = 0;
45   private Process2 p2;
46
47   public void run () {
48     while (true) {
49       y1 = p2.y2 + 1;
50
51       // System.out.println("P1: [ busy wait, y1=" + y1);
52 while ((p2.y2 != 0) && (y1 >= p2.y2)) {
53         ;
54       }
55
56
57       // System.out.println("P1: ] busy wait, y1=" + y1);
58 Property.flag = false;
59       Property.flag = true;
60
61       y1 = 0;
62     }
63   }
64
65   void SetThread (Process2 p) {
66     p2 = p;
67   }
68 }
69
70 /**
71  * DOCUMENT ME!
72  */
73 class Process2 extends Thread JavaDoc {
74   public int y2 = 0;
75   private Process1 p1;
76
77   public void run () {
78     while (true) {
79       y2 = p1.y1 + 1;
80
81       // System.out.println("P2: [ busy wait, y2=" + y2);
82 while ((p1.y1 != 0) && (y2 > p1.y1)) {
83         ;
84       }
85
86
87       // System.out.println("P2: ] busy wait, y2=" + y2);
88 Property.flag = false;
89       Property.flag = true;
90
91       y2 = 0;
92     }
93   }
94
95   void SetThread (Process1 p) {
96     p1 = p;
97   }
98 }
99
100 /**
101  * DOCUMENT ME!
102  */
103 class Bakery_original {
104   public static void main (String JavaDoc[] args) {
105     Process1 process1 = new Process1();
106     Process2 process2 = new Process2();
107     process1.SetThread(process2);
108     process2.SetThread(process1);
109
110     process1.start();
111     process2.start();
112   }
113 }
Popular Tags