|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object sofya.ed.semantic.EventFilter sofya.ed.semantic.EventSelectionFilter sofya.apps.atomicity.HappenBeforeChecker
public final class HappenBeforeChecker
Implementation of the happens-before analysis described by Wang and Stoller, with the exception that vector clocks are used. The vector clock implementation is an adaptation of the hybrid limited happens-before detection algorithm described by O'Callahan and Choi (the lockset portion is factored out in a manner consistent with the multi-lockset algorithm described by Wang and Stoller).
Additionally note that this implementation uses "sparse" vector clocks: a clock is a set of mappings from each thread ID to the current clock value for that thread. The map implementation returns 0 for an absent mapping, thus a clock value is only explicitly stored if it is greater than zero. This improves memory efficiency by avoiding allocating potentially large spans of empty elements, as would be necessary with arrays or vectors.
Nested Class Summary |
---|
Nested classes/interfaces inherited from interface sofya.ed.semantic.EventListener |
---|
EventListener.Arguments, EventListener.CallData, EventListener.ExceptionData, EventListener.FieldData, EventListener.MethodData, EventListener.MonitorData, EventListener.NewAllocationData, EventListener.ObjectData, EventListener.ThreadData, EventListener.ThreadStatus |
Field Summary |
---|
Fields inherited from class sofya.ed.semantic.EventFilter |
---|
listenerCount, listeners |
Constructor Summary | |
---|---|
HappenBeforeChecker(DynamicEscapeDetector escapeDetector)
Creates a new happens-before checker. |
Method Summary | |
---|---|
void |
constructorEnterEvent(EventListener.ThreadData td,
EventListener.ObjectData od,
EventListener.MethodData md)
Notification that a constructor was entered. |
void |
instanceFieldAccessEvent(EventListener.ThreadData td,
EventListener.ObjectData od,
EventListener.FieldData fd)
Notification that an instance field was read. |
void |
instanceFieldWriteEvent(EventListener.ThreadData td,
EventListener.ObjectData od,
EventListener.FieldData fd)
Notification that an instance field was written. |
boolean |
isConcurrent(int threadId,
long objId,
java.lang.String fieldName,
boolean isWrite)
Reports whether a memory access performed by the current thread could potentially be concurrent with other accesses to the same memory location. |
void |
staticFieldAccessEvent(EventListener.ThreadData td,
EventListener.FieldData fd)
Notification that a static field was read. |
void |
staticFieldWriteEvent(EventListener.ThreadData td,
EventListener.FieldData fd)
Notification that a static field was written. |
void |
threadDeathEvent(EventListener.ThreadData td)
Notification that a thread has terminated. |
void |
threadStartEvent(EventListener.ThreadData td)
Notification that a thread has started. |
void |
virtualCallEvent(EventListener.ThreadData td,
EventListener.CallData cd)
Notification that a virtual method was called. |
Methods inherited from class sofya.ed.semantic.EventFilter |
---|
addEventListener, ensureCapacity, removeEventListener |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Constructor Detail |
---|
public HappenBeforeChecker(DynamicEscapeDetector escapeDetector)
escapeDetector
- Dynamic escape detector that is used to determine
when to start recording clock events for memory accesses. Clock events
are not recorded for memory accesses to objects that have not yet
been reported as escaped from their creating thread.Method Detail |
---|
public boolean isConcurrent(int threadId, long objId, java.lang.String fieldName, boolean isWrite)
The current thread's vector clock is compared against the stored clock value for previously recorded events on the same memory location, as described by O'Callahan and Choi in their hybrid technique. It is provable that for determining basic happens-before causal relationships, the full vector clock does not need to be stored for the previously recorded events, and their clock values for other threads are implicitly taken to be zero.
If the current memory access is a read event, it is only checked for concurrency with other write events, otherwise the current memory access is checked for concurrency with all previous accesses.
threadId
- ID of the thread that performed the memory access.objId
- ID of the object owning the memory location (field);
-1 signifies a static field.fieldName
- Name of the memory location.isWrite
- Flag indicating whether the memory access is a write
access.
true
if the current memory access is possibly
concurrent with previous accesses to the same memory location
(e.g. there exists at least one previous access to the same memory
location that did not necessarily have to occur before the current
access to that memory location).public void threadStartEvent(EventListener.ThreadData td)
EventListener
threadStartEvent
in interface EventListener
threadStartEvent
in class EventSelectionFilter
td
- Information about the newly started thread.public void threadDeathEvent(EventListener.ThreadData td)
EventListener
threadDeathEvent
in interface EventListener
threadDeathEvent
in class EventSelectionFilter
td
- Information about the terminated thread.public void virtualCallEvent(EventListener.ThreadData td, EventListener.CallData cd)
EventListener
virtualCallEvent
in interface EventListener
virtualCallEvent
in class EventSelectionFilter
td
- Information about the thread which called the method.cd
- Information about the called method.public void staticFieldAccessEvent(EventListener.ThreadData td, EventListener.FieldData fd)
EventListener
staticFieldAccessEvent
in interface EventListener
staticFieldAccessEvent
in class EventSelectionFilter
td
- Information about the thread in which the field access
occurred.fd
- Information about the accessed field.public void instanceFieldAccessEvent(EventListener.ThreadData td, EventListener.ObjectData od, EventListener.FieldData fd)
EventListener
instanceFieldAccessEvent
in interface EventListener
instanceFieldAccessEvent
in class EventSelectionFilter
td
- Information about the thread in which the field access
occurred.od
- Information about the object which owns the accessed field.fd
- Information about the accessed field.public void staticFieldWriteEvent(EventListener.ThreadData td, EventListener.FieldData fd)
EventListener
staticFieldWriteEvent
in interface EventListener
staticFieldWriteEvent
in class EventSelectionFilter
td
- Information about the thread in which the field write
occurred.fd
- Information about the written field.public void instanceFieldWriteEvent(EventListener.ThreadData td, EventListener.ObjectData od, EventListener.FieldData fd)
EventListener
instanceFieldWriteEvent
in interface EventListener
instanceFieldWriteEvent
in class EventSelectionFilter
td
- Information about the thread in which the field write
occurred.od
- Information about the object which owns the written field.fd
- Information about the written field.public void constructorEnterEvent(EventListener.ThreadData td, EventListener.ObjectData od, EventListener.MethodData md)
EventListener
This is the first point during the object creation process at which the object can be uniquely identified.
constructorEnterEvent
in interface EventListener
constructorEnterEvent
in class EventSelectionFilter
td
- Information about the thread executing the constructor.od
- Information about the object under construction.
At the time of this event, only the object ID will be
valid.md
- Information about the entered constructor.
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |