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, , 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, 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 deterministic sequential processes Each will be abstracted as a sequence of ‘locks’ (denoted ) or ‘unlocks’ (denoted ) applied to shared resources (denoted with suffices and superfixes to distinguish them), so , as so one. Here each is an occurrence of a or a .
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, . The state of the system corresponds to a point in whose coordinate describes the state or ‘local time’ of the process.
We assume that each process starts at (local time) 0 and finishes at (local time) 1; the and actions correspond to sequences of real numbers between 0 and 1, which reflect the order of the s and s. The initial state is and the final state .
To look at a particular example more closely, we suppose and the two processes look like and . 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 with , but . In such a state, both and have acquired and not yet relinquished it, which is impossible since can only be viewed by at most on process at any time. Such states are in the forbidden region.
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 and as abbreviations for the Dutch terms Prolaag, short for probeer te verlagen, literally “try to reduce,” and Verhogen (“increase”).
Let be a set whose elements are called the semaphores. Each semaphore s is associated with an arity that is an integer . We suppose that for each integer , there exist infinitely many semaphores whose arity is . The only instructions are and , where is some semaphore. The terms, , of the language, called processes, are the finite sequences of instructions. When is a process and , an integer less or equal to the length of , we denote by the instruction of the process, in particular 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
as we discussed more informally earlier.
A PV program is a finite sequence of processes separated by the operator , which should be read run concurrently with.
For instance, is an example of a PV program made of two copies of a process, whilst
is an example made of two distinct processes.
(To be continued.)
This entry is partially adapted from the treatment of the idea in the following paper: