+++ /dev/null
-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.
projects / lttv.git / blobdiff