- Types of Objects
- Processes
- Provided Clauses
- Data Objects
- Data Structures
- Message Channels
- Channel Poll Operations
- Sorted Send And Random Receive
- Rendezvous Communication
- Rules For Executability
- Assignments And Expressions
- Control Flow: Compound Statements
- Atomic Sequences
- Deterministic Steps
- Selection
- Repetition
- Escape Sequences
- Inline Definitions
- Reading Input
- Special Features
- Finding Out More
This chapter is from the book
This chapter is from the book
This chapter is from the book
Special Features
The verifiers that can be generated by SPIN by default apply a partial order reduction algorithm that tries to minimize the amount of work done to prove system properties. The performance of this algorithm can be improved, sometimes very substantially, if the user provides some hints about the usage of data objects. For instance, if it is known that some of the message channels are only used to receive messages from a single source process, the user can record this knowledge in a channel assertion.
In the example shown in Figure 3.3, for instance, the number of states that has to be searched by the verifier is reduced by 16 percent if the lines containing the keywords xr and xs are included. (The two keywords are acronyms for exclusive read access and exclusive write access, respectively.) These statements are called channel assertions.
Figure 3.3 Using Channel Assertions
mtype = { msg, ack, nak };
chan q = [2] of { mtype, byte };
chan r = [2] of { mtype };
active proctype S()
{ byte s = 1;
xs q; /* assert that only S sends to chan q */
xr r; /* and only S receives from chan r */
do
:: q!msg(s);
if
:: r?ack; s++
:: r?nak
fi
od
}
active proctype R()
{ byte ns, s;
xs r; /* only R sends messages to chan r */
xr q; /* only R retrieves messages from chan q */
do
:: q?msg(ns);
if
:: (ns == s+1) -> s = ns; r!ack
:: else -> r!nak
fi
od
}
The statements are called assertions because the validity of the claims they make about channel usage can, and will, be checked during verifications. If, for instance, it is possible for a process to send messages to a channel that was claimed to be non-shared by another process, then the verifier can always detect this and it can flag a channel assertion violation. The violation of a channel assertion in effect means that the additional reduction that is based on its presence is invalid. The correct counter-measure is to then remove the channel assertion.
The reduction method used in SPIN (more fully explained in Chapter 9) can also take advantage of the fact that the access to local variables cannot be shared between processes. If, however, the verification model contains a globally declared variable that the user knows to be non-shared, the keyword local can be used as a prefix to the variable declaration. For instance, in the last example we could have declared the variable ns from proctype R as a global variable, without incurring a penalty for this change from the partial order reduction algorithm, by declaring it globally as:
local byte ns;
The use of this prefix allows the verifier to treat all access to this variable as if it were access to a process local variable. Other than for channel assertions, though, the verifier does not check if the use of the prefix is unwarranted.
Another case that one occasionally runs into is when a variable is used only as a scratch variable, for temporary use, say, deep inside a d_step or an atomic sequence. In that case, it can be beneficial to tell the verifier that the variable has no permanent state information and should not be stored as part of the global state-descriptor for the modeled system. We can do so by using the prefix hidden. The variable must again be declared globally, for instance, as:
hidden int t;
In the following PROMELA fragment the variable t is used as a temporary variable that stores no relevant information that must be preserved outside the d_step sequence in which it is used:
d_step { /* swap the values of a an b */
t = a;
a = b;
b = t
}
As with the use of the local prefix, the verifier takes the information on good faith and does not check if the use of the hidden keyword is unwarranted. If a hidden variable does contain relevant state information, the search performed by the verifier will be incomplete and the results of the search become unreliable.
There is a third, and last, type of prefix that can be used with variable declarations in special cases. The use of the prefix show on a variable declaration, as in
show byte cnt;
tells SPIN’s graphical user interface XSPIN that any value changes of this variable should be visualized in the message sequence charts that it can generate. We will discuss this interface in more detail in Chapter 12.
The show prefix can be used on both global and local variable declarations.