Promela Reference -- chan(2)





chan - syntax for declaring and initializing message passing channels.

chan name
chan name = '[' const ']' of { typename [, typename ] * }

Channels are used to transfer messages (cf. definitions S.2 and S.3 in intro(0)) between active processes. Channels are declared using the keyword chan , either locally or globally, much like integer variables, Channels by default store messages in first-in first-out order (but see send(4) and receive(4)).

A single keyword chan can be followed by either a single name, or a comma-separated list of names, each optionally followed by a channel initializer.

The syntax

chan a, b; chan c[3]

declares the names a , b , and c as channel names, the last one as an array of three elements (see arrays(2)). A channel must be initialized before it can be used to store messages. It is rare to declare just a channel name without initialization, but it occurs in, for instance, proctype parameter lists, where the initialized version of a channel is not passed to the process until the time of process instantiation with a run operator.

The channel initializer specifies a channel capacity, as a constant, and the structure of the messages that can be stored in the channel, as a comma-separated list of type names. If the capacity is larger than zero, a normal buffered channel is initialized, with the given number of slots to store messages. If the capacity is specified to be zero, a rendezvous , also called a synchronous , channel, is created. Rendezvous channels can pass messages only through synchronous handshakes between sender and receiver, but they cannot buffer messages (see send(4), receive(4)).


The following channel declaration contains an initializer.

chan a = [16] of { short }

The initializer says that channel a can store up to sixteen messages of type short . Similarly,
chan c[3] = [0] of { mtype }

initializes an array of 3 rendezvous channels for messages that contain just one message field, of type mtype .

If the messages to be passed by the channel have more than one field, the declaration looks as follows:

chan qname = [8] of { mtype, int, chan, byte }

This time, we have defined a single channel that can store up to eight messages, each consisting of four fields: an mtype , followed by an int , followed by a channel name, and a byte . The chan field can be used to pass a channel identifier (a number) from one process to another.

The first field in a channel type declaration is conventionally an mtype , which is used to store a message type indicator in symbolic form. See mtype(2).

In verification, buffered channels contribute significantly to verification complexity. For an initial verification run, choose a small channel capacity, of say 2 or 4. If the verification completes swiftly, you can consider increasing the capacity to a larger size.

arrays(2), mtype(2), send(4), receive(4), empty(5), full(5), len(5), nempty(5), nfull(5), poll(5).

Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page Updated: 16 December 1997)