NAME
send statement - for sending messages to channels.

SYNTAX
name ! send_args
name !! send_args

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

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

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

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

SEE ALSO
chan(2), receive(4), empty(5), full(5), len(5), nempty(5), nfull(5), poll(5).