doc/jpf-core/IdleFilter.md

   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 ~~~~~~~~