Publications by Prof Peter Welch

Concurrency is beginning to be accepted as a core knowledge area in the undergraduate CS curriculum—no longer isolated, for example, as a support mechanism in a module on operating systems or reserved as an advanced discipline for later study. Formal verification of system properties is often considered a difficult subject area, requiring significant mathematical knowledge and generally restricted to smaller systems employing sequential logic only. This paper presents materials, methods and experiences of teaching concurrency and verification as a unified subject, as early as possible in the curriculum, so that they become fundamental elements of our software engineering tool kit—to be used together every day as a matter of course. Concurrency and verification should live in symbiosis. Verification is essential for concurrent systems as testing becomes especially inadequate in the face of complex non-deterministic (and, therefore, hard to repeat) behaviours. Concurrency should simplify the expression of most scales and forms of computer system by reflecting the concurrency of the worlds in which they operate (and, therefore, have to model); simplified expression leads to simplified reasoning and, hence, verification. Our approach lets these skills be developed without requiring students to be trained in the underlying formal mathematics. Instead, we build on the work of those who have engineered that necessary mathematics into the concurrency models we use (CSP, ?-calculus), the model checker (FDR) that lets us explore and verify those systems, and the programming languages/libraries (occam-?, Go, JCSP, ProcessJ) that let us design and build efficient executable systems within these models. This paper introduces a workflow methodology for the development and verification of concurrent systems; it also presents and reflects on two open-ended case studies, using this workflow, developed at the authors' two universities. Concerns analysed include safety (don't do bad things), liveness (do good things) and low probability deadlock (that testing fails to discover). The necessary technical background is given to make this paper self-contained and its work simple to reproduce and extend.

Future systems will be too complex to design and implement explicitly. Instead, we will have to learn to engineer complex behaviours indirectly: through the discovery and application of local rules of behaviour, applied to simple process components, from which desired behaviours predictably emerge through dynamic interactions between massive numbers of instances. This paper describes a process-oriented architecture for fine-grained concurrent systems that enables experiments with such indirect engineering. Examples are presented showing the differing complex behaviours that can arise from minor (non-linear) adjustments to low-level parameters, the difficulties in suppressing the emergence of unwanted (bad) behaviour, the unexpected relationships between apparently unrelated physical phenomena (shown up by their separate emergence from the same primordial process swamp) and the ability to explore and engineer completely new physics (such as force fields) by their emergence from low-level process interactions whose mechanisms can only be imagined, but not built, at the current time.

With the commercial development of multicore processors, the challenges of writing multi-threaded programs to take advantage of these new hardware architectures are becoming more and more pertinent. Concurrent programming is necessary to achieve the performance that the hardware offers. Traditional approaches present concurrency as an advanced topic: they have proven difficult to use, reason about with confidence, and scale up to high levels of concurrency. This paper reviews process oriented design based on Hoare's algebra of Communicating Sequential Processes (CSP), and proposes that this approach to concurrency leads to solutions that are manageable by novice programmers -- that is, they are easy to design and maintain, that they are scalable for complexity, obviously correct and relatively easy to verify using formal reasoning and/or model checkers. These solutions can be developed in conventional programming languages (through CSP libraries) or specialised ones (such as occam-pi) in a manner that directly reflects their formal expression. Systems can be developed without needing specialist knowledge of the CSP formalism, since the supporting mathematics is burnt into the tools and languages supporting it. We illustrate these concepts with the Santa Claus Problem which has been used as a challenge for concurrency mechanisms since 1994. We consider this problem as an example control system, producing external signals reporting changes of internal state (that model the external world). We claim our occam-pi solution is correct-by-design but follow this up with formal verification (using the FDR model checker for CSP) that the system is free from deadlock and livelock, that the produced control signals obey crucial ordering constraints, and that the system has key liveness properties.

A fine-grained massively parallel and process-oriented architecture for the modelling of complex systems is presented. We propose that the concurrency in the model simplifies its design and construction by directly reflecting the processes in the natural world. The architecture is based on CSP, extended with mechanisms for process mobility from the pi-calculus; implementations are presented using the occam-pi language. A case study, modelling platelets (possibly artificial) within a blood vessel, is described. The aim for this model is to engineer emergent behaviour: the clotting of platelets in response to a wound in the blood vessel wall and the staunching of blood loss. A three-dimensional model is constructed, along with mechanisms for visualization and interaction. Its expressiveness and efficiency relies strongly on the dynamic and mobile capabilities of occam-pi. General principles for the design of large and complex system models are drawn. The described case study runs to millions of processes engaged in ever-changing communication topologies. It is free from deadlock, livelock, race hazards and starvation by design, employing a small set of synchronization patterns for which we have proven safety theorems. Compiled occam-p codes automatically and efficiently exploit all cores in a shared-memory multiprocessor system. They are also straightforward to distribute over standard cluster architectures.

Communicating Sequential Processes for Java (JCSP) is a mature library that implements CSP-derived concurrency primitives in Java. A JCSP system is a hierarchical network of autonomous processes communicating over synchronous (optionally buffered) channels, and multiway synchronising through barriers. This paper presents a significant extension to the barrier mechanism: the fast resolution of choice between any number of barrier events, channel communications (in either direction) and timeouts. Previously, and in line with all currently released libraries and languages offering the CSP concurrency model, choice was restricted to channel inputs and timeouts. The paper demonstrates an application of alting barriers and explains the mechanisms used in their implementation that enables their use as guards in a choice. It also shows how choice over channel outputs becomes possible, as a simple consequence of having choice over barriers. Finally, an efficient implementation of CSP's broadcasting channels is presented (using a phased barrier synchronisation pattern) and a mechanism for allowing choice over these is discussed. With this extended JCSP, almost all CSP-specified systems can now be directly implemented. The new library is available under LGPL open source.

A gateway event is a change to a system that leads to the possibility of huge increases in kinds and levels of complexity. It opens up a whole new kind of phase space to the systemÕs dynamics. Gateway events during evolution of life on earth include the appearance of eukaryotes (organisms with a cell nucleus), an oxygen atmosphere, multi-cellular organisms and grass. Gateway events during the development of mathematics include each invention of a new class of numbers (negative, irrational, imaginary, ...), and dropping Euclid's parallel postulate. A gateway event produces a profound and fundamental change to the system: Once through the gateway, life is never the same again. We are currently poised on the threshold of a significant gateway event in computation: That of breaking free from many of our current Òclassical computationalÓ assumptions. Our Grand Challenge for computer science is to journey through the gateway event obtained by breaking our current classical computational assumptions, and thereby develop a mature science of Non-Classical Computation

Continuing research on language design, compilation and kernel support for highly dynamic concurrent reactive systems is reported. The work extends the occam multiprocessing language, which is both sufficiently small to allow for easy experimentation and sufficiently powerful to yield results that are directly applicable to a wide range of industrial and commercial practice. Classical occam was designed for embedded systems and enforced a number of constraints, such as statically predetermined memory allocation and concurrency limits, that were relevant to that generation of application and hardware technology. This work removes most of these constraints and introduces a number of new facilities: explicit channel ends, channel bundles, mobile ends of channels and bundles, dynamic process creation, the extended rendezvous and process priorities. These significantly broaden occam's field of application and raise the level of concurrent system design directly supported. Concurrency overheads have been driven ever downwards, for example synchronising channel communication is now around 100 nanoseconds on an 800 MHz P3, and most operations have unit time cost. Finally, a proposal for secure mobile processes is made.

When building concurrent systems, it would be useful to have a collection of reusable processes to perform standard tasks. However, without knowing certain details of the inner workings of these components, one can never be sure that they will not cause deadlock when connected to some particular network. Here we describe a hierarchical method for designing complex networks of communicating processeswhich are deadlock-free.We use this to define a safe and simple method for specifying the communication interface to third party software components. This work is presented using the CSP model of concurrency and the occam2.1 programming language.

The authors present data-how solutions on a pipeline of transputers for banded and dense systems of linear equations using Gauss elimination and the Gauss-Jordan method, respectively, These implementations, written in occam, are especially effective when there is a continuous supply of right-hand sides to be solved with the same coefficient matrix. Attention is paid to both load balancing and resource handling within the processor elements of the pipeline, When solving multiple right-hand sides, floating-point efficiency levels on 32-processor implementations range from 110% (for dense systems) down to 90% (for banded systems), where 100% represents the peak performance attainable from a single transputer applied to the same problem (effectively back-to-back floating-point operations on data in external memory). Some conclusions are drawn on efficiency issues arising from state-of-the-art massively parallel supercomputers.

By emulating some of the very 'early' vision processes believed to occur close to the photo-receptors of the mammalian retina, dramatic savings can be made in the computational efforts associated with some aspects of image processing. This paper describes the design and implementation of part of a low-cost visiual tracking system that realises the 'smooth pursuit' reflex. It uses no special signal processing, vector processing nor floating-point hardware. Its effectiveness relies only on the parallel replication of fast scaler integer processors with low latency communications. The current (unoptimized) implementation uses 10 T425 transputers, processes 544 x 544 byte-pixel images at camera frame rates and provides 100 Hz tracking feedback signals to the camera pan-and-tilt motors with a latency of no more than one-fith of a second. The system will track any object that occupies the (majority of the) centre of the field of view moving against any background - no special lighting conditions or artificial scenery are required. The design and implementation follow naturally parallel structrues and are expressed at all levels in occam.

Modern VLSI technology has changed the economic rules by which the balance between processing power, memory and communications is decided in computing systems. This will have a profound impact on the design rules for the controlling software. In particular, the criteria for judging efficiency of the algorithms will be somewhat different. This paper explores some of these implications through the development of highly parallel and highly distributable algorithms based on occam and transputer networks. The major results reported are a new simplicity for software designs, a corresponding ability to reason (formally and informally) about their properties, the reusability of their components and some real performance figures which demonstrate their practicality. Some guidelines to assist in these designs are also given. As a vehicle for discussion, an interactive simulator is developed for checking the functional and timing characteristics of digital logic circuits of arbitrary complexity.

This paper reports on our experiences of using commodity GPUs to speed-up the execution of fine-grained concurrent simulations. Starting with an existing process-oriented `boids' simulation, we explore a variety of techniques aimed at improving performance, gradually refactoring the original code. Successive improvements lead to a 10-fold improvement in performance, which we believe can still be improved upon, allowing us to explore simulations with larger numbers of agents (30,000 rather than 2,000) interactively and without significant performance degradation.

With the release of their latest processor microarchitecture, codenamed Haswell, Intel added new Transactional Synchronization Extensions (TSX) to their processors' instruction set. These extensions include support for Restricted Transactional Memory (RTM), a programming model in which arbitrary sized units of memory can be read and written in an atomic manner. This paper describes the low-level RTM programming model, benchmarks the performance of its instructions and speculates on how it may be used to implement and enhance Communicating Process Architectures.

This paper considers some questions prompted by a brief review of the history of computing. Why is programming so hard? Why is concurrency considered an "advanced" subject? What's the matter with Objects? Where did all the Maths go? In searching for answers, the paper looks at some concerns over fundamental ideas within object orientation (as represented by modern programming languages), before focussing on the concurrency model of communicating processes and its particular expression in the occam family of languages. In that focus, it looks at the history of occam, its underlying philosophy (Ockham's Razor), its semantic foundation on Hoare's CSP, its principles of process oriented design and its development over almost three decades into occam-? (which blends in the concurrency dynamics of Milner's ?-calculus). Also presented will be an urgent need for rationalisation – occam-? is an experiment that has demonstrated significant results, but now needs time to be spent on careful review and implementing the conclusions of that review. Finally, the future is considered. In particular, is there a future?

Escape analysis is the process of discovering boundaries of dynamically allocated objects in programming languages. For object-oriented languages such as C++ and Java, this analysis leads to an understanding of which program objects interact directly, as well as what objects hold references to other objects. Such information can be used to help verify the correctness of an implementation with respect to its design, or provide information to a run-time system about which objects can be allocated on the stack (because they do not `escape' the method in which they are declared). For existing object-oriented languages, this analysis is typically made difficult by aliasing endemic to the language, and is further complicated by inheritance and polymorphism. In contrast, the occam-pi programming language is a process-oriented language, with systems built from layered networks of communicating concurrent processes. The language has a strong relationship with the CSP process algebra, that can be used to reason formally about the correctness of occam-pi programs. This paper presents early work on a compositional escape analysis technique for mobiles in the occam-pi programming language, in a style not dissimilar to existing CSP analyses. The primary aim is to discover the boundaries of mobiles within the communication graph, and to determine whether or not they escape any particular process or network of processes. The technique is demonstrated by analysing some typical occam-pi processes and networks, giving a formal understanding of their mobile escape behaviour.

Building robot control programs which function as intended is a challenging task. Roboticists have developed architectures to provide principles, constraints and primitives which simplify the building of these correct, well structured systems. A number of established and prevalent behavioural architectures for robot control make use of explicit parallelism with message passing. Expressing these architectures in terms of a process-oriented programming language, such as occam-π, allows us to distil design rules, structures and primitives for use in the development of process architectures for robot control.

This paper explores a process-oriented approach to complex systems design, using massive fine-grained concurrency, mobile channels and mobile processes. The complex systems studied are self-organising, with emergent and evolving behaviours (apparent at the global level) arising from massive interactions between relatively simple components (that have only local knowledge). Classical ant foraging is used as a case study. Processes are used to represent space, environmental factors and the ants themselves. Ant processes (like all processes) only have knowledge of their internal state (looking for food, looking for their nest) and what they can glean from their local neighbourhood (by interacting with the processes making up that neighbourhood). The networks constructed are dynamic, changing as the ants move around and environmental factors are introduced and modified. The paper reports on two mechanisms for achieving this: channel mobility and process mobility. The language for implementation is occam, which has the necessary concurrency mechanisms built in as fundamental primitives and whose semantics is rooted in the process algebras of CSP and the pi-calculus. Performance figures are given, including speedup curves for multicores, and some conclusions drawn.

CSP processes have a static view of their environment -- a fixed set of events through which they synchronise with each other. In contrast, the pi-calculus is based on the dynamic construction of events (channels) and their distribution over pre-existing channels. In this way, process networks can be constructed dynamically with processes acquiring new connectivity. For the construction of complex systems, such as Internet trading and the modeling of living organisms, such capabilities have an obvious attraction. The occam-pi multiprocessing language is built upon classical occam, whose design and semantics are founded on CSP. To address the dynamics of complex systems, occam-pi extensions enable the movement of channels (and multiway synchronisation barriers) through channels, with constraints in line with previous occam discipline for safe and efficient programming. This paper reconciles these extensions by building a formal (operational) semantics for mobile channels entirely within CSP. These semantics provide two benefits: formal analysis of occam-pi systems using mobile channels and formal specification of implementation mechanisms for mobiles used by the occam-pi compiler and run-time kernel.

Mobile processes, along with mobile channels, enable process networks to be dynamic: they may change their size (number of processes, channels, barriers) and shape (connection topology) as they run much like living organisms. One of the benefits is that all connections do not have to be established statically, in advance of when they are needed and open to abuse. In classical occam, care had to be taken by processes not to use channels when they were not in the right state to use them. With occam-pi mobiles, we can arrange that processes simply do not have those channels until they get into the right state - and not having such channels means that their misuse cannot even be expressed! Of course, it is a natural consequence of mobile system design that the arrivals of channels (or barriers or processes) are the very events triggering their exploitation. In our explorations so far with occam-pi, we have taken advantage of the mobility of data, channels and barriers and seen very good results. Very little work has been done with mobile processes: the ability to send and receive processes through channels, plug them into local networks, fire them up, stand them down and move them on again. This talk illustrates mobile process design through a solution to Trono's classical em Santa Claus Problem. The reindeer and elves are modeled as mobile processes that move through holiday resorts, stables, work, waiting rooms, Santa's Grotto and back again. All those destinations are also processes - though static ones. As the reindeer and elves arrive at each stage, they plug in and do business. We will show the occam-pi mechanisms supporting mobile processes, confess to one weakness and consider remedies. The occam-pi solution did, of course, run correctly the first time it passed the stringent safety checks of the compiler and is available as open source (http://www.santaclausproblem.net).

While we strive to create robust language constructs and design patterns which prevent the introduction of faults during software development, an inevitable element of human error still remains. We must therefore endeavor to ease and accelerate the process of diagnosing and fixing software faults, commonly known as 'debugging'. Current support for debugging occam-pi programs is fairly limited. At best the developer is presented with a reference to the last known code line executed before their program abnormally terminated. This assumes the program does in fact terminate, and does not instead live-lock. In cases where this support is not sufficient, developers must instrument their own tracing support, ``printf style''. An exercise which typically enlightens one as to the true meaning of concurrency... In this paper we explore previous work in the field of debugging occam programs and introduce a new method for run-time monitoring of occam-pi applications, based on the Transterpreter virtual machine interpreter. By adding a set of extensions to the Transterpreter, we give occam-pi processes the ability to interact with their execution environment. Use of a virtual machine allows us to expose program execution state which would otherwise require non-portable or specialised hardware support. Using a model which bears similarities to that applied when debugging embedded systems with a JTAG connection, we describe debugging occam-pi by mediating the execution of one execution process from another.

In the occam-pi programming language, the client-server communication pattern is generally implemented using a pair of unidirectional channels. While each channel's protocol can be specified individually, no mechanism is yet provided to indicate the relationship between the two protocols; it is therefore not possible to statically check the safety of client-server communications. This paper proposes two-way protocols for individual channels, which would both define the structure of messages and allow the patterns of communication between processes to be specified. We show how conformance to two-way protocols can be statically checked by the occam-pi compiler using Honda's session types. These mechanisms would considerably simplify the implementation of complex, dynamic client-server systems.

Distributing process-oriented programs across a cluster of machines requires careful attention to the effects of network latency. The MPI standard, widely used for cluster computation, defines a number of collective operations: efficient, reusable algorithms for performing operations among a group of machines in the cluster. In this paper, we describe our techniques for implementing MPI communication patterns in process-oriented languages, and how we have used them to implement collective operations in PyCSP and occam-pi on top of an asynchronous messaging framework. We show how to make use of collective operations in distributed processoriented applications. We also show how the process-oriented model can be used to increase concurrency in existing collective operation algorithms.

Writing concurrent programs in languages that lack explicit support for concurrency can often be awkward and difficult. Haskell's monads provide a way to explicitly specify sequence and effects in a functional language, and monadic combinators allow composition of monadic actions, for example via parallelism and choice two core aspects of Communicating Sequential Processes (CSP). We show how the use of these combinators, and being able to express processes as first-class types (monadic actions) allow for easy and elegant programming of process-oriented concurrency in a new CSP library for Haskell: Communicating Haskell Processes.

Communicating Sequential Processes (CSP) was developed around a formal algebra of processes and a semantics based on traces (and failures and divergences). A trace is a record of the events engaged in by a process. Several programming languages use, or have libraries to use, CSP mechanisms to manage their concurrency. Most of these lack the facility to record the trace of a program. A standard trace is a flat list of events but structured trace models are possible that can provide more information such as the independent or concurrent engagement of the process in some of its events. One such trace model is View-Centric Reasoning (VCR), which offers an additional model of tracing, taking into account the multiple, possibly imperfect views of a concurrent computation. This paper also introduces ''structural'' traces, a new type of trace that reflects the nested parallelism in a CSP system. The paper describes the automated generation of these three trace types in the Communicating Haskell Processes (CHP) library, using techniques which could easily be applied in other libraries such as JCSP and C++CSP2. The ability to present such traces of a concurrent program assists in understanding the behaviour of real CHP programs and for debugging when the trace behaviours are wrong. These ideas and tools promote a deeper understanding of the association between practicalities of real systems software and the underlying CSP formalism.

When teaching concurrency, using a process-oriented language, it is often introduced through a visual representation of programs in the form of process network diagrams. These diagrams allow the design of and abstract reasoning about programs, consisting of concurrently executing communicating processes, without needing any syntactic knowledge of the eventual implementation language. Process network diagrams are usually drawn on paper or with general-purpose diagramming software, meaning the program must be implemented as syntactically correct program code before it can be run. This paper presents POPed, an introductory parallel programming tool leveraging process network diagrams as a visual language for the creation of process-oriented programs. Using only visual layout and connection of pre-created components, the user can explore process orientation without knowledge of the underlying programming language, enabling a ''processes first'' approach to parallel programming. POPed has been targeted specifically at basic robotic control, to provide a context in which introductory parallel programming can be naturally motivated.

When building simulations of complex systems the task of validation is often overlooked. Validation helps provide confidence in the simulation by exploring the link between the models that we build and the real complex system. We investigate software engineering validation techniques from outside the area of complex systems to assess their applicability for the types of simulation we build. We then provide an example of how such techniques can be applied to a complex systems simulation of cells migrating from blood vessels into lymph nodes through the walls of the blood vessels. We suggest that explicitly stating the modelling and simulation assumptions we make is key to the process of validation. Concluding, we highlight a possible process for validating complex systems that explicitly incorporates environmental aspects.

Complex systems modelling and simulation is becoming increasingly important to numerous disciplines. The CoSMoS project aims to produce a unified infrastructure for modelling and simulating all sorts of complex systems, making use of design patterns and the process-oriented programming model. We provide a description of CoSMoS and present a case study into the modelling of space in complex systems. We describe how two models - absolute geometric space and relational network space - can be captured using process-oriented techniques, and how our models can be refactored to allow efficient, distributed simulation. We identify a number of design, implementation and refactoring patterns that can be applied to future complex systems modelling problems.

The LEGO Mindstorms RCX is a widely deployed educational robotics platform. This paper presents a concurrent operating environment for the Mindstorms RCX, implemented natively using occam-pi running on the Transterpreter virtual machine. A concurrent hardware abstraction layer aids both the developer of the operating system and facilitates the provision of process-oriented interfaces to the underlying hardware for students and hobbyists interested in small robotics platforms.

A fine-grained massively-parallel process-oriented model of platelets (potentially artificial) within a blood vessel is presented. This is a CSP inspired design, expressed and implemented using the occam-pi language. It is part of the TUNA pilot study on nanite assemblers at the universities of York, Surrey and Kent. The aim for this model is to engineer emergent behaviour from the platelets, such that they respond to a wound in the blood vessel wall in a way similar to that found in the human body -- i.e. the formation of clots to stem blood flow from the wound and facilitate healing. An architecture for a three dimensional model (relying strongly on the dynamic and mobile capabilities of occam-pi) is given, along with mechanisms for visualisation and interaction. The biological accuracy of the current model is very approximate. However, its process-oriented nature enables simple refinement (through the addition of processes modelling different stimulants/inhibitors of the clotting reaction, different platelet types and other participating organelles) to greater and greater realism. Even with the current system, simple experiments are possible and have scientific interest (e.g. the effect of platelet density on the success of the clotting mechanism in stemming blood flow: too high or too low and the process fails). General principles for the design of large and complex system models are drawn. The described case study runs to millions of processes engaged in ever-changing communication topologies. It is free from deadlock, livelock, race hazards and starvation em by design, employing a small set of synchronisation patterns for which we have proven safety theorems.

This paper presents the extended and re-integrated JCSP library of CSP packages for Java. It integrates the differing advances made by Quickstones JCSP Network Edition and the core library maintained at Kent. A more secure API for connecting networks and manipulating channels is provided, requiring significant internal re-structuring. This mirrors developments in the occam-pi language for mandated direction specifiers on channel-ends. For JCSP, promoting the concept of channel-ends to first-class entities has both semantic benefit (the same as for occampi) and increased safety. Major extensions include alting barriers (classes supporting external choice over multiple multi-way synchronisations), channel output guards (straightforward once we have the alting barriers), channel poisoning (for the safe and simple termination of networks or sub-networks) and extended rendezvous on channel communications (that simplify the capture of several useful synchronisation design patterns). Almost all CSP systems can now be directly captured with the new JCSP. The new library is available under the LGPL open source license.

The advent of mass-market multicore processors provides exciting new opportunities for parallelism on the desktop. The original C++CSP – a library providing concurrency in C++ – used only user-threads, which would have prevented it taking advantage of this parallelism. This paper details the development of C++CSP2, which has been built around a many-to-many threading model that mixes user-threads and kernel-threads, providing maximum flexibility in taking advantage of multicore and multi-processormachines. New and existing algorithms are described for dealing with the run-queue and implementing channels, barriers and mutexes. The latter two are benchmarked to motivate the choice of algorithm. Most of these algorithms are based on the use of atomic instructions, to gain maximal speed and efficiency. Other issues related to the new design and related to implementing concurrency in a language like C++ that has no direct support for it, are also described. The C++CSP2 library will be publicly released under the LGPL before CPA 2007.

Operating-systems are the core software component of many modern computer systems, ranging from small specialised embedded systems through to large distributed operating-systems. The demands placed upon these systems are increasingly complex, in particular the need to handle concurrency: to exploit increasingly parallel (multicore) hardware; support increasing numbers of user and system processes; and to take advantage of increasingly distributed and decentralised systems. The languages and designs that existing operating-systems employ provide little support for concurrency, leading to unmanageable programming complexities and ultimately errors in the resulting systems; hard to detect, hard to remove, and almost impossible to prove correct. Implemented in occam-pi, a CSP derived language that provides guarantees of freedom from race-hazards and aliasing error, the RMoX operating-system represents a novel approach to operating-systems, utilising concurrency at all levels to simplify design and implementation. This paper presents the USB (universal serial bus) devicedriver infrastructure used in the RMoX system, demonstrating that a highly concurrent process-orientated approach to device-driver design and implementation is feasible, efficient and results in systems that are reliable, secure and scalable.

We are interested in languages that provide powerful abstractions for concurrency and parallelism that execute everywhere, efficiently. Currently, the existing runtime environments for the occam-pi programming language provide either one of these features (portability) or some semblance of the other (performance). We believe that both can be achieved through the careful generation of C from occam-pi, and demonstrate that this is possible using the Transterpreter, a portable interpreter for occam-pi, as our starting point.

The Cell Broadband Engine is a hybrid processor which consists of a PowerPC core and eight vector co-processors on a single die. Its unique design poses a number of language design and implementation challenges. To begin exploring these challenges, we have ported the ttt to the Cell Broadband Engine. The ttt is a small, portable runtime for concurrent languages and can be used as a platform for experimenting with language concepts. This paper describes a preliminary attempt at porting the ttt runtime to the Cell Broadband Engine and explores ways to program it using a concurrent language.

CSP, Hoare's Communicating Sequential Processes, is a formal language for specifying, implementing and reasoning about concurrent processes and their interactions. Existing software tools that deal with CSP directly are largely concerned with assisting formal proofs. This paper presents an alternative use for CSP, namely the compilation of CSP systems to executable code. The main motivation for this work is in providing a means to experiment with relatively large CSP systems, possibly consisting millions of concurrent processes --- something that is hard to achieve with the tools currently available.

Although concurrency is generally perceived to be a `hard' subject, it can in fact be very simple --- provided that the underlying model is simple. The occam-pi parallel processing language provides such a simple yet powerful concurrency model that is based on CSP and the pi-calculus. This paper presents pony, the occam-pi Network Environment. occam-pi and pony provide a new, unified, concurrency model that bridges inter- and intra-processor concurrency. This enables the development of distributed applications in a transparent, dynamic and highly scalable way. The first part of this paper discusses the philosophy behind pony, explains how it is used, and gives a brief overview of its implementation. The second part evaluates pony's performance by presenting a number of benchmarks.

The occam-pi language provides many novel features for concurrent software development. This paper describes a video processing framework that explores the use of these features for multimedia applications. Processes are used to encapsulate operations on video and audio streams; mobile data types are used to transfer data between them efficiently, and mobile channels allow the process network to be dynamically reconfigured at runtime. We present demonstration applications including an interactive video player. Preliminary benchmarks show that the framework has comparable overhead to multimedia systems programmed using traditional methods.

Brooks' subsumption architecture is a design paradigm for mobile robot control that emphasises re-use of modules, decentralisation and concurrent, communicating processes. Through the use of occam-pi the subsumption architecture can be put to use on general purpose modern robotics hardware, providing a clean and robust development approach for the creation of robot control systems.

Cellular automata (CAs) are good examples of systems in which large numbers of autonomous entities exhibit emergent behaviour. Using the occam-pi and JCSP communicating process systems, we show how to construct ``lazy'' and ``just-in-time'' models of cellular automata, which permit very efficient parallel simulation of sparse CA populations on shared-memory and distributed systems.

This paper introduces a safe language binding for CSP multiway events (barriers -- both static and mobile) that has been built into occam-pi (an extension of the classical occam language with dynamic parallelism, mobile processes and mobile channels). Barriers provide a simple way for synchronising multiple processes and are the fundamental control mechanism underlying both CSP (Communicating Sequential Processes) and BSP (Bulk Synchronous Parallelism). Formal semantics (through modelling in classical CSP), implementation details and early performance benchmarks (16 nanoseconds per process per barrier synchronisation on a 3.2 GHz Pentium IV) are presented, along with some likely directions for future research. Applications are outlined for the fine-grained modelling of dynamic systems, where barriers are used for maintaining simulation time and the phased execution of time steps, coordinating safe and desired patterns of communication between millions (and more) of processes. This work forms part of our TUNA project, investigating emergent properties in large dynamic systems (nanite assemblies).

We consider models of emergence, adding downward causation to conventional models where causation permeates from low-level elements to high-level behaviour. We describe an architecture and prototype simulation medium for tagging and modelling emergent features in CA-like systems. This is part of ongoing work on engineering emergence.

Abstract. occam-pi is a programming language based on the CSP process algebra and the pi-calculus, and has a powerful syntax for expressing concurrency. occam-pi does not however, come with interfaces to a broad range of standard libraries (such as those used for graphics or mathematics). Programmers wishing to use these must write their own wrappers using occam-pi?s foreign function interface, which can be tedious and time consuming. SWIG offers automatic generation of wrappers for libraries written in C and C++, allowing access to these for the target languages supported by SWIG. This paper describes the occam-pi module for SWIG, which will allow automatic wrapper generation for occam-pi, and will ensure that occam-pi?s library base can be grown in a quick and efficient manner. Access to database, graphics and hardware interfacing libraries can all be provided with relative ease when using SWIG to automate the bulk of the work.

This paper describes an extension to the KRoC occam-pi system that allows processes programmed in C to participate in occam-pi style concurrency. The uses of this are wide-ranging, from providing low-level C processes running concurrently as part of an occam-pi network, through to concurrent systems programmed entirely in C. The easily extended API for C processes is based on the traditional Inmos C API, used also by CCSP, extended to cover new features of occampi. One of the motivations for this work is to ease the development of low-level network communication infrastructures. A library that provides for networking of channel-bundles over TCP/IP networks is presented, in addition to initial performance figures.

This paper introduces a safe language binding for CSP multiway events (barriers) that has been built into occampi (an extension of the classical occam language with dynamic parallelism, mobile processes and mobile channels). Barriers provide a simple way for synchronising multiple processes and are the fundamental control mechanism underlying both CSP (Communicating Sequential Processes) and BSP (Bulk Synchronous Parallelism). The occampi barriers are more general than those of BSP (an occampi system can contain any number of barriers, with some processes ignoring them and some registered with many). On the other hand, they are also, currently, less general than those of CSP (occampi processes must commit to barrier synchronisation -- it cannot be used as part of a choice or ALT). Structured support for resignation, a higher-level CSP design pattern, is also built into occampi barriers. Applications are outlined for fine-grained modelling of dynamic systems, where the barriers are used for maintaining simulation time and synchronising safe access to shared data between millions of processes. Implementation details and early performance benchmarks (16 nanoseconds per process per barrier synchronisation on a 3.2 GHz. Pentium IV) are also presented, along with some likely directions for future research.

This paper describes our initial experiences of running simple blood-clot simulations on Grid infrastructure. The individual simulations are concurrent process networks programmed in occampi, containing over ten thousand parallel processes. The Minimum intrusion Grid (MiG) infrastructure is used to distribute program execution and result collection automatically across a set of processing nodes.

This paper introduces occam-pi, an efficient and safe binding of key elements from Hoare's CSP and Milner's pi-calculus into a programming language of industrial strength. A brief overview of classical occam is presented, before focussing on the extensions providing data, channel and process mobility. Some implementation details are given, along with current benchmark results. Application techniques exploiting mobile processes for the direct modelling of large-scale natural systems are outlined, including the modelling of locality (so that free-ranging processes can locate each other). Run-time overheads are sufficiently low so that systems comprising millions of dynamically assembling and communicating processes are practical on modest processor resources. The ideas and technology will scale further to address larger systems of arbitrary complexity, distributed over multiple processors with no semantic discontinuity. Semantic design, comprehension and analysis are made possible through a natural structuring of systems into multiple levels of network and the compositionality of the underlying algebra.

This paper presents a new model for mobile processes in occam-pi. A process, embedded anywhere in a dynamically evolving network, may suspend itself mid-execution, be safely disconnected from its local environment, moved (by communication along a channel), reconnected to a new environment and reactivated. Upon reactivation, the process resumes execution from the same state (i.e. data values and code positions) it held when it suspended. Its view of its environment is unchanged, since that is abstracted by its synchronisation (e.g. channels and barriers) interface and that remains constant. The environment behind that interface will (usually) be completely different. The mobile process itself may contain any number of levels of dynamic sub-network. This model is simpler and, in some ways, more powerful than our earlier proposal, which required a process to terminate before it could be moved. Its formal semantics and implementation, however, throw up extra challenges. We present details and performance of an initial implementation.

This paper reports the specification of a sound concept for the mobility of network-channel-types in KRoC.net. The syntax and semantics of KRoC.net have also been modified in order to integrate it more seamlessly into the occam-pi language. These new features are currently in the process of being implemented. Recent developments in occam-pi and KRoC (such as live/dead channel-type-ends and mobile processes) are described, together with their impact on KRoC.net. This paper gives an overview of the recent developments in KRoC.net, and presents its proposed final semantics, as well as the proposed interface between the KRoC.net infrastructure and the KRoC compiler.

Circus is a new notation that may be used to specify both data and behaviour aspects of a system, and has an associated refinement calculus. Although a few case studies are already available in the literature, the industrial fire control system presented in this paper is, as far as we know, the largest case study on the Circus refinement strategy. We describe the refinement and present some new laws that were needed. Our case study makes extensive use of mutual recursion; a simplified notation for specifying such systems and proving their refinements is proposed here.

Aliasing problems are a major source for error in traditional imperative languages (such as C) and modern object-oriented languages (such as Java, C++ and C#). Add in concurrency and the problems compound exponentially. Improperly synchronized access to shared (i.e. aliased) resources leads to problems of race hazard, deadlock, livelock and starvation. This paper describes the binding into occam (a concurrent processing language based on CSP) of a secure, dynamic and efficient way of sharing data between parallel processes with minimal synchronization overheads. The key new facilities provided are: a movement semantics for assignment and communication, strict zero-aliasing, apparently dynamic memory allocation and automatic zero-or-very-small-unit-time garbage collection. With occam becoming available on a variety of microprocessors for GUI building, internet services and small-memory-footprint embedded products, these capabilities are timely. Lessons are drawn for concurrency back in OO languages - and especially for the JCSP (''CSP for Java'') package library. The computer graphics industry, and in particular those involved with films, games and virtual reality, continue to demand more and more realistic computer generated images. The complexity of the scenes being modelled and the high fidelity required of the images means that rendering is simply not possible in a reasonable time (let alone real-time) on a single computer. Interactive ray tracing exists today, but real-time global illumination remains a major challenge. Fortunately, .computer graphics cards are developing at ''Moore's law cubed'' [David Kirk, Chief Scientist, nVIDIA]. Such performance increases are directly due to the inherent parallel nature of modern graphics cards. If this trend continues, they will be 100 times faster in a mere 3.5 years time, 1000 times faster in 5 years and they will be massively parallel. Unfortunately, past experiences in designing systems that can exploit parallel processors in anything beyond embarrassingly trivial ways are not encouraging. For real-time interaction with high fidelity images, the parallel processing requirements will not be embarrassingly trivial! Regular and irregular patterns of synchronisation and communication will have to be managed over networks of fine-grained (for accuracy) model components whose scale, topology and physical distribution are dynamically evolving. This paper reviews weaknesses in our standard approaches to the design and implementation of concurrent systems and describes ways forward that are mature and practical -- both for the programmer to program and the hardware to execute. They are built on decades of research into process algebrae (CSP and the pi-calculus), but are able to preserve and exploit traditional skills and capabilities of serial software engineering and von Neumann architecture (components of which will still form the processor base of parallel systems for at least the next decade). The changes are, therefore, evolutionary rather than revolutionary -- but are nevertheless essential botn the field of graphics and for the wider Grand Challenges of computer science.

KRoC.net is an extension to KRoC supporting the distribution of occam channels over networks, including the internet. Starting in 2001, the development of KRoC.net has gone through a number of stages, each one making the system more flexible, transparent and dynamic. It now enables the occam programmer to set up and close network channels dynamically. Configuration has been simplified. All occam PROTOCOLs can now be sent over network channels, without need for conversion. Many of the new dynamic features in occam have been used to improve KRoC.net. Many of the concepts in KRoC.net are similar to those in the JCSP Network Edition (JCSP.net), KRoC.net's counterpart in the JCSP world. This paper will give an overview over KRoC.net, its usage, its design and implementation, and its future. It will also provide some benchmarks and discuss how the new occam features are being used in the latest KRoC.net version.

This paper reports on a CSP library for C++, developed over the past year at the University of Kent. It is based on the OO-design and API of JCSP and the lightweight algorithms of KRoC occam, with extensions to exploit specific C++ capabilities (such as templates). Both user-level and operating system threads are used to provide a range of oimplementation options and semantics (e.g. for managing blocking system calls intelligently) that run efficiently under either Windows or Linux. The library is presented from the user's point of view, mainly by way of a tutorial. Implementation details are also outlines and some benchmark results given. The performance of C++CSP is between that of KRoC occam and JCSP -- fairly close to KRoC.

This paper reports continuing research on language design, compilation and kernel support for highly dynamic concurrent reactive systems. The work extends the occam multiprocessing language, which is both sufficiently small to allow for easy experimentation and sufficiently powerful to yield results that are directly applicable to a wide range of industrial and commercial practice. Classical occam was designed for embedded systems and enforced a number of constraints - such as statically pre-determined memory allocation and concurrency limits - that were relevant to that generation of application and hardware technology. Most of these constraints have been removed in this work and a number of new facilities introduced (channel structures, mobile channels, channel ends, dynamic process creation, extended rendezvous and process priorities) that significantly broaden occam?s field of application and raise the level of concurrent system design directly supported. Four principles were set for modifications/enhancements of the language. They must be useful and easy to use. They must be semantically sound and policed (ideally, at compile-time) to prevent mis-use. They must have very lightweight and fast implementation. Finally, they must be aligned with the concurrency model of the original core language, must not damage its security and must not add (significantly) to the ultra-low overheads. These principles have all been observed. All these enhancements are available in the latest release (1.3.3) of KRoC, freely available (GPL/open source) from: http://www.cs.ukc.ac.uk/projects/ofa/kroc/ .

Hoare's algebra of Communicating Sequential Processes (CSP) enables a view of systems as layered networks of concurrent components, generating and responding to events communicated to each other through channels, barriers and other formally defined synchronisation primitives. The resulting image and discipline is close to hardware design and correspondingly easy to visualise, reason about, compose and scale. JCSP is a library of Java packages providing an (occam) extended version of this model that may be used alongside, or as a replacement for, the very different threads-and-monitors concurrency mechanisms built into Java. The current release (JCSP 1.0) supports concurrency within a single Java Virtual Machine (which may be multi-processor). This paper reports early experiments with JCSP.net, an extension of JCSP for the dynamic construction of CSP networks across distributed environments. The aims of JCSP.net are to simplify the construction and programming of dynamically distributed and parallel systems. It provides high-level support for CSP architectures, unifying concurrency logic within and between processors. The experiments are on some classical HPC problems, an area of work for which JCSP.net was not primarily designed. However, low overheads in the supporting infrastructure were a primary consideration - along with an intuitive and high-level distributed programming model (based on CSP). Results reported show JCSP holding up well against - and often exceeding - the performance obtained from existing tools such as mpiJava and IBM's TSpaces. The experimental platform was a cluster of 16 dual-processor PIII Linux machines. It is expected that future optimisations in the pipeline for the JCSP.net infrastructure will improve the results presented here. JCSP and JCSP.net were developed at the University of Kent.

This paper illustrates the work presented in 'Part I', giving additional examples of use of channel-types, extended rendezvous and FORKs that lean towards real applications. Also presented are a number of other additions and extensions to the occam language that correct, tidy up or complete facilities that have long existed. These include fixing the PRI ALT bug, allowing an unconditional SKIP guard as the last in a PRI ALT, replicator STEP sizes, run-time computed PAR replication counts, RESULT parameters and abbreviations, nested PROTOCOL definitions, inline array constructors and parallel recursion. All are available in the latest release (1.3.3) of KRoC, freely available (GPL/open source) from: http://www.cs.ukc.ac.uk/projects/ofa/kroc/ .

Concurrency is thought to be an advanced topic - much harder than serial computing which, therefore, needs to be mastered first. This paper contends that this tradition is wrong, which has radical implications for the way we educate people in Computer Science - and on how we apply what we have learnt. A process-oriented design pattern for concurrency is presented with a specific binding for Java. It is based on the algebra of .Communicating Sequential Processes. (CSP) as captured by the JCSP library of Java classes. No mathematical sophistication is needed to master it. The user gets the benefit of the sophistication underlying CSP simply by using it. Those benefits include the simplification wins we always thought concurrency should generate. Although the Java binding is new, fifteen years of working with students at Kent have shown that the ideas within process-oriented design can be quickly absorbed and applied. Getting the ideas across as soon as possible pays dividends - the later it's left, the more difficult it becomes to wean people off serial ways of thought that often fit applications so badly. Concurrency for all (and for everyday use) in the design and implementation of most kinds of computer system is both achievable and necessary

JCSP is a library of Java packages providing an extended version of the CSP/occam model for Communicating Processes. The current (1.0) release supports concurrency within a single Java Virtual Machine (which may be multi-processor). This paper presents recent work on extended facilities for the dynamic construction of CSP networks across distributed environments (such as the Internet). Details of the underlying network fabric and control (such as machine addresses, socket connections, local multiplexing and de-multiplexing of application channels, acknowledgement packets to preserve synchronisation semantics) are hidden from the JCSP programmer, who works entirely at the application level and CSP primitives. A simple brokerage service - based on channel names - is provided to let distributed JCSP components find and connect to each other. Distributed JCSP networks may securely evolve, as components join and leave at run-time with no centralised or pre-planned control. Higher level brokers, providing user- defined matching services, are easy to bootstrap on top of the basic Channel Name Server (CNS) - using standard JCSP processes and networking. These may impose user-defined control over the structure of network being built. JCSP network channels may be configured for the automatic loading of class files for received objects whose classes are not available locally (this uses the network channel from which they were received - the sender must have them). Also provided are connection channels (for extended bi-directional transactions between clients and servers) and anonymous channels (to set up communications without using any central registry - such as the given CNS). The aims of JCSP.net are to simplify the construction and programming of dynamically distributed and parallel systems. It provides high-level support for CSP architectures, unifying concurrency logic within and between processors. Applications cover all areas of concurrent computing - including e-commerce, agent technology, home networks, embedded systems, high-performance clusters and The Grid.

F.R.M. Barnes and P.H. Welch Communicating Process Architectures 2001 (WoTUG 24) Traditional imperative languages (such as C) and modern object-oriented languages are plagued by uncontrolled resource aliasing problems. Add in concurrency and the problems compound exponentially. Improperly synchronised access to shared (i.e. aliased) resources leads to problems of race-hazard, deadlock, livelock and starvation. This paper describes the binding into occam (a concurrent processing language based on CSP) of a secure, dynamic and efficient way of sharing data between parallel processes with minimal synchronisation overheads. The key new facilities provided are: a movement semantics for assignment and communication, strict zero-aliasing, apparently dynamic memory allocation and automatic zero-or-very-small-unit-time garbage collection. The implementation of this mechanism is also presented, along with some initial performance figures (e.g. 80ns for mobile communication on an 800 MHz Pentium 3). With occam becoming available on a variety of microprocessors for GUI building, internet services and small-memory-footprint embedded products, these capabilities are timely. Lessons are drawn for concurrency back in OO languages - and especially for the JCSP (CSP for Java) package library.

Aliasing problems are a major source for error in traditional imperative languages (such as C) and modern object-oriented languages (such as Java, C++ and C#). Add in concurrency and the problems compound exponentially. Improperly synchronized access to shared (i.e. aliased) resources leads to problems of race hazard, deadlock, livelock and starvation. This paper describes the binding into occam (a concurrent processing language based on CSP) of a secure, dynamic and efficient way of sharing data between parallel processes with minimal synchronization overheads. The key new facilities provided are: a movement semantics for assignment and communication, strict zero-aliasing, apparently dynamic memory allocation and automatic zero-or-very-small-unit-time garbage collection. With occam becoming available on a variety of microprocessors for GUI building, internet services and small-memory-footprint embedded products, these capabilities are timely. Lessons are drawn for concurrency back in OO languages - and especially for the JCSP (''CSP for Java'') package library.

Java threads are synchronised through primitives based upon monitor concepts developed in the early 1970s. The semantics of Java's primitives have only been presented in natural language ? this paper remedies this with a simple and formal CSP model. In view of the dif?culties encountered in reasoning about any non-trivial interactions between Java threads, being able to perform that reasoning in a formal context (where careless errors can be highlighted by mechanical checks) should be a considerable con?dence boost. Further, automated model-checking tools can be used to root out dangerous states (such as deadlock and livelock), ?nd overlooked race hazards and prove equivalence between algorithms (e.g. between optimised and unoptimised versions). A case study using the CSP model to prove the correctness of the JCSP and CTJ channel implementations (which are built using standard Java monitor synchronisation) is presented. In addition, the JCSP mechanism for ALTing (i.e. waiting for and, then, choosing between multiple events) is veri?ed. Given the history of erroneous implementations of this key primitive, this is a considerable relief.

Java provides support for concurrent and parallel programming through threads, monitors and its socket and Remote Method Invocation (RMI) classes. However, there have been many concerns expressed about the way in which this support is provided, e.g., [1][2], citing problems such as improper implementation of monitors and difficulty of programming with threads. Hoare's Communicating Sequential Processes (CSP) [3][4][5] model fully specifies thread synchronization and is based on processes, compositions, and channel communication. It provides a mathematical notation for describing patterns of communication using algebraic expressions and contains formal proofs for analyzing, verifying and eliminating undesirable conditions, such as race hazards, deadlocks, livelock, and starvation. Two independent research efforts provide a CSP based process-oriented design pattern for concurrency implemented in Java: Communicating Sequential Processes for Java (JCSP) [6] and Communication Threads in Java (CTJ) [7]. In this paper, we compare these two packages, looking at the philosophy behind their development, their similarities, their differences, their performance, and their use.

This paper describes an extension to Kent Retargetable occam Compiler (KRoC), which enables the execution of a blocking call, without blocking the occam-kernel. This allows a process to make a blocking system call (eg, read, write), without blocking processes running in parallel with it. Blocking calls are implemented using Linux clones which communicate using shared memory, and synchronise using kernel level semaphores. The usefulness of this is apparent in server applications with a need to handle multiple clients simultaneously. An implementation of an occam web-server is described in section 5, which uses standard TCP sockets via an occam socket library. The web-server comes with the ability to execute CGI scripts as well as dispensing static pages, which demonstrates some level of OS process management from within occam. However, this mechanism is not limited to blocking in the Linux kernel. On multi- processor machines, the clones are quite free to be scheduled on different processors, allowing computationally heavy processing to be performed aside the occam world, but still with a reasonable level of interaction with it. Using them in this way provides a coarse-grained level of parallelism from within the fine-grained occam world.

Java threads are synchronised through primitives based upon monitor concepts developed in the early 1970s. The semantics of Java's primitives have only been presented in natural language - this paper remedies this with a simple and formal CSP model. In view of the difficulties encountered in reasoning about any non-trivial interactions between Java threads, being able to perform that reasoning in a formal context (where careless errors can be highlighted by mechanical checks) should be a considerable confidence boost. Further automated model-checking tools can be used to root out dangerous states (such as deadlock and livelock), find overlooked race hazards and prove equivalence between algorithms (e.g. between optimised and un-optimised versions). A case study using the CSP model to prove the correctness of the JCSP channel implementation (which is built in terms of standard Java monitor synchronisations) is presented.

Concurrency is thought to be an advanced topic - much harder than serial computing which, therefore, needs to be mastered first. This paper contends that this tradition is wrong, which has radical implications for the way we educate people in Computer Science - and on how we apply what we have learnt. A process-oriented design pattern for concurrency is presented with a specific binding for Java. It is based on the algebra of Communicating Sequential Processes (CSP) as captured by the JCSP library of Java classes. No mathematical sophistication is needed to master it. The user gets the benefit of the sophistication underlying CSP simply by using it. Those benefits include the simplification wins we always thought concurrency should generate. Although the Java binding is new, fifteen years of working with students at Kent have shown that the ideas within process-oriented design can be quickly absorbed and applied. Getting the ideas across as soon as possible pays dividends - the later it's left, the more difficult it becomes to wean people off serial ways of thought that fit the world so badly. Concurrency for all (and for everyday use) in the design and implementation of most kinds of computer system is both achievable and necessary.

The design of concurrent programs has a reputation for being difficult, and thus potentially dangerous in safety-critical real-time and embedded systems. The recent appearance of Java, with its simple thread model, and new CASE tools that can verify and check the design of concurrent applications, now significantly reduce design and testing time and eliminate those problems which commonly plague concurrent systems. Our approach uses recently developed Java class libraries based on Hoare's Communicating Sequential Processes (CSP); the use of CSP greatly simplifies the design of concurrent systems and, in many cases, a parallel approach often significantly simplifies systems originally approached sequentially. New CSP CASE tools permit designs to be verified against formal specifications and checked for deadlock and livelock. Below we introduce CSP and its implementation in Java and develop a small concurrent application. The formal CSP description of the application is provided, as well as that of an equivalent sequential version. FDR is used to verify the correctness of both implementations, their equivalence, and their freedom from deadlock and livelock.

A new set of synchronisation primitives is described that simplifies the control of very large numbers of fine-grained parallel processes. The new primitives are derived from the multi-way event synchronisation and choice defined in communicating sequential processes (CSP). EVENT provides for dynamically structured and multiple barrier synchronisation that is completely deterministic in its semantics. BUCKET provides for an explicitly non-deterministic version of an EVENT, where the non-determinism is triggered by a programmable internal action. These primitives may be combined with standard CSP channel communication to design and implement a highly parallel model of (e.g.) an urban traffic network. The model is simple to create and understand, being object-oriented with components that directly reflect objects on the ground. The performance and scalability both of the primitives and of the traffic model are discussed in terms of their implementation on a DEC Alpha-based multiprocessor. Overheads for managing channel communications and the EVENT/BUCKET primitives are very light, so that the direct execution of highly parallel designs remains efficient down to very fine levels of granularity. An example is presented that operates more than 100 times faster than real time on a single processor, context switching at more than 250,000 times per second. Going multiprocessor allows larger models to be executed at similar speeds. Feedback from such models enables different kinds of analysis to tried ahead of real time, so that the most effective remedial strategies can be found and adopted within real time.

Many internet, real-time and embedded applications are most naturally designed using concurrency. Unfortunately, the design of concurrent (multithreaded) programs has the reputation of being extremely difficult and dangerous, due to the possibility of deadlock, livelock, race hazards, or starvation - phenomena not encountered in single-threaded programs. Lea [1] emphasizes concern for the apparent difficulty: "Liveness considerations in concurrent software development introduce context dependencies that can make the construction of reusable components harder than in strictly sequential settings." Two approaches he suggests for design sound tedious and perhaps risky: "Top-down (safety first): Initially design methods and classes assuming full synchronization (when applicable), and then remove unnecessary synchronization as needed to obtain liveness and efficiency...Bottom up (liveness first): Initially design methods and classes without concern for synchronization policies, then add them via composites, subclassing, and related layering techniques..." Both suggest lengthy sessions of patching and testing until the application appears to work as desired. Even those intimately connected with Java seem reluctant to employ more than a single thread. The Swing documentation states "If you can get away with it, avoid using threads. Threads can be difficult to use, and they make programs harder to debug. In general, they just aren\'t necessary for strictly GUI work, such as updating component properties" [2]. Oaks and Wong [3], also associated with Sun, are more positive, but note that "Deadlock between threads competing for the same set of locks is the hardest problem to solve in any threaded program. It\'s a hard enough problem, in fact, that we will not solve it or even attempt to solve it." Later they state "Nonetheless, a close examination of the source code is the only option presently available to determine if deadlock is a possibility..." and add that no tools exist for detecting deadlock in Java programs. We feel, however, based on fifteen years of experience, that concurrent approaches are the best way to design most programs. Done properly (e.g., using CSP [4]) this results in better understanding of the problem and the solution, and leads to much cleaner implementations. A tremendous amount of work has been done on and with CSP in recent years, and the present state of the language and the tools offers the Java programmer excellent facilities for the design and analysis of multithreaded programs. Furthermore, Java designs based on CSP class libraries can now be verified against formal specifications and checked for deadlock and livelock with CASE tools - prior to implementation. We present the CSP model (processes, channels, events, networks) and its binding into (100% Pure) Java through the CSP class libraries developed at Kent [5] and Twente [6]. We describe some of the tools associated with CSP (e.g., FDR [7]) and demonstrate, in several practical applications, their use for checking specifications and proving the absence of deadlock. We emphasize that CSP concepts are easy to understand and apply and that the engineering benefits they confer on system design and implementation are significant for both real-time and non-real-time multithreaded systems.

The natural world is certainly not organised through a central thread of control. Things happen as the result of the actions and interactions of unimaginably large numbers of independent agents, operating at all levels of scale from nuclear to astronomic. Computer systems aiming to be of real use in this real world need to model, at the appropriate level of abstraction, that part of it for which it is to be of service. If that modelling can reflect the natural concurrency in the system, it ought to be much simpler Yet, traditionally, concurrent programming is considered to be an advanced and difficult topic - certainly much harder than serial computing which, therefore, needs to be mastered first. But this tradition is wrong. This talk presents an intuitive, sound and practical model of parallel computing that can be mastered by undergraduate students in the first year of a computing (major) degree. It is based upon Hoare's mathematical theory of Communicating Sequential Processes (CSP), but does not require mathematical maturity from the students - that maturity is pre-engineered in the model. Fluency can be quickly developed in both message-passing and shared-memory concurrency, whilst learning to cope with key issues such as race hazards, deadlock, livelock, process starvation and the efficient use of resources. Practical work can be hosted on commodity PCs or UNIX workstations using either Java or the Occam multiprocessing language. Armed with this maturity, students are well-prepared for coping with real problems on real parallel architectures that have, possibly, less robust mathematical foundations.

Java provides support for parallel computing through a model that is built into the language itself. However, the designers of Java chose to be fairly conservative and settled for the concepts of threads and monitors. Monitors were developed by Tony Hoare (and others) in the early 1970s as a structured way of using semaphores to control access to shared resources. Hoare moved away from this, in the late 1970s, to develop the theory of Communicating Sequential Processes (CSP). One reason was that the semantics of monitors are not WYSIWYG, so that designing robust parallel algorithms at this level is seriously hard. This tutorial will look at how this impacts on threaded applications written in Java. Fortunately, it is possible to introduce the CSP model into Java through sets of classes implemented on top of its monitor support. By restricting interaction between active Java objects to CSP synchronisation primitives, Java thread semantics become compositional and systems with arbitrary levels of complexity become possible. Multi-threadedWeb applets and distributed applications become simpler to design and implement, race hazards never occur, difficulties such as starvation, deadlock and livelock are easier to confront and overcome; and performance is no worse than that obtained from directly using the raw monitor primitives. The advantages of teaching parallelism in Java purely through the CSP class librarieswill be discussed. These libraries were developed jointly at Kent and Oxford Universities in the U.K. and the University of Twente in the Netherlands. This paper was developed from material first presented at the Java Threads Workshop [1]. It presents the basic threads model of Java, discusses why they may be a good thing but why they need special care in their management, runs through the monitor mechanisms provided in Java for their control and points out weaknesses in that control. Finally, the CSP primitives are introduced and the case for ignoring the monitor methods presented. This work is one of the foundation stones of the JavaPP project [2], which spun out from the above workshop. The other founding stones [3, 4, 5, 6] were first presented at the WoTUG-20 conference last year.

Four new synchronisation primitives (SEMAPHOREs, RESOURCEs, EVENTs and BUCKETs) were introduced in the KRoC 0.8beta release of occam for SPARC (SunOS/Solaris) and Alpha (OSF/1) UNIX workstations [1][2][3]. This paper reports on the rationale, application and implementation of two of these (SEMAPHOREs and EVENTs). Details on the other two may be found on the web [4]. The new primitives are designed to support higher-level mechanisms of SHARING between parallel processes and give us greater powers of expression. They will also let greater levels of concurrency be safely exploited from future parallel architectures, such as those providing (virtual) shared-memory. They demonstrate that occam is neutral in any debate between the merits of message-passing versus shared-memory parallelism, enabling applications to take advantage of whichever paradigm (or mixture of paradigms) is the most appropriate. The new primitives could be (but are not) implemented in terms of traditional channels, but only at the expense of increased complexity and computational overhead. The primitives are immediately useful even for uni-processors - for example, the cost of a fair ALT can be reduced from O(n) to O(1). In fact, all the operations associated with new primitives have constant space and time complexities; and the constants are very low. The KRoC release provides an Abstract Data Type interface to the primitives. However, direct use of such mechanisms still allows the user to misuse them. They must be used in the ways prescribed (in this paper and in [4]) else their semantics become unpredictable. No tool is provided to check correct usage at this level. The intention is to bind those primitives found to be useful into higher level versions of occam. Some of the primitives (e.g. SEMAPHOREs) may never themselves be made visible in the language, but may be used to implement bindings of higher-level paradigms (such as SHARED channels and BLACKBOARDs). The compiler will perform the relevant usage checking on all new language bindings, closing the security loopholes opened by raw use of the primitives. The paper closes by relating this work with the notions of virtual transputers, microcoded schedulers, object orientation and Java threads.

A multi-processor implementation of occam2.1 for interconnected DEC Alpha processors has been derived from the Kent Retargetable occam Compiler. Each Alpha processor is supported over a PCI bus by a T425 transputer, whose links complete the communications fabric. This paper reports on the software mechanisms for supporting these platforms from occam so that they appear just like any transputer system - a collection of processing nodes connected by channels placed on links. Advantage was taken of a proprietary multi-threading kernel, supplied as part of 3L Parallel C/AXP, to support parallel inter-node communication. occam multiprocessing is supported by the KRoC kernel running within one of the 3L threads. The performance of generated code and networked systems has been benchmarked, with particular care being taken to measure tile interaction overheads between the Alpha and its communication fabric. An image analysis program was also used in the benchmarking as an example of a real multi-processor application.

Java provides support for parallel computing through a model that is built into the language itself. However, the designers of Java chose to be fairly conservative and settled for the concepts of threads and monitors. Monitors were developed by Tony Hoare in the early 1970s as a structured way of using semaphores to control access to shared resources. Hoare moved away from this, in the late 1970s, to develop the theory of Communicating Sequential Processes (CSP). One reason for this was that the semantics of monitors and threads are not WYSIWIG, so that designing robust parallel algorithms at this level is seriously hard.

Four new synchronisation primitives (SEMAPHOREs, RESOURCEs, EVENTs and BUCKETs) were introduced in the KRoC 0.8beta release of occam for SPARC (SunOS/Solaris) and Alpha (OSF/1) UNIX workstations [1][2][3]. This paper reports on the rationale, application and implementation of two of these (SEMAPHOREs and EVENTs). Details on the other two may be found on the web [4]. The new primitives are designed to support higher-level mechanisms of SHARING between parallel processes and give us greater powers of expression. They will also let greater levels of concurrency be safely exploited from future parallel architectures, such as those providing (virtual) shared-memory. They demonstrate that occam is neutral in any debate between the merits of message-passing versus shared-memory parallelism, enabling applications to take advantage of whichever paradigm (or mixture of paradigms) is the most appropriate. The new primitives could be (but are not) implemented in terms of traditional channels, but only at the expense of increased complexity and computational overhead. The primitives are immediately useful even for uni-processors - for example, the cost of a fair ALT can be reduced from O(n) to O(1). In fact, all the operations associated with new primitives have constant space and time complexities; and the constants are very low. The KRoC release provides an Abstract Data Type interface to the primitives. However, direct use of such mechanisms still allows the user to misuse them. They must be used in the ways prescribed (in this paper and in [4]) else their semantics become unpredictable. No tool is provided to check correct usage at this level. The intention is to bind those primitives found to be useful into higher level versions of occam. Some of the primitives (e.g. SEMAPHOREs) may never themselves be made visible in the language, but may be used to implement bindings of higher-level paradigms (such as SHARED channels and BLACKBOARDs). The compiler will perform the relevant usage checking on all new language bindings, closing the security loopholes opened by raw use of the primitives. The paper closes by relating this work with the notions of virtual transputers, microcoded schedulers, object orientation and Java threads.

Serialisation is a key technique for making the most efficient use of multi-processor architecture. It aims at creating a system which is as modular as possible by exploiting parallelism and processes without considering the restriction of the architecture. Afterwards, through transformation, the number of processes is reduced to achieve the required performance. We present composition and abstraction rules for the construction of deadlock-free systems, and transformation rules to reduce the number of processes in order to improve the system's performance. We also describe the graphical interface to support the automatic development of systems based on serialisation.

This paper outlines a new language and run-time technology offering formalised design and effiecient implementation for highly concuurent dynamic systems. It is based on a careful combination of ideas from Hoare's CSP (giving compositional semantics, refinement and safety/liveness analysis) and Milners's pi-calculus (giving dynamic network construction and mobility). We have been experimenting with systems developing as layered networks of self-organising neighbourhood-aware communicating processes, with no need for advanced planning or centralised control. The work reported is part of our TUNA ('Theories Undepinning Nanite Assemblies') project, in parnership with colleagues from the Universities of York and Surry, which is investigating formal approaches to the capture of safe emergent behaviour in highly complex systems. A particular study modelling artificial blood platelets is described. The software technology scales to millions of processes per processor and distributes over common multiprocssor clusters.

This paper outlines the design and performance of a system for executing occam programs on multiprogrammed shared memory multiprocessor workstations. In particular, a fast SMP scheduler that executes process code generated by the standard KRoC compiler (originally designed for uniprocessors) is described; new wait-free multiprocessor-safe algorithms for both committed and alternative CSP channel communication operations are presented; a technique for allowing surplus processors to idle altruistically under a multiprogrammed regime is outlined. The fun-time performance of the system is measured under a range of process granularities on one to four processors, using a synthetic benchmark. The performance of two real applications; namely QuickerSort and matrix multiplication, is then analysed in some detail. Finally, alternative scheduling strategies to further improve the scalability of the system under conditions of wry fine process granularity are proposed.

Java provides support for parallel computing through a model that is built into the language itself. However, the designers of Java chose to be fairly conservative and settled for the contepts of t

This paper presents a graphical design tool for the construction of multi-process systems that are guaranteed free from deadlock, livelock and starvation. The tool is strictly targeted to implement

A high-speed bus, the Octobus, has been designed to be used with Transputer hardware for very-high bandwidth low-latency sharing of large datasets (e.g. video). It provides one-to-one, one-to-many

This book is a collection of the papers presented at the 32nd Communicating Process Architecture conference (CPA), held at the Technical University Eindhoven, the Netherlands, from the 1st to the 4th of November 2009. Concurrency is a fundamental mechanism of the universe, existing in all structures and at all levels of granularity. To be useful in this universe, any computer system has to model and reflect an appropriate level of abstraction. For simplicity, therefore, the system needs to be concurrent -- so that this modeling is obvious and correct. Today, the commercial reality of multicore processors means that concurrency issues can no longer be ducked if applications are going to be able to exploit more than an ever-diminishing fraction of their power. This is a second, but very forceful, reason to take this subject seriously. We need theory and programming technology that turns this around and makes concurrency an elementary part of the everyday toolkit of every software engineer. This is what these proceedings are all about. Subjects covered in this volume include: system design and implementation for both hardware and software; tools for concurrent programming languages, libraries and run-time kernels; and formal methods and applications.

The study of Complex Systems is growing rapidly, and modelling and simulation tools are an important part of the process. This volume brings together work from a multidisciplinary group of scientists, from biology and computer science, who are studying a variety of techniques and applications for modelling and simulating complex systems. A common theme emerging from much of this work is an emphasis on validation: how one can have confidence that a computer simulation is saying something sensible about the complex real-world domain of interest.

Communicating Process Architectures 2008 contains the proceedings of the thirty-first CPA conference, organized under the auspices of WoTUG and the Department of Computer Science of the University of York. The aim of this book is to cover both theoretical aspects and industrial applications of Communicating Processes. Two invited speakers have given excellent contributions to this topic. Professor Samson Abramsky has worked in the areas of semantics and logic of computation, and concurrency. His work on game semantics considers interaction and information flow between multiple agents and their environment. This has yielded new approaches to compositional model-checking and to analysis for programs with state, concurrency, probability and other features. Professor Colin O'Halloran has been instrumental in the uptake of formal methods in the development and verification of high assurance systems on an industrial scale. His research interests are in automating the use of formal methods, and using these techniques at reasonable cost and on an industrial scale.

Contains papers from the conference Communicating Process Architectures, 2006. This work talks about various aspects of communicating process theory and their application to designing and building systems. It includes a case study on large scale formal development and verification, CSP mechanisms for Microsoft's .NET framework, and more.