nLab progress graph

Progress graphs

Contents

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, aa, 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, aa 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 nn deterministic sequential processes Q 1,,Q nQ_1, \ldots, Q_n Each will be abstracted as a sequence of ‘locks’ (denoted PP) or ‘unlocks’ (denoted VV) applied to shared resources (denoted aa with suffices and superfixes to distinguish them), so Q i=R 1a i 1.R 2a i 2R n ia i n iQ_i = R^1a^1_i.R^2a^2_i\ldots R^{n_i}a^{n_i}_i, as so one. Here each RR is an occurrence of a PP or a VV.

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, n\mathbb{R}^n. The state of the system corresponds to a point in n\mathbb{R}^n whose i thi^{th} coordinate describes the state or ‘local time’ of the i thi^{th} process.

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

To look at a particular example more closely, we suppose n=2n = 2 and the two processes look like T 1=Pa.Pb.Vb.VaT_1= P a.P b.V b.V a and T 2=Pb.Pa.Va.VbT_2 = P b.P a.V a.V b. This gives rise to the two dimensional progress graph below:

<inkscape:perspective id='perspective10' inkscape:persp3d-origin='372.04724 : 350.78739 : 1' inkscape:vp_x='0 : 526.18109 : 1' inkscape:vp_y='0 : 1000 : 0' inkscape:vp_z='744.09448 : 526.18109 : 1' sodipodi:type='inkscape:persp3d'></inkscape:perspective> <sodipodi:namedview bordercolor='#666666' borderopacity='1.0' gridtolerance='10000' guidetolerance='10' id='base' inkscape:current-layer='layer1' inkscape:cx='246.70904' inkscape:cy='508.22482' inkscape:document-units='px' inkscape:pageopacity='0.0' inkscape:pageshadow='2' inkscape:window-height='701' inkscape:window-width='663' inkscape:window-x='0' inkscape:window-y='22' inkscape:zoom='0.35355339' objecttolerance='10' pagecolor='#ffffff' showgrid='true'> <inkscape:grid enabled='true' id='grid2383' type='xygrid' visible='true'></inkscape:grid> </sodipodi:namedview> <rdf:RDF> <cc:Work rdf:about=''> <dc:format>image/svg+xml</dc:format> <dc:type rdf:resource='http://purl.org/dc/dcmitype/StillImage'></dc:type> </cc:Work> </rdf:RDF>

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

Formalising PVPV-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{P} and V{V} as abbreviations for the Dutch terms Prolaag, short for probeer te verlagen, literally “try to reduce,” and Verhogen (“increase”).

Let SS be a set whose elements are called the semaphores. Each semaphore s is associated with an arity that is an integer α s2\alpha_s\geq 2. We suppose that for each integer α2\alpha \geq 2, there exist infinitely many semaphores whose arity is α\alpha. The only instructions are P(s){P}(s) and V(s){V}(s), where ss 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 jj, an integer less or equal to the length of \mathbb{P}, we denote by (j)\mathbb{P}(j ) the j thj^{th} instruction of the process, in particular (1)\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).{V}(a)
P(a).P(b).V(a).V(b)P(a).P(b).V(a).V(b)

as we discussed more informally earlier.

Formalising PVPV-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){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){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:

and from

Last revised on December 3, 2010 at 18:32:04. See the history of this page for a list of all contributions to it.