0b55f123 |
1 | Distribution Update History of the SPIN sources |
2 | =============================================== |
3 | |
4 | ==== Version 5.0 - 26 October 2007 ==== |
5 | |
6 | The update history since 1989: |
7 | |
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 |
14 | |
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. |
17 | |
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 |
20 | and |
21 | http://www.spinroot.com/spin/multicore/index.html |
22 | which has additional details on the IEEE TSE paper on Spin V5.0. |
23 | |
24 | ==== Version 5.1 - 3 November 2007 ==== |
25 | |
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. |
40 | |
41 | ==== Version 5.1.1 - 11 November 2007 ==== |
42 | |
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 |
69 | |
70 | ==== Version 5.1.2 - 22 November 2007 ==== |
71 | |
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 |
94 | in multi-core mode |
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 |
111 | |
112 | ==== Version 5.1.3 - 8 December 2007 ==== |
113 | |
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 |
125 | by Peter Schauss |
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) |
130 | |
131 | ==== Version 5.1.4 - 27 January 2008 ==== |
132 | |
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) |
147 | |
148 | ==== Version 5.1.5 - 26 April 2008 ==== |
149 | |
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 |
167 | |
168 | ==== Version 5.1.6 - 9 May 2008 ==== |
169 | |
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. |