Semantics and Analysis of Concurrency

2 Semantics and Analysis of Concurrency

2.1 Interleaving and Non-Interleaving models

The semantics community came back to these geometric considerations with the development of ``truly-concurrent'' semantics, as opposed to ``interleaving'' semantics. The base of the argument was that interleaving semantics, i.e. the representation of parallelism by non-determinism ignores real asynchronous behaviours that actually exist ⁵ : a | b where a and b are atomic is represented by the same transition system as the non-deterministic choice a then b or b then a (see Figure 5).

Figure 5: Interleaving semantics of a | b

Figure 6: A refinement of a | b

This fact creates problems in particular in static analysis of (asynchronous) concurrent systems in that interleaving builds a lot of uninteresting states in the modelisation, hence inducing a high cost in verification. This is called the state-space explosion problem. Some techniques exist now to circumvent part of the problem, actually mostly derived from truly-concurrent considerations (originally Petri nets in [Valmari, 1990] and Mazurkiewicz trace theory in [Godefroid and Wolper, 1991]). Another problem is that refinement, which is a very convenient technique in program analysis, is very difficult to apply in interleaving semantics, see [van Glabbeek and Goltz, 1989] for instance: suppose that action a is in fact non-atomic and is composed of two subactions c then d, then a | b in interleaving semantics is no longer equivalent to a then b or b then a. The path c then b then d is missing there (see Figure 6, the missing part is represented by the dashed line). This implies that interleaving semantics is bound to describe all atomic actions for the derived analyses to be correct, hence incurring a great complexity.

2.2 Higher-Dimensional Automata

Quite a few models for true-concurrency have appeared (see in particular the account of [Winskel and Nielsen, 1994]) but it is only in 1991 that geometry is proposed to solve the problem, in [Pratt, 1991]. The diagnosis is that interleaving is only the boundary of the real picture. a | b is really the filled-in square whose boundary is the non-deterministic choice a then b or b then a (the hollow square). The natural combinatorial notion, extension of transition systems, is that of a cubical set, which is a collection of points (states), edges (transitions), squares, cubes and hypercubes (higher-dimensional transitions representing the truly-concurrent execution of some number of actions). This is introduced in [Pratt, 1991] as well as possible formalizations using n-categories, and a notion of homotopy ⁶ . This is actually a combinatorial view of some kind of progress graph. Look back to Figure 1. Consider all interleavings of actions Pa, Pb, Va and Vb: they form a subgrid of the progress graph. Take as 2-transitions (i.e. squares in the cubical set we are building) the filled-in squares. Only the forbidden region is really interleaved. Cubical sets generalize progress graphs, in that they allow any amount of non-deterministic choices as well as dynamic creation of processes. These cubical sets are called Higher-Dimensional Automata (HDA) following [Pratt, 1991] because it really makes sense to consider a hypercube as some form of transition. Actually at about the same time, a bisimulation semantics was given in [van Glabbeek, 1991]. Notice that 2-transitions or squares are nothing but a local commutation relation as in Mazurkiewicz trace theory [Mazurkiewicz, 1986], independence relation as in asynchronous transition systems, see [Bednarczyk, 1988] and [Shields, 1985], as in trace automata (as used in e.g. [Kahn, 1974, Kahn and MacQueen, 1977]), as in transition systems with independence [Sassone et al., 1994], or (indirectly) as with the ``confluence'' relation of concurrent transition systems [Stark, 1989]. There are two more ingredients with HDA: the elegance and the power of the tools of geometric formalisations, and the natural generalisation to higher-dimensions (i.e. ``higher-order independence relation'' or n-ary independence relations).

The later semantic papers on the subject were very much influenced by [Pratt, 1991]. In 1992, homological methods (see [Mac Lane, 1963] for a start) for studying the properties of Higher-Dimensional Automata were advocated in [Goubault and Jensen, 1992] given that they provide computable invariants of homotopy (at least in the usual case). A semantics of CCS was also discussed in a suitable category of HDA (also studied in [Lanzmann, 1993]) together with a notion of bisimulation ⁷ . This homology theory is not the definitive one, in particular it cannot distinguish some situations which are quite simple. Some further work was needed and began in [Gaucher, 1997a] and [Gaucher, 1997b]. P. Gaucher recently extended his work by using strict globular w-categories (generalizing [Pratt, 1991]) to formalize the execution paths of a parallel automaton, see http://www-irma.u-strasbg.fr/~gaucher for his recent publications. He also defined three new homology theories which are more adequate than the one proposed in [Goubault, 1995a]. The first properties of these theories are now proven, in particular Hurewicz morphisms, are constructed, relating homotopy and homology. It is to be noted that at the very time this was written up, R. Brown from Bangor University and R. Steiner from Glasgow University made an important contribution very much related to this, in showing that the category of w-categories is equivalent to the category of cubical sets with connections and compositions (see [Brown and Higgins, 1981a] and [Brown and Higgins, 1981b] for an introduction).

More general languages were modeled in [Goubault, 1993] with HDAs. Then a few analyses of programs by abstract interpretation ([Cousot and Cousot, 1977] for a start) were designed: some earlier steps in [Cridlig and Goubault, 1993], then the automatic determination of a superset of possible schedules from the geometry of executions (i.e. histories of resource usage) in [Goubault, 1995a] and [Goubault, 1995b], some applications to model-checking in 1995 in [Cridlig, 1995] (for shared-memory programming languages), and in [Cridlig, 1996] (on CML, i.e. message-passing languages). A prototype Parallel Pascal Analyser has been implemented along these lines by R. Cridlig: http://www.dmi.ens.fr/~cridlig.

In ``On the classification of dipaths in geometric models of concurrency'' in a forthcoming issue of ``Mathematical Structure in Computer Science'', M. Raussen focusses on the determination of the dihomotopy classes in cubical complexes, deadlock detection and serializability (see next section) being only special cases. An algorithm is given for the 2-dimensional case and some ideas are given for solving the general case. In ``Loops, Ditopology and Deadlocks'' in the same issue, L. Fajstrup gives a geometric model of a truly-concurrent PV system of n processes with finitely many (nested) loops and proves that it suffices to study a finite number of deloopings of each loop to determine the unsafe region and the deadlocks. Hence the previous algorithm on deadlock detection of [Fajstrup et al., 1998] can be applied to these finitely many deloopings and give the precise unsafe area in concurrent systems with loops.

Some proposals have been made to use the scheduling information obtained from the HDA semantics to derive automatic parallelization algorithms. This has been fully treated for CCS in [Takayama, 1995], [Takayama, 1996].

2.3 Other geometrical models

Most of the models used since V. Pratt's article were based on some form of cubical set. Some more recent work, in [Fajstrup and Raussen, 1996] and [Fajstrup et al., 1998] in particular, introduced topological models, the local po-space models, generalizing the previous models, for being able to reason in a similar way as in ordinary algebraic topology, i.e. by reasoning directly on ``continuous'' shapes and not through their combinatorial representations (simplicial sets in general). Of course, as in the standard case, there is, as shown in [Fajstrup et al., 1999] again, a natural relationship between combinatorial and topological representations through a pair of adjoint functors, geometric realization and singular cube functors. The expected applications of this modelization, as well as some of the basic notions about ``directed homotopy'' and schedules are described in [Fajstrup et al., 1999]. More recently, V. Pratt proposed Chu Spaces (see for instance [Pratt, 1999]) as a model for concurrency, starting back to the failure identified in [Pratt, 1991] of the natural duality event/schedule, in interleaving semantics. V. Pratt in ``Higher-Dimensional Automata Revisited'' in a forthcoming issue of Mathematical Structures in Computer Science, develops this idea and expresses the HDA geometric model in terms of Chu spaces.

Some potentially related semantic models are the n-categorical formulations of [Buckland and Johnson, 1996] and some other recent combinatorial or categorical formulations in [Fiore et al., 1997], [Sassone and Cattani, 1996], [Sokolowski, 1998a], [Sokolowski, 1998b], [Sokolowski, 1998c].