Mathematical Models for the Semantics of Parallelism

A flexible abstraction mechanism for models of concurrency, which allows systems which “look the same” to be considered equivalent, is proposed. Using three classes of atomic observations (sequences of actions, sequences of multisets of actions and partial orderings of actions) different information on the causal and temporal structure of Event Structures, a basic model of parallelism, is captured. As a result, three different semantic models for concurrent systems are obtained. These models can be used as the basis for defining interleaving, multisets or partial ordering semantics of concurrent systems. The common framework used to define the models allows us to study the relationship between these three traditional approaches to the semantics of concurrent communicating systems.

Operational and denotational semantic models are designed for languages with process creation, and the relationships between the two semantics are investigated. The presentation is organized in four sections dealing with a uniform and static, a uniform and dynamic, a nonuniform and static, and a nonuniform and dynamic language, respectively. Here uniform/nonuniform refers to a language with uninterpreted/interpreted elementary actions, and static/dynamic to the distinction between languages with a fixed/growing number of parallel processes. The contrast between uniform and nonuniform is reflected in the use of linear time versus branching time models., the latter employing a version of Plotkin's resumptions. The operational semantics make use of Hennessy and Plotkin's transition systems. All models are built on metric structures, and involve continuations in an essential way. The languages studied are abstractions of the parallel object-oriented language POOL for which we have designed separate operational and denotational semantics in earlier work. The paper provides a full analysis of the relationship between the two semantics for these abstractions. Technically, a key role is played by a new operator which is able to decide dynamically whether it should act as sequential or parallel composition.

An outline is presented of the SMoLCS methodology for the specification of concurrent systems and languages. Its main novelties lie in a high level of modularity and parameterization and in the fact that, within the same homogeneous framework, functions, data types and concurrency can be handled together. Indeed a concurrent system is algebraically specified as an abstract data type obtained by instantiating a parameterized schema (a parameterized abstract data type) for defining and composing process specifications. The semantics of a language is given by a two-steps approach, which keeps an overall denotational flavour, but can be seen just as another algebraic specification. A metalanguage schema is naturally associated with the methodology, consisting of an algebraic and of an applicative kernel. Relying on the overall algebraic structure, tools have been developed for rapid prototyping of specifications of concurrent systems and languages.

A number of distinct views of distributed systems and ways for their formal modelling are explained, discussed, and related. By this, in particular, an attempt is undertaken to unify and show the connection between distinct approaches to formalizing distributed systems and programs describing them.

A new class of Petri Nets, called Augmented Condition/Event Systems is defined, by slightly relaxing the condition for enabling events. One system, called Σ_CCS, from this class is used to give a new operational semantics to Milner's Calculus of Communicating Systems. The set of CCS agents together with the traditional, interleaving based, derivation relation is proved isomorphic to the case graph of Σ_CCS (when single transitions only are considered). Our achievement is twofold: first, we provide CCS with a semantics which is able to describe concurrency and causal dependencies between the actions the various agents can perform; second, we guarantee an adequate linguistic level for the particular class of Petri Nets which can be defined through CCS operators.

In the first part of the paper we show how to construct categorical models for Milner's CCS [Mil80], Hoare's CSP [Hoa78], and similarly defined calculi for synchronized and parallel computations.

We consider a generic category C of processes with morphisms which are labelled by strings of actions belonging to a monoid A. We define the synchronization between two processes in C as a functor (if it exists) from a subcategory of C × C into C. We introduce the notions of categorical semantics and good categorical semantics for processes.

In the second part of the paper we show that the Categories of Trees we will define, is optimal for most synchronizations described in the literature. That result is presented also in the framework of the Enriched Category Theory [Law74] for indicating its meaning in terms of an internal logic [Law74].

The thesis we present in this paper states that for every concurrent program π there exists a set of modal formulas, also called the axioms Ax(π), such that a) the structure of admissible parallel executions of the program π is a Kripke model of the set Ax(π) and, b) any Kripke model of the axioms Ax(π) is an extension of the structure of all admissible distributed (i.e. parallel) executions of the program π.