Typos found in the first printing (August 2003)

Statistics: The list above contains roughly 128 reported typos and goofs in the first printing of the book. There are approximately 340K words in the book, giving 1 reported defect per 2,650 words written. At and average of 10 words per sentence, this is about 4 reported defects per 1,000 sentences in the book, which is roughly on par with a reasonably good software development process of 1-10 residual defects (after testing) per 1,000 lines of non-comment source code written. As in software, the number of reported defects depends both on the number of latent defects and on the number of users/readers (i.e., unread books will have no reported typos...).
Note (*) on the example used on p. 20, provided by Heikki Tauriainen.
Date: Wed, 01 Feb 2006 21:10:54 +0200 (EET) 
From: heikki.tauriainen [atsign] tkk [dot] fi 
Subject: Spin book: Doran & Thomas's mutual exclusion algorithm 

Dear Dr. Holzmann,

Keijo Heljanko and I are giving at Helsinki University of Technology
a basic course on parallel and distributed systems, using Spin for
examples on model checking.  To demonstrate using the tool, we
considered Dekker's mutual exclusion algorithm found in your Spin
book (p. 20) and the variant of the algorithm by Doran and Thomas
mentioned on p. 22.

According to the Spin book, Doran and Thomas's algorithm can be
obtained from Dekker's algorithm by simply changing the outer do-loop
of the algorithm into an if-selection, and this change is claimed to
preserve the correctness of the algorithm.  This doesn't, however,
seem to be the case, as the verification results using the Promela
models distributed in the package
somewhat unexpected (unless, of course, the models in the package are
deliberately faulty).  I'm referring to the file CH2/mutex.pml in the

The Promela model uses a preprocessor directive (DORAN) to choose
between the algorithm with the do-loop and the algorithm with the
if-selection. Verifying the model with the do-loop indeed gives the
expected result (no assertion violations).  Firstly, however, Spin
doesn't directly accept the model of the variant of the algorithm:

$ spin -DDORAN -a mutex.pml
spin: line  30 "mutex.pml", Error: misplaced break statement    saw '-2'' near 'break'

After the obvious change of making the 'break' keyword at line 30
apply only to the variant with the do-loop, that is, changing lines
29--35 to read

        :: else ->
#ifdef DORAN

and then verifying the mutual exclusion algorithm gives, however,
the following (unexpected) result:

$ spin -DDORAN -a mutex.pml
$ gcc -o -DBFS -o pan pan.c
$ ./pan
pan: assertion violated (cnt==1) (at depth 9)
pan: wrote mutex.pml.trail
(Spin Version 4.2.6 -- 27 October 2005)
Warning: Search not completed
        + Using Breadth-First Search
        + Partial Order Reduction

Full statespace search for:
        never claim             - (none specified)
        assertion violations    +
        cycle checks            - (disabled by -DSAFETY)
        invalid end states      +

State-vector 20 byte, depth reached 9, errors: 1
      56 states, stored
              56 nominal states (stored-atomic)
      32 states, matched
      88 transitions (= stored+matched)
       0 atomic steps
hash conflicts: 0 (resolved)

2.302   memory usage (Mbyte)

$ spin -DDORAN -p -t mutex.pml
Starting mutex with pid 0
Starting mutex with pid 1
  1:    proc  1 (mutex) line  11 "mutex.pml" (state 1)  [i = _pid]
  1:    proc  1 (mutex) line  12 "mutex.pml" (state 2)  [j = (1-_pid)]
  2:    proc  0 (mutex) line  11 "mutex.pml" (state 1)  [i = _pid]
  2:    proc  0 (mutex) line  12 "mutex.pml" (state 2)  [j = (1-_pid)]
  3:    proc  1 (mutex) line  14 "mutex.pml" (state 3)  [flag[i] = 1]
  4:    proc  1 (mutex) line  29 "mutex.pml" (state 12) [else]
  5:    proc  1 (mutex) line  37 "mutex.pml" (state 15) [cnt = (cnt+1)]
  6:    proc  0 (mutex) line  14 "mutex.pml" (state 3)  [flag[i] = 1]
  7:    proc  0 (mutex) line  21 "mutex.pml" (state 4)  [(flag[j])]
  8:    proc  0 (mutex) line  27 "mutex.pml" (state 9)  [else]
  9:    proc  0 (mutex) line  37 "mutex.pml" (state 15) [cnt = (cnt+1)]
spin: trail ends after 9 steps
#processes: 2
                turn = 0
                flag[0] = 1
                flag[1] = 1
                cnt = 2
  9:    proc  1 (mutex) line  38 "mutex.pml" (state 16)
  9:    proc  0 (mutex) line  38 "mutex.pml" (state 16)
2 processes created

Trying to find a reason for this unexpected result, I compared the
model with the algorithm in Doran and Thomas's original article [1].
It appears that the model in fact differs from that algorithm
(repeated below from [1], Fig. 1)

Process A                           Process B
  1. A_needs := true;                    B_needs :=  true;
  2. if B_needs then begin               if A_needs then begin
  3.   if turn = 'B' then begin            if turn = 'A' then begin
  4.     A_needs := false;                   B_needs := false;
  5.     wait until turn = 'A';              wait until turn = 'B';
  6.     A_needs := true;                    B_needs := true;
  7.     end;                                end;
  8.   wait until !B_needs;                wait until !A_needs;
  9.   end;                                end;
 11. turn := 'B';                        turn := 'A';
 12. A_needs := false;                   B_needs := false;

In particular, the Promela model has no corresponding construct for
line 8 of this algorithm, which appears to be critical to its
correctness: changing the outer if-selection to read

        :: flag[j] ->
                :: turn == j ->
                        flag[i] = false;
                        !(turn == j);
                        flag[i] = true
                :: else
                (!flag[j]);    /* needed for correctness */
        :: else ->

fixes the error.  However, it is not sufficient to simply
replace the do-loop with an if-selection, although the wording
on page 22 of the Spin book can be interpreteted to suggest
otherwise (at least both I and Keijo were surprised, that's why
we decided to write this report).

(The example file suggests that the model is taken from the book
[2] instead of directly from Doran and Thomas's original article [1].
As a matter of fact, this book---at least its English translation---contains the same error.  This is probably also the
reason why the model is faulty.)

Best regards,
Heikki Tauriainen


[1] R. W. Doran and L. K. Thomas.  Variants of the software solution to
    mutual exclusion.  Information Processing Letters 10(4--5):206--208,

[2] M. Raynal.  Algorithms for mutual exclusion.  North Oxford Academic
    Publishers Ltd., 1986.

book home page
Spin home page
Last updated: 1 January 2007