3 - Concurrent processes

Summary

INTERLEAVING

In order to be able to describe processes that occur in parallel, concurrently, we introduce the merge operator ||.

The process χ || y is the process that executes processes χ and y in parallel. If we assume

that the observation of an atomic action has no duration, and that two actions cannot happenn simultaneously, then it appears that in χ || y the atomic actions of χ are merged or interleaved with those of y: every time we either see the next action of χ, or the next action of y. Thus, in a || b (a,b ∈ A) we either see a first, followed by b, or we see b first, followed by a. We obtain the following identity:

a||b = ab + ba.

This approach to the merge operator is called arbitrary interleaving or shuffle in the literature. Notice that we do not assert that the first action has terminated when the second one starts. This can depend on the implementation of a process (on a sequential or a parallel machine). We can however, if we want to, explicitly state that two actions can overlap in time: if g and h are two events having some duration, we can introduce atomic actions begin(g), end(g), begin(h) and end(h), and then we can describe process g || h by

This process has begin(g)·begin(h)·end(g)·end(h) as one of its possible execution sequences.

Note that in this theory, we cannot mention time explicitly, contrary to theories like temporal logic.

In 3.1.2 we will expand the system BPA from chapter 2 with this merge operator. In order to specify the merge in finitely many equations, we need an auxiliary operator.