convert from svn repository: remove tags directory

[lttv.git] / trunk / verif / Spin / Doc / V1.Updates

Update History of the SPIN Version 1.0 sources
==============================================

==== Version 1.0 - January 1991 ====

The version published in the first printing of
``Design and Validation of Computer Protocols''
is nominally SPIN Version 1.0.
The notes below describe all modifications to that
source that were made between January 1991 and
December 1994 (when the distribution switched to
Spin Version 2.0, see V2.Updates).

==== Version 1.1 - April 1991 ====

1. (4/6/91)
a queue with a single field of type bool is now mapped onto
an unsigned char to avoid compilers mapping it onto unsigned int.
2. (4/7/91)
variables are now sorted by type in the statevector (more compact
and thus improves hashing)
3. (4/7/91)
improved handling of atomic move (removes a statespace-intercept
bug for initial process with id=0)
4. (5/22/91)
allow multiple labels per statement, without needing skip-fillers
5. (6/11/91)
fixed bug in reassigning labels in pan.t 
6. (7/30/91)
- added proc_skip[] and q_skip[] arrays to pan sources
  the creation of processes and queues was not always
  reversible due to word-alignment errors... [caused sv_restor() error]
- removed Have_claim from sched.c; the adjustment of pids was incorrect
- a remote ref to a non-existing pid is now always 0, and does not
  cause a dummy global variable to be created by default with -t...
  (chages in vars.c and sched.c)
7. (8/1/91)
- fixed a potentially infinite cycle in walk_sub()
8. (8/7/91)
- fixed bug: couldn't complete rendez-vous inside atomic sections
9. (8/22/91)
- lookup(s) failed to check a match on globals when
  performing a local lookup of names; caused guided simulations
  to report type clashes.

==== Version 1.2 - August 1991 ====

1. (9/11/91)
- added traps to check for uninitialized channels in pan.c
- added descriptive statement strings into transition matrix
  which are now reported with unreached code etc.
2. (1/7/92)
- removed bug: no state should be stored in mid-rv.
  note that a rv need not complete and matching
  on the mid state of an unsuccessful rv may cause
  missing errors (a rv may legally not complete in
  some cases, without causing deadlock, and not in others).
  the change also reduces the number of states stored.
3. (1/11/92)
- made printout for R different from r in mesg.c

==== Version 1.3 - January 1992 ==== [current USL Toolchest version]

1. 3/6/92
- bug fixed in usage of -l with rendez-vous (forgot "if (boq==-1)") pangen1.h
2. 4/10/92
- converted to new hstore with sorted linked lists (roughly 10% faster)
3. 6/3/92
- remote variables were not promoted to (int) before referral in expressions
  updated Errata with some warnings (e.g., about modeling system invariants
  in the presence of timeouts, and using the wrong number of parameters in
  receives)
- updated makefile with hint for yacc-flags
4. 6/10/92
- spin now returns the number of parse errors found upon exit from main
- yyin is now declared extern in main
- srand is now declared void in spin.h
5. 7/4/92
- added pan options -d and -d -d to printout the internal state tables
  pan will no longer report structurally unreachable states as
  dynamically unreachable
- added warning when spec is modified since pan.trail written
- solved a trail problem when user guess pids which are offset by claim
- print proper process numbers for spin -t when a claim is running
- fixed error in lookup of _p values (it's a local var not global)
- improved claim checking with geoffrey browns claim stuttering semantics

==== Version 1.4 - July 1992 ====

1. 7/8/92
- replaced emalloc with a dedicated emalloc/malloc/free package; this
  is six times faster on pftp.ses1 example compared to sysV library malloc
2. 7/12/92
- added default array bounds checking (except for remote references)
  makes validations a little slower (say 5% - 10%), but is safer, and
  the user can override it by compiling: cc -DNOBOUNDCHECK pan.c
3. 8/26/92
- improved the acceptance cycle detection method with a new algorithm
  due to Patrice Godefroid, that works in both bitstate and exhaustive
  search mode (the old version worked only in exhaustive mode)
  time and space complexity of the new algorithm is the same as that for
  non-progress cycle detection algorithm (at worst twice that of a straight search)
  the method is functionally the same as the earlier method due to Courcoubetis,
  Vardi, Wolper, and Yannakakis (CAV'90), but uses the 2-bit demon trick from
  the non-progress cycle detector to distinguish between 1st and 2nd search.
- fixed a buglet in lex.l that catenated strings printed on a single line
  (thanks Alan Wenban for catching it)
4. 12/11/92
- intermediate states in atomic sequences were not stored in standard search
  mode, but stored when a never claim was defined - that was unnecessary, and
  has now been avoided.  behavior doesn't change, but memory consumption in
  exhaustive mode is now reduced somewhat.
- the acceptance cycle detection algorithm would initiate its second search
  from an accepting state within a never claim, even when the system was
  inside an atomic sequence - it could therefore produce non-existing cycles.
  has been fixed (both fixes thanks to Patrice Godefroid and Didier Pirrotin)

==== Version 1.5 - January 1993 ====

1.5.0
- an option -V was added both to spin itself and to the analyzers
  generated by spin to print the source version number.
- a compiler directive VERBOSE was added to the generated analyzers
  to assist the user in understanding how the depth-first searches
  are performed.  to invoke the extra printouts compile
  the source as cc -DVERBOSE pan.c (plus any other directives you may
  be using, such as -DBITSTATE or -DMEMCNT=23)
- a small bug-fix was added to avoid a misplaced compiler directive
  (in BITSTATE mode, in the absence of accept labels in the model, there
  could be a compiler error that is now avoided)
- somewhat improved error reporting.
- several more important runtime options for the generated analyzers
  were added:
  1     an explicit runtime option -a to invoke the search for
        acceptance cycles.  until now this used to happen by default
        unless you specified an explicit -l option for a search for
        non-progress cycles.  from now on a search for cycles
        always has to be specified explicitly as either -a or -l.
  2     a runtime option -f to modify the search for cycles under
        `weak fairness.'   it works for both -a (acceptance cycles)
        and for -l (non-progress cycles), and is independent of the
        search mode (full state storage or bitstate hashing)
        using -f may increase the time-complexity of a search, but
        it does not alter the space requirements
- specifying -f without either -a or -l would have no effect, so it
  is considered an error.
- you cannot combine options -a and -l
- you can always combine -a with a never claim, but
- you cannot combine -l with a never claim.
- a harmless glitch in the setting of tau values for atomic moves
  was fixed - it should not alter the behavior of the analyzers
- another small fix in the reporting of unreachable code (previous versions
  of spin could forget to report some of the states)
- remember: to search for acceptance cycles, you always must
  specify option -a now (or -f -a if restricted to fair cycles)

=
1.5.1 - 2/23/93
- the acceptance cycle detector now starts the search for an acceptance
  cycle after any move, whether in the claim or in the system
  (until now, it only did so after a system move - which did not cover
   all cases correctly, specifically for cases that are covered by the
   claim stutter semantics, and for cases where acceptance cycles are only
   defined inside the claim, and not in the system)
1.5.2 - 3/1/93
- the change from 1.5.1 was incorrect - a search from acceptence cycles
  starts after system moves, or after stutter-claim moves, but not
  for other claim moves (a stutter claim move is used to cycle the claim
  in valid and invalid endstates - it triggers an error report if the claim
  can cycle through an accept state in this case - it should not trigger
  error reports in any other case)
1.5.3 - 3/19/93
- spin now catches SIGPIPE signals, and exits when it sees one.
  added an option -X to use stdout instead of stderr for all error messages
  (these upgrades are in preparation for an X-interface to spin)
1.5.4 - 4/15/93
- in simulation mode spin didn't always flag it as an error if an array-name
  was used as a formal parameter in a proctype declaration (spin -a always
  reports it correctly) - the error report is now given
- added Xspin to the distribution as bundle4 - an X-interface to spin based
  on the (public domain) toolkit Tcl/Tk from the university of berkeley.
1.5.5 - 4/21/93
- fixed an error in fair_cycle(); the original algorithm omitted to set
  the correct value in a pointer to the current process during the fairness
  checks - the result was that fairness calls were not always accurate.
- some small improvements in the Xspin interface (call it XSPIN version 1.0.1)
- improvement in sched.c - to match the assignemnts of pids to those of the validator
1.5.6 - 5/21/93
- another error in fair_cycle; code inserted for the detection of self-loops
  was incorrect; it has been omitted.
  non-fair cycles that can become fair *only* by the inclusion of a dummy
        "do :: skip od"
  loop in one of the processes may be missed in a verification using the -f flag.
  since such busy-looping constructs are not (or should not be) used in Promela
  anyway, this should not create problems
- changed the data-types used in the hash-functions - to secure portability
  of SPIN to 64 bit machines.
1.5.7 - 7/1/93
- fixed a subtle error that happens when a remote variable is used deeply nested inside
  the index of another remote variable (array)
- also fixed a spurious error report on array bound checking in such cases
- both cases should be rare enough that it didn't bite anyone - they affected only
  simulation mode
1.5.8 - 10/1/93
- made it an error to place a label at the first statement of a sub-sequence.
  spin's optimization strategy (to speed up searches) can defeat such an
  unconventional label placement easily, which can cause problems in remote references.
  the rule is (and has actually always been) that constructs such as
        do              if              atomic {
        :: L: a = 1     :: L: a = 1             L: a = 1
        od              fi              }
  should be written as:
        L: do           L: if           L: atomic {
           :: a = 1        :: a = 1             a = 1
           od              fi              }
  the rule is now enforced.  to make it easier, the above message is printed if the
  label is accidentily misplaced, in the heat of design...
  note that the first state of a subsequence equals the state of the enclosing
  construct (e.g., the start state of each option in a do-structure is the very
  same state as the start state of the do-structure itself)
1.5.9 - 11/17/93
 A small error in the management of rendez-vous status during the search had
 slipped in on 9/11/91.  finally caught and removed.
1.5.10 - 11/19/93
-spin attempts to optimize goto and break statements by removing them from
 the transition matrix wherever possible.  this has no visible effect, other
 then achieving an extra speedup of the validation.
 in a small number of cases, though, the labels must be preserved
 one such case is when a goto or break carries a progress, end, or accept label.
 in that case the jump is preserved (that case was always treated correctly).
 another case, that was overlooked so far, is when the label in front of a goto
 is used in a remote reference, such as P[pid]:label.  the use is dubious, but
 cannot be excluded. in 1.5.10 this case has been added to the exceptions - where
 the gotos are not removed from the matrix.
-also fixed: the never claim no longer steps in the middle of a rendez-vous handshake
 (it was correctly observed by a user that it shoudln't - since its really atomic)
-also fixed: the initial state of a newly started process in the simulator
 now always matches that of the validator (same optimization steps are done)
 the avoids some cases of lost trails in guided simulations
1.5.11 - 2/1/94
-the fix from 1.5.10 works by inserting a dummy skip statement in between
 a label and the statement that follows it (a goto in this case)
 that calls for an extra statement, with a unique state number
 the extra state numbers weren't counted in the allocation of memory for the
 transition matrix - which could cause some peculiar behavior in the (luckily)
 few cases where this improvement kicked in.  it's fixed in this release.
-another improvement, that had been waiting in the wings for a chance to make it
 into the released version - is that the timeout variable is now testable inside
 never claims (that wasn't true before).
1.5.12 - 1/20/94
-added a random number generator - compliments of Thierry Cattel.
 as an alternative to the badly performing standard routines provided 
 on most systems.  should improve simulations - affects nothing else.
1.5.13 - 3/27/94
-small improvement in handling of syntax errors in parser.
-added clarifications to the file `roadmap' in bundle3
-added manual.ps to the distribution
1.5.14 - 4/22/94
-until now you had to turn on message loss (-m) explicitly when following
 a backtrace (using spin -t) from a system that was generated with message
 loss enabled (i.e., with spin -a -m).  that is easy to forget.  spin -t no
 longer explicitly requires the -m flag in these cases, to avoid confusion.
 it is still valid to use -m in combination with -t, but not required.
1.5.15 - 5/20/94
-removed small bug from sched.c (the simulator) that could prevent a process
 from being deleted correctly from the run queue when the last two processes die.
1.5.16 - 6/3/94
-if a goto jump inside an atomic sequence jumped to the last statement of the
 sequence, spin would get confused and mark that jump as non-atomic
 version 1.5.16 handles this case correctly
-added an error production to the grammar - to improve syntax error reporting
1.5.17 - 7/15/94
-a remote reference to a non-existing variable could result in a core-dump
 during guided simulations;  fixed in this version.
1.5.18 - 8/1/94
-during simulation a remote reference to a previously unused local variable
 from another process would return the default 0 value - instead of the initial
 value of such a variable.  this caused the behavior of validator and simulator
 to differ in such cases (in the validator all variables are always created and
 initialized upon process creation - in the simulator variables are created and
 initialized in a `lazy' fashion: upon the first reference.
 this is now fixed so that the simulator's behavior is now no different from
 the validator: refering to a previously unused variable of a running process
 returns its initial value - as it should.

==== Version 1.6 - August 1994 ====

1.6.0 - 8/5/94
-Important improvement - Please Read!
-it was always a problem to get ``mtype'' names used inside messages to
 be distinguished properly from other integers in (guided) simulations.
 the rule used so far was that if a message field held a ``constant''
 it was interpreted and printed as an mtype name, and else as a value.

 starting with version 1.6 this is handled better as follows:
 if you declare a message field to have type ``mtype'' it is ALWAYS printed
 as a symbolic name, never as a value. 
 for example, you can now declare a channel as:
        chan sender = [12] of { mtype, byte, short, chan, mtype };
 so that the first and last field are always printed symbolically as a name,
 never as a value.  only bits, bytes, shorts, and ints, are now printed
 as values.
 make good note of the change:  you will almost always want to use mtype
 declarations for at least some of the fields in any channel declaration.
 the new functionality greatly increases the clarity of tracebacks with spin -t

-new compile time option cc -DPEG pan.c - to force the runtime analyzer to
 gather statistics about how often each transition (the bracketed number in
 the pan -d output) is executed.

1.6.1 - 8/16/94
-added a declaration of procedure putpeg, to avoid a compiler warning
-made sure that booleans such as q?[msg] can be used in any combination
 in assert statements (until now spin could insert newlines that spoiled
 printfs on debugging output)

1.6.2 - 8/20/94
-tightened the parser to reject expressions inside receive statements.
 so far these were silently accepted (incorrectly) - and badly translated
 into pan.[mb] files.  the fields in a receive statement can legally only
 contain variable-names or constants (mtypes).  variables are set, and
 constant fields are matched in the receive.
-cleaned up the enforcement of the MEMCNT parameter (the compile time parameter
 that is used to set a physical memory limit at 2**MEMCNT bytes)
 we now check *before* allocating a new chunk of memory whether this will
 exceed the limit - instead of *after* having done so - as was the case so far.
 gives a better report on which memory request caused memory to run out.

1.6.3 - 8/27/94
-the simulator failed to recognize remote label references properly.
 has been fixed in sched.c.
-the validator failed to report blocking statements inside atomic sequences
 when a never claim was present - it defaulted to claim stutter instead.
 it now correctly reports the error.

1.6.4 - 9/18/94
-in rare cases, an accept cycle could be missed if it can only be closed
 by multiple claim stutter moves through a sequence of distinct claim states
 this now works as it should.
-added some helpful printfs that are included when the -DVERBOSE and -DDEBUG
 compile time flags are used on pan.c's

1.6.5 - 10/19/94
-the mtype field of message queues wasn't interpreted correctly in
 in the printout of verbose simulation runs (the field was printed
 numerically instead of symbolically).

1.6.6 - 11/15/94
 minor fix in procedure call of new_state - to avoid compiler complaints
 about use of an ANSI-isms in an otherwise pre-ANSI-C source.
 (version 2.0 - see below) is completely ANSI/POSIX standard and will not
 compile with pre-ANSI compilers.  version 1.6.6 is the last
 version of SPIN that does not make this requirement.

12/24/94
 Version 1.6.6 is the last update of Spin Version 1.
 The distribution will switch to Spin Version 2.0, and
 all further updates will be documented in: Doc/V2.Updates.