NOTE: This transcription was contributed by Martin P.M. van der Burgt, who has devised a process for producing transcripts automatically. Although its markup is incomplete, we believe it serves a useful purpose by virtue of its searchability and its accessibility to text-reading software. It will be replaced by a fully marked-up version when time permits. —HR
Copyright Notice
The following manuscript | |
EWD 608 An elephant inspired by the Dutch National Flag | |
is held in copyright by Springer-Verlag New York. | |
The manuscript was published as pages 264–267 of | |
Edsger W. Dijkstra, Selected Writings on Computing: A Personal Perspective, | |
Springer-Verlag, 1982. ISBN 0–387–90652–5. | |
Reproduced with permission from Springer-Verlag New York. | |
Any further reproduction is strictly prohibited. |
An elephant inspired by the Dutch National Flag.
Encouraged by the success of EWD607, we now embark upon the analysis of a more intricate elephant. We start with a cyclic arrangement of 3 + 3 mosquitoes. Three main mosquitoes, called R(ed), W(hite), and B(lue) respectively, and three buffer mosquitoes RW, WB, and BR, in between:
R → RW → W → WB → B → BR → R .
The buffer mosquitoes are quite simple, e.g.:
RW: begin channel W; | |||
begin channel R; buf: pebble; | |||
do R?(buf) → W!(buf) od | |||
end | |||
end |
When its (input)channel with R ceases to exist, R?(buf) will become false, and block exit will cause termination of the existence of the (output)channel with W. Each of the main mosquitoes has three “bags of pebble”, named “r(ed)”, “w(hite)”,and “b(lue)” . The R mosquito must collect in its bag called “r” all red pebbles in the system; its “foreign” pebbles it transmits, one at a time, via the buffer mosquito RW , first emptying its blue bag because its blue pebbles —that have to reach their destination via W — have to travel the longer distance. The arrangement is worth investigating because we expect problems with the proof of termination.
The solution that I am proposing has also a starting problem, but I am not going to divulge that now: I hope that that difficulty emerges “naturally” from a systematic analysis of our system.
mosquito R:
begin channel BR; | |||
x, y: pebble; r, w, b: bag 3: pebble; | |||
proc accept: if non BR?(y) → skip ▯ BR?(y) → place fi corp; | |||
proc place: if white(y) → w:= w ≁ y ▯ red(y) → r:= r ≁ y fi corp; | |||
r, w, := “initial values” {R3}; | |||
begin channel RW; | |||
do card(b) > 0 → x:= any(b);’b:= b ≃ x; | |||
RW!(x); accept | |||
od {R2}: | |||
do card(w) > 0 → x:= any(w); w:= w ≃ x; | |||
RW!(x); accept | |||
od | |||
end {R1}; Note: “card” -short for “cardina1ity”— | |||
do BR?(y) → place od {R0} denotes “number of elements in”. | |||
end (End of note.) |
We assume that —by some magic, not to be discussed here— BR (the text of which starts with “begin channel R”) and R (the text of which starts with “begin channel BR”) perform the entry to their outer blocks simultaneously, thereby establishing the channel between them (which will be used only as an input channel to R ). when the three input channels to the main mosquitoes have been established, the six inner blocks will be entered —pairwise simultaneously, but now R paired with RW — and the output channels for the main mosquitoes have been established. (This is very informal and intuitive, but OK for the moment: if coded wrongly, such paired block entries can, of course, create a glorious deadlock.)
Let us now study mosquito R backwards. My final goal is to establish proper termination with
R0: | card(b) = card(w) = 0 and y-tai1(R0) is empty, |
The first step is to investigate the transition from R1 to R0 . Termination of the repetitive construct in between guarantees non BR?(y) , i.e. guarantees that y-tail(R0) is empty; infinite repetition is excluded by y-tail(R1) is finite .
Because card(b) = card(w) = 0 does not follow from “non BB” it had better hold at R1 and be kept invariant by “place”. Keeping card(w) = 0 invariant by “place” implies the absence of white pebbles in the tail, avoiding abortion implies the absence of blue ones, and we find for R1
R1: | card(b) = card(w) = 0 and y-tail(R1) is finite and red only |
The next step is to investigate the transition from R2 to R1 . Because card(b) = 0 does not follow from “non BB” , we require it at R2 ; exclusion of abortion taken into account:
card(b) = 0 and y-tail(R2) contains no blue pebbles |
card(w) = 0 and y-tail(R1) is finite and red only . |
y-tail (R2) is finite |
Let us define for a finite tail without blue pebbles
if tail contains no white pebbles: | slack = - 1 |
if tail contains white pebbles 2 slack : | the total number of red pebbles preceding the last white one |
1) card(w) = 0 implies that the finite tail is all red
2) card(w) > slack is an invariant for the repeatable statement from R2 to R1 ; because card(w) ≥ 0 by definition, this is obvious if the resulting tail has no white pebbles, otherwise
2a) y has been white, in which case both’ card(w) and slack remained unchanged | |
2b) y has been red, in which case both card(w) and slack have been decreased by 1 . |
R2: | card(b) = 0 and y-tail(R2) is finite, without blue pebbles and card(w) >-slack(R2) . |
card(b) + card(w) >-slack |
R3: | y-tail(R3) is finite, without blue pebbles and eard(b) + card(w) > slack(R3) . |
Taking the finiteness for a moment for granted, we see that
1) the absence of blue pebbles in the y-tail is guaranteed (because R does
not transmit red pebbles, and cyclicly)
2) slack(R3) ≥ 0 (because R does transmit blue pebbles, if any, before
white ones, if any, and cyclicly.)
Hence, a safe starting state is: each mosquito with at least one foreign pebble! The complication at the start has, indeed, shown up nicely.
Termination was more easily demonstrated than originally feared.
1) Mosquito R will generate in its x-sequence an a priori bounded number of
blue pebbles.
2) In the same way, mosquito B will only generate in its x-sequence an
a priori bounded number of white pebbles.
3) Equating the x-output of B with the y-input of R , we conclude that
mosquito R will only receive a bounded number of white pebbles.
Combining 1) and 3) we conclude that mosquito R will only generate a finite
x-sequence.
The proof of total conservation of pebbles is left to the reader.
Plataanstraat 5 | prof.dr.Edsger W.Dijkstra |
NL-4565 NUENEN | Burroughs Research Fellow |
The Netherlands |
Transcribed by Martin P.M. van der Burgt
Last revision