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.