ACM Computing Surveys 28A(4), December 1996, http://www.acm.org/surveys/1996/ThomsenProgramming/. Copyright © 1996 by the Association for Computing Machinery, Inc. See the permissions statement below.
Abstract: This paper is a revised and expanded version of my position statement [Tho96] for the ACM Strategic Directions workshop as a member of the concurrency working group.
Concurrency theory has the potential for entering main stream computing as the need for programming languages with advanced and well understood concurrency models increas - particularly fueled by the emergence of mobile agents on the internet, but also because most systems in the future will be distributed and highly concurrent.
Categories and Subject Descriptors: D.1.3 [PROGRAMMING TECHNIQUES]: Concurrent Programming - Distributed programming; D.2.2 [SOFTWARE ENGINEERING]: Tools and Techniques - Programmer workbench; D.3.1 [PROGRAMMING LANGUAGES]: Formal Definitions and Theory - Semantics; D.3.2 [PROGRAMMING LANGUAGES]: Language Classifications - Concurrent, distributed, and parallel languages; D.3.3 [PROGRAMMING LANGUAGES]: Language Constructs and Features - Concurrent programming structures; F.1.2 [COMPUTATION BY ABSTRACT DEVICES]: Modes of Computation - Parallelism and concurrency; F.3.1 [LOGICS AND MEANINGS OF PROGRAMS]: pecifying and Verifying and Reasoning about Programs - Specification techniques; F.3.3 [LOGICS AND MEANINGS OF PROGRAMS]: Studies of Program Constructs - Type structure.
General Terms: Concurrency theory, Verification tools, Programming languages.
Additional Key Words and Phrases: Multi paradigm programming, Type systems, Mobile agents.
A good sign of maturity of concurrency theory is that it is starting to shed new light on very fundamental aspects of computing in general, such as logic, the lambda-calculus, distributed, object oriented and constraint programming.
Clearly, there are still many things to be understood about the foundations of concurrency theory, i.e. questions about synchrony vs. asynchrony, broadcast v.s. point-to-point communication, static binding v.s. dynamic binding of names, names or no names, operational semantics v.s. denotational semantics, etc. However, difficult questions such as the relationship between true (non-interleaving) and false (interleaving) concurrency are now largely understood.
Thus concurrency theory is now at a stage where it has the potential to move decisively out of its traditional niche as an enrichment to formal methods and into main stream computing. For this to happen three important directions are emerging:
One direction is enrichments of concurrency formalisms to deal with more aspects than the purely behavioural one. These include real-time and probabilities, value passing, link passing and process passing.
A second direction is the development of tools, analysers, verifiers, theorem provers, etc. and their applications in large scale systems to test the viability and scalability of tools and methods.
A third direction is the development of programming languages with a strong foundation from concurrency theory.
In fact these trends have the potential for complementing each other very well. If design of formalism, tool and programming language go hand in hand, or at least are kept closely together so divergence is avoided, it may be possible to address the question of analysis of ``real code'' based on firm formal footing. The advantage is that there will be no gap between model and implementation of a system. This is in sharp contrast to traditional analysis of systems where there inevitably is a gap between the formal model and the running code since the analysis takes place in a formal model of the system, but the system itself is implemented in a traditional programming language without formal foundation.
In the following sections I will expand a bit on the third direction based on work I have been involved in.
I have been involved in the design and implementation of one such language: The Facile Language [TLK96]. Facile combines a predominantly functional programming language, Standard ML (SML) [MTH90], with a model of concurrency based on CCS [Mil89] and its higher order and mobile extensions (CHOCS [Tho89, Tho93, Tho95], and the pi-calculus [MPW92]). Furthermore, constructs for distributed computing are based on recent results from timed process algebra and true concurrency theory. The Facile system may be viewed as a combination of language, compiler and distributed systems technology, based on strong formal foundations, that puts an emphasis on reliability of software, as well as flexible (and reliable) management of applications that need to evolve over time in terms of architecture, interfaces and functionalities.
The requirements satisfied by Facile are common to different application domains, such as industrial automation, air traffic control, telecommunications and financial markets. Extensive experiments and demonstrative applications show that Facile or similar languages will be valuable tools for the implementation of the infrastructures that support applications in these domains.
Clearly there are foundational issues concerned with the ability to express adequately the interface for a subsystem, written in one paradigm, to another subsystem, written in another paradigm and clearly there is scope for design and experimentation and plenty of research to be done in finding a good balance between constructs based on (concurrency) theory, efficient implementation(s) and practical applicability.
I am involved in creating a new type system for Facile based on effect systems and behavioural analysis [Tho94]. Behavioural descriptions will capture essential static information about a program's potential dynamic behaviour, in particular its potential for communication and for dynamic creation of processes. This information may impact:
Further properties may be captured in new type systems that guarantee safety and liveness properties in the same way as traditional type systems guarantee safety in calling functions and procedures. Promising new results in this area have started to emerge [Abr96, AGN96].
Mobile agents bring with them the fear of viruses, Troyan horses and other nastities. To avoid troubles of this kind, the main approach to agent based systems is based on development of safe languages, i.e. languages that do not allow peek and poke, unsafe pointer manipulations and unrestricted access to file operations. This is often achieved through interpreted languages. Java [Gos95], Safe-TCL [Gal94], Telescript [Whi94] are examples of this approach.
Even when the fear of viruses has been eliminated, mobile agent systems may be a magnitude more complex to develop than traditional client/server applications since it is very easy to create agents that will counter act each other or inadvertently ``steal'' resources from other agents. Since an agent can move from place to place, it can be very hard to trace the execution of such systems and special care must be taken when constructing systems of this nature.
However, apart from being safe languages in the above sense, the mentioned languages are rather traditional, based on the object oriented paradigm and/or traditional imperative scripting language techniques, hence these languages offer very little support for the analysis of systems.
Thus with the emergence of mobile agent based systems the design of safe and secure languages with a well understood (concurrency) model is becoming increasingly important.
When such languages are used, concurrency theory can play a very important role in helping designers in analysing very sophisticated systems based on the mobile agents paradigm.
I have been involved in one such attempt using Facile [TKLC95], analysing a system of mobile agents based on a true concurrency semantics for Facile [BDPLT96].
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 firstname.lastname@example.org.