ACM Computing Surveys 28A(4), December 1996, Copyright © 1996 by the Association for Computing Machinery, Inc. See the permissions statement below.

Programming Languages,
Analysis Tools
Concurrency Theory

Bent Thomsen

ICL, Technology Businesses, Research & Advanced Technology,
Lovelace Road, Bracknell, Berkshire RG12 8SN, UK.

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.

1 Introduction

Concurrency theory is now entering a very exciting era. Many of the fundamental aspects of the formalisms that collectively are known as concurrency theory are now beginning to be understood, and systematic comparisons and unified foundations are beginning to emerge.

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.

3 Programming Languages for Concurrency

In recent years languages that strive to combine several programming paradigms in a single system both for sequential and for concurrent/parallel/distributed computing have been put forward. Examples include OCCAM [Inm88], Oz[Smo95], PICT [PT95a, PT95b], CML [Rep92] and Facile [GMP89,TLK96]. A language which supports multiple programming paradigms often enables a more direct expression of the design, since many problems and solutions consist of various components that are more natural and easier when viewed in different ways. Allowing the implementation to exploit a more direct expression of the design helps in avoiding unnecessary encodings that often are great sources of software errors and maintenance complication.

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.

4 Type Systems

A promising direction to bring concurrency into main stream computing could go via the influence that concurrency theory is currently having on type systems for concurrent object oriented systems  [Nie90] and functional concurrent systems  [NN93, NN94], where the type is augmented with behavioural information.

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:

  1. compile-time optimisations of run-time placement of processes and channels in distributed environments such as networks of workstations or parallel processors.
  2. fault-tolerance in distributed environments. E.g. dead-lock detection and static approximation (for reduction) of resource replication.
  3. safety in communication of mobile agents (i.e. higher-order functions and processes) in distributed applications. E.g. an application may receive an agent that was compiled elsewhere. The application may want/need to check the potential external effects of the incoming agent in the application's environment. Thus behaviour inference may provide a level of safety since only agents satisfying a behaviour specified by the receiving side are accepted.

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].

5 Mobile Agents

With the emergence of mobile agent based systems a new class of applications has started to roam the information highway. Mobile agent based systems bring the promise of new, more advanced and more flexible services and systems. Mobile agents are self-contained pieces of software that can move between computers on a network. Agents can serve as local representatives for remote services, provide interactive access to data they accompany, and carry out tasks for a mobile user temporarily disconnected from the network. Agents also provide a means for the set of software available to a user to change dynamically according to the user's needs and interests [TKLC95].

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].


S. Abramsky. Retracing some paths in process algebra. In Proceedings of CONCUR '96 - Seventh Intl. Conf. on Concurrency Theory, volume 1119 of Lecture Notes in Computer Science, pages 1-17. Springer-Verlag, 1996.

S. Abramsky, S. Gay, and R. Nagarajan. Specification structures and propositions-as-types for concurrency. Springer-Verlag, 1996.

R. Borgia, P. Degano, C. Priami, L. Leth and B. Thomsen. Understanding Mobile Agents via a non-interleaving semantics for Facile. Technical report ECRC-96-4, 1996.

F. Gallo. Agent-Tcl: A white paper. Draft document, posted to the mailing list, December 1994.

A. Giacalone, P. Mishra, and S. Prasad. Facile: A symmetric integration of concurrent and functional programming. In International Journal of Parallel Programming, 18:121--160, 1989.

J. Gosling and H. McGilton. The Java language environment. White paper, May 1995. Sun Microsystems, 2550 Garcia Avenue, Mountain View, CA 94043, USA.

INMOS, Ltd. OCCAM-2 Reference Manual, Prentice-Hall International, Englewood Cliffs, NJ, 1988.

R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.

R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, Parts I and II. Information and Computation, 100, 1992.

R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, Cambridge, Massachusetts, 1990.

O. Nierstrasz. Viewing objects as patterns of communicating agents. In Proceedings of ECOOP/OOPSLA'90; European Conference on Object-Oriented Programming/Object-Oriented Programming Systems, Languages and Applications, pages 38-43, 1990.

F. Nielson and H. R. Nielson. From CML to process algebras. In Proceedings of CONCUR '93 -- Fourth International Conference on Concurrency Theory. Volume 715 of Lecture Notes in Computer Science, Springer-Verlag, 1993.

H. R. Nielson and F. Nielson. Higher-order concurrent programs with finite communication topology. In Proceedings of 21st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 84-97. ACM Press, 1994.

B. Pierce and D. Turner. PICT Language Definition. University of Indiana, December 1995. Available at URL

B. C. Pierce and D. N. Turner. Concurrent objects in a process calculus. In Theory and Practice of Parallel Programming, volume 907 of Lecture Notes in Computer Science, Sendai, Japan, April 1995. Springer-Verlag.

J. H. Reppy. High-order Concurrency. PhD thesis, Cornell University, 1992. Also Cornell Univ. Computer Science Dept. Tech. Report 92-1285.

G. Smolka. The definition of kernal Oz, in Constraints: Basic and Trends", Lecture Notes in Computer Science 910, Springer Verlag, 1995.

B. Thomsen. A Calculus of Higher Order Communicating Systems. In Proceedings of POPL'89. ACM Press, 1989.

B. Thomsen. A Second Generation Calculus for Higher Order Processes. Acta Informatica 30, pages 1-59, 1993. Preliminary version in Technical Report 89/04, Imperial College 1989.

B. Thomsen. Polymorphic Sorts and Types for Concurrent Functional Programs. In Proceedings of the 6th International Workshop on the Implementation of Functional Languages (Ed. J. Glauert), UEA Norwich, UK, 1994.

B. Thomsen. A theory of higher order communicating systems. Information and Computation, 116(1):38-57, January 1995.

B. Thomsen. Position statement for the ACM Strategic Directions workshop as a member of the concurrency working group. HTML document (, June 1996.

B. Thomsen, F. Knabe, L. Leth and P.-Y. Chevalier. Mobile Agents Set to Work, In Communications International, July, 1995. Preliminary version available as URL

B. Thomsen, L. Leth, and T.-M. Kuo. A Facile tutorial. In Proceedings of CONCUR '96 - Seventh Intl. Conf. on Concurrency Theory, volume 1119 of Lecture Notes in Computer Science, pages 278-298. Springer-Verlag, 1996.

J. E.  White. Telescript technology: The foundation for the electronic marketplace. General Magic white paper, 2465 Latham Street, Mountain View, CA 94040, 1994.

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

Last modified Thu Nov 15 16:00:52 GMT 1996
Bent Thomsen <>