JPF Output

There are three different ways a JPF run can produce output, each of them with a different purpose, but all controlled by the general JPF configuration mechanism:

  1. application output - what is the application doing?
  2. JPF logging - what is JPF doing?
  3. JPF reporting system - what is the result of the JPF run?

Application Output

This is the most simple form of output, which usually just consists of System.out.println(...) calls embedded in the application code. There is only one caveat - since this is executed by JPF as part of the application, the same print statement might be executed several times:

public class MyApplication ..{
    ...
    boolean cond = Verify.getBoolean();
    System.out.println("and the cond is: " + cond);
    ...
}

will produce

...
and the cond is: true
...
and the cond is: false
...

The second execution of the print statement is of course preceeded by a backtrack operation of JPF (the Verify.getBoolean() statement has two choices {true,false}), but the backtracking might not be visible, e.g. when running without the ExecTracker or ChoiceTracker listeners.

Since it can be sometimes confusing to see the same output twice without knowing if there is an iteration in the application, or JPF did backtrack between executions, there are two configuration options to control the output behavior:

vm.tree_output={true|false} - means output is shown on the console each time a print statement is executed. This corresponds to the above example, and is the default behavior.

vm.path_output={true|false} - will not immediately print the output on the console, but store in the path for subsequent processing once JPF terminates (if the output topic is specified - see below). This should produce the same output as running the test application on a normal JVM.

JPF Logging

This is a more interesting form of JPF output, primarily intended to show what JPF does internally. For this purpose, it has to support various levels of details, ranging from severe errors to fine grained logging of JPF operations.

JPF's logging mechanism does not reinvent the wheel, it piggybacks on the standard java.util.logging infrastructure. While this means it would be possible to use customized LogHandlers and Formatters (e.g. to log in XML format), there are specialized JPF incarnations of these classes, mainly to enable logging configuration via the standard JPF configuration mechanism rather than system properties.


logging for users - this includes two aspects: (1) controlling log output destination, and (2) setting log levels. Both are done with JPF property files.

To set the default log level, use

log.level=..

(the supported levels being severe,warning,info,fine,finer,finest)

To set a separate level for certain aspects (classes, packages or mechanisms), specify a list of the relevant logger IDs for the desired level, e.g.:

log.fine=gov.nasa.jpf.jvm.JVM:gov.nasa.jpf.jvm.ThreadInfo

If you want to log to a different console that possibly even runs on a remote machine, use the gov.nasa.jpf.tools.LogConsole on the machine that should display the log messages:

>java gov.nasa.jpf.tools.LogConsole port

Then start JPF on the test machine, specifying where the log output should go:

>jpf +log.output=host:port ... MyTestApp

The default host is localhost, default port is 20000. If these are suitable settings, you can start the LogConsole without parameters, and just specify +log.output=socket when running JPF.


logging for developers - there is one simple rule:

don't use System.out or System.err for any permanent logging!

(of course we all do this temporarily during debugging, but it shouldn't stay in the code). The logging infrastructure is quite easy to use. Just declare a static logger instance with an approproiate id (either package or logging topic) at the top of your class, and then use the Logger API to create output:

...
import java.util.logging.Level;
import java.util.logging.Logger;

package x.y.z;

class MyClass .. {
  static Logger log = JPF.getLogger("x.y.z");
  ...
    log.severe("there was an error");
  ...
    log.warning("there was a problem");
  ...
    log.info("something FYI");
  ...
    if (log.isLoggable(Level.FINE)){    // (1) don't create garbage
        log.fine("this is some detailed info about: " + something);
    }
  ...
}

Note that there is only one instance for each Logger ID, i.e. you can have a corresponding static field in all your relevant classes, and don't have to share the fields. Another aspect that is mostly important for the lower log levels (e.g. FINE) is that you should't concatenate log messages in operations that occur frequently (1), since the corresponding StringBuilder instances can cause performance degradations even if the log level is not set (the arguments still get evaluated). In this case, encapsulate the logging in log.isLoggable(level){..} blocks.

JPF Report System

The JPF reporting system is used to show the outcome of a JPF run, to report property violations, print traces, show statistics and much more. This is in a way the most important part of the JPF user interface, and might involve various different output formats (text, XML, API calls) and targets (console, IDE). Depending on application and project, users might also need control over what items are displayed in which order. It is also obvious this needs to be an extensible mechanism, to adapt to new tools and properties. The JPF report system provides all this, again controlled by JPF's general configuration mechanism.

The basic concept is that reporting depends on a predefined set of output phases, each of them with a configured, ordered list of topics. The output phases supported by the current system are:

  • start - processed when JPF starts
  • transition - processed after each transition
  • property_violation - processed when JPF finds a property violation
  • finished - processed when JPF terminates
  • Not all topics make sense for each phase (e.g. statistics during the start phase), but a number of them can indeed be varied in terms of topic and order. The standard list of start topics includes:

  • jpf - identifies the JPF version
  • platform - identifies machine, OS and Java version
  • user - identifies the user
  • dtg - identifies the date and time of the JPF run
  • config - shows which JPF configuration was used in the run
  • sut - identifies the application that was executed by JPF
  • There is no standard transition topic yet (but it could be implemented in PublisherExtensions). The standard property_violation topics include:

    Last not least, the finished list of topics that usually summarizes the JPF run:

    The system consists of three major components: (1) the Reporter, (2) any number of format specific Publisher objects, and (3) any number of tool-, property- and Publisher-specific PublisherExtension objects. Here is the blueprint:


    Figure 1: JPF Report System

    The Reporter is the data collector. It also manages and notifies Publisher extensions when a certain output phase is reached. The Publishers are the format (e.g. text, XML) specific output producers, the most prominent one being the ConsolePublisher (for normal, readable text output on consoles). PublisherExtensions can be registered for specific Publishers at startup time, e.g. from Listeners implementing properties or analysis modes (like the DeadlockAnalyzer. This is so common that the ListenerAdapter actually implements all the required interface methods so that you just have to override the ones you are interested in.

    Configuration is quite easy, and involves only a handful of JPF properties that are all in the jpf.report category. The first property specifies the Reporter class itself, but is not likely to be redefined unless you have to implement different data collection modes.

    jpf.report.class=gov.nasa.jpf.report.Reporter

    The next setting specifies a list of Publisher instances to use, using symbolic names:

    jpf.report.publisher=console:xml

    Each of these symbolic names has to have a corresponding class name defined:

    jpf.report.console.class=gov.nasa.jpf.report.ConsolePublisher

    Finally, we have to specify for each symbolic publisher name and output phase what topics should be processed in which order, e.g.

    jpf.report.console.property_violation=error:trace:snapshot

    Again, the order of these topics matters, and gives you complete control over the report format. As usual, please refer to defaults.properties for default values.

    Publisher classes can have their own, additional properties. For instance, the ConsolePublisher implementation can be further configured with respect to the information that is included in traces (bytecodes, method names etc.), and to redirect output (file, socket). Please refer to the constructor of this class for further details.

    # save report to file
    jpf.report.console.file=My_JPF_report

    All of the involved core classes and interfaces reside in the gov.nasa.jpf.report package. The most common way to extend the system is to use your own PublisherExtension implementation, which involves two steps:

    1. implement the required phase- and format- specific methods
    2. register the extension for s specific Publisher class

    The DeadlockAnalyzer (which is a listener to analyze concurrency defects) can be used as an example of how to do this:

    public class DeadlockAnalyzer extends ListenerAdapter {
      ...
      public DeadlockAnalyzer (Config config, JPF jpf){
        jpf.addPublisherExtension(ConsolePublisher.class, this);  // (1)
        ...
      }
      ...
      public void publishPropertyViolation (Publisher publisher) { // (2)
        PrintWriter pw = publisher.getOut();
        publisher.publishTopicStart("thread ops " + publisher.getLastErrorId());
        
        ... // use 'pw' to generate the output
      }
    }