End of Google Summer of Code - Concluding Remarks

Since the program is officially ending, everyone should know the state of the jpf-prism code at this end. In case there is anyone reading this blog that I don't email updates to, I'm going post some concluding remarks here, taken from an email I sent to my advisers/supervisors.

All the code for the project is found at the BitBucket repository, https://bitbucket.org/jpfprism/jpf-prism, which is still private, but hopefully we'll open it up soon. The Javadoc for the code, which unfortunately cannot be hosted on the same page, is located on my department webpage: http://www.math.uvic.ca/~jgorzny/jpf-prism-doc/ (and is included in the repository). A pointer to this link, as well as brief tutorials on how to install the code, run the code, and specify properties to check, can be found on the wiki on the BitBucket repository: https://bitbucket.org/jpfprism/jpf-prism/wiki/Home. 

As for the final state of the code in terms of functionality, I think it went pretty well (though not everyone was finished, I'm afraid). The short of it is that we can check any Java program that uses probabilistic functions based on Java's Random() (or jpf-probabilistic's Choice()) method. By "check" I mean that PRISM will be invoked on the states of the system and compute the probability of reaching a state with that property being true. Further, in case verification takes too long, or to confirm results, jpf-prism can be used to run the Java code repeatedly without interference, to get an empirical measure of the probability of reaching such a state. Further, the code will optimize the states of the systems if possible: it will reduce chains of states that are connected with probability 1 to a single state, unless it cannot (e.g., a choice was made, or a property must be evaluated in one, but not all of the chain's states).

So I think the project was mostly a success: the basic goal of leveraging the ease of checking a Java program with JPF and the support of probabilistic programs of PRISM has been accomplished. 

Finally, if you play around with any of the code, and something goes wrong, please let me know! I'd like to think I've got a pretty stable version of the code in the end, but if you find a bug I will be more than happy to fix it.

JUnit Tests / Day 72

Today I spent the majority of the day working on making some JUnit tests for many of the methods I've written in the past months. In some cases, this was not easy as setting up a "fake" JPF instance (used in tests) so that I can properly test methods involved setting up a lot of things that I had previously taken for granted due to configuration options or default settings. But the good news is that so far, I haven't had any tests fail! So things should be working as intended, and finding more bugs really was something I was hoping to avoid so late in the program, so I was happy with the tests.

Javadoc Generation and More Cleanup / Day 71

So I noticed for Friday's post I didn't actually say what I did, so I'll just note here that it was largely more of the same: cleanup, documentation and other non-functionality related things. I'll also note that I was busy in class all day today, as well as on Thursday so I don't have a post for that day.

As for today, the goal was to generate Javadoc, maybe start writing a (JUnit) test or two, and put the example description onto the wiki, and re-do the overview page on the BitBucket page. I didn't get around to anything but the Javadoc, and since BitBucket doesn't host Javadoc (at least, not externally to the repository's copy), I've hosted them on my department website which should have pretty good up-time. The URL for the Javadoc is therefore: http://www.math.uvic.ca/~jgorzny/jpf-prism-doc/. Since this is external to the repository's version, I'll try to keep it updated but no promises that the updates will happen as quickly as the code changes. So if you want the most updated Javadoc, you can checkout the repository (or update it, as the case may be), and look in the "doc" directory (assuming I remember to keep writing comments and generating the Javadoc before each commit!).

Example (Finally!) / Day 70

Day 70 - Friday September 13th

Today I'm going to show a quick example of the kinds of output you might see when running jpf-prism. To do this, I'll talk about the Biased Die example that is provided by jpf-probabilistic (and has been copied into our repository), since this one is already publicly available. Over simplifying, the example is of a system that generates the roll of a die with some bias during computation. The computation of the roll result is done by an algorithm from Knuth and Yao in '76; the jpf-probabilistic repository describes it in greater detail, so check it out there if you're unfamiliar with it. jpf-probabilistic would display the something similar to following (taken from the jpf-probabilistic repository, note that in this case there's no bias, since the probabilities are all 0.5):

0 ------> 1
1 ------> 2
2 -0.50-> 3
3 -0.50-> 4
4 -0.50-> 3
4 -0.50-> 5 *
3 -0.50-> 6
6 -0.50-> 5 *
6 -0.50-> 5 *
2 -0.50-> 7
7 -0.50-> 8
8 -0.50-> 5 *
8 -0.50-> 5 *
7 -0.50-> 9
9 -0.50-> 7
9 -0.50-> 5 *

For this example, the property we'll check is whether or not the roll is less than 2 (i.e., a 1 is rolled).

While in jpf-prism we can do something similar, we only get an output like that if we're in debugging mode, and then we get a whole more (probably uninteresting) information, so don't expect quite that. We do display the Markov chain for our SUT, but only after we've built it, passed it to PRISM, and then queried for it. In short, this means a less pretty output for the chain itself. So what we actually get is the following:

Executing command: java -jar C:\Users\Jan\Documents\Google Summer of Code 2013\GSoC2013 Workspace\jpf-core\build\RunJPF.jar +shell.port=4242 C:\Users\Jan\Documents\Google Summer of Code 2013\GSoC2013 Workspace\jpf-prism\src\examples\prism\probabilistic\BiasedDieTest.jpf 
JavaPathfinder v7.0 (rev 1067+) - (C) RIACS/NASA Ames Research Center


====================================================== system under test
prism.probabilistic.BiasedDieTest.main()

====================================================== search started: 15/09/13 5:19 PM
a: 1
a: 5
a: 4
a: 6
a: 2
a: 3

====================================================== Exporting to PRISM
Search finished, printing PRISM's interpretation of the Markov Chain
trans: [ 0: {1=1.0}, 1: {2=0.5, 3=0.5}, 2: {4=0.5, 5=0.5}, 3: {6=0.5, 7=0.5}, 4: {2=0.5, 8=0.5}, 5: {8=1.0}, 6: {8=0.5, 9=0.5}, 7: {3=0.5, 8=0.5}, 8: {}, 9: {8=1.0} ]
Printing to dot file "C:\Users\Jan\Documents\Google Summer of Code 2013\GSoC2013 Workspace\jpf-prism\dotfile.txt"


In order to make this easier to read, I suggest exporting the chain to a dotfile, and viewing the result with Graphviz. The result is an image like the following:

Which is much easier to read than a text representation anyways. Note that there may also be more or fewer states, depending on if we can condense a chain of probability 1 transition/state pairs, or if we need to add states because a property's evaluation in the SUT becomes different and we need to track that to determine which state to pass to PRISM.

After jpf-prism outputs this information, PRISM will then compute the reachability probabilities for each of the probabilities, and that will look something like this.

Starting probabilistic reachability...
Starting Prob0...
Prob0 took 4 iterations and 0.001 seconds.
Starting Prob1...
Prob1 took 8 iterations and 0.0 seconds.
target=1, yes=1, no=5, maybe=4
Starting Gauss-Seidel...
Gauss-Seidel took 17 iterations and 0.001 seconds.
Probabilistic reachability took 0.002 seconds.
0.16666666651144624

And then JPF will finish its output:

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:00:00
states:             new=10, visited=7, backtracked=17, end=6
search:             maxDepth=0, constraints hit=0
choice generators:  thread=3 (signal=0, lock=1, shared ref=0), data=7
heap:               new=690, released=95, max live=0, gc-cycles=17
instructions:       10829
max memory:         120MB
loaded code:        classes=65, methods=1334

====================================================== search finished: 15/09/13 5:19 PM

And that's it! To verify the accuracy, you might simulate the SUT a few times to see if this value matches in practice. If you did that, the output would look something like this:

Executing command: java -jar C:\Users\Jan\Documents\Google Summer of Code 2013\GSoC2013 Workspace\jpf-core\build\RunJPF.jar +shell.port=4242 C:\Users\Jan\Documents\Google Summer of Code 2013\GSoC2013 Workspace\jpf-prism\src\examples\prism\probabilistic\BiasedDieTest.jpf 
JavaPathfinder v7.0 (rev 1067+) - (C) RIACS/NASA Ames Research Center


====================================================== system under test
prism.probabilistic.BiasedDieTest.main()

====================================================== search started: 15/09/13 5:14 PM

====================================================== Simulation #0
a: 3

...(omitted)

====================================================== Simulation #9999
a: 1
p1 was true in this simulation.

====================================================== Simulations over: results
p1 was true at the end of the simulation 1694/10000 = 0.1694% of the time.

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:01:46
states:             new=0, visited=0, backtracked=0, end=0
search:             maxDepth=0, constraints hit=0
choice generators:  thread=22793 (signal=0, lock=10000, shared ref=0), data=36708
heap:               new=4210184, released=200000, max live=0, gc-cycles=59501
instructions:       104953788
max memory:         0MB
loaded code:        classes=65, methods=1334

====================================================== search finished: 15/09/13 5:15 PM

Note that this value is pretty close to the one above, so things went as expected. And for a fair die, the probability of rolling a 1 should be 1/6 = ~0.166666..., so we have even more confidence in the answer.

Documentation & Package Separation / Day 69

Today was spent equal parts writing comments & documentation and separating the packages used in the code. Documentation wise, I added two pages to the wiki on the jpf-prism repository: one to describe the command line interface (though not yet any problems with compiling it!), and one to describe how to specify a jpf-prism property. Tomorrow I hope to put up some examples on the Wiki as well. That brings me to my second point: separating packages. Recall that I was borrowing some classes from jpf-probabilistic, and that I had copied them into our repository. However, I didn't change the package names. So while this was not a big issue while also requiring jpf-probabilistic, I'm trying to free us of that requirement by excluding it. This means in some cases changing our classes so that the correct classes are being used. This was a fair bit of work, because apparently sometimes the behaviour didn't quite copy over to new class names, opting instead to try to find old (non-classpath-included) classes. But that was fairly straightforward to resolve, even if it was tedious.  I also cleaned up a few "TODO" comments in the code, by handling more corner cases or cleaning up output.

Winding Down / Day 68

After getting settled into my new program, I'm back to concentrating on this project. I hadn't really meant to put this aside last week, but the first week was full of classes and orientation sessions to sit in on, so I didn't have any real time to work on this. That being said, I'm back to nearly full concentration on this project, though it's unfortunate that this week has to be used in order to prepare for the pencils down portion of the program. That being said, I'm definitely planning to continue working on the project after the Google program ends, but this pencils down period must still be observed.

Today was spent doing things towards exactly that end. The day started with an early Skype meeting, which outlined some tasks to be done before the pencils down deadline. First, there was some issues with compiling my wrapper script, so I may look into simplifying that further, but it's not a big priority. Second, an issue regarding properties which I thought I had fixed resurfaced; I think I've got it fixed for sure this time, but only future testing will confirm this. Third, much was discussed about cleaning up the code, documentation, and other things that need to be done that I've been putting off.

To that end, the wrapper lacks a "-debug" option, that I've put in. I'll put out an "official" guide for command line calls to it on the page tomorrow, as well as a description of how to specify properties.

I've also started actually cleaning up code and separating anything from other packages (like jpf-probabilistic) and removing classes that aren't used anymore. And code documentation needs to be updated for most of the code, and so I spent some time doing that as well.

Simulating might still have a bug too, as during the meeting an attempt to simulate the BiasedDie example didn't terminate quickly. Might just be due to the Math.Random native peer enumerating too many options. I'm investigating. Along with that is checking various properties to see if they converge to values suggested by the PRISM output for the probability of the property being true. I'm not going to compile a formal report of these examples, but I'll probably make a spreadsheet and describe them here on the blog.

Multiple Updates / Days 62-67

Day 62 - Wednesday August 21st
Again, looking at the Random native peer from JPF. I was under the impression the whole day that I had to write a new ChoiceGenerator to invoke the peer, or methods from it, but this doesn't seem to work, and it seems that my code doesn't quite like accepting new ChoiceGenerators, so I'm not sure this is the way to go. I was also looking at modifying search classes to work with Random calls, but that seems even harder. I'm still committed to getting arbitrary Random method calls to work though!

Day 63 - Thursday August 22nd
Today was another Skype meeting, and I didn't do a whole lot prior to it. The meeting was quite productive I think, serving at the very least to alert me to some bugs in the code that I was not aware of (always fun to have during a demo situation!). In addition, installation seemed to be a bit of an issue so I also resolved to test the installation (and functionality) on Mac and Linux systems, though I don't have access to the former. I might be able to use a Mac when I start up studies again in September, so I'll keep this in mind. I did install things on my Ubuntu installation, and all seemed to go well. I had a few environment variables not set on another Windows install, but beyond that it did seem to work well on a fresh install (though I may have done something to ease the process without knowing it).

Beyond the demo-related incidents, the meeting served to discuss the code I had worked on the previous week, and we certainly cleared up some issues. There was a lot of talk about getting the Random calls to work and that seems to be the best way to go. Also a small issue of where properties that don't have a location specified are checked. For ease of use, I'll also develop a wrapper to automate .jpf file creation and calls to JPF.

Day 64 - Friday August 23rd
Random() method calls work! The fix was extraordinarily easy too: a parameter passed into the configuration, and a few checks to see what ChoiceGenerators are already registered to JPF when using those options. Then it was just a matter of finding the right one(s) and getting the probabilities out of them. I'm very glad that was accomplished.

Moved to Victoria between these days!

Day 65 - Monday August 26th
Today was a bug fixing day -- as I mentioned above, the Skype meeting revealed some deadly bugs that I had to squash, and they were a welcome change from looking at native peer code all day.

Day 66 - Tuesday August 27th
After fixing the bugs, I was confirming behavior should work as required, and I started by looking at where properties that are specified but never marked with a location (using a method to specify where in the code) are marked to be checked by PRISM. They were supposed to be checked at end states, but somewhere during the last few weeks that must have been changed, and they were not. Sadly (and rather unproductively), I spent the day working on fixing that.

Day 67 - Wednesday August 28th/Thursday August 29th
To sum up today: clean up. Specifically, testing, translation fixes, and a wrapper class for use by command line users. The examples provided were a mix of Java programs and C programs as I've said; the Java ones work, but the C ones did not, largely due to my translation to Java. I think I have some of those working now too though (though since some functions are defined in libraries I external to the provided code, they may not be truly correct; I need to confirm some of the implementations). Regardless, there was work to be done cleaning up things and using Random calls instead of Choice calls.

Beyond that, I developed the wrapper class for command line calls. The idea is to simplify use and avoid having to create .jpf files. For example, instead of having to create a few lines to run the simulation-aspect of the code, a user can now simply run

jpf-prism-run -simulate [-d:dotfilepath] -n class propertiesfile 

from the command line (after appropriate environment variables are set, as I think will always be necessary), where n is the number of times to simulate the specified class (which must contain the main method to run) with the properties contained in the propertiesfile. Generating a dotfile can be done using -d:dotfilepath to specify a file to output it to. "Standard" (non-simulation) verification is even easier:

jpf-prism-run [-d:dotfilepath] class propertiesfile

where the user no longer has to specify watched variables: only those in a property will be watched.