| 1 | Errata for `Design and Validation of Computer Protocols' |
| 2 | [trivial typos not listed] |
| 3 | |
| 4 | CHAPTER 2, page 26 - Example of a Shorter Error Scenario |
| 5 | ============================================================ |
| 6 | |
| 7 | A duplicate message can be accepted after even a single |
| 8 | transmission error occurs. E.g.: |
| 9 | |
| 10 | (A) (B) |
| 11 | ~ ~ |
| 12 | | | |
| 13 | | ack 'z' /-----------<---------+ |
| 14 | +-----------/ | |
| 15 | accept(z) | | |
| 16 | +-----------\ ack 'a' -> err | |
| 17 | | \----------->--------+ |
| 18 | | | |
| 19 | | nak 'z' /-----------<--------+ |
| 20 | +------------/ | |
| 21 | accept(z) | | |
| 22 | |
| 23 | |
| 24 | CHAPTER 3, page 61/62 - Revised CRC-Algorithm |
| 25 | (Bits renumbered in more standard right to left order.) |
| 26 | ============================================================ |
| 27 | |
| 28 | The following C program, by Don Mitchell of AT&T Bell |
| 29 | Laboratories, generates a lookup table for an arbitrary |
| 30 | checksum polynomial. Input for the routine is an octal |
| 31 | number, specified as an argument, that encodes the generator |
| 32 | polynomial. |
| 33 | In the version of the program shown here, compliments of Ned |
| 34 | W. Rhodes, Software Systems Group, bits are numbered from |
| 35 | zero to r-1, with bit zero corresponding to the right-most |
| 36 | bit, and r the degree of the generator polynomial. (In |
| 37 | Mitchell's original algorithm the bits in the message and |
| 38 | generator polynomial were reversed.) The r-th bit itself is |
| 39 | omitted from the code word, since it is implicit in the |
| 40 | length. Using this program takes two separate steps. |
| 41 | First, the program is compiled and run to generate the |
| 42 | lookup tables. Then the checksum generation routine can be |
| 43 | compiled, with the precalculated lookup tables in place. On |
| 44 | a UNIX system, the program is compiled as |
| 45 | |
| 46 | $ cc -o crc_init crc_init.c |
| 47 | |
| 48 | Lookup tables for the two most popular CRC-polynomials can |
| 49 | now be produced as follows: |
| 50 | |
| 51 | $ crc_init 0100005 > crc_16.h |
| 52 | $ crc_init 010041 > crc_ccitt.h |
| 53 | |
| 54 | This is the text of crc_init.c: |
| 55 | |
| 56 | |
| 57 | main(argc, argv) |
| 58 | int argc; char *argv[]; |
| 59 | { |
| 60 | unsigned long crc, poly; |
| 61 | int n, i; |
| 62 | |
| 63 | sscanf(argv[1], "%lo", &poly); |
| 64 | if (poly & 0xffff0000) |
| 65 | { fprintf(stderr, "polynomial is too large\n"); |
| 66 | exit(1); |
| 67 | } |
| 68 | |
| 69 | printf("/*\n * CRC 0%o\n */\n", poly); |
| 70 | printf("static unsigned short crc_table[256] = {\n"); |
| 71 | for (n = 0; n < 256; n++) |
| 72 | { if (n % 8 == 0) printf(" "); |
| 73 | crc = n << 8; |
| 74 | for (i = 0; i < 8; i++) |
| 75 | { if (crc & 0x8000) |
| 76 | crc = (crc << 1) ^ poly; |
| 77 | else |
| 78 | crc <<= 1; |
| 79 | crc &= 0xFFFF; |
| 80 | } |
| 81 | if (n == 255) printf("0x%04X ", crc); |
| 82 | else printf("0x%04X, ", crc); |
| 83 | if (n % 8 == 7) printf("\n"); |
| 84 | } |
| 85 | exit(0); |
| 86 | } |
| 87 | |
| 88 | The table can now be used to generate checksums: |
| 89 | |
| 90 | unsigned short |
| 91 | cksum(s, n) |
| 92 | register unsigned char *s; |
| 93 | register int n; |
| 94 | { |
| 95 | register unsigned short crc=0; |
| 96 | |
| 97 | while (n-- > 0) |
| 98 | crc = crc_table[(crc>>8 ^ *s++) & 0xff] ^ (crc<<8); |
| 99 | |
| 100 | return crc; |
| 101 | } |
| 102 | |
| 103 | |
| 104 | CHAPTER 4, page 81 - Typo |
| 105 | ============================================================ |
| 106 | |
| 107 | old< Taking the modulo M effect into account, this becomes: |
| 108 | valid(m) = ( 0 < p - m <= W ) || ( 0 < p - M - m <= W ) |
| 109 | |
| 110 | new> Taking the modulo M effect into account (p is always |
| 111 | smaller than M), this becomes: |
| 112 | valid(m) = ( 0 < p - m <= W ) || ( 0 < p + M - m <= W ) |
| 113 | |
| 114 | ERROR, Page 83, Figure 4.14 |
| 115 | =========================== |
| 116 | |
| 117 | should not "accept:i" if (a==e) is false |
| 118 | |
| 119 | |
| 120 | CHAPTER 5, error/typos |
| 121 | =========================== |
| 122 | |
| 123 | Page 96, bottom |
| 124 | |
| 125 | The mutual exclusion algorithm attributed to Dekker is |
| 126 | really a simplication of Dekker's algorithm that is known |
| 127 | as Peterson's algorithm. |
| 128 | Dekker's original solution is modeled in Promela like this: |
| 129 | |
| 130 | #define true 1 |
| 131 | #define false 0 |
| 132 | #define Aturn 1 |
| 133 | #define Bturn 0 |
| 134 | |
| 135 | bool x, y, t; |
| 136 | |
| 137 | proctype A() |
| 138 | { |
| 139 | do |
| 140 | :: x = true; |
| 141 | if |
| 142 | :: y == true && t == Bturn -> |
| 143 | x = false; |
| 144 | (t == Aturn) |
| 145 | :: y == false -> |
| 146 | break |
| 147 | fi |
| 148 | od; |
| 149 | |
| 150 | /* critical section */ |
| 151 | |
| 152 | t = Bturn; |
| 153 | x = false |
| 154 | } |
| 155 | |
| 156 | proctype B() |
| 157 | { |
| 158 | do |
| 159 | :: y = true; |
| 160 | if |
| 161 | :: x == true && t == Aturn -> |
| 162 | y = false; |
| 163 | (t == Bturn) |
| 164 | :: x == false -> |
| 165 | break |
| 166 | fi |
| 167 | od; |
| 168 | |
| 169 | /* critical section */ |
| 170 | |
| 171 | t = Aturn; |
| 172 | y = false |
| 173 | } |
| 174 | |
| 175 | init { run A(); run B() } |
| 176 | |
| 177 | =========================== |
| 178 | |
| 179 | Page 98, last paragraph |
| 180 | |
| 181 | old> "If the receive operation tries to retrieve more parameters |
| 182 | than are available, the value of the extra parameters is undefined; |
| 183 | if it receives fewer than the number of parameters that was sent, |
| 184 | the extra information is lost." |
| 185 | new> "It is always an error if the receive operation tries to retrieve |
| 186 | a different number of parameters than the corresponding channel |
| 187 | declaration specifies." |
| 188 | |
| 189 | =========================== |
| 190 | |
| 191 | Page 99, last line of "init", middle of page: |
| 192 | |
| 193 | old< qname!qforb |
| 194 | |
| 195 | new> qname[0]!qforb |
| 196 | |
| 197 | Page 100, delete last line on page: |
| 198 | |
| 199 | old< byte name; /* delete */ |
| 200 | |
| 201 | Page 103, in the Dijkstra example: |
| 202 | |
| 203 | old< chan sema = [0] of { bit }; |
| 204 | |
| 205 | new> chan sema = [0] of { mtype }; |
| 206 | |
| 207 | Page 108, "init" section, top of page: |
| 208 | |
| 209 | old< chan Ain = [2] of { byte }; |
| 210 | chan Bin = [2] of { byte }; |
| 211 | chan Aout = [2] of { byte }; |
| 212 | chan Bout = [2] of { byte }; |
| 213 | |
| 214 | new> chan Ain = [2] of { byte, byte }; |
| 215 | chan Bin = [2] of { byte, byte }; |
| 216 | chan Aout = [2] of { byte, byte }; |
| 217 | chan Bout = [2] of { byte, byte }; |
| 218 | |
| 219 | =========================== |
| 220 | |
| 221 | Page 107, last sentence of first paragraph Section 5.12: |
| 222 | |
| 223 | old< discussed in Section 2.4. |
| 224 | new> discussed in Section 2.3. |
| 225 | |
| 226 | =========================== |
| 227 | |
| 228 | Page 110, exercise 5-3: |
| 229 | |
| 230 | old< Revise the two programs from Section 5.6 |
| 231 | new> Revise the two programs from Section 5.8 |
| 232 | |
| 233 | |
| 234 | CHAPTER 6 |
| 235 | |
| 236 | |
| 237 | TYPO, page 117 |
| 238 | ======================= |
| 239 | old< chan sema[0] of {bit}; |
| 240 | new> chan sema = [0] of {bit}; |
| 241 | |
| 242 | SERIOUS OMISSION, Section 6.4, page 116-117: |
| 243 | ================================================= |
| 244 | The treatment of formalizing system invariants in a 1-statement |
| 245 | monitor process is correct only if the model does not contain |
| 246 | any timeout statements. |
| 247 | If it does, the statements in the model that would be executed |
| 248 | after a timeout expires are not checked (since assert is always |
| 249 | executable, it would always be executed before the timeout expires |
| 250 | under default timeout heuristics used in spin). |
| 251 | there are two possible solutions: |
| 252 | |
| 253 | - disable the default timeout heuristics for a fully exhaustive |
| 254 | search for all possible choices of timeouts (brute force) |
| 255 | to do this, include a single line |
| 256 | #define timeout skip |
| 257 | as the first line of your model - and nothing else has to change |
| 258 | |
| 259 | - use a safer formalization of the system invariant, using a never claim. |
| 260 | the simples formalization is: |
| 261 | never { do :: assert(invariant) od } |
| 262 | which checks the truth of the invariant for every reachable state, |
| 263 | independent of timeouts. |
| 264 | another way would be to use the implicit matching behavior of a never |
| 265 | claim, without an explicit assertion: |
| 266 | never |
| 267 | { do |
| 268 | :: (invariant) /* things are fine, the invariant holds */ |
| 269 | :: !(invariant) -> break /* invariant fails - match */ |
| 270 | od |
| 271 | } |
| 272 | |
| 273 | CLARIFICATION, page 118, Section 6.5 |
| 274 | ==================================== |
| 275 | The validator SPIN does not enforce the second criterion |
| 276 | for a proper endstate, i.e., the emptiness of all channels. |
| 277 | It does enforce the revised first criterion from the bottom |
| 278 | of page 118. |
| 279 | |
| 280 | TYPO, page 121 middle: |
| 281 | ================================================= |
| 282 | |
| 283 | old< never { do :: skip od -> P -> !Q } |
| 284 | |
| 285 | new> never { do :: skip :: break od -> P -> !Q } |
| 286 | |
| 287 | ADDED EXPLANATIONS (throughout page 121 and onw.): |
| 288 | ================================================= |
| 289 | |
| 290 | A terminating claim is matched, and the corresponding correctness |
| 291 | property thereby violated, if and when the claim body terminates. |
| 292 | |
| 293 | A non-terminating claim is matched, and the corresponding |
| 294 | correctness property violated, if and when an acceptance cycle |
| 295 | is detected. |
| 296 | |
| 297 | SPECIFYING TEMPORAL CLAIMS |
| 298 | |
| 299 | The body of a temporal claim is defined just like PROMELA |
| 300 | proctype bodies. This means that all control flow struc- |
| 301 | tures, such as if-fi selections, do-od repetitions, and |
| 302 | goto jumps, are allowed. There is, however, one important |
| 303 | difference: |
| 304 | |
| 305 | Every statement inside a temporal claim is (interpreted |
| 306 | as) a boolean condition. |
| 307 | |
| 308 | Specifically, this means that the statements inside temporal |
| 309 | claims should be free of side-effects. For reference, the |
| 310 | PROMELA statements with side-effects are: assignments, |
| 311 | assertions, sends, receives, and printf statements. |
| 312 | |
| 313 | Temporal claims are used to express system |
| 314 | behaviors that are considered undesirable or illegal. We |
| 315 | say that a temporal claim is matched if the undesirable |
| 316 | behavior can be realized, and thus our correctness claim can |
| 317 | be violated. The most useful application of temporal claims |
| 318 | is in combination with acceptance labels. There are then |
| 319 | two ways to match a temporal claim, depending on whether the |
| 320 | undesirable behavior defines terminating or cyclic execution |
| 321 | sequences. |
| 322 | |
| 323 | For a terminating execution sequence, a temporal claim |
| 324 | is matched only when it can terminate (reaches the |
| 325 | closing curly brace) That is, the claim can be violated |
| 326 | if the closing curly brace of the PROMELA body of the |
| 327 | claim is reachable. |
| 328 | |
| 329 | For a cyclic execution sequence, the claim is matched |
| 330 | only when an explicit acceptance cycle exists. The |
| 331 | acceptance labels within temporal claims are user |
| 332 | defined, there are no defaults. This means that in the |
| 333 | absence of acceptance labels no cyclic behavior can be |
| 334 | matched by a temporal claim. It also means that to |
| 335 | check a cyclic temporal claim, acceptance labels should |
| 336 | only occur within the claim and not elsewhere in the |
| 337 | PROMELA code. |
| 338 | |
| 339 | ERROR, page 124, top |
| 340 | ======================= |
| 341 | old< :: len(receiver) == 0 |
| 342 | |
| 343 | new> :: skip /* allow any time delay */ |
| 344 | |
| 345 | ERROR, page 125, top |
| 346 | ======================= |
| 347 | the claim can of course always be violated (== matched), |
| 348 | whether timeout is redefined or not. |
| 349 | |
| 350 | CHAPTER 7 |
| 351 | |
| 352 | ERROR, page 139, bottom |
| 353 | ======================= |
| 354 | old< Pr(Burst >= 17) = 0.08 . e ^ { -0.08 . 17 } = 0.007 |
| 355 | |
| 356 | new> Pr(Burst >= 17) = 0.009 . e ^ { -0.009 . 17 } = 0.007 |
| 357 | |
| 358 | ERROR, page 156, middle |
| 359 | ======================= |
| 360 | old< flow_to_dll[n]!sync_ack,0 |
| 361 | new> flow_to_dll[n]!sync_ack,m |
| 362 | (and move the new line up to precede: "m=0;") |
| 363 | |
| 364 | old< flow_to_ses[n]!sync_ack,0 |
| 365 | new> flow_to_ses[n]!sync_ack,m |
| 366 | |
| 367 | old< To avoid circularity, the synchronization messages |
| 368 | do not carry sequence numbers. |
| 369 | new> The sync_ack message echos the session number of the |
| 370 | sync message. |
| 371 | |
| 372 | ERROR, page 156, bottom |
| 373 | ======================= |
| 374 | old< || (0<p-m-M && p-m-M<=W)); |
| 375 | new> || (0<p-m+M && p-m+M<=W)); |
| 376 | |
| 377 | |
| 378 | CHAPTER 11 |
| 379 | |
| 380 | ERROR, page 224, algorithm "analyze()" |
| 381 | ====================================== |
| 382 | old< q = element from W; |
| 383 | new> q = last element from W; |
| 384 | |
| 385 | further down: |
| 386 | ============= |
| 387 | old< If states are stored in set W in first-in first-out order, |
| 388 | the algorithm performs a breadth-first search of the state space tree. |
| 389 | new> If states are stored in set W in first-in last-out (i.e., stack) |
| 390 | order, the algorithm performs a depth-first search of the state space tree. |
| 391 | |
| 392 | further down: |
| 393 | ============= |
| 394 | old< If states are stored in first-in last-out (i.e., stack) |
| 395 | < order, this changes into a depth-first search. |
| 396 | |
| 397 | new> If states are stored and removed in first-in first-out |
| 398 | order, this changes into a breadth-first search |
| 399 | (element q must be deleted upon retrieval from set W in |
| 400 | this type of algorithm). |
| 401 | |
| 402 | Page 227, top |
| 403 | ============= |
| 404 | old< q = element from W; |
| 405 | new> q = last element from W; |
| 406 | |
| 407 | Page 237, bottom |
| 408 | ================ |
| 409 | old< after removing states 4, 3, and 2 from the stack... |
| 410 | new> after removing states 4, and 3 from the stack... |
| 411 | |
| 412 | CHAPTER 13 |
| 413 | |
| 414 | Page 315, 2nd para in 13.9 |
| 415 | ========================== |
| 416 | The first two sentences of this paragraph are incorrect. |
| 417 | At the low end, just 1 state would be stored in the hash-array, |
| 418 | taking up 2 bits of storage out of N available bits; at the |
| 419 | high end, all N bits would be set at the end of the run, and |
| 420 | (allowing overlaps) we cannot have seen more than N states. |
| 421 | This leads to a possible range of values for the hash factor |
| 422 | of N/2 >= hf >= 1 |
| 423 | For full state space storage the hash factor is meaningless. |
| 424 | |
| 425 | CHAPTER 14 |
| 426 | |
| 427 | Page 331, lines 86, 88, and 94 |
| 428 | ============================== |
| 429 | See the corrections described for CHAPTER 7, page 156. |
| 430 | |
| 431 | APPENDIX C |
| 432 | ============================== |
| 433 | |
| 434 | Page 387-388 |
| 435 | The syntax of remote referencing has changed in SPIN Version 2.0. |
| 436 | Remote referencing to local variables is no longer allowed |
| 437 | (page 387, 5th line from below). |
| 438 | The syntax for referencing the state of another process has changed |
| 439 | from (page 388, 3rd line): |
| 440 | same[2]:here |
| 441 | to: |
| 442 | same[2]@here |
| 443 | |
| 444 | /===================================================================\ |
| 445 | | Final Erratum: | |
| 446 | | | |
| 447 | | This book is now replaced with the new, up to date description of | |
| 448 | | the current version of Spin (per 9/2003): | |
| 449 | | http://spinroot.com/spin/Doc/Book_extras/index.html | |
| 450 | \===================================================================/ |
| 451 | |
| 452 | =end errata= |