sofya.apps.atomicity
Class HappenBeforeChecker

java.lang.Object
  extended by sofya.ed.semantic.EventFilter
      extended by sofya.ed.semantic.EventSelectionFilter
          extended by sofya.apps.atomicity.HappenBeforeChecker
All Implemented Interfaces:
EventListener

public final class HappenBeforeChecker
extends EventSelectionFilter

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.

Version:
06/09/2006
Author:
Alex Kinneer

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.EventSelectionFilter
callReturnEvent, classPrepareEvent, constructorCallEvent, constructorExitEvent, exceptionCatchEvent, exceptionThrowEvent, executionStarted, interfaceCallEvent, monitorAcquireEvent, monitorContendEvent, monitorPreReleaseEvent, monitorReleaseEvent, newAllocationEvent, staticCallEvent, staticInitializerEnterEvent, staticMethodEnterEvent, staticMethodExitEvent, systemExited, systemStarted, virtualMethodEnterEvent, virtualMethodExitEvent
 
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

HappenBeforeChecker

public HappenBeforeChecker(DynamicEscapeDetector escapeDetector)
Creates a new happens-before checker.

Parameters:
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

isConcurrent

public 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.

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.

Parameters:
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.
Returns:
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).

threadStartEvent

public void threadStartEvent(EventListener.ThreadData td)
Description copied from interface: EventListener
Notification that a thread has started. These events are not dependent on the module description.

Specified by:
threadStartEvent in interface EventListener
Overrides:
threadStartEvent in class EventSelectionFilter
Parameters:
td - Information about the newly started thread.

threadDeathEvent

public void threadDeathEvent(EventListener.ThreadData td)
Description copied from interface: EventListener
Notification that a thread has terminated. These events are not dependent on the module description.

Specified by:
threadDeathEvent in interface EventListener
Overrides:
threadDeathEvent in class EventSelectionFilter
Parameters:
td - Information about the terminated thread.

virtualCallEvent

public void virtualCallEvent(EventListener.ThreadData td,
                             EventListener.CallData cd)
Description copied from interface: EventListener
Notification that a virtual method was called.

Specified by:
virtualCallEvent in interface EventListener
Overrides:
virtualCallEvent in class EventSelectionFilter
Parameters:
td - Information about the thread which called the method.
cd - Information about the called method.

staticFieldAccessEvent

public void staticFieldAccessEvent(EventListener.ThreadData td,
                                   EventListener.FieldData fd)
Description copied from interface: EventListener
Notification that a static field was read.

Specified by:
staticFieldAccessEvent in interface EventListener
Overrides:
staticFieldAccessEvent in class EventSelectionFilter
Parameters:
td - Information about the thread in which the field access occurred.
fd - Information about the accessed field.

instanceFieldAccessEvent

public void instanceFieldAccessEvent(EventListener.ThreadData td,
                                     EventListener.ObjectData od,
                                     EventListener.FieldData fd)
Description copied from interface: EventListener
Notification that an instance field was read.

Specified by:
instanceFieldAccessEvent in interface EventListener
Overrides:
instanceFieldAccessEvent in class EventSelectionFilter
Parameters:
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.

staticFieldWriteEvent

public void staticFieldWriteEvent(EventListener.ThreadData td,
                                  EventListener.FieldData fd)
Description copied from interface: EventListener
Notification that a static field was written.

Specified by:
staticFieldWriteEvent in interface EventListener
Overrides:
staticFieldWriteEvent in class EventSelectionFilter
Parameters:
td - Information about the thread in which the field write occurred.
fd - Information about the written field.

instanceFieldWriteEvent

public void instanceFieldWriteEvent(EventListener.ThreadData td,
                                    EventListener.ObjectData od,
                                    EventListener.FieldData fd)
Description copied from interface: EventListener
Notification that an instance field was written.

Specified by:
instanceFieldWriteEvent in interface EventListener
Overrides:
instanceFieldWriteEvent in class EventSelectionFilter
Parameters:
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.

constructorEnterEvent

public void constructorEnterEvent(EventListener.ThreadData td,
                                  EventListener.ObjectData od,
                                  EventListener.MethodData md)
Description copied from interface: EventListener
Notification that a constructor was entered.

This is the first point during the object creation process at which the object can be uniquely identified.

Specified by:
constructorEnterEvent in interface EventListener
Overrides:
constructorEnterEvent in class EventSelectionFilter
Parameters:
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.