Mercurial > hg > Members > kono > jpf-core

comparison src/tests/gov/nasa/jpf/test/mc/basic/SharedPropagationTest.java @ 0:61d41facf527

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial v8 import (history reset)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 23 Jan 2015 10:14:01 -0800
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:61d41facf527
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 package gov.nasa.jpf.test.mc.basic;
20
21 import gov.nasa.jpf.util.test.TestJPF;
22 import org.junit.Test;
23
24 /**
25 * various shared object propagations that could lead to missed paths
26 */
27 public class SharedPropagationTest extends TestJPF {
28
29 static class Gotcha extends RuntimeException {
30 // nothing in here
31 }
32
33 //--- simple local ref
34
35 static class T1 extends Thread {
36
37 static class X {
38
39 boolean pass;
40 }
41 X myX; // initially not set
42
43 public static void main(String[] args) {
44 T1 t = new T1();
45 t.start();
46
47 X x = new X();
48 t.myX = x; // (0) x not shared until this GOT executed
49
50 //Thread.yield(); // this would expose the error
51 x.pass = true; // (1) need to break BEFORE assignment or no error
52 }
53
54 @Override
55 public void run() {
56 if (myX != null) {
57 if (!myX.pass) { // (2) won't fail unless main is between (0) and (1)
58 throw new Gotcha();
59 }
60 }
61 }
62 }
63
64 @Test
65 public void testLocalRef(){
66 if (verifyUnhandledException( Gotcha.class.getName(), "+vm.scheduler.sharedness.class=.vm.GlobalSharednessPolicy")){
67 T1.main(new String[0]);
68 }
69 }
70
71
72 //--- one reference level down
73
74 static class T2 extends Thread {
75
76 static class X {
77 boolean pass;
78 }
79
80 static class Y {
81 X x;
82 }
83
84 Y y;
85
86 public static void main(String[] args) {
87 T2 t = new T2();
88 Y y = new Y();
89 X x = new X();
90
91 y.x = x;
92 // neither x nor y shared at this point
93
94 t.start();
95 t.y = y; // y becomes shared, and with it x
96
97 x.pass = true;
98 }
99
100 @Override
101 public void run() {
102 if (y != null) {
103 if (!y.x.pass) {
104 throw new Gotcha();
105 }
106 }
107 }
108 }
109
110 @Test
111 public void testLevel1Ref(){
112 if (verifyUnhandledException(Gotcha.class.getName())){
113 T2.main(new String[0]);
114 }
115 }
116
117 //--- propagation via static field
118
119 static class T3 extends Thread {
120
121 static class X {
122 boolean pass;
123 }
124
125 static class Y {
126 X x;
127 }
128 static Y globalY; // initially not set
129
130
131 public static void main(String[] args) {
132 T3 t = new T3();
133 t.start();
134
135 X x = new X();
136 Y y = new Y();
137 y.x = x;
138
139 globalY = y; // (0) x not shared until this GOT executed
140
141 //Thread.yield(); // this would expose the error
142 x.pass = true; // (1) need to break BEFORE assignment or no error
143 }
144
145 @Override
146 public void run() {
147 if (globalY != null) {
148 if (!globalY.x.pass) { // (2) won't fail unless main is between (0) and (1)
149 throw new Gotcha();
150 }
151 }
152 }
153 }
154
155 @Test
156 public void testStaticFieldPropagation(){
157 if (verifyUnhandledException(Gotcha.class.getName(), "+vm.scheduler.sharedness.class=.vm.GlobalSharednessPolicy")){
158 T3.main(new String[0]);
159 }
160 }
161
162
163 //--- the infamous Hyber example
164
165 static class Hyber {
166 private static Timeout thread = new Timeout();
167
168 public static void main(String[] args) {
169 thread.start();
170 Timeout.Entry timer = thread.setTimeout(); // (0)
171 //Thread.yield(); // this forces the error
172 timer.hyber = true; // (1) we need to break here to catch the error
173 }
174 }
175
176 static class Timeout extends Thread {
177
178 static class Entry {
179 boolean hyber = false;
180 Entry next = null;
181 Entry prev = null;
182 }
183 Entry e = new Entry();
184
185 Timeout() {
186 e.next = e.prev = e;
187 }
188
189 public Entry setTimeout() {
190 Entry entry = new Entry();
191 synchronized (e) {
192 entry.next = e;
193 entry.prev = e.prev;
194 entry.prev.next = entry;
195 entry.next.prev = entry;
196 }
197
198 return entry;
199 }
200
201 @Override
202 public void run() {
203 synchronized (e) {
204 for (Entry entry = e.next; entry != e; entry = entry.next) {
205 if (!entry.hyber) { // (2) only fails if main thread between (0) and (1)
206 throw new Gotcha();
207 }
208 }
209 }
210 }
211 }
212
213 @Test
214 public void testHyber() {
215 if (verifyUnhandledException(Gotcha.class.getName(), "+vm.scheduler.sharedness.class=.vm.GlobalSharednessPolicy")){
216 Hyber.main(new String[0]);
217 }
218 }
219
220 }