Posts for the month of January 2011

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.