Mercurial > hg > Members > kono > jpf-core
comparison doc/jpf-core/IdleFilter.md @ 0:61d41facf527
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 # IdleFilter # | |
2 | |
3 The `gov.nasa.jpf.listener.IdleFilter` is a listener that can be used to close state spaces with loops. Consider a simple "busy waiting" loop | |
4 | |
5 ~~~~~~~~ {.java} | |
6 for (long l=0; l<10000000; l++); | |
7 ~~~~~~~~ | |
8 | |
9 While not a good thing to do in general, it is benign if executed in a normal VM. For JPF, it causes trouble because it adds a lot of useless steps to the stored path, and slows down execution considerably. | |
10 | |
11 In addition, people who expect JPF to match states can get surprised by programs like | |
12 | |
13 ~~~~~~~~ {.java} | |
14 while (true){ | |
15 // no transition break in here | |
16 } | |
17 ~~~~~~~~ | |
18 not being state matched, and hence not terminating (it wouldn't terminate in a normal VM either). | |
19 | |
20 `IdleFilter` is a little tool to deal with such (bad) loops. It counts the number of back-jumps it encounters within the same thread and stackframe, and if this number exceeds a configured threshold it takes one of the following actions: | |
21 | |
22 * warn - just prints out a warning that we have a suspicious loop | |
23 * break - breaks the transition at the back-jump `goto` instruction, to allow state matching | |
24 * prune - sets the transition ignored, i.e. prunes the search tree | |
25 * jump - skips the back-jump. This is the most dangerous action since you better make sure the loop does not contain side-effects your program depends on. | |
26 | |
27 | |
28 ### Properties ### | |
29 Consequently, there are two options: | |
30 | |
31 * `idle.max_backjumps = \<number\>` : max number of back-jumps that triggers the configured action (default 500) | |
32 * `idle.action = warn|break|prune|jump` : action to take when number of back-jumps exceeds threshold | |
33 | |
34 ### Examples ### | |
35 | |
36 **(1)** The test program | |
37 | |
38 ~~~~~~~~ {.java} | |
39 ... | |
40 public void testBreak () { | |
41 int y = 4; | |
42 int x = 0; | |
43 | |
44 while (x != y) { // JPF should state match on the backjump | |
45 x = x + 1; | |
46 if (x > 3) { | |
47 x = 0; | |
48 } | |
49 } | |
50 } | |
51 ~~~~~~~~ | |
52 | |
53 would never terminate under JPF or a host VM. Running it with | |
54 | |
55 ~~~~~~~~ {.bash} | |
56 > bin/jpf +listener=.listener.IdleFilter +idle.action=break ... | |
57 ~~~~~~~~ | |
58 | |
59 does terminate due to state matching and produces the following report | |
60 | |
61 ~~~~~~~~ {.bash} | |
62 ... | |
63 ====================================================== search started: 4/8/10 4:14 PM | |
64 [WARNING] IdleFilter breaks transition on suspicious loop in thread: main | |
65 at gov.nasa.jpf.test.mc.basic.IdleLoopTest.testBreak(gov/nasa/jpf/test/mc/basic/IdleLoopTest.java:42) | |
66 ... | |
67 ====================================================== results | |
68 no errors detected | |
69 ~~~~~~~~ | |
70 | |
71 ----- | |
72 **(2)** The following program would execute a long time under JPF | |
73 | |
74 ~~~~~~~~ {.java} | |
75 ... | |
76 public void testJump () { | |
77 for (int i=0; i<1000000; i++){ | |
78 //... | |
79 } | |
80 | |
81 System.out.println("Ok, jumped past loop"); | |
82 } | |
83 ~~~~~~~~ | |
84 | |
85 If we run it with | |
86 | |
87 ~~~~~~~~ {.bash} | |
88 > bin/jpf +listener=.listener.IdleFilter +idle.action=jump ... | |
89 ~~~~~~~~ | |
90 | |
91 JPF comes back quickly with the result | |
92 | |
93 ~~~~~~~~ {.bash} | |
94 ====================================================== search started: 4/8/10 4:20 PM | |
95 [WARNING] IdleFilter jumped past loop in: main | |
96 at gov.nasa.jpf.test.mc.basic.IdleLoopTest.testJump(gov/nasa/jpf/test/mc/basic/IdleLoopTest.java:74) | |
97 Ok, jumped past loop | |
98 ... | |
99 ~~~~~~~~ |