SPIN NEWSLETTER Nr. 25
Contents NewsLetter 25 - May 10, 1999:
The deadline for the 6th Spin workshop, held at the
World Congress in Formal Methods (FM99) in Toulouse,
on 21 September this year, has been extended until:
May 17, 1999
Papers up to 20 pages in length can be submitted by email,
in Postscript, up to midnight in a time-zone of your choice
on May 17 1999 to Stefan Leue at sleue@uwaterloo.ca .
We have a tight schedule for this workshop, so please note
that this new deadline is really strict. For more details see:
http://fee.uwaterloo.ca/~sleue/6thSPIN99.html
More information on FM99 can be found at:
http://www.it.dtu.dk/~db/fm99/FM99Main/FM99Main.html
There will be a joint proceedings for the
two Spin workshops of 1999 as a volume of
a Springer Lecture Notes in Computer Science.
The new release of Spin is getting close to being generally
available. This new Version 3.3.0 has been a few months in
the making, and is considerably more efficient than the current
release (3.2.4), often cutting memory use in half or more.
The most important changes that help to make this so are:
-
Sequences of globally safe or atomic statements are now merged
automatically to form d_step sequences. This can dramatically
reduce the number of states (and the depth of the search stack
that is required to solve a problem).
(This and the next change was inspired by work on the new XMC
model checker at Stony Brook.)
-
A fast dataflow analysis option is added to avoid redundant
data values from increasing the search space unnecessarily.
-
A new stack-cycling option is added to automatically perform
a caching algorithm on the depth-first search stack, using disk
for backup storage with minimal runtime overhead.
If this option is used, you no longer have to guess what the
maximum search depth for your problem will be.
-
The generated transition code for model checking is
organized more intelligently, so that common
statements can share common code. This can cut the size
of the C program that is compiled in half, which translates
directly in faster turn-around times for the verifications
(the code compiles faster).
-
There is a new data declaration tag 'local' which can be used
where currently only 'show' or 'hidden' can be used.
It allows one to identify global variables that are
effectively local (used by only 1 process) as data objects
of which manipulation is safe for partial order reductions.
-
Unused or write-only variables are hidden automatically
to exclude them from the state-vector.
There are other small improvements, many requested by
faithful users, to simplify life. Multiple mtype definitions,
for instance, are now allowed, and there's a more sensible
compiler directive to specify the amount of available memory
in Megabytes instead of as a power of two.
Spin version 3.3.0 is still undergoing more testing, but we
expect that it will become available before the end of this month.
Please let us know if you would like to test a beta version
before the final release is made.
End of Newsletter Nr. 25.
Spin homepage
(spin_list@research.bell-labs.com)