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