+++ /dev/null
-<html>\r
-<head>\r
-<title>Book Errata - The Spin Model Checker</title>\r
-</head>\r
-<h3>Typos found in the first printing (August 2003)</h3>\r
-<font face=helvetica,arial>\r
-<ul>\r
-<li>p. vi chapter 8 topic listings, Breath-First -> Breadth-First</li>\r
-<li>p. 2 line 16 "always explicitly" -> "usually"</li>\r
-<li>p. 3 figure 1.1 is mirror reversed</li>\r
-<li>p. 4 the website crashdatabas.com no longer seems to exist</li>\r
-<li>p. 20 See note (*) below, provided by Heikki Tauriainen (Feb 1, 2006).\r
-<li>p. 22 6th line from the bottom: "if" -> "of"</li>\r
-<li>p. 25 4th line from the bottom: "variable in" -> "variable cnt"</li>\r
-<li>p. 26 10th line from bottom: "set to false" -> "set to true"</li>\r
-<li>p. 27 an error slipped into Figure 2.6. The fragment\r
-<pre>\r
- M?data -> /* receive data */\r
- do\r
- :: W!data /* send data */\r
- :: W!shutup; /* or shutdown */\r
- break\r
- od\r
-</pre>\r
-is an unfortunate last-minute rewrite of the originally intended version:\r
-<pre>\r
- do\r
- :: M?data -> W!data\r
- :: M?data -> W!shutup;\r
- break\r
- od\r
-</pre>\r
-The behavior is of course not equivalent.\r
-In particular, the version in the book cannot create the error scenario\r
-given on page 29, but the intended version can.</li>\r
-<li>p. 33 8th line from bottom: "the specification" -> "the specification of"</li>\r
-<li>p. 33 3rd line from bottom: "functions pointers" -> "function pointers</li>\r
-<li>p. 41 "1 <= n <= 32" -> "1 <= n < 32".</li>\r
-<li>p. 43 appel -> apple</li>\r
-<li>p. 52 11th line from the top: "p. 39." -> "p. 38."</li>\r
-<li>p. 69 bottom line: "exclusive read and exclusive write" -> "exclusive receive and exclusive send"</li>\r
-<li>p. 75 and 548 Goldstein -> Goldstine</li>\r
-<li>p. 81 and 271 pan.trail -> fair.pml.trail</li>\r
-<li>p. 81 3rd line from the bottom: "trace fpr" -> "trace for"</li>\r
-<li>p. 82 18th line from the bottom: "process than" -> "process that"</li>\r
-<li>p. 92 4th line from bottom: "Even traces" -> "Event traces"</li>\r
-<li>p. 96 middle of page identify -> identity</li>\r
-<li>p. 96 l. -6, for -> by</li>\r
-<li>p. 111 below figure 5.4: "f==free" -> "f=free"</li>\r
-<li>p. 119 12th line from the bottom; "xDm" -> "Dm"</li>\r
-<li>p. 121 figure 5.8, in captions on bottom two figures: "p" -> "q"</li>\r
-<li>p. 137 14th line from bottom (first rule in list): first 3 chars in wrong font</li>\r
-<li>p. 139 last line; italic P -> roman P</li>\r
-<li>p. 142 3rd line from bottom: "reach" -> "reached"</li>\r
-<li>p. 142 5th line from bottom: omit comma</li>\r
-<li>p. 148 middle of the page: "can be express" -> "can be expressed"</li>\r
-<li>p. 149 5th line from bottom: "eventually always" -> "always eventually"</li>\r
-<li>p. 150 replace "it is impossible for p to hold only in even steps in a run, but never at odd steps"\r
-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>\r
-<li>p. 150 Omega-Regular Properties, line 1: "that" -> "than"</li>\r
-<li>p. 158 middle of page: redundant space after "("</li>\r
-<li>p. 168 the list of properties given for < and > is not exhaustive</li>\r
-<li>p. 174 11th line from bottom: "but" -> "by"</li>\r
-<li>p. 177 Procedure Search() in Figure 8.6 is incorrect. A corrected version is:\r
-<pre>\r
-Search()\r
-{\r
- while (Empty_Queue(D) == false)\r
- { s = Del_Queue(D)\r
- for each (s,1,s') member A.T\r
- if In_Statespace(V, s') == false\r
- { Add_Statespace(V, s')\r
- Add_Queue(D, s')\r
- }\r
- }\r
-}\r
-</pre>\r
-</li>\r
-<li>p. 178 2nd line from top: "at state" -> "at each state", "of each state" -> "of that state"</li>\r
-<li>p. 179 lead -> led</li>\r
-<li>p. 180 before first 'if' stmnt inside for loop add: if (toggle == true)</li>\r
-<li>p. 185 Fig. 8.10, circle at s^{1}_{2} should be dotted</li>\r
-<li>p. 187 line -11: "interative" -> "iterative"</li>\r
-<li>p. 188 replace "(RxB)+(k+2)" with "Rx(B+k+2)"</li>\r
-<li>p. 193 Fig. 9.2, the two circles labeled 0,1,0 should be dashed</li>\r
-<li>p. 193 7th line from bottom: "g=g*2," -> "g=g*2."</li>\r
-<li>p. 196 line -9: "control control" -> "control"</li>\r
-<li>p. 204 last line, "to 133 seconds" -> "to 53 seconds"</li>\r
-<li>p. 208 a goof: m changes from bits to bytes between 2nd and 3rd paragraph</li>\r
-<li>p. 209 in first two formulas: (1-1/m) sup {kr}.</li>\r
-<li>p. 211 3rd line from below: probabilitie -> probabilities</li>\r
-<li>p. 212 line -2: "ration" -> "ratio"</li>\r
-<li>p. 214 A formal -> Formal</li>\r
-<li>p. 216 1st-2nd line: 'collissions' -> 'collisions'</li>\r
-<li>p. 219 last paragraph: missing right parenthesis</li>\r
-<li>p. 228 Celcius -> Celsius</li>\r
-<li>p. 228 in the list at the bottom: there are just 6 entries with 'keep' as a target</li>\r
-<li>p. 237 12th line from below: "postive" -> "zero".</li>\r
-<li>p. 237 4th line from below: "unsound" -> "incomplete".</li>\r
-<li>p. 238 knifes -> knives</li>\r
-<li>p. 241 7th line from bottom: "world0" -> "world\n"</li>\r
-<li>p. 243 Pressburger -> Presburger</li>\r
-<li>p. 251 Selet -> Select</li>\r
-<li>p. 262 10th line from bottom: "do to" -> "due to"</li>\r
-<li>p. 272 an basic -> a basic</li>\r
-<li>p. 272 "As a special feature [...], if the statement" omit "if"</li>\r
-<li>p. 279 "#define q" -> "#define r"\r
-<!--\r
-<li>p. 280 (strong) -> (weak)</li>\r
--->\r
-<li>p. 281 Automata View -> Automaton View</li>\r
-<li>p. 283 The correct wording of the quote from Willem L. van der Poel, as corrected by its author:\r
- <pre>"There are no wrong programs, it simply is another program."</pre>\r
- (email from the author, Feb 1, 2006).\r
-<li>p. 284 8th line from bottom: omit "blue"</li>\r
-<li>p. 287 6th line from top: omit "blue"</li>\r
-<li>p. 307 top of page: "ringtone" -> "ring tone" </li>\r
-<li>p. 307 top of page: "dialtone" -> "dial tone"</li>\r
-<li>p. 307 top of page: "notone" -> "no tone"</li>\r
-<!-- <li>p. 332 3rd line from bottom: UTS without a trademark (see also next page, 1x)</li> -->\r
-<li>p. 333 11th line from top: "and early version" -> "an early version"</li>\r
-<li>p. 338 the line numbered [19] is actually from the FIX</li>\r
-<li>p. 339 6th line from below: pid 1 -> pid 0</li>\r
-<li>p. 393 2nd line from top: "innermostn" -> "innermost"</li>\r
-<li>p. 341 10th line from top: "body ," -> "body,"</li>\r
-<li>p. 346 identificatio -> identification</li>\r
-<li>p. 346 middle of the page: "tranaction" -> "transaction"</li>\r
-<li>p. 349 55 is not the integer square root of either 1024 or 3601.</li>\r
-<li>p. 356 n=1<<30 does not fail on all systems</li>\r
-<li>p. 359 Fig. 15.8: what looks like commas are really single quotes</li>\r
-<li>p. 359 Fig. 15.8: the automaton fails to detect strings that start inside a comment;</li>\r
-unfortunate given the example that also appears on this page...</li>\r
-<li>p. 365 the grammar listing misses productions for inlines</li>\r
-<li>p. 365 [active] PROCTYPE -> [active ['[' const ']']] PROCTYPE</li>\r
-<li>p. 367 "PRINT" -> "PRINTF"</li>\r
-<li>p. 369 in PREDEFINED: "373last" -> "374"</li>\r
-<li>p. 369 in PREDEFINED: "373nr_pr" -> "376"</li>\r
-<li>p. 369 5th line from bottom: "special case" -> "special cases"</li>\r
-<li>p. 370 8th line from bottom: "p.272" -> "p. 272"</li>\r
-<li>p. 370 2nd line from bottom: "(434)" -> "(p. 434)"</li>\r
-<li>p. 370 2nd line from bottom: "(p, 483)" -> "(p. 483)"</li>\r
-<li>p. 371 2nd line from top: "Two" -> "Three"</li>\r
-<li>p. 371 9th line from top: "or both of the above two" -> "of the above" </li>\r
-<li>p. 374 11th line from bottom: "from into" -> "to"</li>\r
-<li>p. 376 5th line from bottom: "at 256" -> "at 255"</li>\r
-<li>p. 377 5th line in DESCRIPTION: "process" -> "processes"</li>\r
-<li>p. 381 4th line from bottom: "four process" -> "four processes"</li>\r
-<li>p. 381 3rd line from bottom: "to three" -> "to four"</li>\r
-<li>p. 390 9th line from bottom: "recepient" -> "recipient"</li>\r
-<li>p. 393 10th line from bottom: "label L1" -> "label L2"\r
-<li>p. 395 6th line from top: "multiple field" -> "multiple fields"</li>\r
-<li>p. 397 4th line from top: "the the" -> "the"</li>\r
-<li>p. 398 11th line from bottom: redundant space after "("</li>\r
-<li>p. 402 7th line from top, "accidentily" -> "accidentally"</li>\r
-<li>p. 404 mixed fonts in Table</li>\r
-<li>p. 404 5th line from bottom: "the fact the" -> "the fact that the"</li>\r
-<li>p. 407 in Notes, 2nd line: "tha" -> "that"</li>\r
-<li>p. 408 "(x < 0)" -> "(x <= 0)"</li>\r
-<li>p. 411 last line: "ltl len" -> "ltl, len"</li>\r
-<li>p. 425 11th line from top: "followin" -> "following"</li>\r
-<li>p. 440 11th line from top: "equivalents" -> "equivalent"</li>\r
-<li>p. 441 middle of page: "LTL formula" -> "LTL formulae"</li>\r
-<li>p. 446 10th line from top: "equivalents" -> "equivalent"</li>\r
-<li>p. 450 last example in notes should be: atomic { P && qname?[ack,var] -> qname?ack,var }</li>\r
-<li>p. 452 15th line from bottom: "will included" -> "will be included"</li>\r
-<li>p. 455 5th line from top: "restrction" -> "restriction"</li>\r
-<li>p. 456 middle of page: "type main" -> "type fact"</li>\r
-<li>p. 456 12th line from bottom: "2,147,483,648" ->"2,147,483,647"</li>\r
-<li>p. 456 10th line from bottom: 13! = 6,227,020,800 (and so even 13! > 2^31-1)</li>\r
-<li>p. 464 9th line from bottom: "just and safe" -> "justified and safe" (2x)</li>\r
-<li>p. 466 1st line in EFFECT: "to the" -> "of the" </li>\r
-<li>p. 476 in EXAMPLES (2x): "b = a" -> "b = tmp"</li>\r
-<li>p. 479 7th line from top: "can are" -> "are"</li>\r
-<li>p. 496 6th line: "in in" -> "in"</li>\r
-<li>p. 498 2nd line from bottom: "coord.trail" -> "example.trail"</li>\r
-<li>p. 509 13th line from bottom: "known the" -> "known. The"</li>\r
-<li>p. 512 middle of page: "an pointer" -> "a pointer"</li>\r
-<li>p. 518 l -8, most -> must</li>\r
-<li>p. 519 l -10, -rthis -> -r, this</li>\r
-<li>p. 521 5th line from bottom: "substitions" -> "substitutions"</li>\r
-<li>p. 528 under basic options -DBFS, "reducting" -> "reducing"</li>\r
-<li>p. 532 under -DSDUMP, replace "-DCHECK" with: "-DVERBOSE or -DDEBUG"</li>\r
-<li>p. 532 under -DSVDUMP, replace "a file named svdump" with "a file with extension .svd"</li>\r
-<li>p. 541 11th line from bottom: "-a" in wrong font</li>\r
-<li>p. 543 middle of page: "two for processes" -> "three for processes"</li>\r
-<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>\r
-<li>p. 547 Entry for Emerson: "model logic" -> "modal logic"</li>\r
-<li>p. 553 13th line from bottom: "to represents" -> "to represent"</li>\r
-<li>p. 554 10th line from top: "product" -> "products"</li>\r
-<li>p. 561 DEADLOCK DETECTION, 1st line: "is system" -> "is a system"</li>\r
-<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>\r
-<li>p. 565 4th line from top: "andq, r" -> "q and r"</li>\r
-<li>p. 566 define BDD (Binary Decision Diagram) and NP (Non-deterministic Polynomial)</li>\r
-<li>p. 572 l 8, wil -> will</li>\r
-<li>p. 575 10th line from bottom should be: spin -a -m ex2</li>\r
-<li>p. 575 9th line from bottom should be: cc -DPC -DBITSTATE -DSAFETY -o pan pan.c</li>\r
-<li>p. 577 C.9., 1st line: "an little" -> "a little"</li>\r
-<li>p. 579 5th line from top: "these tool" -> "these tools"</li>\r
-</ul>\r
-</font>\r
-<hr>\r
-Statistics:\r
-The list above contains\r
-roughly 128 reported typos and goofs in the first printing of the book.\r
-There are approximately 340K words in the book, giving 1 reported defect\r
-per 2,650 words written. At and average of 10 words per sentence, this is\r
-about 4 reported defects per 1,000 sentences in the book, which is roughly\r
-on par with a reasonably good software development process of 1-10 residual\r
-defects (<em>after</em> testing) per 1,000 lines of non-comment source code written.\r
-As in software, the number of reported defects depends both on the number of\r
-latent defects <em>and</em> on the number of users/readers\r
-(i.e., unread books will have no reported typos...).\r
-<hr>\r
-Note (*) on the example used on p. 20, provided by Heikki Tauriainen.\r
-<pre>\r
-Date: Wed, 01 Feb 2006 21:10:54 +0200 (EET) \r
-From: heikki.tauriainen [atsign] tkk [dot] fi \r
-Subject: Spin book: Doran & Thomas's mutual exclusion algorithm \r
-\r
-Dear Dr. Holzmann,\r
-\r
-Keijo Heljanko and I are giving at Helsinki University of Technology\r
-a basic course on parallel and distributed systems, using Spin for\r
-examples on model checking. To demonstrate using the tool, we\r
-considered Dekker's mutual exclusion algorithm found in your Spin\r
-book (p. 20) and the variant of the algorithm by Doran and Thomas\r
-mentioned on p. 22.\r
-\r
-According to the Spin book, Doran and Thomas's algorithm can be\r
-obtained from Dekker's algorithm by simply changing the outer do-loop\r
-of the algorithm into an if-selection, and this change is claimed to\r
-preserve the correctness of the algorithm. This doesn't, however,\r
-seem to be the case, as the verification results using the Promela\r
-models distributed in the package\r
-<http://spinroot.com/spin/Doc/Book_extras/examples.tar.gz> were\r
-somewhat unexpected (unless, of course, the models in the package are\r
-deliberately faulty). I'm referring to the file CH2/mutex.pml in the\r
-package.\r
-\r
-The Promela model uses a preprocessor directive (DORAN) to choose\r
-between the algorithm with the do-loop and the algorithm with the\r
-if-selection. Verifying the model with the do-loop indeed gives the\r
-expected result (no assertion violations). Firstly, however, Spin\r
-doesn't directly accept the model of the variant of the algorithm:\r
-\r
-$ spin -DDORAN -a mutex.pml\r
-spin: line 30 "mutex.pml", Error: misplaced break statement saw '-2'' near 'break'\r
-$\r
-\r
-After the obvious change of making the 'break' keyword at line 30\r
-apply only to the variant with the do-loop, that is, changing lines\r
-29--35 to read\r
-\r
- :: else ->\r
-#ifdef DORAN\r
- fi;\r
-#else\r
- break\r
- od;\r
-#endif\r
-\r
-and then verifying the mutual exclusion algorithm gives, however,\r
-the following (unexpected) result:\r
-\r
-$ spin -DDORAN -a mutex.pml\r
-$ gcc -o -DBFS -o pan pan.c\r
-$ ./pan\r
-pan: assertion violated (cnt==1) (at depth 9)\r
-pan: wrote mutex.pml.trail\r
-(Spin Version 4.2.6 -- 27 October 2005)\r
-Warning: Search not completed\r
- + Using Breadth-First Search\r
- + Partial Order Reduction\r
-\r
-Full statespace search for:\r
- never claim - (none specified)\r
- assertion violations +\r
- cycle checks - (disabled by -DSAFETY)\r
- invalid end states +\r
-\r
-State-vector 20 byte, depth reached 9, errors: 1\r
- 56 states, stored\r
- 56 nominal states (stored-atomic)\r
- 32 states, matched\r
- 88 transitions (= stored+matched)\r
- 0 atomic steps\r
-hash conflicts: 0 (resolved)\r
-\r
-2.302 memory usage (Mbyte)\r
-\r
-$ spin -DDORAN -p -t mutex.pml\r
-Starting mutex with pid 0\r
-Starting mutex with pid 1\r
- 1: proc 1 (mutex) line 11 "mutex.pml" (state 1) [i = _pid]\r
- 1: proc 1 (mutex) line 12 "mutex.pml" (state 2) [j = (1-_pid)]\r
- 2: proc 0 (mutex) line 11 "mutex.pml" (state 1) [i = _pid]\r
- 2: proc 0 (mutex) line 12 "mutex.pml" (state 2) [j = (1-_pid)]\r
- 3: proc 1 (mutex) line 14 "mutex.pml" (state 3) [flag[i] = 1]\r
- 4: proc 1 (mutex) line 29 "mutex.pml" (state 12) [else]\r
- 5: proc 1 (mutex) line 37 "mutex.pml" (state 15) [cnt = (cnt+1)]\r
- 6: proc 0 (mutex) line 14 "mutex.pml" (state 3) [flag[i] = 1]\r
- 7: proc 0 (mutex) line 21 "mutex.pml" (state 4) [(flag[j])]\r
- 8: proc 0 (mutex) line 27 "mutex.pml" (state 9) [else]\r
- 9: proc 0 (mutex) line 37 "mutex.pml" (state 15) [cnt = (cnt+1)]\r
-spin: trail ends after 9 steps\r
-#processes: 2\r
- turn = 0\r
- flag[0] = 1\r
- flag[1] = 1\r
- cnt = 2\r
- 9: proc 1 (mutex) line 38 "mutex.pml" (state 16)\r
- 9: proc 0 (mutex) line 38 "mutex.pml" (state 16)\r
-2 processes created\r
-$\r
-\r
-Trying to find a reason for this unexpected result, I compared the\r
-model with the algorithm in Doran and Thomas's original article [1].\r
-It appears that the model in fact differs from that algorithm\r
-(repeated below from [1], Fig. 1)\r
-\r
-Process A Process B\r
- 1. A_needs := true; B_needs := true;\r
- 2. if B_needs then begin if A_needs then begin\r
- 3. if turn = 'B' then begin if turn = 'A' then begin\r
- 4. A_needs := false; B_needs := false;\r
- 5. wait until turn = 'A'; wait until turn = 'B';\r
- 6. A_needs := true; B_needs := true;\r
- 7. end; end;\r
- 8. wait until !B_needs; wait until !A_needs;\r
- 9. end; end;\r
- 10. CRITICAL SECTION CRITICAL SECTION\r
- 11. turn := 'B'; turn := 'A';\r
- 12. A_needs := false; B_needs := false;\r
- 13. NON-CRITICAL SECTION NON-CRITICAL SECTION\r
-\r
-In particular, the Promela model has no corresponding construct for\r
-line 8 of this algorithm, which appears to be critical to its\r
-correctness: changing the outer if-selection to read\r
-\r
- if\r
- :: flag[j] ->\r
- if\r
- :: turn == j ->\r
- flag[i] = false;\r
- !(turn == j);\r
- flag[i] = true\r
- :: else\r
- fi;\r
- (!flag[j]); /* needed for correctness */\r
- :: else ->\r
- fi;\r
-\r
-fixes the error. However, it is not sufficient to simply\r
-replace the do-loop with an if-selection, although the wording\r
-on page 22 of the Spin book can be interpreteted to suggest\r
-otherwise (at least both I and Keijo were surprised, that's why\r
-we decided to write this report).\r
-\r
-(The example file suggests that the model is taken from the book\r
-[2] instead of directly from Doran and Thomas's original article [1].\r
-As a matter of fact, this book---at least its English translation---contains the same error. This is probably also the\r
-reason why the model is faulty.)\r
-\r
-Best regards,\r
-Heikki Tauriainen\r
-\r
-\r
-References:\r
-\r
-[1] R. W. Doran and L. K. Thomas. Variants of the software solution to\r
- mutual exclusion. Information Processing Letters 10(4--5):206--208,\r
- 1980.\r
-\r
-[2] M. Raynal. Algorithms for mutual exclusion. North Oxford Academic\r
- Publishers Ltd., 1986.\r
-</pre>\r
-<hr>\r
-<a href="http://spinroot.com/spin/Doc/Book_extras/index.html">book home page</a>\r
-<br>\r
-<a href="http://spinroot.com/spin/">Spin home page</a>\r
-<hr>\r
-<font size=2>Last updated: 1 February 2006</font>\r
-</html>\r
projects / lttv.git / blobdiff