|
|
Past and Present Research on Theory of ConcurrencyMaciej Koutny |
If one were to ask whether there is a single common characteristics of the past and present research on concurrency theory carried out at Newcastle, then with little hesitation the answer would be that such a characteristic can indeed be found. For with very few exceptions, it was concerned with what is usually referred to as 'non-interleaving' or 'partial order' theory of concurrent systems. This particular approach was first applied in Newcastle by Peter Lauer and his group in the mid 1970s, and has since been used without a noticeable break until now. This document is an attempt to trace the work on concurrency at Newcastle over more than 20 years, and as such it has to be selective. It will concentrate on two models of concurrent systems, COSY and Petri nets, and a general theme of partial order semantics of non-sequential behaviour and their applications to the modelling and verification of concurrent systems.
The design of COSY [L74, L75a, LC, LTS] was influenced by the view that a language is both a natural and a powerful tool for expressing the semantics of dynamic systems. In the case of sequential systems, there already existed concepts in the formal language theory, such as automata and grammars, which provided suitable language descriptions. To model concurrent systems, however, further work was needed to support a similar framework. The route chosen at Newcastle was to consider a concurrent system as a composition of a collection of purely sequential subsystems, where a sequential subsystem consists of a number of events whose occurrences are constrained by the synchronic structure of the system. In the case of COSY, a sequential system is specified using a path expression which is a specification device introduced by Roy Campbell and Nico Haberman [CH]. For example,
a system which can, again cyclically, execute 'c' followed by 'b'. The 'a', 'b' and 'c' are themselves abstract representations of system's activities which are assumed to be atomic, i.e., they are indivisible and their execution is instantaneous.
A concurrent system is represented as a collection of sequential subsystems operating independently and synchronising their activities whenever it is necessary. The central part of the model is the synchronisation mechanism which specifies that an event can be executed by an individual subsystem only if it is executed synchronously by every other subsystem whose specification includes this event; if no such subsystem exists, then the former one is allowed to proceed with the execution. Using COSY syntax, we may specify a concurrent system consisting of the above two sequential subsystems thus.
Intuitively, it can perform (cyclically) two sequences of events, 'acb' and 'cab'. However, it may observed that the order in which 'a' and 'c' are performed is not a result of any synchronisation, but rather a decision to represent the behaviour using sequential (or total ) order of event occurrences. It is a very point at which the 'non-interleaving' and 'interleaving' approach to concurrency diverge. For the former decides to represent the behaviour represented by two sequences, 'acb' and 'cab', using a single partial order in which 'a' and 'c' are unordered and both precede 'b'. In this way, the spatial distribution of the subsystems present in the specification of a concurrent system can be reflected on the level of its abstract behaviours since events performed by the disjoint parts of the systems are not (directly) ordered. Similar comments apply to Petri nets and their partial order semantics.
The theory of COSY is therefore built on the view that a behaviour of a concurrent system is any partial order of event occurrences. The decomposition of a global system into sequential subsystems reduced the complexity of comprehension and validation of the system. It is interesting to note that the standard semantics of COSY used 'vector firing sequences' to represent partial orders of event occurrences [S79]. For example, the partial order described above would be represented as (ab,cb), thus representing the distribution of events among different subsystems even more explicitly. These ideas were further developed and the concept of various execution semantics (such as maximally concurrent execution) investigated [JLKD, JK86, JK91].
Another development of the COSY approach was the introduction of the high level COSY notation which provides a succinct representation of possibly large basic COSY specifications using indexed events and specific constructs capable of, e.g., generating a three dimensional cube of events [LTS,C82].
One of the main themes addressed in the first few years of research on COSY was the relationship between the structure and behaviour of a concurrent system. The idea was to find conditions on the static structure of a design which would be equivalent to the satisfaction of some important behavioural property, such as deadlock-freeness or adequacy (no event in a system can ever be prevented from possibly occurring in future). These conditions were developed for some types of syntactically restricted programs, and later the concept of adequacy-preserving transformations was also developed [S79, B82, K92b].
An important part of COSY related research was a computer-aided environment, BCS. It was based on the high level COSY notation, and was designed and implemented in a succession of SERC-funded projects in the early 1980s [H83].
Right from the begiining, COSY and its related theory have been applied to a number of synchronisation problems in the area of concurrent and distributed systems. Early examples include the "Cigarette Smoker's Problem" and "the Banker's Problem" [LC, LTD, LS81]. A significant amount of work was done investigating and solving a complex synchronisation problem proposed by Phil Merlin and Brian Randell, called the "Train Problem" [Shi79a, L85, K86]. COSY was also used to provide a means for the translation of sequential specifications into concurrent ones [LS79,J84], and to specify and prove correct a synchronisation skeleton for a Triple Modular Redundancy system [KM].
Other research on concurrency theory carried out at that time was an investigation into the semantics and the design of concurrent programs using atomic actions [B81, BR].
Over the years, a number of people worked at Newcastle on the development of the COSY model, including Eike Best, Roy Campbell, Yiannis Cotronis, Raymond Devillers, Hartmann Genrich, Brian Hamshere, Ryszard Janicki, Maciej Koutny, Peter Lauer, Luigi Mancini, Mike Shields, Piero Torrigiani and Phesany Wong (some of them as visiting researchers).
Petri Box Calculus (PBC) [BDH] - PBC is a formal model of non-sequential computation which combines concepts derived from two areas of concurrency theory, viz. Petri nets and process algebras. One of the motivations for introducing PBC was to provide a semantical tool for dealing with concurrent programming languages and algorithms. PBC is based on an algebra of process expressions, each expression having an associated Petri net called a box (with its standard Petri net transition firing rule). In addition to this, there exists a consistent semantics in terms of the rules of structural operational semantics
Petri net based programming notation [BH] - A related strand of research was concerned with providing a Petri net semantics of concurrent programming languages, such as occam; a novel programming notation, B(PN)2, was also proposed. Some other issues related to Petri net modelling of programming constructs, such as triple modular redundancy, were also investigated [H94].
Semantics of Nets with Priorities [BK92, K92a] - Giving a formal meaning to concurrent systems which employ priority specifications is often difficult; the work in this area provided a number of results characterising priority relation for different classes of nets, and different classes of priority relation (including dynamic priorities).
Extensions of the partial order model [JK93, JK94] - A related area of research, investigated in collaboration with Ryszard Janicki of the McMaster University, was that of the foundational aspects of concurrent behaviour. This work led to the introduction of a model of concurrency generalising causal partial orders. The approach proposed to include, in the semantical description of concurrent systems, some additional information about the relationship between actions capturing more closely the complex interactions in a concurrent environment (e.g., in the presence of priorities and exceptions).
Close international links established during the lifetime of DEMON were further strengthened within the Esprit Basic Research Working Group CALIBAN (Causal Calculi Based on Nets, No. 6067, 1992-1995) which involved essentially the same partners as DEMON. The main achievements of this follow-up project, as far as Newcastle was concerned, can be summarised as follows.
High Level PBC and the Box Algebra [BFFHKP, BK95a, BK95b, H96] - The development of the PBC model was consolidated at the basic Petri net level, and at the coloured Petri net level. Several consistency results between different levels of abstraction, and different semantical settings, were obtained. Moreover, these results led to an improved and fully compositional treatment of the concurrent programming notation B(PN)2 which was subsequently implemented in a computer-aided specification and verification tool, PEP. The PBC model was further developed in the sense that it was possible to find a common generalisation of PBC and other process algebras. The resulting model, called the Box Algebra, was provided with complete and consistent Petri net semantics and operational (derivation rules based) semantics. It was also possible to treat recursion in its most general form, and introduce a class of operators on Petri nets which guarantee a compositional behaviour of the resulting nets. Such an approach make the proposed way of combining nets and process algebras generic, since one can focus on those operators which can be given clear representation in the domain of Petri nets. This work is still in progress [BKD, KB]. The problem of deriving process expressions from nets and axiomatisations of net equivalences were investigated by Martin Hesketh [H97].
Basic properties of causality [JK95, JK97] - In the standard causality semantics of concurrent systems, one uses the independence relation as a basic tool to characterise relationship between distributed actions. In a more general approach, this independence relation needs to be replaced or augmented by weaker relationships. The results obtained were used to give a novel semantics to Petri nets with inhibitor arcs. This characterisation was later extended, and the synthesis problem for such nets solved by Marta Pietkiewicz-Koutny in [P97].
To summarise, the extensive involvement in two EU funded projects undertaken by leading European centres of Petri net research, provided a strong stimulus and focal point for the Newcastle group.
Ending this brief tour of the past research on concurrency at Newcastle, one should add that although COSY, Petri nets, and causal partial order semantics were of particular interest and importance, other models and related techniques have also been investigated at Newcastle. Notable examples include Temporal Logic [K91, D96, M94], Communicating Sequential Processes [P94, KMP] and Complexity of Concurrent Systems [S95] which were investigated by Zhenhua Duan, Maciej Koutny, Luigi Mancini, Ben Moszkowski, Giuseppe Pappalardo and Iain Stewart.
[B82] E. Best: Adequacy Properties of Path Programs. Theoretical Computer Science 18(1992), 149-171.
[BDH] E. Best, R. Devillers, J.G. Hall: The Petri Box Calculus: a New Causal Algebra with Multilabel Communication. Advances in Petri Nets 1992, G.Rozenberg (ed.), Springer-Verlag, Lecture Notes in Computer Science Vol. 609, 21-69 (1992).
[BDK] E. Best, R. Devillers, M. Koutny: Petri Nets, Process Algebras and Concurrent Programming Languages. To appear in Advances in Petri Nets (1998).
[BFFHKP] E. Best, H. Fleischhack, W. Fraczak, R.P. Hopkins, H. Klaudel, E. Pelz: A Class of Composable High Level Petri Nets. Proc. Petri Nets'95, Torino, G. De Michelis, M. Diaz (eds). Springer-Verlag, Lecture Notes in Computer Science Vol. 935, 103--120 (1995).
[BH] E. Best, R.P. Hopkins: B(PN)2 - a Basic Petri Net Programming Notation. Proc. of PARLE'93, Springer-Verlag, Lecture Notes in Computer Science Vol. 694, 379-390 (1993).
[BK92] E. Best, M. Koutny: Petri net semantics of priority systems. Theoretical Computer Science 94,1 (1992), 175-215.
[BK95a] E. Best, M. Koutny: A Refined View of the Box Algebra. Proceedings of the Petri Net Conference'95, G.De Michelis, M.Diaz (eds.), Springer-Verlag, Lecture Notes in Computer Science Vol.935, 1-20 (1995).
[BK95b] E. Best, M. Koutny: Solving Recursive Net Equations. Proc. ICALP-95, Springer-Verlag, Lecture Notes in Computer Science Vol.944, 605-623 (1995).
[BR] E. Best, B. Randell: A Formal Model of Atomicity in Asynchronous Systems. Acta Informatica 16(1981) 93-124.
[CH] R.H. Campbell, N. Haberman: The Specification of Process Synchronization by Path Expressions. Springer-Verlag, Lecture Notes in Computer Science Vol. 16 (1974), 89-102.
[C82] J.Y. Cotronis: Programming and Verifying Asynchronous Systems. PhD Thesis, University of Newcastle upon Tyne (1982).
[D96] Z. Duan: An Extended Interval Temporal Logic and a Framing Technique for Temporal Logic Programming. PhD Thesis, University of Newcastle upon Tyne (1996).
[H96] J.G. Hall: An Algebra of High-level Petri Nets. PhD Thesis, University of Newcastle upon Tyne (1996).
[H83] B.C. Hamshere: A Computer Based Environment for the Design and Analysis of Concurrent Systems: SIMULA Implementation of the COSY Notation. In Proc. of 11th Annula Conf. of SIMULA Users, Paris (1983).
[H97] M. Hesketh: On Synthesis of Box Expressions from Petri Boxes. Manuscript, University of Newcastle upon Tyne (1997).
[H94] R.P. Hopkins: Voting on Synchronous Communication. Proc. of PARLE'94, Springer-Verlag, Lecture Notes in Computer Science Vol. 817 (1994).
[JK84] R. Janicki: A Method for DEveloping Concurrent Systems. Lecture Notes in Computer Science Vol. 167, Springer (1984), 155-166.
[JK86] R. Janicki, M. Koutny: On Equivalent Execution Semantics of Concurrent Systems. In: Advances in Petri Nets 1986. Lecture Notes in Computer Science Vol. 266, Springer (1987), 179-190.
[JK91] R. Janicki, M. Koutny: Optimal Simulations, Nets and Reachability Graphs. In: Advances in Petri Nets 1991. Lecture Notes in Computer Science Vol. 524, Springer (1991), 205-226.
[JK93] R. Janicki, M. Koutny: Structure of Concurrency. Theoretical Computer Science 112 (1993), 5-52.
[JK94] R. Janicki, M. Koutny: Representations of Discrete Interval Orders and Semi-Orders. J. Inform. Process. Cybernet. EIK 30 3(1994), 161-168.
[JK95] R. Janicki, M. Koutny: Semantics of Inhibitor Nets. Information and Computation 123,1 (1995), 1-17.
[JK97] R. Janicki, M. Koutny: Order Structures and Generalisations of Szpilrajn's Theorem. Acta Informatica 34(5) (1997), 367-388.
[DJKL] R. Janicki, P.E. Lauer, M. Koutny, R. Devillers: Concurrent and Maximally Concurrent Evolution of Nonsequential Systems. Theoretical Computer Science 43(1986), 213-238.
[K86] M. Koutny: The Merlin-Randell Problem of Train Journals. Acta Informatica 23 (1986), 429-463.
[K91] M. Koutny: Axiom System Induced by CTL* Logic. Fundamenta Informaticae 14, 2(1991), 235-253.
[K92a] M. Koutny: Modelling Systems with Dynamic Priorities. In: Advances in Petri Nets 1992. Lecture Notes in Computer Science Vol. 609, Springer (1992), 251-266.
[K92b] M. Koutny: Adequacy-Preserving Transformations of COSY Path Programs. Theoretical Computer Science 94, 1(1992), 141-158.
[KM] M. Koutny, L. Mancini: Synchronizing Events in Replicated Systems. The Journal of Systems and Software 9(1989), 183-190.
[KMP] M. Koutny, L. Mancini, G. Pappalardo: Traces, Failures and Divergences in the Correctness of Communicating Replicated Processes. Formal Aspects of Computing 9 (1997), 119-148.
[KB] M. Koutny, E. Best: Operational and Denotational Semantics for the Box Algebra. Fundamental Study. Theoretical Computer Science (to appear in 1998).
[L74] P.E. Lauer: Path Expressions as Petri Nets, or Petri Nets with fewer Tears, Technical Report Memo MRM/70, Computing Laboratory, University of Newcastle upon Tyne (1974).
[L75a] P.E. Lauer: A Project to Investigate a Design Technique for Asynchronous Systems of Processes. Technical Report Memo MRM/89, Computing Laboratory, University of Newcastle upon Tyne (1975).
[L85] P.E. Lauer: A Simple Railway System. Springer-Verlag, Lecture Notes in Computer Science Vol. 207, (1985), 271-292.
[LC] P.E. Lauer and R.H. Campbell: Formal Semantics of a Class of High-Level Primitives for Coordinating Concurrent Processes. Acta Informatica 5(1975), 297-332.
[LTD] P.E. Lauer, P.R. Torrigiani, R.E. Devillers: A COSY Banker: Specification of Highly Parallel and distributed Resource management. Springer-Verlag, Lecture Notes in Computer Science Vol. 83 (1980), 223-239.
[LTS] P.E. Lauer, P.R. Torrigiani and M.W. Shields: COSY: A System Specification Language Based on Paths and Processes. Acta Informatica 12(1979), 109-158.
[M94] B. Moszkowski: Some Very Compositional Temporal Properties. Programming Concepts, Methods and Calculi. Elsevier Science B.V. (North-Holland), (1994) 307-326.
[P94] G. Pappalardo: Specification and Verification Issues in a Process Language. PhD Thesis, University of Newcastle upon Tyne (1994).
[P97] M. Pietkiewicz-Koutny: Transition Systems of Elementary Net Systems with Inhibitor Arcs. Proc. of 18th International Conference, ICATPN'97 Toulouse, Springer-Verlag, Lecture Notes in Computer Science Vol. 1248 (1997), 310-327.
[S79] M.W. Shields: Adequate Path Expressions. Springer-Verlag, Lecture Notes in Computer Science Vol. 70, 249-265 (1979).
[S95] I.A. Stewart: Reachability in Some Classes of Acyclic Petri Nets. Fundamenta Informaticae 23 (1995) 91-100.
N.B. When compiling the above reference list, only those contributions were included where (at least one) author was working at Newcastle at the time of its writing. It is therefore necessarily incomplete as far as, e.g., the theory of COSY or PBC are concerned. I have also omitted all references to work which appeared in the Departmental Technical report series, which are listed elsewhere.