| 1 | Update History of the SPIN Version 1.0 sources |
| 2 | ============================================== |
| 3 | |
| 4 | ==== Version 1.0 - January 1991 ==== |
| 5 | |
| 6 | The version published in the first printing of |
| 7 | ``Design and Validation of Computer Protocols'' |
| 8 | is nominally SPIN Version 1.0. |
| 9 | The notes below describe all modifications to that |
| 10 | source that were made between January 1991 and |
| 11 | December 1994 (when the distribution switched to |
| 12 | Spin Version 2.0, see V2.Updates). |
| 13 | |
| 14 | ==== Version 1.1 - April 1991 ==== |
| 15 | |
| 16 | 1. (4/6/91) |
| 17 | a queue with a single field of type bool is now mapped onto |
| 18 | an unsigned char to avoid compilers mapping it onto unsigned int. |
| 19 | 2. (4/7/91) |
| 20 | variables are now sorted by type in the statevector (more compact |
| 21 | and thus improves hashing) |
| 22 | 3. (4/7/91) |
| 23 | improved handling of atomic move (removes a statespace-intercept |
| 24 | bug for initial process with id=0) |
| 25 | 4. (5/22/91) |
| 26 | allow multiple labels per statement, without needing skip-fillers |
| 27 | 5. (6/11/91) |
| 28 | fixed bug in reassigning labels in pan.t |
| 29 | 6. (7/30/91) |
| 30 | - added proc_skip[] and q_skip[] arrays to pan sources |
| 31 | the creation of processes and queues was not always |
| 32 | reversible due to word-alignment errors... [caused sv_restor() error] |
| 33 | - removed Have_claim from sched.c; the adjustment of pids was incorrect |
| 34 | - a remote ref to a non-existing pid is now always 0, and does not |
| 35 | cause a dummy global variable to be created by default with -t... |
| 36 | (chages in vars.c and sched.c) |
| 37 | 7. (8/1/91) |
| 38 | - fixed a potentially infinite cycle in walk_sub() |
| 39 | 8. (8/7/91) |
| 40 | - fixed bug: couldn't complete rendez-vous inside atomic sections |
| 41 | 9. (8/22/91) |
| 42 | - lookup(s) failed to check a match on globals when |
| 43 | performing a local lookup of names; caused guided simulations |
| 44 | to report type clashes. |
| 45 | |
| 46 | ==== Version 1.2 - August 1991 ==== |
| 47 | |
| 48 | 1. (9/11/91) |
| 49 | - added traps to check for uninitialized channels in pan.c |
| 50 | - added descriptive statement strings into transition matrix |
| 51 | which are now reported with unreached code etc. |
| 52 | 2. (1/7/92) |
| 53 | - removed bug: no state should be stored in mid-rv. |
| 54 | note that a rv need not complete and matching |
| 55 | on the mid state of an unsuccessful rv may cause |
| 56 | missing errors (a rv may legally not complete in |
| 57 | some cases, without causing deadlock, and not in others). |
| 58 | the change also reduces the number of states stored. |
| 59 | 3. (1/11/92) |
| 60 | - made printout for R different from r in mesg.c |
| 61 | |
| 62 | ==== Version 1.3 - January 1992 ==== [current USL Toolchest version] |
| 63 | |
| 64 | 1. 3/6/92 |
| 65 | - bug fixed in usage of -l with rendez-vous (forgot "if (boq==-1)") pangen1.h |
| 66 | 2. 4/10/92 |
| 67 | - converted to new hstore with sorted linked lists (roughly 10% faster) |
| 68 | 3. 6/3/92 |
| 69 | - remote variables were not promoted to (int) before referral in expressions |
| 70 | updated Errata with some warnings (e.g., about modeling system invariants |
| 71 | in the presence of timeouts, and using the wrong number of parameters in |
| 72 | receives) |
| 73 | - updated makefile with hint for yacc-flags |
| 74 | 4. 6/10/92 |
| 75 | - spin now returns the number of parse errors found upon exit from main |
| 76 | - yyin is now declared extern in main |
| 77 | - srand is now declared void in spin.h |
| 78 | 5. 7/4/92 |
| 79 | - added pan options -d and -d -d to printout the internal state tables |
| 80 | pan will no longer report structurally unreachable states as |
| 81 | dynamically unreachable |
| 82 | - added warning when spec is modified since pan.trail written |
| 83 | - solved a trail problem when user guess pids which are offset by claim |
| 84 | - print proper process numbers for spin -t when a claim is running |
| 85 | - fixed error in lookup of _p values (it's a local var not global) |
| 86 | - improved claim checking with geoffrey browns claim stuttering semantics |
| 87 | |
| 88 | ==== Version 1.4 - July 1992 ==== |
| 89 | |
| 90 | 1. 7/8/92 |
| 91 | - replaced emalloc with a dedicated emalloc/malloc/free package; this |
| 92 | is six times faster on pftp.ses1 example compared to sysV library malloc |
| 93 | 2. 7/12/92 |
| 94 | - added default array bounds checking (except for remote references) |
| 95 | makes validations a little slower (say 5% - 10%), but is safer, and |
| 96 | the user can override it by compiling: cc -DNOBOUNDCHECK pan.c |
| 97 | 3. 8/26/92 |
| 98 | - improved the acceptance cycle detection method with a new algorithm |
| 99 | due to Patrice Godefroid, that works in both bitstate and exhaustive |
| 100 | search mode (the old version worked only in exhaustive mode) |
| 101 | time and space complexity of the new algorithm is the same as that for |
| 102 | non-progress cycle detection algorithm (at worst twice that of a straight search) |
| 103 | the method is functionally the same as the earlier method due to Courcoubetis, |
| 104 | Vardi, Wolper, and Yannakakis (CAV'90), but uses the 2-bit demon trick from |
| 105 | the non-progress cycle detector to distinguish between 1st and 2nd search. |
| 106 | - fixed a buglet in lex.l that catenated strings printed on a single line |
| 107 | (thanks Alan Wenban for catching it) |
| 108 | 4. 12/11/92 |
| 109 | - intermediate states in atomic sequences were not stored in standard search |
| 110 | mode, but stored when a never claim was defined - that was unnecessary, and |
| 111 | has now been avoided. behavior doesn't change, but memory consumption in |
| 112 | exhaustive mode is now reduced somewhat. |
| 113 | - the acceptance cycle detection algorithm would initiate its second search |
| 114 | from an accepting state within a never claim, even when the system was |
| 115 | inside an atomic sequence - it could therefore produce non-existing cycles. |
| 116 | has been fixed (both fixes thanks to Patrice Godefroid and Didier Pirrotin) |
| 117 | |
| 118 | ==== Version 1.5 - January 1993 ==== |
| 119 | |
| 120 | 1.5.0 |
| 121 | - an option -V was added both to spin itself and to the analyzers |
| 122 | generated by spin to print the source version number. |
| 123 | - a compiler directive VERBOSE was added to the generated analyzers |
| 124 | to assist the user in understanding how the depth-first searches |
| 125 | are performed. to invoke the extra printouts compile |
| 126 | the source as cc -DVERBOSE pan.c (plus any other directives you may |
| 127 | be using, such as -DBITSTATE or -DMEMCNT=23) |
| 128 | - a small bug-fix was added to avoid a misplaced compiler directive |
| 129 | (in BITSTATE mode, in the absence of accept labels in the model, there |
| 130 | could be a compiler error that is now avoided) |
| 131 | - somewhat improved error reporting. |
| 132 | - several more important runtime options for the generated analyzers |
| 133 | were added: |
| 134 | 1 an explicit runtime option -a to invoke the search for |
| 135 | acceptance cycles. until now this used to happen by default |
| 136 | unless you specified an explicit -l option for a search for |
| 137 | non-progress cycles. from now on a search for cycles |
| 138 | always has to be specified explicitly as either -a or -l. |
| 139 | 2 a runtime option -f to modify the search for cycles under |
| 140 | `weak fairness.' it works for both -a (acceptance cycles) |
| 141 | and for -l (non-progress cycles), and is independent of the |
| 142 | search mode (full state storage or bitstate hashing) |
| 143 | using -f may increase the time-complexity of a search, but |
| 144 | it does not alter the space requirements |
| 145 | - specifying -f without either -a or -l would have no effect, so it |
| 146 | is considered an error. |
| 147 | - you cannot combine options -a and -l |
| 148 | - you can always combine -a with a never claim, but |
| 149 | - you cannot combine -l with a never claim. |
| 150 | - a harmless glitch in the setting of tau values for atomic moves |
| 151 | was fixed - it should not alter the behavior of the analyzers |
| 152 | - another small fix in the reporting of unreachable code (previous versions |
| 153 | of spin could forget to report some of the states) |
| 154 | - remember: to search for acceptance cycles, you always must |
| 155 | specify option -a now (or -f -a if restricted to fair cycles) |
| 156 | |
| 157 | = |
| 158 | 1.5.1 - 2/23/93 |
| 159 | - the acceptance cycle detector now starts the search for an acceptance |
| 160 | cycle after any move, whether in the claim or in the system |
| 161 | (until now, it only did so after a system move - which did not cover |
| 162 | all cases correctly, specifically for cases that are covered by the |
| 163 | claim stutter semantics, and for cases where acceptance cycles are only |
| 164 | defined inside the claim, and not in the system) |
| 165 | 1.5.2 - 3/1/93 |
| 166 | - the change from 1.5.1 was incorrect - a search from acceptence cycles |
| 167 | starts after system moves, or after stutter-claim moves, but not |
| 168 | for other claim moves (a stutter claim move is used to cycle the claim |
| 169 | in valid and invalid endstates - it triggers an error report if the claim |
| 170 | can cycle through an accept state in this case - it should not trigger |
| 171 | error reports in any other case) |
| 172 | 1.5.3 - 3/19/93 |
| 173 | - spin now catches SIGPIPE signals, and exits when it sees one. |
| 174 | added an option -X to use stdout instead of stderr for all error messages |
| 175 | (these upgrades are in preparation for an X-interface to spin) |
| 176 | 1.5.4 - 4/15/93 |
| 177 | - in simulation mode spin didn't always flag it as an error if an array-name |
| 178 | was used as a formal parameter in a proctype declaration (spin -a always |
| 179 | reports it correctly) - the error report is now given |
| 180 | - added Xspin to the distribution as bundle4 - an X-interface to spin based |
| 181 | on the (public domain) toolkit Tcl/Tk from the university of berkeley. |
| 182 | 1.5.5 - 4/21/93 |
| 183 | - fixed an error in fair_cycle(); the original algorithm omitted to set |
| 184 | the correct value in a pointer to the current process during the fairness |
| 185 | checks - the result was that fairness calls were not always accurate. |
| 186 | - some small improvements in the Xspin interface (call it XSPIN version 1.0.1) |
| 187 | - improvement in sched.c - to match the assignemnts of pids to those of the validator |
| 188 | 1.5.6 - 5/21/93 |
| 189 | - another error in fair_cycle; code inserted for the detection of self-loops |
| 190 | was incorrect; it has been omitted. |
| 191 | non-fair cycles that can become fair *only* by the inclusion of a dummy |
| 192 | "do :: skip od" |
| 193 | loop in one of the processes may be missed in a verification using the -f flag. |
| 194 | since such busy-looping constructs are not (or should not be) used in Promela |
| 195 | anyway, this should not create problems |
| 196 | - changed the data-types used in the hash-functions - to secure portability |
| 197 | of SPIN to 64 bit machines. |
| 198 | 1.5.7 - 7/1/93 |
| 199 | - fixed a subtle error that happens when a remote variable is used deeply nested inside |
| 200 | the index of another remote variable (array) |
| 201 | - also fixed a spurious error report on array bound checking in such cases |
| 202 | - both cases should be rare enough that it didn't bite anyone - they affected only |
| 203 | simulation mode |
| 204 | 1.5.8 - 10/1/93 |
| 205 | - made it an error to place a label at the first statement of a sub-sequence. |
| 206 | spin's optimization strategy (to speed up searches) can defeat such an |
| 207 | unconventional label placement easily, which can cause problems in remote references. |
| 208 | the rule is (and has actually always been) that constructs such as |
| 209 | do if atomic { |
| 210 | :: L: a = 1 :: L: a = 1 L: a = 1 |
| 211 | od fi } |
| 212 | should be written as: |
| 213 | L: do L: if L: atomic { |
| 214 | :: a = 1 :: a = 1 a = 1 |
| 215 | od fi } |
| 216 | the rule is now enforced. to make it easier, the above message is printed if the |
| 217 | label is accidentily misplaced, in the heat of design... |
| 218 | note that the first state of a subsequence equals the state of the enclosing |
| 219 | construct (e.g., the start state of each option in a do-structure is the very |
| 220 | same state as the start state of the do-structure itself) |
| 221 | 1.5.9 - 11/17/93 |
| 222 | A small error in the management of rendez-vous status during the search had |
| 223 | slipped in on 9/11/91. finally caught and removed. |
| 224 | 1.5.10 - 11/19/93 |
| 225 | -spin attempts to optimize goto and break statements by removing them from |
| 226 | the transition matrix wherever possible. this has no visible effect, other |
| 227 | then achieving an extra speedup of the validation. |
| 228 | in a small number of cases, though, the labels must be preserved |
| 229 | one such case is when a goto or break carries a progress, end, or accept label. |
| 230 | in that case the jump is preserved (that case was always treated correctly). |
| 231 | another case, that was overlooked so far, is when the label in front of a goto |
| 232 | is used in a remote reference, such as P[pid]:label. the use is dubious, but |
| 233 | cannot be excluded. in 1.5.10 this case has been added to the exceptions - where |
| 234 | the gotos are not removed from the matrix. |
| 235 | -also fixed: the never claim no longer steps in the middle of a rendez-vous handshake |
| 236 | (it was correctly observed by a user that it shoudln't - since its really atomic) |
| 237 | -also fixed: the initial state of a newly started process in the simulator |
| 238 | now always matches that of the validator (same optimization steps are done) |
| 239 | the avoids some cases of lost trails in guided simulations |
| 240 | 1.5.11 - 2/1/94 |
| 241 | -the fix from 1.5.10 works by inserting a dummy skip statement in between |
| 242 | a label and the statement that follows it (a goto in this case) |
| 243 | that calls for an extra statement, with a unique state number |
| 244 | the extra state numbers weren't counted in the allocation of memory for the |
| 245 | transition matrix - which could cause some peculiar behavior in the (luckily) |
| 246 | few cases where this improvement kicked in. it's fixed in this release. |
| 247 | -another improvement, that had been waiting in the wings for a chance to make it |
| 248 | into the released version - is that the timeout variable is now testable inside |
| 249 | never claims (that wasn't true before). |
| 250 | 1.5.12 - 1/20/94 |
| 251 | -added a random number generator - compliments of Thierry Cattel. |
| 252 | as an alternative to the badly performing standard routines provided |
| 253 | on most systems. should improve simulations - affects nothing else. |
| 254 | 1.5.13 - 3/27/94 |
| 255 | -small improvement in handling of syntax errors in parser. |
| 256 | -added clarifications to the file `roadmap' in bundle3 |
| 257 | -added manual.ps to the distribution |
| 258 | 1.5.14 - 4/22/94 |
| 259 | -until now you had to turn on message loss (-m) explicitly when following |
| 260 | a backtrace (using spin -t) from a system that was generated with message |
| 261 | loss enabled (i.e., with spin -a -m). that is easy to forget. spin -t no |
| 262 | longer explicitly requires the -m flag in these cases, to avoid confusion. |
| 263 | it is still valid to use -m in combination with -t, but not required. |
| 264 | 1.5.15 - 5/20/94 |
| 265 | -removed small bug from sched.c (the simulator) that could prevent a process |
| 266 | from being deleted correctly from the run queue when the last two processes die. |
| 267 | 1.5.16 - 6/3/94 |
| 268 | -if a goto jump inside an atomic sequence jumped to the last statement of the |
| 269 | sequence, spin would get confused and mark that jump as non-atomic |
| 270 | version 1.5.16 handles this case correctly |
| 271 | -added an error production to the grammar - to improve syntax error reporting |
| 272 | 1.5.17 - 7/15/94 |
| 273 | -a remote reference to a non-existing variable could result in a core-dump |
| 274 | during guided simulations; fixed in this version. |
| 275 | 1.5.18 - 8/1/94 |
| 276 | -during simulation a remote reference to a previously unused local variable |
| 277 | from another process would return the default 0 value - instead of the initial |
| 278 | value of such a variable. this caused the behavior of validator and simulator |
| 279 | to differ in such cases (in the validator all variables are always created and |
| 280 | initialized upon process creation - in the simulator variables are created and |
| 281 | initialized in a `lazy' fashion: upon the first reference. |
| 282 | this is now fixed so that the simulator's behavior is now no different from |
| 283 | the validator: refering to a previously unused variable of a running process |
| 284 | returns its initial value - as it should. |
| 285 | |
| 286 | ==== Version 1.6 - August 1994 ==== |
| 287 | |
| 288 | 1.6.0 - 8/5/94 |
| 289 | -Important improvement - Please Read! |
| 290 | -it was always a problem to get ``mtype'' names used inside messages to |
| 291 | be distinguished properly from other integers in (guided) simulations. |
| 292 | the rule used so far was that if a message field held a ``constant'' |
| 293 | it was interpreted and printed as an mtype name, and else as a value. |
| 294 | |
| 295 | starting with version 1.6 this is handled better as follows: |
| 296 | if you declare a message field to have type ``mtype'' it is ALWAYS printed |
| 297 | as a symbolic name, never as a value. |
| 298 | for example, you can now declare a channel as: |
| 299 | chan sender = [12] of { mtype, byte, short, chan, mtype }; |
| 300 | so that the first and last field are always printed symbolically as a name, |
| 301 | never as a value. only bits, bytes, shorts, and ints, are now printed |
| 302 | as values. |
| 303 | make good note of the change: you will almost always want to use mtype |
| 304 | declarations for at least some of the fields in any channel declaration. |
| 305 | the new functionality greatly increases the clarity of tracebacks with spin -t |
| 306 | |
| 307 | -new compile time option cc -DPEG pan.c - to force the runtime analyzer to |
| 308 | gather statistics about how often each transition (the bracketed number in |
| 309 | the pan -d output) is executed. |
| 310 | |
| 311 | 1.6.1 - 8/16/94 |
| 312 | -added a declaration of procedure putpeg, to avoid a compiler warning |
| 313 | -made sure that booleans such as q?[msg] can be used in any combination |
| 314 | in assert statements (until now spin could insert newlines that spoiled |
| 315 | printfs on debugging output) |
| 316 | |
| 317 | 1.6.2 - 8/20/94 |
| 318 | -tightened the parser to reject expressions inside receive statements. |
| 319 | so far these were silently accepted (incorrectly) - and badly translated |
| 320 | into pan.[mb] files. the fields in a receive statement can legally only |
| 321 | contain variable-names or constants (mtypes). variables are set, and |
| 322 | constant fields are matched in the receive. |
| 323 | -cleaned up the enforcement of the MEMCNT parameter (the compile time parameter |
| 324 | that is used to set a physical memory limit at 2**MEMCNT bytes) |
| 325 | we now check *before* allocating a new chunk of memory whether this will |
| 326 | exceed the limit - instead of *after* having done so - as was the case so far. |
| 327 | gives a better report on which memory request caused memory to run out. |
| 328 | |
| 329 | 1.6.3 - 8/27/94 |
| 330 | -the simulator failed to recognize remote label references properly. |
| 331 | has been fixed in sched.c. |
| 332 | -the validator failed to report blocking statements inside atomic sequences |
| 333 | when a never claim was present - it defaulted to claim stutter instead. |
| 334 | it now correctly reports the error. |
| 335 | |
| 336 | 1.6.4 - 9/18/94 |
| 337 | -in rare cases, an accept cycle could be missed if it can only be closed |
| 338 | by multiple claim stutter moves through a sequence of distinct claim states |
| 339 | this now works as it should. |
| 340 | -added some helpful printfs that are included when the -DVERBOSE and -DDEBUG |
| 341 | compile time flags are used on pan.c's |
| 342 | |
| 343 | 1.6.5 - 10/19/94 |
| 344 | -the mtype field of message queues wasn't interpreted correctly in |
| 345 | in the printout of verbose simulation runs (the field was printed |
| 346 | numerically instead of symbolically). |
| 347 | |
| 348 | 1.6.6 - 11/15/94 |
| 349 | minor fix in procedure call of new_state - to avoid compiler complaints |
| 350 | about use of an ANSI-isms in an otherwise pre-ANSI-C source. |
| 351 | (version 2.0 - see below) is completely ANSI/POSIX standard and will not |
| 352 | compile with pre-ANSI compilers. version 1.6.6 is the last |
| 353 | version of SPIN that does not make this requirement. |
| 354 | |
| 355 | 12/24/94 |
| 356 | Version 1.6.6 is the last update of Spin Version 1. |
| 357 | The distribution will switch to Spin Version 2.0, and |
| 358 | all further updates will be documented in: Doc/V2.Updates. |