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

# 2 The System Model

Figure 1: The Basic System

#### Problem Statement

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 n2 channels between all pairs of processes1. 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` in Zn->B,
• `chan` in Zn x Zn->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 (Zn denotes the set {0, ..., n-1}). The variable `chan` represents the system channels, i.e., `chan`i, j holds a sequence of messages < m0, ...ml-1 > (where every mi is an element of some domain MSG) that were sent by process i but have not yet been received by process j.

#### Temporal Logic

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

s = < s0, s1, ... >
such that each si describes the values of all program variables in step i. For instance,
si(`act`k) = false
says that in step i process k is inactive.

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

/\
• Initn(`act`, `chan`)
• [][Actionn(`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.

#### Initial State Condition

The initial state condition Init describes the values of the variables `act` and `chan` in state s0, i.e.,

Initn(`act`, `chan`) :<=>
/\
• forall i in Zn: `act`i
• forall i in Zn, j in Zn: `chan`i, j = < > .

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

#### Actions

The predicate Action models the transition from one state to the next, i.e., it describes a relation between any two subsequent states si and si+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 si and the values of these variables in state si+1 (denoted by `x``'` and `y``'`). Above formula therefore means

/\
• si+1(x) = si(`x`)+si(`y`)
• si+1(y) = si(`y`)+1
and roughly corresponds to the programming language statement
```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

`c` = < `m``'` > o `c``'`
is only enabled in a state in which `c` holds a non-empty sequence c; in the successor state `m` holds the first element of c and `c` holds the rest of c.

We denote by

f[i |-> v]
the function g that is identical to f except for gi = v. The action
`a` = `a`[i |-> `a`i+1]
thus roughly corresponds to the programming language statement
```a[i] = a[i]+1;
```

#### Temporal Formulas

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 si in every behavior s; if P is an action, then P is true for every pair of states si and si+1; iff P is itself a temporal formula, P is true for every suffix < si, si+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".

#### Specification and Action Parameters

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,

Systemn in N(`act` in Zn->B, `chan` in Zn x Zn->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

Systemn in N(`act` in Zn->B, `chan` in Zn x Zn->Seq(MSG)) :<=>
let
• Inactivatei(`act`) :<=>
`act``'` = `act`[i |-> false]
• ...
...
only refers to the variable `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.,
`chan``'` = `chan`
in above case.

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

• in `p` signals that the variable `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 `p` signals that `p` occurs in the formula only in the primed form, i.e., it constrains the value of the variables only the "successsor" state.
• io `p` signals that `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.
Apparently a state predicate (such as the initial condition) only has in qualifiers. We freely skip the qualifier when we do not consider it useful in some context.

#### The System Specification

Specification 1: The Basic System

Systemn in N(`act` in Zn->B, `chan` in Zn x Zn->Seq(MSG)) :<=>
(a system with n processes, active or inactive, connected by channels)
let
• Init(in `act`, in `chan`) :<=>
(all processes are active, all channels are empty)
/\
• forall i in Zn: `act`i
• forall i in Zn, j in Zn: `chan`i, j = < > ,
• Sendi, 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 > ],
• Receivei, 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],
• Inactivatei(io `act`) :<=>
(process i becomes inactive)
• `act``'` = `act`[i |-> false],
• Actionn, i(io `act`, io `chan`) :<=>
(process i is involved in some action)
\/
• exists j in Zn: Sendi, j(in `act`i, io `chan`)
• exists j in Zn: Receivei, j(io `act`, io `chan`)
• Inactivatei(io `act`):

(initial state condition and transition relation)
/\

• Init(in `act`, in `chan`)
• [][exists i in Zn: Actionn, 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:

Inactivatei(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

Sendi, j(in `a`, io `chan`) :<=>

/\
• `a`
• exists m in MSG: `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

Receivei, j(io `act`, io `chan`) :<=>

/\
• `act``'` = `act`[j |-> true]
• exists m in MSG: `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