Product Operator

The second aspect of distributed programming we focused on is the problem of "true concurrency." That there is a need for taking into account true concurrency is probably more debatable than the need for studying communication. This is probably why only one half of the group took interest in my work on a product operator. Actually, each time I talk about that product, half people found the result interesting and half people claim that the problem does not exist to start with.

What is true concurrency, anyway? In many formalisms (including LTL, UNITY, TLA, ...), systems are described in terms of atomic actions, and concurrency is expressed through interleaving of those atomic actions. To express the fact that actions A and B occur in parallel, we say that that what actually occurs is one of "A then B" OR "B then A". In other words, nondeterminism is used to represent concurrency.

True concurrency (also called noninterleaved concurrency) is the case when A and B occur simultaneously. This case is not taken into account in the usual interleaved description. Should we care about true concurrency? That's where the debate begins. Some people say that overlapping of concurrent actions exists in the "real world", and that true concurrency is a way to make a mathematical model closer to reality. Other people say that, if overlapping of actions becomes an issue, then the grain of atomicity used in the model must be changed to something finer.

Following what Leslie Lamport said (I think it was during a TLA+ tutorial in Toulouse in September 1999): If you want true concurrency in your program, you can just add it. In other words, even in a formalism based on interleaving, like UNITY or TLA, you can always add a specific action, say AB, to represent the simultaneous execution of A and B. Then, what can happen is "A then B", "B then A" or "AB" and true concurrency is taken into account.

What I did, through the definition of the product operation, was to ask (and partially answer) the question: If additional statements are added to represent true concurrency, what happens? In other words, how different are the two models, with and without true concurrency. The answer I got (in the limited context of UNITY programs that use observation to communicate) is that both systems do not differ as much as we could expect.

Actually, the difference between a model with true concurrency, say TC, and a corresponding model without it, say IC, can be characterized by the properties that are true in IC but, because of true concurrency, false in TC. Note that any property true in TC should be also true in IC because of the case when true concurrency simply "doesn't happen".

Consider the following simple example, due to Philippe Queinnec. A system consists of two processes A, with a state variable a, and B, with a state variable b. Both variables a and b are initially zero. Each process does a single thing before it stops: it assigns its variable with value 1. In the interleaving model, both actions cannot take place at the same time and one process must assign its variable before the other. In other words, a state where a+b = 1 will occur. In UNITY, this is expressed by the property true leads-to a+b=1. This property is not true for the model with true concurrency, in which it is possible that both processes assign their variable at the same time. This leads-to property is an example of a property true in IC but not in TC.

I studied the case of distributed programs, described in UNITY, and that use observation mechanism to communicate. In this context, you can prove that safety properties like invariant (or always , see the discussion on substitution axiom) are the same in both models, and that the leads-to properties that are true in IC and not in TC must have a global and transient right-hand side (i.e., properties of the form p leads-to q will also be the same in both processes except, possibly, for properties where the predicate q is global (it references several processes) and transient (it becomes false after it was true)).

If you think of it, leads-to properties with a global transient right-hand side are not likely to appear in distributed systems specifications, because, in general, they cannot be observed. Therefore, for "useful" properties (invariants and observable leads-tos), systems IC and TC do not differ, and taking true concurrency into account or not is irrelevant.

Check the papers for the details of the product operator for true concurrency as well as the proofs of property preservation.

Michel Charpentier <>