SPIN NEWS - Nr. 3 - February 15, 1995

Contents of this NewsLetter:

New Feature: Message Sequence Charts

Inspired by a proposal from Ted Ewanchyna from Concordia University in Canada, XSPIN has now been extended with graphical support for `message sequence charts' (or if you prefer `time sequence diagrams')
The MSC's give a graphical depiction of the flow of messages between processes. The current version is smart enough to figure out the proper semantics of sorted send and random receive operations from Promela2, and they give graphical support for indicating cycles (non-progress cycles and acceptance cycles, as reported by the verifier in error-trails).
A first version of this MSC implementation in XSPIN was tested by Michael Griffioen, Patrice Godefroid, and Pieter van Eijk (thanks!), and extended based on their feedback.
If you are unsure if this new feature could be useful to you - you are encouraged to give it a try. It can make a large difference in the clarity of simulations. If nothing else, the graphical displays (dynamically updated during simulation runs) makes for an impressive demonstration of online verification methodology, and it has good instructive value (for those teaching courses).

Retrieve the file 

	/netlib/spin/spin2.Xspin.tar.Z
to obtain the new version (you'll need the updated version of the SPIN sources themselves as well for optimal effect. See below.)

Other Recent Changes

A good number of bugs (unintended features?) in the new release of SPIN has now (with help from many of you!) been traced down and repaired. After 9 initial minor updates that could safely be ignored, there is now a more stable new release of SPIN, numbered Version 2.1 (15 February 1995).

Version 2.1 fixes a number of problems that could occur with deeply nested user-defined data structures (typedefs) that can be specified in the new Promela2 (some were caught by Roberto Manione and colleagues from CSELT, and some others by Rob Gerth from Eindhoven University in the Netherlands). Line number references are more accurate now, and some nasty bugs in the implementation of d_step sequences have also been fixed.

To reduce the chores of updating the sources to a minimum, the organization of the distribution files has been improved

All SPIN sources are now retrievable from a separate tar-file: 

	/netlib/spin/spin2.Src.tar.Z
	(these are all files with names beginning Src/...)
All XSPIN files separately retrievable in the file: 
	/netlib/spin/spin2.Xspin.tar.Z
	(all file names beginning with Xspin/..)
All remaining files, with documentation, test-cases etc, that you typically need never refresh once you have a copy, are available in: 
	/netlib/spin/spin2.Other.tar.Z
To simplify updates for minor releases, a small file is maintained called: 
	/netlib/spin/upgrades
this file contains a bourne shell script (/bin/sh) that can update your existing sources online - provided they have a matching major release number.

Since we now switched to a new major release (meaning significant fixes or extensions have been made), we start off with an empty upgrades file for now (and you'll need to retrieve spin2.Src.tar to get the new clean version of SPIN)

-> The recommendation is, if you are now using a SPIN version between 2.0 and 2.0.9 (say `spin -V' to find out which you have), to retrieve the new version of the sources: 

	/netlib/spin/spin2.Src.tar.Z

Feedback from SPIN Users

Several people whose project appeared on the list of SPIN Projects, included the first newsletter, reported that they have received a good number of enquiries from other users about their work. Some of these contacts have meanwhile led to new collaborations.

Kartik Subramanian, whose request for job suggestions appeared in the last newsletter, reported that he did get at least one response from a research lab - and he is now pursuing the lead.

These are two good examples of the types of connections that this newsletter may help establish more often. Do let me know if you have something that might be of interest to other SPIN users that could be included.

Some Frequently Asked Questions

1. On Stuttering Semantics

The algorithms used in SPIN are based on the theory of omega automata, see e.g. [1] for an overview. In standard automata theory, a sequence of inputs is `accepted' by a finite automaton if the inputs drive that automaton from an initial state to a final state that was labeled as accepting. The sequence is therefore always a finite one. Since computations can just as easily be infinite (for non-terminating programs) and since correctness properties may have to be applied to infinite computations (e.g., liveness properties), we need a theory that can handle a different type of automaton, where acceptance is defined specifically for infinite computations. Such an automaton is called an omega automaton, and one particular instance of an automaton of that type is the Buchi automaton - about which more shortly.

Very briefly again, an omega automaton accepts an input sequence iff that sequence drives the automaton from an initial state through a sequence of states that contains an accepting state infinitely often. SPIN's accept labels are defined in such a way that they match precisely this formalism.

The question is now reversed: what can we do with terminating computations within a formal framework that deals only with non-terminating computations?
The standard method is to force a terminating computation to become infinite, by adding a dummy selfloop to the final state that is reached in such a computation. This has just the desired effect, because indeed when the computation terminates, the final state reached does persist forever-after (which can be important for the correctness argument), and also if the final state was accepting, it will function just like the accepting state of a classic (non-omega) automaton.

To express correctness properties for liveness in SPIN, the recommended procedure is therefore as follows:

  1. express the *negation* of the property in next-time-free linear time temporal logic (LTL). this property formalizes all *counter-examples* to the original correctness claim
  2. build the Buchi automaton that formally corresponds to the LTL formula just constructed. at the moment, this is best done by hand - and generally not very hard to do. The Buchi automaton is constructed such that it will accept precisely the counter-examples formalized in the first step. (We are working on efficient translation procedures so that Promela may soon be extended with a syntax for expressing LTL properties directly)
  3. describe the automaton in the syntax of a Promela never claim, and add it to the specification.
In this method, accept labels are used *exclusively* in the never claim, and not in the remainder of a Promela specification. SPIN is able to treat both the never claim *and* each proctype as Buchi automata (meaning: you can use accept labels anywhere), but the above method of working conforms more closely to the automata theoretic foundation.

Suppose we have a never claim, based on a Buchi automaton, derived from an LTL formula (there are hints in the Doc directory for how to proceed with this - more documentation is in preparation for this aspect - so don't worry if this looks a bit difficult).
If we run the verification and encounter a terminating computation, the process of extending the final state of such a terminating computation with a dummy self-loop (to make it infinite) is called `stuttering.' Since only the never claim can make real transitions at this point we also call it `claim stuttering' in SPIN. If an acceptance cycle can be closed through claim stuttering we have a violation of the original correctness property (i.e., we found a matching counter example to it).

The translation from LTL to Buchi automaton is always possible (see [2,3]). The method to do verification with the negation of an LTL property, rather than directly with a property (i.e., to search for counter-examples to a correctness claims, instead of for compliance with a claim) has advantages to the verification procedure, by potentially reducing the computational expense in typical applications - (though of course not in the worst case). The reason is that if a counter-example is infeasible - this can often be shown quickly - after inspecting just an initial fraction of the full system behavior. To demonstrate compliance with a positive claim always forces an exhaustive exploration of all system behavior. The negation method is also due to Wolper. Its implementation in SPIN was suggested by Costas Courcoubetis in 1989.

2. The Semantics of Unless

It was observed by Roberto Manione and Paola that there is one case where the semantics of the new `unless' primitive from Promela2 are different from what might be expected. Briefly, execution of the compound statement: 

	p unless q; r
with `p' and `q' Promela fragments, is begun by executing statements from `p' *provided* that the initial statement from `q' (the `guard' of the escape sequence) remains unexecutable. If the guard of `q' becomes executable before or during the execution of `p', execution switches to `q'. If this does not happen, execution of `p' proceeds normally, and if it terminates control moves to the next statement `r' (i.e., `q' is then skipped).

`p' is called the `main sequence' and `q' is called the `escape sequence' of the unless.

Now consider the following case: 

	{ ...; a; ... } unless { b; ... }
where `a' is a rendez-vous *receive* operation, and `b' is an arbitrary statement that happens to be executable when `a' is reached in the main sequence. The semantics of `unless' suggest that execution of `a' is suppressed in favor of a switch to the escape sequence. However, the semantics of rendez-vous introduce an extra requirement on the execution - that takes precedence. Assume that the matching rendez-vous send-half for `a' is executed in another process, and has become executable at the point in the execution that we are considering (i.e., `a' is reached in the main sequence).
This other process can initiate the rendez-vous (after all, the unless is not defined within that process - so the executability of `b' is immaterial to that process), and the rules of the rendez-vous dictate that if the rendez-vous can be completed it must be completed atomically. Control has now moved to after `a' (forced by the sending process) even though `b' was also executable.

This exception for the normal semantics of an `unless' statement can only be forced through a rendez-vous handshake which is initiated by another process - so it seems harmless. It seems natural to interpret the semantics of `unless' in this way - but other opinions are solicited!

Appendix: Project Description

[Description of a planned verification effort, potentially extending the verification approach from SPIN substantially. by Ratan Nalumasu, ratan@cs.utah.edu]

General:

Our department at the University of Utah obtained ARPA funding for design of a 64 node multiprocessor based on HP's new PA-7100 CPUs. My part of the work is to contribute to the verification of the system. Of course, some parts are too complex, and hence techniques such as SPIN's supertrace will be employed.

The project is called the `Avalanche project.' One of the main objectives of the design is to reduce the memory latency for cache-coherent distributed shared memory and message passing applications. Principal architect is Prof. Al Davis formerly of HP-Labs. HP's interest in this is to see what changes would nee to be made to the CPU. They provide development tools and all the hardware necessary.

Specifics:

Protocols involving all 64 processors are of course not verifiable. We hope to mitigate the state explosion problem by employing on the fly techniques that can exploit known symmetries in the system.
In case of a protocol with N symmetric processes, reductions of up to factorial(N) times may turn out to be feasible. A multi-processor with local cache has two kinds of symmetry: (a) symmetries within the cache, namely the ability to interchange the lines of the cache without affecting the properties satisfied, and (b) symmetries across the system: the ability to interchange two processors without affecting the properties. Both types may be exploited. Finding a normal-form state description that captures and exploits such multiple symmetries, however, is NP-hard in general.

Simple symmetry relations, or conservative approximations of more complex ones, can be exploited automatically by a front-end compiler for the specification language. The specification language can also be extended with special "symmetric datatypes" (called scalar sets in some tools) to express the symmetries. Still other techniques, like homomorphic reductions, can be used to specify larger classes of equivalences, such as those that apply to circular queues. We are thinking of defining a rewrite system that can be used to define both homomorphic reductions and scalar sets in a uniform way.
Any feedback from other verification gurus is welcome!

End of NewsLetter Nr. 3

Gerard J. Holzmann (gerard@research.bell-labs.com)