sofya.apps.atomicity
Class RBAutomataExt52

java.lang.Object
  sofya.apps.atomicity.RBAutomata
      sofya.apps.atomicity.RBAutomataExt52

All Implemented Interfaces:

EventListener

public class RBAutomataExt52
extends RBAutomata

Extension of the atomicity checking automata that implements the regular expression described in Lemma 5.2 by Wang and Stoller.

Version:

12/20/2005

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

protected static int

ACCEPT_MATCH_R Constant indicating the automata is in the state where it will only accept a left-mover that matches the previous right mover (the two events are on the same lock).

Fields inherited from class sofya.apps.atomicity.RBAutomata

ACCEPT_L, ACCEPT_R, classifier, method, REJECT, state

Constructor Summary

RBAutomataExt52(EventClassifier classifier, MethodSignature method)
Creates a new reduction-based atomicity checking automata.

Method Summary

void	monitorAcquireEvent(EventListener.ThreadData td, EventListener.ObjectData od, EventListener.MonitorData md) Notification that a thread has acquired a monitor.
void	monitorReleaseEvent(EventListener.ThreadData td, EventListener.ObjectData od, EventListener.MonitorData md) Notification that a thread has released a monitor.
protected void	update(EventClassifier.EventClass eventClass) Updates the state of the automata based on the current event.

Methods inherited from class sofya.apps.atomicity.RBAutomata

callReturnEvent, classPrepareEvent, constructorCallEvent, constructorEnterEvent, constructorExitEvent, exceptionCatchEvent, exceptionThrowEvent, executionStarted, instanceFieldAccessEvent, instanceFieldWriteEvent, interfaceCallEvent, isAccepting, monitorContendEvent, monitorPreReleaseEvent, newAllocationEvent, staticCallEvent, staticFieldAccessEvent, staticFieldWriteEvent, staticInitializerEnterEvent, staticMethodEnterEvent, staticMethodExitEvent, systemExited, systemStarted, threadDeathEvent, threadStartEvent, virtualCallEvent, virtualMethodEnterEvent, virtualMethodExitEvent

Methods inherited from class java.lang.Object

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

Field Detail

ACCEPT_MATCH_R

protected static final int ACCEPT_MATCH_R

Constant indicating the automata is in the state where it will only accept a left-mover that matches the previous right mover (the two events are on the same lock). This implements the (L + AcqRel)* component of the extended regular expression.

See Also:

Constant Field Values

Constructor Detail

RBAutomataExt52

public RBAutomataExt52(EventClassifier classifier,
                       MethodSignature method)

Creates a new reduction-based atomicity checking automata.

Parameters:

classifier - Reference to the global event classifier, so that the published global classifications can be accessed if necessary.

method - Signature of the method for which this automata is to check for atomicity.

Method Detail

update

protected void update(EventClassifier.EventClass eventClass)

Updates the state of the automata based on the current event.

Overrides:

update in class RBAutomata

Parameters:

eventClass - Classification of the event as a left-mover, right-mover, non-mover, or both-mover.

monitorAcquireEvent

public void monitorAcquireEvent(EventListener.ThreadData td,
                                EventListener.ObjectData od,
                                EventListener.MonitorData md)

Description copied from interface: EventListener

Notification that a thread has acquired a monitor.

Specified by:

monitorAcquireEvent in interface EventListener

Overrides:

monitorAcquireEvent in class RBAutomata

Parameters:

td - Information about the thread which acquired a monitor.

od - Information about the object which owns the monitor.

md - Information about the location of the monitor acquisition.

monitorReleaseEvent

public void monitorReleaseEvent(EventListener.ThreadData td,
                                EventListener.ObjectData od,
                                EventListener.MonitorData md)

Description copied from interface: EventListener

Notification that a thread has released a monitor.

Specified by:

monitorReleaseEvent in interface EventListener

Overrides:

monitorReleaseEvent in class RBAutomata

Parameters:

td - Information about the thread which released a monitor.

od - Information about the object which owns the monitor.

md - Information about the location of the monitor release.