Friday, May 31, 2013

Looking at Code / Day 3

Today, I spent some time doing what I can probably always improve on: getting familiar with the code that I will be working on. Although I had done this before, and I will likely spend much more time looking at the documentation and code for the two model checkers I'll be working with, but of course, the more I look at it, the more I remember, and so this should hopefully transition into more efficient coding when that time comes. At the very least, it should help me when I need to know where to look for something. Further, I've got a bit of a question document going to send to the experts, so being able to relate high-level concepts with code seems to make those questions more precise.

Wednesday, May 29, 2013

Listeners / Day 1

Today was the first day where I did not spend the majority of it setting things up or completing administrative tasks. Instead, I spent the day following the slides I alluded to in my last post, and created a JPF listener that was a separate stand-alone extension to the jpf-core package. I won't post the slides online, but I think they were a great tutorial (and I'm guessing that if you were at FSE'12 there was a chance you saw them). I also spent time looking at the code structure for the PRISM and JPF checkers.

As I said yesterday, however, I would like to take some time to explain concepts in greater detail, largely to make sure that I myself understand them (often, trying to explain topics helps speed the time it takes to understand the concept). So today, I'll talk briefly about JPF listeners.

JPF listeners are a primary method for extending JPF, and operate at the same level of the model checker without need to modify the model checker code. Configuration is done through .jpf files and this instructs JPF to make sure this listener is notified to the appropriate events: listeners are effectively implementations of the common observer pattern; i.e. they listen for events to happen (who would have guessed?). When JPF is working, it acts on two major objects: the Java Virtual Machine (JVM), and search objects. search objects are those that control which state the JVM tries to explore next, backtracks to, or otherwise changes what state the JVM should be dealing with. Listeners can be notified by search objects or the JVM. Note that the code being checked never directly interacts the listener; only JPF deals with listeners.

Listeners are also built easily; various listeners can be extended so that a developer wanting a new listener needs only to extend a class, override the appropriate methods, and implement the desired functionality. In the basic example I was shown, it was only necessary to implement 7 short (one to four line) methods by extending the appropriate listener. The choice of listener to extend may be confusing (jpf-core comes with 43 of them), but building from scratch is always a viable option. The list of methods in the interfaces for listeners can be found, as well as an official (and more detailed) description of listeners can be found here.

First post / Day 0

I spent today setting up for the challenges ahead: I created this blog, set up the Bitbucket repository, and submitted the necessary documentation to Google. I also spent time building a toy JPF Listener (which just printed to console any time anything really happened to a state; there was a lot of spam in console) just to play around with, and to make sure I still understand how JPF works. I did this first by encoding one and putting it in the jpf-core files, building all of them again, and then calling the listener. This is the not ideal way to do it: it puts the listener in the wrong spot (it should be a separate extension to jpf-core, not a part of it). But this was the way I remembered by memory, so I did it anyways. Then I started looking to clone jpf-template and  make a listener the proper way--which was easy, especially since while I was doing this one of my mentors sent me slides on how to do exactly that. The hardest part was getting ant to work and build the code--but thankfully it was only a matter of an environment variable.

The purpose of this blog is largely to track my own progress: I'm expecting that it will be much harder for me to go off track if I have to report (if only to myself) at the end of every day. That being said, I would like to make it more interesting than a simple statement similar "today I accomplished tasks x, y, and z", so I'll also try to explain each topic. For example, in this post, I might explain what a listener is, or the architecture of JPF at a high level. However, it's the first day, and since I have no concrete plans for tomorrow, I'm going to save that for tomorrow and likely make a "good" post of it.

I am rather excited about being accepted for Google Summer of Code and I'm really looking forward to the coming months when the work and posts become really interesting.