pointers - indirect memory addressing.
There are no pointers in the basic Promela language, although there is a way to circumvent this restriction through the use of embedded C code.
The two main reasons for leaving pointers out of the basic language are efficiency and tractability. To make verification possible, the verifier needs to be able to track all data that are part of reachable system states. Spin maintains all such data, that is, local process states, local and global variables, and channel contents, in a single data structure called the system ``state vector.'' The efficiency of the Spin verifiers is in large part due to the availability of all state data within the simple, flat state vector structure, which allows each state comparison and state copying operation to 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 constant factor times the time needed to copy the bits in the state vector from one place to another (that is, the cost of an invocation of the system routine memcpy() ).
The use of data that are only accessible through pointers during verification runs requires the verifier to collect the relevant data from all memory locations that could be pointed to at any one time and copy such information into the state vector. The associated overhead immediately translates in reduced verification efficiency.
See also the use of embedded C code fragments.
Spin Online References
Promela Manual Index
|(Page updated: 28 November 2004)|