- 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
Message Channels
Message channels are used to model the exchange of data between processes. They are declared either locally or globally. In the declaration
chan qname = [16] of { short, byte, bool }
the typename chan introduces a channel declaration. In this case, the channel is named qname, and it is declared to be capable of storing up to sixteen messages. There can be any finite number of fields per message. In the example, each message is said to consist of three fields: the first is declared to be of type short, the second is of type byte, and the last is of type bool. Each field must be either a user-defined type, such as Field from the last section, or a predefined type from Table 3.1. In particular, it is not possible to use an array as a type declarator in a message field. An indirect way of achieving this effect is again to embed the array into a user-defined type, and to use the type name as the type declarator for the message field. Note also that since the type chan appears in Table 3.1, it is always valid to use chan itself as a field declarator. We can make good use of this capability to pass channel identifiers from one process to another.
The statement
qname!expr1,expr2,expr3
sends a message with the values of the three expressions listed to the channel that we just created. The value of each expression is cast to the type of the message field that corresponds with its relative position in the list of message parameters. By default 2 the send statement is only executable if the target channel is not yet full, and otherwise it blocks.
The statement
qname?var1,var2,var3
retrieves a message from the head of the same buffer and stores the values from the three fields into the corresponding variables.
The receive statement is executable only if the source channel is non-empty.
It is an error to send or receive either more or fewer message fields than were declared for the message channel that is addressed.
An alternative, and equivalent, notation for the send and receive operations is to use the first message field as a message type indication, and to enclose the remaining fields in parentheses, for instance, as follows:
qname!expr1(expr2,expr3) qname?var1(var2,var3)
Some or all of the parameters to a receive operation can be given as constants (e.g., mtype symbolic constants) instead of variables:
qname?cons1,var2,cons2
In this case, an extra condition on the executability of the receive operation is that the value of all message fields specified as constants match the value of the corresponding fields in the message that is to be received. If we want to use the current value of a variable for this purpose, that is, to constrain the receive operation to messages that have a matching field, we can use the predefined function eval, for instance, as follows:
qname?eval(var1),var2,var3
In this case, the variable var1 is evaluated, and its value is used as a constraint on incoming messages, just like a constant. The receive operation is now executable only if a message is available that has a first field with a value that matches the current value of var1. If so, the values of var2 and var3 are set to the values of the corresponding fields in that message, and the message is removed from channel qname.
A simple example of the mechanisms discussed so far is as follows:
mtype = { msg0, msg1, ack0, ack1 };
chan to_sndr = [2] of { mtype };
chan to_rcvr = [2] of { mtype };
active proctype Sender()
{
again: to_rcvr!msg1;
to_sndr?ack1;
to_rcvr!msg0;
to_sndr?ack0;
goto again
}
active proctype Receiver()
{
again: to_rcvr?msg1;
to_sndr!ack1;
to_rcvr?msg0;
to_sndr!ack0;
goto again
}
The model shown here is a simplified version of the alternating bit protocol as defined by Bartlett, Scantlebury, and Wilkinson [1969]. We will extend it into a more complete version shortly, after we have covered a little bit more of the language.
The declaration
mtype = { msg0, msg1, ack0, ack1 };
introduces the four types of messages we will consider as symbolic constants.
We have used a label, named again in each proctype and a goto statement, with the usual semantics. We talk in more detail about control-flow constructs towards the end of this chapter. The first ten steps of a simulation run with the model above generate the following output.
$ spin -c -u10 alternatingbit.pml proc 0 = Sender proc 1 = Receiver q 0 1 1 to_rcvr!msg1 1 . to_rcvr?msg1 2 . to_sndr!ack1 2 to_sndr?ack1 1 to_rcvr!msg0 1 . to_rcvr?msg0 2 . to_sndr!ack0 2 to_sndr?ack0 ------------ depth-limit (-u10 steps) reached ------------ ...
We have used the SPIN option -c to generate a columnated display of just the send and receive operations, which in many cases gives us just the right type of information about process interaction patterns. Every channel and every process is assigned an identifying instantiation number. Each column in the display above corresponds to a process number as before. Each row (line) of output also contains the instantiation number of the channel that is addressed in the left margin.
We have also used the SPIN option -u10 to limit the maximum number of steps that will be executed in the simulation to ten.
There are many more operations in PROMELA that may be performed on message channels. We will review the most important operations here.
The predefined function len(qname) returns the number of messages that is currently stored in channel qname. Some shorthands for the most common uses of this function are: empty(qname), nempty(qname), full(qname), and nfull(qname) with the obvious connotations.
In some cases we may want to test whether a send or receive operation would be executable, without actually executing the operation. To do so, we can transform each of the channel operations into a side effect free expression. It is, for instance, not valid to say:
(a > b && qname?msg0) /* not valid */
or
(len(qname) == 0 && qname!msg0) /* not valid */
because these expressions cannot be evaluated without side effects, or more to the point, because send and receive operations do not qualify as expressions (they are i/o statements).
To state a condition that should evaluate to true when both (a > b) and the first message in channel qname is of type msg0, we can, however, write in
PROMELA:
(a > b && qname?[msg0]) /* valid */
The expression qname?[msg0] is true precisely when the receive statement qname?msg0 would be executable at the same point in the execution, but the actual receive is not executed, only its precondition is evaluated. Any receive statement can be turned into a side effect free expression in a similar way, by placing square brackets around the list of message parameters. The channel contents remain undisturbed by the evaluation of such expressions.