uk.ac.man.cs.rainbow.simulator
Class RainbowThread

java.lang.Object
  |
  +--uk.ac.man.cs.rainbow.simulator.RainbowThread

Direct Known Subclasses:

RainbowDevice, RASMThread

public abstract class RainbowThread

extends Object

Superclass of all Rainbow threads. Threads are schedulable objects that are used to implement the behaviour of the Rainbow system for simulation and state enumeration (for deadlock and temporal model checking.)

See Also:

Scheduler, Rainbow Implementors Guide

Inner Class Summary

static class	RainbowThread.IllegalChannelStateException Indicate an attempt to do something naughty with a channel.
static class	RainbowThread.IllegalThreadTerminationException Indicate an attempt to do exit a top-level thread.
static class	RainbowThread.SavedRainbowThreadState For saving our state.

Field Summary

static int	AFTER_CHOICE Used to indicate (in some cases) that the thread is executing immediately after making a non-deterministic choice.
static int	BACKWARD Used to indicate that the thread is executing backwards.
static int	FORWARD Used to indicate that the thread is executing forwards.
static int	INITIALISE Used to indicate that the thread is initialising itself.
protected Scheduler	scheduler This thread's scheduler.

Constructor Summary

RainbowThread(RainbowThread parent)
Create a new thread that is a child of the given thread.

RainbowThread(Scheduler scheduler)
Create a new top-level thread in the given scheduler.

Method Summary

abstract Data	characterise() Characterise this thread.
boolean	choice(int choiceRange) Request a non-deterministic choice.
boolean	delay(int delay) Request that this thread should be delayed for a bit.
protected abstract void	execute() Make this thread execute in the current direction.
void	execute(int direction) Make this thread execute in the specified direction.
void	exitSelf() Make the current thread terminate.
int	getChoice() What non-deterministic choice was taken?
int	getChoiceRange() Over what values should a non-deterministic choice be made?
int	getDirection() What direction is this thread executing in?
Data	getFromChannel(Channel chan) Read a value off a channel.
RainbowThread	getParent() Get this thread's parent thread.
boolean	isAvailable(Channel chan) Test whether the given channel is available.
void	loadState(SavedState saved) Reload a previously saved state.
void	putToChannel(Channel chan, Data value) Put a value onto a channel.
boolean	release(Channel chan) Release the given channel.
SavedState	saveState() Save the state of this thread.
protected RainbowThread	scheduleChild(RainbowThread child) Schedule the thread for execution.
protected void	setChoice(int choice) Set what non-deterministic choice was taken.
boolean	signalForward(Channel chan) Attempt to transfer the value currently on the channel to the other end.
void	sleep() Mark this thread as wanting to yield.
boolean	stillBusy(Channel chan) Test to see if the target end has finished reading from the channel.
String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

FORWARD

public static final int FORWARD

Used to indicate that the thread is executing forwards.

See Also:

execute(int)

BACKWARD

public static final int BACKWARD

Used to indicate that the thread is executing backwards.

See Also:

execute(int)

INITIALISE

public static final int INITIALISE

Used to indicate that the thread is initialising itself.

See Also:

execute(int), Scheduler.initialise()

AFTER_CHOICE

public static final int AFTER_CHOICE

Used to indicate (in some cases) that the thread is executing immediately after making a non-deterministic choice.

See Also:

execute(int), NDChoice, StateEnumerator

scheduler

protected Scheduler scheduler

This thread's scheduler.

Constructor Detail

RainbowThread

public RainbowThread(Scheduler scheduler)

Create a new top-level thread in the given scheduler.

Parameters:

scheduler - The scheduler that will schedule the created thread.

RainbowThread

public RainbowThread(RainbowThread parent)

Create a new thread that is a child of the given thread.

Parameters:

parent - The thread that the created thread will be a child of.

Method Detail

execute

public final void execute(int direction)
                   throws RainbowException

Make this thread execute in the specified direction.

Parameters:

direction - Which direction to execute in.

Throws:

RainbowException - If something goes wrong during the thread's execution.

See Also:

FORWARD, BACKWARD, INITIALISE, execute()

execute

protected abstract void execute()
                         throws RainbowException

Make this thread execute in the current direction.

Throws:

RainbowException - If something goes wrong during the thread's execution.

See Also:

execute(int), getDirection()

characterise

public abstract Data characterise()

Characterise this thread. When the value by this method changes, the state of the thread has changed in such a way as to indicate that its future behaviour will be different.

Returns:

A value that encapsulates the state of this thread.

See Also:

StateEnumerator.characterise(Data[])

setChoice

protected void setChoice(int choice)

Set what non-deterministic choice was taken.

See Also:

Scheduler

getChoice

public int getChoice()

What non-deterministic choice was taken?

getChoiceRange

public int getChoiceRange()

Over what values should a non-deterministic choice be made?

getDirection

public int getDirection()

What direction is this thread executing in?

See Also:

FORWARD, BACKWARD, INITIALISE, AFTER_CHOICE

getParent

public RainbowThread getParent()

Get this thread's parent thread.

Returns:

null if this is a top-level thread.

getFromChannel

public final Data getFromChannel(Channel chan)
                          throws RASMThread.Exception

Read a value off a channel.

Throws:

RainbowThread.IllegalChannelStateException - If the channel is not activated.

See Also:

Channel.getContents(), Get

putToChannel

public final void putToChannel(Channel chan,
                               Data value)
                        throws RASMThread.Exception

Put a value onto a channel.

Throws:

RainbowThread.IllegalChannelStateException - If the channel is activated.

See Also:

Channel.setContents(Data), Put

signalForward

public final boolean signalForward(Channel chan)

Attempt to transfer the value currently on the channel to the other end. Handles interactions with the scheduler to wake up the far end correctly if there is a thread waiting there. All signalling from a channel writer to a channel reader must use this method.

Returns:

Whether to suspend this thread and retry the operation.

See Also:

Scheduler, SignalForward

stillBusy

public final boolean stillBusy(Channel chan)

Test to see if the target end has finished reading from the channel.

See Also:

WaitRelease

isAvailable

public final boolean isAvailable(Channel chan)

Test whether the given channel is available. Note that it also marks the thread as being interested in notifications of when the channel becomes active if the channel is not currently active.

Parameters:

chan - The channel to test for availability.

Returns:

Whether the channel was available.

See Also:

getFromChannel(Channel), release(Channel), IsAvailable

release

public final boolean release(Channel chan)

Release the given channel. Acknowledges the receipt of the value that was written on the channel.

Parameters:

chan - The channel to release.

Returns:

Whether the thread should yield. If the thread should yield, then the operation was not successfully completed and should be reattempted when the thread next executes.

See Also:

Release

sleep

public final void sleep()

Mark this thread as wanting to yield. The calling code should actually perform the yielding itself, but for the semantics of some of the other operations it is vital that this method be called.

delay

public final boolean delay(int delay)

Request that this thread should be delayed for a bit.

Parameters:

delay - How long to delay the thread for.

Returns:

Whether the thread should yield to the scheduler.

Throws:

IllegalArgumentException - If the delay is less than zero.

choice

public final boolean choice(int choiceRange)

Request a non-deterministic choice.

Parameters:

choiceRange - One more than the maximum value that can be chosen (the minimum is 0)

Returns:

True if the thread should drop out to the simulator to let the choice be made, or false if there is no valid choice to make and the system should not let itself be rescheduled.

exitSelf

public final void exitSelf()
                    throws RainbowException

Make the current thread terminate.

Throws:

RainbowException - If this thread is a top-level thread.

scheduleChild

protected final RainbowThread scheduleChild(RainbowThread child)

Schedule the thread for execution. Called when a thread is starting to execute.

Parameters:

child - The thread to schedule. Must be a child of this thread.

saveState

public SavedState saveState()

Save the state of this thread. Should be overridden by subclasses, which should then call this to return a token representing their superclass's state to incorporate into their own saved state.

Returns:

A saved state token for loading later.

See Also:

StateEnumerator.saveState(), loadState(SavedState)

loadState

public void loadState(SavedState saved)

Reload a previously saved state. Should be overridden by subclasses, which should then call this to reload the state of their superclass. Note that this method enforces the restriction that saved states can only ever be reloaded into their creator, so subclasses that call this method do not need to separately enforce that.

Parameters:

saved - The saved state token to reload.

Throws:

IllegalArgumentException - If the state token was not created by this thread.

See Also:

StateEnumerator.restoreState(SavedState), saveState()

toString

public String toString()

Overrides:

toString in class Object