Day 60 - Monday August 19th
Today, I was running more experiments while also looking into the jpf-core version of the Native Peer for java.util.Random(), which of course I was not aware of last week! From the looks of it, it would not have been particularly helpful for the current translations, as it is almost too powerful for the work around that was implemented. But this of course might be better. I spent some time looking at it, and seeing if I can use a modification of it to make translations even more straightforward, or to require to no translations at all. That would be really nice. No progress there yet!
(And I know I said results today, but I was distracted. They will be ready very soon!)
Day 61 - Tuesday August 20th
Today, I was looking at the jpf-core implementation of Random again. I haven't made a whole lot of progress, but I would really like to get this version working, with at least the simulation aspect of the code. The idea of not having to translate many Java programs is just too irresistible, and I feel it will make the the code much more easily usable. I think the problem is that the class tries to enumerate all random choices, and this causes the run-time to sky-rocket, although in most cases we only need a small subset of all possible random choices. And I don't yet know how to control this behavior. I spent some time cleaning up the code just as a change: there was a fair bit of dead code, old comments, and not-commented code, so I cleared many of these issues.
Wednesday, August 21, 2013
Monday, August 19, 2013
Approximating results listener / Days 58 - 59
Day 58 - Thursday August 15th
A new listener made up much of today's work, and the idea is observation only. The listener is not meant to interfere with choice generation at all, but rather to run the SUT as if the JPF VM was any old Java VM, and have it run it's course. Then it looks to see at given times (or at the end of the run) is a given property is true or false (e.g. through a new method similar to others added this week: EvaluateHere(String propertyName), and similarly for many properties). Then it records this information, and then runs it all again, and again, up to a given bound, to see how many times each property was true or false, and reports this. Today was the start of that listener (which for the most part is a re-purpose of VarRecorder, with some changes), but unfortunately not the end of it.
Day 59 - Friday August 16th
Friday was a continuation and completion of Thursday's work. It looks like I've got the listener running the way it should, and I spent a bit of the day testing it, and comparing results with that of results from earlier runs. I also toyed around with the notion of letting it run the SUT for as many runs as it can before X minutes pass, but I wasn't really successful there.
I was also updating data for all the examples and I still had some larger examples to try that I'll just leave running at various times over the weekend so that I can get some really interesting (read: larger size) scalability results, and possible track memory usage in addition to time), so that I can pass off that report/spreadsheet I mentioned earlier. Expect that Monday (though probably not on this blog!).
A new listener made up much of today's work, and the idea is observation only. The listener is not meant to interfere with choice generation at all, but rather to run the SUT as if the JPF VM was any old Java VM, and have it run it's course. Then it looks to see at given times (or at the end of the run) is a given property is true or false (e.g. through a new method similar to others added this week: EvaluateHere(String propertyName), and similarly for many properties). Then it records this information, and then runs it all again, and again, up to a given bound, to see how many times each property was true or false, and reports this. Today was the start of that listener (which for the most part is a re-purpose of VarRecorder, with some changes), but unfortunately not the end of it.
Day 59 - Friday August 16th
Friday was a continuation and completion of Thursday's work. It looks like I've got the listener running the way it should, and I spent a bit of the day testing it, and comparing results with that of results from earlier runs. I also toyed around with the notion of letting it run the SUT for as many runs as it can before X minutes pass, but I wasn't really successful there.
I was also updating data for all the examples and I still had some larger examples to try that I'll just leave running at various times over the weekend so that I can get some really interesting (read: larger size) scalability results, and possible track memory usage in addition to time), so that I can pass off that report/spreadsheet I mentioned earlier. Expect that Monday (though probably not on this blog!).
Property locations, native peer execution and examples (again) / Days 55 - 57
Day 55 - Monday August 12th
Let me start the blog post by quickly adding that during the Skype meeting last week we also spoke about one other issue: tracking not only when a property becomes true or false, but where it does so: that is, tracking the location in the program where this could happen, as well as being able to ask jpf-prism not about about an expression, but an expression being true at a given line of code in the SUT. This is what I started off the day implementing, and I think it went well. The idea I used here was to give each property in the .jpf file a name (so that the syntax is name: expression), and then to add a JPF utility class with static methods PropertyIsTrueHere(String propertyName) and PropertyIsFalseHere(String propertyName) that the SUT can call at the appropriate code location with the name of desired property passed in. Then jpf-prism will look at method it enters, and if it's one of these, it'll flag the state and pass it to PRISM for the appropriate checks.
The rest of the day was committed to the native-peer programming. The issues I had were largely technical, and were overcame today, so it was a pretty good day; I'll omit the details, and instead talk about the solution. The idea was that the Choice class was unable to re-size its arrays dynamically for the SUT, and so translations were rather difficult (or at least tedious). In order to fix this, I created a new method in the Choice class that not only gets a random choice from an array of probabilities, but then also returns a new probability array with the choice removed, and the probability of that choice uniformly distributed to the remaining entries in the array. This way a SUT can use a dynamically shrinking probability array much more easily (two lines for every random() call, instead of the previous five or size). But beyond this, there might be other situations where you need to change the array, so I also created a few other methods: for example, if you're only making the call on one such array (that only shrinks throughout execution) we can further reduce this to a single call that will do the same thing as above but with a single call after providing an initial array to the peer. Or if you need to change the probability of the resulting array with a bias, there's a method to do that so that the new array returned is modified with a bias (supplied as an array) added to the appropriate terms (though in this case it's up to the SUT to make sure the probabilities sum to 1).
Day 56 - Tuesday August 13th
Today was spent dealing with examples again. This was also a good test of the new native peer code, but I was looking more to dealing with issues of scalability. Again, examples are not yet public, but one deals with dealing random playing cards out, and for small deck sizes (< 6), the code returns almost instantly, but for larger values it does take a fair bit longer, for example a deck size of 8 took about 30 minutes, and 7 was somewhere in between. I'm hoping still that might be because I'm not correctly abstracting states, but at this point I'm not so sure. (And in case any one is wondering, the PC I'm using is an Intel Core i7 2.8Ghz with two cores and 8GB of RAM on Windows 7, so while it's not the best, it's not a slow system.)
Day 57 - Wednesday August 14th
Today was more dealing with examples; I'm compiling a report of the results to send to the mentors, but I also had to re-do some of the translations I had done last week. And there were a few more issues with my code finding bad indexes or null pointers, so I had to make a few fixes, change them, and re-run all the results again.
Additionally, I updated the PropertyIsTrueHere (and similarly, false) to support many properties at once: PropertiesAreTrueHere(String[] propertyNames), just for convenience.
Let me start the blog post by quickly adding that during the Skype meeting last week we also spoke about one other issue: tracking not only when a property becomes true or false, but where it does so: that is, tracking the location in the program where this could happen, as well as being able to ask jpf-prism not about about an expression, but an expression being true at a given line of code in the SUT. This is what I started off the day implementing, and I think it went well. The idea I used here was to give each property in the .jpf file a name (so that the syntax is name: expression), and then to add a JPF utility class with static methods PropertyIsTrueHere(String propertyName) and PropertyIsFalseHere(String propertyName) that the SUT can call at the appropriate code location with the name of desired property passed in. Then jpf-prism will look at method it enters, and if it's one of these, it'll flag the state and pass it to PRISM for the appropriate checks.
The rest of the day was committed to the native-peer programming. The issues I had were largely technical, and were overcame today, so it was a pretty good day; I'll omit the details, and instead talk about the solution. The idea was that the Choice class was unable to re-size its arrays dynamically for the SUT, and so translations were rather difficult (or at least tedious). In order to fix this, I created a new method in the Choice class that not only gets a random choice from an array of probabilities, but then also returns a new probability array with the choice removed, and the probability of that choice uniformly distributed to the remaining entries in the array. This way a SUT can use a dynamically shrinking probability array much more easily (two lines for every random() call, instead of the previous five or size). But beyond this, there might be other situations where you need to change the array, so I also created a few other methods: for example, if you're only making the call on one such array (that only shrinks throughout execution) we can further reduce this to a single call that will do the same thing as above but with a single call after providing an initial array to the peer. Or if you need to change the probability of the resulting array with a bias, there's a method to do that so that the new array returned is modified with a bias (supplied as an array) added to the appropriate terms (though in this case it's up to the SUT to make sure the probabilities sum to 1).
Day 56 - Tuesday August 13th
Today was spent dealing with examples again. This was also a good test of the new native peer code, but I was looking more to dealing with issues of scalability. Again, examples are not yet public, but one deals with dealing random playing cards out, and for small deck sizes (< 6), the code returns almost instantly, but for larger values it does take a fair bit longer, for example a deck size of 8 took about 30 minutes, and 7 was somewhere in between. I'm hoping still that might be because I'm not correctly abstracting states, but at this point I'm not so sure. (And in case any one is wondering, the PC I'm using is an Intel Core i7 2.8Ghz with two cores and 8GB of RAM on Windows 7, so while it's not the best, it's not a slow system.)
Day 57 - Wednesday August 14th
Today was more dealing with examples; I'm compiling a report of the results to send to the mentors, but I also had to re-do some of the translations I had done last week. And there were a few more issues with my code finding bad indexes or null pointers, so I had to make a few fixes, change them, and re-run all the results again.
Additionally, I updated the PropertyIsTrueHere (and similarly, false) to support many properties at once: PropertiesAreTrueHere(String[] propertyNames), just for convenience.
Tuesday, August 13, 2013
Examples and clarifications / Days 51 - 54
Day 51 - Tuesday August 6
Today I was working on making sure that the examples worked in more than just a syntactic manner. And, unsurprisingly, they did not. There were several issues discovered across the examples, some of which are most like bugs in my code, others that are slightly more fundamental, and a few that may just be translation issues. Since the examples are not public, I won't talk about the specific issues in each example, but try to summarize the high level concerns. First, ignoring the issues that I think are related to my code functioning properly, there are issues translating arbitrary random codes: they each have their own notion of random(), which makes translation difficult, and in some cases, impossible, at least without further changes. In particular, for each call that should return a new "random" number, or get one from a choice, we (JPF) need a native-peer to execute, so that we (specifically, our choice generator class), can see what choices were possible, and what was made, to exhaustively check choices correctly. So a Java program calling just calling random() needs to be modified, so we know what the context is, and what the options are (that make sense). So we need something like jpf-probabilistic's Choice class, that is executed on the JPF side so that everything works. In some cases, we can use this class, but that also causes other issues: we need to know the possible choices not only at the beginning, but every time we need a choice, so that if our possible choices change, the program is then also responsible for tracking that, and updating the Choice class as necessary. So there isn't always a 1-1 call replacement in translation. Of course, if we don't do this, and run the examples with Java's random(), then JPF returns rather quickly, because it thought it didn't have to make any choices, and so there wasn't a whole lot to model check: but this means nothing was really accomplished.
Day 52 - Wednesday August 7th
Today I managed to get some of the examples working with this extra code that tracks choice/probability changes across program execution so that we could get something to work. This was somewhat successful: the code seems to do everything correctly (at least on one example), but I have hit some issues with scalability. For a program with about 12 (uniform) choice options, my patience ran out before the system returned (but after waiting at least half an hour). I was deterred because of this, and spent the rest of the day trying to convert other examples to resolve the issues mentioned above.
Day 53 - Thursday August 8th
Today was marked by a Skype meeting with one of my mentors, that set the stage for the next week and clarification of the ideas that I was working on during this week and last week. First, we talked about breaking transitions on expression evaluations, and there were some changes that I implemented: it shouldn't be quite as simple as I was making it: we do want to track every choice and note with special concern when states change due to an expression evaluation changing. So I went back and modified this so that every choice generated is a new state, and when an evaluation changes. The idea now is that we only merge or condense states if they're linked by a transition of probability 1. For the resolution of the random() function, we've decided that we can almost certainly get a work-around using the Choice class that will offload much of the tracking of probabilities during execution to this class, as opposed to the SUT. I won't go into detail on this until I'm done implementing it, so as to avoid confusion if I have to change anything. In addition, if I have time next week, I'm to start working on something like a statistical estimator for checking probabilistic systems: basically, run the SUT in JPF-prism X times without modification to choices (i.e. as if we're running it on any other Java VM), and watch the variables/property expressions. Then we can count Y/X, an empirical estimate of a property becoming true based on what we've seen.
Day 54 - Friday August 9th
Today was working on augmenting the Choice class to accommodate changes with respect to the notes above. This was somewhat complicated, as I have to make sure that I get the base class working correctly and modifying the JPF native-peer correctly, the latter of which is a new concept to me, and one that stood in my way a bit. As a result, I'm still working on this.
Today I was working on making sure that the examples worked in more than just a syntactic manner. And, unsurprisingly, they did not. There were several issues discovered across the examples, some of which are most like bugs in my code, others that are slightly more fundamental, and a few that may just be translation issues. Since the examples are not public, I won't talk about the specific issues in each example, but try to summarize the high level concerns. First, ignoring the issues that I think are related to my code functioning properly, there are issues translating arbitrary random codes: they each have their own notion of random(), which makes translation difficult, and in some cases, impossible, at least without further changes. In particular, for each call that should return a new "random" number, or get one from a choice, we (JPF) need a native-peer to execute, so that we (specifically, our choice generator class), can see what choices were possible, and what was made, to exhaustively check choices correctly. So a Java program calling just calling random() needs to be modified, so we know what the context is, and what the options are (that make sense). So we need something like jpf-probabilistic's Choice class, that is executed on the JPF side so that everything works. In some cases, we can use this class, but that also causes other issues: we need to know the possible choices not only at the beginning, but every time we need a choice, so that if our possible choices change, the program is then also responsible for tracking that, and updating the Choice class as necessary. So there isn't always a 1-1 call replacement in translation. Of course, if we don't do this, and run the examples with Java's random(), then JPF returns rather quickly, because it thought it didn't have to make any choices, and so there wasn't a whole lot to model check: but this means nothing was really accomplished.
Day 52 - Wednesday August 7th
Today I managed to get some of the examples working with this extra code that tracks choice/probability changes across program execution so that we could get something to work. This was somewhat successful: the code seems to do everything correctly (at least on one example), but I have hit some issues with scalability. For a program with about 12 (uniform) choice options, my patience ran out before the system returned (but after waiting at least half an hour). I was deterred because of this, and spent the rest of the day trying to convert other examples to resolve the issues mentioned above.
Day 53 - Thursday August 8th
Today was marked by a Skype meeting with one of my mentors, that set the stage for the next week and clarification of the ideas that I was working on during this week and last week. First, we talked about breaking transitions on expression evaluations, and there were some changes that I implemented: it shouldn't be quite as simple as I was making it: we do want to track every choice and note with special concern when states change due to an expression evaluation changing. So I went back and modified this so that every choice generated is a new state, and when an evaluation changes. The idea now is that we only merge or condense states if they're linked by a transition of probability 1. For the resolution of the random() function, we've decided that we can almost certainly get a work-around using the Choice class that will offload much of the tracking of probabilities during execution to this class, as opposed to the SUT. I won't go into detail on this until I'm done implementing it, so as to avoid confusion if I have to change anything. In addition, if I have time next week, I'm to start working on something like a statistical estimator for checking probabilistic systems: basically, run the SUT in JPF-prism X times without modification to choices (i.e. as if we're running it on any other Java VM), and watch the variables/property expressions. Then we can count Y/X, an empirical estimate of a property becoming true based on what we've seen.
Day 54 - Friday August 9th
Today was working on augmenting the Choice class to accommodate changes with respect to the notes above. This was somewhat complicated, as I have to make sure that I get the base class working correctly and modifying the JPF native-peer correctly, the latter of which is a new concept to me, and one that stood in my way a bit. As a result, I'm still working on this.
Tuesday, August 6, 2013
Expression based properties, examples & test cases, and some under-the-hood changes / Days 46 - 50
Day 46 - Tuesday July 30th
Breaking transitions based on expression evaluation
appears to be working, though it is currently limited to expressions regarding
integer variables--I think that for our purposes, this will be sufficient, and the step to changing it to support, say real values, is not hard, it's just a matter of adding more cases to some statements and making sure some parsing and type-checking works. I've omitted this for now, but I mean to get back to it very shortly for completeness. I'll try to explain how this system works below.
At a high level, what I've done is connected the Search class, that actually determines new states and stores them (or indicates the VM to store them) within the JPF VM, a listener that watches for InstructionExecuted notifications, which observes what variables take what values, with our StateRecord class, which records the state of the system, and has been since modified to keep track of the properties as well.
The system starts in an initial state, parses the properties, detects what variables to watch, and proceeds to execute instructions according to the search class, in this case, RandomSearch (initially supplied by jpf-probabilistic), which has been modified to prohibit the calls of notifyStateStored, notifyStateAdvanced, and other similar state-traversal methods (and those that label the state of the system) unless it has been allowed to by the monitoring listeners. Execution of instructions is monitored by the VarRecorder listener class, which determines if the search class can proceed to store a state and consider a new (or old) state.
If the instruction executed does not affect watched variables (or variables included in the property definition), then the listener instructs the search that it can proceed to the next instruction to be executed, but without updating the state number, or considering this a new system state (though, since instructions are executed, I believe the kernel state in JPF to be changing--but this is not something we're ever dealing with, so I'm side-stepping this). On the other hand, if the variable is watched and included in a property, then we observe what value this property had before executing the instruction, compare it to the evaluation of the property after the executed instruction, and if this changes, we let the search class proceed, but this time telling it to consider this a new system state, as the evaluation of the property expression has changed. And this process is repeated for every executed instruction.
Basically, we're only considering new states if it changes a property's evaluation, otherwise we're in the same state. For example, consider a system with variable var, and property var != 2, under the following instructions taken by JPF's search (where state will serve to track the system state we're in), omitting probabilities for simplicity:
1. Initial state is populated:
state = 0
var = undefined
2. JPF executes "var = 0;"
state = 1 (this happens since this is an evaluation of var != 2 returns true, and this is state other than the initial JPF state)
var = 0
3. JPF executes "var = 1;"
state = 1 (nothing happens: the evaluation of var != 2 still returns true, so we don't consider this a new JPF state; with respect to our properties, nothing new has really happened here)
var = 1
4. JPF executes "var = 2;"
state = 2 (this happens since this is an evaluation of var != 2 returns false, so we know something has changed with respect to a property, and we need a new state)
var = 2
5. JPF executes "var = 3;"
state = 1 (this happens since this is an evaluation of var != 2 returns true, so we know something has changed with respect to a property, and since we've seen this before, we'll reuse state 1)
var = 3
6. JPF terminates
The state space with transitions would be three states, with transitions from 0->1, 1->2, and 2->1, with appropriate probabilities in the real thing.
The system starts in an initial state, parses the properties, detects what variables to watch, and proceeds to execute instructions according to the search class, in this case, RandomSearch (initially supplied by jpf-probabilistic), which has been modified to prohibit the calls of notifyStateStored, notifyStateAdvanced, and other similar state-traversal methods (and those that label the state of the system) unless it has been allowed to by the monitoring listeners. Execution of instructions is monitored by the VarRecorder listener class, which determines if the search class can proceed to store a state and consider a new (or old) state.
If the instruction executed does not affect watched variables (or variables included in the property definition), then the listener instructs the search that it can proceed to the next instruction to be executed, but without updating the state number, or considering this a new system state (though, since instructions are executed, I believe the kernel state in JPF to be changing--but this is not something we're ever dealing with, so I'm side-stepping this). On the other hand, if the variable is watched and included in a property, then we observe what value this property had before executing the instruction, compare it to the evaluation of the property after the executed instruction, and if this changes, we let the search class proceed, but this time telling it to consider this a new system state, as the evaluation of the property expression has changed. And this process is repeated for every executed instruction.
Basically, we're only considering new states if it changes a property's evaluation, otherwise we're in the same state. For example, consider a system with variable var, and property var != 2, under the following instructions taken by JPF's search (where state will serve to track the system state we're in), omitting probabilities for simplicity:
1. Initial state is populated:
state = 0
var = undefined
2. JPF executes "var = 0;"
state = 1 (this happens since this is an evaluation of var != 2 returns true, and this is state other than the initial JPF state)
var = 0
3. JPF executes "var = 1;"
state = 1 (nothing happens: the evaluation of var != 2 still returns true, so we don't consider this a new JPF state; with respect to our properties, nothing new has really happened here)
var = 1
4. JPF executes "var = 2;"
state = 2 (this happens since this is an evaluation of var != 2 returns false, so we know something has changed with respect to a property, and we need a new state)
var = 2
5. JPF executes "var = 3;"
state = 1 (this happens since this is an evaluation of var != 2 returns true, so we know something has changed with respect to a property, and since we've seen this before, we'll reuse state 1)
var = 3
6. JPF terminates
The state space with transitions would be three states, with transitions from 0->1, 1->2, and 2->1, with appropriate probabilities in the real thing.
Day 47 - Thursday August 1st
Yesterday I was largely travelling, but I had several hours
on a plane in order to translate a few examples to test our code on, and I did spend today translating code. The code
was provided in C by one of my mentors, and show it had to translated into Java
to be run on our code. I won't describe the notion of examples, because I been asked not to release them yet, but I will say that there are about 12 of them (though 5 are already in Java). I spent most of the day translating the C examples into Java and making sure something runs with them, not yet with an eye towards checking the output of the examples, aside from making sure that at a glance it doesn't break anything. And so far, that was successful.
Day 48 - Friday August 2nd
I started today by supporting real-valued variables as mentioned in an earlier post; it didn't take long and I'm glad I got it out of the way. The rest of the day was committed to making sure that the example outputs were more than just functional: making sure that the results that we're getting are the one's we're expecting--this did not go well. Although I had mentioned in the past that I can parse properties successfully, I forgot that I only really had this working at a very syntactic level. I should explain, though I do recall mentioning this in the Skype meeting we had during the last week of July. Basically, in the past I had parsed properties to get them into memory on the JPF side: this involved ensuring the syntax was correct, that we had values for property expressions (at least when necessary), and of course breaking transitions and creating new JPF-states as a result of these properties changing. However, on the PRISM side of the code, which was largely untouched for quite some time, I had been passing in the same generic property to check reach-ability for: not the one that I was dealing with on the JPF-side. And while I had all this information, I didn't bother to update the PRISM calls. This was of course where the output started to falter, but I soon realized this, and spent the day parsing the property in a more semantic-case: understanding the property in terms of what state's it was targeting, and conveying this information to PRISM dynamically based on the property. The day was mostly spent on this issue.
Day 49 - Sunday August 4th
Today was spent towards the same issue as above: getting properties into PRISM in a suitable manner. It looks like the problem was resolved after some time for simple cases involving only a single property. The idea here is that since we break transitions based on properties, and each state corresponds to an evaluation of a property, we simply flag the state that corresponds to the true evaluation of the property, and ask PRISM to get the reach-ability of that state. (Of course, what happens if there is no such state? Then we don't even bother with any PRISM calls, and can return from the JPF-side code directly stating this. I think this makes sense--I will put this in an e-mail shortly.) The case with multiple properties doesn't seem any harder conceptually, but it required too many technical changes for today.
Day 50 - Monday August 5th
Again, and unfortunately, more of the same: getting multiple properties into PRISM in a meaningful sense. Conceptually, this was not hard, except that now there might be a number of states in which a given property is evaluated as true, and so we have to pass a number of states to PRISM. This I don't think required any special re-tooling on the PRISM side, as the computeUntilProbs (and similar) method takes a set of states to target. The changes to support these multiple states seems to have been implemented without cause for concern, but I want to test them. I started, again, to play around with translated examples, but I was actually pretty tired and my experiments didn't last long. I'll re-visit them, with some concrete news on their results tomorrow.
Subscribe to:
Posts (Atom)