Concise Promela Reference

Rob Gerth, Eindhoven University

This reference is based on information and text scattered through the various Spin version 2.9.7 documentation files. Comments, suggestion etc. to robg@win.tue.nl

Document date: June 1997.

Converted to html, with minor twiddles: August 1997.

Introduction

Given a model system specified in Promela, Spin can perform random or interactive simulations of the system's execution or it can generate a C program that performs a fast exhaustive verification of the system state space. During simulations and verifications Spin checks for the absence of deadlocks, unspecified receptions, and unexecutable code. The verifier can also be used to prove the correctness of system invariants and it can find non-progress execution cycles. Finally, it supports the verification of linear time temporal constraints; either with Promela never-claims or by directly formulating the constraints in temporal logic.

The verifier is setup to be fast and to use a minimal amount of memory. The exhaustive verifications performed by Spin are conclusive. They establish with certainty whether or not a system's behavior is error-free. Very large verification runs, that can ordinarily not be performed with automated techniques, can be done in Spin with a ``bit state space'' technique. With this method the state space is collapsed to a few bits per system state stored. Although this technique doesn't guarantee certainty, the coverage is better, and often much better, than that obtained with traditional random simulation.

Promela

The syntax of Promela is C-like. Below, our tendency is to use examples for those parts that are similar to C, but we attempt to be more precise elsewhere.

Lexical conventions

Comments

Identifiers

Keywords

	active		assert		atomic		bit

	bool		break		byte		chan

	d_step		Dproctype	do		else

	empty		enabled		fi		full

	goto		hidden		if		init

	int		len		mtype		nempty

	never		nfull		od		of

	pcvalue		printf		priority	proctype

	provided	run		short		skip

	timeout		typedef		unless		unsigned

	xr		xs

Labels

Constants

	#define NAME	5 

Expressions

	+	-	*	/	%	>

	>=	<	<=	==	!=	!

	&	||	&&	|	~	>>

	<<	^	++	--

	len()	empty()	nempty()	nfull()	full()

	run	eval()	enabled()	pc_value()

Conditional expressions

	(expr1 -> expr2 : expr3)

Declarations

Variables

	byte name1, name2 = 4, name3

Arrays

	int name[4]

Symbolic constants

	mtype = {OK, READY, ACK}

	mtype Status = OK;

The advantage of mtypes over #defines is that the former type of symbolic constants is recognized by Spin and during simulations the symbolic names are used instead of the values they represent.

Message channels

	chan Transfer =[2] of {mtype, bit, short, chan},

	     Device[3] =[0] of {byte},

	     Channel

Note that a channel can be part of a message.

Exclusive receive (xr) and send (xs) on channels

	xr Transfer;

	xs Channel;

It is a run-time error if during analysis it turns out that some other process receives from Transfer or sends to Channel.

See Reductions for more detail.

Structures

	typedef Msg {

		byte a[3], b;

		chan p

	}

	Msg foo;

	chan stream =[0] of {mtype,Msg}

	foo.a[1]

Hidden variables

   hidden int foo

Only global declarations can be thus qualified; elements of a structure are considered local. Bit, bool and channel variables cannot be hidden.

There is a pre-declared hidden variable, _, which can be assigned to in any context. Its (implicit) type is int so that it can be used to assign bit, bool, byte, mtype, short and int values to.

Processes

	proctype pname( chan In, Out; byte id )

	{ statements }

	run pname(Transfer, Device[0], 0)

Processes cannot have arrays as (part of) a formal parameter type, but structures are allowed.

Process declarations can be augmented in various ways. The most general form is

	active [N] proctype pname(...) provided (E) priority M

A proctype can have an enabling condition E associated with it, which is a general side-effect free expression that may contain constants, global variables, the predefined variables timeout and pid, but not other local variables or parameters, and no remote references. Enabling conditions are evaluated once, in the initial state.

For use during random simulations, a process instance can run with a priority M, a constant >=1. Such a process is M times as likely to be scheduled than a default (priority 1) process. Execution priorities can be used in a run-statement as well:

	run pname(...) priority M

Note that priorities have no effect during analysis.

Deterministic processes

	Dproctype pname( chan In, Out; byte id )

	{ statements }

Note that determinism is a dynamic property. E.g., if pname has in its body the statement

	if

	:: In?v  -> ...

	:: Out!e -> ...

	fi

Init process

	init { statements }

Never claim

	never { statements }

The individual statements in statements are interpreted as conditions (see Exec and ExprStat) and, therefore, should not have side-effects (although this will cause warnings rather than syntax-errors).

Statements that can have side-effect are assignments, auto-increment and decrement operations, communications, run and assert statements.

Never claims can use three additional functions:

• enabled(pid) This boolean function returns true if the process with instantiation number denoted by pid is able to perform an operation. This function can only be used in systems that do not admit synchronous communication
• pcvalue(pid) This function returns the number of the state that the process with instantiation number denoted by pid is currently in. (With state-numbers as given by the -d runtime option.)
• _np This predicate is true if the system is in a non-progress state and is false otherwise. It is introduced to enable more efficient searches for non-progress cycles. See progress and SearchNPC.

Special variables

	_pid, _last

Remote references

	procname[pid]@label

Statements

	assert		assignment	atomic		break

	declaration	d_step		else		expression

	goto		receive		selection	skip

	repetition	send		timeout		unless

Statements are separated by either a semi-colon (;) or, equivalently, an arrow (->). The arrow is sometimes used to indicate a causal relation between successive statements and also in selection and repetition statements to separate the guard from the statements it is guarding; see select and repet.

Statements that have no smaller statements as a constituent, are called basic. E.g., an assignment is a basic statement whereas a selection is not.

Execcutability

Assert

	assert( expression )

Atomic

	atomic { statements }

Making local computations atomic can effect important reductions of the complexity of the verification system; cf. MemAtD.

During its execution, control can only be transferred outside the scope of an atomic statement by an explicit goto or at a point where a statement within its scope becomes blocked. If this statement subsequently becomes enabled again, execution may continue at that point.

There is no constraint on what may occur inside the scope, other than that no nested atomic or d_step is allowed. In particular, it is possible to jump to any (labeled) location within the scope of an atomic.

The body of a process instance activated by a run-statement is considered to be outside the scope of the atomic statement performing the activation.

Break

Goto

	goto label

Deterministic step

	d_step { statements }

	goto label;

	...

label:

	d_step {

		...

		do

		...

			break

		...

		od

	}

	goto label;

	...

label: skip;

	d_step {

		...

		do

		...

			break

		...

	od; skip

	}

Else

Expressions

For example, instead of writing a busy wait loop

	while (a != b) skip

	(a == b)

Channel operations

 	q!var1,const,var2,...  or, equivalently  q!var1(const,var2,...)

	q?var1,const,var2,...  or, equivalently  q?var1(const,var2,...)

Constants in the list of a receive, constrain its enabledness by forcing the corresponding values in the oldest message (or matching send) to be the same; if not, the receive is blocked.

It is possible to use a local or global variable to likewise constrain a channel operation's enabledness:

	q?var1,eval(var2),var3

For buffered channels, there are additional operations:

• q?[var1,const,var2] returns true (i.e. a non-zero value) precisely if the corresponding receive operation would be enabled.
• q? like a standard receive operation except that the message is not removed from the buffer.
• q!!var1,const,var sorted send; it inserts its message into the buffer immediately ahead of (so that it will be younger than) the oldest message that succeeds it in numerical, lexicographic order.
• q??var1,const,var random receive; it executes if there is some message in the buffer for which it is enabled and then retrieves the oldest such message.
• q??[var1,const,var2] returns true (i.e. a non-zero value) precisely if the corresponding receive operation would be enabled.
• q?? like a standard random receive operation except that the message is not removed from the buffer.

Selection

	if

	:: statements

	...

	:: statements

	fi

Repetition

	do

	:: statements

	...

	:: statements

	od

Skip

Timeout

Unless

	{ statements-1 } unless { statements-2 }

In an unless, a d_step, in contrast with an atomic, is considered indivisible; i.e., enabledness of statements-2 is not checked if control in statements-1 resides within the scope of a d_step.

Executing a Promela system

Initially, all global (non-initialized) variables contain the value 0 and the channel buffers are empty. The existing process instances are the ones created through the active modifier on the proctype declarations together with the init and never processes, if present. The location counters of these instances are at their first statements.

A system state of a Promela system uniquely identifies the enabled statements in every (active) process instance. An execution step in a system without never claim, proceeds by arbitrarily selecting one of the enabled statements and then executing that statement, thus arriving in a new system state. So, process instances execute asynchronously. Note, however, that in case the selected statement was an unbuffered send (receive), a corresponding receive (send) statement was executed simultaneously.

If the system does have a never claim, an execution step is a combined, synchronized step: executing an (enabled) statement from the never claim together with a step from the rest of the system, as above. Thus, a never claim blocks execution of the system, in those situations in which the never claim has no enabled statements (in the current state); also see tempclaim.

The execution sequences, or behaviors, of a Promela system are the maximal (possibly infinite) sequences of execution steps, in which the first step is taken from the initial system state and each successive step from the state produced by the preceding step. In particular, notice that Promela allows starvation of processes during an execution. This behavior can be influenced by the analyzer command line switch -f: if given, process starvation cannot occur; i.e., execution sequences along which some process instance eventually does not make a move anymore although the instance remains continuously enabled are no longer possible.

Atomic statements and d_steps

Analysis

End-states

Strictly speaking, valid end-states should also require channels to be empty. Conformance with this stricter condition is obtained through Spin's -q option.

When checking for state properties, the verifier will complain if there is an execution that terminates in an invalid end-state.

Progress states

When checking for non-progress cycles, the verifier will complain if there is an execution that does not visit infinitely often a progress state.

Acceptance states

When checking for acceptance cycles, the verifier will complain if there is an execution that visits infinitely often an acceptance state.

Temporal claims

When checking for state properties, the verifier will complain if there is an execution that ends in a state in which the never claim has terminated; i.e., has reached the closing } of its body. When checking for acceptance cycles, the verifier will complain if there is an execution that visits infinitely often an acceptance state. Thus, a temporal claim can detect illegal infinite (hence cyclic) behavior by labeling some statements in the never claim with an acceptance label.

In such situations the never claim is said to be matched. In the absence of acceptance labels, no cyclic behavior can be matched by a temporal claim. Also, to check a cyclic temporal claim, acceptance labels should only occur within the claim and nowhere else in the Promela system.

A never claim is intended to monitor every execution step in the rest of the system for illegal behavior and for this reason it executes in lock-step. Such illegal behavior is detected if the never claim matches along a computation. If a claim blocks (because no statement in its body is enabled) but it is not at its closing }, then there is no need to explore this computation any further because it cannot lead to a violation; whence a blocked claim terminates execution in the rest of the system so that other executions can be explored.

Note that if a never claim exhibits non-determinism then, according to the definition of execution sequence, the different ways in which this non-determinism is resolved result in different executions.

Example claim

``along every computation, each system state in which p is true (a p-state) is eventually followed by a q-state''

never {

	do

	:: p -> break

	:: skip

	od;

accept:

	do

	:: !q

	od

}

Note that replacing skip by else would check only the first occurrence of a p-state along computations. Stated differently, by giving the first repetition the non-deterministic choice in p-states to either break or continue and by relying on the exhaustive search mechanism of the analyzer, every occurrence of a p-state is checked. In fact, one can show that it is impossible to check this property without using non-determinism as above.

Memory and time requirements

As to the memory demands when checking for state properties, the visited system states need to be stored in order to decide when to backtrack, as well as the partial computation that is being extended (the `stack' in terms of depth-first generation) in order to know where to backtrack to. This, together with the number of bytes needed to represent a system state, i.e., the size of the state vector, determines the amount of memory that is needed to complete an analysis. In particular, the set of already visited system states must be kept in main memory as this set is accessed in an, essentially, random way during analysis. This is the reason why the size of the system that can be analyzed is directly determined by the amount of physical RAM.

If analysis has to establish the presence (progress) or absence (acceptance) of cyclic computations, both the number of stored states and the size of the `stack' at worst doubles when compared to the case of checking state properties. Note that checking a never claim corresponds to the analysis of a property in one of these three classes. Also note that adding a non-deterministic never claim to a system will in itself increase the state space so that it is quite possible that the memory demands increase more than twofold when searching for behavior matching a never-claim that has an acceptance state.

Analysis time is proportional to the number of visited configurations.

Atomic statements and d_steps

Partial order reduction

Partial order reduction as implemented in Spin has the most effect on loosely coupled systems that interact through shared, global variables and/or buffered channels. If a system has no shared variables and uses only unbuffered communication channels, there will be no reduction in memory or time.

Stutter closedness

	never { p; p }

Any property that can be expressed in linear temporal logic without using the `next-state' (X) operator is guaranteed to be stutter-closed. In fact, the above never claim would correspond to the temporal logic formula: p && X p.

In fact, independently of whether partial order reduction is used or not, it is probably a good idea to only verify stutter closed never claims. The reason is that Spin translates Promela programs to intermediate code before analyzing them and stutter closed claims shield from the translation specifics.

Searching for non-progress cycles

never {

	/* non-progress: <>[] _np */

	do

	:: skip

	:: _np -> break

	od;

accept:

	do

	:: _np

	od

}

Note that for more complex non-progress properties, the user has to supply her own never claim and it is here that the _np-predicate is of use.

Increasing the amount of reduction

	If you declare   Other processes may only do





	xr q             send actions on q

	                 nfull(q)

	xs q             receive actions on q

	                 nempty(q) 

Bit-state hashing

Bit-state hashing works by allowing more states to be stored in the memory, M, set aside for recording visited states; the memory needed to store the stack is not reduced. It achieves this reduction by viewing every bit in M as a bucket in a hash table. Each system state is hashed onto a fixed number of buckets (i.e., 2), but only the fact that a bucket has become filled is recorded. In other words, there is no collision detection and if two system states hash onto the same buckets, they are deemed to be the same states. It is this feature that allows many more states to be stored. E.g., if the state vector of a system is 100 bytes then bit-state hashing, in the ideal case of a perfect hashing function, allows upto 800 times as many states to be stored and visited as would be possible with an exhaustive analysis using the same amount of memory.

Reality is more complex. Hash functions are not perfect, collisions will occur and get more common the fuller the hash table becomes and each collision potentially causes a part of the state space to remain unexplored.

The analyzer gives an indication of the quality of a bit-state search in the form of a hash factor: the fraction of buckets that were filled. I.e., a hash-factor of 100 means that, on average, at most 1 out of every 100 bits in M was set. This is taken as indicating a good quality search. Spin reports in this case ``expected coverage: >= 99.9% on avg.''. For a hash-factor between 10 and 100, Spin gives an expected coverage of 98% on average. These are heuristic estimates, and the variance can be large. E.g., experiments indicate that `98% coverage on average' can mean as low as 84% during an actual analyzer run. On the other hand, such coverage still is much superior over what is achieved by a standard random simulation.

Spin Online References Promela Manual Index Promela Grammar

Spin HomePage