Members of the Concurrency Working Group met at MIT on June 14-15, 1996. What follows is a first draft of the working group report, assembled mainly from notes taken during the group meetings. The report contains three sections: an introductory section that defines concurrency and highlights some of the major issues in the area, a section that presents the state-of-the-art in concurrency research, and a final section that gives strategic directions.
Concurrency is concerned with the conceptual and fundamental aspects underlying any system employing multiple computing agents and possessing some infrastructure to allow these agents to communicate. We refer to such systems as concurrent systems, a notion that spans a wide range of system architectures: from tightly coupled, mostly synchronous parallel systems, to loosely coupled, largely asynchronous distributed systems. Similarly, we refer to computer programs written for concurrent systems as concurrent programs.
Concurrent programs may be contrasted with sequential programs written for single-cpu systems in languages such as C, C++, Lisp, and Fortran, performing traditional tasks such as sorting, searching, text editing, and financial accounting. Concurrent programs may be written in languages with special support for concurrency, such as Ada95, occam, and SR, or in a language such as C, relying on system calls to the operating system to deal with concurrency-related matters.
At some intrinsic level, concurrent programs are much more difficult to analyze for correctness than their sequential counterparts, owing to the multiple threads of control present in a concurrent system. Issues such as interference, race conditions, deadlock, and livelock are peculiar to concurrent programming. Attempting to keep track of the different "global states" of a concurrent program gives rise to the state space explosion problem.
When dealing with concurrent programs we must also be careful to define what we mean by "correctness." In the sequential case, program correctness is expressed in term of partial (the program produces the expected output) and total correctness (the program terminates on all inputs). This notion of correctness remains appropriate for a concurrent program representing a "parallelized" version of some sequential program; in this case, concurrency (parallelism) has been introduced solely for performance purposes.
There exists, however, an important class of concurrent programs known as reactive systems for which concurrency is in some sense fundamental, and the sequential correctness criteria no longer apply. In particular, a correctly behaving reactive system never terminates; rather it engages in a continual interaction with its environment, reacting to stimuli supplied by the environment. Examples of reactive systems include operating systems, database systems, and air-traffic control systems.
The correctness of a reactive system is given by a collection of safety (nothing bad ever happens) and liveness (something good eventually happens) properties. Typical safety properties are mutual exclusion, which stipulates that no more than one process may occupy its critical section at any moment in time, and the absence of deadlocks. A typical liveness property is of the form: "a request for service is eventually granted." Note that the safety and liveness characterization of correctness is not limited to software but rather all types of concurrent systems, including hardware.
To avoid confusion, the term "concurrency" should be contrasted with the term "concurrency control." The latter deals with simultaneous access to a database by multiple users. A properly designed concurrency control mechanism will ensure that user transactions do not interfere with one another, even if they try to access the same data at the same time. Indeed, concurrency control is a prime example of a concurrency-related problem.
Concurrency research falls into six major categories: models, logics, languages, algorithms and methodologies, tools, and applications.
There is a basic agreement between the different schools of thought: Models of concurrent systems need to to be non-functional. It is not sufficient to just capture their input-output behavior; their models have to be less abstract than mathematical functions. It is necessary to take into account the fact that systems do not run in isolation but interact with other systems; thus patterns of stimuli/response relationships varying over time have to be used for their modeling. Starting from the basic notion of atomic action, representing a generic "uninterpreted operation", the behavior, or computations of systems are defined in terms of these atomic unit of changes for many models of concurrency.
Here we want to to list just a few of these models. One of the most used one is that of (Finite State Automata), possibly extended by adding to the basic actions information about their type (I/O Automata), or by extending states with the additional structure of set to reflect their spatial distribution (Petri Nets). Another widely used models, directly inspired by automata is that of Labeled Transition Systems. Alternative models, directly based on atomic actions are sets of sequences of actions (Hoare's Traces), that might be structured as trees (Synchronization Trees), or might be prefix closed sets but with additional information about the reaction to external request (Acceptance Trees or Refusal Sets). Sets of sequences of actions might be also equipped with with an independence relation between actions (Mazurkievicz's Traces), to capture possible concurrency. To this purpose, atomic actions are in other cases used as labels of partially ordered sets of events (Pomsets), possibly enriched with a conflict relation (Labeled Event Structures).
The difference between all of these models can be understood in terms of the decision has been taken with respect to the following three dichotomies:
1. Intentional models (like a labeled transition system or a Petri nets) require explicit description of systems states and their states changes determined by the execution of specific actions. The intentional models, like Hoare's traces, synchronization trees or event structures, concentrate just on the pattern of possible interactions over time.
2. Within the interleaving approach, the basic assumption of sequential observations is made and the execution of parallel actions is reduced to nondeterministic interleaving (the presence of any concurrent actions is rendered as the choice between their sequential execution). The truly concurrent models assume instead concurrency as fundamental notion, the behavior of systems is represented by expliciting the causal relations among the events performed by the components of distributed states (actions that are not causally related are concurrent) or by describing the location at which the action take place.
3. The difference between branching time models and linear time ones lies in the way they deals with the choice that systems might have to face during their execution. In the former case the point of execution where choice are taken is considered as important while in the latter it is not. Thus, models that do not respect branching time describe concurrent systems in terms of the sets of their possible (partial) runs while in branching time models the point of divergence of different computation is always recorded. Hoare's traces and pomsets are linear time models while synchronization trees and labeled event structures are branching time models.
Due to the great variety of aspects to be taken into account, different decisions about the three dichotomies are appropriate for different purposes.
These notions, especially when defined over models that are equipped with operators that permit "hiding" of some of the performed actions, make it possible to relate different systems and to prove their properties.
The same formalism can be used to describe both specifications and implementations of a system, and correctness of an implementation with respect to a specification can be determineded by establishing their behavioural equivalence.
Behavioural preorders, can be use to prove that a stepwise refinement of a loose specification into a fully specified one is correct by establishing that a sequence of transformations preserves correctness.
Correctness (with respect to) a behavioural relation can be also used to minimize a model before analizing it or before using it for other purposes, e.g. before using it as a basis for model checking logical formulae describing systems properties.
Different opinions about which ones are the relevant aspects of concurrent systems, and thus about which ones are those that can be ignored, have led to a number of behavioral equivalences or preorders. Also in this case one could see the three dichotomies, Intentional vs Extentional, Interleaving vs True Concurrency, Branching vs Linear Time, mentioned above.
Indeed, we can divide the different relations proposed in the literature in two main classes, namely those based on bisimulation, that require some knowledge of the internal structure of the modeled systems, and those based on Extentional Testing that just compare the outcomes of external experiments on systems in order to decide whether they are equivalent or whether they are related via a semantic preorder. One could say than that bisimulation is somehow extensional while testing is extensional.
The choice between having interleaving or true concurrency based equivalence is instead determined by deciding the grain of actual observations. One can have observations consisting of single atomic actions, or of sequence thereof, or of structured sets of atomic actions, etc. Then, weak bisimulation, that ignores the possible concurrency of actions is an interleaving equivalence, while history-preserving bisimulation, that assumes that partial orderings of actions are observable, permits distinguishing systems with different causal relations between actions.
The choice between linear and branching time is determined by decision about the way successive experiments are structured, e.g. by deciding whether all experiments have to start from the initial state, whether intermediate experiments are possible, whether experimenters can make copies of the system under examinations, etc. Thus, the classical Nerode equivalence for automata can be retrieved by only allowing considering the accepted sequences of experiments, while branching time semantics, like that based on bisimulation, can be obtained by having fully interactive observations.
Bisimulation based equivalences are certainly the best known ones. Intuitively, two systems are bisimulation equivalent whenever they can perform the same sequence of actions to reach bisimulation equivalent states. Testing based equivalence are instead based on comparing the outcome of experiments by external observers rather than directly comparing systems computation. By changing the set of the external observers and the way of organizing the outcome of observations different relation can be obtained, that range from the classical trace equivalence of finite state machines, to the failure equivalence that can also be obtained via Refusal Sets. Even bisimulation based equivalence can be obtained, if experimenters can make an unbounded number of copies of the systems they are experimenting on.
??? NOT SURE WHETHER RELEVANT. It depends on what is written in the other section. ???
In parallel with the definition of behavioral equivalences, different attempts have been made towards defining (modal and temporal) logics that permit specifying specific properties of concurrent systems. The logics having the advantage over behavioral equivalences of not always requiring to specify the full behavior of a system; they permit one to concentrate on specifying particular properties of a system, like safety, fairness, etc., that are of interest.
Indeed, modal and temporal logics have been proved useful formalisms for specifying and verifying properties of concurrent systems, and different tools have been developed to support such activities. Since a logic naturally gives rise to equivalences (two systems are equivalent if they satisfy the same formulae) often the proposed logics have been contrasted with behavioral equivalences for a better understanding and evaluation. In general, establishing a direct correspondence between a logic and a behavioral equivalence provides additional confidence in both approaches.
A well-known result relating operational and logical semantics is that about Hennessy-Milner Logic (HML). When this logic is interpreted over labeled transition systems with and without silent actions, it is in full agreement with strong and weak observational equivalence. Other correspondences have been established for equivalences over Kripke structures (node-labeled transition systems): a variant of strong observational equivalence coincides with the equivalence induced by CTL*; and then that CTL* without the next operator (CTL*- X) is in full agreement with stuttering equivalence, an equivalence based on the idea of merging adjacent states that have the same labeling.
There has been a great deal of effort spent on developing logical formalisms for specifying and reasoning about concurrent systems. In particular, various dynamic, modal, and temporal logics have been proposed which can express the capabilities available to a computation at various points of time during its (typically infinite) execution. Two major varieties of such logics exist: linear-time logics express properties of complete runs, whilst branching-time logics permit a finer consideration of when choices within computation paths are made. The study of such logics is now quite broad and detailed, as is the work on model-checking, the problem of determining if a system possesses a logical property.
There exists however a dichotomy in the study of the model-checking problem, roughly defined by linear-time versus branching-time approaches to logical properties. On the one hand, classical automata-theoretic techniques have been exploited in the linear-time case: to verify that a particular system satisfies a particular property, one constructs an automaton which represents in essence the cartesian product of the system in question with the negation of the property in question, and thus reduces the problem to one of checking emptiness of the language generated by an automaton. One drawback to this approach is the overhead incurred in constructing such an automaton: even if the system being analysed can be represented by a finite-state automaton, this automaton will typically be of a size which is exponential in its description (due to the problem of state space explosion), and hence this approach to the verification problem will be (at least) exponential in the worst case.
Another approach to the model-checking problem attempts to exploit structural properties. The essence of this approach is to work as far as possible with a syntactic description of the system and property at hand rather than with their semantic interpretations as automata. Typically this involves the development of tableau-based proof systems which exploit congruence and decomposition properties. This allows more of a so-called local model checking technique which feasibly could handle even infinite-state systems, as the overhead of constructing the relevant semantic automata is avoided.
Whichever approach is considered, there are common goals which are stressed. Firstly, the methodology must be faithful to the system descriptions being modelled, as well as to the intended properties being defined. The methodology must be sound with respect to its intended purpose. Of importance as well is the ability to automate the techniques; as systems become ever more complex, the need for automated support for their verification becomes ever more evident. Algorithms developed for automated analyses must furthermore be tractable. There will clearly be trade-offs between the expressivity of a formalism employed to define system properties, and the complexity of the verification of these properties. The verification procedures, beyond being sound, must be effective, as well as of an acceptable level of time- and space-complexity.
We thus have the following important themes appearing in the ongoing research in concurrency theory:
Several automated tools exist which can exploit local model-checking techniques or binary decision diagram (BDD) encodings of regular systems so as to analyze very large (and in some cases infinite state) systems. The general model checking problem for the modal mu-calculus however remains an intriguing mystery: the best algorithms are exponential in the worst case, though the problem is known to be both in NP and in co-NP, giving strong evidence that the problem can be solved in polynomial time.
For these reasons, the design of a good general-purpose concurrent programming language is inherently difficult -- perhaps inherently unsolvable -- problem. On the one hand, abstract languages such as CSP, SR (Shared Resources), and to a certain extent Ada, do not address the so-called "mapping problem", i.e. how to map a program onto a given hardware topology in an optimal way. On the other hand, in practice one often uses languages which are tuned towards some hardware topology, such as C augmented by semaphores (for a shared data topology) or C augmented by message-passing primitives (for a bus-based or message-based topology). Languages such as Linda, occam (on account of its placed-par command), and to a certain extent Java, can be placed in the second category. An added complication is that, to date, the languages and models used in the semantics and verification of parallel systems are almost disjoint from those used in parallel complexity theory, and both are almost disjoint from those used in practice. Thus, the correctness of a program may perhaps be verified in one notation, its runtime estimated in another notation, while it is then implemented in yet another notation. However, over the past decade, theory and practice have progressed to such an extent that (a), it is possible, in principle, to give semantics (of all kinds: operational, denotational, interleaving, partial order) to almost any arbitrary well-defined concurrent language, (b), the computational complexity of a wide class of parallel algorithms is well-understood and basic complexity classes relevant for parallel programming have been investigated extensively, and (c), parallel systems of a wide variety (ranging from distributed operating systems to weather forecast systems and, e.g., concurrent prime number decomposition programs) have been designed and implemented on a range of hardware platforms. Presently, we are at the brink of bringing many of the facets pertaining to parallel programming mentined above into synergy. For instance, the recently developed language NESL attempts to reconcile verification and complexity calculation for parallel programs while still neglecting the mapping problem.
Concurrency models allow the designer to describe the system in a mathematically precise notation. Once such descriptions are written, they can be analyzed to detect inconsistencies. Several analysis techniques have emerged as powerful debugging tools. When the system under design can be described by variables ranging over finite types, algorithmic analysis is possible. In this case, we have optimal decision procedures for checking equivalence of two descriptions, for checking whether a detailed description is a correct implementation of the more abstract one, and for verifying if the system description meets its logical specification.
Over the past decade, a variety of heuristics have been invented to enhance the applicability of these algorithms. These include local algorithms that explore the underlying state-space only as needed, symbolic algorithms that manipulate implicit representations like binary decision diagrams, and reductions based on symmetries among states and state-sequences. Recent results indicate that algorithmic analysis is also possible for certain infinite systems such as pushdown and real-time systems.
An orthogonal and complementary technique for reasoning about formal descriptions is the use of proof systems. Compositional and modular proof rules allow to decompose the analysis problem into subproblems by exploiting the structure of the description. Different styles of proof systems have been devised for specific notations, and are embedded within theorem provers to facilitate the proof construction.
The past decade has also seen research into the development of tools that use concurrency theory as a basis for automating the design and analysis of concurrent systems. The tools vary greatly in terms of the kinds of analysis supported and particular aspect of semantics of concurrency used; however, each implicitly shares the philosophy that truly useful design tools must have the sort of rigorous and mathematical theoretical basis that concurrency theory provides. The remainder of this section provides an overview of the tools that have been developed, while the following section reviews a few of the systems-analysis problems to which they have been applied.
This category of tools may be further broken down into tools that used labeled transition systems as their underlying system model and those that use Kripke structures. In the former, transitions are labeled with events that indicate potential interactions the system may have with its environment, while the latter labels states with information indicating the properties, such as values of variables, that hold in the state. Tools based on the labeled transition models have typically been used to model loosely coupled concurrent systems such as communications protocols, while those based on Kripke structures have been devoted to more tightly coupled systems such as hardware. Examples of labeled-transition-system-based tools include the following.
TELECOMMUNICATIONS is probably the most important application area, and one where significant contributions can be made. A single day's outage can cost ten times more than an error in a floating point unit. Both profits and losses are likely to increase tenfold in the next century.
We present a number of strategic directions we would like to see followed in concurrency research. Several "grand challenges" are also given.
These different types of requirements are often contradictory. Reliability for instance requires the use of additional resources, which usually decreases the performance of the system and thus may endanger timeliness. Up to now, formal methods mainly focus on functionality. In recent years several specification logics and system description languages for specifying timing behavior have been proposed. Also concerning the addition of probabilistic information there has been progress. We need to develop formalisms to capture these phenomena separately first, and then integrated with the description of other phenomena; e.g. a formalism that captures timing information and probabilistic information, in addition to functional correctness. It should be easy to construct a model that captures that subset of the requirements that is most relevant to a given problem.
Then, there is still the major challenge of bring all these formalisms out of the "test-tube" environment and apply them in an integrated way for the specification, verification and design of complex real-life systems.
A concrete challenge here is the formal modeling and analysis of the emerging micro electro-mechanical systems (MEMS) technology.
Overall, the explosion of formalisms has led to healthy diversity rather than fragmentation of the discipline: the existing variety of individual concurrency theories has proved suitable for a wide range of application domains, and comparative concurrency theory has identified deep mathematical relationships between individual theories.
Yet, potential customers, such as the designers of communication protocols and embedded systems, have been reluctant in applying concurrency-theoretic methods. This reluctance is reinforced by the perceived need of having to buy into one particular formalism and tool from what must seem, to the bystander, a bewildering, crowded, and unstructured array of possible choices.
Indeed, this perception is often perpetuated, not countered, by occasional unifying efforts, both in theory and in practice. In theory, there is a tendency towards ever more fundamental and intricate mathematical theories. In practice, there is a tendency to force all kinds of applications into one's favorite model and onto one's favorite tool, no matter how natural or effective the fit. Neither effort offers concrete help, only additional confusion, to the open-minded customer who needs to predict the relative effectiveness of various tools for a given application.
Challenge: In order to achieve a general acceptance of concurrency practice, we need a systematic and coherent way of presenting concurrency theory on a level that is acceptable to the customer and the student. This can be achieved by a simple uniform framework that permits an application-oriented taxonomy of the major models and a structured organization of the core results. Such a framework will aid the student, the customer, and also the researcher.
Student. Concurrency theory is concerned with the understanding of multiple interacting processes in the most general sense. As a result, in a world of interactive, networked, and embedded computing, the basic concepts of concurrency theory are fundamental to computer science as a whole. Yet they have not found their way into the standard curriculum, which again can be traced largely to the lack of a simple uniform framework that allows the systematic and coherent presentation of the subject. See the section on Concurrency Education below.
Customer. A uniform framework provides the nonexpert customer of design and analysis tools with objective selection criteria that isolate essential truths and complexities from accidental model-dependent idiosyncrasies. The framework allows an explicit declaration and study of the underlying assumptions that make a formalism or method more, or less, practical for a given application domain. It will enable tool developers to emphasize strengths while explaining limitations, and to shift the standard from universality to integration of specialized tools.
Researcher. Large applications are often highly heterogeneous, with synchronous and asynchronous, discrete and continuous, hardware and software components, and with multiple clock domains. A uniform framework aids the development of new methods and tools for the design and analysis of heterogeneous systems. For example, a uniform framework supports the asynchronous interaction of synchronous domains, or the implementation of asynchronous protocols using synchronous circuits.
Challenge: Verify larger systems.
There are two important observations about the current state in design and verification of concurrent systems.
The transformation of the design and verification techniques into methodologies that employ the structure of concurrent systems, and of which the effectiveness is being tested by application, is one of the major tasks for the concurrency community in the next decade.
In design, the question that must primarily be addressed is how to structure the system such that it can effectively provide the required functionality. Then the behaviour of different components must be designed. During this process the design must become comprehensible, unambiguous, efficient and often extendible.
Many individual and complementary techniques exist to develop such ideal designs; e.g. formal specification languages; distributed algorithmics, abstraction by layering. Yet, there is no systematic treatment and very little common experience on how to integrate the individual techniques. It seems that integration, streamlining, field testing and tooling are the required activities to develop the design methodology.
If such a methodology would exist (as in the construction of buildings or machinery), these will allow the education of design engineers being able to design neat systems with considerable functionality. This will both lower cost and increase reliability of future computerized systems.
For verification the current situation is less clear. But as verification appears to be a more difficult activity than design the desire for good verification methodologies is higher. There exist many competitive verification techniques that are sometimes diametrically opposed to each other concerning their approach (e.g. verification by decomposition vs. verification using expansion). There are many different ways to state the correctness of systems (pre/post conditions, equalities, modal logics) and it is not clear which method is most appropriate in which situation.
It appears that for verification concurrent systems belong to particular classes; e.g. communication protocols; distributed termination algorithms; leader election algorithms. The verification for systems in each class follow similar patterns. The patterns for each class must be identified and it must be established which mixture of verification techniques is most suitable.
It is expected that a good training in verification methodology will make it cost effective for system designers and programmers to verify their products. As such this will become one of the next revolution in computerized system development.
There are two broad principles of system design that apply to concurrent system designs as well: modularity and refinement. Modularity requires us to design a large program in smaller pieces, called modules, so that certain aspects of the system behavior can be guaranteed by each module, and these guarantees from the different modules may be combined to yield the properties of the system. Refinement deals with constructing a skeleton of the design in which certain aspects (data structures, program text) may yet to be developed; these aspects are developed (refined) at a later stage. What exactly constitutes a module or a step in a refinement is largely problem dependent. Different application domains - telecommunications, avionics, industrial process control - will apply these principles in different ways. The goal of research is to study a number of these application areas to establish common design principles that are more specific than the ones listed above.
Designs of sequential programs have relied to a large extent on the fact that there is a single thread of control in any sequential program; therefore, assertions can be made about the system state at each point in the program text. When we approach concurrent program design, however, reasoning based on temporal behavior of a program is grossly inadequate; we simply can't imagine that one processor can execute a million steps while another has yet to complete a single step! We are more likely to leave out such pathological cases in our reasoning. Therefore, it is essential that concurrent programs be developed employing design methodologies that guarantee specific properties of the final program. Testing is not a viable alternative.
A program that is executed is never proven; what is proven is only an abstraction of that program that is subsequently compiled and linked. We have sufficient confidence in the compilers and linkers that we continue to believe in an executing program even though we have proved only an abstraction of it. Stated in another way, we find it cost-effective to argue about two different correctness problems (using different methods): The correctness of a high-level program and the correctness of the compiler. For concurrent programs, one would like to establish a number of properties, and different methods may be appropriate for each property. We may wish to know the program's performance on a given machine (or whether it meets some real-time constraints), the amount of buffer spaces it consumes or the network traffic it generates. It is essential to develop different methods to address these different questions. While correctness can be studied entirely within mathematical logic, at least in principle, questions of performance are best treated through a combination of analytical and empirical methods. Similarly, different methods may be employed to prove different kinds of correctness properties, safety and liveness.
One of the major benefits of a design theory is that it avoids a-posteriori verification of properties. The design methods guarantee that certain properties are established, or that previously established properties are preserved by a refinement step, for instance. In order to construct an effective design theory, the properties have to be stated in a logic that boasts a number of deduction rules, because such rules can often be mapped to program design rules. A fundamental research problem is a careful taxonomy of the different properties we are likely to require of our concurrent programs, a hierarchy of logics for specifications and deductions of these properties from simpler ones, and different design methodologies to establish these properties.
Designing such languages is not a trivial task. Adding a notion of concurrency to an existing language often breaks some of the tacit assumptions that a language is making about the underlying system, e.g. determinism and no interference on variables. Thus designing a language with an explicit concurrency model from scratch is often less error-prone.
Having an explicit concurrency model in a programming language also makes the programmer aware of the task at hand and helps making the pitfalls of concurrency, e.g. the introduction of deadlocks or livelocks, more evident to the programmer. If the language is sufficiently expressive it could lead to the construction of re-usable abstractions for sophisticated synchronisation mechanisms in much the same way as objects are used in sequential systems today.
Furthermore, as pointed out by Best, a well-designed language could promote portability without limiting parallelism. Languages such as ESTERELLE and Occam have, in their respective domains, proved the viability of this approach.
It is important that the development of models, formalisms, logics, tools and programming languages goes hand in hand, or at least are kept relatively synchronised to avoid divergence and thus defeating the overall objective of being able to verify running code. Currently there is a growing list of initiatives in this direction, to mention a few: Oz, PICT, CML and Facile. This direction of work bears similarities with the efforts of extending concurrency formalisms to capture more non-concurrency aspects, e.g. the current enrichments to LOTOS for describing abstract data types. Joint developments should strongly be encouraged. It is important that the theoretical footing of these languages is seen as an advantage, not as a hindrance. Then concurrency theory will be able to give its contribution to the creation of better and more reliable mainstream computing systems.
A step toward the above (somewhat) ultimative goal could go via the influence that concurrency theory is currently having on type systems for concurrent object oriented systems, where the type is augmented with behavioural information, or it could go through new type systems that guarantee safety and liveness properties in the same way as traditional type systems guarantee safety in calling functions and procedures.
As pointed out by Prasad and Thomsen, the design of safe and secure languages with a well understood (concurrency) model is becoming increasingly important now that mobile agents or applets have started to roam the internet. At the moment such mobile agents are written in languages such as Java, Telescript or Tcl/Tk, all having rudimentary notions of concurrency, e.g. based on threads and semaphores. However, there is a growing need for extending the concurrency constructs of these languages or designing new languages with more advanced synchronisation mechanisms, based e.g. on synchronous channels, multi-cast groups and constraint variables. Concurrency theory can play a very important role in helping designers in analysing very sophisticated systems based on the mobile agents principle, in particular higher order and mobile theories. Although the future for concurrency theory in this direction looks bright there is still a need for further developments in verification techniques and technology.
The following list includes some essential concepts that can and should be taught at the undergraduate level, perhaps as part of a course on distributed systems.