Recent posts (max 20) - Browse or Archive for more

JPF Workshop 2012

The Java PathFinder Workshop 2012 is co-located with FSE 2012.

Organizers: Peter Mehlitz, Neha Rungta, and Willem Visser

Submission Deadline: July 24th, 2012

The JPF Workshop will provide: (1) an introductory tutorial of the JPF framework for attendees unfamiliar with JPF, (2) detailed tutorials of JPF extensions such as symbolic execution, incremental program analysis, and android verification, and (3) give researchers and practitioners who already use JPF a forum to present their work. The workshop provides an opportunity to learn about software engineering, verification, and program analyses related research within the context of the Java Pathfinder framework.

We solicit submissions for existing research, applications, work in progress, and position papers on topics related to JPF or its extensions. If the underlying research idea has been published in another venue the paper needs to clarify the novel aspects that are being presented in the paper. We also solicit comparative analysis papers that evaluate algorithms in JPF or its extensions with relevant tools. The goal of the workshop is to encourage the flow of ideas relevant to JPF. The papers should be at most 5 pages long in the IEEE trans format.

Accepted papers will be published in the ACM digital library.

Submission Deadline: July 24, 2012 Notification of Acceptance: Aug 15, 2012 Final Version Submission: Sept 2, 2012

We hope you will submit to the workshop and attend it as well.

Mango plugin for Eclipse Workbench is ready

As advertised at the Workshop, the Mango plugin for the Eclipse workbench is ready for use. For examples and installation instructions, see jpf-mango.

Mango builds a functional model of Java code, exposed as navigable browser pages. When used as a sanity checker, Mango will halt at every case-split, allowing the programmer to compare source code with generated model.

As an educational tool. Those learning Java as a first programming language have the opportunity to compare procedural and functional views of code. This comparison facilitates the exposition of formal modeling concepts. For this purpose, the Mango installation contains a comprehensive set of first year Java code examples, such as CarRecall

Mango may potentially be used to generate and apply filters for known Java security issues, see for example Oracle guidelines Currently this is the active area of development. Waiting in the wings is formal theorem proving, see these comments.

ThreadList changes

Revision 588 has some significant ThreadList changes that are supposed to fix the problem of ThreadInfos being associated with wrong java.lang.Thread objects (the infamous "DiningPhil 8" problem). This happened if thread objects were sequentially created with the same reference value (due to collection of the previous object), and could have caused all sort of things from exceptions to missed paths. The culprit was the thread object to ThreadInfo map that was used by ThreadInfo.getThreadInfo(objRef), which was utterly unaware of re-used reference values.

Since this map needs to be state managed, we now use ThreadList for the mapping. ThreadInfos are added upon creation, and are removed when the object is collected. This has a number of implications for ThreadList:

  • the thread list can contain terminated threads
  • the list can shrink along a given path
  • thread ids don't have to correspond with storing order !!
  • thread ids can be re-used

Thread ids are re-used in order to be packed (which is required to efficiently keep track of referencing threads in ElementInfo reftids).

To implement all this, two housekeeping mechanisms were added:

(1) object ReleaseActions which are triggered when an object is collected. So far, we only support class based ReleaseActions, but those are quite useful to manage JPF object to host Java object relations

(2) JVM.addPostGcAction(Runnable), which can be used to walk over all live heap objects after the sweep is finished.

All this should be transparent if you didn't store ThreadInfos in listeners or peers, relying on that they never change identity for the same thread object. However, ThreadInfo.getIndex() was renamed to getId(), and ElementInfo.getIndex() was renamed to getObjectRef(), to make clear there is no guarantee that respective values are used as index values in corresponding containers.

Support for multiple attributes

support for multiple attributes was finally added for

  • ChoiceGenerators
  • objects (ElementInfo/Fields)
  • fields (ElementInfo/Fields)
  • operands (ThreadInfo/StackFrame)
  • locals (ThreadInfo/StackFrame)

The API is a compromise though, trying to balance runtime/memory costs, not changing existing clients, and providing new capabilities. The underlying implementation is using gov.nasa.jpf.util.ObjectList, which provides a static API to transparently handle lists that can either be a single Object value (i.e. no list, just a single element), or a linked list that uses a private type which does not conflict with potential element values. See ObjectList for restrictions and invariants (such as no null values etc.).

The assumed usage pattern is that listeners/peers use their own, private types for attributes, and retrieve attributes using such private types to make sure there are no other clients interfering with the same attribute types.

The general interface in the above classes looks like this

  • hasAttr()
  • hasAttr(Class<?>type)
  • getAttr() - returns all attributes (i.e. either the single value or the list head), so use only if you just want to copy all, or process elements by means of ObjectList (since it returns either an Object attr value, or a private ObjectList node instance)
  • getAttr(Class<T> type) - get the first attribute value of this type
  • getNextAttr(Class<T> type, Object prevValue) - iterate over the remaining attribute values of this type
  • attrIterator() - LIFO iterate over all attribute values (it's actually returning an Iterable, i.e. can be directly used in foreach loops)
  • attrIterator(Class<T> type) - LIFO iterate over all values of the specified type
  • setAttr(Object attr) - this sets all attributes, i.e. potentially overwrites the list head. Use only if you want to copy all that was obtained by a previous getAttr(), you want to make sure there is only a single attribute set, or what you set was created with ObjectList.createList(Object... a)
  • addAttr(Object attr) - this adds a new value as the first list element (which implies enumeration is LIFO)
  • removeAttr(Object attr) - uses equals() comparison to identify the attribute value to remove (if only one attribute remains, representation changes back to Object)
  • replaceAttr(Object oldAttr, Object newAttr) - if the order of attribute enumeration should not be changed

The danger is of course that some listeners/peers don't play nicely with others and just indiscriminately use get/setAttr(), overwriting everything. This in turn can cause funny force fights between multiple pre-exec listeners, post-exec listeners and peers. However, enforcing attribute containers and renaming the API would have ended in a lot of @Deprecated methods, which people just tend to ignore anyways. Since we still anticipate this is mostly used in a single attribute value context, adding containers would also also have imposed significant runtime overhead (attributes are state stored).

Bottom line is to be a nice citizen that (a) uses its own attribute types and (b) is aware of that there might be other attributes.

The jpf-core itself will not make use of attributes for internal purposes.

Slides for Summer School on Formal Techniques

I just uploaded the slides for the JPF talks and lab given at the First Summer School on Formal Techniques (05/22-05/27/2011 Menlo College, Atherton CA) to the presentations page. You can find PowerPoint, Keynote and PDF versions in the attachments section of this page. Especially the lab is a good basis for a first hands-on course of about 2h.

JPF Workshop 2011

We have a JPF Workshop 2011 co-located with ASE 2011 in Oread, Lawrence, Kansas on Nov 12.

Call for Contributions:

We welcome contributions on all topics related to JPF or one of its extensions. In addition to research papers, we also solicit comparative analysis papers that evaluate algorithms in JPF or its extensions with relevant tools. The goal of the workshop is to encourage the flow of ideas relevant to JPF. We solicit two kinds of papers:

  1. Full Papers: The full papers should be at most 12 pages long in the IEEE trans format. The paper should describe a fully matured research topic that has been implemented within JPF core or one of its extensions. The papers can be previously published at other peer-reviewed venues or be original research papers not been published before. In previously published work we highly encourage addition of new material that provides new insights about either the implementation, engineering, or evaluation with respect to JPF.
  1. Short Papers: The short papers should be at most 5 pages long in the IEEE trans format. Short papers can describe an extension of JPF as a tool paper. Work in progress descriptions can also be submitted as short papers.

The best papers in the workshop will be invited to be included in a special STTT issue on Java Pathfinder.

Important Dates and Deadlines:

  • Paper Submission Deadline: August 29, 2011
  • Notification of acceptance/rejection: September 30, 2011
  • Deadline for Final Version: October 15, 2011

different Instruction class hierachies

jpf-core r474 aims at making gov.nasa.jpf.jvm agnostic to specific Instruction class hierarchies. This mostly works by relaxing the gov.nasa.jpf.jvm.InstructionFactory interface to return abstract Instruction types, and should be transparent to most InstructionFactory implementors.

However, if you use your own TABLESWITCH, LOOKUPSWITCH or xRETURN classes that are not derived from their jpf-core counterparts, you have to make them implement the corresponding

  • TableSwitchInstruction
  • LookupSwitchInstruction
  • ReturnInstruction

interfaces from gov.nasa.jpf.jvm. This should not require any new methods, just add the respective implements spec to your instruction class.

so long BCEL

I just pushed the de-BCEL'ed jpf-core and corresponding changes to jpf-numeric, jpf-aprop and jpf-concurrent. With this, the jpf-core runtime does not require any 3rd party libs anymore (we still use Ant and JUnit for our build system). Apart from saving about 400 BCEL classes (essentially replaced by gov.nasa.jpf.classfile.ClassFile), this also comes with a significant class load time reduction. The most important aspect however is that we can now easily deal with classfile extensions such as JSR-308.

This was a rather big change, and I expect this to take a little time to stabilize.

Nothing is for free, there are two changes that affect other JPF projects:

(1) InstructionFactory - this is now a straight forward factory pattern with dedicated factory methods such as

  public ALOAD aload(int localVarIndex) {
    return new ALOAD(localVarIndex);

To adapt to the new scheme, create a InstructionFactory class in your ...bytecode package, derive it from gov.nasa.jpf.jvm.bytcode.InstructionFactory, and override the factory methods for your own bytecodes. Don't forget to use @Override to catch typos, to make sure JPF is actually using your factory methods. Check out jpf-numeric for an example.

(2) separate classpaths - it turns out there still was a classpath crossover from the JPF classpath to the host VM native_classpath in the previous jpf-core version, which was mostly used (implicitly) from regression tests using JPF classes inside of JPF executed code. While it would be easy to reinstate under the new classfile parsing, it seems to be wise to strictly separate the two worlds. This means you now have to setup your <project>.test_classpath in your correctly. In some cases, it is more appropriate to add this directly as a "+classpath=.." argument to the verify..(jpfArgs) calls in your tests. This is somewhat annoying at first, but at least now you know where JPF gets its classes from (you can see by setting "+log.fine=gov.nasa.jpf.classfile").

Please update your projects accordingly.

upcoming BCEL replacement

this is a heads-up that the BCEL replacement is going to be pushed to babelfish within the next 10 days or so. Most projects shouldn't be affected, but if you have your own bytecode factories, those have to be changed. It becomes straight forward inheritance though, with a method per opcode. You just override the methods for your own instruction types:

public class MyInstructionFactory extends 
            gov.nasa.jpf.jvm.bytecode.InstructionFactory {
  public void astore_0() {
    add( new ASTORE(0));  // your instruction class here

more details will follow.

Added page for hosting Eclipse plugin

I have added a page describing Sandro's method for hosting an Eclipse plugin. You have to do it from the wiki, I am convinced now you cannot do it (or at least should not do it) from the repository. See hosting an Eclipse plugin update site.

JPF accepted for GSoC 2011

Java Pathfinder has been accepted as one of the mentoring organizations for Google Summer of Code 2011. Students interested in JPF-related projects are encouraged to peruse the ideas for projects page on the wiki at:

Students interested in projects are encouraged to explore ideas listed on the page as well as their own ideas. Email us at jpf.gsoc [at] gmail [dot] com if you have project specific questions. Ask questions on the JPF mailing list if the question seems relevant for the larger JPF community. The JPF mailing list is open to everyone at:

We hope to have a very busy summer with lots of work on interesting JPF projects.

SystemState.setNextChoiceGenerator() changes

In the wake of enabling customized POR by means of choiceGeneratorRegistered() listeners, SystemState.setNextChoiceGenerator() now returns a boolean indicating if there is a CG set after all listeners got notified.

NOTE: this requires recompilation of projects using setNextChoiceGenerator()

Of course there are occasions where overriding CGs is not allowed, such as blocking sync calls or waits. These cases should now use SystemState.setMandatoryNextChoiceGenerator(cg,failMsg), which will throw an exception in case no CG was provided or a listener did override it.

Only callers in jpf-core have been updated accordingly. If you want to make your extensions listener POR-able, you have to add similar patterns.

Overridable CG:

  ChoiceGenerator<..> cg = ...;
  if (ss.setNextChoiceGenerator(cg)){
    return this;                        // if in a bytecode instruction
    // env.repeatInvocation(); return;  // if in a peer method

Non-overridable CG:

  ChoiceGenerator<..> cg = ...;
  ss.setMandatoryNextChoiceGenerator(cg, "somebody screwed up, no CG set for ..");

listener changes

Three changes you should be aware of:

(1) Search now always does stateAdvanced() notifications before propertyViolated(). The rationale is that many listeners use stateAdvanced() to maintain property specific traces, in which case the trace update for the last transition had to be duplicated in propertyViolated(), which was a common pitfall. If a listener has to determine if a stateAdvanced() lead into an error, it has to call Search.getCurrentError(), which is set before stateAdvanced() is notified.

Search classes should do the propertyViolated() notification from inside their search() loop, to make the order of notifications more obvious.

(2) Reporter is now only a SearchListener, and gets always notified after all user configured listeners. The rationale is that a lot of listeners are also PublisherExtensions, and it is next to pointless to publish before actually being notified.

(3) listeners are not anymore allowed to change the KernelState from within choiceGeneratorSet(), choiceGeneratorAdvanced() and choiceGeneratorProcessed() notifications. The reason is that these notifications will happen before state storage (which does not happen at all if there is no next choice in the current CG). In the future there might be a check for changed fields or thread states outside transitions, but for now you have to make sure that you avoid such side effects.

Version 6 Released

I have just pushed a new major jpf-core release to the babelfish repo - v5 is dead, long live v6. Welcome to a new internal design - and a whole new set of bugs: I expect this will take some time to consolidate.

For the most part, this should be transparent if you didn't directly work with state management (Restorer and Serializer), or directly used the DynamicArea instead of the Heap interface. This was the major objective: make object allocation time linear in terms of heap size. Unfortunately, the DynamicArea was pretty much hardwired into the CollapsingRestorer and FilteringSerializer, so both state-storage/restore and state-matching infrastructure had to be rewritten too. Long story short (the long story will go to the developers section of the wiki once I have recovered), the problem is solved: allocation and garbage collection are much faster, and overall memory consumption is much lower, esp. in the gc and serializing peaks.

Two side effects you might want to employ in your JPF applications: we now keep track of which threads access an object, and at least with the SparseClusterArrayHeap you can also see which thread allocated the object (reference values are thread based). You will also see a different search graph, since the old recursive and very expensive prospective reachability analysis has been replaced with the thread access bitmap. As a downside Thread.start() now always has to be a transition break if you want to detect data races (don't fiddle with cg.threads.break_start unless you really have to). I'm sure this topic will be subject to more wiki postings.

Since there already were so many changes, I did throw in two things that might require some work in your projects. JPF now has a full type system for Fields and FieldInfos. We now store arrays as the target types, not unconditionally as int[] arrays. This not only makes conversions (e.g. from listeners) and arraycopy much faster, but can esp. save some memory if your SUT is heavy on Strings or byte[] arrays. I expect less problems from that, but more from the FieldInfo type hierarchy (which resembles the host VM). JPF is not cavalier about storing int values into non int fields anymore - it checks the types on both field/array getters and setters. Can be a little annoying if you were used to Q&D, but the added type safety is worth it.

I'm sure I forgot a ton of changes, but we do them one at a time. Let the mayhem begin.

new choiceGeneratorRegistered() notification

There is a new VMListener.choiceGeneratorRegistered(vm) notification that is done each time the VM, a native peer or a listener registers a new ChoiceGenerator, which normally ends the current transition. This is also the reason for having such a notification, in addition to the already existing choiceGeneratorSet(). The latter one happens at the beginning of a new transition, i.e. after state matching/storage, whereas choiceGeneratorRegistered() is called before the previous one is terminated. Theoretically, a listener could even revert some CG registrations to do fancy state space optimizations. However, be aware of that there might be several listeners around, it wouldn't help much if you try to revert a CG that is set by a CG that was registered later.

NativeMethodInfos and NativeStackFrames

a big change that will require some external projects to be updated

From the commit message of

peer method executions now have their own NativeMethodInfos and NativeStackFrames, i.e. we have MethodInfo and StackFrame class hierarchies. The NativeStackFrame instances only execute two new, synthetic insns: EXECUTENATIVE and NATIVERETURN. The reason for this is mostly twofold:

(1) to have symmetric invoke/return instructions, no matter if the implementation of a method is MJI or not

(2) to solve the old problem of not having a scheduling point upon return from a synchronized native/MJI method. Having only one on the invoke inns isn't enough since the peer method can of course have thread-global effects

As a side effect, we now don't have to cache the invoke arguments anymore, since the caller StackFrame is kept intact until NATIVERETURN execution.

Another even more beneficial side effect is that we now have a place to store data from peer methods that have to do a (potentially open) number of roundtrips (think native HashMap). The NativeStackFrame operands and locals are not used for arguments and return values for the corresponding method, they are completely yours for use from within peer methods.

The downside of all this is that there already was a lot of code that explicitly handled/assumed the old non-symmetrical behavior. This code has to be changed to reap the benefits mentioned above, mostly for two things:

(a) post-exec listeners on InvokeInstructions have to be aware of that the peer method has not been executed yet. Listen on the EXECUTENATIVE instead.

(b) peer methods have to be aware of that the caller stack frame is *not* on top. To get the caller (e.g. to get locals etc.), use ThreadInfo.getLastNonSyntheticStackFrame()

required changes in your code

from simple to more severe:

  • if you have InstructionVisitor implementations, you have to add EXECUTENATIVE,NATIVERETURN and DIRECTCALLRETURN * DirectCallStackFrames don't have a 'nextPc' anymore, they always come back to the current pc of the issuing stack frame. Hence both the DirectCallStackFrame constructor and ClassInfo.initialize() don't take nextInsn arguments - just delete them
  • there is no ThreadInfo.isResumedInstruction(insn) anymore, to be used within your peer methods. Replace it with ThreadInfo.hasReturnedFromDirectCall(id), and use meaningful direct call names
  • if you have instructionExecuted() listeners making implicit assumptions about certain methods being native, and native peer methods already being executed upon notification, these have to be adapted. There is a new EXECUTENATIVE synthetic instruction, which in most cases can be used as a more precise replacement
  • if you had your own StackFrame/MethodInfo class hierarchies, this has to be redesigned to use delegation

cascaded ChoiceGenerators

as per changeset 270 (, the restriction of having only one CG/choice per transition is gone - say hello to cascaded ChoiceGenerators.

This is especially useful to create CGs from listeners, since you don't have to worry about at what states/instructions you can set a CG without colliding with the ones that are created by JPF itself (e.g. ThreadChoiceGenerators in scheduling points).

If you happily live in single-CG bliss, you can (for now) continue to do so with no or just minimal changes (CG constructors now require String ids). The old APIs are still there.

In order to use the new feature, you need to give your CGs meaningful (reads unique) ids, and retrieve them specifying this id and their type, as in

SystemState ss = jvm.getSystemState();
ThreadInfo ti = jvm.getLastThreadInfo();
if (!ti.isFirstStepInsn()) { // create and register CG
  IntChoiceGenerator cg = new IntChoiceFromSet("fieldReplace", ...);
} else { // second time around, use the CG
  IntChoiceGenerator cg = ss.getCurrentChoiceGenerator("fieldReplace", IntChoiceGenerator.class);
  assert cg != null : "no 'fieldReplace' IntChoiceGenerator found";
  int choice = cg.getNextChoice();
  ... // process choice

Now there are some caveats if it comes to using cascaded CGs from listeners, but these are mostly caused by various execution states of the triggering instructions (which normally reexecute when they set CGs themselves). Just be aware of that you get pre- and post execution notifications no matter if the instruction is reexecuted or completed. Use ThreadInfo.willReExecuteInstruction() if in doubt.

This change might break some extensions out there, but it should only require adding ids to your ChoiceGenerator constructor calls to fix it.

configurable JNI library lookup

If you absolutely have to, you can now configure how to load native JNI libraries at runtime. This works by using a (minimal) JPFClassLoader that does findLibrary() lookup through a native_libraries property, which in turn gets initialized by collecting all


settings. and os.arch are the standard system properties. In order to use this, you have to know their values on the target machine, and you have to know the platform specific library name mapping, which you can find out through System.mapLibraryName(). Only properties that match the target platform at runtime are considered.

lock-free wait optimization

there now is support to do wait/notify without holding the corresponding lock. While this is not possible within Java (the language), it helps to save states in native methods such as sun.misc.Unsafe.park()/unpark() and java.lang.Thread.join(). It solves the problem of having two CGs within an atomic context that doesn't change the thread state, which otherwise produces redundant transitions (the diamond with one degenerated edge on each side). If you think you might need such a thing, look at the JPF_java_lang_Thread.join() example.

revamped testing infrastructure

In the wake of the new initialization scheme, TestJPF got an overhaul too. It no longer requires org.junit to be in the classpath when resolving your test class, and there is now an executable RunTest.jar that lets you execute tests standalone. If you are in a JPF project dir, you invoke it like

> bin/test <your-test-class> [<test-method> ... ]

You have to add one line to the of your project to make it work, which usually looks like

<my-project>.test_classpath = build/tests

More importantly, there is now a public low level test API which allows you to obtain the JPF objects in question, e.g. to analyze the number of states and other statistics. Test methods using it look like this

class MyTests extends TestJPF {
@Test public void someTest () {
    JPF jpf = null;

    if ((jpf = noPropertyViolation("MyTests", "someTest")) == null){
      //... this is only executed by JPF

    if (jpf != null){
      //... this is only executed outside of JPF
      // you can use the JPF object to do inspection of a previous run
      assert jpf.getSearchErrors().isEmpty() : "unexpected JPF search errors";

Please note that you have to provide the test class and the test method names explicitly, but this also allows you to separate the test driver and the JPF tested code if you want to do so.