Inferring State (Part V) / Day 30

Today was a productive day: some important lessons were learned. First, return values from methods that are not also stored in a variable are not considered by the JPF VM to be a StoreInstruction. This means that I was looking for variables to take the values that methods, like roll(), would return. I couldn't find them, and then I realized this was the case. I modified the BiasedDie example to assign the return value to a variable first, in order to check it better—but this may not be the case in arbitrary code. I’m mentioning it here (as well as making it an issue) so that I look into it later. Second, and much more concerning, I discovered that variables can take on different values in the same JPF state! So I was initially looking for a specific value for each variable in each state, but that’s not the case. This is a bit disconcerting, as it means I’m not doing enough to determine the “state”. I need to do more than look for specific values: I need to look into how JPF characterizes or abstracts a state, and find a way to transfer that to PRISM. That seems much harder, and I left it to tomorrow. Today, code-wise, I did get VarRecorder to work, and now I have a small hash table of states, variables, and their possible values. With this, and a bit of work, I could probably transfer this information to PRISM. I’m concerned that the hash table will not scale well, but I want to get past this problem, so for now I’m going to run with this and find some time to do scalability testing. I figure that if it doesn't scale well, I’ll see if I can pass state information into PRISM directly and on-the-fly, so that scaling is only limited by PRISM’s capabilities: one that I wouldn't be able to overcome anyways.

Unfortunately, as I’m writing this, Toronto has suffered severe storms bad enough to cause some minor street-level  flood downtown (not near me), but worse, to knock out power in many areas: myself included. I'm posting this a day late now from a coffee shop: the next post might also be similarly delayed.

Inferring State (Part IV) / Days 28 & Day 29

Day 28 - Saturday July 6
Today I was working on inferring state again. I was a bit surprised to find that in the JPF listeners directory, there are two, VarTracker and VarRecorder that appear to do much of what I was trying to do before (certainly these do what the goal of the code for Day 26 would be re-purposed for in the future), and they do so much better than I could probably do it. I'm rather quite happy that I found them: they don't solve the entire problem, but I think they're a good start. Of course, they don't work with our test examples yet: debugging & configuring them is the goal here. But I'm hopeful, and I think as long as they do work, I'm going to use them to track state in an internal state and worry about scalability later--I think any method would require something like this anyways, and we can possibly prune what we store later in order to handle larger programs.

Day 29 - Sunday July 7
Today was more debugging/configuring with the two listeners described above. Not a whole lot of luck: VarTracker was easy to change, but it doesn't actually report on the variable values: it only deals with when (with respect to what state) a variable is changed. VarRecorder on the other hand, will say explicitly what the value is, so this is the one I want to get working, but no luck yet.

Inferring State (Part III) / Day 27

Today, instead of toying around with methods to see what information I could extract from the JPF VM, I decided to take another route: to modify the ChoiceGenerator object, so that we could possibly use older methods (tracking all variables) in a smarter manner. In particular, I modified the ProbabilisticChoiceGenerator so that we can find out the last choice it made. Using this, we can query all variable information like listed two days ago (method #2), but we only need to do this once, and then we can just track changes based on the choices made. I'm under the impression that this is quicker than the alternative, at the very least, we can use both and we can track the choices for other purposes, if we need them. Of course, it's still not optimal: if the choice generated leads to other variables changing (as it almost certainly would), then we're still going to need to look for these variables changing after the choice generator returns. But maybe we can calculate dependent variables by pre-processing the code. Again, not optimal, but perhaps more clever. I'll look into it more tomorrow.

Inferring State (Part II) / Day 26

Today I was continuing in the spirit of finding out what state corresponds to which label that jpf-probabilistic returns. The first thing I noted while looking through code was a method getStateDescription() for ThreadInfo objects, and while I didn't get my hopes up, I tried it didn't work: it returns the state of the thread. Really, no surprise there--but I thought I'd mention it in case anyone was to point it out. Simply too good to be true. Instead I was looking at the VMListener interface in JPF. It seems to implement several methods that can be used to track what goes on during verification (expanding on the ideas of the last post). I fear it might be too detailed: many methods involve threads, which probably isn't terribly important for determining what state the system is in. I wrote up a quick  implementation of the interface, but I'm not sure it'll be useful on it's own--it's got a lot of information, but I'm still not sure what I'm looking for until I settle on a method for determining state. That being said, it'll be useful in future code I'm sure. I'll be exploring more ideas tomorrow.

In addition to the above, I set up bug-tracking (and/or issue tracking) that uses FogBugz. I realize BitBucket had it's own issue tracker, but I wanted something that I could save tasks by directly using Eclipse plug-ins, and Mylyn supports FogBugz. I'm not entirely sold on it yet: I want the issues to be public ideally,  as this is an open-source project, and FogBugz doesn't seem to allow me to do this (though it's possible that anyone with a FogBugz account might be able to see them, but still, hiding them behind a log-in is not something I really like the idea of). I may switch to Bugzilla if I find out it can do that (and I find/set up a host). The bigger issues I'll also list on the BitBucket issues page.

And in case you didn't see it yesterday (I forgot to mention it in the blog), I've updated the Wiki on the jpf-prism page. It's not much, but it has the installation instructions now, and a few other obvious links. It's nice to have a place to put text that might be useful beyond the lifetime of this blog.

Inferring State / Day 25

Today's goal was to determine what state is referenced by each integer label returned by jpf-probabilistic. To this end, there were a few methods that could possibly do this. First, and easiest, but probably also least useful, was to augment the listener to look for specific variables within the code. However, there are drawbacks: 1) it appears you can only target variables at the class level (that is, variables defined in a smaller scope, say within a Java method, cannot be targeted through this method); I could be wrong, but the FieldSpec documentation in JPF didn't seem to support more than this, and 2) you need to know the variables beforehand so that you can manually enter them into the .jpf file you are verifying (this could be mitigated by writing a tool to look at the code and add all of these to the .jpf file, but it seems like this much work is not ideal before verifying arbitrary code). Second, and perhaps even easier, is to have JPF report on all variables as they are updated, and keep an internal representation of their values. This could get complicated (especially for large programs), and it has the added downside of also reporting system variables that are called, so this is not optimal. Some combination of the two might be best, or the second method with some filtering. I think for this to work (easily), we may need to pre-process the code that we want to verify and pass that to the listener so that it limits its work, or find some way to target only some classes/methods/variables--I feel like this might very well be possible, but I need to look into it more. I'm going to look into more methods tomorrow as well.

Model Properties / Day 24

Today I was working with checking model properties on JPF-generated Markov chains in PRISM, and trying to infer state from a given example model. The first task was relatively easy: it looks like just an appropriate set-up of the property, and the appropriate method call. The result is a bit messy: I'm toying around so I didn't make JPF publish it appropriately, so the console output is a bit out-of-order. I'll fix that tomorrow. And I plan to revisit properties: they seem easy enough but I want to run more of them to make sure things work properly and to ensure I'm setting them up correctly. Additionally, since the actual state of a model will likely be of interest, I spent a fair bit of time thinking of how to infer the state of a model (jpf-probabilistic currently only returns states with an integer label so far (and I'm not sure if the integer has any significance). I think the JPF vm can be very helpful here, but I haven't been successful here yet (and I'm not sure what degree of state inference will be considered successful--being aware of all variable values? That's the first thing that comes to mind for me). Tomorrow I'm going to talk more about this. And I also set up a blog post on how to install and run my code.

Installing jpf-prism

In case you were interested in running jpf-prism while it is under development, this blog post will tell you how to do that.

What you'll need: Eclipse (possibly with Mercurial and SVN), jpf-core, jpf-nhandler, jpf-probabilistic, PRISM (built from source), and of course jpf-prism.

First, if you need to install JPF, download and build jpf-core, which is available here via Mercurial:  http://babelfish.arc.nasa.gov/hg/jpf/jpf-core. If it asks for a version, take the "default" version (not v6), as the system is being developed for v7 which is default as of June 22nd (see here). Build the project, and then install the JPF Eclipse plugin and set up your site.properties file.

Second, download and build jpf-nhandler from the following Mercurial repository: https://bitbucket.org/nastaran/jpf-nhandler . Make sure that you modify your site.properties file to include it as described on the BitBucket page.

Third, download and build jpf-probabilistic from the following Mercurial repository: https://bitbucket.org/discoveri/jpf-probabilistic . Again, make sure that you modify your site.properties file to include it as described on the BitBucket page. (Note: since the interesting classes we're using in jpf-prism have been copied into jpf-prism, this might not actually be necessary, but I'm including it to be safe.)

Next, download the source for PRISM, build it (for the C/C++ parts), and set it up for Eclipse as described here (you can also get it from SVN). Then make a new a project in Eclipse and import the prism directory (as described in the last link) and build it again (for the Java files). Then add a variable, say prism-jpf, to your site.properties file pointing to the classes folder of the build, for example: prism-jpf = ${user.home}/GSoC2013 Workspace/prism-jpf/prism/classes/

Lastly, download and build jpf-prism, which is available  from the following Mercurial repository: https://bitbucket.org/jpfprism/jpf-prism . Add jpf-prism to the site.properties file, for example: jpf-prism = ${user.home}/GSoC2013 Workspace/jpf-prism (or wherever your jpf-prism project is located) and adding ${jpf-prism} to the extensions variable.

Now you should be ready to go! To test the installation, try using JPF to verify the BiasedDieTest.java by creating BiasedDieTest.jpf and putting the following in:
@using = jpf-nhandler
target=probabilistic.BiasedDieTest
classpath=${jpf-probabilistic}/build/jpf-probabilistic-examples.jar
native_classpath= ${prism-jpf}
listener=prism.listener.MarkovExporter

Then run JPF on the .jpf file. And that's it. If there are any concerns or comments, please feel free to contact me.