1 Distribution Update History of the SPIN sources
2 ===============================================
4 ==== Version 5.0 - 26 October 2007 ====
6 The update history since 1989:
8 Version 0: Jan. 1989 - Jan. 1990 5.6K lines: original book version
9 Version 1: Jan. 1990 - Jan. 1995 7.9K lines: first version on netlib
10 Version 2: Jan. 1995 - Aug. 1997 6.1K lines: partial-order reduction
11 Version 3: Aug. 1997 - Jan. 2003 17.9K lines: bdd-like compression (MA)
12 Version 4: Jan. 2003 - Oct. 2007 28.2K lines: embedded c-code, bfs
13 Version 5: Oct. 2007 - 32.8K lines: multi-core support
15 See the end of the V4.Updates file for the main changes
16 between the last Spin version 4.3.0 and Spin version 5.0.
18 For more details on the use of the new options in 5.0, see also:
19 http://www.spinroot.com/spin/multicore/V5_Readme.html
21 http://www.spinroot.com/spin/multicore/index.html
22 which has additional details on the IEEE TSE paper on Spin V5.0.
24 ==== Version 5.1 - 3 November 2007 ====
26 - fixed an endless loop in the parser for complex atomic sequences
27 (thanks to Mirek Filipow for the example)
28 - noticed poor scaling for shared memory system with more than 8 cpus
29 in large rings the downstream cpus can fail to receive sufficient work
30 for some applications, which leads to poor performance.
31 modified the algorithm by adding a global queue that allows
32 cpus to also share some states independent of the ring structure.
33 (and modified the termination algorithm slightly to accomodate this)
34 this improves overall behavior, allows for deeper handoff depths, and
35 restores the scaling on mega-multicore systems
36 linear scalling sometimes stops past roughly 8 cpu's, but some speedup
37 was measured with the new algorithm up to 36 cpu-nodes
38 - disabling the global queue is possible but not recommended
39 - other smaller fixes, e.g. in issueing recompilation hints etc.
41 ==== Version 5.1.1 - 11 November 2007 ====
43 - added a new directive -DSFH for fast safety verification
44 this uses a little more memory, but can give a significant speedup
45 it uses Hsieh's fast hash function, which isn't as good as Jenkins,
46 but can be faster, especially when compiling -O2 or -O3.
47 this option does not work in 64-bit mode (yet).
48 the speedup for safety properties the speedup can be up to 2x.
49 - some more code cleanup -- more uses of #error and #warning to
50 give faster feedback on unsupported combinations of directives
51 - reduced verbosity of outputs in multi-core mode somewhat
52 - moved queue access pointers (free and full) into shared memory
53 to give more flexibility in defining handoff strategies
54 (i.e., all cores can now access all queues in principle)
55 added experimental handoff strategies -DPSTAT (with or without -DRROBIN)
56 another experimental handoff strategy is -DFRUGAL (when not using -DPSTAT)
57 [removed in 5.1.2 -- after more experiments showing limited benefit]
58 - changed handoff heuristic for bitstate mode, to no longer drop
59 states silently if the target q is full, but instead to explore
60 such states locally -- this increases maxdepth requirements, but
61 is more faithful to the way non-bitstate searches work, and gives
62 better coverage overall
63 - changed the way that the global queue is used for multi-core search
64 (the global queue was introduced in 5.1.0 to support scaling to larger
65 number of cores) it is now the second choice, not the first, for a
66 handoff -- the first choice is the normal handoff strategy (normally
67 a handoff to the right neighbor in the logical ring of cores)
68 - removed the obsolete directive -DCOVEST
70 ==== Version 5.1.2 - 22 November 2007 ====
72 - added an automatic resize option for the hashtable in non-bitstate mode
73 this is generally more efficient, although it will still remain faster to
74 choose the right -w parameter up front.
75 this option increases memory use somewhat (the hash now has to be stored
76 in the hashtable together with each state -- which adds about 4 bytes to
77 each state) the automatic resizing feature can be disabled with -DNO_RESIZE
78 (e.g., to reduce memory). not enabled in multi-core mode.
79 - replaced the global heap in multicore mode with separate heaps for each
80 process (still using shared memory of course) -- this reduces the
81 amount of locking needed (suggested by Petr Rockai -- comparable to using hoard)
82 - rewrote the compress function with some loop unwinding to try to speed
83 it up a bit (but no major improvement noticed)
84 - increased the number of critical sections used for hashtable access in
85 multi-core mode 8x. this improves scaling for some problems
86 (e.g., for elevator2.3 from the BEEM database).
87 - made it in principle possible to use more than 2 cores for liveness
88 verification, although more work would be needed to turn this into
89 a method that can speedup the verification of liveness properties further
90 - reduced SFH to non-bitstate mode (it is slower than Jenkins if used for
91 double-bit hash computations)
92 - changed the format of printfs a little to line up numbers better in output.
93 also improved the accuracy of the resource usage numbers reported
95 - removed the experimentsl directives PSTAT, RROBIN, and FRUGAL from 5.1.1
96 - also removed another stale directive R_H
97 - updated the 64-bit version of Jenkins hash with the latest version
98 posted on his website (already a few years ago it seems).
99 no big difference in performance or accuracy could be noted though.
100 - made liveness verification work with a global queue
101 - changed the details of the state handoff mechanism, to rely more on
102 the global queue, to improve scaling behavior on larger numbers of cores
103 - reduced the sizes of the handoff queues to the handoff-depth leaving
104 only the global queue at a fixed 128 MB -- in measurements this was a win
105 - improved code for setting default values for MEMLIM
106 - increased the value of VMAX to match that of the full VECTORSZ, so that
107 redefining it will be less frequently necessary -- leaving VMAX too high
108 reduces only the number of available slots in the queues
109 - increased the value of PMAX and QMAX from 16 to 64, so that they
110 also should need adjusting much more rarely
112 ==== Version 5.1.3 - 8 December 2007 ====
114 - fixed important bug that was introduced in 5.1.2 -- the automatic resize option
115 did not work correctly when -DCOLLAPSE was used. the result of a verification was
116 still correct, but the hashtable would become very slow after a single resizing,
117 and possibly duplicate work being done. corrected. (found by Alex Groce)
118 - if the directive -DSPACE is defined, a more memory frugal (and slightly slower)
119 algorithm is used. no automatic resize of the hashtable and no suppression of
120 the default statevector compression mode (used by default in combination with SFH)
121 - COLLAPSE compression didn't work with the new hash functions
122 - if NGQ is defined (no global queue) in multi-core mode, the local workqueues
123 of the cpus is now a fixed size, rather than derived from the -z argument
124 - preventing crash of the parser on the structure if :: false fi, reported
126 - on CYGWIN the max segment size for shared memory is now restricted to 512MB,
127 matching the max imposed by cywin itself
128 - increased the max length of an input line to 1024 (from 512), to avoid preprocessing
129 problems for very long LTL formulae (reported by Peter Schauss)
131 ==== Version 5.1.4 - 27 January 2008 ====
133 - fixed bug in enforcement of weak fairness -- introduced in 4.2.8 with the shortcut
134 based on Schwoon & Esparza 2005. the early stop after a match on the stack did
135 not take the fairness algorithm into account -- which means that it could generate
136 a counter-example that did not meet the fairness requirement.
137 reported by david farago.
138 - added option to explore dfs in reverse with -DREVERSE (useful for very large searches
139 that run out of memory or time before completing the search)
140 - added option to allow bfs to use disk, by compiling with -DBFS_DISK
141 - can set limit to incore bfs queue with -DBFS_LIMIT=N (default N=100000 states)
142 - can set limit to size of each file created with -DBFS_DISK_LIMIT=N (default N=1000000 states)
143 - removed obsolete directive -DQLIST
144 - made disk-use option for multi-core search work in more cases
145 - new runtime option for pan.c to set a time limit to a verification run to a fixed
146 number of N minutes by saying ./pan -QN (single-core runs only)
148 ==== Version 5.1.5 - 26 April 2008 ====
150 - added directives -DT_REVERSE to reverse order in which transitions are explored
151 (complementary to -DREVERSE from 5.1.4 and an alternative to -DRANDOMIZE)
152 - added directive -DSCHED to enforce a context switch restriction (see pan -L)
153 - added directive -DZAPH in bitstate mode, resets the hash array to empty each time it becomes half full
154 - see online references for usage of all new directives
155 http://spinroot.com/spin/Man/Pan.html
156 - directive -DRANDOMIZE can now take an optional random-seed value, as in -DRANDOMIZE=4347
157 - added pan runtime option -x to prevent overwriting existing trail files
158 - added pan runtime option -L to set a max for context switches (in combination with -DSCHED)
159 - pan runtime option -r can take an argument, specifying the trailfile to use
160 - pan runtime option -S replays a trail while printing only user-defined printfs
161 - omitted references to obsolete directives OHASH, JHASH, HYBRIDHASH, COVEST, NOCOVEST, BCOMP
162 - added directive -DPUTPID to include the process pid into each trailfile name
163 - better check for inline parameter replacement, to prevent infinite recursion
164 when the formal parameter contains the replacement text
165 - increased maximum size of a line for internal macro replacement to 2K
166 - other small fixes, e.g., in verbose output, cleaned up multi-core usage detail
168 ==== Version 5.1.6 - 9 May 2008 ====
170 - the bug fix from 5.1.4 for Schwoon & Esparza's shortcut in combination with fairness
171 did not go far enough. an example by Hirofumi Watanabe showed that the shortcut is
172 not compatible with the fairness algorithm at all. the result was the possible
173 generation of invalid accept cycles. the short-cut is no longer used when fairness
174 is enabled. no other changes in this version.
projects / lttv.git / blob