previous up next
Go up to A The Scheduler Protocol
Go forward to A.2 Message Passing
RISC-Linz logo

A.1 Protocol Variables

The protocol is expressed in terms of the following program variables:

S: String
denotes the current status of the program.
T: String
denotes a substatus, i.e., a refinement of the current status; T may take the special constant `null'.
version: String
identifies the version of the protocol that the application program understands.
taskStack: Array[Message]
denotes the stack of task messages that were received by the external application program and for which it has not yet delivered corresponding results; a result may be only delivered for the task on the top of the stack.
taskDepth: Natural
denotes the number of elements on the task stack.
waitStack: Array[Message]
denotes the stack of wait messages that were sent by the external application program and for which it has not yet received corresponding replies; a reply can be only received for the wait message on the top of the stack.
waitDepth: Natural
denotes the number of elements on the wait stack.
taskId: TaskId
describes the identifier used to denote the next task to be created.
taskMin: TaskId
describes the lower bound of the range of identifiers that may be used to denote new tasks.
taskMax: TaskId
describes the upper bound of the task identifier range.

We use the following types in variable annotations of the form v: T to assert that v must be an element of the set T:

String
An arbitrary sequence of characters not including the newline character.
Command
A string that may be evaluated as a command by the application program.
Expression
A string that may be evaluated as an expression by the application program.
Integer
An integer number.
Natural
A non-negative integer number.
TaskId
A natural number that identifies a task.
Array[T]
An indexable array of elements of type T.
Message
A record m such that m.key is a string denoting the type of a message and m.body is an array of strings.

In our protocol specification, Integers are implicitly converted to strings (using thee textual representation of an integer as its string encoding). Likewise we assume that there is some encoding of commands and expressions as strings.


Maintainer: Wolfgang Schreiner
Last Modification: July 6, 2001

previous up next