Mercurial > hg > Members > kono > jpf-core

annotate doc/jpf-core/IdleFilter.md @ 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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
1 # IdleFilter #
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
2
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
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
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
4
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
5 ~~~~~~~~ {.java}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
6 for (long l=0; l<10000000; l++);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
7 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
8
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
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.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
10
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
11 In addition, people who expect JPF to match states can get surprised by programs like
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
12
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
13 ~~~~~~~~ {.java}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
14 while (true){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
15 // no transition break in here
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
16 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
17 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
18 not being state matched, and hence not terminating (it wouldn't terminate in a normal VM either).
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
19
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
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:
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
21
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
22 * warn - just prints out a warning that we have a suspicious loop
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
23 * break - breaks the transition at the back-jump `goto` instruction, to allow state matching
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
24 * prune - sets the transition ignored, i.e. prunes the search tree
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
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.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
26
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
27
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
28 ### Properties ###
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
29 Consequently, there are two options:
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
30
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
31 * `idle.max_backjumps = \<number\>` : max number of back-jumps that triggers the configured action (default 500)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
32 * `idle.action = warn|break|prune|jump` : action to take when number of back-jumps exceeds threshold
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
33
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
34 ### Examples ###
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
35
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
36 **(1)** The test program
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
37
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
38 ~~~~~~~~ {.java}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
39 ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
40 public void testBreak () {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
41 int y = 4;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
42 int x = 0;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
43
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
44 while (x != y) { // JPF should state match on the backjump
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
45 x = x + 1;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
46 if (x > 3) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
47 x = 0;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
48 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
49 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
50 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
51 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
52
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
53 would never terminate under JPF or a host VM. Running it with
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
54
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
55 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
56 > bin/jpf +listener=.listener.IdleFilter +idle.action=break ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
57 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
58
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
59 does terminate due to state matching and produces the following report
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
60
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
61 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
62 ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
63 ====================================================== search started: 4/8/10 4:14 PM
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
64 [WARNING] IdleFilter breaks transition on suspicious loop in thread: main
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
65 at gov.nasa.jpf.test.mc.basic.IdleLoopTest.testBreak(gov/nasa/jpf/test/mc/basic/IdleLoopTest.java:42)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
66 ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
67 ====================================================== results
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
68 no errors detected
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
69 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
70
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
71 -----
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
72 **(2)** The following program would execute a long time under JPF
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
73
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
74 ~~~~~~~~ {.java}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
75 ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
76 public void testJump () {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
77 for (int i=0; i<1000000; i++){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
78 //...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
79 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
80
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
81 System.out.println("Ok, jumped past loop");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
82 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
83 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
84
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
85 If we run it with
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
86
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
87 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
88 > bin/jpf +listener=.listener.IdleFilter +idle.action=jump ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
89 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
90
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
91 JPF comes back quickly with the result
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
92
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
93 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
94 ====================================================== search started: 4/8/10 4:20 PM
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
95 [WARNING] IdleFilter jumped past loop in: main
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
96 at gov.nasa.jpf.test.mc.basic.IdleLoopTest.testJump(gov/nasa/jpf/test/mc/basic/IdleLoopTest.java:74)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
97 Ok, jumped past loop
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
98 ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
99 ~~~~~~~~