A Decade of Concurrency Reflections and Perspectives

Frontmatter

Data-flow synchronous languages

Abstract

In this paper, we present a theory of synchronous data-flow languages. Our theory is supported by both some heuristic analysis of applications and some theoretical investigation of the data-flow paradigm. Our model covers both behavioural and operational aspects, and allows both synchronous and asynchronous styles of implementation for synchronous programs. This model served as a basis to establish the GC common format for synchronous data-flow languages.

Albert Benveniste, Paul Caspi, Paul Le Guernic, Nicolas Halbwachs

Process algebra with backtracking

J. A. Bergstra, A. Ponse, J. J. van Wamel

Some Chemical Abstract Machines

Abstract

This paper explains by a series of examples the use of the notion of a Chemical Abstract Machine. This is a framework for parallel computations which builds upon the chemical metaphor of Banâtre and Le Métayer. We first illustrate the CHAM style by describing the operational semantics of process calculi constructs. Then we apply our approach to the λ-calculus, designing a CHAM for the weak β-reduction with sharing, and specializing it into a CHAM for the call-by-need reduction strategy. Our last example is the π-calculus. We discuss the notions of “asynchronous” and “fully asynchronous” reductions, and some π-calculus encodings of the λ-calculus.

Gérard Boudol

Verification tools for finite-state concurrent systems

Abstract

Temporal logic model checking is an automatic technique for verifying finite-state concurrent systems. Specifications are expressed in a propositional temporal logic, and the concurrent system is modeled as a state-transition graph. An efficient search procedure is used to determine whether or not the state-transition graph satisfies the specification. When the technique was first developed ten years ago, it was only possible to handle concurrent systems with a few thousand states. In the last few years, however, the size of the concurrent systems that can be handled has increased dramatically. By representing transition relations and sets of states implicitly using binary decision diagrams, it is now possible to check concurrent systems with more than 10¹²⁰ states. In this paper we describe in detail how the new implementation works and give realistic examples to illustrate its power. We also discuss a number of directions for future research. The necessary background information on binary decision diagrams, temporal logic, and model checking has been included in order to make the exposition as self-contained as possible.

E. Clarke, O. Grumberg, D. Long

Linear logic on Petri nets

Abstract

This article shows how individual Petri nets form models of Girard's intuitionistic linear logic. It explores questions of expressiveness and completeness of linear logic with respect to this interpretation. An aim is to use Petri nets to give an understanding of linear logic and give some appraisal of the value of linear logic as a specification logic for Petri nets. This article might serve as a tutorial, providing one in-road into Girard's linear logic via Petri nets. With this in mind we have added several exercises and their solutions. We have made no attempt to be exhaustive in our treatment, dedicating our treatment to one semantics of intuitionistic linear logic.

Completeness is shown for several versions of Girard's linear logic with respect to Petri nets as the class of models. The strongest logic considered is intuitionistic linear logic, with ⊗, ⊸, &, ⊕ and the exponential ! (“of course”), and forms of quantification. This logic is shown sound and complete with respect to atomic nets (these include nets in which every transition leads to a nonempty multiset of places). The logic is remarkably expressive, enabling descriptions of the kinds of properties one might wish to show of nets; in particular, negative properties, asserting the impossibility of an assertion, can also be expressed. A start is made on decidability issues.

Uffe Engberg, Glynn Winskel

An introduction to the theoretical aspects of Coloured Petri Nets

Abstract

This paper presents the basic theoretical aspects of Coloured Petri Nets (CP-nets or CPN). CP-nets have been developed, from being a promising theoretical model, to being a full-fledged language for the design, specification, simulation, validation and implementation of large software systems (and other systems in which human beings and/or computers communicate by means of some more or less formal rules). The paper contains the formal definition of CP-nets and their basic concepts (e.g., the different dynamic properties such as liveness and fairness). The paper also contains a short introduction to the analysis methods, in particular occurrence graphs and place invariants.

The development of CP-nets has been driven by the desire to develop a modelling language — at the same time theoretically well-founded and versatile enough to be used in practice for systems of the size and complexity that we find in typical industrial projects. To achieve this, we have combined the strength of Petri nets with the strength of programming languages. Petri nets provide the primitives for the description of the synchronisation of concurrent processes, while programming languages provide the primitives for the definition of data types and the manipulation of their data values.

The paper does not assume that the reader has any prior knowledge of Petri nets — although such knowledge will, of course, be a help.

Kurt Jensen

Temporal verification of simulation and refinement

Abstract

The paper presents temporal logic methods for proving simulation and refinement relations between programs. After introducing the notions of fair transition systems and the specification language of temporal logic, we present proof rules for verifying properties of programs. We then define the relations of simulation and refinement between programs and relate them to inclusion relations between computations and observations of the compared systems.

We then show that these semantic definitions can be formalized in temporal logic by the use of the temporal and observational semantics formulas. This representation expresses simulation and refinement as implications between a pair of such formulas. We provide proof rules, based on the rules for verifying program properties. The proof rules are illustrated on several simple examples. Towards the end, we recognize the usefulness of having a stuttering robust version of temporal logic.

The second part of the paper presents a proposed temporal logic, called TLR, which is insensitive to stuttering. This logic is interpreted over sequences of sarnpling points, alternating between persistent and transient sample points. This logic possesses an idempotent next-time operator, which gives some insight into its stuttering robustness. We present a decision procedure and a complete axiomatic system for the propositional version of TLR. It is shown that, if all system variables are taken to be left-continuous, then most of the rules of regular temporal logic are still sound for TLR.

Finally, we present a stronger proof rule for refinement, and illustrate its use to prove refinement of two programs that cannot be done within the regular temporal logic framework.

Yonit Kesten, Zohar Manna, Amir Pnueli

Verification and specification of concurrent programs

Abstract

I explore the history of, and lessons learned from, eighteen years of assertional methods for specifying and verifying concurrent programs. I then propose a Utopian future in which mathematics prevails.

Leslie Lamport

Simulation techniques for proving properties of real-time systems

Abstract

The method of simulations is an important technique for reasoning about real-time and other timing-based systems. It is adapted from an analogous method for untimed systems. This paper presents the simulation method in the context of a very general automaton (i.e., labelled transition system) model for timing-based systems. Sketches are presented of several typical examples for which the method has been used successfully. Other complementary tools are also described, in particular, invariants for safety proofs, progress functions for timing proofs, and execution correspondences for liveness proofs.

Nancy Lynch

Relationships between models of concurrency

Abstract

Models for concurrency can be classified with respect to the three relevant parameters: behaviour/system, interleaving/noninterleaving, linear/branching time. When modelling a process, a choice concerning such parameters corresponds to choosing the level of abstraction of the resulting semantics. The classifications are formalized through the medium of category theory.

Mogens Nielsen, Vladimiro Sassone, Glynn Winskel

Interaction diagrams

Abstract

Interaction diagrams are graphic representations of concurrent processes with evolving access capabilities; in particular they illustrate the points of access and relations between them. The basic step of computation is the migration of an access point between processes. This paper explains interaction diagrams through a sequence of examples. Diagrams can be regarded as graphic counterparts of terms in the π-calculus and illuminate some interesting points on its construction.

Joachim Parrow

Algebraic theories for name-passing calculi

Abstract

In a theory of processes the names are atomic data items which can be exchanged and tested for identity, but which admit no other functions or predicates. A well-known example of a calculus for name-passing is the π-calculus, where names additionally are used as communication ports. We provide complete axiomatisations of late and early bisimulation equivalences in such calculi. Since neither of the equivalences is a congruence we also axiomatise the corresponding largest congruences. We consider a few variations of the signature of the language; among these, a calculus of deterministic processes which is reminiscent of sequential functional programs with a conditional construct. Most of our axioms have been shown to be independent. The structure of the systems reveals the symmetries of the calculi and equivalences since they differ only by a few simple axioms.

Joachim Parrow, Davide Sangiorgi

Initial algebra and final coalgebra semantics for concurrency

Abstract

The aim of this paper is to relate initial algebra semantics and final coalgebra semantics. It is shown how these two approaches to the semantics of programming languages are each others dual, and some conditions are given under which they coincide. More precisely, it is shown how to derive initial semantics from final semantics, using the initiality and finality to ensure their equality. Moreover, many facts about congruences (on algebras) and (generalized) bisimulations (on coalgebras) are shown to be dual as well.

Jan Rutten, Daniele Turi

Logical specifications of infinite computations

Abstract

Starting from an identification of infinite computations with ω-words, we present a framework in which different classification schemes for specifications are naturally compared. Thereby we connect logical formalisms with hierarchies of descriptive set theory (e.g., the Borel hierarchy), of recursion theory, and with the hierarchy of acceptance conditions of ω-automata. In particular, it is shown in which sense these hierarchies can be viewed as classifications of logical formulas by the complexity measure of quantifier alternation. In this context, the automaton theoretic approach to logical specifications over ω-words turns out to be a technique to reduce quantifier complexity of formulas. Finally, we indicate some perspectives of this approach, discuss variants of the logical framework (first-order logic, temporal logic), and outline the effects which arise when branching computations are considered (i.e., when infinite trees instead of ω-words are taken as model of computation).

Wolfgang Thomas, Helmut Lescow

Partial order based design of concurrent systems

Abstract

A partial order based graph model for concurrency is introduced, using hierarchical structured graphs with relations denoting concurrency, causal ordering, and temporal ordering. Both compositionally structured processes as well as partial order based structures describing the semantics of processes can be expressed in this unified framework. Thus we obtain a powerful calculus that allows to algebraically transform processes or to prove properties of them.

Apart from algebraic properties we also study state based properties of the process language, by means of assertional techniques. We use the combination of the two to derive, in a number of transformation and refinement steps, a distributed minimum weight spanning tree algorithm, in the style of Gallagher, Humblet, and Spira.

Job Zwiers, Wil Janssen

Backmatter