ACM Computing Surveys 28A(4), December 1996, http://www.acm.org/surveys/1996/DeNicolaPractice/. Copyright © 1996 by the Association for Computing Machinery, Inc. See the permissions statement below.
Abstract: Concurrency theory is concerned with the modeling and verification of concurrent systems, while concurrency practice promulgates the application of concurrency theory to concurrent systems of practical interest. We assert that a strong interplay between concurrency theory and practice is essential for the continued development of both fields.Categories and Subject Descriptors: C.2.2 [COMPUTER-COMMUNICATION NETWORKS]: Network Protocols - Protocol Verification; D.1.3 [PROGRAMMING TECHNIQUES]: Concurrent Programming; D.2.4 [SOFTWARE ENGINEERING]: Program Verification; F.1.2 [COMPUTATION BY ABSTRACT DEVICES]: Modes of Computation - Parallelism and Concurrency; F.3.1 [LOGICS AND MEANINGS OF PROGRAMS]: Specifying and Verifying and Reasoning about Programs; F.3.2 [LOGICS AND MEANINGS OF PROGRAMS]: Semantics of Programming Languages
General Terms: Languages, Theory, Verification
Additional Key Words and Phrases: Abstraction, behavioral relations, concurrency theory, concurrent systems, interleaving, observations, true concurrency
Modeling and abstraction are two key concepts of computer science that go hand-in-hand. If we would like to model a computer system for the purpose of (computer-aided) analysis, it is essential that we choose the right level of abstraction when describing the system. This choice is even more critical when concurrent systems are considered. A concurrent system can be viewed as a collection of sequential processes, possibly running on different processors, that interact and exchange results with each other and with the external environment.
Abstraction in the description of concurrent systems can be obtained by devising a theory of observations. The semantics of concurrent processes heavily depends on their interaction with other processes and on their reaction to external stimuli. Thus, different formalisms and models can be used depending on the environments in which systems are going to operate and on the kind of properties we are interested in. We can resort to observations consisting of sequences of possible interactions if we are interested only in describing completely abstract behaviors or if we assume sequential users. We can, instead, make use of sequences of multisets of interactions if potential concurrency (performance considerations or multiple users) has to be taken into account. Finally, partial orderings of potential interactions are appropriate when one is interested in using systems descriptions as guidelines for concurrent implementations. Whenever the environment within which a (sub-)system is going to be used is known, and the system designer has a clear idea of the properties of interest, then sets of observations can be devised to fix its semantics.
The main difference between a theory of sequential systems and one of concurrent ones is that for the latter it is not possible to fix once and for all the abstraction level at which systems can be most advantageously described. Indeed, in the last decade we have witnessed a lively debate on the interleaving vs. true concurrency approach to the description of systems. This can essentially be seen as a discussion about the abstraction level of system descriptions. Another example of this problem is the wealth of different behavioral relations among transition systems proposed in the literature, each aiming at ignoring specific aspects of systems descriptions. Indeed, descriptions in terms of labeled transition systems are often considered too concrete and behavioral relations such as equivalences or preorders have been proposed to assess the relationships between different views of the same system. If both the specification and the implementation of a concurrent system are described via the same formalism then the correctness of the latter with respect to the former can be established by studying their behavioral relationship.
Due to the great variety of aspects to be taken into account, a single approach to systems description relying on a fixed abstraction level may not be sufficient; a way for providing a uniform interpretation of the different semantics of concurrent processes would be that of describing them parametrically with respect to sets of observations. Systems semantics based on (hierarchies of) observations may at the same time offer different views of the same system while explaining the exact relationships between them. This point of view could be instrumental also for understanding the foundations of interactive computing, a new paradigm based on the idea that the semantics of a system heavily depends on the environment in which it operates and the external stimuli it receives.
The field of concurrency theory has matured to the point where many of its constituents are concerned about the application of this theory to real-world problems. We call such application "concurrency practice". The hope is that concurrency practice will enable us to design and build more reliable computer software and hardware, especially those related to safety-critical systems.
Interest in concurrency practice is witnessed by two ongoing research tracts: extensions of concurrency theory to better cope with real-world problems, and the development of efficient and useful tools for applying the basic theory and its extensions. Relevant extensions include real-time, probability, priority, mobility, security, and hybrid systems phenomena. Relevant tools include temporal and modal logic model checkers, behavioral equivalence and preorder checkers, practical theorem provers, state reachability analyzers, and graphical user interfaces.
The future of concurrency practice looks bright. Successful case studies---concerning practical problems such as communication protocols, hardware design and verification, process control systems, and traffic control systems---appear regularly in the literature. New and improved algorithms, upon which tools can be built, are being developed. Advances in system technology, such as larger memories, faster processors, and computing with networks of workstations, increase the range of concurrency practice.
The question remains, though, whether concurrency practice can keep pace with the increasingly complex applications it is likely to be subjected to. The answer from this position is a cautious but optimistic yes, and we believe that such successes will be fueled a continuation of the close interplay between theory and practice that we are currently witnessing. In the field of concurrency we often see application and experimentation going on in parallel with the development of new theories. This was not the case with the foundational theories of sequential programming. where significative advances in theory did not lead to comparable advances in software production.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org.