Rocco De Nicola
and
Scott A. Smolka, Chair
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.
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 is determined by their interaction with other processes and/or by their reaction to external stimuli. Whenever, the environment, the framework, the circumstances, ... within which a (sub-)system is going to be used are known, 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.