Ebook: Communicating Process Architectures 2006

Napier University in Edinburgh are very pleased to be hosting this year's Communicating Process Architectures 2006 conference. It is perhaps appropriate that a meeting concerning simple ways of designing, implementing and reasoning about concurrent systems should be held in an institution named after the inventor of a simple, and highly concurrent, adding machine. The house in which John Napier lived forms part of the campus where the meeting is being held.

This is the 29th meeting in this conference series. The first was a single day workshop, organised by Inmos, and took place in Bristol in 1985. With the success of the Transputer, we grew into an international conference, with proceedings formally published by IOS Press since March 1988. The fact that we are still here – and thriving – shows that the founding ideas have continuing relevance. Indeed, we believe they are still ahead of the game.

The papers this year are as varied and wide ranging as ever and we thank all the authors for their efforts in submitting papers and returning the camera ready copies to a very tight time schedule. Subjects include various aspects of communicating process theory and their application to designing and building systems. One of the hottest current topics – safe and effective programming models for multicore processors (e.g. IBM's Cell) – has a natural home in this community and is addressed. Other papers include a case study on large scale formal development and verification, CSP mechanisms for Microsoft's .NET framework, parallel systems on embedded and mobile devices, modern link technology (“SpaceWire”), various applications of occam-π, JCSP and JCSP.net (video processing, robotics, massive multiplayer gaming, material and biological modeling, etc.), visual design languages and tools for CSP and real-time systems, new process oriented programming and design environments, new developments of the Transterpreter, efficient cluster computing and the debugging of message-passing systems. And, still, there is The Fringe programme!

We anticipate that you will have a very fruitful get-together and hope that it will provide you with as much inspiration and motivation as we have always experienced. We trust you will survive the many late nights this conference seems to provoke.

Finally, we thank the Programme Committee for all their diligent and hard work in reviewing the papers and Fiona Dick and Jennifer Willies (Napier University) in making the arrangements for this meeting.

Jon Kerridge (Napier University), Frederick Barnes (University of Kent), Peter Welch (University of Kent)

DS-links were created to provide a low-latency, high performance data link between parallel processors. When the primary processor using them was withdrawn these links largely disappeared from view but were, in fact, still being used (albeit not for parallel computing) in the Space industry. The potential for these links, with their simple implementation, led to their adoption, in modified form, for a growing range of data communication applications. In 2003, the European Space Agency published a definition of DS-links known as SpaceWire. We briefly describe the original DS-links and detail how SpaceWire has kept or modified them to produce a now popular technology with a rapidly increasing number of implementations and wide take-up.

This paper reports on CSP.NET, developed over the last three months at the University of Copenhagen. CSP.NET is an object oriented CSP library designed to ease concurrent and distributed programming in Microsoft.NET 2.0. The library supports both shared memory multiprocessor systems and distributed-memory multi-computers and aims towards making the architecture transparent to the programmer. CSP.NET exploits the power of .NET Remoting to provide the distributed capabilities and like JCSP, CSP.NET relies exclusively on operating system threads. A Name Server and a workerpool are included in the library, both implemented as Windows Services. This paper presents CSP.NET from a users perspective and provides a tutorial along with some implementation details and performance tests.

Java has become a development platform that has migrated from its initial focus for small form devices, to large full scale desktop and server applications and finally back to the small in the form of Java enabled mobile phones. Here we discuss the necessary requirements to convert the existing JCSP framework so that it can be used in these resource constrained systems. We also provide some performance comparisons on various platforms to evaluate this implementation.

The increasing availability of tri-band mobile devices with mobile phone, wi-fi and Bluetooth capability means that the opportunities for increased access by mobile devices to services provided within a smaller locality becomes feasible. This increase in availability might, however, be tempered by users switching off their devices as they are overloaded with a multitude of messages from a variety of sources. A wide range of opportunities can be realised if we can provide a managed environment in which people can access wireless services specific to a particular physical site or location in a ubiquitous manner, independent of the service, and they can also choose from which services they are willing to receive messages. These opportunities range from retail promotions as a person walks down the street, to shopper specific offers as people enter stores that utilise reward card systems, to information about bus arrivals at a bus stop, additional curatorial information within a museum and access to health records within a hospital environment. The CPA paradigm offers a real opportunity to provide such capability with mobile processes, rather than the current approach that, typically, gives users access to web pages.

We present a CSP framework developed for the .NET platform, building upon the ideas developed for the JCSP library. Discussing the development of the core functionality and then onto extra features in .NET that can be taken advantage of, we have created an initial platform that can provide simple development of CSP style process networks. However, we demonstrate that the Microsoft .NET implementation is more resource hungry for multi-threaded applications than other approaches considered in this paper.

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-π parallel processing language provides such a simple yet powerful concurrency model that is based on CSP and the π-calculus. This paper presents pony, the occam-π Network Environment. occam-π 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.

Percolation theory provides models for a wide variety of natural phenomena. One of these phenomena is the dielectric breakdown of composite materials. This paper describes how we implemented the percolation model for dielectric breakdown in a massively parallel processing environment. To achieve this we modified the breadth-first search algorithm such that it works in probabilistic process networks. Formal methods were used to reason about this algorithm. Furthermore, this algorithm provides the basis for a JCSP implementation which models dielectric breakdowns in composite materials. The implementation model shows that it is possible to apply formal methods in probabilistic processing environments.

Modern lifestyle depends on embedded systems. They are everywhere: sometimes they are hidden and at other times they are handled as a fashion accessory. In order to serve us better they have to do more and more tasks at the same time. This calls for sophisticated mechanisms to handle concurrency. In this paper we present CSP (Communicating Sequential Processes) as a method which helps to solve a number of problems of embedded concurrent systems. To be specific, we describe implementations of the commstime benchmark in multithreaded, multiprocessor and architecture fusion systems. An architecture fusion system combines machine and hardware-logic architectures. Our results are twofold. First, architecture fusion systems outperform all the other systems we tested. Second, we implemented all the systems without a change in the design philosophy. The second point is the more important result, because it shows the power of CSP based design methods.

We have developed a simple massively multiplayer online game system as a test bed for evaluating the usefulness and performance of JCSP.net. The system consists of a primary login server, secondary servers managing play on geographically distinct playing fields, and an arbitrary number of players. The basic structure of the game system is fairly simple, and has been verified to be free from deadlock and livelock using CSP and FDR. The JCSP.net implementation is straight-forward and includes over-writing buffers so that disconnected players will not block the servers and other players. Performance tests on local area networks under Windows demonstrate that five secondary servers easily support 1,000 machine-generated players making moves every two to five seconds. The player move end-to-end time was about 65 milliseconds, which is considered fast enough to support fast-action online games. Conversion from Windows to Linux required minimal effort; limited tests confirmed that versions using Linux alone, and Windows and Linux together, were also successful.

This paper introduces SystemCSP – a design methodology based on a visual notation that can be mapped onto CSP expressions. SystemCSP is a graphical design specification language aimed to serve as a basis for the specification of formally verifiable component-based designs of distributed real-time systems. It aims to be a graphical formalism that covers various aspects needed for the design of distributed real-time systems in single framework.

SystemCSP is a graphical modeling language based on both CSP and concepts of component-based software development. The component framework of SystemCSP enables specification of both interaction scenarios and relative execution ordering among components. Specification and implementation of interaction among participating components is formalized via the notion of interaction contract. The used approach enables incremental design of execution diagrams by adding restrictions in different interaction diagrams throughout the process of system design. In this way all different diagrams are related into a single formally verifiable system. The concept of reusable formally verifiable interaction contracts is illustrated by designing set of design patterns for typical fault tolerance interaction scenarios.

TCP is the only widely supported protocol for reliable communication. Therefore, TCP is the obvious choice when developing distributed systems that need to work on a wide range of platforms. Also, for this to work a developer has to use the standard TCP interface provided by a given operating system.

This work explores various ways to use TCP in high performance distributed systems. More precisely, different ways to use the standard Unix TCP API efficiently are explored, but the findings apply to other operating systems as well. The main focus is how various threading models affect TCP input in a process that has to handle both computation and I/O.

The threading models have been evaluated in a cluster of Linux workstations and the results show that a model with one dedicated I/O thread generally is good. It is at most 10% slower than the best model in all tests, while the other models are between 30 to 194% slower in specific tests.

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 Transterpreter to the Cell Broadband Engine. The Transterpreter 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 Transterpreter runtime to the Cell Broadband Engine and explores ways to program it using a concurrent language.

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.

This paperdetailsthe design ofa new concurrentprocess-oriented programming language, Rain. The language borrows heavily from occam-π and C++ to create a new language based on process-oriented programming, marrying channel-based communication, a clear division between statement and expression, and elements of functional programming. An expressive yet simple type system, coupled with templates, underpins the language.

Modern features such as Unicode support and 64-bit integers are included from the outset, and new ideas involving permissions and coding standards are also proposed. The language targets a new virtual machine, which is detailed in a companion paper along with benchmarks of its performance.

A long-runningrecenttrend in computerprogrammingis the growthin popularity of virtual machines. However, few have included good support for concurrency — a natural mechanism in the Rain programming language. This paper details the design and implementation of a secure virtual machine with support for concurrency, which enables portability of concurrent programs.

Possible implementation ideas of many-to-many threading models for the virtual machine kernel are discussed, and initial benchmarks are presented. The results show that while the virtual machine is slow for standard computation, it is much quicker at running communication-heavy concurrent code — within an order of magnitude of the same native code.

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-π 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-π, and demonstrate that this is possible using the Transterpreter, a portable interpreter for occam-π, as our starting point.

Using the extended model for view-centric reasoning, EVCR, we focus on the many possibilities for concurrent processes to be composed. EVCR is an extension of VCR, both models of true concurrency; VCR is an extension of CSP, which is based on an interleaved semantics for modeling concurrency. VCR, like CSP, utilizes traces of instantaneous events, though VCR permits recording parallel events to preserve the perception of simultaneity by the observer(s). But observed simultaneity is a contentious issue, especially for events that are supposed to be instantaneous. EVCR addresses this issue in two ways. First, events are no longer instantaneous; they occur for some duration of time. Second, parallel events need not be an all-or-nothing proposition; it is possible for events to partially overlap in time. Thus, EVCR provides a more realistic and appropriate level of abstraction for reasoning about concurrent processes. With EVCR, we begin to move from observation to the specification of concurrency, and the compositions of concurrent processes. As one example of specification, we introduce a description of I/O-PAR composition that leads to simplified reasoning about composite I/O-PAR processes.

A software design usually manifests a composition of software specifications. It consists of hierarchies of black box and white box specifications which are subject to refinement verification. Refinement verification is a model-checking process that proves the correctness of software specifications using formal methods. Although this is a powerful tool for developing reliable and robust software, the applied mathematics causes a serious gap between academics and software engineers. I-Mathic comprehends a software specification refinement and verification method and a supporting toolset, which aims at eliminating the gap through hiding the applied mathematics by practical modelling concepts. The model-checker FDR is used for refinement verification and detecting deadlocks and livelocks in software specifications. We have improved the method by incorporating CSP programming concepts into the specification language. These concepts make the method suitable for a broader class of safety-critical concurrent systems. The improved I-Mathic is illustrated in this paper.

The occam-π 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.

This article is a follow-up after the paper “From message queue to ready queue”, presented at the ERCIM Workshop last year. A (mostly) synchronous layer had been implemented on top of an existing asynchronous run-time system. After that workshop, we discovered that the initial implementation contained two errors: both concerning malignant process rescheduling associated with timers and “reuse” of the input side of a channel. Also, the set of process/dataflow patterns was not sufficient. To keep complexity low, we have made two new patterns to reflect better the semantic needs inherent in the application. Our assumption of correctness is also, this time, based both on heuristics and “white-board reasoning”. However, both the previous and this paper have been produced before any first shipment of the product, and well within full-scale testing. Our solutions and way of attacking the problems have been in an industrial tradition.

In this paper, we present the results of a significant and large case study in Circus. Development is top-down—from a sequential abstract specification about which safety properties can be verified, to a highly concurrent implementation on a Field Programmable Gate Array. Development steps involve applying laws of Circus allowing for the refinement of specifications; confidence in the correctness of the development is achieved through the applicability of the laws applied; proof obligations are discharged using the model-checker for CSP, FDR, and the theorem prover for Z, Z/Eves. An interesting feature of this case study is that the design of the implementation is guided by domain knowledge of the application—the application of this domain knowledge is supported by, rather than constrained by the calculus. The design is not what would have been expected had the calculus been applied without this domain knowledge. Verification highlights a curious error made in early versions of the implementation that were not detected by testing.

In this paper we investigate two major topics; firstly, througha survey given to graduate students in a parallel message passing programming class, we categorize the errors they made (and the ways they fixed the bugs) into a number of categories. Secondly,we analyze these answers and providesome insight into how software could be built to aid the development, deployment, and debugging of parallel message passing systems. We draw parallels to similar studies done for sequential programming, and finally show how the idea of multilevel debugging relates to the results from the survey.

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 compilationof CSP systems to executablecode. The main motivationfor this work is in providinga means to experimentwith relatively large CSP systems, possibly consisting millions of concurrent processes — something that is hard to achieve with the tools currently available.