27
$\begingroup$

I often hear phrases like 'true concurrency semantics' and 'true concurrency equivalences' without any references. What does those terms mean and why are they important?

What are some examples of true concurrency equivalences and what is the need for them? E.g. in which cases they are more applicable than more standard equivalences (bisimulation, trace equivalence, etc)?

$\endgroup$
23
$\begingroup$

The term "true concurrency" arises in the theoretical study of concurrent and parallel computation. It is in contrast to interleaving concurrency. True concurrency is concurrency that cannot be reduced to interleaving. Concurrency is interleaved if at each step in the computation, only one atomic computing action (e.g. an exchange of messages between sender and receiver) can take place. Concurrency is true if more than one such atomic action take place in a step.

The simplest way of distinguishing both is to look at the rule for parallel composition. In an interleaving based setting, it would look something like this:

$$\frac{P \rightarrow P'}{P|Q \rightarrow P'|Q}$$

This rule enforces that only one process in a parallel composition can execute an atomic action. For true concurrency, a rule like the following would be more appropriate.

$$\frac{P \rightarrow P'\quad Q \rightarrow Q'}{P|Q \rightarrow P'|Q'}$$

This rule allows both participants in a parallel composition to execute atomic actions.

Why would one be interested in interleaved concurrency, when concurrency theory is really the study of systems that execute computation steps in parallel? The answer is, and that's a great insight, that for simple forms of message passing concurrency, true concurrency and interleaving based concurrency are not contextually distinguishable. In other words, interleaved concurrency behaves like true concurrency as far as observers can see. Interleaving is a good decomposition of true concurrency. Since interleaving is easier to handle in proofs, people often only study the simpler interleaving based concurrency (e.g. CCS and $\pi$-calculi). However, this simplicity disappears for concurrent computation with richer forms of observation (e.g. timed computation): the difference between true concurrency and interleaved concurrency becomes observable.

Standard equivalences like bisimulations and traces have the same definitions for true and interleaving based concurrency. But they may or may not equate different processes, depending on the underlying calculus.

Let me give an informal explanation of why interleaving and truly concurrent interaction are indistinguishable in simple process calculi. The setting is a CCS or $\pi$-like calculus. Say we have a program

$$ P \quad=\quad \overline{x} \ |\ \overline{y} \ |\ x.y.\overline{a} \ |\ y.\overline{b} $$ Then we have the following truly concurrent reduction: \begin{eqnarray*} P &\rightarrow& y.\overline{a} \ |\ \overline{b} \end{eqnarray*} This reduction step can be matched by the following interleaved steps: \begin{eqnarray*} P &\rightarrow & \overline{x} \ |\ x.y.\overline{a} \ |\ \overline{b} \\ &\rightarrow & y.\overline{a} \ |\ \overline{b} \end{eqnarray*} The only difference between both is that the former takes one step, while the latter two. But simple calculi cannot detect the number of steps used to reach a process.

At the same time, $P$ has the following second interleaved reduction sequence: \begin{eqnarray*} P &\rightarrow & \overline{y} \ |\ y.\overline{a} \ |\ y.\overline{b} \\ &\rightarrow & \overline{a} \ |\ y.\overline{b} \end{eqnarray*} But this is also a reduction sequence in a truly concurrent setting, as long as true concurrency is not forced (i.e. interleaved executions are allowed even when there is potential for more than one interaction at a time).

$\endgroup$
  • $\begingroup$ Thanks, great answer! Can you please give me some references for further reading? $\endgroup$ – Daniil May 9 '13 at 13:14
  • $\begingroup$ @Daniil I'm afraid I don't have any good references handy. In part it's folklore, in parts it's been investigated in the early days of concurrency theory, before I started. If you like to do a bit of maths, you can establish basic results yourself. Take a simple process calculus, e.g. the asynchronous $\pi$-calculus, equip it with truly concurrent reductions and show that two processes in the new calculus are equated by your favourite (weak) notion of equivalence exactly when they are equated in the interleaving calculus. $\endgroup$ – Martin Berger May 9 '13 at 18:06
0
$\begingroup$

To say the truth, I was googling for an answer myself. What is the semantics here? We assign a meaning "transition system" to the description "process algebra"; i.e. meaning is the transition system that is generated from the initial system description using defined SOS rules. Thus, using interleaving semantics, we lose all the concurrent structure in the obtained transition system.

Another answer could be that it is not "observable difference" but the difference in "observability". Using an interleaving semantics, we can observe only linear runs; whilst, using true concurrency we may observe "concurrent runs" (cf W.Reisig'13 Petri nets book).

Still, I have some doubts on what I said above, and it would be interesting to hear deeper insights. I.e., using Lamport vector clocks, how much of relativity theory can be transferred to concurrency theory.

$\endgroup$
  • 1
    $\begingroup$ That the step from a concurrent program to a transition system can be made in a lossy way has been observed early on. John Reynolds formulated what is now known as Reynolds' criterion, to characterise when interleaving semantics is accurate for shared-variable concurrent programs. Vaughan Pratt investigated true concurrency as a model P 1986 and, together with Gordon Plotkin, showed when the partiality of the order on actions is observable P&P, 1987. $\endgroup$ – Kai Feb 6 at 10:33
  • $\begingroup$ @Kai, the references are very appreciated! I'll write them down in case the links will be broken: Vaughan Pratt, Modelling Concurrency with Partial Orders; G. Plotkin V. Pratt, Teams Can See Pomsets. > can be made in a lossy way Certainly, I just wanted to cleary separate concepts in "syntactical description/ semantics/ meaning". $\endgroup$ – Leonid Dworzanski Feb 6 at 14:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.