Go backward to 1 IntroductionGo up to TopGo forward to 3 The Termination Detection Algorithm |

Figure 1: The Basic System

We are given a system with `n` processes numbered 0 to
`n`-1. Each process can send via buffered communication
channels messages to all other processes, i.e., there exist
`n`^{2} channels between all pairs of processes^{1}. Initially all processes are
active; a process may send messages only, if it is active. An active
process may spontaneously decide to become inactive (but not vice versa); on
receipt of a message, a process becomes active again.

Our problem is to design an algorithm that allows a process, say process 0, to detect whether the system has terminated, i.e., whether all processes in the system are inactive and all channels are empty. If the system has terminated, no process will ever become active again.

We model the system with the help of the following variables (see Figure 1):

`act`

inZ_{n}->B,`chan`

inZ_{n}xZ_{n}->Seq(MSG).

The variable `act`

represents a predicate (a boolean-valued function)
such that `act`

_{i} is true if and only if process `i` is
active (**Z**_{n} denotes the set {0,
...,
`n`-1}). The variable `chan`

represents the system
channels, i.e., `chan`

_{i, j} holds a sequence of
messages < `m`_{0}, ...`m`_{l-1} > (where every
`m`_{i} is an element of some domain `MSG`) that
were sent by process `i` but have not yet been received by process
`j`.

For specifying the system and the termination detection algorithm, we use
the language of temporal logic in a style close to TLA [Lam94]. A
system is identified with the set of its possible behaviors where a
behavior `s` is an infinite sequence of states

such that each

s=<s_{0},s_{1}, ... >

says that in steps_{i}(`act`

_{k})=false

We describe the set of system behaviors by logical formula of the following structure

/\

Init_{n}(`act`

,`chan`

)- [][
Action_{n}(`act`

,`chan`

)]

where a list of predicates bulleted with /\ denotes the conjunction of these predicates (and analogously for disjunction). The rest of this section explains the construction of this formula.

The initial state condition `Init` describes the values of the
variables `act`

and `chan`

in state `s`_{0}, i.e.,

Init_{n}(`act`

,`chan`

) :<=>/\

foralliinZ_{n}:`act`

_{i}foralliinZ_{n},jinZ_{n}:`chan`

_{i, j}=< > .

Since `Init` only constrains the variables in a single state, it is
a so called state predicate.

The predicate `Action` models the transition from one state to the
next, i.e., it describes a relation between any two subsequent states
`s`_{i} and `s`_{i+1}. We call such
a predicate an action. An action is denoted by a formula like

/\

`x`

`'`

=`x`

+`y`

`y`

`'`

=`y`

+1

which describes the relationship between the values of the variables `x`

and `y`

in state `s`_{i} and the values of these variables
in state `s`_{i+1} (denoted by `x`

`'`

and `y`

`'`

). Above formula therefore means

and roughly corresponds to the programming language statement/\

s_{i+1}(x)=s_{i}(`x`

)+s_{i}(`y`

)s_{i+1}(y)=s_{i}(`y`

)+1

x = x+y; y = y+1;

An action `A` is enabled in some state, written as
`Enabled` `A`, if there exists a possible successor state such
that the action models the relationship between both states (i.e., if an
action is not enabled in a state, it is not possible to execute the action in
that state). For instance, the action

is only enabled in a state in which`c`

=<`m`

`'`

> o`c`

`'`

`c`

holds a non-empty sequence
`m`

holds the first element of `c`

holds the rest of We denote by

the functionf[i|->v]

thus roughly corresponds to the programming language statement`a`

=`a`

[i|->`a`

_{i}+1]

a[i] = a[i]+1;

The temporal formula []`P` ("always `P`") describes a
property of whole behaviors: if `P` is a state predicate, then `P`
is true for every state `s`_{i} in every behavior `s`; if
`P` is an action, then `P` is true for every pair of states
`s`_{i} and `s`_{i+1}; iff `P` is itself a
temporal formula, `P` is true for every suffix
< `s`_{i}, `s`_{i+1}, ... > of the
behavior.

A formula of the form []`P` turns out to be too restrictive to
specify concurrent systems: we want to have
`S` => `T` whenever system `S` "implements" or
"refines" system `T`, i.e., `S` must fulfill all constraints of
`T` but may e.g. introduce new variables and actions on these
variables. However, then a step of `S` may only change variables
that are not visible in `T`, which is not allowed by the implication if
`T` is specified by a formula []`P` that constrains
*every* step of the system.

We therefore introduce the operator [`P`] informally defined as "if not
`P`, then all visible variables remain unchanged". The "next-state"
relation of a system is then specified by a formula [][`P`], which
allows "stuttering" steps, i.e., sequences of states in which none of the
visible variables changes (see below on the definition of "visibility").

The temporal formula <>`P` ("eventually `P`") is a
shortcut for ~[]~`P`, i.e., `P` must not be false
forever. The operator < `P` > is informally defined as
"`P` and some of the visible variables changes".

The operators [.] and < . > depend on the set of program variables that are "visible" in a specification. In order to make this set explicit, we parameterize every system specification by the set of all visible variables and interpret each occurence of these operators with respect to this set. For instance,

System_{n in N}(`act`

inZ_{n}->B,`chan`

inZ_{n}xZ_{n}->Seq(MSG))

has `act`

and `chan`

as visible program variables. As a visual and
mental aid, we usually include the expected variable types in such parameter
specifications. We use subscripts to denote parameterization by mathematical
variables, such as the mathematical variable `n` in above specification.

Likewise, each action defined in a specification is parameterized by the
variables referenced in this action. For instance, the action
`Inactivate` defined in

only refers to the variableSystem_{n in N}(`act`

inZ_{n}->B,`chan`

inZ_{n}xZ_{n}->Seq(MSG)) :<=>

let

...

Inactivate_{i}(`act`

) :<=>

`act`

`'`

=`act`

[i|-> false]- ...

`act`

. The body of the action is thus
implicitly conjoined with conditions that state that all variables remain
unchanged that are visible in the specification but are not referenced in the
body of the action, i.e.,
in above case.`chan`

`'`

=`chan`

We usually also tag every parameter of an action by a "qualifier":

**in**

signals that the variable`p`

`p`

occurs in the corresponding formula only in the unprimed form, i.e., the variable only appears as part of the enabling condition of the action constraining its value only in the "current" state.**out**

signals that`p`

`p`

occurs in the formula only in the primed form, i.e., it constrains the value of the variables only the "successsor" state.**io**

signals that`p`

`p`

occurs in the formula both in its primed and in its unprimed form and thus describes a relationship between the values of the variable in both states.

qualifiers. We freely skip the qualifier when we do not consider it
useful in some context.
Specification 1: The Basic System

`act`

`chan`

`Init`_{}(**in**`act`

,**in**`chan`

) :<=>

*(all processes are active, all channels are empty)***/\****forall**`i``in`**Z**_{n}:`act`

_{i}**forall**`i``in`**Z**_{n},`j``in`**Z**_{n}:`chan`

_{i, j}`=`< > ,

`Send`_{i, j}(**in**`a`

,**io**`chan`

) :<=>

*(active process*`i`sends some message to process`j`)**/\**`a`

**exists**`m``in``MSG`:`chan`

`'`

`=``chan`

[(`i`,`j`) |->`chan`

_{i, j}o <`m`> ],

`Receive`_{i, j}(**io**`act`

,**io**`chan`

) :<=>

*(having received some message from process*`i`, process`j`is active)**/\**`act`

`'`

`=``act`

[`j`|-> true]**exists**`m``in``MSG`:`chan`

`=``chan`

[(`'`

`i`,`j`) |-> <`m`> o`chan`

`'`

_{i, j}],

`Inactivate`_{i}(**io**`act`

) :<=>

*(process*`i`becomes inactive)`act`

`'`

`=``act`

[`i`|-> false],`Action`_{n, i}(**io**`act`

,**io**`chan`

) :<=>

*(process*`i`is involved in some action)**\/****exists**`j``in`**Z**_{n}:`Send`_{i, j}(**in**`act`

_{i},**io**`chan`

)**exists**`j``in`**Z**_{n}:`Receive`_{i, j}(**io**`act`

,**io**`chan`

)`Inactivate`_{i}(**io**`act`

):

*(initial state condition and transition relation)*
**/\**

`Init`_{}(**in**`act`

,**in**`chan`

)- [][
**exists**`i``in`**Z**_{n}:`Action`_{n, i}(**io**`act`

,**io**`chan`

)]

Having introduced the language of our specifications, we now continue with defining the actions of the system sketched at the start of this section:

Inactivate_{i}(io`act`

) :<=>

`act`

`'`

=`act`

[i|-> false],

says that process `i` may become inactive at any time (if it is already
inactive, this action does not have any effect). Sending a message is
expressed by

Send_{i, j}(in`a`

,io`chan`

) :<=>

/\

`a`

existsminMSG:`chan`

`'`

=`chan`

[(i,j) |->`chan`

_{i, j}o <m> ],

which is only enabled in a state where `a`

(to be instantiated by
`act`

_{i}) holds. In the successor state,
some message `m` is appended to the current content of channel
`chan`

_{i, j}. The action

Receive_{i, j}(io`act`

,io`chan`

) :<=>

/\

`act`

`'`

=`act`

[j|-> true]existsminMSG:`chan`

=`chan`

[(`'`

i,j) |-> <m> o`chan`

`'`

_{i, j}]

is only enabled in a state where `chan`

_{i, j} holds a
message `m`. In the successor state, `m` is removed from this
channel and `act`

_{j} is set to true (i.e., an inactive process
becomes active again).

The complete system description is compiled in Specification 1.

Maintainer: Wolfgang Schreiner

Last Modification: August 20, 1998