nLab progress graph

Progress graphs

Idea.

Progress graphs are a simple model for a certain aspect of concurrency theory in Computer Science. The basic idea is to give a description of what can happen when several processes are modifying shared resources. Given a shared resource, $a$, we consider it as a semaphore which controls its behaviour with respect to processes. (This is a bit like the counter or token used in some old single track railway systems to prevent two trains being on the same stretch of line at the same time.) We are not worried exactly how the resource is used merely the ‘locking’ and ‘unlocking’ of the access to that resource. For instance, $a$ may be a shared variable, so a semaphore is used to ensure that only one process can write on it at a time. (Editing pages in the n-Lab is another example!)

Our system will have $n$ deterministic sequential processes $Q_1, \ldots, Q_n$ Each will be abstracted as a sequence of ‘locks’ (denoted $P$) or ‘unlocks’ (denoted $V$) applied to shared resources (denoted $a$ with suffices and superfixes to distinguish them), so $Q_i = R^1a^1_i.R^2a^2_i\ldots R^{n_i}a^{n_i}_i$, as so one. Here each $R$ is an occurrence of a $P$ or a $V$.

There is a natural way to understand the possible behaviours of the concurrent execution of these processes. We associate to each process a different coordinate direction in the topological space, $\mathbb{R}^n$. The state of the system corresponds to a point in $\mathbb{R}^n$ whose $i^{th}$ coordinate describes the state or ‘local time’ of the $i^{th}$ process.

We assume that each process starts at (local time) 0 and finishes at (local time) 1; the $P$ and $V$ actions correspond to sequences of real numbers between 0 and 1, which reflect the order of the $P$s and $V$s. The initial state is $(0,\ldots,0)$ and the final state $(1,\ldots, 1)$.

To look at a particular example more closely, we suppose $n = 2$ and the two processes look like $T_1= P a.P b.V b.V a$ and $T_2 = P b.P a.V a.V b$. This gives rise to the two dimensional progress graph below:

The shaded area in the picture represents those states that correspond to ‘mutual exclusion’. Suppose we look at a state $(x,y)$ with $Pb\lt x\lt Vb$, but $Pb\lt y\lt Vb$. In such a state, both $T_1$ and $T_2$ have acquired $b$ and not yet relinquished it, which is impossible since $b$ can only be viewed by at most on process at any time. Such states are in the forbidden region.

Formalising $PV$-programs

The PV language was introduced in 1968 by E. W. Dijkstra? as an example of a toy language allowing concurrent execution of sequential processes . The PV language offers only two instructions called ${P}$ and ${V}$ as abbreviations for the Dutch terms Prolaag, short for probeer te verlagen, literally “try to reduce,” and Verhogen (“increase”).

Let $S$ be a set whose elements are called the semaphores. Each semaphore s is associated with an arity that is an integer $\alpha_s\geq 2$. We suppose that for each integer $\alpha \geq 2$, there exist infinitely many semaphores whose arity is $\alpha$. The only instructions are ${P}(s)$ and ${V}(s)$, where $s$ is some semaphore. The terms, $\mathbb{P}$, of the language, called processes, are the finite sequences of instructions. When $\mathbb{P}$ is a process and $j$, an integer less or equal to the length of $\mathbb{P}$, we denote by $\mathbb{P}(j )$ the $j^{th}$ instruction of the process, in particular $\mathbb{P}(1)$ is the first instruction.

We will separate the instructions of a process by a dot, mostly in order to make them easier to read. For example we have the processes

$${P}(a).{V}(a)$$

$$P(a).P(b).V(a).V(b)$$

as we discussed more informally earlier.

Formalising $PV$-programs and their semantics

Definition

A PV program is a finite sequence of processes separated by the operator $\mid$, which should be read run concurrently with.

For instance, ${P}(a).{V}(a) | {P}(a).{V}(a)$ is an example of a PV program made of two copies of a process, whilst

$${P}(a).{P}(b).{V}(a).{V}(b) | {P}(b).{P}(a).{V}(b).{V}(a)$$

is an example made of two distinct processes.

(To be continued.)

References

This entry is partially adapted from the treatment of the idea in the following paper:

• Eric Goubault, Some geometric perspectives in concurrency theory,

and from

• Emmanuel Haucourt, Concurrency and Directed Algebraic Topology, Notes École Polytechique, Jan. 2010.