| 1 | Distribution Update History of the SPIN sources |
| 2 | =============================================== |
| 3 | |
| 4 | ==== Version 4.0.0 - 1 January 2003 ==== |
| 5 | |
| 6 | See the end of the V3.Updates file for the main changes |
| 7 | between the last version 3.5.3 and version 4.0.0. |
| 8 | A glimpse of the Spin update history since 1989: |
| 9 | |
| 10 | Version 0: Jan. 1989 - Jan. 1990 5.6K lines: book version |
| 11 | Version 1: Jan. 1990 - Jan. 1995 7.9K lines: first version on netlib |
| 12 | Version 2: Jan. 1995 - Aug. 1997 6.1K lines: partial-order reduction |
| 13 | Version 3: Aug. 1997 - Jan. 2003 17.9K lines: bdd-like compression (MA) |
| 14 | Version 4: Jan. 2003 - 28.2K lines: embedded c-code, bfs |
| 15 | |
| 16 | ==== Version 4.0.1 - 7 January 2003 ==== |
| 17 | |
| 18 | - the rule that one cannot combine a run operator |
| 19 | in an expression with any other type of boolean |
| 20 | or arithmetic operator within the same expression |
| 21 | is now enforced. |
| 22 | - bfs now produces the usual stats upon finding |
| 23 | and error; and it now supports the -e option. |
| 24 | - extended bfs to deal also with safety properties |
| 25 | specified in never claims and trace assertions. |
| 26 | unlike the regular dfs search, the bfs search cannot |
| 27 | handle the use of atomic sequences inside never claims. |
| 28 | it will issue a warning, and will abort, if it sees this. |
| 29 | unless constructs, d_steps, etc. should all work also |
| 30 | within never claims |
| 31 | a warning is issued if accept labels are found inside |
| 32 | the never claim (to warn that the bfs search is restricted |
| 33 | to safety properties only). |
| 34 | the never claim does always work to restrict the search |
| 35 | space to the part that is covered by the claim. |
| 36 | - fixed bug in simulation mode, where atomicity was not |
| 37 | always correctly preserved across rv actions from one |
| 38 | atomic chain to another (if the sender action was the |
| 39 | last statement in an atomic sequence) reported by Judi Romijn. |
| 40 | - added the BFS option also in the advanced verification |
| 41 | options panel of xspin401.tcl |
| 42 | |
| 43 | ==== Version 4.0.2 - 6 March 2003 ==== |
| 44 | |
| 45 | - removed a long-standing bug in the marking of transitions |
| 46 | for partial order reduction: |
| 47 | the guard statement of an atomic or d_step sequence within |
| 48 | which a non-atomic,atomic,or d_step sequence is nested did |
| 49 | not always get the proper tag |
| 50 | if the tag assigned was local and it should have been global, |
| 51 | the p.o. reduction algorithm could make an invalid reduction. |
| 52 | such a case can indirectly be constructed if an atomic sequence |
| 53 | contains an call of an inline function as the first statement. |
| 54 | (this case was found by Bram de Wachter) |
| 55 | - removed reliance on tmpnam() in main.c -- gcc complains about |
| 56 | it allowing a race condition on the use of the name returned. |
| 57 | we now use fixed local names for the temporary files. |
| 58 | there could be a problem now if two users run spin within the |
| 59 | same directory simultaneously -- but that problem already |
| 60 | exists with xspin as well (pan.tmp and pan.pre) and is |
| 61 | easily avoided. (if needed, we could add a locking mechanism |
| 62 | at some point, but this seems overkill for the time being.) |
| 63 | - the -m option now works the same in breadth-first search as it |
| 64 | does in depth-first search. there's less of a strict reason |
| 65 | to cutoff the search at the -m depth with bfs, since the |
| 66 | stack is not pre-allocated in this case; it grows dynamically. |
| 67 | by setting -m to a very large number, one can therefore just |
| 68 | let the verifier proceed until it exhausts memory, or finishes |
| 69 | (that is to recreate the earlier behavior when needed). |
| 70 | - increased the size of some internal arrays a bit to better |
| 71 | accomodate the use of very long identifier or structure names. |
| 72 | - much improved rule for creating and locating error trail files: |
| 73 | if possible, the trail file is created by appending .trail |
| 74 | to the filename of the source model |
| 75 | some older operating systems don't like it if the filename |
| 76 | for the source model already contains a period, so if a |
| 77 | failure is detect, a second attempt is now made by stripping |
| 78 | the existing . extesion (e.g., .pml) and replacing it with |
| 79 | .trail (some os's also truncate this to .tra, which is also |
| 80 | accepted). |
| 81 | |
| 82 | ==== Version 4.0.3 - 3 April 2003 ==== |
| 83 | |
| 84 | - no verbose steps printed for never claim in guided simulations |
| 85 | unless -v is given as a commandline argument |
| 86 | state changes in the never claim are still printed, but with |
| 87 | the already existing separate output ("Never claim moves to...") |
| 88 | - new spin command-line option -I, to reproduce a version of the |
| 89 | specification after preprocessing and inlining operations are |
| 90 | done. the reproduced code is not complete: declarations and |
| 91 | process parameters are skipped, some internally generated labels |
| 92 | and jumps (e.g., replacing break statements) also become visible. |
| 93 | the version is intended only to show what the effect of inlining |
| 94 | and preprocessing is. |
| 95 | - change in sched.c to suppres printing of final value of variables |
| 96 | marked 'show' -- this looks like an assignment, which is confusing. |
| 97 | - small fixes in xspin, which is now xspin402.tcl |
| 98 | - in guided simulation mode, when a claim from an ltl property is |
| 99 | present, the simulator's pid nrs did not always agree with the |
| 100 | verifiers numbers -- this could lead to the wrong name for a |
| 101 | process being printed in the simulation trails. |
| 102 | |
| 103 | ==== Version 4.0.4 - 12 April 2003 ==== |
| 104 | |
| 105 | - there was a bug in 4.0.3 that prevented successful compilation |
| 106 | of pan.c (and unbalanced endif, caused by a missing newline |
| 107 | character in pangen1.h on line 3207) |
| 108 | - there was a maximum of 128 variables that could be changed per |
| 109 | atomic sequence, this is now 512. |
| 110 | |
| 111 | ==== Version 4.0.5 - 29 May 2003 ==== |
| 112 | |
| 113 | - correction in the reporting of process id's during guided simulation. |
| 114 | the numbers could be off by one when never claims are used. |
| 115 | (just a reporting problem, the run itself was always correct) |
| 116 | - increased bounds on the length of strings passed as preprocessor |
| 117 | commands |
| 118 | - explicit cast of return value ot strlen to int, to keep compilers |
| 119 | happier |
| 120 | - fixed subtle bug in the fairness option (reported by Dragan |
| 121 | Bosnacki). with fairness enabled, standard claim stutter could |
| 122 | in special cases cause a false acceptance cycle to be reported |
| 123 | (i.e., a cycle not containing an accepting state). |
| 124 | for compatibility, the old behavior can still be obtained by |
| 125 | compiling the pan.c verifiers with -DOLDFAIR. the default is |
| 126 | the fixed algorithm. |
| 127 | - restricted the maximum length of a string in the lookup table |
| 128 | for c_code segments to 1024 characters. this table is only used |
| 129 | to print out the code segment in error traces -- so the truncation |
| 130 | is cosmetic, not functional. it avoids compiler complaints about |
| 131 | excessively long strings though (which could prevent compilation). |
| 132 | - improved error reporting when a value outside the range of the |
| 133 | target data type is passed as an parameter in a run statement |
| 134 | |
| 135 | ==== Version 4.0.6 - 29 May 2003 ==== |
| 136 | |
| 137 | - the fix of the fairness option wasn't quite right. |
| 138 | directive -DOLDFAIR is gone again, and the real fix |
| 139 | is now in place. |
| 140 | |
| 141 | ==== Version 4.0.7 - 1 August 2003 ==== |
| 142 | |
| 143 | .------------------------------------------------------. |
| 144 | | Version 4.0.7 is the version of Spin that is | |
| 145 | | described in the Spin book (Addison-Wesley 2003) | |
| 146 | | and that is used for all examples there | |
| 147 | | http://spinroot.com/spin/Doc/Book_extras/index.html | |
| 148 | .------------------------------------------------------. |
| 149 | |
| 150 | - added (really restored) code for allowing separate |
| 151 | compilation of pan.c for model and claim |
| 152 | two new (previously undisclosed) commandline |
| 153 | options -S1 and -S2 -- usage documented in the new book |
| 154 | |
| 155 | - if it is detected that a c_expr statement definitely has |
| 156 | side effects, this now triggers a fatal error. |
| 157 | |
| 158 | - complains about more than 255 active processes |
| 159 | being declared in active prefix |
| 160 | |
| 161 | - fix in -A option: removed bug in handling of eval() |
| 162 | |
| 163 | - cosmetic changes: |
| 164 | endstate and end-state are now spelled 'end state' as |
| 165 | preferred by Websters dictionary (...) |
| 166 | hash-array, hash-table, and never-claim similarly |
| 167 | are now spelled without hyphens |
| 168 | |
| 169 | - improved error replay for models with embedded c code |
| 170 | |
| 171 | - the -m option is no longer automatically set in guided |
| 172 | simulation runs. |
| 173 | |
| 174 | - change spin.h to allow it to be included twice without |
| 175 | ill effects (happens in y.tab.c, generated from spin.y) |
| 176 | |
| 177 | - updated the make_gcc file for newer versions if cygwin |
| 178 | |
| 179 | ==== Version 4.1.0 - 4 December 2003 ==== |
| 180 | |
| 181 | - new spin option -h, when used it will print out the |
| 182 | seed number that was used for the random number |
| 183 | generator at the end of a simulation run -- useful |
| 184 | when you have to reproduce a run precisely, but forgot |
| 185 | to set an explicit seed value with option -n |
| 186 | |
| 187 | - c_track now has an optional extra argument, to be |
| 188 | documented - the extra qualifier cannot be used with BFS |
| 189 | (spin.h, spin.y, spinlex.c, pangen4.c, ...) |
| 190 | |
| 191 | - the documentation (book p. 41) says that unsigned data |
| 192 | can use a width specifier up to 32 bits -- it actually |
| 193 | only worked up to 31 bits. it now works as advertised. |
| 194 | fix courtesy of Doug McIlroy. (vars.c) |
| 195 | |
| 196 | - when trying to compile a model without initialized |
| 197 | channels, a confusing compiler error would result. |
| 198 | now avoided (spin.y, pangen1.c) |
| 199 | |
| 200 | - there is no longer a default maximum memory arena |
| 201 | on verifications, that would apply in the absence of |
| 202 | an explicit -DMEMCNT or -DMEMLIM setting (the default |
| 203 | was 256 Mb). |
| 204 | |
| 205 | - some more fixes to account for 64bit machines, courtesy |
| 206 | of C. Scott Ananian. |
| 207 | |
| 208 | - from Dominik Brettnacher, some instructions on compiling Spin |
| 209 | on a Mac under OS X, added to the installation README.html |
| 210 | file. |
| 211 | |
| 212 | - so far you could not use a -w parameter larger than |
| 213 | 31 during bitstate search -- this effectively limited |
| 214 | the max bitarray to about 512Mb. the max is now -w32 |
| 215 | which extends this to 1Gb (i.e., 4 10^9 bits). |
| 216 | (really should be allowed to go higher, but wordsize |
| 217 | gets in the way for now.) |
| 218 | |
| 219 | - suppressed a redundant 'transition failed' message |
| 220 | that could occur during guided simulations (guided.c) |
| 221 | |
| 222 | - fixed a long standing bug that could show up if the last |
| 223 | element of an atomic sequence was itself a sub-sequence |
| 224 | (e.g., defined as an inline or as an unless stmnt). |
| 225 | in those cases, atomicity could be lost before the |
| 226 | last statement (sequence) completed. (flow.c) |
| 227 | |
| 228 | - fixed two long standing bugs in parsing of |
| 229 | nested unless structures. the bug showed up in |
| 230 | a double nested unless that is itself embedded in a |
| 231 | non-atomic block. symptom was that some code became |
| 232 | unreachable (thanks to Judi Romijn for the example). |
| 233 | goto statements that survived state machine optimization |
| 234 | also did not properly get tagged with escape options. |
| 235 | |
| 236 | - also fixed a bug in handling excessively long assertion |
| 237 | strings (larger than 999 characters) during verification |
| 238 | |
| 239 | - revised the way that c_track is implemented (the points |
| 240 | where c_update and c_revert are called) to make it a |
| 241 | little easier to maintain |
| 242 | |
| 243 | - removed some no longer used code from pangen1.h |
| 244 | |
| 245 | - fixed bug in treatment of rendezvous statements in BFS mode |
| 246 | |
| 247 | - xspin408.tcl update: compiler errors are now printed in the |
| 248 | log window, as they should have been all along... |
| 249 | (courtesy Doug McIlroy) |
| 250 | |
| 251 | ==== Version 4.1.1 - 2 January 2004 ==== |
| 252 | |
| 253 | - extended bitstate hashing on 32-bit machines to work correctly |
| 254 | with -w arguments up to and including -w34 (courtesy Peter Dillinger) |
| 255 | - reduced amount of memory allocated to dfs stack in bitstate |
| 256 | mode to something more reasonable (it's accessed through a |
| 257 | hash function -- now related to the maxdepth, not the -w |
| 258 | parameter |
| 259 | - fixed bug that could cause problem with very long assertions |
| 260 | (more than 256 characters long) |
| 261 | |
| 262 | - in xspin411, verbose mode during verifications is now default |
| 263 | (it adds line numbers reached in the never claim to the output) |
| 264 | - small fixes to the search capability in most text windows |
| 265 | |
| 266 | ==== Version 4.1.2 - 21 February 2004 ==== |
| 267 | |
| 268 | - fixed bug in support for notrace assertions (the pan.c would |
| 269 | not compile if a notrace assertion was defined) |
| 270 | - fixed unintended feature interaction between bitstate search |
| 271 | and the -i or -I runtime flags for finding the shortest |
| 272 | counter-example |
| 273 | - some cosmetic changes to ease the life of static analyzers |
| 274 | - fixed implementation of Jenkins function to optionally |
| 275 | skip a semi-compression of the statevector -- to increase speed |
| 276 | (pointed out by Peter Dillinger) |
| 277 | - fixed bug in resetting memory stack arena that could show up |
| 278 | in iterative verification runs with pan -R argument |
| 279 | (also found by Peter Dillinger) |
| 280 | - new version of xspin 4.1.2, with a better layout of some |
| 281 | of the panels |
| 282 | |
| 283 | ==== Version 4.1.3 - 24 April 2004 ==== |
| 284 | |
| 285 | - changed from using "cpp" by default to using "gcc -E -x c" |
| 286 | given that most users/systems have gcc anyway to compile c programs |
| 287 | and not all systems have cpp in a fixed place. |
| 288 | there should be no visible effect of this change. |
| 289 | |
| 290 | - a rendezvous send operation inside an atomic sequence was |
| 291 | incorrectly accepted as a candidate for merging with subsequent |
| 292 | statements in the atomic sequence. it is the only type of statement |
| 293 | that can cause loss of atomicity (and a switch to another process) |
| 294 | when *executable* (rather than when blocking, as is the case for |
| 295 | all other types of statements, including asynchronous sends). |
| 296 | this is now fixed, such that if there is at least one rv channel |
| 297 | in the system, send operations inside atomic sequences cannot |
| 298 | be merged with any other statement |
| 299 | (in general, we cannot determine statically if a send operation |
| 300 | targets an rv channel or an asynchronous channel, so we can only |
| 301 | safely allow the merging if there are no rv channels at all). |
| 302 | this can cause a small increase in the number of stored states |
| 303 | for models with rendezvous cannels |
| 304 | |
| 305 | - counter-examples produced for liveness properties (non-progress or |
| 306 | acceptance cycles) often contained one step too many -- now fixed |
| 307 | |
| 308 | - added check for reuse of varnames in multiple message fields |
| 309 | i.e., q?x,x is not allowed (would cause trouble in the verifier) |
| 310 | |
| 311 | - added a warning against using a remote reference to a label |
| 312 | that is declared inside an atomic or d_step sequence -- such |
| 313 | labels are always invisible to the never claim (since the |
| 314 | executing of the sequence containing the label is meant to be |
| 315 | indivisible), which can cause confusion. |
| 316 | |
| 317 | - "StackOnly" can be used as an alternative to "UnMatched" when used |
| 318 | as the optional 3rd argument a c_track primitive (see Spin2004 paper) |
| 319 | |
| 320 | ==== Version 4.2.0 - 27 June 2004 ==== |
| 321 | |
| 322 | - main.c now recognizes __OpenBSD__ and treats it the same as __FreeBSD__ |
| 323 | |
| 324 | - general cleanup of code (removing some ifdefs etc) |
| 325 | |
| 326 | - allow reuse of varnames in multiple message fields (see 4.1.3) if |
| 327 | var is an array variable (e.g., using different elements) |
| 328 | |
| 329 | - deleted support for directive -DCOVEST -- replaced with -DNOCOVEST |
| 330 | |
| 331 | - deleted support for directive -DHYBRID_HASH |
| 332 | |
| 333 | - deleted support for directive -DOHASH, -DJHASH, -DEXTENDED |
| 334 | added -DMM for an experimental/debugging mode (non-documented) |
| 335 | |
| 336 | - replaced Jenkins' original hashfunction with an extended version |
| 337 | contributed by Peter Dillinger. |
| 338 | it uses more of the information to generate multiple pseudo hash values |
| 339 | (multi-hashing with anywhere from 1,2,... hash-functions) |
| 340 | |
| 341 | - added runtime verifier flag -k to support multi-hashing in Bitstate mode. |
| 342 | pan -k2 reproduces the default behavior, with 2 bits set per state. |
| 343 | pan -k1 is the same as the old pan -s (which also still works). |
| 344 | (as also first suggested by Dillinger and Manolios from Georgia Tech.) |
| 345 | |
| 346 | - some more useful hints are generated at the end of each bitstate |
| 347 | run about possible improvements in coverage, based on the results |
| 348 | obtained in the last run. |
| 349 | |
| 350 | - updated xspin420.tcl to match the above changes in verification options. |
| 351 | |
| 352 | ==== Version 4.2.1 - 8 October 2004 ==== |
| 353 | |
| 354 | - improvement of BFS mode for partial order reduction, thanks to |
| 355 | Dragan Bosnacki |
| 356 | - fewer redundant declarations and fewer complaints from static analyzers |
| 357 | - a d_step could under some circumstances interfere with a rendezvous |
| 358 | in progress (e.g., when the d_step started with an if statement, or |
| 359 | when it started with a send or receive rather then a straight guard |
| 360 | condition (i.e., an expression). this now works as it should. |
| 361 | - 4.2.0 attempted to make support for coverage estimates the default. |
| 362 | this, however, means that on some systems the pan.c source has to be |
| 363 | compiled with an additional -lm flag (for the math library) |
| 364 | coverage estimates had to be turned off explicitly by compiling with |
| 365 | -DNOCOVEST |
| 366 | in 4.2.1 the earlier default is restored, meaning that you have to |
| 367 | specify -DCOVEST to get the coverage estimates (and presumably you |
| 368 | will then know to compile also with -lm) |
| 369 | - fixed bug that caused an internal name conflict on the verification |
| 370 | of the mobile1 model from the Test distribution |
| 371 | - fixed a problem that prevented having more than 127 distinct proctypes |
| 372 | the max is now 255, the same as the max number of running processes. |
| 373 | - fix to restore bitstate hashing to work on 64-bit machines |
| 374 | we still only compute a 32-bit hash; the largest usable bitstate |
| 375 | hash-array remains 2^35 bits (i.e., 2^32 bytes or 4 Gigabytes). |
| 376 | (the maximum on 32-bit machines remains -w34 or 2 Gigabytes) |
| 377 | for 64-bit mode, we will extend this soon to take advantage of |
| 378 | larger memory sizes available on those machines. [see 4.2.5] |
| 379 | - the default number of hash-functions used in bitstate hashing |
| 380 | is now 3 (equivalent to a runtime option -k3), which gives slightly |
| 381 | better coverage in most cases |
| 382 | |
| 383 | ==== Version 4.2.2 - 12 December 2004 ==== |
| 384 | |
| 385 | - verifiers now can be compiled with -DRANDOMIZE (for dfs mode only) |
| 386 | to achieve that transitions within each process are explored in |
| 387 | random, rather than fixed, order. the other in which processes are |
| 388 | explored remains fixed, with most recently created process explored |
| 389 | first (if we can think of a good way of supporting random mode |
| 390 | for this, we may add this later). if there is an 'else' transition |
| 391 | among the option, no randomization is done (since 'else' currently |
| 392 | must be explored as the last option in a set, to work correctly). |
| 393 | this option can be useful to get more meaningful coverage of very |
| 394 | large states that cannot be explored exhaustively. |
| 395 | the idea for this option is Doron Peled's. |
| 396 | - fixed a limitation in the pan.c verifiers that prevented the use |
| 397 | of channels with more than 256 slots. this should rarely be an |
| 398 | issue, since very large asynchronous channels are seldomly useful |
| 399 | in verifications, but it might as well work. |
| 400 | - fix to avoid a compiler complaint about a missing prototype when |
| 401 | compiling pan.c with -DBFS |
| 402 | - renamed error message about us of hidden arrays in parameter list |
| 403 | to the more accurate description 'array of structures' |
| 404 | |
| 405 | ==== Version 4.2.3 - 5 February 2005 ==== |
| 406 | |
| 407 | - _pid and _ are no longer considered global for partial order reduction |
| 408 | - fixed bug that could lead to the error "confusing control structure" |
| 409 | during guided simulations (replay of error trails) |
| 410 | - fixed problem where an error trail could be 1 step too long for |
| 411 | invalid endstate errors |
| 412 | - added experimental 64-bit hash mode for 64-bit machines, |
| 413 | compile pan.c in bitstate mode with the additional directive -DHASH64 |
| 414 | the code is by Bob Jenkins: http://burtleburtle.net/bob/c/lookup8.c |
| 415 | [placeholder for a later extension for 64 bit machines] |
| 416 | |
| 417 | ==== Version 4.2.4 - 14 February 2005 ==== |
| 418 | |
| 419 | - added missing newline after #ifdef HASH64 -- introduced in 4.2.3 |
| 420 | this caused a compiler warning when compiling pan.c in -DBITSTATE mode |
| 421 | - a terminating run ending in an accept state was not stutter extended |
| 422 | unless a never claim was defined. this now works also without a |
| 423 | never claim, provided that a search for acceptance cycles is performed. |
| 424 | in the absence of a never claim the corresponding error type is |
| 425 | called a 'accept stutter' sequence (to distinguish it from 'claim stutter') |
| 426 | (bug report from Alice Miller) |
| 427 | the extension is disabled if the compiler directive -DNOSTUTTER is used, |
| 428 | just like for the normal claim stutter extension rule |
| 429 | - added support for using -DSC on file sizes larger than 2Gb (courtesy Hendrik Tews) |
| 430 | - in simulation mode, the guard statement of a d_step sequence was not |
| 431 | subject to escape clauses from a possible unless statement, contrary to the |
| 432 | language spec. in verification mode this did work correctly; simulation mode fixed. |
| 433 | (courtesy Theo Ruys and David Guaspari) |
| 434 | - added warning for use of an 'unless' construct inside a d_step sequence |
| 435 | |
| 436 | ==== Version 4.2.5 - 2 April 2005 ==== |
| 437 | |
| 438 | - the default bitstate space size is now 1 Mb (was 512K) |
| 439 | - the default hashtable size in exhaustive mode is now 512K slots (was 256K) |
| 440 | - fixed memory leak that can bite in very long simulation runs |
| 441 | (courtesy Hendrik Tews) |
| 442 | - now turns off dataflow optimization (setting dead variables to 0) |
| 443 | when remote variable references are used. (this is a little bit of |
| 444 | overkill, since we'd only need to turn it off for the variables |
| 445 | that are being monitored from the never claim, but it is simple and safe) |
| 446 | - you can now compile pan.c with -DHASH64 to invoke a 64bit Jenkins hash, |
| 447 | (enabled by default on 64bit machines) or disable it by compiling with -DHASH32 |
| 448 | (which is the default on 32bit machines) |
| 449 | the 64-bit version of Spin (and of the pan.c files it generates) has now been |
| 450 | fully tested; this means that we can now use more than 4 Gbyte of memory, both |
| 451 | in full state and in bitstate mode. |
| 452 | - added pan runtime options -M and -G (inspired by the work of Peter Dillinger |
| 453 | and Panagiotis Manolios on 3Spin), with a simple implementation. |
| 454 | (the code for pangen1.h actually got smaller in this update). |
| 455 | |
| 456 | these two new options are available in bitstate mode only and allow the user to |
| 457 | define a bitstate hash array that is not necessarily equal to a power of two. |
| 458 | if you use -M or -G, then this overrides any other setting you may have |
| 459 | used for -w. for example: |
| 460 | pan -M5 will use a hash array of 5 Megabytes |
| 461 | pan -G7 will use a hash array of 7 Gigabytes. |
| 462 | use this instead of -w when the hash array cannot be a power of 2 bytes large. |
| 463 | pan -M4 is technically the same as pan -w25 in that it will allocate |
| 464 | a hash array of 4 Megabytes (2^(25-3) bytes), but it can be slower |
| 465 | because indices into the hash-array are now computed with a modulo operator |
| 466 | instead of with faster bit masks and bit shifts. similarly, |
| 467 | pan -G1 is technicall the same as pan -M1024 or pan -w33 |
| 468 | whether the use of -M and -G is slower than -w depends on your compiler. |
| 469 | many modern compilers (e.g. gcc and microsoft visual studio) will automatically |
| 470 | optimize the hash array access anyway when it effectively is a power |
| 471 | of two large (i.e., independent of whether you use -w25 or -M4). |
| 472 | in a small set of tests on a 2.5 GHz machine, using both gcc and the MS |
| 473 | compilers, no meaningful difference in speed when using -M or -G could be |
| 474 | measured, compared with -w (not even for non powers of two hash array sizes). |
| 475 | (the difference in runtime was in the order of 3 to 4%). |
| 476 | |
| 477 | ==== Version 4.2.6 - 27 October 2005 ==== |
| 478 | |
| 479 | - mostly small fixes -- one bug fix for reading error trails on 64bit machines |
| 480 | (courtesy Ignacy Gawedzki) |
| 481 | - the full tar file now creates all files into a single common directory named |
| 482 | Spin, which will simplify keep track of versions and updates |
| 483 | - small update of xspin as well (now xspin4.2.6) |
| 484 | the main change in xspin is that on startup it will now look for a file with |
| 485 | the same name as the filename argument given (which is typically the name of |
| 486 | the file with the Promela model in it) with extension .xsp |
| 487 | so when executing "xspin model" the command will look for a file "model.xsp". |
| 488 | xspin will read this file (if present) for commands to execute upon startup. |
| 489 | (very useful for demos!) |
| 490 | commands must start with either "X:" or "L:" |
| 491 | an L: command must be followed by a number, which is used to set the number of |
| 492 | lines that should be visible in the command log window |
| 493 | an X: command can be followed by any shell command, that xspin will now execute |
| 494 | automatically, with the output appearing in the command log window |
| 495 | an example .xsp file: |
| 496 | |
| 497 | X: spin -a model |
| 498 | L: 25 |
| 499 | X: nice gcc -DMEMLIM=1000 -DCOLLAPSE -DSAFETY -DREACH -o pan pan.c |
| 500 | X: nice time -p ./pan -i -m150 |
| 501 | X: spin -t -c -q3 model |
| 502 | X: cp model.trail pan_in.trail |
| 503 | |
| 504 | ==== Version 4.2.7 - 23 June 2006 ==== |
| 505 | |
| 506 | - change in pc_zpp.c, courtesy of Sasha Ivanov, to fix an incorrect order of |
| 507 | preprocessing directives -- scanning "if" before "ifdef" and "ifndef" |
| 508 | |
| 509 | - all 3 very dubious types of statements in the following model were erroneously |
| 510 | accepted by Spin version 4.2.6 and predecessors. |
| 511 | they no longer are -- courtesy of the class of 2006 @ Caltech CS |
| 512 | active proctype X() { |
| 513 | chan q = [2] of { int, int }; |
| 514 | |
| 515 | _nr_pr++; /* change the number of processes... */ |
| 516 | _p = 3; /* change the state of process X.... */ |
| 517 | q!2(run X()); /* something really devious with run */ |
| 518 | } |
| 519 | |
| 520 | - added the compiler directive __NetBSD__ |
| 521 | |
| 522 | - the vectorsize is now always stored in an unsigned long, to avoid |
| 523 | some obscure bugs when the size is chosen too small |
| 524 | |
| 525 | - fix in the parsing of LTL formulae with spin -f to make sure that |
| 526 | unbalanced braces are always detected |
| 527 | |
| 528 | - added warning against use of rendezvous in BFS mode -- which cannot |
| 529 | guarantee that all invalid endstates will be preserved |
| 530 | |
| 531 | - minor things: make_pc now defaults to gcc instead of cl (the microsoft |
| 532 | visual studio compiler) |
| 533 | |
| 534 | - xspin4.2.7 disables some bindings that seem to be failing |
| 535 | consistently now on all platforms, although the reason is unclear |
| 536 | (this occurs in the automata view and the msc views, which are supposed |
| 537 | to track states or execution steps to source lines in the main text |
| 538 | window -- instead these bindings, if enabled, now seem to hang the gui) |
| 539 | |
| 540 | ==== Version 4.2.8 - 6 January 2007 ==== |
| 541 | |
| 542 | - added optimizations in cycle search described by Schwoon & Esparza 2005, |
| 543 | in 'a note on on-the-fly verification algorithms' and in |
| 544 | Gastin, Moro, and Zeitoun 2004, 'Minimization of counter-examples in Spin' |
| 545 | to allow for early detection of acceptance cycles, if a state is found |
| 546 | on the stack that is accepting, while still in the 1st dfs. the version |
| 547 | also mentioned in Schwoon & Esparza -- for the case where the source state |
| 548 | of such a transition is accepting -- is also included. |
| 549 | |
| 550 | - eleminated many of the #ifdef PC directives that distinguished between |
| 551 | use of y.tab.h and y_tab.h which is no longer needed with the newer |
| 552 | versions if yacc on cygwin (e.g., bison yacc) |
| 553 | |
| 554 | - the use of a non-local x[rs] assertion is now fatal |
| 555 | |
| 556 | - fixed small problem where scheduler could lose track of a process during |
| 557 | simulations |
| 558 | |
| 559 | - small rewrites for problems spotted by static analyzers |
| 560 | |
| 561 | - restored correct working of separate compilation option (-S[12]) |
| 562 | |
| 563 | - fixed initialization problem with local variables (making sure that |
| 564 | a local can be initialized with a parameter or with the value of a |
| 565 | previously declared and initialized local |
| 566 | |
| 567 | - emalloc now returns NULL when 0 bytes are requested (robert shelton 10/20/06) |
| 568 | |
| 569 | - using _stat instead of stat on WIN32 platforms for compatibility with cl.exe |
| 570 | |
| 571 | - avoided a problem with non-writable strings, in pan.c |
| 572 | |
| 573 | - renamed QPROVISO to Q_PROVISO in preparation for related updates in 4.3.0 |
| 574 | |
| 575 | - fixed problem with the final transition of an error trail sometimes |
| 576 | not appearing in the trail file (alex groce) |
| 577 | |
| 578 | ==== Version 4.2.9 - 8 February 2007 ==== |
| 579 | |
| 580 | - the optimization for cycle search from 4.2.8 wasn't complete -- it could cause |
| 581 | annoying messages to show up, and the start of a cycle not being identified |
| 582 | in all cases (Moti Ben-Ari) -- it now works they way it was intended |
| 583 | |
| 584 | - made it possible to compile pan.c with visual studio, provided that -DWIN32 or |
| 585 | -DWIN64 are included in the compiler directives; see make_pc for an example. |
| 586 | without this, file creat calls would crash the application -- because the windows |
| 587 | implementation of this call uses its own set of flags... |
| 588 | |
| 589 | - the spin parser now flags all cases where the wrong number of parameters |
| 590 | is specified in a run statement (as suggested by Klaus Havelund) |
| 591 | |
| 592 | - it is now possible to use a c_expr inside an expression, e.g. as in |
| 593 | x[ c_expr { 4 } ] = 3 or x[ c_expr { f() } ] (Rajeev Joshi) |
| 594 | |
| 595 | - a new option for ./pan when embedded C code is used: -S to replay the |
| 596 | error trace without printing anything other than the user-defined printfs |
| 597 | from the model itself or from inside c_code fragments - (Rajeev Joshi) |
| 598 | |
| 599 | ==== Version 4.3.0 - 22 June 2007 ==== |
| 600 | |
| 601 | - bug fix (thank you Claus Traulsen) for goto jumps from one atomic |
| 602 | sequence into another. if the first was globally safe, but the second |
| 603 | was not, then an erroneous partial-order reduction was possible |
| 604 | - small changes based on static analyzer output, to increase robustness |
| 605 | - smaller pan.c files generated if huge arrays are part of the model |
| 606 | - more accurate reporting of statecounts in bitstate liveness mode |
| 607 | - better portability for compilation with visual studio |
| 608 | - likely to be the last spin version 4 release -- the next should be 5.0 |
| 609 | which supports safety and liveness verification on multi-core systems |
| 610 | |
| 611 | ==== Version 5.0 - 26 October 2007 ==== |
| 612 | |
| 613 | - lots of small changes to make the sources friendlier to static analyzers, |
| 614 | like coverity, klocwork, codesonar, and uno, so that they find fewer things |
| 615 | to warn about |
| 616 | - improved check for a match of the number of operands specified to a run |
| 617 | operator with the number of formal parameters specified for the proctype |
| 618 | (courtesy an example by Klaus Havelund) |
| 619 | - memory counts are now printed properly as MB quantities (divided by |
| 620 | 1024*1024 instead of 1,000,000) |
| 621 | - more accurate treament of atomic sections that contain goto statements, |
| 622 | when they jump into a different atomic section (especially when the two |
| 623 | atomics have different properties under partial order reduction) |
| 624 | (courtesy and example by Claus Traulsen) |
| 625 | - improvement treatment of run statements for processes that initialize |
| 626 | local variables with global expressions. in these cases the run |
| 627 | statement itself is now recognized as global -- otherwise it can still |
| 628 | be treated as local under partial order reduction rules |
| 629 | - improved treatment of variable update printing when xspin is used. |
| 630 | before, large structures were always full printed on every step, which |
| 631 | could slow down xspin significantly -- this now happens only if there |
| 632 | was a change of at least one of the values printed. |
| 633 | |
| 634 | Additions: |
| 635 | - support for use of multi-core systems, for both safety and liveness |
| 636 | properties. see: http://www.spinroot.com/spin/multicore/ |
| 637 | - added the time of a run in seconds as part of all outputs, and in many |
| 638 | cases also the number of new states reached per second |
| 639 | |
| 640 | - new compile-time directives for pan.c supported in Version 5.0 include: |
| 641 | NCORE, SEP_STATE, USE_DISK, MAX_DSK_FILE, FULL_TRAIL, T_ALERT |
| 642 | and for more specialized use: |
| 643 | SET_SEG_SIZE, SET_WQ_SIZE, C_INIT, SHORT_T, ONESECOND |
| 644 | the following three can be left unspecified unless prompted by pan itself |
| 645 | on a first trial run: |
| 646 | VMAX, PMAX, QMAX, |
| 647 | the use of all the above directives is explained in |
| 648 | http://www.spinroot.com/spin/multicore/V5_Readme.html |
| 649 | for typical multi-core applications only the use of -DNCORE=N is |
| 650 | typically needed |
| 651 | - a small number of other new directives is not related to the use of |
| 652 | multicore verifications - their use is also explained (at the very |
| 653 | bottom of) the V5_Readme.html file mentioned above. they are: |
| 654 | FREQ, NUSCC, BUDGET, THROTTLE, LOOPSTATE, NO_V_PROVISO |