for sending messages to channels.
A send statement on a
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
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
channel consists, conceptually, of two steps:
and a rendezvous
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
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
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
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
must match precisely.
The first form of the statement is the standard
The second form of the send statement, with the double '!!,'
is called a
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
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).