Example (2): Asynchrony

In the previous example:

Alice -> Bob: integer;
Alice -> Carol: integer;

We have seen that there can be a sequencing at the source (sender) without having the corresponding sequencing in the targets (receivers). A simple variant of this is:

Alice -> Bob: integer;
Dave -> Carol: integer;

In this case even though it is written in a sequential order the sending itself cannot be done in this order: it is done by different senders so that it is most natural to consider this is just a way to write: the same thing can be written as:

Dave -> Carol: integer;
Alice -> Bob: integer;

This seems to invalidate the idea of "sequencing": anyway we often wish to write down interactions as they come into our mind, so let's not worry. Our "not worrying" in fact means something like the following: if we scribble

Alice -> Bob: integer;
Dave -> Carol: integer;
Bob -> Alice: string;

and this is the whole conversation then we as a reader consider it as meaning the conversation

Alice -> Bob: integer;
Bob -> Alice: string;

and the conversation:

Dave -> Carol: integer;

done in parallel. This "in parallel" can be written as

parallel {
  Alice -> Bob: integer;
  Bob -> Alice: string;
} and {
  Dave -> Carol: integer;
}

which means there are two conversations in parallel: one may consider this is a "normal form" of the original three lines. In the new, and more verbose, presentation, the conversation as a whole is given as the parallel composition of smaller conversations each of which is now sequenced. For example

Alice -> Bob: integer;
Bob -> Alice: string;

is sequenced depicting the situation Alice first sends Bob an integer and then Bob sends Alice a string.

Looks ad-hoc? Well there is a simple rule underlying all this. That rule says: if

(1) Alice (say) appears in one line and
(2) Alice appears in a later line (combined by the sequencing semicolon ";")

then Alice's respective actions are in fact sequenced.

So in particular if we write

Alice -> Bob: integer;
Alice -> Bob: string;

then we assume Alice sends to Bob one integer then she sends to him a string: there is indeed a sequencing.

In the next post we consider further (and somewhat subtle) examples of asynchrony.