Invariance and nondeterminacy

Copyright Notice

The following manuscript

EWD 871: Invariance and Nondeterminacy

is held in copyright by The Royal Society and the author.

The manuscript was first published in

Philosophical Transactions of the Royal Society, Series A, Volume 312, 1984.

and subsequently as

C.A.R. Hoare and J.C. Shepherdson, eds., Mathematical Logic and Programming Languages, Prentice Hall International, 1985: 157-165.

Permission to reproduce the manuscript here has been granted by the Royal Society.

Invariance and Nondeterminacy

An accident introduced me 32 years ago to automatic computing, a topic that has fascinated me ever since. As the years go by, I am beginning to appreciate the length of my involvement more and more, since I owe to it a very lively picture of a sizeable part of the history of the growth of a science. I have observed profound changes in our thinking habits, and I have found those ob- servations interesting and instructive.

I do remember, for instance, one of my first efforts - in the mid 50's- to come to grips with what we would call now "repetition." It was profoundly inadequate, and in the course of this talk I hope to explain to you why. Very operationally, I tried to deal with it as a recurrence relation: one instructs the machine to start with an initial value $x_0$ and to generate from there enough values from the sequence further defined by the recurrence relation

x _ {i + 1} = f (x _ {i})

Why did I do that? I think because I was glad to recognize something familiar, and in those days Iliarity was more important than significance. The knowledge I had at the time was already sufficient to doubt the significance, but I don't remember I did. You see, a well-known concept was the "order" of a recurrence relation, the Fibonacci sequence

being given by the $2^{nd}$ -order recurrence rela-

tion

\overline {{t}} _ {n + 2} = \overline {{t}} _ {n + 1} + \overline {{t}} _ {n};

but any programmer would implement this by

(A, B) _ {n + 1} = (A + B, A) _ {n}

i.e. a 15-order recurrence relation! In short,

already then I should have been suspicious.

But it was the prevailing view in that decade: not only FORTRAN but even ALGOL60 included only repetitive constructs of which the so-called "controlled variable" was an essential ingredient.

My estimation is that the introduction of the so-called "controlled variable" has delayed the development of computing science by almost a decade. I got very suspicious in the late 60s when I discovered that the dyed-in-the-wool FORTRAN or ALGOL programmer had been conditioned so as to be unable to design the elegant solution to what became known as The Problem of the Dutch National Flag. The fact that, in the 70's, Euclid's Algorithm for the gcd of the positive integers X and Y became a paradigm I can only explain by the circumstance that it is the simplest program that demonstrates so convincingly the inappropriateness of the notion of the "controlled variable".

(Eudid's Algorithm became known in the form:

\begin{array}{l} \prod_ {x, y: i n t} \ ; x, y := X, Y \ ; \underline {{d o}} x > y \rightarrow x := x - y \ \begin{array}{r}\square y > x \rightarrow y := y - x\end{array} \ \prod^ {o d} \ \end{array}

This is evidently a repetition in which there is no place for a "controlled variable" counting something of relevance and/or controlling ter- mination.

Another accident - A.W.Dek's invention of the real-time interrupt- introduced me 25 years ago to nondeterminacy. My first major concern was to show that saving register contents at program interruption and restoring them at program resumption could not be corrupted by the occurrence of a next interrupt. The arguments required were very tricky, so tricky as a matter of fact that I was not surprised at all when I found flaws in the designs of the interrupt facilities of later machines such as the CDC 165 and the IBM 360. I experienced the problems caused by the unpredictable interleaving as completely novel ones, not suspecting that, about a decade later, they would be tackled by the same techniques that would then be used for reasoning about repetitions.

I am, of course, referring to the technique

of the so-called "invariant" as illustrated in the following type of annotation of a repetition -assertions being written within braces-

{P }

\frac {d o}{d p} \mathcal {B} \rightarrow {P \wedge B } S {P } \underline {{o d}}

In words: if assertion $P$ ,guard $B$ ,and statement S are such that the additional init. ial validity of $B$ guarantees that execution of $S$ does not destroy the validity of $P$ , then the whole repetition do $B \rightarrow S$ od will not destroy the validity of $P$ ,no matter how often the repeatable statement ’s is repeated.

Now, if we have, instead of a single $B \rightarrow S$ , a bunch of those, none of which destroys the validity of $P$ , the validity of $P$ will not be destroyed. no matter how often and in what order they are repeated. In other words, the pattern appropriate for reasoning about repetitions is straightforwardly able to cope with the nondeterminacy that has to be absorbed by the operating system for, say, a multiprogrammed installation.

The technique has been used rather constructively in the design of the THE Multiprogramming System to derive the synchronization conditions" (i.e. guards) that would ensure , for instance, that

no buffer would become emptier than empty or fuller than full. At the time we did not know the Axiom of Assignment; we only knew what it entailed for simple assignment statements, such as $n = n + 1$ , and equally simple P such as $n ≤ N$ . This was in the first half' of the 60's.

In the second half of the 60's, the method was formalized for deterministic sequential programs by R.W. Floyd and by C.A.R. Hoare. Floyd included proofs of termination, but addressed him-self to programs as could be expressed by arbitrary flow charts. (This latter generality was not too attractive. In the control graph one had to select a set of so-called "cutting edges", i.e. a set of edges such that their removal would leave a graph with no cycles, and to each cutting edge a proof obligation corresponded. The awkward thing is that for an arbitrary control graph, the problem of determining a minimum set of cutting edges is most unattractive.) Hoare's subsequent contribution was twofold: on account of the structure of the Axiom of Assignment he definitely decided in favour of so-called "backwards reason." Floyd had left this choice open- and he tried the proof obligations in with syntactic constructs for the flow of control. Ironically, he confined himself to partial correctness, though the problem of finding a minimum set of cutting

edges - which are required for termination proofs- had been reduced to trivially by the sequencing discipline he had adopted.) All this was synthetized in the early 70's by Edgior W. Dgkstra, whose "guaraded commands", besides forming a basis for a calculus for the derivation of programs, re-introduced nondeterminacy again.

Central to this game was the formal expression of so-called "assertions" or "conditions", i.e. predicates that contained the coordinates of the program's state space as free variables, and the formal manipulation of such expressions, e.g. in order to derive for a program fragment the precondition corresponding to a given postcondition. (It is this direction of the functional dependence to which the term "backwards reasoning" refers. The pragmatic advantages of backwards reasoning are twofold. It circumvents undefined values, since for any program fragment the precondition is a total function of the postcondition, whereas the postcondition is, in general, a partial function of the precondition. Furthermore, the calculus includes nondeterminacy at no extra cost at all.)

For the formulation and manipulation of these conditions, the predicate calculus became a vital tool, so much so that during the last decade it became for many a programming computing scientist an indispensable tool for his

daily reasoning. (In passing I may mention my strong impression that those computing scientists may very well have been the first to use the predicate calculus regularly. Mathematicians, and even logicians, for whom, for instance, the facts that equivalence is associative, that disjunction distributes over equivalence and that conjunction distributes over nonequivalence, belong to their active knowledge are extremely rare. I never met one. Without intimate knowledge of such basic properties of the logical connectives one can hardly be expected to be a very effective user of the predicate calculus. Hence my strong impression. In retrospect I found the conclusion, so to speak, that as far as the mathematical community is concerned George Boole has lived in vain, rather shocking.)

The extensive use of the predicate calculus in pro- gram derivation during the last decade has had a profound influence, the consequences of which are still unfathomed. It turned program development into a calculational activity (and the idea of pro- gram correctness into a calculational notion). The consequences are unfathomed because suddenly we find ourselves urgently invited to apply formal techniques on a much more grandiose scale than we were used to. It turns out that the predicate calculus only solves the problem "in principle": without careful choice of our extra-logical primitives

and their notation, the formulae to be manipulated have a tendency of becoming unmanageably complicated. As a result, each specific problem may pose a new conceptual and notational challenge. By way of illustration, I shall show an extreme example from the field of distributed programming; the example is extreme in the sense that almost all the manipulations of the derivation belong to the extra-logical calculus.

We consider a network of machines that can send messages to each other. Each machine is in 1 of 3 states, viz.

n for "neutrally engaged". for "delayed", or c for "critically engaged"

A critical engagement lasts only a finite period and is immediately followed by a neutral engagement of the machine in question. Between a neutral and the subsequent critical engagement a delay may occur in view of the requirement that at any moment at most 1 machine be critically engaged (so-called "mutual exclusion"). The implied synchronization has to be implemented in such a manner that no delay lasts forever (so-called "fairness").

We introduce a single token, either held by one of the machines or being sent from one machine to another. Mutual exclusion is then achieved by maintaining

a critically engaged machine holds the token. The machines maintain this by (i) not initiating a critical engagement unless holding the token, and (ii) not sending the token to another machine while being critically engaged.

Furthermore each machine maintains

the machine holding the token is not delayed by (i) skipping the delay upon termination of a neutral engagement while holding the token, and (ii) initiating a critical engagement upon receipt of the token while delayed. Fairness is therefore ensured when each delayed machine receives the token within a finite period of time.

The rest of this example deals with the control of the movement of the token. To this end the machines are arranged in a ring, the two circular directions in which are called "to the left" and "to the right" respectively. The token is sent to the left, so-called signals are sent to the right. Each link connecting two neighbouring machines in the ring is in 1 of 3 states, viz.

u for "unused" t for "carrying the token to the left" s for "carrying a signal to the right"

The latter two states are postulated to last only a finite period of time.

The computation will be broken up in so-called "atomic actions". (An "atomic action" is the same type of idealization as the "point mass" in physics.) Each atomic action is performed by one of the machines and involves a state change for that machine and for its link(s). There are four atomic actions to be designed:

(n) upon completion of a neutral engagement (c) upon completion of a critical engagement (s) upon arrival of a signal (t) upon arrival of the token.

(We need not bother about "completion of a delay" since this will be subsumed by the arrival of the token; similarly, the "completion" of the state "unused" for a link is subsumed in sending either the token or a signal over that link.)

Our invariant for the whole system is, loosely speaking, "the ring is in a permissible state", but this is only helpful provided we have a very pre- cise characterization of the set of permissible states. This set of permissible states will be derived as the transitive closure of the atomic transitions

From a given initial state, say: all machines neutrally engaged, all the links unused, and the token residing in one of the machines.

Immediately the question arises how to charac- terize sets of ring states. Since a string of the appropriate length, in which machine states and link states alternate, characterizes a ring state -by lying the string around-, we can characterize a set of ring states by writing down a grammar for representative strings. In this example we shall use the grammar of so-called "regular expressions".

It will turn out to be handy to give machines one of two colours, either black (b) or white (w), and a machine state will be coded by prefixing one of three states n , d , or c , by one of the colours b or w . The machine holding the token will be identified by writing its colour with the corresponding capital letter. Initially all machines being white, we can characterize the initial state by the regular expression

(0) - (w n u) ^ {*} W n u -

Note. If a regular expression is used to characterize a set of ring states, we shall surround it by a pair of dashes. This implies, for instance, that (o) is equivalent with

- (u w n) ^ {*} u W n -

(End of Note.)

In (0), the star * denotes "a succession of zero or more instances of the enclosed".

In (o), only completion of neutral engagements is possible. For the time being we confine our attention to the more interesting case of such completions taking place in machines not holding the token, and propose the transition

(n.o) $\operatorname{wn}u \rightarrow \operatorname{wd}s$

i.e. a white machine without the token completes its neutral engagement by becoming delayed and sending a signal over the link to its right. (Transition n.o only caters for the situation that a wn has a u to its right.)

The transitive closure of (0) under (n.o) is

in which $\mathbb{I}$ -which syntactically has been given the lowest binding power- should be read as "or".

For the arrival of a signal at a white neutral machine (note that (1) is equivalent to

- (w n u) w d s w d s w n u) ^ {*} W n u -

we propose the transition

(s.o)

i.e. the machine transmits the signal and blackens itself. The transitive closure of (o) under (n.o) and

(s.o) is given by

- (w n u ] w d (u b n) ^ {} s) ^ {} W n u -

Closing this furthermore under

(n.1) $u {bn} \rightarrow u {bd}$ [\text{S.1}]

yields

- (w n u \Vert w d (u b n \Vert u b d) ^ {} s) ^ {} W n u -,

which we record as

(2) $- {H}^{ * }{W}{n}u =$ with (3) $H = \operatorname{wn}u∥ Qs$ with $Q = {wd}\left( {u{b}{n}$ 11 $u {bd}}\right)$

We note that the grammars $H, H^{}$ , and $H^{}Q$ -note the absence of dashes: these grammars correspond to sets of strings- are also closed under the four transitions considered so far. [The reader is not expected to see this at a glance: the formal verification of the above requires a -be it short- calculation.] Furthermore we note that under the transitions given so far the transitive closure of the string wn u H* equals $H H^{*}$

Let us now look at the more interesting case that a signal arrives at the machine

holding the token. The only way in which we can make in (2) the substring s Wn explicit is by adding the superfluous term Q s Wn u

- H ^ {*} (W _ {n} u) \cap Q = W _ {n} u) - \cdot ,

which we can close under

(5.2) $s {W}{n} \sim + {f}{n}u$

by applying (s.2) now as rewrite rule:

- H ^ {*} (W n u) Q + w n u) -

As a result of the emergence of a new instance of wn u , this is no longer closed under the previous transformations, but we have seen that the closure yields

(5) $- {H}^{ * }\left( {{W}_{n}u\mathbb{I}Q + H}\right) -$

Closing (5) under

(n.2) $\operatorname{Wn}u \rightarrow \operatorname{Wc}u$

obviously yields

(6) $- {H}^{ * }\left( {{W}{n}u∥ {W}{n}u}\right) Q + H -$

which is also closed under the inverse

(c.o) ${W}{c}u \rightarrow {W}{n}u$

with the introduction of the term We u we have created the possibility of a signal

arriving at the critically engaged machine (that holds the token). Observing that in (6) the substring is We can only occur in Q s Wc u , adding this as superfluous term , and applying the transition

(5.3) $S ⇒ u \rightarrow u$ BC $u$

as rewrite rule, we derive the closure

(7) $- {H}^{ * }\left( {{W}{n}u∥ {W}{c}u∥ Q + H∥ Q}uB\left( u\right) -$

The introduction of the term Bc intro- duces a new form of critical engagement, which may terminate, for which we suggest the transition

(c.1) $u B\left( {u \rightarrow + w}\right) u$

Since the resulting Q+WN u is sub- sumed by the preceding Q+H , (7) is closed under (c.1) as well.

We leave to the reader the verification that (7) is also closed under the remain- ing three transitions that enumerate how the token can arrive

$\left( {t,0}\right)$ ${wd} + \rightarrow {Wc} \sim$

$\left( {k,1}\right) u {b}{n} + \rightarrow t {w}{n}u$

(+2) $u {bd} + \rightarrow u {Bc} \sim u$

Since (7) tells us that $t$ has a string Q

the construction of the closure and of the list of transitions that might be needed has now been completed.

The above enables us to convince ourselves that each delay will be of finite duration. To that purpose we associate with a delayed machine the string of (alternating) links and machines to its right, up to and including the machine that holds or the link that carries the token. For that string we define $k$ by

$k =$ the number of elements in the string $+$ the number of white machines in the string.

To begin with we observe that $k ≥ 0$ and that none of the transitions increase $k$ . We now convince ourselves that $k$ decreases within a finite period of time because the states $s, t$ , and $c$ are of finite duration:

from (7) and (4) we conclude that the delayed machine occurs in a Q;

(i) for a $Q$ in $H$ ,the string contains an s, and within a finite time s.o,s.l,s.2,or s.3 will decrease k (ii) for the $Q$ in $Q + H,t,0,t,1,$ or t.2 will decrease k within a finite time. (iii) for the $\mathcal{Q}$ in $Q \cup {B}_{C}u,c$ ,will decrease $k$ within a finite time.

and from (7) we conclude that this case analysis has been exhaustive.

And this concludes (the compact presentation of) our example.

A number of retrospective remarks are in order.

In the above, the machines themselves have rema nained anonymous. We could have numbered them from 0 through N-1, but invite the reader to try to visualize how our invariant (7) would have looked like, had we used quantifications over machine subscripts! It would have been totally unmanageable. (Not only did we leave the individu al machines anonymous, but even their number is not mentioned in the analysis: for a ring of N machines, only the strings of length 2.N that belong to the grammar (7) are applicable. A fringe benefit is that very small values of N do not require a special analysis.)

After the decision to try to use regular expressions, it took me several iterations before I had reached the above treatment. My first efforts contained errors, due to my lack of experience in using the "regularity calculus" for deriving a transitive closure under rewrite rules.

The lack of experience was the more severe since the same language can be characterized by

many different regular expressions: for instance, (a) $b$ ),(a) $b$ a $b$ ),(a) $b$ a*) are all equivalent. In the beginning I experienced this great freedom as a nuisance, but now I think this was naive, since precisely these language-preserving transformations enable us to massage a regular expression in a form suitable for our next manipulation. Equivalences lie at the heart of any practical calculus.

Finally, it took me quite some time before I dis- covered the proper abbreviations to introduce. (The H and the Q ,easy to defend in hindsight, could have been chosen much earlier, had we had more familiarity with the regularity calculus.)

I mentioned that, due to the calculational ap-. proach to program design, each specific problem may pose a new conceptual and notational chal- lenge. The above example has been included to give the reader some feeling for the forms that challenge may take. I called the consequences of this recent development still unfathomed, the reason being that the machines executing our programs are truly worthy of the name general-purpose equipment" and that, consequently, the area that calls for the effective application of formal techniques seems to have lost its boundaries.

Acknowledgements. The example illustrating the use of the regularity calculus was developed under the critical inspiration of the Tuesday Afternoon Club, and of F.E.J. Kruseman Aretz in particular. It was a privilege to write half of the above with A.J.M. van Gasteren looking over my shoulder.

The above has been written by way of con- tribution to the Royal Society Discussion Meeting on "Mathematical Logic and Programming Languages, organized by Sir Michael Atiyah, F.R.S., Professor C.A.R. Hoare, F.R.S., and Professor J.C. Shepherdson and to be held in London, 15-16 February 1984.

Plataanstraat 5

5671 AL NUENEN

The Netherlands

1 February 1984

prof.dr.Edsger W.Dgkstra

Burroughs Research Fellow