0b55f123 |
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. |