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
A correction on EWD651.
The day after I had mailed the copies of EWD651 to its various recipients I discovered that it was miserably wrong: the transfer from the L-group to the R-group did not work properly. In the new version the boolean L is replaced by the four-valued integer k . ’
A notational difference is the introduction of the integers pL and pH , counting the numbers of blocked processes in the L-group and in the R-group respectively. The former variables wL and wR have disappeared, their values being pL - nL and pR - nR respectively.
The integer k controls whether a process with a false guard will arrive in the L-group or in the R-group. In contrast to EWD651, in which the value of L was left undefined when both groups were empty, we have now decided that the first process to be blocked will come in the R-group, thus being faithful to the intention of maintaining m = 0 or pL = 0 or pR > 0 . Initially we have k = 1 . We shall now describe the meaning of the variable k.
k = 0 .
The process finding its guard false either just entered the critical activity via P(m) or is retesting its guard; in the latter case it came from the L-group. In either case it is directed towards the L-group. During the test of a guard with k = 0, we have pR = nR > 0 , and all the processes in the R-group have a false guard.
k = 1 .
If the process finding its guard false just entered the critical activity via P(m), we had pL = pR = 0 , and the process is entered into the R-group. If the process finding its guard false is retesting its guard, it came from the R-group and returns to it, and the values of the guards of the processes in the L-group —if any— are unknown.
k = 2 .
This state, which is one of the transfer states, cannot occur with m = 1, hence a process finding its guard false has not just entered the critical activity. The process that is retesting its guard came from the L-group and will be directed into the R-group. The state k ≥ 2 remains until the L-group is empty, so as to ensure that all L-processes escape or become an R-process before a new process is admitted via P(m) . This is done in order to exclude infinite overtaking of a process in the L-group. During k = 2 we have pR = nR , and all processes in the R-group —if any— have a false guard.
k = 3 .
This second transfer state can also not occur with m = 1 . It is only entered when in the “middle” of the transfer of processes from the L-group to the R-group —i.e. when k = 2 — one of the processes escapes via S . As soon as that has happened, we are no longer sure that all processes in the R-group have a false guard. Therefore all the processes in the R-group have to retest their guard before the transfer from the L-group to the R-group can be resumed. When with k = 3 a process finds its guard false, it came from the R-group and will be returned to the R-group, just as in state k = 1 The values of the guards of the processes in the L-group —if any— are unknown, when it has been established that the R-group only contains processes with a false guard and the L-group is not empty, the transfer will be resumed with k = 2.
When, with pR > 0 , it has been established that all processes in the R-group have a false guard — pR = nR — the primary case distinction is whether the L-group is empty or not. In the first case, the critical activity is terminated via V(m) with k = 0 , because a new process that blocks itself, should do so in the L-group. In the second case —because when processes from the R-group are tested, the guards of those in the L-group are never known— those in the L-group have to retest their guard. The last process (re)entering the R-group did so with k: 1, 2, or 3 ; the L-testing has to be resumed with k = 0, 2, 2 respectively, hence the
| do odd(k) → k:=k-1 od. |
Upon completion of an S , when there are no blocked processes, the critical activity is terminated via V(m) with k = 1 , because the first new
| P(m); | ||||||||||
| do non Bi → | ||||||||||
| if k = 0 → | ||||||||||
| pL, nL := pL + l, nL + 1; | ||||||||||
| if pL > nL → V(tL) ▯ pL = nL → V(m) fi; | ||||||||||
| P(sL); nL:= nL - 1; | ||||||||||
| if nL > 0 → V(sL) ▯ nL = 0 - V(tL) fi; | ||||||||||
| P(tL); pL:= pL - l | ||||||||||
| ▯ k > 0 → | ||||||||||
| pR, nR := pR + 1, nR + 1; | ||||||||||
| if pR > nR → V(tR) | ||||||||||
| ▯ pR = nR → | ||||||||||
| if pL = 0 → k:= 0; V(m) | ||||||||||
| ▯ pL > 0 → do odd(k) → k:= k - 1 od | ||||||||||
| if nL > 0 → V(sL) ▯ nL = 0 → V(tL) fi; | ||||||||||
| fi | ||||||||||
| fi; . | ||||||||||
| P(sR); nR:= nR - 1; | ||||||||||
| if nR > 0 → V(sR) ▯ nR = 0 → V(tR) fi; | ||||||||||
| P(tR); pR:= pR - l | ||||||||||
| fi | ||||||||||
| od ; | ||||||||||
| Si; | ||||||||||
| if pR = 0 → | ||||||||||
| if pL = 0 → k:= l; V(m) | ||||||||||
| ▯ pL > 0 → k:= 2; if nL > 0 → V(sL) ▯ nL = 0 → V(tL) fi; | ||||||||||
| fi | ||||||||||
| ▯ pR > 0 → | ||||||||||
| do even(k) → k:= k + 1 od; if nR > 0 → V(sR) ▯ nR = 0 → V(tR) fi | ||||||||||
| fi | ||||||||||
| do even(k) → k:= k + 1 od |
Note. The integer k was introduced when I had discovered the need for the state k = 2 , but not yet the need for the state k = 3 . Had I foreseen that fourth state, I would have used a second boolean , tf say (“transfer”), and would have coded
| k = 0 | as L and non tf |
| k = 1 | as non L and non tf |
| k = 2 | as L and tf |
| k = 3 | as non L and tf , |
| and the statements: | do odd(k) → k:= k - 1 od | and | do even(k) → k:= k +1 od |
| simply as: | L:= true | and | L:= false |
I can only describe the blunder of EWD651 as “most instructive”, because I know exactly how it occurred: we did not stick to our own rules, fell back into our old bad habits and rushed into coding! Besides that the whole experience provides a (totally unintended but welcome) confirmation of my often stated conjecture that pictures give a false sense of security. Although somewhat humiliated I am actually glad that I blundered so clearly!
I wish everybody a happy 1978!
| Plataanstraat 5 | prof.dr.Edsger W.Dijkstra |
| 5671 AL Nuenen | Burroughs Research Fellow |
| The Netherlands |
Transcribed by Martin P.M. van der Burgt
Last revision 2015-01-26
.