verif/Spin/Doc/Book91_Errata.txt

   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=