- 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
Rendezvous Communication
So far we have talked about asynchronous communication between processes via message channels that are declared for instance as
chan qname = [N] of { byte }
where N is a positive constant that defines the maximum number of messages that can be stored in the channel. A logical extension is to allow for the declaration
chan port = [0] of { byte }
to define a rendezvous port. The channel capacity is now zero, that is, the channel port can pass, but cannot store messages. Message interactions via such rendezvous ports are by definition synchronous. Consider the following example:
mtype = { msgtype };
chan name = [0] of { mtype, byte };
active proctype A()
{ name!msgtype(124);
name!msgtype(121)
}
active proctype B()
{ byte state;
name?msgtype(state)
}
Channel name is a rendezvous port. The two processes synchronously execute their first statement: a handshake on message msgtype and a transfer of the value 124 from process A into local variable state in process B. The second statement in process A is unexecutable (it blocks), because there is no matching receive operation for it in process B.
If the channel name is defined with a non-zero buffer capacity, the behavior is different. If the buffer size is at least two, the process of type A can complete its execution, before its peer even starts. If the buffer size is one, the sequence of events is as follows. The process of type A can complete its first send action, but it blocks on the second, because the channel is now filled to capacity. The process of type B can then retrieve the first message and terminate. At this point A becomes executable again and also terminates, leaving its second message as a residual in the channel.
Rendezvous communication is binary: only two processes, a sender and a receiver, can meet in a rendezvous handshake.
Message parameters are always passed by value in PROMELA. This still leaves open the possibility to pass the value of a locally declared and instantiated message channel from one process to another. The value stored in a variable of type chan is nothing other than the channel identity that is needed to address the channel in send and receive operations. Even though we cannot send the name of the variable in which a channel identity is stored, we can send the identity itself as a value, and thereby make even a local channel accessible to other processes. When the process that declares and instantiates a channel dies, though, the corresponding channel object disappears, and any attempt to access it from another process fails (causing an error that can be caught in verification mode).
As an example, consider the following model:
mtype = { msgtype };
chan glob = [0] of { chan };
active proctype A()
{ chan loc = [0] of { mtype, byte };
glob!loc;
loc?msgtype(121)
}
active proctype B()
{ chan who;
glob?who;
who!msgtype(121)
}
There are two channels in this model, declared and instantiated in two different levels of scope. The channel named glob is initially visible to both processes. The channel named loc is initially only visible to the process that contains its declaration. Process A sends the value of its local channel variable to process B via the global channel, and thereby makes it available to that process for further communications. Process B now transmits a message of the proper type via a rendezvous handshake on that channel and both processes can terminate. When process A dies, channel loc is destroyed and any further attempts to use it will cause an error.