2 Listeners are perhaps the most important extension mechanism of JPF. They provide a way to observe, interact with and extend JPF execution with your own classes. Since listeners are dynamically configured at runtime, they do not require any modification to the JPF core. Listeners are executed at the same level like JPF, so there is hardly any limit of what you can do with them.
4 ![Figure 1: JPF Listeners](../graphics/listener-overview.svg){align=center width=800}
6 The general principle is simple: JPF provides an observer pattern implementation that notifies registered observer instances about certain events at the search level and the VM level. These notifications cover a broad spectrum of JPF operations, from low level events like `instructionExecuted` to high level events like `searchFinished`. Each notification is parameterized with the corresponding source (either the `Search` or the `VM` instance), which can be then used by the notified listener to obtain more information about the event and the JPF's internal state.
8 Configuration is usually done with the `listener` property, either from the command line, or a .jpf property file. Listeners can also be associated with annotations, to be automatically loaded whenever JPF encounters such an annotation. Applications can use the `@JPFConfig` annotation to explicitly specify JPF listeners. Lastly, if JPF is used in an embedded mode, listeners can be registered with an API.
14 There are two basic listener interfaces, depending on corresponding event sources: `SearchListeners` and `VMListeners`. Since these interfaces are quite large, and listeners often need to implement both, we also provide "adapter" classes, i.e. implementors that contain all required method definitions with empty method bodies. Concrete listeners that extend these adapters therefore only have to override the notification methods they are interested in.
16 The adapter classes are used for the majority of listener implementations, especially since they also support two other interfaces/extension mechanisms that are often used in conjunction with `Search` and `VMListeners`:
18 1. `Property` - to define program properties
19 2. `PublisherExtension` - to produce output within [the JPF reporting system](report)
21 `ListenerAdapter` is the bare adapter implementation for `SearchListener`, `VMListener` and `PublisherExtension`. This is what is mostly used to collect information during JPF execution (e.g. `CoverageAnalyzer` and `DeadlockAnalyzer`).
23 `PropertyListenerAdapter` is used in case the listener implements a program property, i.e. it can terminate the search process. A prominent example of this category is `PreciseRaceDetector`.
25 ![Figure 2: Listener Types](../graphics/listeners.svg){align=center width=800}
27 Choosing the right type for your listener is important, since JPF automatically registers listeners (and properties) based on this type. You can bypass and directly implement single listener interfaces, but then you also have to do the proper registrations.
29 Usually, the notification alone is not enough, and the listener needs to acquire more information from JPF. For this purpose, we provide either the `Search` or the `VM` instance as notification arguments, and the listener has to use these as "Facades" to query or interact JPF. It therefore matters to implement the listener within the right package.
35 `SearchListener` instances are used to monitor the state space search process, e.g. to create graphical representations of the state-graph. They provide notification methods for all major Search actions.
38 package gov.nasa.jpf.search;
39 public interface SearchListener extends JPFListener {
40 void searchStarted (Search search);
41 void stateAdvanced (Search search); // got next state
42 void stateProcessed (Search search); // state is fully explored
43 void stateBacktracked (Search search); // state was backtracked one step (same path)
44 void stateStored (Search search); // somebody stored the state
45 void stateRestored (Search search); // previously generated state was restored (any path)
46 void propertyViolated (Search search); // JPF encountered a property violation
47 void searchConstraintHit (Search search); // e.g. max search depth
48 void searchFinished (Search search);
53 For the standard depth first search (`gov.nasa.jpf.search.DFSearch`), listener implementations can assume the following notification model:
56 ![Figure 3: Depth first listener notifications](../graphics/DFSListener.svg){align=center width=500}
58 The most frequently used notifications are:
60 `stateAdvanced` - to store additional, backtrackable state information in an associative array
62 `stateBacktracked` - to restore additional state information
64 `searchFinished` - to process listener results
70 This is a fat interface, reflecting various VM operations
73 package gov.nasa.jpf.jvm;
74 public interface VMListener extends JPFListener {
75 //--- basic bytecode execution
76 void executeInstruction (JVM vm); // JVM is about to execute the next instruction
77 void instructionExecuted (JVM vm); // JVM has executed an instruction
79 //--- thread operations (scheduling)
80 void threadStarted (JVM vm); // new Thread entered run()
81 void threadBlocked (JVM vm); // thread waits to acquire a lock
82 void threadWaiting (JVM vm); // thread is waiting for signal
83 void threadNotified (JVM vm); // thread got notified
84 void threadInterrupted (JVM vm); // thread got interrupted
85 void threadTerminated (JVM vm); // Thread exited run()
86 void threadScheduled (JVM vm); // new thread was scheduled by JVM
88 //--- class management
89 void classLoaded (JVM vm); // new class was loaded
91 //--- object operations
92 void objectCreated (JVM vm); // new object was created
93 void objectReleased (JVM vm); // object was garbage collected
94 void objectLocked (JVM vm); // object lock acquired
95 void objectUnlocked (JVM vm); // object lock released
96 void objectWait (JVM vm); // somebody waits for object lock
97 void objectNotify (JVM vm); // notify single waiter for object lock
98 void objectNotifyAll (JVM vm); // notify all waiters for object lock
100 void gcBegin (JVM vm); // start garbage collection
101 void gcEnd (JVM vm); // garbage collection finished
103 void exceptionThrown (JVM vm); // exception was thrown
105 //--- ChoiceGenerator operations
106 void choiceGeneratorSet (JVM vm); // new ChoiceGenerator registered
107 void choiceGeneratorAdvanced (JVM vm); // new choice from current ChoiceGenerator
108 void choiceGeneratorProcessed (JVM vm); // current ChoiceGenerator processed all choices
113 The most commonly used methods are the instruction notifications:
115 `executeInstruction` - is called before a bytecode instruction gets executed by the VM. The listener can even use this to skip and/or replace this instruction, which is useful for non-invasive instrumentation.
117 `instructionExecuted` - is the post-execution notification, which is suitable to keep track of execution results (method invocations, assigned field values, branch results etc.)
122 The following example is a slightly abbreviated form our race detector. The basic idea is simple: every time we encounter a new scheduling point (i.e. new `ThreadChoiceGenerator` object) that is due to a field access on a shared object, we check if any of the other runnable threads is currently accessing the same field on the same object. If at least one operation is a `putfield`, we have a potential race.
124 The example shows three aspects that are quite typical:
126 1. listeners often use only a small number of notification methods
128 2. they often do not require a huge amount of code (most expensive operations are performed by the `VM` and the `Search` objects)
130 3. sometimes you have to dig deep into JPF internal constructs, to extract things like `ThreadInfo`, `FieldInfo` and `ChoiceGenerator` instances
133 public class PreciseRaceDetector extends PropertyListenerAdapter {
136 //--- the Property part
137 public boolean check(Search search, JVM vm) {
138 return (raceField == null);
141 //--- the VMListener part
142 public void choiceGeneratorSet(JVM vm) {
143 ChoiceGenerator<?> cg = vm.getLastChoiceGenerator();
145 if (cg instanceof ThreadChoiceFromSet) {
146 ThreadInfo[] threads = ((ThreadChoiceFromSet)cg).getAllThreadChoices();
147 ElementInfo[eiCandidates = new ElementInfo[threads.length](]);
148 FieldInfo[fiCandidates = new FieldInfo[threads.length](]);
150 for (int i=0; i<threads.length; i++) {
151 ThreadInfo ti = threads[i];
152 Instruction insn = ti.getPC();
154 if (insn instanceof FieldInstruction) { // Ok, its a get/putfield
155 FieldInstruction finsn = (FieldInstruction)insn;
156 FieldInfo fi = finsn.getFieldInfo();
158 if (StringSetMatcher.isMatch(fi.getFullName(), includes, excludes)) {
159 ElementInfo ei = finsn.peekElementInfo(ti);
161 // check if we have seen it before from another thread
163 for (int j=0; j<i; j++) {
164 if ((ei ## eiCandidates[&& (fi ## fiCandidates[j](j])))) {
170 if (idx >= 0){ // yes, we have multiple accesses on the same object/field
171 Instruction otherInsn = threads[idx].getPC();
172 if (isPutInsn(otherInsn) || isPutInsn(insn)) {
173 raceField = ((FieldInstruction)insn).getFieldInfo();
178 eiCandidates[i] = ei;
179 fiCandidates[i] = fi;
187 public void executeInstruction (JVM jvm) {
188 if (raceField != null) { // we're done, report as quickly as possible
189 ThreadInfo ti = jvm.getLastThreadInfo();
190 ti.breakTransition();
198 Explicit instantiation of a listener (e.g. from a JPF shell) can be done in any way. If the listener is specified as a JPF property, it's class either needs to have a default constructor, or a constructor that takes a single `gov.nasa.jpf.Config` argument. The `Config` object that is passed into this constructor by JPF is the same that was used for the initialization of JPF itself. This is the preferred method if the listener has to be parameterized. In case of the `PreciseRaceDetector` example, this can be used to filter relevant fields with regular expressions:
201 public class PreciseRaceDetector extends PropertyListenerAdapter {
203 StringSetMatcher includes = null;
204 StringSetMatcher excludes = null;
206 public PreciseRaceDetector (Config conf) {
207 includes = StringSetMatcher.getNonEmpty(conf.getStringArray("race.include"));
208 excludes = StringSetMatcher.getNonEmpty(conf.getStringArray("race.exclude"));
211 public void choiceGeneratorSet(JVM vm) {
214 if (StringSetMatcher.isMatch(fi.getFullName(), includes, excludes))
222 Listener configuration can be done in a number of ways: via JPF properties from the command line or a .jpf file, via JPF APIs from a JPF shell (a program invoking JPF), or from the system under test by using Java annotations (i.e. without code modification).
224 Since listeners are executed by the host VM, they have to be in the `CLASSPATH` (`jpf-core.native_classpath` property).
230 the *listener* property can be used to specify a colon separated list of listener class names:
233 bin/jpf ... +listener=x.y.MyFirstListener,x.z.MySecondListener ...
237 ### .jpf property file ###
240 If you have several listeners and/or a number of other JPF options, it is more convenient to add the `listener` property to a .jpf file:
243 # Racer-listener.jpf - JPF mode property file to detect data races in jpftest.Racer
244 target = jpftest.Racer
245 listener=gov.nasa.jpf.tools.PreciseRaceDetector
249 ### Autoload Annotations ###
252 Consider your system under test is marked up with a Java annotation that represent properties. For example, you can use the `@NonNull` annotation to express that a method is not allowed to return a `null` value:
255 import gov.nasa.jpf.NonNull;
257 @NonNull X computeX (..) {
258 //.. some complex computation
263 You can use .jpf property files (or the command line, if you love to type) to tell JPF that it should automatically load and register a corresponding listener (e.g. `NonNullChecker`) if it encounters such a `@NonNull` annotation during class loading:
267 listener.autoload = gov.nasa.jpf.NonNull,...
268 listener.gov.nasa.jpf.NonNull = gov.nasa.jpf.tools.NonNullChecker
273 ### @JPFConfig annotation (SuT) ###
276 You can also explicitly direct JPF to load the listener from within your application by using the `@JPFConfig` annotation:
279 import gov.nasa.jpf.JPFConfig;
281 // set JPF properties via properties at class load time
282 @JPFConfig ({"listener+=.tools.SharedChecker", ..})
283 public class TestNonShared implements Runnable {
288 However, this is not recommended outside JPF tests - the application would run, but not compile without JPF.
291 ### Verify API (SuT) ###
294 A less often used method is to set listeners is to use the `gov.nasa.jpf.vm.Verify` API from within your application. With this, you can control the exact load time of the listener (but be aware of backtracking). With this, the above example would become
297 import gov.nasa.jpf.vm.Verify;
299 public class TestNonShared implements Runnable {
301 public static void main (String[] args){
303 // set JPF properties programmatically
304 Verify.setProperties("listener+=.tools.SharedChecker", ...);
310 This method should only be used in special cases (models written explicitly for JPF verification), since it does not run outside JPF.
313 ### JPF API (embedded mode) ###
316 If JPF is explicitly started from within another application, listeners can be instantiated at will and configured via the `JPF.addListener(..)` API:
319 MyListener listener=new MyListener(..);
321 Config config = JPF.createConfig( args);
322 JPF jpf = new JPF( config);
323 jpf.addListener(listener);
328 Most listeners tend to fall into three major categories:
330 1. system class (e.g. for logging) - is usually configured via the default.properties.
331 2. complex properties - is configured with an application specific mode property file.
332 3. JPF debugging - is specified via the command line (`+key=value` overrides).