0b55f123 |
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 |