gov.nasa.jpf.listener

Class PreciseRaceDetector

java.lang.Object

gov.nasa.jpf.GenericProperty

gov.nasa.jpf.PropertyListenerAdapter

gov.nasa.jpf.listener.PreciseRaceDetector

All Implemented Interfaces:

JPFListener, Property, PublisherExtension, SearchListener, Printable, VMListener, java.lang.Cloneable

public class PreciseRaceDetector
extends PropertyListenerAdapter

This is a Race Detection Algorithm that is precise in its calculation of races, i.e. no false warnings. It exploits the fact that every thread choice selection point could be due to a possible race. It just runs through all the thread choices and checks whether there are more than one thread trying to read & write to the same field of an object. Current limitation is that it is only sound, i.e. will not miss a race, if the sync-detection is switched off during model checking. This is due to the fact that the sync-detection guesses that an acess is lock-protected when it in reality might not be. The listener also checks races for array elements, but in order to do so you have to set "cg.threads.break_arrays=true" (note that it is false by default because this can cause serious state explosion) This algorithm came out of a discussion with Franck van Breugel and Sergey Kulikov from the University of York. All credits for it goes to Franck and Sergey, all the bugs are mine. NOTE - the PreciseRaceDetector is machine type agnostic Author: Willem Visser

Field Summary

Fields

Modifier and Type	Field and Description
protected StringSetMatcher	excludes
protected StringSetMatcher	includes
protected gov.nasa.jpf.listener.PreciseRaceDetector.Race	race

Constructor Summary

Constructors

Constructor and Description
PreciseRaceDetector(Config conf)

Method Summary

Modifier and Type	Method and Description
boolean	check(Search search, VM vm) return true if property is NOT violated
protected boolean	checkRace(ThreadInfo[] threads)
void	choiceGeneratorSet(VM vm, ChoiceGenerator<?> newCG) a new ChoiceGenerator was set, which means we are at the beginning of a new transition.
void	executeInstruction(VM vm, ThreadInfo ti, Instruction insnToExecute) VM is about to execute the next instruction
java.lang.String	getErrorMessage()
void	reset()

Methods inherited from class gov.nasa.jpf.PropertyListenerAdapter

choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorRegistered, classLoaded, clone, exceptionBailout, exceptionHandled, exceptionThrown, gcBegin, gcEnd, instructionExecuted, loadClass, methodEntered, methodExited, objectCreated, objectExposed, objectLocked, objectNotify, objectNotifyAll, objectReleased, objectShared, objectUnlocked, objectWait, propertyViolated, publishConstraintHit, publishFinished, publishProbe, publishPropertyViolation, publishStart, publishTransition, searchConstraintHit, searchFinished, searchProbed, searchStarted, stateAdvanced, stateBacktracked, stateProcessed, statePurged, stateRestored, stateStored, threadBlocked, threadInterrupted, threadNotified, threadScheduled, threadStarted, threadTerminated, threadWaiting, vmInitialized

Methods inherited from class gov.nasa.jpf.GenericProperty

getExplanation, printOn

Methods inherited from class java.lang.Object

equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

race

protected gov.nasa.jpf.listener.PreciseRaceDetector.Race race

includes

protected StringSetMatcher includes

excludes

protected StringSetMatcher excludes

Constructor Detail

PreciseRaceDetector

public PreciseRaceDetector(Config conf)

Method Detail

check

public boolean check(Search search,
                     VM vm)

Description copied from interface: Property

return true if property is NOT violated

Specified by:

check in interface Property

Overrides:

check in class PropertyListenerAdapter

reset

public void reset()

Specified by:

reset in interface Property

Overrides:

reset in class PropertyListenerAdapter

getErrorMessage

public java.lang.String getErrorMessage()

Specified by:

getErrorMessage in interface Property

Overrides:

getErrorMessage in class GenericProperty

checkRace

protected boolean checkRace(ThreadInfo[] threads)

choiceGeneratorSet

public void choiceGeneratorSet(VM vm,
                               ChoiceGenerator<?> newCG)

Description copied from interface: VMListener

a new ChoiceGenerator was set, which means we are at the beginning of a new transition. NOTE - this notification happens before the KernelState is stored, i.e. listeners are NOT allowed to alter the KernelState (e.g. by changing field values or thread states)

Specified by:

choiceGeneratorSet in interface VMListener

Overrides:

choiceGeneratorSet in class PropertyListenerAdapter

executeInstruction

public void executeInstruction(VM vm,
                               ThreadInfo ti,
                               Instruction insnToExecute)

Description copied from interface: VMListener

VM is about to execute the next instruction

Specified by:

executeInstruction in interface VMListener

Overrides:

executeInstruction in class PropertyListenerAdapter