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.
No comments:
Post a Comment