Promela Reference -- xr(2)




xr , xs - for defining channel assertions.

xr name [, name ]*
xs name [, name ]*

Channel assertions such as

can only appear within a proctype declaration. The channel assertions are only valid if there can be at most one single instantiation of the proctype in which they appear.

The first type of assertion, xr , states that the executing process has exclusive read-access to the channel that is specified. That is, it is asserted to be the only process in the system (determined by its process instantiation number) that can receive messages from the channel.

The second type of assertion, xs , states that the process has exclusive write-access to the channel that is specified. That is, it is asserted to be the only process that can send messages to the channel.

Channel assertions have no effect in simulation runs. With the information that is provided in channel assertions, the partial order reduction algorithm that is normally used during verification, though, can optimize the search and achieve significantly greater reductions.

Any test on the contents or length of a channel referenced in a channel assertion, including receive poll operations, counts as both a read and a write access of that channel. If such access conflicts with a channel assertion, it is flagged as an error during the verification. If the error is reported, this means that the additional reductions that were applied may be invalid.

The only channel poll operations that are consistent with the use of channel assertions are nempty (consistent with the use of xr), and nfull (consistent with the use of xs). Their predefined negations empty and full have no similar benefit. The grammar prevents circumvention of the type rules by attempting constructions such as !nempty(q), or !full(q).

Summarizing: If a channel-name appears in an xs (xr) channel assertion, messages may be sent to (received from) the corresponding channel by only the process that contains the assertion, and that process can only use send (receive) operations, or the predefined operator nfull (nempty). All other types of access will generate run-time errors from the verifier.


Channel assertions do not work for rendezvous channels.

For channel arrays, a channel assertion on any element of the array is applied to all elements.

In some cases, the check for compliance with the declared access patterns is too strict. This can happen, for instance, when a channel name is used as a parameter in a run statement, which is counted as both a read and a write access.

Another example of an unintended violation of a channel assertion can occur when a single process can be instantiated with different process instantiation numbers, depending on the precise moment that the process is instantiated in a run. In cases such as these, the checks on the validity of the channel assertions can be suppressed, while maintaining the reductions they allow. To do so, the verifier pan.c can be compiled with directive -DXUSAFE . Use with caution.


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)