Tutorial at ASE 2006 

1. Remote Agent Deadlock

oldclassic.java is aptly names since it was essentially the first program ever 
to be run through JPF. It is a small version of the deadlock that
occured during the Deep-Space 1 Remote Agent mission in May 1999.

bin/jpf ase2006.oldclassic

2. Attempted Fix for oldclassic

clean.java

When we tried to fix the bug, JPF still reported an error. Since this was early
days we thought the tool had a bug, as it turns out, it was correct - there
was still a bug. This version must have the "count = event?.count" assignments. 
when it those are replaced by "count = 0" the program is deadlock free.

bin/jpf ase2006.clean

3. K9 Rover

This is a Java version of a prototype Mars rover (orginally in C/C++). It was used 
during an extensive experiment to determine the usefulness of model checking
versus testing:
Experimental Evaluation of Verification and Validation Tools on Martian Rover Software
G. Brat, D. Drusinsky, D. Giannakopoulou, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, A. Venet, R. Washington and W. Visser
Formal Methods in Systems Design Journal
Volume 25, September 2005 
Download from Google "Willem Visser" under Journal Papers

bin/jpf -c k9.properties k9.Main
k9.properties sets the search to BFS with a 200 frontier and also allows the use of
the two Filtering options (by commenting the relevant one out).

Below follow the results to finding the deadlock in the code:

Running without Filtering:

  abs time:          00:02:02  (122141 ms)
  rel. time [ms]:    2141

  search depth:      84 (max: 84)
  new states:        70451
  revisited states:  3246
  end states:        0
  backtracks:        73696
  processed states:  14984 (4.9 bt/proc state)
  restored states:   14984
  queue size:        199

  total memory [kB]: 588948 (max: 1040512)
  free memory [kB]:  209387
  heap objects:      385 (max: 1701)

With Filtering: // getting rid of unnecessary information in the states and does heap symmetry 

  abs time:          00:02:17  (137625 ms)
  rel. time [ms]:    7625

  search depth:      70 (max: 70)
  new states:        45123
  revisited states:  12163
  end states:        0
  backtracks:        57285
  processed states:  12011 (4.7 bt/proc state)
  restored states:   12011
  queue size:        199

  total memory [kB]: 162084 (max: 1040512)
  free memory [kB]:  55512
  heap objects:      1504 (max: 1701)

With Abstraction (which includes filtering): // also does thread symmetry

  abs time:          00:04:43  (283766 ms)
  rel. time [ms]:    3766

  search depth:      70 (max: 70)
  new states:        45123
  revisited states:  12163
  end states:        0
  backtracks:        57285
  processed states:  12011 (4.7 bt/proc state)
  restored states:   12011
  queue size:        199

  total memory [kB]: 184572 (max: 1040512)
  free memory [kB]:  71805
  heap objects:      1504 (max: 1701)

Thread symmetry therefore did nothing here, except increase runtime, not 
too suprising since there is no thread symmetry here!

4. Dining Philosophers!

Needs no introduction!

Reults are for 5 Philosophers and all checks are switched off.

bin/jpf -c dining.properties ase2006.DiningPhil

No Filtering: 
  abs time:          00:01:28  (88797 ms)
  rel. time [ms]:    8797

  search depth:      1 (max: 18)
  new states:        155791
  revisited states:  301191
  end states:        1
  backtracks:        456981
  processed states:  155790 (2.9 bt/proc state)
  restored states:   0

  total memory [kB]: 8280 (max: 1040512)
  free memory [kB]:  2631
  heap objects:      143 (max: 146)

Filtering:

  abs time:          00:00:02  (2640 ms)
  rel. time [ms]:    2640

  search depth:      1 (max: 18)
  new states:        2301
  revisited states:  5272
  end states:        1
  backtracks:        7572
  processed states:  2300 (3.2 bt/proc state)
  restored states:   0

  total memory [kB]: 3572 (max: 1040512)
  free memory [kB]:  0
  heap objects:      134 (max: 146)

Abstraction:

  abs time:          00:00:03  (3203 ms)
  rel. time [ms]:    3203

  search depth:      1 (max: 18)
  new states:        1337
  revisited states:  3145
  end states:        1
  backtracks:        4481
  processed states:  1336 (3.3 bt/proc state)
  restored states:   0

  total memory [kB]: 3580 (max: 1040512)
  free memory [kB]:  0
  heap objects:      134 (max: 146)

One can now see that the Thread symmetry can make a difference in the states.

Now let us try bigger numbers:

8 Philos

Normal: no point!

Filtering: 

  abs time:          00:04:00  (240312 ms)
  rel. time [ms]:    312

  search depth:      1 (max: 30)
  new states:        209014
  revisited states:  884380
  end states:        1
  backtracks:        1093393
  processed states:  209013 (5.2 bt/proc state)
  restored states:   0

  total memory [kB]: 10652 (max: 1040512)
  free memory [kB]:  4133
  heap objects:      137 (max: 161)

Abstraction:

  abs time:          00:06:39  (399109 ms)
  rel. time [ms]:    9078

  search depth:      1 (max: 30)
  new states:        149801
  revisited states:  640377
  end states:        1
  backtracks:        790177
  processed states:  149800 (5.2 bt/proc state)
  restored states:   0

  total memory [kB]: 7528 (max: 1040512)
  free memory [kB]:  2717
  heap objects:      137 (max: 161)

One can see that the more advanved the reductions the longer it takes.

5. Stoned Hippies (aka Crossing)

This is the classic problem of how to get 4 stoned hippies from Germany to the
Netherlands over a bringe with just one flashlight; at most two at a time; and 
they take must cross at the speed of the slowest one - respectively 1,2,5 and 
10 minutes each. Spoiler: answer is 17. 

Lets use JPF to find it. The problem is encoded in Java and it is asserted 
that all solutions are greater than 17. JPF then finds the counterexample which
is also the answer to the puzzle. To illustrate a number of different 
features we will solve it in many different ways.

The main file is Crossing.java.

In the vanilla run we just let JPF loose on it in BFS mode using the 
crossing.properties file for configuration:

bin/jpf -c crossing.properties ase2006.Crossing

After running for a while (+- 2s) it will produce:

p3(5)p4(10) - 2 -> p1(1)p2(2)

p2(2)p3(5)p4(10) - 4 -> p1(1)

p2(2) - 14 -> p1(1)p3(5)p4(10)

p1(1)p2(2) - 15 -> p3(5)p4(10)

 - 17 -> p1(1)p2(2)p3(5)p4(10)

total time = 17

i.e. the answer to the puzzle (first move 1,2 then bring 2 back, move 5,10 then
bring 1 back and finally 1,2 cross = total 17).

Now uncomment the following line in Crossing.java:
Verify.ignoreIf(total > 17);

This line tells JPF to chop off any path that reaches this point in
the code and the condition does not hold. This basically means that we
make this problem finite - note it was not finite state before, since 
the time taken keeps increasing if you constantly cross. Rerunning will
prduice the same results as before. However now one can also find the 
solution in DFS mode, so comment out the line in properties file
taht sets the heuristic search, which has the net effect of doing a DFS.

Exercise to the reader, what will happen if we change the line to
Verify.ignoreIf(total > 50);
and still do a DFS search?

Answer: it will run longer, but the problem is still finite so it will find
the solution.

And in BFS?

Answer: nothing will change from the original BFS without that line, in BFS
it will find the solution long before it will chop off any paths.

Ok, but we cheated here, we knew the answer was 17, what if we didn't know 
that! Now things get more tricky, since we need to run JPF find a solution
and use that solution to try and get a better one, etc. until we find the
optimal solution. But how do we store a solution? Note, we cannot just store 
the answer at the end, since that is not persistent, it will get removed the 
moment JPf backtracks to look for another path to explore. 

We will first use the Model Java Interface (MJI) approach. By using some
native peer methods we can store persistent results, since the data in the
peer is not in the state of the program being checked and is thus persistent.

bin/jpf -c crossing.properties ase2006.CrossingNative

will produce (starting with a best solution of 30):
new total 24
new total 23
new total 21
new total 20
new total 19
new total 17

The trick here lies in the JPF_ase2006_CrossingNative.java file
where the getTotal and setTotal methods are defined which are
declared native in the class JPF is running on namely CrossingNative.
Basically the original solution (30) is set at the beginning and
then every time a better solution is found (by comparing the 
current solution with the getTotal()) the new solution is set.
Note also that the line that chops off bad paths are now:
Verify.ignoreIf(total >= getTotal());
which says if the current solution is >= the optimal so far
then stop analyzing it.

There is one more approach one can take here to find the optimal solution
and that is to use a listener. This will also illustrate how to run JPF 
from within another program (the Listener in this case). 

Now run:

Optimizer ase2006.CrossingListener 30

This will start running JPF with a best solution of 30, if it finds one
smaller then it asserts false which is a property violation and it records the
solution at the time with which it then reruns JPF, until two solutions
in a row are the same, i.e. a fixpoint is reached. It communicates the 
solution via a listener that listens for the CheckTotal call and then
records the solution. See the Optimzer code and the CrossingListener code.

Exercise to the reader: what will happen if comment out the body of the 
CheckTotal method in CrossingListener?

Answer: it will find the optimal solution straight away! Why??

6. Now for a more useful Listener - the Race Detector

In the file RaceReal.java we have a race violation. If we run:

bin/jpf +jpf.listener=gov.nasa.jpf.tools.RaceDetector ase2006.RaceReal

it find the error, producing the call stacks:

thread index=0,name=main,status=RUNNING,this=java.lang.Thread@3,target=null,priority=5,lockCount=0
  call stack:
	at ase2006.RaceReal.main(ase2006\RaceReal.java:15)

thread index=1,name=Thread-0,status=RUNNING,this=java.lang.Thread@100,target=ase2006.RaceReal@99,priority=5,lockCount=0
  call stack:
	at ase2006.RaceReal.run(ase2006\RaceReal.java:6)

Note it also states earlier in the results which field is accessed in the
violation as well as the exact steps to get to this situation.

In the file Race1.java we have a barrier that protects the access
to the field. If we run the RaceDetector in it's simple form it thinks there
is a race:
bin/jpf +jpf.listener=gov.nasa.jpf.tools.RaceDetector ase2006.Race1

Output:

potential race detected: ase2006.Race1@103.f
	read from thread: "Thread-0", holding locks {} in ase2006.Race1.ase2006.Race1.run()V at ase2006\Race1.java:27
	write from thread: "main", holding locks {} in ase2006.Race1.ase2006.Race1.main([Ljava/lang/String;)V at ase2006\Race1.java:36

If however we check to see if it is also possible for this race to occur in the
reverse order (uysing the race.verigy_cycle=true option), we find it is not, 
which means it was a spurious warning. 

bin/jpf +jpf.listener=gov.nasa.jpf.tools.RaceDetector +race.verify_cycle=true ase2006.Race1

No error found.

7. Showing the effects of modCount

If you did not do model checking for Java you'd probably not know that a program
such as BasicModCount

8. Showing the effect of annotations in BasicIgnore

Filtering the BitSet, gives you count+1 states

Filtering also the loop counter, gives you 1 state

Note that we don't currentlly support Filtering of local variables - 9/16/06

3. Testing of Partial Traces

bin/jpf +vm.use_trace=testPartialTrace.trace ase2006.TestPartialTrace

When run the first time it generates a trace to get to a specific state in the 
state space; when rerun it explores from that state, but first executing the 
trace and then to explore the state space.

This effect is illustrated by printing the values of ChoiceGenerators:
1st run: 
pre-trace choice 0,100
2nd run: 
pre-trace choice: 0,100
post-trace choice: 0,100,0
post-trace choice: 0,100,1
post-trace choice: 0,100,2
post-trace choice: 0,100,3



