SPIN NEWS - Nr. 2 - January 15, 1995

Feel free to submit items that could be of interest to other SPIN users for this NewsLetter. Two submitted items are included at the end of this mailing.

Contents of this NewsLetter:

Spin URLs

There is now a URL on the WWW with an index that gives access to previous and current SPIN NewsLetters:

	http://spinroot.com/spin/News/

Purpose and Statistics of the Distribution

Although this is a little unusual, the SPIN software will continue to be distributed only in source form. The reason for doing so is to help in the creation of a more open research environment in formal verification. If one of us publishes the results of a verification experiment, all of us should be able to reproduce it in detail, to consider variations in the algorithms used - while keeping all other factors that may affect the outcome of the experiment constant - and study how the results are affected by such changes.
All of this is only possible if everyone can have access to the sources of at least a few reference implementations of the algorithms that we use.

To maintain this capability, the SPIN software will probably continue to evolve also in the coming years. The criterion for adopting new algorithms into the basic SPIN software is that the algorithms are well-documented and understood, have predictable performance, and can be implemented robustly.

In the 48 months from 1/1991 to 1/1995 there have been 48 updates to the sources. Half of these updates concerned extensions or improvements of existing functionality. The other half concerned the unavoidable bug-fixes. To maintain the integrity of the distribution, a deliberate effort is made to be honest about any bugs in the software that are found, be they large or small. Every change to the software, as well as the reason for the change is listed in the updates files, and will remain available for the lifetime of the software, whatever that may be.

A quick count of the size of the sources, in total lines of source:

	Version 1.0.0	01/01/91    4,444 lines
	Version 1.6.6	12/24/94    5,609 lines
	Version 2.0.4	15/01/95   10,482 lines.
The increase in the switch to Version 2.0 is mostly caused by the new functionality (e.g. structures, d_steps etc.) and the addition of the partial order reduction options.

The current mailing list contains 71 active SPIN users. About 140 different sites have installed the new version of the software in the last two weeks. (As an aside, the names of these sites are no longer logged by our netlib software, to preserve anonymity of ftp accesses to the database.)

Toolchest Returns

SPIN was originally available only through the UNIX systems Toolchest. The phone numbers listed on p.434 of the book, however, stopped working when the Toolchest software left AT&T, first to USL (UNIX Systems Laboratories) and later to Novell - which is a competitor of AT&T.
The Toolchest distribution system has now returned to AT&T, and distribution of SPIN through that channel has become possible again. (No worry: the free netlib distribution will not be affected.)

In two cases you may want to contact the Toolchest distribution people to obtain SPIN sources:

  1. if you have no access to anonymous FTP to retrieve the sources yourself from netlib, and
  2. if you want to use SPIN for commercial purposes.
The Toolchest people will charge a modest fee for providing you with the SPIN sources on a medium of your choice (tape, floppy), and/or a fee for issuing a commercial license. For more information, please contact AT&T's Paul Fillinich (email: attmail!pfillinich).

Some Frequently Asked Questions

1. Compilation

The most frequently made observation about the installation of the version 2 sources was that compilation with non-ansi C compilers can fail if the include file is not present in the default include directories. The particular include file is needed for the compilation of just one procedure with a variable number of arguments (yyerror), but the error serves as a good warning that the compiler that issues it isn't ANSI compatible.

The problem can be avoided by switching to, for instance, the Gnu-C compiler (gcc), which is available on most systems. If gcc is needed to compile the SPIN sources, however, you will also have to twiddle two files from the Xspin directory. The following bourne shell (/bin/sh) script will do the job:

	cd Xspin
	for i in *.tcl
	do
		sed "s/cc -o pan/gcc -o pan/" $i > foo
		mv foo $i
	done

2. Use of printf statements

If you use a printf statement in the PROMELA model, and you leave it in during verification, you get a flurry of output, that is generally hard to interpret. The verifier makes no distinction between the various types of statements that are part of a PROMELA model. If a statement is executable (and a printf statement always is), it gets executed, and it adds transitions to the reachability graph. Of course, the order in which the printfs are executed is determined by the depth-first search traversal of the reachability graph, which does not necessarily make sense if you try to interpret it as being part of a single straight execution. To avoid the clutter, the SPIN documentation recommends to comment out the printfs. If no arguments are used, this can be done as:

	#define printf(x)	skip
The advantage of mapping printf to a skip is that the mapping can be undone when an error trace has been produced, and the printfs can this resume their effect during guided simulations. (The skip is in all contexts equivalent to a printf, and vice versa, so the traces remain the same. The skip in effect serves as a place-holder for the printf, without its side-effects.)

If the printf's use varying numbers of arguments, they can be mapped onto skips with the following little sed-script, that was suggested by Michael Griffioen at NCR/GIS/AT&T, in the Netherlands:

	sed "s/printf.*\)/skip/" spec.in > spec.out
The change can be applied automatically, each time you do a verification run, by adding the following 3 lines to the Xspin source, as also suggested by Michael:
	add_log ""
	catch "eval exec sed s/printf.*\)/skip/ pan.in > _p" err
	catch "eval exec mv _p pan.in" err
add these lines immediately above:
	add_log "spin $a_options pan.in"; update
in Xspin/Validation.tcl

3. Remote referencing

It was noted by Pierre-Alain Etique from Switzerland that since `init' is not a valid proctype name, it is not possible to refer to the state of the init process with a remote reference:

	init[0]@label	/* no good */
The solution is to avoid using init { ... }. SPIN version 2 has a more general mechanism for defining an initial process, for instance as follows:
	active proctype main()
	{
	label:	printf("my instantiation nr is %d\n", _pid)
	}
the prefix `active' makes that an instance of proctype main will run in the initial system state, and its state can be interrogated like any other process (except init) as in:
	main[0]@label
which is true if and only if the process with instantiation number 0 of proctype main is currently in the state named label. (The first process always has instantiation number 0.)

Generating a Display of the Reachability Graph

The output produced by a verbose run of the verifiers produced by SPIN contains enough information to convert it into a complete reachability graph of the system. There is a little awk-script that can be used to extract the required information, and convert it into the proper input formal for `dag' (a tool for drawing directed acyclic graphs). The format can probably be converted relatively easily for other graph drawing tools, such as `dot.' Clearly, this only works for relatively small graphs, say of less than a thousand states, but it may be a useful tool for small tests and demonstrations. An awk-script for the conversion is 44 lines. Send mail if you're interested in obtaining this script, or seeing it included in the next mailing.

Recent Changes

There have been a few small changes in the SPIN 2.0 sources. All changes, from this point on, will be made available both in the spin tar file from the distribution and in a small bourne shell script called `upgrades.' By retrieving and executing only the shell script, you can always bring your sources up to date within minimal hassle. This will work reliably no matter which version of the SPIN sources you have installed (as long as it is version 2.0 from 1/1/95 or later) and will work independent of whether or not you've run a previous version of the upgrades script before.

This policy applies only to the SPIN C-sources (the most bulky part of the distribution, and the part most likely to change once in a while). The (smaller) Xspin sources are updated in-place. Xspin and SPIN, however, each have their own tar-file in the distribution from now on so that you can retrieve them separately.

A short recap of the recent changes follows.

SPIN source changes - none of the changes are critical.

2.0.1 - 7 Jan 95:
	Changed the lexical analyzer to accept redundant
	text at the end of preprocessor directives, that
	some versions of cpp produce.
2.0.2 - 10 Jan 95:
	Two small updates to avoid problems on systems when
	(1) compiling pan.c for runtime profiling on (cc -p)
	(2) when using the new predefined function `enabled()' 
	in combination with partial order reduction.
2.0.3 - 12 Jan 95:
	Added listing of the mappings from label names to the
	state numbers used in the verifier with SPIN option -d.
2.0.4 - 12 Jan 95:
	made the use of a semicolon or arrow after an `else'
	statement optional; preventing complaints about a common
	and easily recoverable syntax error.
Two Xspin twiddles - neither is critical, unless you've had these problems on your system:
*	On some systems the format of the /bin/ps -e appears
	to be very verbose, which can make the execution-tracking
	in Validation.tcl fail (symptom: the run appears to go
	on forever - when in fact it has long terminated).
	To fix this, three lines were changed in Validation.tcl.
*	A small change in Simulation.tcl to redirect more output
	from a run from the log window to the process window, and
	to avoid misinterpreting output from printf statements
	in the model.

Appendix 1 - SPIN Project Description

Submitted by Thierry Cattel, [email protected]

Application:

Modelling and verification of the Harmony multiprocessor real-time kernel

Developed by:

Software Engineering Laboratory, National Research Council of Canada

Formal method/specification language:

PROMELA

Tools:

SPIN

Domain:

Multiprocesseur Real-time Operating System

Period:

July 1, 1993 - August 10, 1994

Size:

Harmony is written in C and assembler 680xx and is about 10000 LOC. The PROMELA models are about 2000 LOC. The effort was one man/year.

Description:

Harmony is a portable real-time multitasking multiprocessor operating system. We used a modeling approach and formalized the models of the system, the scenarios and the properties that are to be checked in PROMELA using the SPIN tool. Several models of the systems were produced with various degrees of abstraction and completeness. The most recent is a tractable one that enables the expression, simulation and verification of any scenario that consists of a bounded number of tasks that may use all the services of the kernel. An exhaustive verification of the intertask communication features of Harmony was carried out by automatic model- checking. It revealed a bug that has been in the system for more than ten years. The first verifications of the dynamic task management primitives lead to the discovery of two other bugs and potential issues of critical races.

Conclusions:

This work shows that it is possible to detect more than deadlocks when using formal methods for the study of a real medium-sized operating system that encompasses complex internal management. The project was rather successful for two reasons. First because of the results obtained (a model of the entire kernel, 3 bugs and about 15 races). Second because it succeeded in convincing my management, who initially was very skeptical, of the usefulness of the approach and of the necessity to integrate it into the ongoing development of future versions of Harmony. A person freshly hired is continuing the project.

Relevant publications:

Cattel, T. Modelling and verification of a multiprocessor realtime OS kernel. Proc. 7th Int. Conf. on Formal Description Techniques. Berne, Switzerland. Oct. 4-7, 1994. Available by FTP at ltidec1.epfl.ch file: /pub/spin/papers/forte94.ps

Contacts:

	Thierry Cattel
	Computer Networking Laboratory
	Laboratoire de Teleinformatique (LTI)
	Swiss Federal Institute of Technology  (EPFL)
	Address: EPFL-DI-LTI, CH-1015 Lausanne, Switzerland
	E-mail:  [email protected]
	Phone:   +41(21) 693 67 76 (Central European Time)
	Fax:     +41(21) 693 66 00
	WWW:     http://ltiwww.epfl.ch/~cattel

	Morven Gentleman
	Software Engineering Laboratory
	National Research Council of Canada
	K1A OR6 Ottawa, Canada
	E-mail : [email protected]
	Phone:   +1 (613) 993 3857
	Fax:     +1 (613) 952 7998
	WWW:     http://wwwsel.iit.nrc.ca

Further remarks:

FTP server ltidec1.epfl.ch /pub/spin/harmony and /pub/xspin+ contain respectively the PROMELA models of Harmony and the Tcl/Tk extension of SPIN for graphical debugging intensively used for analysing the SPIN verification results.

Appendix 2 - Jobhunt

Submitted by Kartik Subramanian, graduate student, Monmouth College

I am on the lookout for a full time position in the Networking area. If you know of a company that is hiring please let me know. Expertise with SPIN verification, ATM networks and willing to work in the areas of protocols and networking. Kartik
Email: [email protected]

End of NewsLetter Nr. 2

Gerard J. Holzmann ([email protected])