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