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 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 also the sorted send option in the manual page for send and the random receive option in the manual page for receive ).

The keyword chan can be followed by one or more names, in a comma-separated list, each optionally followed by a channel initializer. The syntax

declares the names a , b , and c as uninitialized channels, the last one as an array of three elements.

A channel variable must be initialized before it can be used to transfer 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 a process is instantiated 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 channel capacity is larger than zero, a buffered channel is initialized, with the given number of slots to store messages. If the capacity is specified to be zero, a rendezvous port, also called a synchronous channel, is created. Rendezvous ports can pass messages only through synchronous handshakes between sender and receiver, but they cannot store messages.

All data types can be used inside a channel initializer, including typedef structure names, but not including the typename unsigned .

The following channel declaration contains an initializer:

The initializer says that channel a can store up to 16 messages. Each message is defined to have only one single field, which must be of type short . Similarly, initializes an array of three rendezvous channels for messages that contain just one message field, of type mtype .

The following is an example of the declaration of a channel that can pass messages with multiple fields:

This time the channel can store up to eight messages, each consisting of four fields of the types listed. The chan field can be used to pass a channel identifier from one process to another. In this way, a channel that is declared locally within one process, can be made accessible to other processes. A locally declared and instantiated channel disappears, though, when the process that contain the declaration dies.

The first field in a channel type declaration is conventionally of type mtype , and is used to store a message type indicator in symbolic form.

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


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