Promela Reference -- send(4)


Basic Statement


send statement - for sending messages to channels.

name ! send_args
name !! send_args

A send statement on a buffered channel is executable in every global system state where the target channel is non-full. Spin supports a mechanism 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. 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). The rendezvous send operation can only take place if the offer made is accepted by a matching receive operation in another process.

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 exclamation mark, the message is appended to the tail of the channel, maintaining fifo (first in, first out) order. In the second form, with a double exclamation mark, the message is inserted into the channel immediately ahead of the first 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.

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 target channel, and the values of the expressions specified in the message fields must be compatible with the datatype that was declared for the corresponding field. If the type of a message field is either a user-defined type or chan , then the types must match precisely.

The first form of the send statement is the standard fifo send. The second form, with the double exclamation mark, is called a sorted send operation. 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, thus forcing a message ordering in the target channel.

In the following example our test process uses sorted send operations to send three messages into a buffered channel named x . Then it adds one more message with the value four.

All four values are now receivable in numerical order; the last message only coincidentally, but the first three due to the ordering discipline that is enforced by the sorted send operators. A simulation confirms this:

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 fifo send operations can safely be mixed.


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