NAME
pointers - indirect memory addressing.

DESCRIPTION
There are no pointers in Promela. To make verification possible, the verifier needs to be able to track all data that are part of a reachable system states. Spin maintains all such data, i.e., local process states, local and global variables, and channel contents, in a single flat structure called a ``state vector.'' The efficiency of the Spin verifiers is due to the availability of all state data within the state vector, so that state comparison and copying can each be performed with a single system call.

The performance of a Spin verifier can be measured in the number of reachable system states per second that can be generated and analyzed. In the current system, this performance is determined exclusively by the length of the state vector: a vector twice as long requires twice as much time to verify per state, and vice versa, every reduction in the length of a state vector translates into an increase of the verifier's efficiency. The cost per state is in most cases a small linear factor times the time needed to copy the bits in the state vector from one place to another (i.e., a single invocation of the system routine memcpy() ).

A memory pointer would require the verifier to collect the relevant pieces of system data from every place in memory that could be accessible via the pointers, and to collect these into a composite state vector, once for every transition executed (i.e., possibly millions of times during the verication process). This means that in return for a fairly modest increase of expressiveness, we would lose a significant part of Spin's efficiency, and in the process unintentionally discourage the user from making the judicious abstractions that can help to keep a system tractable.

SEE ALSO
arrays(2), typedef(2).