Coordination Programming: Mechanisms, Models and Semantics

The following sections are included:

• Preface

• Contents

Gamma was originally proposed in 1986 as a formalism for the definition of programs without artificial sequentiality. The basic idea underlying the formalism is to describe computation as a form of chemical reaction on a collection of individual pieces of data. Due to the very minimal nature of the language, and its absence of sequential bias, it has been possible to exploit this initial paradigm in various directions. This paper reviews most of the work done by various groups along these lines and the current perspectives of our own research on Gamma. For the sake of clarity we separate the contributions in three categories: (1) the relevance of the chemical reaction model for software engineering, (2) extensions of the original model and (3) implementation issues.

Coordinating autonomous, possibly heterogeneous agents requires, at least, a flexible communication infrastucture allowing interactions between the coordinated entities (called the “participants”), respecting their autonomy and capable of dealing with their heterogeneity. Shared dataspace communication models, such as Linda¹, fulfill these requirements. In such models, for each coordinated entity, a piece of code interfacing the entity with the shared dataspace must be provided. The advantage of this approach is that each of these interfaces can be written with whatever languages and systems are most suited to the entity which they interface. However, a drawback is that the coordination code must be incorporated inside these interfaces, and none of them, being attached to individual participants, have a global vision of what the coordinated behavior should be. By analogy with an orchestra, one cannot expect the different players to coordinate their activities simply by listening to the output of the rest of the group; a conductor, who has a global vision of the expected coordinated behavior, is needed.

In this paper, we present an overview of the work based on the LO coordination model, aiming at simplifying the design of coordinators, seen as “software conductors”. Coordination in LO is specified declaratively using rules. On the one hand, rules are well suited to the kind of flexible synchronization constraints required by coordination. On the other hand, they manipulate only high level properties of the participants, abstracting away the complexity due to their heterogeneity. This complexity is transfered into the interfaces in charge of publishing the properties of the participants.

Rules are a powerful programming concept which can be understood in many different ways. Two concrete coordination programming systems have stemmed from the LO framework, adopting different views of rules. One, called ForumTalk adopts a “re-active” reading of rules, and considers participants as clients to the coordination service. Communication between the clients and the coordination service is purely asynchronous. The other system called the CLF adopts, on the contrary, a “pro-active” reading of rules where the participants become servers to the coordination activity. The two systems are presented in detail here.

We propose a computation model based on the separation between truth and action. The state of an agent is considered to consist of two components: the task, representing actions to be performed, and the database, representing certain truths. The task specifies a composition (parallel, sequential, choice, synchronous) of elementary actions: queries and commands. Queries may only be executed when certain truths are entailed by the database. Commands always execute and as an effect may change the database. We thus have the osmosis metaphor: the task and database are separated as if by a membrane through which information flows in both directions causing the system to evolve. Truth may enable actions (queries) to be accomplished, and actions (commands) may change what is true. Commands are assumed to have a deterministic nature. We discuss the fundamental semantic properties needed for accommodating this basic model, and consider extensions to accomodate named tasks and their refinement rules, variables in tasks, and systems of named agents with separate rules and databases.

Models for generative communication use a common space, where concurrent agents put or retrieve data; data extraction is controlled by various kinds of filtering techniques, usually based on the structure of the data itself. However, for higher-order communication, i.e. when the data consists of software fragments, such techniques are not appropriate: structural information does not reflect the behaviour of a software fragment. This paper studies a filtering mechanism based instead on type information, so that software components can be retrieved according to type specifications. A rich type system with polymorphism and subtyping gives enough flexibility to formulate type specifications at various levels of detail.

We provide a temporal logic semantics for the multiset rewrite language Gamma.

Despite some problems with expressing program stuttering, we are able to use Lamport's Temporal Logic of Actions to describe the behaviour of Gamma programs.

We then give a detailed description of how the semantics can be used to formally reason about program properties. This description consists of details of the formal language required, the various levels of proof theory and an example of the use of the formal system in proving a total correctness result.

We take a systematic approach to the construction of a program logic for Gamma, by applying Abramsky's domain theory in logical form to a denotational semantics of the language. Starting from a resumption semantics of Gamma, we are able to derive both the formulae and the proof system of the transition assertion logic previously proposed by Errington, Hankin and Jensen. The general theory enables us to prove soundness of the logic, although completeness fails because the resumption semantics of Gamma is not fully abstract. At the end of the paper we discuss the possibilities for obtaining a complete logic.

The GAMMA formalism is a programming model based on the nondeterministic rewriting of multisets. Programs in this formalism are expressed with a minimum of control, which makes the model very well-suited for writing parallel programs at a high level of abstraction. In the implementation, however, the chaotic behaviour of GAMMA programs poses serious problems. To overcome these problems, we introduce in this paper a language that can be used to effectively control the nondeterministic behaviour. We show that the language is expressive enough to describe the complete spectrum, ranging from chaotic behaviour to deterministic algorithms. An important property is that the control information is specified separately from the program text. This allows control issues to be treated separately from the logic of a program.

This article studies composed reduction systems: systems of programs built up from the reduction relations of some reduction system, by means of parallel and sequential composition operators. The Calculus of Gamma Programs previously studied by Hankin et al are an instance of these systems in the case where the reduction relations are a certain class of multi-set rewriting relations. The trace-based compositional semantics of composed reduction systems is considered, and a new graph-representation is introduced as an intermediate program form which seems well-suited to the study of compositional semantics and program logics.

The Gamma model is a minimal programming notation based on the chemical reaction metaphor. Hankin, Le Métayer, and Sands derived a Calculus of Gamma Programs adding two operators to the notation: the parallel and sequential composition operators. In this paper we address some compositional problems due to the semantics of the parallel operator for which we propose an alternative semantics as a solution to these problems. The semantics of the new version of the calculus is also defined by means of a labeled transition system. This permits the definition of some observational equivalences. We introduce two of them using the concept of bisimulation. The equivalences are proved to be congruences and are characterized by means of sound and complete axiomatizations.

Using the methodology of abstract logic programming in linear logic, we establish a correct and complete translation between the language NABLA and first order linear logic. NABLA is a modification of the coordination language GAMMA with parallel and sequential composition. NABLA, without modifying GAMMA basic computational model, is amenable to this kind of analysis, at the price of a weaker expressive power. The translation is correct and complete in the sense that we establish a two way correspondence between computations in NABLA and the search for proofs in a suitable fragment of first order linear logic. Moreover, the translation is not an encoding, meaning that to the algebraic structure of NABLA programs is assigned logical meaning through a non-trivial use of linear logic connectives, as opposed to merely reflecting their operational behavior through a simulation into terms of the logic. In this way we hope that the connection established between the two formalisms can compensate for the diminished expressive power of NABLA with a powerful analysis tool, which could lead both to theoretical and practical improvements in semantic foundations of GAMMA-style languages and in the design of efficient implementations of their interpreters. The main difficulty has been to deal with sequential composition of programs, and to smoothly integrate its logical treatment in a recursive framework. An intermediate step is the definition of the language SMR, by which it is possible to specify in a very intuitive way NABLA operational semantics, and to prove that this specification is actually equivalent to the SOS-style one derived from GAMMA semantics.

In this report we investigate the use of Higher-Order Gamma as a specification language for software architectures. In particular, we specify the run-time system of a reflective and distributed implementation of the coordination language LO.

The clients and servers of LO's run-time system are modeled as embedded Gamma systems. Several alternative architectures are investigated. Not only the individual components of a distributed architecture, but also their interfaces are concisely captured by the specification. Furthermore the Higher-Order Gamma specification, consisting of a hierarchy of embedded Gamma systems, clarifies the concept of reflection.

An additional advantage of using Gamma comes from the work on program composition and transformation. Starting from highly parallel initial specifications, we refine the Higher-Order Gamma program until the individual clients and servers are entirely sequential. Every remaining parallel thread corresponds to a different client or server. Thus we end up with a specification which truthfully mirrors the parallelism available in a distributed system running on a number of sequential machines.

This report investigates how coordination languages can be made practical. We focus on one aspect of this problem: How can we rapidly design and evaluate the software architecture of alternative run-time systems for a coordination language? The plethora of architectures for distributed systems, from master/slave to client/server, from proxy-based to replicated, shows that there is no good general solution. Starting from the observation that no single run-time architecture suits a wide enough range of distribution requirements, we propose a reflective framework. We gradually show how a basic architecture can be modularly adapted to achieve our goal. Most importantly, decisions on architectural trade-offs can be delayed until sufficient knowledge about the target architecture and application is available, thus avoiding premature (and suboptimal) design commitments.

Based on extensive experimentation, we analyze the costs and the benefits of the reflective approach. As it turns out, the price we pay is perfectly reasonable for the increased modularity and flexibility it buys.

We describe Gammalög, a logic language based on multiset rewriting. The language combines the ability of describing parallel programs made of multiset transformation rules, as in Gamma, with the execution model of logic programming in a strongly typed framework, as in Gödel. We present the design choices, the language syntax, and its formal semantics. Gammalög provides a standard model theoretic semantics expressed in terms of multiset rewritings; soundness and completeness results are proved with respect to extended SLD resolution. Finally, we present a prototype implementation of a compiler for Gammalög: it is based on the original Gödel implementation, which has been extended to support first class multisets.

ConCoord is an environment for programming networks of sequential and parallel machines, namely heterogeneous concurrent systems. ConCoord contributes in two ways to concurrent programming. First, it provides explicit and dynamic manipulation of a diversity of concurrency grains which can be supported efficiently on a concurrent system. Second, ConCoord simplifies the programming task by separating the treatment and reuse of sequential and concurrent aspects of programming into computation and coordination respectively. In this paper, we start by discussing ConCoord's main motivation. Afterwards, we define the features of ConCoord that will be used in this paper examples. This definition is followed by two programming examples which illustrate the manipulation of two different concurrency grains and show ConCoord's support for reuse. Next, we compare ConCoord with other approaches for coordinated programming. In the conclusions, we summarise the current state of ConCoord and future work.

We discuss the advantages for methodology and software engineering afforded by extending Gamma with chromatic typing. Chromatic typing is a typing discipline orthogonal to both tagging and sub-typing. Chromatic typing improves the readability, modularity and efficiency of Gamma programs and makes them easier to debug. We give the rules for chromatic type inference and a number of examples to demonstrate the usefulness of the approach. Our examples are programs for generating fractal objects similar to certain biological structures. The advantages are twofold: firstly, we gain an expanded suite of Gamma programs and, secondly, we demonstrate that fractal growth is an application area within which interest in Gamma programming may be generated. Coding the examples in Gamma leads to a number of insights into the advantages and disadvantages of the formalism and into programming therein. We also discuss an extension to chromatic typing which enables I/O to be accommodated in a natural way.