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.
18 package gov.nasa.jpf.test.vm.threads;
20 import gov.nasa.jpf.annotation.FilterField;
21 import gov.nasa.jpf.util.test.TestJPF;
22 import gov.nasa.jpf.vm.Verify;
24 import org.junit.Test;
30 public class ThreadTest extends TestJPF {
31 static String didRunThread = null;
33 @Test public void testDaemon () {
34 if (verifyNoPropertyViolation()) {
35 Runnable r = new Runnable() {
39 Thread t = Thread.currentThread();
42 throw new RuntimeException("isDaemon failed");
45 didRunThread = t.getName();
51 Thread t = new Thread(r);
57 } catch (InterruptedException ix) {
58 throw new RuntimeException("thread was interrupted");
61 String tname = Thread.currentThread().getName();
62 if ((didRunThread == null) || (didRunThread.equals(tname))) {
63 throw new RuntimeException("thread did not execute: " + didRunThread);
68 @Test public void testDaemonTermination () {
69 if (verifyNoPropertyViolation("+cg.threads.break_start=true",
70 "+cg.threads.break_yield=true")) {
71 final Thread mainThread = Thread.currentThread();
73 Runnable r = new Runnable() {
75 @FilterField // without this, we have a perfectly open state space and never finish in JPF
80 while (true) { // loop forever or until main finishes
83 // NOTE: this does not necessarily hold outside of JPF, since the daemon might still run for a few cycles
84 assert (n < 100) || mainThread.isAlive() : "main terminated but daemon still running";
85 System.out.println(" daemon running in round: " + n);
92 Thread t = new Thread(r);
97 // finishing this thread should also (eventually) terminate the daemon
98 System.out.println("main terminating");
102 @Test public void testMain () {
103 if (verifyNoPropertyViolation()) {
104 Thread t = Thread.currentThread();
105 String refName = "main";
107 String name = t.getName();
109 if (!name.equals(refName)) {
110 throw new RuntimeException("wrong main thread name, is: " + name +
111 ", expected: " + refName);
114 refName = "my-main-thread";
118 if (!name.equals(refName)) {
119 throw new RuntimeException("Thread.setName() failed, is: " + name +
120 ", expected: " + refName);
123 int refPrio = Thread.NORM_PRIORITY;
124 int prio = t.getPriority();
126 if (prio != refPrio) {
127 throw new RuntimeException("main thread has no NORM_PRIORITY: " + prio);
131 t.setPriority(refPrio);
132 prio = t.getPriority();
134 if (prio != refPrio) {
135 throw new RuntimeException("main thread setPriority failed: " + prio);
139 throw new RuntimeException("main thread is daemon");
144 @Test public void testName () {
145 if (verifyNoPropertyViolation()) {
146 Runnable r = new Runnable() {
150 Thread t = Thread.currentThread();
151 String name = t.getName();
153 if (!name.equals("my-thread")) {
154 throw new RuntimeException("wrong Thread name: " + name);
163 Thread t = new Thread(r, "my-thread");
166 //Thread t = new Thread(r);
171 } catch (InterruptedException ix) {
172 throw new RuntimeException("thread was interrupted");
175 String tname = Thread.currentThread().getName();
176 if ((didRunThread == null) || (didRunThread.equals(tname))) {
177 throw new RuntimeException("thread did not execute: " + didRunThread);
182 public void testSingleYield () {
186 @Test public void testYield () {
187 if (verifyNoPropertyViolation("+cg.threads.break_start=true",
188 "+cg.threads.break_yield=true")) {
189 Runnable r = new Runnable() {
193 Thread t = Thread.currentThread();
195 while (!didRunThread.equals("blah")) {
199 didRunThread = t.getName();
203 didRunThread = "blah";
205 Thread t = new Thread(r);
208 while (didRunThread.equals("blah")) {
212 String tname = Thread.currentThread().getName();
213 if ((didRunThread == null) || (didRunThread.equals(tname))) {
214 throw new RuntimeException("thread did not execute: " + didRunThread);
220 @Test public void testPriority () {
221 if (verifyNoPropertyViolation()) {
222 Runnable r = new Runnable() {
226 Thread t = Thread.currentThread();
227 int prio = t.getPriority();
229 if (prio != (Thread.MIN_PRIORITY + 2)) {
230 throw new RuntimeException("wrong Thread priority: " + prio);
233 didRunThread = t.getName();
239 Thread t = new Thread(r);
240 t.setPriority(Thread.MIN_PRIORITY + 2);
245 } catch (InterruptedException ix) {
246 throw new RuntimeException("thread was interrupted");
249 String tname = Thread.currentThread().getName();
250 if ((didRunThread == null) || (didRunThread.equals(tname))) {
251 throw new RuntimeException("thread did not execute: " + didRunThread);
256 @Test public void testJoin () {
257 if (verifyNoPropertyViolation()) {
258 Runnable r = new Runnable() {
261 public synchronized void run() {
262 didRunThread = Thread.currentThread().getName();
266 Thread t = new Thread(r);
271 if (didRunThread != null) {
272 throw new RuntimeException("sync thread did execute before lock release");
278 } catch (InterruptedException ix) {
279 throw new RuntimeException("main thread was interrupted");
282 if (didRunThread == null) {
283 throw new RuntimeException("sync thread did not run after lock release");
288 @Test public void testTimeoutJoin () {
290 Verify.resetCounter(0);
291 Verify.resetCounter(1);
294 if (verifyNoPropertyViolation()) {
295 Runnable r = new Runnable() {
300 System.out.println("[t] started");
302 didRunThread = Thread.currentThread().getName(); // this causes a CG
303 System.out.println("[t] finished");
307 Thread t = new Thread(r);
312 if (didRunThread != null) {
313 throw new RuntimeException("sync thread did execute before lock release");
318 System.out.println("[main] joining..");
320 System.out.println("[main] joined, t state: " + t.getState());
322 // we should get here for both terminated and non-terminated t
323 switch (t.getState()) {
325 if (didRunThread != null){
326 Verify.incrementCounter(0);
330 Verify.incrementCounter(1);
333 throw new RuntimeException("infeasible thread state: " + t.getState());
336 } catch (InterruptedException ix) {
337 throw new RuntimeException("main thread was interrupted");
342 assert Verify.getCounter(0) > 0;
343 assert Verify.getCounter(1) > 0;
348 @Test public void testInterrupt() {
349 if (verifyNoPropertyViolation()) {
351 Runnable r = new Runnable() {
354 public synchronized void run() {
356 didRunThread = Thread.currentThread().getName();
357 System.out.println("-- t waiting");
359 } catch (InterruptedException x) {
360 System.out.println("-- t interrupted");
363 System.out.println("-- t terminated");
367 Thread t = new Thread(r);
370 while (didRunThread == null) {
375 System.out.println("-- main thread interrupting...");
381 } catch (InterruptedException ix) {
382 throw new RuntimeException("main thread was interrupted");
385 if (didRunThread != null) {
386 throw new RuntimeException("t did not get interrupted");
389 System.out.println("-- main thread terminated");
394 @Test public void testSimpleThreadGroup () {
395 if (verifyNoPropertyViolation()) {
397 System.out.println("-- main thread started");
399 Thread mainThread = Thread.currentThread();
400 final ThreadGroup sysGroup = mainThread.getThreadGroup();
403 assert sysGroup != null && sysGroup.getName().equals("main");
405 int active = sysGroup.activeCount();
407 Thread[] list = new Thread[active];
409 int n = sysGroup.enumerate(list);
410 assert (n == active);
411 assert list[0] == mainThread;
414 Runnable r = new Runnable() {
418 System.out.println("-- t started");
419 didRunThread = Thread.currentThread().getName();
421 Thread t = Thread.currentThread();
422 ThreadGroup group = t.getThreadGroup();
424 assert group != null && group == sysGroup;
426 int active = group.activeCount();
428 Thread[] list = new Thread[active];
430 int n = group.enumerate(list);
431 assert (n == active);
434 System.out.println("-- t terminated");
438 Thread t = new Thread(r);
443 } catch (InterruptedException ix) {
444 throw new RuntimeException("main thread was interrupted");
447 if (didRunThread == null) {
448 throw new RuntimeException("t did not run");
451 System.out.println("-- main thread terminated");