Promela |
Declarator |
xr(2) |
NAME
xr
-
for optimizing read-access to a message passing channel.
DESCRIPTION
The declaration
xr q1can only appear locally within a proctype body (anywhere), and is used to declare that a single instantiation of this proctype has exclusive read-access to this channel, e.g., to receive messages. It is an error if more than one active process attempts read-access to the channel thus tagged. With this information, the partial order reduction algorithm can be optimized and verification complexity can be reduced, often by a substantial amount. Any test on the contents of a channel, including receive polls and the use of len(q1) , counts as both a read and a write access of the channel q1 , which may conflict with an xr or xs declaration, and is flagged as an error if it occurs.
The only safe channel poll operations, that are consistent with an xr or xs declaration, are nempty , and nfull , respectively. (Their predefined negations empty and full have no similar benefit, but are included for symmetry.) The grammar prevents circumvention of the type rules by attempting constructions such as !nempty(q) .
NOTES
These assertions cannot be made for rendez-vous channels.
If a channel array is declared, then an assertion of this
type on any one of the elements of the array is understood
to apply to all elements. (Both these are hopefully temporary
implementation constraints.)
In some cases, the check for compliance with the declared access patterns is too strict, for instance when a channel name is passed as a parameter to a process (which counts as both a read and a write access). In those cases, the checks for compliance can be suppressed, while maintaining the benefit of the optimization of the verification. To do so, the verifier source in pan.c can be compiled with the directive -DXUSAFE . Use with caution.
SEE ALSO
chan(2), xs(2), len(5), nempty(5), nfull(5).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |