| |
|
| gov.nasa.jpf.PropertyListenerAdapter gov.nasa.jpf.tools.RaceDetector
RaceDetector | public class RaceDetector extends PropertyListenerAdapter (Code) | | Simple field access race detector example
This implemenation so far doesn't deal with synchronization via signals, it
only checks if the lockset intersections of reads and writes from different
threads get empty. A more sophisticated version would check if the two
suspicious access operations (one read, one write) will also happen in reverse
order (that's the beauty of using this inside a model checker)
|
Inner Class :static class FieldAccess | |
Inner Class :static class FieldAccessSequence | |
fields | HashMap fields(Code) | | private fields and methods ***************************************
|
raceField | FieldAccessSequence raceField(Code) | | |
terminate | boolean terminate(Code) | | |
verifyCycle | boolean verifyCycle(Code) | | |
check | public boolean check(VM vm, Object arg)(Code) | | GenericProperty *************************************************
|
instructionExecuted | public void instructionExecuted(VM vm)(Code) | | VMListener ******************************************************
|
stateAdvanced | public void stateAdvanced(Search search)(Code) | | SearchListener ***************************************************
|
stateBacktracked | public void stateBacktracked(Search search)(Code) | | |
|
|
|