Tuesday 7 August 2007

Example (1): Asynchrony

The following is Matthew's example (well he had a few and this is the simplest one). To write it down we do not yet use our scribble notation: we borrow the standard notation people use for cryptographic protocols. We write down a signature using it.

participant Alice, Bob, Carol;

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

The first statement is declaration of three participants. Then it says Alice sends Bob an integer. Then it says Alice sends Carol an integer.

And that's it. What's a big deal about this description?

(By the way you may say we have not followed Decrees from those Initial Days: don't we also need to specify channels and operators in an interaction? We shall come back to this, but let me just note it is not that we are unfaithful: let's just say for now we are starting simple and concise.)

The question Matthew asked is this:
OK, I can see Alice does these two sendings in sequence: that makes sense. But how about the ordering of arrival events?
We are assuming here, as we should inevitably do so in most real-world settings, an asynchronous message transport such as TCP (and as in TCP we may also assume the preservation of order of messages when they are from a common source to a common target: but this point deserves a lot of discussions, and fortunately or unfortunately interesting discussions, so let's do not consider about it here, anyway this assumption is not needed).

So we assume asynchronous communication: but then since Bob and Carol are different participants, hence may as well be located in different sites, there is no guarantee that messages arrive at Bob's and Carol's in this order.

So we realise that these two simple lines are not as simple as it may look. Each interaction takes place in that vast expanse: a message should travel through it, which takes time and efforts if the latter usually hidden from users' eyes, in that expanse which to us looks as if it had been existing for eternity. So we may interpret the two lines above as follows:
Once upon a time, there were participants Alice, Bob and Carol. Alice sent two integers consecutively to Bob and Carol in this order: and Bob and Carol would receive these messages targeted for them, though we do not know the order of receptions, they would go over this expanse. And that is the end of this scenario, which happened a long time ago.
Since this is a scenario there is indeed no tense: it can be about something that has happened, it can be something which is happening (and there can be many instances of it) and it can be about what may take place in future. Anyway the scenario --- or signature --- says that there are two consecutive sendings and there are two unordered receptions of them.

So this is the story of the two line descriptions above --- indeed we have more discussions about these two lines, many more. But they can be left for later: this is enough for today. In this first example we have seen that we cannot ignore the existence of that expanse through which interactions travel through, though our expression of this understanding is done abstractly since we are interested in modelling.