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 textreading software. It will be replaced by a fully markedup version when time permits. —HR
A tutorial on the split binary semaphore.
The purpose of this note is threefold. It has been written to
introduce the student to
1) the technique of the socalled “split binary semaphore” —originally
discovered, but at the same time not recommended, by C.A.R.Hoare—
2) the use of formal techniques in the development of multiprograms
3) the now canonical example of “The readers and the writers”, which the
student must know anyhow; it will be used as a carrier for the other two
purposes. The problem of the readers and the writers was designed by D.L.
Parnas.
We consider two classes of cyclic processes, called “readers” and
“writers” respectively. with “ncs” standing for “noncritical section”,
they can be described by the programs
reader: 
do true → ncs; READ od  (1)

writer: 
do true → ncs; WRITE od 

respectively. Here “READ” and “WRITE” denote their respective critical
sections, critical in the sense that when a writer is engaged in its critical
section, it must be
the only process engaged in its critical section. This
problem can be solved in many different ways —the problem is canonical in
the sense that everybody proposing new synchronization primitives has solved
it in his way— , we shall now solve it using a split binary semaphore.
Our first step is the introduction of variables, in terms of which we
express our synchronization requirement formally; we call them “ar” and
“aw” —short for “number of active readers” and “number of active writers”
respectively— and consider the following multiprogram:

ar = 0, aw = 0, mutex = 1 
reader: do true → ncs; 
 
P(mutex); ar: ar + 1; V(mutex); 
 
READ; 
 
P(mutex); ar: ar  1; V(mutex) 

od 
writer: do true → ncs; 
 
P(mutex); aw:= aw + 1; V(mutex); 
 
WRITE; 
 
P(mutex); aw:= aw  1; V(mutex) 

od 
For multiprogram (2) the invariance of
follows immediately in the usual way “from the topology of the program”.
(Associate with reader
_{i} an additional variable c
_{i} , initially : 0, and
satisfying 0 ≤ c
_{i} ≤ 1 ; replace ar:= ar + 1 by c
_{i}, ar := 1, ar + 1 and
ar:= ar  1 by c
_{i}, ar := 0, ar  1 and observe the invariance of ar =
Σci , etc.)
Note. Looking at program (2) and interpreting it operationally, one might be
tempted to say: clearly ar ≥ the number of readers engaged in READ , and
as ”a number of readers“ is never negative, ar ≥ 0 follows immediately, and
similarly for aw ≥ 0 . I prefer not to do so, to prove the invariance of
P0 from the uninterpreted text (2), and to conclude from P0 that it does
not prohibit the interpretation of ar and aw as natural numbers. (End of
Note.)
In terms of ar and aw I propose the required invariance of
P1: aw = 0 or (aw = 1 and ar = 0)
as a suitable formal expression of our operational requirement ”when a writer
is engaged in its critical section, it must be the only process engaged in
its critical section“. The term aw = 0 is intended to cover the situation
when no writer is engaged in its critical section, the term aw = 1 and ar = 0
should cover the case when a writer is engaged in its critical section.
Note. The attentive reader will already have decided that he should not
expect more eloquence from me on the “suitability” of the proposal captured by
P1 . (End of Note.)
In order to prevent ar:= ar + 1 from violating P1 we can make
it into a guarded command of the form
 wp(“ar:= ar + 1”, P1) → ar:= ar + 1 .

The axiom of assignment gives for this guard
 aw = 0 or (aw = 1 and ar + 1 = 0)

but on account of P0 the second term is false, and we simplify
In order to prevent aw:= aw + 1 from violating P1 we consider
 wp(“aw:= aw + 1”, P1) → aw:: aw + 1 .

The axiom of assignment gives for this guard
 aw + 1 = 0 or (aw + 1 = 1 and ar = 0)

but, again, P0 admits simplification of this guard —its first term is false—
and we find
 aw = 0 and ar = 0 → aw:= aw + 1 .

The decrease ar:= ar  1 is similarly guarded
 wp(“ar:= ar  1”, P1) → ar:= ar  1 ,

and we get for the guard with the axiom of assignment
 aw = 0 or (aw = 1 and ar  1 = 0) ,

which, thanks to P1 can be simplified as
The known invariance of P0 tells us that the precondition of ar:= ar  1
implies wp(“ar:= ar  1”, P0) , i.e. implies ar  1 ≥ 0 ; on account of
P1 this implies aw = 0 , and, therefore, we can simplify to
i.e. the decrease ar:= ar  1 need not be guarded at all.
The verification that also aw:= aw  1 need not be guarded is left
to the reader.
Inserting the guards as derived we get
initial state: 
ar = 0, aw = 0, mutex = 1  (3)

reader: do true → ncs; 
§  
P(mutex); if aw = 0 → ar:= ar + 1 fi; V(mutex); 
 
READ; 
 
P(mutex); ar:= ar  1; V(mutex) 

od 
writer: do true → ncs; 
§§  
P(mutex); if aw = 0 and ar = 0 → aw:= aw + 1 fi; V(mutex); 
 
WRITE; 
 
P(mutex); aw:= aw  1; V(mutex) 

od 
Multiprogram (3) has been designed so as to leave P0
and P1
invariant, and that is fine. It has, however, a major drawback: both alternative
constructs, in the lines marked § and §§ respectively, may lead to
abortion! The socalled split binary semaphore provides us with a technique for
preventing the selection of the critical sections marked § and §§
respectively under those circumstances in which they would lead to abortion.
We replace the single binary semaphore mutex by three, also binary,
semaphores — m , r , and w say— , related to the original mutex by
mutex = m + r + w ,
and replace in multiprogram (3) each P(mutex) by P(m), P(r), or P(w)
—the three ways of decreasing mutex by 1— and each V(mutex) by V(m),
V(r), or V(w) —the three ways of increasing mutex by 1— . (Because
m, r, and w are semaphores, we thus guarantee 0 ≤ mutex ≤ 1 .) More
precisely: we replace the P(mutex) marked by § by P(r) , replace the
P(mutex) marked by §§ by P(w) , and the P(mutex) that opens a critical
section that cannot lead to abortion by P(m) .
We can now avoid selection of an aborting critical section by guarding
V(r) by aw = 0 and by guarding V(w) by aw = 0 and ar = 0 , because
the precondition of a Voperation on a component of a split binary semaphore
can be taken as the postcondition of the corresponding Poperation. Our
analysis so far would suggest that it suffices to replace V(mutex) everytime
by
Q: 
if true → V(m) ▯ aw = 0 → V(r) ▯ aw = 0 and ar = 0 → V(w) fi  (4)

This, however, is too naive. To start with: how do we translate the
initialization mutex = 1 ? The initialization m = 0, r = 1, w = 0 is too
restrictive: if all readers remain in their ncs , no writer could perform
WRITE. The initialization m = 0 , r = 0, w = 1 has to be rejected on
similar grounds. In order to make the only remaining possible initialization
m = 1, r = 0, w = 0 acceptable, readers and writers should encounter as
first Poperation one that cannot lead to abortion. We can satisfy this
requirement by inserting in both readers and writers of (3) after ncs
before performing the substitution described above. This would lead to the
following multiprogram
initial state: 
ar = 0, aw = 0, m = 1, r = 0, w = 0  (5)

reader: do true → ncs; P(m); Q; 
 
P(r) {aw = 0}; ar:= ar + 1; Q; 
 
READ; 
 
P(m); ar:= ar  1; Q 

od 
writer: do true → ncs; P(m); Q; 
 
P(w) {aw = 0 an 
 
ar = 0}; aw:= aw + 1; Q; 
 
WRITE; 
 
P(m); aw:= aw  1; Q 

od 
Multiprogram (5) is, however, still too naive: the nondeterminacy, that has
been introduced by Q as given in (4), has lead to a system with the danger
of deadlock. The recipe for its prevention is, however, universal.
1) At initialization and at each Voperation, the “type of the next
operation” —i.e. the component of the split binary semaphore on which this
program will perform its next Poperation— must be uniquely defined.
Our program (5) satisfies this condition, as do all programs without initial
nondeterminacy nor nondeterminacy between a Voperation and the dynamically
next Poperation. If a program does not satisfy this condition we can always
make it satisfying it by introducing one or more extra components of the split
binary semaphore, and by replacing essentially

if true → P(component 1);... 
 
▯ true → P(component 2);... 

fi 
by

if true → P(extra component); Q; P(component 1);... 
 
▯ true → P(extra component); Q; P(cpmponent 2);... 

fi 
Task. Prove that for this substitution process only a finite number of
different extra components is needed. (End of Task.)
2) with each component of the binary semaphore we associate a counter,
initialized to the number of processes for which the first Poperation is of
the corresponding type.
3) After each Poperation we insert a decrease by 1 of the counter
associated with its type.
4) Before each Q we insert an increase by 1 of the counter associated
with the type of the dynamically next Poperation. (Thanks to step 1
this is a we11defined counter.)
Note. For the operationally minded each counter can be interpreted as the
number of processes “ready” or “headed” for a Poperation on the
corresponding component. (End of Note.)
5) Strengthen in Q the guarding of each V(component) by the requirement
that the corresponding counter is positive.
Associating with the semaphore components m , r , and w the counters
bm , br , and bw respectively, carrying out the above transformations on
program (5) leads to
initial state: 
ar = 0, aw = 0, bm = number of processes, hr = 0, bw = 0
m = 1, r = 0, w = 0
 (6)

reader: do true → ncs; 
 
P(m); bm:= bm  1; br:= br + 1; Q; 
 
P(r); br:= hr  1; ar:= ar + 1; bm:= bm + 1; Q; 
 
READ; 
 
P(m); bm:= bm  1; ar:= ar  1; bm:= hm + 1; Q 

od 
writer: do true → ncs; 
 
P(m); bm:= bm  1; bw:= bw + 1; Q; 
 
P(w); bw:= bw  1; aw:= aw + 1; bm:= bm + 1; Q; 
 
WRITE; 
 
P(m); bm:= bm  1 aw:= aw  1; bm:= bm + 1; Q 

od 
with Q short for
 
▯ aw = 0 and br > 0 i V(:) 
 
▯ aw = 0 and ar = 0 and bw > 0 → V(w) 

fi 
Note. The transformation of the introduction of the counters and of the
strengthening of the guards in Q by the requirement that the corresponding
counters be positive, excludes the danger of deadlock. If the original
requirement —in our case: the invariance of P1— entailed intrinsically the
danger of deadlock, this danger is now made manifest by the danger of abortion
in Q . The systematic procedure for dealing with that situation falls
outside the scope of this tutorial. (End of Note.)
Our original system was free from deadlock, hence we must —see above
note— be able to prove the absence of the danger of abortion in Q . The
precondition of Q implies everywhere in (6)

bm + br + bw = number of readers + number of writers 

ar + br ≤ number of readers 

aw + bw ≤ number of writers 
Task. Verify the above three assertions. (End of Task.)
From the above we conclude

ar + aw ≤ bm , and hence 

bm > 0 or (ar = 0 and aw = 0) . 
Assuming the number of processes to be larger than zero —otherwise the danger
of abortion is absent anyhow!;— , we also have
 bm > 0 or br > 0 or bw > 0

and from the last two relations it follows that at least one of the guards of
Q as given in (6’) is true.
The above form of Q as given in (6’) is still very nondeterministic:
we have the strategic freedom of strengthening the guards as long as we avoid
the danger of abortion. As it stands, our solution does not exclude that
readers or a writer are denied access to their critical section READ or
WRITE without reason. Within Q we can give “priority” to V(r) or V(w)
by strengthening the guard of V(m) to the conjunction of the complements of
the other two guards:
Am:  (aw > 0 or br = 0) and (aw > 0 or ar > 0 or bw = 0)

Denoting by Ar and Aw respectively:
Ar:  aw = 0 and br > 0

Aw:  aw = 0 and ar = 0 and bw > 0

we can new substitute for Q in (6)
Q: 
if Am → V(m) ▯ Ar → V(r) ▯ Aw → V(w) fi .  (7')

All (new superfluous) operations on bm can be omitted; using the
postconditions of the Poperations, the substitution instances of Q as given
by (7’) can be simplified. Thus we derive from (6) the multiprogram
initial state: 
ar = 0, aw = 0, br = 0, bw = 0, m = 1, r = 0, w = 0  (7)

reader: 
do true → ncs; 

P(m); br:= br + l; if aw > 0 → V(m) ▯ aw = 0 → V(r) fi; 

P(r); br, ar := br  l, ar + l; if br = 0 → V(m) ▯ br > 0 → V(r) fi; 

READ; 

P(m); ar:= ar  1; if ar > 0 or bw = 0 → V(m) 
   
▯ ar = 0 and bw > 0 → V(w) 
 
fi 
od 
writer: 
do true → ncs; 

P(m); bw:= bw + l; if aw > 0 or ar > 0 → V(m) 
  
▯ aw = 0 and ar = 0 → V(w) 
 
fi 

P(w); bw, aw := bw  l, aw + 1; V(m); 

WRITE; 

P(m) ; aw:= aw  l ; if br = 0 and bw = 0 → V(m) 
     
▯ br > 0 → V(r) 
     
▯ bw > 0 → V(w) 
    
fi 
od 
Remark. An inspection of the alternative constructs in (7) shows that only
the very last one is nondeterministic: here we have, therefore, still a
strategic freedom. Investigate the consequences of replacing the last
guarded command bw > 0 → V(w) by bw > 0
and br = 0 → V(w) . (End of
Remark.)
* *
*
In the above we have derived our final program as the end of a sequence
of successive versions. We have done so for educational reasons, with the
intent of introducing the different aspects of programs synchronized with
a split binary semaphore one after the other. This is not meant as a
suggestion that in the case of actual program design one should write down all those
successive versions! The experienced programmer knows that “outside the
critical sections” as delineated by the P  V pairs, we have an invariant of
the form
 (m = 0 or Am) and (r = 0 or Ar) and (w = 0 or Aw)

and focusses his attention on the A’s; having chosen them he derives the final
code. I make this remark because socalled “program transformations” are
sometimes suggested as a practical way of program derivation —not by me,
for as a rule it leads to an undue amount of writing— .
5th March 1979 

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
20150209
.