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) .
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.