Using SPIN
Gerard J. Holzmann
gerard@plan9.bell-labs.com
ABSTRACT
SPIN can be used for proving or disproving logical properties of concurrent systems. To render the proofs, a concurrent system is first modeled in a formal specification language called PROMELA. The language allows one to specify the behaviors of asynchronously executing processes that may interact through synchronous or asynchronous message passing, or through direct access to shared variables.
System models specified in this way can be verified for both safety and liveness properties. The specification of general properties in linear time temporal logic is also supported.
The first part of this manual discusses the basic features of the specification language PROMELA. The second part describes the verifier SPIN.
1. The Language PROMELA
PROMELA is short for Protocol Meta Language [Ho91]. PROMELA is a modeling language, not a programming language. A formal model differs in two essential ways from an implementation. First, a model is meant to be an abstraction of a design that contains only those aspects of the design that are directly relevant to the properties one is interested in proving. Second, a formal model must contain things that are typically not part of an implementation, such as worst-case assumptions about the behavior of the environment that may interact with the system being studied, and a formal statement of relevant correctness properties. It is possible to mechanically extract abstract models from implementation level code, as discussed, for instance in [HS99].
Verification with SPIN is often performed in a series of steps, with the construction of increasingly detailed models. Each model can be verified under different types of assumptions about the environment and for different types of correctness properties. If a property is not valid for the given assumptions about system behavior, the verifier can produce a counter-example that demonstrates how the property may be violated. If a property is valid, it may be possible to simplify the model based on that fact, and prove still other properties.
Section 1.1 covers the basic building blocks of the language. Section 1.2 introduces the control flow structures. Section 1.3 explains how correctness properties are specified. Section 1.4 concludes the first part with a discussion of special predefined variables and functions that can be used to express some correctness properties.
Up to date manual pages for SPIN can always be found online at: http://cm.bell-labs.com/cm/cs/what/spin/Man/
1.1. Basics
A PROMELA model can contain three different types of objects:
∙ Processes (section 1.1.1),
∙ Variables (section 1.1.2),
∙ Message channels (section 1.1.3).
All processes are global objects. For obvious reasons, a PROMELA model must contain at least one process to be meaningful. Since SPIN is specifically meant to prove properties of concurrent systems, a model typically contains more than one process.
Message channels and variables, the two basic types of data objects, can be declared with either a global scope or a local scope. A data object with global scope can be referred to by all processes. A data object with a local scope can be referred to by just a single process: the process that declares and instantiates the object. As usual, all objects must be declared in the specification before they are referenced.
1.1.1. Processes
Here is a simple process that does nothing except print a line of text:
init {
printf("it works\n")
}
There are a few things to note. Init is a predefined keyword from the language. It can be used to declare and instantiate a single initial process in the model. (It is comparable to the main procedure of a C program.) The init process does not take arguments, but it can start up (instantiate) other processes that do. Printf is one of a few built-in procedures in the language. It behaves the same as the C version. Note, finally, that no semicolon follows the single printf statement in the above example. In PROMELA, semicolons are used as statement separators, not statement terminators. (The SPIN parser, however, is lenient on this issue.)
Any process can start new processes by using another built-in procedure called run. For example,
proctype you_run(byte x)
{
printf("my x is: %d\n", x)
}
init {
run you_run(1);
run you_run(2)
}
The word proctype is again a keyword that introduces the declaration of a new type of process. In this case, we have named that type you_run and declared that all instantiations of processes of this type will take one argument: a data object of type byte, that can be referred to within this process by the name x. Instances of a proctype can be created with the predefined procedure run, as shown in the example. When the run statement completes, a copy of the process has been started, and all its arguments have been initialized with the arguments provided. The process may, but need not, have performed any statement executions at this point. It is now part of the concurrent system, and its execution can be interleaved arbitrarily with those of the other, already executing processes. (More about the semantics of execution follows shortly.)
In many cases, we are only interested in creating a single instance of each process type that is declared, and the processes require no arguments. We can define this by prefixing the keyword proctype from the process declaration with another keyword: active. Instances of all active proctypes are created when the system itself is initialized. We could, for instance, have avoided the use of init by declaring the corresponding process in the last example as follows:
active proctype main() {
run you_run(1);
run you_run(2)
}
Note that there are no parameters to instantiate in this case. Had they been declared, they would default to a zero value, just like all other data objects that are not explicitly instantiated.
Multiple copies of a process type can also be created in this way. For example:
active [4] proctype try_me() {
printf("hi, i am process %d\n", _pid)
}
creates four processes. A predefined variable _pid is assigned to each running process, and holds its unique process instantiation number. In some cases, this number is needed when a reference has to be made to a specific process.
Summarizing: process behavior is declared in proctype definitions, and it is instantiated with either run statements or with the prefix active. Within a proctype declaration, statements are separated (not terminated) by semicolons. As we shall see in examples that follow, instead of the semicolon, one can also use the alternative separator -> (arrow), wherever that may help to clarify the structure of a PROMELA model.
Semantics of Execution
In PROMELA there is no difference between a condition or expression and a statement. Fundamental to the semantics of the language is the notion of the executability of statements. Statements are either executable or blocked. Executability is the basic means of enforcing synchronization between the processes in a distributed system. A process can wait for an event to happen by waiting for a statement to become executable. For instance, instead of writing a busy wait loop:
while (a != b) /* not valid Promela syntax */
skip; /* wait for a==b */
...
we achieve the same effect in PROMELA with the statement
(a == b);
...
Often we indicate that the continuation of an execution is conditional on the truth of some expression by using the alternate statement separator:
(a == b) -> ...
Assignments and printf statements are always executable in PROMELA. A condition, however, can only be executed (passed) when it holds. If the condition does not hold, execution blocks until it does. There are similar rules for determining the executability of all other primitive and compound statements in the language. The semantics of each statement is defined in terms of rules for executability and effect. The rules for executability set a precondition on the state of the system in which a statement can be executed. The effect defines how a statement will alter a system state when executed.
PROMELA assumes that all individual statements are executed atomically: that is, they model the smallest meaningful entities of execution in the system being studied. This means that PROMELA defines the standard asynchronous interleaving model of execution, where a supposed scheduler is free at each point in the execution to select any one of the processes to proceed by executing a single primitive statement. Synchronization constraints can be used to influence the interleaving patterns. It is the purpose of a concurrent system’s design to constrain those patterns in such a way that no correctness requirements can be violated, and all service requirements are met. It is the purpose of the verifier either to find counter-examples to a designer’s claim that this goal has been met, or to demonstrate that the claim is indeed valid.
1.1.2. Variables
The table summarizes the five basic data types used in PROMELA. Bit and bool are synonyms for a single bit of information. The first three types can store only unsigned quantities. The last two can hold either positive or negative values. The precise value ranges of variables of types short and int is implementation dependent, and corresponds to those of the same types in C programs that are compiled for the same hardware. The values given in the table are most common.
The following example program declares a array of two elements of type bool and a scalar variable turn of the same type. Note that the example relies on the fact that _pid is either 0 or 1 here.
/*
* Peterson’s algorithm for enforcing
* mutual exclusion between two processes
* competing for access to a critical section
*/
bool turn, want[2];
active [2] proctype user()
{
again:
want[_pid] = 1; turn = _pid;
/* wait until this condition holds: */
(want[1 - _pid] == 0 || turn == 1 - _pid);
/* enter */
critical: skip;
/* leave */
want[_pid] = 0;
goto again
}
In the above case, all variables are initialized to zero. The general syntax for declaring and instantiating a variable, respectively for scalar and array variables, is:
type name = expression;
type name[constant] = expression
In the latter case, all elements of the array are initialized to the value of the expression. A missing initializer fields defaults to the value zero. As usual, multiple variables of the same type can be grouped behind a single type name, as in:
byte a, b[3], c = 4
In this example, the variable c is initialized to the value 4; variable a and the elements of array b are all initialized to zero.
Variables can also be declared as structures. For example:
typedef Field {
short f = 3;
byte g
};
typedef Msg {
byte a[3];
int fld1;
Field fld2;
chan p[3];
bit b
};
Msg foo;
introduces two user-defined data types, the first named Field and the second named Msg. A single variable named foo of type Msg is declared. All fields of foo that are not explicitly initialized (in the example, all fields except foo.fld2.f) are initialized to zero. References to the elements of a structure are written as:
foo.a[2] = foo.fld2.f + 12
A variable of a user-defined type can be passed as a single argument to a new process in run statements. For instance,
proctype me(Msg z) {
z.a[2] = 12
}
init {
Msg foo;
run me(foo)
}
Note that even though PROMELA supports only one-dimensional arrays, a two-dimensional array can be created indirectly with user-defined structures, for instance as follows:
typedef Array {
byte el[4]
};
Array a[4];
This creates a data structure of 16 elements that can be referenced, for instance, as a[i].el[j].
As in C, the indices of an array of N elements range from 0 to N-1.
Expressions
Expressions must be side-effect free in PROMELA. Specifically, this means that an expression cannot contain assignments, or send and receive operations (see section 1.1.3).
c = c + 1; c = c - 1
and
c++; c--
are assignments in PROMELA, with the same effects. But, unlike in C,
b = c++
is not a valid assignment, because the right-hand side operand is not a valid expression in PROMELA (it is not side-effect free).
It is also possible to write a side-effect free conditional expression, with the following syntax:
(expr1 -> expr2 : expr3)
The parentheses around the conditional expression are required to avoid misinterpretation of the arrow. The example expression has the value of expr2 when expr1 evaluates to a non-zero value, and the value of expr3 otherwise.
In assignments like
variable = expression
the values of all operands used inside the expression are first cast to signed integers before the operands are applied. After the evaluation of the expression completes, the value produced is cast to the type of the target variable before the assignment takes place.
1.1.3. Message Channels
Message channels are used to model the transfer of data between processes. They are declared either locally or globally, for instance as follows:
chan qname = [16] of { short, byte }
The keyword chan introduces a channel declaration. In this case, the channel is named qname, and it is declared to be capable of storing up to 16 messages. Each message stored in the channel is declared here to consist of two fields: one of type short and one of type byte. The fields of a message can be any one of the basic types bit, bool, byte, short, int, and chan, or any user-defined type. Message fields cannot be declared as arrays.
A message field of type chan can be used to pass a channel identifier through a channel from one process to another.
The statement
qname!expr1,expr2
sends the values of expressions expr1 and expr2 to the channel that we just created. It appends the message field created from the values of the two expressions (and cast to the appropriate types of the message fields declared for qname) to the tail of the message buffer of 16 slots that belongs to channel qname. By default the send statement is only executable if the target channel is non-full. (This default semantics can be changed in the verifier into one where the send statement is always executable, but the message will be lost when an attempt is made to append it to a full channel.)
The statement
qname?var1,var2
retrieves a message from the head of the same buffer, and stores the two expressions in variables var1 and var2.
The receive statement is executable only if the source channel is non-empty.
If more parameters are sent per message than were declared for the message channel, the redundant parameters are lost. If fewer parameters are sent than declared, the value of the remaining parameters is undefined. Similarly, if the receive operation tries to retrieve more parameters than available, the value of the extra parameters is undefined; if it receives fewer than the number of parameters sent, the extra information is lost.
An alternative, and equivalent, notation for the send and receive operations is to structure the message fields with parentheses, as follows:
qname!expr1(expr2,expr3)
qname?var1(var2,var3)
In the above case, we assume that qname was declared to hold messages consisting of three fields.
Some or all of the arguments of the receive operation can be given as constants instead of as variables:
qname?cons1,var2,cons2
In this case, an extra condition on the executability of the receive operation is that the value of all message fields specified as constants match the value of the corresponding fields in the message that is to be received.
Here is an example that uses some of the mechanisms introduced so far.
proctype A(chan q1)
{ chan q2;
q1?q2;
q2!123
}
proctype B(chan qforb)
{ int x;
qforb?x;
printf("x = %d\n", x)
}
init {
chan qname = [1] of { chan };
chan qforb = [1] of { int };
run A(qname);
run B(qforb);
qname!qforb
}
The value printed by the process of type B will be 123.
A predefined function len(qname) returns the number of messages currently stored in channel qname. Two shorthands for the most common uses of this function are empty(qname) and full(qname), with the obvious connotations.
Since all expressions must be side-effect free, it is not valid to say:
(qname?var == 0)
or
(a > b && qname!123)
We could rewrite the second example (using an atomic sequence, as explained further in section 1.2.1):
atomic { (a > b && !full(qname)) -> qname!123 }
The meaning of the first example is ambiguous. It could mean that we want the condition to be true if the receive operation is unexecutable. In that case, we can rewrite it without side-effects as:
empty(qname)
It could also mean that we want the condition to be true when the channel does contain a message with value zero. We can specify that as follows:
atomic { qname?[0] -> qname?var }
The first statement of this atomic sequence is an expression without side-effects that evaluates to a non-zero value only if the receive operation
qname?0
would have been executable at that point (i.e., channel qname contains at least one message and the oldest message stored consists of one message field equal to zero). Any receive statement can be turned into a side-effect free expression by placing square brackets around the list of all message parameters. The channel contents remain undisturbed by the evaluation of such expressions.
Note carefully, however, that in non-atomic sequences of two statements such as
!full(qname) -> qname!msgtype
and
qname?[msgtype] -> qname?msgtype
the second statement is not necessarily executable after the first one has been executed. There may be race conditions when access to the channels is shared between several processes. Another process can send a message to the channel just after this process determined that it was not full, or another process can steal away the message just after our process determined its presence.
Two other types of send and receive statements are used less frequently: sorted send and random receive. A sorted send operation is written with two, instead of one, exclamation marks, as follows:
qname!!msg
A sorted send operation will insert a message into the channel’s buffer in numerical order, instead of in FIFO order. The channel contents are scanned from the first message towards the last, and the message is inserted immediately before the first message that follows it in numerical order. To determine the numerical order, all message fields are taken into account.
The logical counterpart of the sorted send operation is the random receive. It is written with two, instead of one, question marks:
qname??msg
A random receive operation is executable if it is executable for any message that is currently buffered in a message channel (instead of only for the first message in the channel). Normal send and receive operations can freely be combined with sorted send and random receive operations.
Rendezvous Communication
So far we have talked about asynchronous communication between processes via message channels, declared in statements such as
chan qname = [N] of { byte }
where N is a positive constant that defines the buffer size. A logical extension is to allow for the declaration
chan port = [0] of { byte }
to define a rendezvous port. The channel size is zero, that is, the channel port can pass, but cannot store, messages. Message interactions via such rendezvous ports are by definition synchronous. Consider the following example:
#define msgtype 33
chan name = [0] of { byte, byte };
active proctype A()
{ name!msgtype(124);
name!msgtype(121)
}
active proctype B()
{ byte state;
name?msgtype(state)
}
Channel name is a global rendezvous port. The two processes will synchronously execute their first statement: a handshake on message msgtype and a transfer of the value 124 to local variable state. The second statement in process A will be unexecutable, because there is no matching receive operation in process B.
If the channel name is defined with a non-zero buffer capacity, the behavior is different. If the buffer size is at least 2, the process of type A can complete its execution, before its peer even starts. If the buffer size is 1, the sequence of events is as follows. The process of type A can complete its first send action, but it blocks on the second, because the channel is now filled to capacity. The process of type B can then retrieve the first message and complete. At this point A becomes executable again and completes, leaving its last message as a residual in the channel.
Rendezvous communication is binary: only two processes, a sender and a receiver, can be synchronized in a rendezvous handshake.
As the example shows, symbolic constants can be defined with preprocessor macros using #define. The source text of a PROMELA model is translated by the standard C preprocessor. The disadvantage of defining symbolic names in this way is, however, that the PROMELA parser will only see the expanded text, and cannot refer to the symbolic names themselves. To prevent that, PROMELA also supports another way to define symbolic names, which are preserved in error reports. For instance, by including the declaration
mtype = { ack, msg, error, data };
at the top of a PROMELA model, the names provided between the curly braces are equivalent to integers of type byte, but known by their symbolic names to the SPIN parser and the verifiers it generates. The constant values assigned start at 1, and count up. There can be only one mtype declaration per model.
1.2. Control Flow
So far, we have seen only some of the basic statements of PROMELA, and the way in which they can be combined to model process behaviors. The five types of statements we have mentioned are: printf, assignment, condition, send, and receive.
The pseudo-statement skip is syntactically and semantically equivalent to the condition (1) (i.e., to true), and is in fact quietly replaced with this expression by the lexical analyzer of SPIN.
There are also five types of compound statements.
∙ Atomic sequences (section 1.2.1),
∙ Deterministic steps (section 1.2.2),
∙ Selections (section 1.2.3),
∙ Repetitions (section 1.2.4),
∙ Escape sequences (section 1.2.5).
1.2.1. Atomic Sequences
The simplest compound statement is the atomic sequence:
atomic { /* swap the values of a and b */
tmp = b;
b = a;
a = tmp
}
In the example, the values of two variables a and b are swapped in a sequence of statement executions that is defined to be uninterruptable. That is, in the interleaving of process executions, no other process can execute statements from the moment that the first statement of this sequence begins to execute until the last one has completed.
It is often useful to use atomic sequences to start a series of processes in such a way that none of them can start executing statements until all of them have been initialized:
init {
atomic {
run A(1,2);
run B(2,3);
run C(3,1)
}
}
Atomic sequences may be non-deterministic. If any statement inside an atomic sequence is found to be unexecutable, however, the atomic chain is broken, and another process can take over control. When the blocking statement becomes executable later, control can non-deterministically return to the process, and the atomic execution of the sequence resumes as if it had not been interrupted.
1.2.2. Deterministic Steps
Another way to define an indivisible sequence of actions is to use the d_step statement. In the above case, for instance, we could also have written:
d_step { /* swap the values of a and b */
tmp = b;
b = a;
a = tmp
}
The difference between a d_step sequence and an atomic sequence are:
∙ A d_step sequence must be completely deterministic. (If non-determinism is nonetheless encountered, it is always resolved in a fixed and deterministic way: i.e., the first true guard in selection or repetition structures is always selected.)
∙ No goto jumps into or out of a d_step sequence are permitted.
∙ The execution of a d_step sequence cannot be interrupted when a blocking statement is encountered. It is an error if any statement other than the first one in a d_step sequence is found to be unexecutable.
∙ A d_step sequence is executed as one single statement. In a way, it is a mechanism for adding new types of statements to the language.
None of the items listed above apply to atomic sequences. This means that the keyword d_step can always be replaced with the keyword atomic, but the reverse is not true. (The main, perhaps the only, reason for using d_step sequences is to improve the efficiency of verifications.)
1.2.3. Selection Structures
A more interesting construct is the selection structure. Using the relative values of two variables a and b to choose between two options, for instance, we can write:
if
:: (a != b) -> option1
:: (a == b) -> option2
fi
The selection structure above contains two execution sequences, each preceded by a double colon. Only one sequence from the list will be executed. A sequence can be selected only if its first statement is executable. The first statement is therefore called a guard.
In the above example the guards are mutually exclusive, but they need not be. If more than one guard is executable, one of the corresponding sequences is selected nondeterministically. If all guards are unexecutable the process will block until at least one of them can be selected. There is no restriction on the type of statements that can be used as a guard: it may include sends or receives, assignments, printf, skip, etc. The rules of executability determine in each case what the semantics of the complete selection structure will be. The following example, for instance, uses receive statements as guards in a selection.
mtype = { a, b };
chan ch = [1] of { byte };
active proctype A()
{ ch!a
}
active proctype B()
{ ch!b
}
active proctype C()
{ if
:: ch?a
:: ch?b
fi
}
The example defines three processes and one channel. The first option in the selection structure of the process of type C is executable if the channel contains a message named a, where a is a symbolic constant defined in the mtype declaration at the start of the program. The second option is executable if it contains a message b, where, similarly, b is a symbolic constant. Which message will be available depends on the unknown relative speeds of the processes.
A process of the following type will either increment or decrement the value of variable count once.
byte count;
active proctype counter()
{
if
:: count++
:: count--
fi
}
Assignments are always executable, so the choice made here is truly a non-deterministic one that is independent of the initial value of the variable (zero in this case).
1.2.4. Repetition Structures
We can modify the above program as follows, to obtain a cyclic program that randomly changes the value of the variable up or down, by replacing the selection structure with a repetition.
byte count;
active proctype counter()
{
do
:: count++
:: count--
:: (count == 0) -> break
od
}
Only one option can be selected for execution at a time. After the option completes, the execution of the structure is repeated. The normal way to terminate the repetition structure is with a break statement. In the example, the loop can be broken only when the count reaches zero. Note, however, that it need not terminate since the other two options remain executable. To force termination we could modify the program as follows.
active proctype counter()
{
do
:: (count != 0) ->
if
:: count++
:: count--
fi
:: (count == 0) -> break
od
}
A special type of statement that is useful in selection and repetition structures is the else statement. An else statement becomes executable only if no other statement within the same process, at the same control-flow point, is executable. We could try to use it in two places in the above example:
active proctype counter()
{
do
:: (count != 0) ->
if
:: count++
:: count--
:: else
fi
:: else -> break
od
}
The first else, inside the nested selection structure, can never become executable though, and is therefore redundant (both alternative guards of the selection are assignments, which are always executable). The second usage of the else, however, becomes executable exactly when !(count != 0) or (count == 0), and is therefore equivalent to the latter to break from the loop.
There is also an alternative way to exit the do-loop, without using a break statement: the infamous goto. This is illustrated in the following implementation of Euclid’s algorithm for finding the greatest common divisor of two non-zero, positive numbers:
proctype Euclid(int x, y)
{
do
:: (x > y) -> x = x - y
:: (x < y) -> y = y - x
:: (x == y) -> goto done
od;
done:
skip
}
init { run Euclid(36, 12) }
The goto in this example jumps to a label named done. Since a label can only appear before a statement, we have added the dummy statement skip. Like a skip, a goto statement is always executable and has no other effect than to change the control-flow point of the process that executes it.
As a final example, consider the following implementation of a Dijkstra semaphore, which is implemented with the help of a synchronous channel.
#define p 0
#define v 1
chan sema = [0] of { bit };
active proctype Dijkstra()
{ byte count = 1;
do
:: (count == 1) ->
sema!p; count = 0
:: (count == 0) ->
sema?v; count = 1
od
}
active [3] proctype user()
{ do
:: sema?p;
/* critical section */
sema!v;
/* non-critical section */
od
}
The semaphore guarantees that only one of the three user processes can enter its