Expressions for Properties (Part II) / Day 45

Day 45 - Monday July 29th

Today I was working on getting transitions to break on the evaluation of Java expressions, as mentioned in the last post. The back-end code was in place and all I had to do was populate a symbol table of watched variables in order to see when the expression’s Boolean value changes.  Although this was simple, I have some concerns regarding whether or not to change JPF’s state (i.e. modify the search class that is in use) or track state externally again (more complicated). I have opted for the first.  Still some minor corner cases to handle, but on the whole this is looking pretty good. On the administrative side of the program, I also wrote up a draft of the midterm evaluation, and I’ll revise it and upload it (to Melange) tomorrow.

Parsing Fixes & Expressions for Properties / Days 41 - 44

Day 41 - Monday July 22nd & Tuesday July 23rd
I'm splitting this work day in two because I was fairly distracted again: on Monday I was finding an apartment (which I did!) for my upcoming move, and Tuesday was a half-day trip to the dentist. So I will have to make up a day of work.

Anyways, what I did work on was to see if I could parse more interesting state/property descriptions. The initial parser I had written was sloppy and didn't quite work as well as I had initially thought. So I spent the day re-writing this; I'm still not particularly happy with it (it's not a standard LALR parser, so it's likely slower than other existing parsers, like SableCC.), but it will do for now, and it parses based on variable/value, as opposed to state number. That is, we accept markov.properties="[](<> \"x.y.outValue:5\")"), type properties. That being said, although it parses better, I'm not yet doing anything with the property: I'm still checking nothing related to it. But the parser did need the fix, so this was the first step.

Day 42 - Wednesday July 24th
Today the day was started with a demo of the code and an outline of it to my mentors on Skype. The talk was very helpful and productive, and suggested many changes to the code and outlined a concrete direction to take for the immediate next steps of the project. There were some small changes that were easily fixed: moving some classes to the appropriate packages in the source and moving a parameter from the .jpf files to the jpf.properties file. Easily done. Only slightly harder was building the Markov Chain in PRISM on-the-fly (as opposed to when the search was finished), and that too is now implemented. This should reduce our memory footprint when checking models. The system can now also export the Markov chain in a DotFile for use with visualization with Graphviz. The most interesting ideas were the next steps: to get the the properties that we're interested in checking to be represented not as states, or particular variable values, but rather to be handled as Java expressions. Further, we could use these expressions to break transitions (or not) and use this to also trim the search space. The rest of the day was focused on introducing myself to the tools I was suggested as a starting point: the PreCondition class from the gov.nasa.jpf.symbc.numeric package.

Day 43 - Thursday July 25th
Today was more looking at using expressions as properties. The class listed in yesterday's entry is interesting, but unfortunately, the code itself (as well as jpf-symbc, where it comes from), doesn't compile. Instead of debugging someone else's code (again), I copied the relevant code, repaired those files (much quicker than getting the whole project working, I imagine), and I'm going to implement on top of these--which are already well coded. I managed to get the code recognizing the expression, which is step one. Next, I need to augment the code so that it breaks transitions when the value changes.

Day 44 - Friday July 26th
Today I was working towards more than just parsing of the new property syntax. In particular, in order to use the expressions I need to have a working system to access them and check their values during transitions, to determine if it needs to break into a new state or not. There was a fair bit of work to implementing this, and although I'm not done, I think I'm close. All the appropriate classes seem to have all the necessary information, I just haven't been able to access it all in the right way from what I can tell. But I have some ideas and I think this should be relatively easy--I'm expecting to spend no more than half a day on it on Monday.

State Reduction / Day 40

Day 40 - Friday July 19th
Today most of the work was again centered around the idea of reducing the number of states that JPF creates. There was a simple fix: I was not checking the relevance of the store instruction in the right spot. The idea is to break transitions only if the store instruction is storing into a watched variable (since now that we have a list, and won't print the other variables anyways, it makes no sense to break on all store instructions), but I was breaking all instructions, then checking to see if I should record the data--this was backwards. This put the state count at 15. I think I'm going to leave this issue alone for a bit (or ask around as to possible causes), because after looking at the code for 2 days I still don't have any other ideas, and it's pretty close to optimal. I can revisit this after a break, or if I get some new insights.

Misc. Fixes / Days 37 - 39

Day 37  - Tuesday July 16th
For the most part, state inference is complete: JPF will create a state every time a variable changes, and the code provides descriptions of the variables (that it has been instructed to watch) in that state. And of course we also know the transitions between the states, so we have a good idea of what the code in the SUT is doing. With this in mind, there were some small issues alluded to in the last post that needed some work, and most of this work has been bug-fixing, or cleaning up corner cases, or re-factoring code. Relatively small tasks that when combined, should allow for more interesting programs to be checked.

First on the list was to get the property we want to check in PRISM from the JPF configuration file. This wasn't a terribly difficult thing to import. The harder part came when trying to parse the property to get PRISM to then check for this particular property. What I did was to implement a basic parser and then invoke specific commands in the PRISM code to check various properties, based on the LTL syntax. I did this in a manner very similar to jpf-ltl, but whereas jpf-ltl annotates properties on methods in the SUT, for example,

@LTLSpec("[](<> \"done()\" && <> \"foo()\")")
public class AlwaysDoubleEventuallyFinite2 { ... }

we expect ours upfront, and phrased in terms of states, rather than methods:

markov.properties="[](<> \"state:5\")")

A current downside for this implementation is that since I'm requiring the property to be phrased in terms of system states, it currently requires two-passes to check a property: a first pass for the user to understand the states, and then a second to add a property phrased in state numbers and check it again using PRISM. What I want this to evolve into (since the checking so-far is mostly variable-centric) is to replace states with variables and values, for example:

markov.properties="[](<> \"x.y.outValue:5\")")

I think this is more flexible than jpf-ltl's technique of phrasing properties in terms of method calls (as method calls could return values as well). But I left this to another day. (And if we did want method calls in our properties, it's now easy to add them given that the underlying parsing has been implemented.)

Beyond this, I also wanted to support local variables. Currently, the way to specify what variables to watch uses JPF's pattern of package.class.variableName so that when JPF was matching variable names that it extracted during instruction executions, it could match them directly (they were extracted following the same pattern). I thought this was okay, but since we're also keeping track of all the methods being executed anyways, why not also track local variables (noting, that I'm putting off the issue, for now, of what should happen when a variable goes out of scope). So my pattern, package.class.method-methodName.localVariableName was introduced so that my code would identify when a local variable was also to be observed, in order to watch for entering and exiting of those methods, and look for those variables as well. When the variable is out of scope in a state, that variable is flagged in that state description as such.


Day 38 - Wednesday July 17th
In addition to supporting local variables, one of the issues I had pointed out in the past was that when store instructions were executed, array stores were not supported: the store would read as  "?[0] = 1", which meant that I had no idea what what array was getting this value. I decided today would be a good day to look into this issue. This was a bit tougher than the last issues, and I'm not actually sure that I got anywhere. I think the solution is to build my own symbol table as JPF executes stores & loads with respect to arrays, and then track the addresses, and use those to look up the name and replace the "?" in the output above. However, that was a fairly daunting task that I couldn't complete without spending more time on (and even then, maybe not), so I put this off. I found a quick hack that will work for smaller systems; in particular, systems with at most one array variable: we can take the name of the array in the configuration file, and use that to descriptions of the array in the state descriptions (which really just adds readability). For 2 or more arrays, I still wouldn't know which is which so I couldn't make any improvements there. This is marked as an issue to revisit.

Still, the code feels much more complete and much less a prototype--though I'm sure it still is.

Day 39 - Thursday July 18th
Today's goal was to see if I could be more clever with respect to transition optimizing, thus reducing the number of states JPF generates. For example, many of the "21" states are empty states, that don't appear to change anything important in the system state, and just lead to another empty state. I found one source of this (a missing if-statement in the executed instruction method of my listener), and we dropped 3 states, but the source as to why so many other states are happening. I know from my listener there aren't more than a handful of additional changes (5) to variables in a state beyond those that caused the initial 8-state chain in the BiasedDie example listed on this blog much earlier (and as an example on the jpf-probabilistic page). So getting this down to 18 was good I suppose, but I would have liked to narrow it down to the (suspected) minimal of 13, or find an explicit reason as to why I cannot do that.

Inferring State (Part XI) / Day 36

Although I think I have a working system for state inference in jpf-prism, I don't think it's perfect yet (those small technical details have yet to be resolved, and I'm still not sure about scalability). One of the ways I might get to a better system was to ask my mentors. You might recall that one of the big issues with JPF "state" is that a variable can occasionally take multiple values in a state because JPF's search can choose to re-use an old state and update the value of a variable within it. I had corrected this by recording these changes to the state as "substates", which are nice because they are external to JPF's notion of state (and thus also to notions of state as recorded by, say, jpf-probabilistic, whose search mechanism we're using for the moment). So when we get a Markov chain out of JPF using this code, we see what we would expect: the Markov chain for the examples has the appropriate number of states, but also, we have what my code outputs: the details of the substates, and if a transition comes from a state with substates, we also know what substate it comes from--but if you don't care about this much detail (as in the case with jpf-probabilistic), you can ignore that.

The alternative is to change how the search object classifies a new state: make it so that any change in variable is a new JPF-state, and then proceed as before by using breakTransition() (a method in the VM I was unaware of until today). This is the method that is used by jpf-ltl, which was suggested by one of my mentors. This approach is probably safer, but it also might lead to confusion: if you're expecting a particular Markov chain, you might get one with extra states as no state will be reused, and so every variable change corresponds to a new entry in the chain. This method is what I was implementing today, and I think I had some good success--though I want to check it in greater detail tomorrow, and I'll need to modify it a bit still. I would have been done today, but some of my printing methods failed under the new state structure and I have to repair them a bit still. And there's optimization to be done: using the breakTransition method I was initially getting 33 states instead of the usual 8--I'm sure I don't need to break all of these transitions. Since then it's down to 21 (since some memory stores don't actually matter, for example, class loads). I think I can do a bit better still.

Further, borrowing ideas from jpf-ltl, I am also implementing ways of flagging certain variables to watch, or consider important during model checking, in addition to specifying a property before hand so that we can pass it through to PRISM--which will likely be necessary unless we're going to be generating all of the properties we're going to be checking in PRISM. This is not yet done, but it's not hard: maybe another hour of work tomorrow.

Inferring State (Part X) / Day 35

Day 35 - Saturday July 13th
Despite the successes described in the last post, I had omitted some other small flaws. Particularly, if a single instruction changes the state of the system, and we're only looking at that instruction, then at most we've noted one variable has changed and we're in a new state. But if that is all you look at, then when you get into this state and start recording variable values, you find only the one that has changed. So you're (probably) missing a lot of information. This can be resolved by identifying the prior state, and importing or inheriting all the other variables with their unchanged values (if they were changed, you would have observed a new store instruction). That's what I implemented today.

Still, not everything is perfect: if a variable goes out of scope from one state to the next, the code will currently import that variable and its last value anyways. Further, the method for tracking the store instructions does not seem to support even primitive typed arrays.

Inferring State (Parts VIII & IX) / Days 33 & 34

Day 33 - Thursday July 11
Today was spent implementing the ideas of the last post: the idea that within a certain state, a choice generator may be invoked several times, and that this results in transitions from a state to itself. This was not entirely correct, from the looks of it: the transitions can go back to a similar state, but the choice generator won't make a new choice for that particular choice call--it will execute the program in this state until a new choice is necessary (which may be the same choice). For example, consider the following code:

if(makeChoice()){
   variable = 1;
} else {
   variable = 2;
}

In this case, if the choice returns true so that variable is set to 1, then that might cause JPF to create a new state, where variable takes on a value of one (and of course, the search object determines when a new state is created or when one is re-used). If the choice returns false, then the variable is set to 2, but in this example, this would likely not create a new state--JPF (or, rather, the search object) will reuse the state that it was in before reaching the branching code.

So basically, looking at probabilities does not define the abstractions over the state variables (there are none) or the set of possible values, but it does provide the probabilities for these transitions, so it's still useful to get this information from the Probabilistic search object.

Day 34 - Friday July 12
Despite the ideas changing a bit in the last few days rather quickly, I always kept in mind that the end goal was to make sure that in a given JPF state, we also have the explicit state of the variables, as well as the transitions between states, and the probabilities that each transition was taken. The transitions were easy; the states a bit harder. The transitions, as alluded to in the last couple of posts can be exactly determined by the Probabilistic Search object and the listener's we're already using. The states were harder: defining what they were was hard: there's no way in JPF (at least not one that I know of) to ask it what the value of a variable in the SUT is in a given state (that would be a great extension!). So instead you need to track them by observing the instructions that JPF executes, looking out for the store instructions that modify a variable's value, and record those. And you need to make sure you're aware of when the state changes, and what it changes to. A small hiccup comes when it's realized that although instructions are executed in a transition, a transition doesn't know what state it's leading to until it completes and the search object tells the VM. So you need to store the result of the execution outside of the transition or the VM and then clean it up by putting those results in whatever state you now know you're in. I'm a bit concerned this will lead to greater memory bottlenecks, but for now it works.

The upside of monitoring instructions like this is that every explicit state of the SUT can be monitored: anytime a variable changes, we're aware. So that means when a state changes it's values, we can choose to either keep this information as a set, for example in state X, we know variable a = {1, 0} for exactly one of these values, or we can generate new (non-JPF-SystemState) "sub-states" that make it explicit: in state X, variable a = 1, but in state X.1, variable a = 0. The "set" method was in use early in the week but I wasn't satisfied, so now jpf-prism works with the latter system. The benefits of this is now that I track that a transition from a state to itself changes a variable in that state (and how it changes), but also if a transition into or out of state X is from anywhere in X, or in exactly X.Y (some substate). So now I exactly know the execution trace of the SUT. The disadvantage is that I'm storing much more information: in addition to tracking what state preceded another, I also now store a new substate for every value a variable can take. This will undoubtedly increase memory overhead.