Promela Reference -- send(4)





send statement - for sending messages to channels.

name ! send_args
name !! send_args

A send statement on a buffered channel (see chan(2)) is by default executable in every global system state where the target channel is non-full. Spin contains an option to override this default with option -m , When this option is used, a send statement on a buffered channel is always executable, and the message is lost if the target channel is full.

The execution of a send statement on a rendezvous channel consists, conceptually, of two steps: a rendezvous offer and a rendezvous accept . The rendezvous offer can be made at any time (see Intro(0)). The offer can be accepted only if another active process can perform the matching receive operation immediately (i.e., with no intervening steps by any process). An offer that cannot be accepted is considered to have not been issued.

For buffered channels, assuming no message loss occurs (see above), the message is added to the channel. In the first form of the send statement, with a single '!,' the message is appended to the tail of the channel, maintaining fifo order. In the second form, with a double '!!,' the message is inserted into the channel immediately ahead of the oldest message in the channel that succeeds it in numerical order. To determine the numerical order, all message fields are significant.

Within the semantics model, the effect of issuing the rendezvous offer is to set global system variable handshake to the channel identity of the target channel (see Intro(0)).

The number of message fields that is specified in the send statement must always match the number of fields that is declared in the channel declaration for the channel addressed, and the values of the expressions specified in the message fields must be compatible with the range of the integer datatype that was declared for the corresponding field. The types of message fields that were declared to contain a either user-defined data type or a chan must match precisely.

The first form of the statement is the standard fifo send statement. The second form of the send statement, with the double '!!,' is called a sorted send statement. The sorted send operation can be exploited by, for instance, listing an appropriate message field (e.g., a sequence number) as the first field of each message.

By convention, the first field in a message is used to specify the message type, and is defined as an mtype .

Sorted send operations and the FIFO send operations may be used in any combination within a model and with any buffered channel.

chan(2), 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 May 2000)