verif/Spin/Doc/Book2003Errata.html

   1 <html>
   2 <head>
   3 <title>Book Errata - The Spin Model Checker</title>
   4 </head>
   5 <h3>Typos found in the first printing (August 2003)</h3>
   6 <font face=helvetica,arial>
   7 <ul>
   8 <li>p. vi       chapter 8 topic listings, Breath-First -> Breadth-First</li>
   9 <li>p.  2       line 16 "always explicitly" -> "usually"</li>
  10 <li>p.  3       figure 1.1 is mirror reversed</li>
  11 <li>p.  4       the website crashdatabas.com no longer seems to exist</li>
  12 <li>p. 20       See note (*) below, provided by Heikki Tauriainen (Feb 1, 2006).
  13 <li>p. 22       6th line from the bottom: "if" -> "of"</li>
  14 <li>p. 25       4th line from the bottom: "variable in" -> "variable cnt"</li>
  15 <li>p. 26       10th line from bottom: "set to false" -> "set to true"</li>
  16 <li>p. 27       an error slipped into Figure 2.6. The fragment
  17 <pre>
  18         M?data ->       /* receive data */
  19         do
  20         :: W!data       /* send data */
  21         :: W!shutup;    /* or shutdown */
  22                 break
  23         od
  24 </pre>
  25 is an unfortunate last-minute rewrite of the originally intended version:
  26 <pre>
  27         do
  28         :: M?data -> W!data
  29         :: M?data -> W!shutup;
  30                 break
  31         od
  32 </pre>
  33 The behavior is of course not equivalent.
  34 In particular, the version in the book cannot create the error scenario
  35 given on page 29, but the intended version can.</li>
  36 <li>p. 33       8th line from bottom: "the specification" -> "the specification of"</li>
  37 <li>p. 33       3rd line from bottom: "functions pointers" -> "function pointers</li>
  38 <li>p. 41       "1 <= n <= 32" -> "1 <= n < 32".</li>
  39 <li>p. 43       appel -> apple</li>
  40 <li>p. 52       11th line from the top: "p. 39." -> "p. 38."</li>
  41 <li>p. 69       bottom line: "exclusive read and exclusive write" -> "exclusive receive and exclusive send"</li>
  42 <li>p. 75 and 548       Goldstein -> Goldstine</li>
  43 <li>p. 81 and 271       pan.trail -> fair.pml.trail</li>
  44 <li>p. 81       3rd line from the bottom: "trace fpr" -> "trace for"</li>
  45 <li>p. 82       18th line from the bottom: "process than" -> "process that"</li>
  46 <li>p. 92       4th line from bottom: "Even traces" -> "Event traces"</li>
  47 <li>p. 96       middle of page identify -> identity</li>
  48 <li>p. 96       l. -6, for -> by</li>
  49 <li>p. 111      below figure 5.4: "f==free" -> "f=free"</li>
  50 <li>p. 119      12th line from the bottom; "xDm" -> "Dm"</li>
  51 <li>p. 121      figure 5.8, in captions on bottom two figures: "p" -> "q"</li>
  52 <li>p. 137      14th line from bottom (first rule in list): first 3 chars in wrong font</li>
  53 <li>p. 139      last line; italic P -> roman P</li>
  54 <li>p. 142      3rd line from bottom: "reach" -> "reached"</li>
  55 <li>p. 142      5th line from bottom: omit comma</li>
  56 <li>p. 148      middle of the page: "can be express" -> "can be expressed"</li>
  57 <li>p. 149      5th line from bottom: "eventually always" -> "always eventually"</li>
  58 <li>p. 150      replace "it is impossible for p to hold only in even steps in a run, but never at odd steps"
  59 with "it is possible for p to hold in even steps in a run, but it is not possible for p to hold in odd steps"</li>
  60 <li>p. 150      Omega-Regular Properties, line 1: "that" -> "than"</li>
  61 <li>p. 158      middle of page: redundant space after "("</li>
  62 <li>p. 168      the list of properties given for < and > is not exhaustive</li>
  63 <li>p. 174      11th line from bottom: "but" -> "by"</li>
  64 <li>p. 177      Procedure Search() in Figure 8.6 is incorrect. A corrected version is:
  65 <pre>
  66 Search()
  67 {
  68         while (Empty_Queue(D) == false)
  69         {       s = Del_Queue(D)
  70                 for each (s,1,s') member A.T
  71                 if In_Statespace(V, s') == false
  72                 {       Add_Statespace(V, s')
  73                         Add_Queue(D, s')
  74                 }
  75         }
  76 }
  77 </pre>
  78 </li>
  79 <li>p. 178      2nd line from top: "at state" -> "at each state", "of each state" -> "of that state"</li>
  80 <li>p. 179      lead -> led</li>
  81 <li>p. 180      before first 'if' stmnt inside for loop add: if (toggle == true)</li>
  82 <li>p. 185      Fig. 8.10, circle at s^{1}_{2} should be dotted</li>
  83 <li>p. 187      line -11: "interative" -> "iterative"</li>
  84 <li>p. 188      replace "(RxB)+(k+2)" with "Rx(B+k+2)"</li>
  85 <li>p. 193      Fig. 9.2, the two circles labeled 0,1,0 should be dashed</li>
  86 <li>p. 193      7th line from bottom: "g=g*2," -> "g=g*2."</li>
  87 <li>p. 196      line -9: "control control" -> "control"</li>
  88 <li>p. 204      last line, "to 133 seconds" -> "to 53 seconds"</li>
  89 <li>p. 208      a goof: m changes from bits to bytes between 2nd and 3rd paragraph</li>
  90 <li>p. 209      in first two formulas: (1-1/m) sup {kr}.</li>
  91 <li>p. 211      3rd line from below: probabilitie -> probabilities</li>
  92 <li>p. 212      line -2: "ration" -> "ratio"</li>
  93 <li>p. 214      A formal -> Formal</li>
  94 <li>p. 216      1st-2nd line: 'collissions' -> 'collisions'</li>
  95 <li>p. 219      last paragraph: missing right parenthesis</li>
  96 <li>p. 228      Celcius -> Celsius</li>
  97 <li>p. 228      in the list at the bottom: there are just 6 entries with 'keep' as a target</li>
  98 <li>p. 237      12th line from below: "postive" -> "zero".</li>
  99 <li>p. 237      4th line from below: "unsound" -> "incomplete".</li>
 100 <li>p. 238      knifes -> knives</li>
 101 <li>p. 241      7th line from bottom: "world0" -> "world\n"</li>
 102 <li>p. 243      Pressburger -> Presburger</li>
 103 <li>p. 251      Selet -> Select</li>
 104 <li>p. 262      10th line from bottom: "do to" -> "due to"</li>
 105 <li>p. 272      an basic -> a basic</li>
 106 <li>p. 272      "As a special feature [...], if the statement" omit "if"</li>
 107 <li>p. 279      "#define q" -> "#define r"
 108 <!--
 109 <li>p. 280      (strong) -> (weak)</li>
 110 -->
 111 <li>p. 281      Automata View -> Automaton View</li>
 112 <li>p. 283      The correct wording of the quote from Willem L. van der Poel, as corrected by its author:
 113                 <pre>"There are no wrong programs, it simply is another program."</pre>
 114                 (email from the author, Feb 1, 2006).
 115 <li>p. 284      8th line from bottom: omit "blue"</li>
 116 <li>p. 287      6th line from top: omit "blue"</li>
 117 <li>p. 307      top of page: "ringtone" -> "ring tone" </li>
 118 <li>p. 307      top of page: "dialtone" -> "dial tone"</li>
 119 <li>p. 307      top of page: "notone" -> "no tone"</li>
 120 <!-- <li>p. 332 3rd line from bottom: UTS without a trademark (see also next page, 1x)</li> -->
 121 <li>p. 333      11th line from top: "and early version" -> "an early version"</li>
 122 <li>p. 338      the line numbered [19] is actually from the FIX</li>
 123 <li>p. 339      6th line from below: pid 1 -> pid 0</li>
 124 <li>p. 393      2nd line from top: "innermostn" -> "innermost"</li>
 125 <li>p. 341      10th line from top: "body ," -> "body,"</li>
 126 <li>p. 346      identificatio -> identification</li>
 127 <li>p. 346      middle of the page: "tranaction" -> "transaction"</li>
 128 <li>p. 349      55 is not the integer square root of either 1024 or 3601.</li>
 129 <li>p. 356      n=1<<30 does not fail on all systems</li>
 130 <li>p. 359      Fig. 15.8: what looks like commas are really single quotes</li>
 131 <li>p. 359      Fig. 15.8: the automaton fails to detect strings that start inside a comment;</li>
 132 unfortunate given the example that also appears on this page...</li>
 133 <li>p. 365      the grammar listing misses productions for inlines</li>
 134 <li>p. 365      [active] PROCTYPE -> [active ['[' const ']']] PROCTYPE</li>
 135 <li>p. 367      "PRINT" -> "PRINTF"</li>
 136 <li>p. 369      in PREDEFINED: "373last" -> "374"</li>
 137 <li>p. 369      in PREDEFINED: "373nr_pr" -> "376"</li>
 138 <li>p. 369      5th line from bottom: "special case" -> "special cases"</li>
 139 <li>p. 370      8th line from bottom: "p.272" -> "p. 272"</li>
 140 <li>p. 370      2nd line from bottom: "(434)" -> "(p. 434)"</li>
 141 <li>p. 370      2nd line from bottom: "(p, 483)" -> "(p. 483)"</li>
 142 <li>p. 371      2nd line from top: "Two" -> "Three"</li>
 143 <li>p. 371      9th line from top: "or both of the above two" -> "of the above" </li>
 144 <li>p. 374      11th line from bottom: "from into" -> "to"</li>
 145 <li>p. 376      5th line from bottom: "at 256" -> "at 255"</li>
 146 <li>p. 377      5th line in DESCRIPTION: "process" -> "processes"</li>
 147 <li>p. 381      4th line from bottom: "four process" -> "four processes"</li>
 148 <li>p. 381      3rd line from bottom: "to three" -> "to four"</li>
 149 <li>p. 390      9th line from bottom: "recepient" -> "recipient"</li>
 150 <li>p. 393      10th line from bottom: "label L1" -> "label L2"
 151 <li>p. 395      6th line from top: "multiple field" -> "multiple fields"</li>
 152 <li>p. 397      4th line from top: "the the" -> "the"</li>
 153 <li>p. 398      11th line from bottom: redundant space after "("</li>
 154 <li>p. 402      7th line from top, "accidentily" -> "accidentally"</li>
 155 <li>p. 404      mixed fonts in Table</li>
 156 <li>p. 404      5th line from bottom: "the fact the" -> "the fact that the"</li>
 157 <li>p. 407      in Notes, 2nd line: "tha" -> "that"</li>
 158 <li>p. 408      "(x < 0)" -> "(x <= 0)"</li>
 159 <li>p. 411      last line: "ltl len" -> "ltl, len"</li>
 160 <li>p. 425      11th line from top: "followin" -> "following"</li>
 161 <li>p. 440      11th line from top: "equivalents" -> "equivalent"</li>
 162 <li>p. 441      middle of page: "LTL formula" -> "LTL formulae"</li>
 163 <li>p. 446      10th line from top: "equivalents" -> "equivalent"</li>
 164 <li>p. 450      last example in notes should be: atomic { P && qname?[ack,var] -> qname?ack,var }</li>
 165 <li>p. 452      15th line from bottom: "will included" -> "will be included"</li>
 166 <li>p. 455      5th line from top: "restrction" -> "restriction"</li>
 167 <li>p. 456      middle of page: "type main" -> "type fact"</li>
 168 <li>p. 456      12th line from bottom: "2,147,483,648" ->"2,147,483,647"</li>
 169 <li>p. 456      10th line from bottom: 13! = 6,227,020,800  (and so even 13! > 2^31-1)</li>
 170 <li>p. 464      9th line from bottom: "just and safe" -> "justified and safe" (2x)</li>
 171 <li>p. 466      1st line in EFFECT: "to the" -> "of the" </li>
 172 <li>p. 476      in EXAMPLES (2x): "b = a" -> "b = tmp"</li>
 173 <li>p. 479      7th line from top: "can are" -> "are"</li>
 174 <li>p. 496      6th line: "in in" -> "in"</li>
 175 <li>p. 498      2nd line from bottom: "coord.trail" -> "example.trail"</li>
 176 <li>p. 509      13th line from bottom: "known the" -> "known. The"</li>
 177 <li>p. 512      middle of page: "an pointer" -> "a pointer"</li>
 178 <li>p. 518      l -8, most -> must</li>
 179 <li>p. 519      l -10, -rthis -> -r, this</li>
 180 <li>p. 521      5th line from bottom: "substitions" -> "substitutions"</li>
 181 <li>p. 528      under basic options -DBFS, "reducting" -> "reducing"</li>
 182 <li>p. 532      under -DSDUMP, replace "-DCHECK" with: "-DVERBOSE or -DDEBUG"</li>
 183 <li>p. 532      under -DSVDUMP, replace "a file named svdump" with "a file with extension .svd"</li>
 184 <li>p. 541      11th line from bottom: "-a" in wrong font</li>
 185 <li>p. 543      middle of page: "two for processes" -> "three for processes"</li>
 186 <li>p. 547      Americans would put "Dijkstra" above "Dillon" in alphabetical order. Dutchmen, though, recognize the "ij" as a single letter, and place "Dijkstra" below "Doran" as shown. Dijkstra was, of course, a Dutchman...</li>
 187 <li>p. 547      Entry for Emerson: "model logic" -> "modal logic"</li>
 188 <li>p. 553      13th line from bottom: "to represents" -> "to represent"</li>
 189 <li>p. 554      10th line from top: "product" -> "products"</li>
 190 <li>p. 561      DEADLOCK DETECTION, 1st line: "is system" -> "is a system"</li>
 191 <li>p. 561      10th line from bottom: replace "invalid endstate" with "valid endstate", and replace the subsentence after the comma with: "from which we can derive the definition of an invalid endstate, matching Spin's formalization of a system deadlock. In an invalid endstate at least one process has not reached its closing curly brace or a state marked with an endstate label."</li>
 192 <li>p. 565      4th line from top: "andq, r" -> "q and r"</li>
 193 <li>p. 566      define BDD (Binary Decision Diagram) and NP (Non-deterministic Polynomial)</li>
 194 <li>p. 572      l 8, wil -> will</li>
 195 <li>p. 575      10th line from bottom should be: spin -a -m ex2</li>
 196 <li>p. 575      9th line from bottom should be: cc -DPC -DBITSTATE -DSAFETY -o pan pan.c</li>
 197 <li>p. 577      C.9., 1st line: "an little" -> "a little"</li>
 198 <li>p. 579      5th line from top: "these tool" -> "these tools"</li>
 199 </ul>
 200 </font>
 201 <hr>
 202 Statistics:
 203 The list above contains
 204 roughly 128 reported typos and goofs in the first printing of the book.
 205 There are approximately 340K words in the book, giving 1 reported defect
 206 per 2,650 words written. At and average of 10 words per sentence, this is
 207 about 4 reported defects per 1,000 sentences in the book, which is roughly
 208 on par with a reasonably good software development process of 1-10 residual
 209 defects (<em>after</em> testing) per 1,000 lines of non-comment source code written.
 210 As in software, the number of reported defects depends both on the number of
 211 latent defects <em>and</em> on the number of users/readers
 212 (i.e., unread books will have no reported typos...).
 213 <hr>
 214 Note (*) on the example used on p. 20, provided by Heikki Tauriainen.
 215 <pre>
 216 Date: Wed, 01 Feb 2006 21:10:54 +0200 (EET)
 217 From: heikki.tauriainen [atsign] tkk [dot] fi
 218 Subject: Spin book: Doran & Thomas's mutual exclusion algorithm
 219
 220 Dear Dr. Holzmann,
 221
 222 Keijo Heljanko and I are giving at Helsinki University of Technology
 223 a basic course on parallel and distributed systems, using Spin for
 224 examples on model checking.  To demonstrate using the tool, we
 225 considered Dekker's mutual exclusion algorithm found in your Spin
 226 book (p. 20) and the variant of the algorithm by Doran and Thomas
 227 mentioned on p. 22.
 228
 229 According to the Spin book, Doran and Thomas's algorithm can be
 230 obtained from Dekker's algorithm by simply changing the outer do-loop
 231 of the algorithm into an if-selection, and this change is claimed to
 232 preserve the correctness of the algorithm.  This doesn't, however,
 233 seem to be the case, as the verification results using the Promela
 234 models distributed in the package
 235 <http://spinroot.com/spin/Doc/Book_extras/examples.tar.gz> were
 236 somewhat unexpected (unless, of course, the models in the package are
 237 deliberately faulty).  I'm referring to the file CH2/mutex.pml in the
 238 package.
 239
 240 The Promela model uses a preprocessor directive (DORAN) to choose
 241 between the algorithm with the do-loop and the algorithm with the
 242 if-selection. Verifying the model with the do-loop indeed gives the
 243 expected result (no assertion violations).  Firstly, however, Spin
 244 doesn't directly accept the model of the variant of the algorithm:
 245
 246 $ spin -DDORAN -a mutex.pml
 247 spin: line  30 "mutex.pml", Error: misplaced break statement    saw '-2'' near 'break'
 248 $
 249
 250 After the obvious change of making the 'break' keyword at line 30
 251 apply only to the variant with the do-loop, that is, changing lines
 252 29--35 to read
 253
 254         :: else ->
 255 #ifdef DORAN
 256         fi;
 257 #else
 258                 break
 259         od;
 260 #endif
 261
 262 and then verifying the mutual exclusion algorithm gives, however,
 263 the following (unexpected) result:
 264
 265 $ spin -DDORAN -a mutex.pml
 266 $ gcc -o -DBFS -o pan pan.c
 267 $ ./pan
 268 pan: assertion violated (cnt==1) (at depth 9)
 269 pan: wrote mutex.pml.trail
 270 (Spin Version 4.2.6 -- 27 October 2005)
 271 Warning: Search not completed
 272         + Using Breadth-First Search
 273         + Partial Order Reduction
 274
 275 Full statespace search for:
 276         never claim             - (none specified)
 277         assertion violations    +
 278         cycle checks            - (disabled by -DSAFETY)
 279         invalid end states      +
 280
 281 State-vector 20 byte, depth reached 9, errors: 1
 282       56 states, stored
 283               56 nominal states (stored-atomic)
 284       32 states, matched
 285       88 transitions (= stored+matched)
 286        0 atomic steps
 287 hash conflicts: 0 (resolved)
 288
 289 2.302   memory usage (Mbyte)
 290
 291 $ spin -DDORAN -p -t mutex.pml
 292 Starting mutex with pid 0
 293 Starting mutex with pid 1
 294   1:    proc  1 (mutex) line  11 "mutex.pml" (state 1)  [i = _pid]
 295   1:    proc  1 (mutex) line  12 "mutex.pml" (state 2)  [j = (1-_pid)]
 296   2:    proc  0 (mutex) line  11 "mutex.pml" (state 1)  [i = _pid]
 297   2:    proc  0 (mutex) line  12 "mutex.pml" (state 2)  [j = (1-_pid)]
 298   3:    proc  1 (mutex) line  14 "mutex.pml" (state 3)  [flag[i] = 1]
 299   4:    proc  1 (mutex) line  29 "mutex.pml" (state 12) [else]
 300   5:    proc  1 (mutex) line  37 "mutex.pml" (state 15) [cnt = (cnt+1)]
 301   6:    proc  0 (mutex) line  14 "mutex.pml" (state 3)  [flag[i] = 1]
 302   7:    proc  0 (mutex) line  21 "mutex.pml" (state 4)  [(flag[j])]
 303   8:    proc  0 (mutex) line  27 "mutex.pml" (state 9)  [else]
 304   9:    proc  0 (mutex) line  37 "mutex.pml" (state 15) [cnt = (cnt+1)]
 305 spin: trail ends after 9 steps
 306 #processes: 2
 307                 turn = 0
 308                 flag[0] = 1
 309                 flag[1] = 1
 310                 cnt = 2
 311   9:    proc  1 (mutex) line  38 "mutex.pml" (state 16)
 312   9:    proc  0 (mutex) line  38 "mutex.pml" (state 16)
 313 2 processes created
 314 $
 315
 316 Trying to find a reason for this unexpected result, I compared the
 317 model with the algorithm in Doran and Thomas's original article [1].
 318 It appears that the model in fact differs from that algorithm
 319 (repeated below from [1], Fig. 1)
 320
 321 Process A                           Process B
 322   1. A_needs := true;                    B_needs :=  true;
 323   2. if B_needs then begin               if A_needs then begin
 324   3.   if turn = 'B' then begin            if turn = 'A' then begin
 325   4.     A_needs := false;                   B_needs := false;
 326   5.     wait until turn = 'A';              wait until turn = 'B';
 327   6.     A_needs := true;                    B_needs := true;
 328   7.     end;                                end;
 329   8.   wait until !B_needs;                wait until !A_needs;
 330   9.   end;                                end;
 331  10. CRITICAL SECTION                    CRITICAL SECTION
 332  11. turn := 'B';                        turn := 'A';
 333  12. A_needs := false;                   B_needs := false;
 334  13. NON-CRITICAL SECTION                NON-CRITICAL SECTION
 335
 336 In particular, the Promela model has no corresponding construct for
 337 line 8 of this algorithm, which appears to be critical to its
 338 correctness: changing the outer if-selection to read
 339
 340         if
 341         :: flag[j] ->
 342                 if
 343                 :: turn == j ->
 344                         flag[i] = false;
 345                         !(turn == j);
 346                         flag[i] = true
 347                 :: else
 348                 fi;
 349                 (!flag[j]);    /* needed for correctness */
 350         :: else ->
 351         fi;
 352
 353 fixes the error.  However, it is not sufficient to simply
 354 replace the do-loop with an if-selection, although the wording
 355 on page 22 of the Spin book can be interpreteted to suggest
 356 otherwise (at least both I and Keijo were surprised, that's why
 357 we decided to write this report).
 358
 359 (The example file suggests that the model is taken from the book
 360 [2] instead of directly from Doran and Thomas's original article [1].
 361 As a matter of fact, this book---at least its English translation---contains the same error.  This is probably also the
 362 reason why the model is faulty.)
 363
 364 Best regards,
 365 Heikki Tauriainen
 366
 367
 368 References:
 369
 370 [1] R. W. Doran and L. K. Thomas.  Variants of the software solution to
 371     mutual exclusion.  Information Processing Letters 10(4--5):206--208,
 372     1980.
 373
 374 [2] M. Raynal.  Algorithms for mutual exclusion.  North Oxford Academic
 375     Publishers Ltd., 1986.
 376 </pre>
 377 <hr>
 378 <a href="http://spinroot.com/spin/Doc/Book_extras/index.html">book home page</a>
 379 <br>
 380 <a href="http://spinroot.com/spin/">Spin home page</a>
 381 <hr>
 382 <font size=2>Last updated: 1 February 2006</font>
 383 </html>