Course notes for ELG-7187C
Often one only considers two events in the life of a message: (a) the source sends the message, and (b) the destination receives the message. This is what is normally shown in UML sequence diagrams. However, received messages are often queued before they are actually processed by the destination process. The reception means that the messages arrives at the destination (and may be stored in a queue). Then we can identify the event (c) that the message is consumed (or processed) by the destination process.
When discussing reachability analysis for the abcd-Example, we assumed (Assumption A1) that the message that was sent by the source during a transition of the source process was immediately put into a queue associated with the destination (called input queue), and the destination would consume the messages in the input queue in FIFO order.
One can often assume that the transmission of messages between a given source and destination has the FIFO property, that is, the messages are received in order. Note, however, that the order is normally not conserved when more than two processes are involved. The diagram below shows a very common situation where message m1 is sent before message m2, but m2 is received before m1 (due to a longer transmission delay from process B to A.
For the communication between two processes, if we have message reception in order, then Assumption A1 is justified, because it does not really matter whether the message waits while being transmitted or while sitting in the input queue. However, this is not true when messages may change their order during transmission (which is possible for IP packets transmitted between two computers).
The SDL specification language assumes that each state machine has a single input queue for all messages coming from different sources. Considering the message transmission example above and assuming that the behavior of agent A is given by the state machine in diagram (b) above, we see that there is a problem because the agent A expects message m1 first, but it finds m2 at the head of the queue. This is a case of an non-specified reception and the semantics of SDL foresees that in this case the message at the head would be dropped. We note that this problem would be solved by having two separate input queues, one for each source. In this case the receiving process can determine in which order it wants to consume messages from the different input queues and no message would be lost. Therefore many theoretical models of communicating FSMs assume that each FSM has a separate input queue for each source. SDL solves this problem by allowing the designer of the agent behavior to specify that a given type of message would be "saved", if it appears at the head of the input queue; this means that the next message in the input queue should be considered for consumption. The message at the head may be consumed in the next state that is reached if it is not "saved" in that state, too.
We note that a similar problem would arise if the transmission from B to A does not preserve the order of messages (e.g. message m4 is received before m1 in the diagram above). If an application has to operate in such an environment, one may introduce a message pool (instead of a set of message queues). Received messages would be buffered in the pool until the destination process is ready to consume the particular message. Such message pools are assumed to exist in certain specification languages, sometimes called "tuple space". They are also implemented in certain Web Service environments (e.g. IBM's WebSphere BPEL execution environment). We will use this concept later in the course when we talk about "deriving protocols".