Promela Reference -- procedures(6)

`procedures`

NAME
procedures - for structuring a program text.

DESCRIPTION
There is no explicit support in the basic Promela language for defining procedures or functions. This restrction can be circumvented in some cases through the use of either inline primitives, or embedded C code fragments.

The reason for this restriction to the basic language is that Spin targets the verification of process interaction and process coordination structures, and not internal process computations. Abstraction is then best done at the process and system level, not at a computational level. It is possible to approximate a procedure call mechanism with Promela process instantiations, but this is rarely a good idea. Consider, for instance, the following model:

#ifndef N
#define N	12
#endif

int f = 1;

proctype fact(int v)
{
	if
	:: v > 1 -> f = v*f; run fact(v-1)
	:: else
	fi
}

init {
	run fact(N);
	(_nr_pr == 1) ->
	printf("%d! = %d\n", N, f)
}

Initially, there is just one process in this system, the init process. It instantiates a process of type fact passing it the value of constant N , which is defined in a macro. If the parameter passed to the process of type fact is greater than one, the value of global integer f is multiplied by v , and another copy of fact is instantiated with a lower value of the parameter.

The procedure of course closely mimics a recursive procedure to compute the factorial of N . If we store the model in a file called badidea and execute the model, we get

$ spin badidea
12! = 479001600
13 processes created

which indeed is the correct value for the factorial. But, there are a few potential gotcha's here. First, the processes that are instantiated will execute asynchronously with the already running processes. Specifically, we cannot assume that the process that is instantiated in a run statement terminates its execution before the process that executed the run reaches its next statement. Generally, the newly created process will start executing concurrently with its creator. Nothing can be assumed about the speed of execution of a running process. If a particular order of execution is important, this must be enforced explicitly through process synchronization. In the initially running init process from the example, synchronization is achieved in one place with the expression

(_nr_pr == 1)

The variable _nr_pr is a predefined, global system variable that records the number of current executing processes, see the corresponding manual page. Because there is initially just one executing process (the process of type main itself), we know in this case that all newly instantiated processes must have terminated once the evaluation of this expression yields true. Recall that a condition statement can only be executed in Promela if it evaluates to true, which gives us the required synchronization, and guarantees that the final value of f is not printed before it is fully computed.

A more obvious gotcha is that the maximum useful value we can choose for the constant N is limited by the maximum number of processes that can simultaneously be instantiated. The maximum value that can be represented in a variable of type int is more restrictive in this case, though. The size of an int is the same in Promela as it is in the underlying programming language C, which at the time of writing means only 32 bits on most machines. The maximum signed value that can be represented in a 32 bit word is 2^31 -1 = 2,147,483,648, which means that the largest factorial we can compute with our model is an unimpressive 13! = 1,932,053,504. To do better, we would need a data type double or float , but Promela deliberately does not have them. The only way we could get these would be through the use of embedded C code fragments. The more fundamental reason why these data types are not part of native Promela is that any need to represent data quantities of this size almost certainly means that the user is trying to model a computational problem, and not a process synchronization problem. The omission of the larger data types from the language serves as a gentle warning to the user that the language is meant for design verification, and not for design implementation.

If a procedural mechanism is to be used, the most efficient method would be to use a macro or an inline definition. This amounts to an automatic inlining of the text of a procedure call into the body of each process that invokes it. A disadvantage of a macro is that line-number references will be restricted to the location of the macro call, not a line number within a macro definition itself. This problem does not exist with an inline definition.

If a separate process is used to model the procedure, the best way to do so is to declare it as a permanent server by declaring it as an active proctype : receiving requests from user processes via a special globally defined channel, and responding to these requests via a user-provided local channel.

The least attractive method is to instantiate a new copy of a process once for each procedure call and wait for that process to return a result (via a global variable or a message channel) and then disappear from the system before proceeding. This is less attractive because it produces the overhead of process creation and deletion, and can add the complication of determining reliably when precisely a process has disappeared from the system.

Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage (Page updated: 28 November 2004)

`Promela`

`Omission`

`procedures`