Promela |
Declarator |
xs(2) |
NAME
xs
-
for optimizing write-access to a message passing channel.
DESCRIPTION
The declaration
xs q1can only appear locally within a proctype body (anywhere), and is used to declare that a single instantiation of this proctype has exclusive write-access to this channel, e.g., to send messages. With this information, the partial order reduction algorithm can be optimized and verification complexity can be reduced. For the partial order reduction, any test on the contents of a channel, including receive polls and the use of len(q1) , count as both a read and a write access of the channel q1 , which may conflict with an xr or xs assertion, and flagged as an error.
The only safe channel poll operations, that are consistent with an xr or xs declaration, are nfull , and nempty , 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 !nfull(q) .
Summarizing: if a channel-name appears in an xs declaration, it can safely be accessed only with send operations and with nempty . If a channel-name appears in an xr declaration, it can safely be accessed only with receive operations and with nfull . All other types of access will generate run-time complaints from the verifier.
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), xr(2), len(5), nempty(5), nfull(5).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |