- Types of Objects
- Processes
- Provided Clauses
- Data Objects
- Data Structures
- Message Channels
- Channel Poll Operations
- Sorted Send And Random Receive
- Rendezvous Communication
- Rules For Executability
- Assignments And Expressions
- Control Flow: Compound Statements
- Atomic Sequences
- Deterministic Steps
- Selection
- Repetition
- Escape Sequences
- Inline Definitions
- Reading Input
- Special Features
- Finding Out More
This chapter is from the book
This chapter is from the book
This chapter is from the book
Sorted Send And Random Receive
Two other types of send and receive statements are used less frequently: sorted send and random receive. A sorted send operation is written with two, instead of one, exclamation marks, as follows:
qname!!msg0
A sorted send operation inserts a message into the channel’s buffer in numerical, rather than in FIFO, order. For instance, if a process sends the numbers from one to ten into a channel in random order, but using the sorted send operation, the channel automatically sorts them, and stores them in numerical order.
When a sorted send operation is executed, the existing contents of the target channel is scanned from the first message towards the last, and the new message is inserted immediately before the first message that follows it in numerical order. To determine the numerical order, all message fields are taken into account and are interpreted as integer values.
The counterpart of the sorted send operation is the random receive. It is written with two, instead of one, question marks:
qname??msg0
A random receive operation is executable if it is executable for any message that is currently buffered in a message channel (instead of being restricted to a match on the first message in the channel). In effect, the random receive operation as implemented in SPIN will always return the first message in the channel buffer that matches, so the term “random receive” is a bit of a misnomer.
Normal send and receive operations can freely be combined with sorted send and random receive operations. As a small example, if we consider the channel with the sorted list of integers from one to ten, a normal receive operation can only retrieve the first message, which will be the smallest value one. A random receive operation on the same channel would succeed for any of the values from one to ten: the message need not be at the head of the queue. Of course, a random receive operation only makes sense if at least one of the parameters is a constant, and not a variable. (Note that the value of a variable is not evaluated to a constant unless forced with an eval function.)