org.jcsp.nxt.lang
Class Alternative

java.lang.Object
  org.jcsp.nxt.lang.Alternative

public class Alternative
extends java.lang.Object

This enables a process to wait passively for and choose between a number of Guard events.

Shortcut to the Constructor and Method Summaries.

Description

The Alternative class enables a CSProcess to wait passively for and choose between a number of Guard events. This is known as ALTing.

Note: for those familiar with the occam multiprocessing language, this gives the semantics of the ALT and PRI ALT constructs, extended with a built-in implementation of the classical FAIR ALT.

The Alternative constructor takes an array of guards. Processes that need to Alt over more than one set of guards will need a separate Alternative instance for each set.

types of Guard provided in org.jcsp.lang:

• AltingChannelInputInt: integer channel input -- ready if unread data is pending in the channel.

By invoking one of the following methods, a process may passively wait for one or more of the guards associated with an Alternative object to become ready. The methods differ in the way they choose which guard to select in the case when two or more guards are ready:

• fairSelect waits for one or more of the guards to become ready. If more than one become ready, it prioritises its choice so that the guard it chose the last time it was invoked has lowest priority this time. This corresponds to a common occam idiom used for real-time applications. If fairSelect is used in a loop, a ready guard has the guarantee that no other guard will be serviced twice before it will be serviced. This enables an upper bound on service times to be calculated and ensures that no ready guard can be indefinitely starved.

Implementation Footnote

This Alternative class and the various channel classes (e.g. One2OneChannelInt) are mutually dependent monitors -- they see instances of each other and invoke each others' strongly interdependent methods. This logic is inspired by the published algorithms and data structures burnt into the microcode of the transputer some 15 years ago (1984). Getting this logic `right' in the context of Java monitors is something we have done (n + 1) times, only to find it flawed n times with an unsuspected race-hazard months (sometimes years) later. Hopefully, we have it right now ... but a proof of correctness is really needed!

To this end, a formal (CSP) model of Java's monitor primitives (the synchronized keyword and the wait, notify and notifyAll methods of the Object class) has been built. This has been used for the formal verification of the JCSP implementation of channel read and write, along with the correctness of 2-way channel input Alternatives. Details and references are listed under `A CSP Model for Java Threads' on the JCSP web-site. [The proof uses the FDR model checker. Model checkers do not easily allow verification of results containing free variables - such as the correctness of the n-way Alternative. An investigation of this using formal transformation of one system of CSP equations into another, rather than model checking is being considered.]

The transputer designers always said that getting its microcoded scheduler logic right was one of their hardest tasks. Working directly with the monitor concept means working at a similar level of difficulty for application programs. One of the goals of JCSP is to protect users from ever having to work at that level, providing instead a range of CSP primitives whose ease of use scales well with application complexity - and in whose implementation those monitor complexities are correctly distilled and hidden.

Author:

P.H.Welch, P.D.Austin, Alex Panayotopoulos

See Also:

,

Field Summary

protected java.lang.Object

altMonitor The monitor synchronising the writers and alting reader

Constructor Summary

Alternative(Guard[] guard)
Construct an Alternative object operating on the Guard array of events.

Method Summary

int	fairSelect() Returns the index of one of the ready guards.
int	fairSelect(boolean[] preCondition) Returns the index of one of the ready guards whose preCondition index is true.
(package private) void	schedule() This is the wake-up call to the process ALTing on guards controlled by this object.
int	select() Returns the index of one of the ready guards.
int	select(boolean[] preCondition) Returns the index of one of the ready guards whose preCondition index is true.
(package private) void	setTimeout(int msecs) This is the call-back from a CSTimer guard.

Methods inherited from class java.lang.Object

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

Field Detail

altMonitor

protected java.lang.Object altMonitor

The monitor synchronising the writers and alting reader

Constructor Detail

Alternative

public Alternative(Guard[] guard)

Construct an Alternative object operating on the Guard array of events. Supported guard events are channel inputs (AltingChannelInput and AltingChannelInputInt), CALL channel accepts (AltingChannelAccept), timeouts (CSTimer) and skips (Skip).

Parameters:

guard - the event guards over which the select operations will be made.

Method Detail

select

public final int select()

Returns the index of one of the ready guards. The method will block until one of the guards becomes ready. If more than one is ready, an arbitrary choice is made.

fairSelect

public final int fairSelect()

Returns the index of one of the ready guards. The method will block until one of the guards becomes ready. Consequetive invocations will service the guards `fairly' in the case when many guards are always ready. Implementation note: the last guard serviced has the lowest priority next time around.

select

public final int select(boolean[] preCondition)

Returns the index of one of the ready guards whose preCondition index is true. The method will block until one of these guards becomes ready. If more than one is ready, an arbitrary choice is made.

Note: the length of the preCondition array must be the same as that of the array of guards with which this object was constructed.

Parameters:

preCondition - the guards from which to select

fairSelect

public final int fairSelect(boolean[] preCondition)

Returns the index of one of the ready guards whose preCondition index is true. The method will block until one of these guards becomes ready. Consequetive invocations will service the guards `fairly' in the case when many guards are always ready. Implementation note: the last guard serviced has the lowest priority next time around.

Note: the length of the preCondition array must be the same as that of the array of guards with which this object was constructed.

Parameters:

preCondition - the guards from which to select

setTimeout

void setTimeout(int msecs)

This is the call-back from a CSTimer guard. It is still in the flow of control of the ALTing process.

schedule

void schedule()

This is the wake-up call to the process ALTing on guards controlled by this object. It is in the flow of control of a process writing to an enabled channel guard.