Subversion Repositories planix.SVN

.HTML "Using SPIN

.\" runoff as:

.\" eqn file | tbl | troff -ms

.\"

.ds P \\s-1PROMELA\\s0

.ds V \\s-1SPIN\\s0

.ds C pcc

.\" .tr -\(hy

.EQ

delim $#

.EN

.TL

Using \*V

.AU

Gerard J. Holzmann

gerard@plan9.bell-labs.com

.AB

\*V 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 \*P.

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.

.LP

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.

.LP

The first part of this manual

discusses the basic features of the specification language \*P.

The second part describes the verifier \*V.

.AE

.NH 1

The Language \*P

.LP

\*P is short for Protocol Meta Language [Ho91].

\*P is a \f2modeling\f1 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].

.LP

Verification with \*V 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.

.LP

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.

.LP

Up to date manual pages for \*V can always be found online at:

.CW

http://cm.bell-labs.com/cm/cs/what/spin/Man/

.R

.NH 2

Basics

.LP

A \*P model can contain three different types of objects:

.IP

.RS

\(bu Processes (section 1.1.1),

.br

\(bu Variables (section 1.1.2),

.br

\(bu Message channels (section 1.1.3).

.RE

.LP

All processes are global objects.

For obvious reasons, a \*P model must contain at least one

process to be meaningful.

Since \*V is specifically meant to prove properties of

concurrent systems, a model typically contains more than

one process.

.LP

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.

.NH 3

Processes

.LP

Here is a simple process that does nothing except print

a line of text:

.P1

init {

	printf("it works\en")

}

.P2

There are a few things to note.

.CW 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

.CW main

procedure of a C program.)

The

.CW init

process does not take arguments, but it can

start up (instantiate) other processes that do.

.CW 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

.CW printf

statement in the above example.

In \*P, semicolons are used as statement separators,

not statement terminators.  (The \*V parser, however, is

lenient on this issue.)

.LP

Any process can start new processes by using another

built-in procedure called

.CW run .

For example,

.P1

proctype you_run(byte x)

{

	printf("my x is: %d\en", x)

}

.P2

.P1

init {

	run you_run(1);

	run you_run(2)

}

.P2

The word

.CW proctype

is again a keyword that introduces the declaration

of a new type of process.

In this case, we have named that type

.CW you_run

and declared that all instantiations of processes

of this type will take one argument:  a data object

of type

.CW byte ,

that can be referred to within this process by the name

.CW x .

Instances of a

.CW proctype

can be created with the predefined procedure

.CW run ,

as shown in the example.

When the

.CW 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.)

.LP

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

.CW proctype

from the process declaration with another keyword:

.CW active .

Instances of all active proctypes are created when the

system itself is initialized.

We could, for instance, have avoided the use of

.CW init

by declaring the corresponding process in the last example

as follows:

.P1

active proctype main() {

	run you_run(1);

	run you_run(2)

}

.P2

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.

.LP

Multiple copies of a process type can also be created in

this way.  For example:

.P1

active [4] proctype try_me() {

	printf("hi, i am process %d\en", _pid)

}

.P2

creates four processes.

A predefined variable

.CW _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.

.LP

Summarizing:  process behavior is declared in

.CW proctype

definitions, and it is instantiated with either

.CW run

statements or with the prefix

.CW 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

.CW "->"

(arrow), wherever that may help to clarify the structure

of a \*P model.

.SH

Semantics of Execution

.LP

In \*P there is no difference between a condition or

expression and a statement.

Fundamental to the semantics of the language is the

notion of the \f2executability\f1 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:

.P1

while (a != b)	/* not valid Promela syntax */

	skip;	/* wait for a==b */

\&...

.P2

we achieve the same effect in \*P with the statement

.P1

(a == b);

\&...

.P2

Often we indicate that the continuation of an execution

is conditional on the truth of some expression by using

the alternate statement separator:

.P1

(a == b) -> \&...

.P2

Assignments and

.CW printf

statements are always executable in \*P.

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.

.LP

\*P 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 \*P 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.

.NH 3

Variables

.LP

The table summarizes the five basic data types used in \*P.

.CW Bit

and

.CW 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

.CW short

and

.CW 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.

.KS

.TS

center;

l l

lw(10) lw(12).

=

\f3Type	Range\f1

_

bit   	0..1

bool   	0..1

byte   	0..255

short	   $-2 sup 15# .. $2 sup 15 -1#

int	   $-2 sup 31# .. $2 sup 31 -1#

_

.TE

.KE

.LP

The following example program declares a array of

two elements of type

.CW bool

and a scalar variable

.CW turn

of the same type.

Note that the example relies on the fact that

.CW _pid

is either 0 or 1 here.

.MT _sec5critical

.P1

/*

 * 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

}

.P2

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:

.P1

type name = expression;

type name[constant] = expression

.P2

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:

.P1

byte a, b[3], c = 4

.P2

In this example, the variable

.CW c

is initialized to the value 4; variable

.CW a

and the elements of array

.CW b

are all initialized to zero.

.LP

Variables can also be declared as structures.

For example:

.P1

typedef Field {

        short f = 3;

        byte  g

};

typedef Msg {

        byte a[3];

        int fld1;

        Field fld2;

        chan p[3];

        bit b

};

Msg foo;

.P2

introduces two user-defined data types, the first named

.CW Field

and the second named

.CW Msg .

A single variable named

.CW foo

of type

.CW Msg

is declared.

All fields of

.CW foo

that are not explicitly initialized (in the example, all fields except

.CW foo.fld2.f )

are initialized to zero.

References to the elements of a structure are written as:

.P1

foo.a[2] = foo.fld2.f + 12

.P2

A variable of a user-defined type can be passed as a single

argument to a new process in

.CW run

statements.

For instance,

.P1

proctype me(Msg z) {

	z.a[2] = 12

}

init {

	Msg foo;

	run me(foo)

}

.P2

.LP

Note that even though \*P supports only one-dimensional arrays,

a two-dimensional array can be created indirectly with user-defined

structures, for instance as follows:

.P1

typedef Array {

	byte el[4]

};

Array a[4];

.P2

This creates a data structure of 16 elements that can be

referenced, for instance, as

.CW a[i].el[j] .

.LP

As in C, the indices of an array of

.CW N

elements range from 0 to

.CW N-1 .

.SH

Expressions

.LP

Expressions must be side-effect free in \*P.

Specifically, this means that an expression cannot

contain assignments, or send and receive operations (see section 1.1.3).

.P1

c = c + 1; c = c - 1

.P2

and

.P1

c++; c--

.P2

are assignments in \*P, with the same effects.

But, unlike in C,

.P1

b = c++

.P2

is not a valid assignment, because the right-hand side

operand is not a valid expression in \*P (it is not side-effect free).

.LP

It is also possible to write a side-effect free conditional

expression, with the following syntax:

.P1

(expr1 -> expr2 : expr3)

.P2

The parentheses around the conditional expression are required to

avoid misinterpretation of the arrow.

The example expression has the value of \f(CWexpr2\f1 when \f(CWexpr1\f1

evaluates to a non-zero value, and the value of \f(CWexpr3\f1 otherwise.

.LP

In assignments like

.P1

variable = expression

.P2

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.

.NH 3

Message Channels

.LP

Message channels are used to model the transfer of data

between processes.

They are declared either locally or globally,

for instance as follows:

.P1

chan qname = [16] of { short, byte }

.P2

The keyword

.CW chan

introduces a channel declaration.

In this case, the channel is named

.CW 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

.CW short

and one of type

.CW byte .

The fields of a message can be any one of the basic types

.CW bit ,

.CW bool ,

.CW byte ,

.CW short ,

.CW int ,

and

.CW chan ,

or any user-defined type.

Message fields cannot be declared as arrays.

.LP

A message field of type

.CW chan

can be used to pass a channel identifier

through a channel from one process to another.

.LP

The statement

.P1

qname!expr1,expr2

.P2

sends the values of expressions

.CW expr1

and

.CW 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

.CW qname )

to the tail of the message buffer of 16 slots that belongs

to channel

.CW 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.)

.LP

The statement

.P1

qname?var1,var2

.P2

retrieves a message from the head of the same buffer,

and stores the two expressions in variables

.CW var1

and

.CW var2 .

.LP

The receive statement is executable only if the source channel

is non-empty.

.LP

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.

.LP

An alternative, and equivalent, notation for the

send and receive operations is to structure the

message fields with parentheses, as follows:

.P1

qname!expr1(expr2,expr3)

qname?var1(var2,var3)

.P2

In the above case, we assume that

.CW qname

was declared to hold messages consisting of three fields.

.PP

Some or all of the arguments of the receive operation

can be given as constants instead of as variables:

.P1

qname?cons1,var2,cons2

.P2

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.

.LP

Here is an example that uses some of the mechanisms introduced

so far.

.P1

proctype A(chan q1)

{	chan q2;

	q1?q2;

	q2!123

}

.P2

.P1

proctype B(chan qforb)

{	int x;

	qforb?x;

	printf("x = %d\en", x)

}

.P2

.P1

init {

	chan qname = [1] of { chan };

	chan qforb = [1] of { int };

	run A(qname);

	run B(qforb);

	qname!qforb

}

.P2

The value printed by the process of type

.CW B

will be

.CW 123 .

.LP

A predefined function

.CW len(qname)

returns the number of messages currently

stored in channel

.CW qname .

Two shorthands for the most common uses of this

function are

.CW empty(qname)

and

.CW full(qname) ,

with the obvious connotations.

.LP

Since all expressions must be side-effect free,

it is not valid to say:

.P1

(qname?var == 0)

.P2

or

.P1

(a > b && qname!123)

.P2

We could rewrite the second example (using an atomic sequence,

as explained further in section 1.2.1):

.P1

atomic { (a > b && !full(qname)) -> qname!123 }

.P2

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:

.P1

empty(qname)

.P2

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:

.P1

atomic { qname?[0] -> qname?var }

.P2

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

.P1

qname?0

.P2

would have been executable at that

point (i.e., channel

.CW 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.

.LP

Note carefully, however, that in non-atomic sequences

of two statements such as

.P1

!full(qname) -> qname!msgtype

.P2

and

.P1

qname?[msgtype] -> qname?msgtype

.P2

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.

.LP

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:

.P1

qname!!msg

.P2

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.

.LP

The logical counterpart of the sorted send operation

is the random receive.

It is written with two, instead of one, question marks:

.P1

qname??msg

.P2

A random receive operation is executable if it is executable for \f2any\f1

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.

.SH

Rendezvous Communication

.LP

So far we have talked about asynchronous communication between processes

via message channels, declared in statements such as

.P1

chan qname = [N] of { byte }

.P2

where

.CW N

is a positive constant that defines the buffer size.

A logical extension is to allow for the declaration

.P1

chan port = [0] of { byte }

.P2

to define a rendezvous port.

The channel size is zero, that is, the channel

.CW port

can pass, but cannot store, messages.

Message interactions via such rendezvous ports are

by definition synchronous.

Consider the following example:

.P1

#define msgtype 33

chan name = [0] of { byte, byte };

active proctype A()

{	name!msgtype(124);

	name!msgtype(121)

}

.P2

.P1

active proctype B()

{	byte state;

	name?msgtype(state)

}

.P2

Channel

.CW name

is a global rendezvous port.

The two processes will synchronously execute their first statement:

a handshake on message

.CW msgtype

and a transfer of the value 124 to local variable

.CW state .

The second statement in process

.CW A

will be unexecutable,

because there is no matching receive operation in process

.CW B .

.LP

If the channel

.CW 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

.CW 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

.CW 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

.CW B 

can then retrieve the first message and complete.

At this point

.CW A

becomes executable again and completes,

leaving its last message as a residual in the channel.

.LP

Rendezvous communication is binary: only two processes,

a sender and a receiver, can be synchronized in a

rendezvous handshake.

.LP

As the example shows, symbolic constants can be defined

with preprocessor macros using

.CW #define .

The source text of a \*P model is translated by the standard

C preprocessor.

The disadvantage of defining symbolic names in this way is,

however, that the \*P parser will only see the expanded text,

and cannot refer to the symbolic names themselves.

To prevent that, \*P also supports another way to define

symbolic names, which are preserved in error reports.

For instance, by including the declaration

.P1

mtype = { ack, msg, error, data };

.P2

at the top of a \*P model, the names provided between the

curly braces are equivalent to integers of type

.CW byte ,

but known by their symbolic names to the \*V parser and the

verifiers it generates.

The constant values assigned start at 1, and count up.

There can be only one

.CW mtype

declaration per model.

.NH 2

Control Flow

.LP

So far, we have seen only some of the basic statements

of \*P, and the way in which they can be combined to

model process behaviors.

The five types of statements we have mentioned are:

.CW printf ,

.CW assignment ,

.CW condition ,

.CW send ,

and

.CW receive .

.LP

The pseudo-statement

.CW skip

is syntactically and semantically equivalent to the

condition

.CW (1)

(i.e., to true), and is in fact quietly replaced with this

expression by the lexical analyzer of \*V.

.LP

There are also five types of compound statements.

.IP

.RS

\(bu

Atomic sequences (section 1.2.1),

.br

\(bu

Deterministic steps (section 1.2.2),

.br

\(bu

Selections (section 1.2.3),

.br

\(bu

Repetitions (section 1.2.4),

.br

\(bu

Escape sequences (section 1.2.5).

.RE

.LP

.NH 3

Atomic Sequences

.LP

The simplest compound statement is the

.CW atomic

sequence:

.P1

atomic {	/* swap the values of a and b */

	tmp = b;

	b = a;

	a = tmp

}

.P2

In the example, the values of two variables

.CW a

and

.CW 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.

.LP

It is often useful to use

.CW 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:

.P1

init {

	atomic {

		run A(1,2);

		run B(2,3);

		run C(3,1)

	}

}

.P2

.CW Atomic

sequences may be non-deterministic.

If any statement inside an

.CW 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.

.NH 3

Deterministic Steps

.LP

Another way to define an indivisible sequence of actions

is to use the

.CW d_step

statement.

In the above case, for instance, we could also have written:

.P1

d_step {	/* swap the values of a and b */

	tmp = b;

	b = a;

	a = tmp

}

.P2

The difference between a

.CW d_step

sequence

and an

.CW atomic

sequence are:

.IP \(bu

A

.CW 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.)

.IP \(bu

No

.CW goto

jumps into or out of a

.CW d_step

sequence are permitted.

.IP \(bu

The execution of a

.CW 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

.CW d_step

sequence is found to be unexecutable.

.IP \(bu

A

.CW 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.

.LP

None of the items listed above apply to

.CW atomic

sequences.

This means that the keyword

.CW d_step

can always be replaced with the keyword

.CW atomic ,

but the reverse is not true.

(The main, perhaps the only, reason for using

.CW d_step

sequences is to improve the efficiency of

verifications.)

.NH 3

Selection Structures

.LP

A more interesting construct is the selection structure.

Using the relative values of two variables

.CW a

and

.CW b

to choose between two options, for instance, we can write:

.P1

if

:: (a != b) -> option1