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: 2006年2月01日 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
 were
somewhat unexpected (unless, of course, the models in the package are
deliberately faulty). I'm referring to the file CH2/mutex.pml in the
package.
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
 fi;
#else
 break
 od;
#endif
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;
 10. CRITICAL SECTION CRITICAL SECTION
 11. turn := 'B'; turn := 'A';
 12. A_needs := false; B_needs := false;
 13. NON-CRITICAL SECTION NON-CRITICAL SECTION
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
 if
 :: flag[j] ->
 if
 :: turn == j ->
 flag[i] = false;
 !(turn == j);
 flag[i] = true
 :: else
 fi;
 (!flag[j]); /* needed for correctness */
 :: else ->
 fi;
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
References:
[1] R. W. Doran and L. K. Thomas. Variants of the software solution to
 mutual exclusion. Information Processing Letters 10(4--5):206--208,
 1980.
[2] M. Raynal. Algorithms for mutual exclusion. North Oxford Academic
 Publishers Ltd., 1986.
book home page
Spin home page
Last updated: 1 January 2007

AltStyle によって変換されたページ (->オリジナル) /