Ebook: Communicating Process Architectures 2008

The thirty-first Communicating Process Architectures Conference, CPA 2008, organised under the auspices of WoTUG and the Department of Computer Science of the University of York, is being held in York, UK, 7–10 September 2008.

The York Department of Computer Science is delighted to host this conference again. The thirteenth Occam User Group Technical Meeting (from which these CPA conferences are descended) on “Real-Time Systems with Transputers” was held at this University in September, 1990. York has a long history of close contacts with this conference, from the early heady days when occam was new, to current collaborations with the University of Kent using occam-π for simulating complex systems. The satellite workshop “Complex Systems Modelling and Simulation (CoSMoS)”, arising from this collaboration, is part of this year's conference.

The city of York, one of Europe's most beautiful cities, combines evidence of a history going back to Roman times with a bustling modern city centre. York Minster, built on the foundations of the Roman city and an earlier Norman cathedral, is among the finest Gothic cathedrals, and dominates the city. Romans, Vikings, and more recent history are commemorated in a number of top-class museums, as well as being apparent in the architecture of the city.

We are delighted to have two excellent invited speakers, covering both theoretical aspects and industrial applications of Communicating Processes. Professor Samson Abramsky, FRS, is the Christopher Strachey Professor of Computing at the University of Oxford, where he leads the Theory and Automated Verification group. He 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 is the head of the Systems Assurance Group at QinetiQ. He 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.

This conference and workshop were partially supported by AWE, EPSRC, Microsoft Research, and WoTUG. The editors would like to thank all the paper reviewers for the detailed feedback they provided the authors, the authors for their diligence in responding well to (sometimes harsh) criticism, the staff at the University of York – especially Bob French and Jenny Baldry – for the website and local arrangements – and, finally, to those individuals at the Universities of Kent and Tromsø – especially Carl Ritson, Neil Brown, John Markus Bjørndalen and Jon Simpson – without whom these Proceedings would not have made their press deadline!

Peter Welch (University of Kent),

Susan Stepney (University of York),

Fiona Polack (University of York),

Frederick Barnes (University of Kent),

Alistair McEwan (University of Leicester),

Dyke Stiles (Utah State University),

Jan Broenink (University of Twente),

Adam Sampson (University of Kent).

We shall develop a simple and natural formalization of the idea of client-server architectures, and, based on this, define a notion of orthogonality between clients and servers, which embodies strong correctness properties, and exposes the rich logical structure inherent in such systems. Then we generalize from pure clients and servers to components, which provide some services to the environment, and require others from it. We identify the key notion of composition of such components, in which some of the services required by one component are supplied by another. This allows complex systems to be built from ultimately simple components. We show that this has the logical form of the Cut rule, a fundamental principle of logic, and that it can be enriched with a suitable notion of behavioural types based on orthogonality, in such a way that correctness properties are preserved by composition. We also develop the basic ideas of how logical constructions can be used to develop structured interfaces for systems, with operations corresponding to logical rules. Finally, we show how the setting can be enhanced, and made more robust and expressive, by using names (as in the π-calculus) to allow clients to bind dynamically to generic instances of services.

In this talk, I shall discuss work on the necessary technology required for flight clearance of Autonomous Aircraft employing Agents by reducing the certification problem to small verifiable steps that can be carried out by a machine. The certification of such Agents falls into two parts: the validation of the safety of the Agent; and the verification of the implementation of the agent. The work focuses on the Soar agent language and the main results are:

• language subset for Soar, designed for formal analysis;

• a formal model of the Soar subset written in CSP;

• a prototype translator “Soar2Csp” from Soar to the CSP model;

• a framework for static analysis of Soar agents through model checking using FDR2;

• the identification of “healthiness conditions” required of any Soar Agent;

• a verifiable implementation of the CSP based Soar agents on an FPGA.

CSP processes have a static view of their environment – a fixed set of events through which they synchronise with each other. In contrast, the π-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-π multiprocessing language is built upon classical occam, whose design and semantics are founded on CSP. To address the dynamics of complex systems, occam-π 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-π systems using mobile channels and formal specification of implementation mechanisms for mobiles used by the occam-π compiler and run-time kernel.

In this paper we introduce the core features of CSO (Communicating Scala Objects) – a notationally convenient embedding of the essence of occam in a modern, generically typed, object-oriented programming language that is compiled to Java Virtual Machine (JVM) code. Initially inspired by an early release of JCSP, CSO goes eyond JCSP expressively in some respects, including the provision of a unitary extended rendezvous notation and appropriate treatment of subtype variance in channels and ports. Similarities with recent versions of JCSP include the treatment of channel ends (we call them ports) as parameterized types. Ports and channels may be transmitted on channels (including inter-JVM channels), provided that an obvious design rule – the ownership rule – is obeyed. Significant differences with recent versions of JCSP include a treatment of network termination that is significantly simpler than the “poisoning” approach (perhaps at the cost of reduced programming convenience), and the provision of a family of type-parameterized channel implementations with performance that obviates the need for the special-purpose scalar-typed channel implementations provided by JCSP. On standard benchmarks such as Commstime, CSO communication performance is close to or better than that of JCSP and Scala's Actors library.

A special feature of the occam programming language is that its concurrency support is at the very base of the language. However, its ability to specify scheduling requirements is insufficient for use in some real-time systems. Toc is an experimental programming language that builds on occam, keeping occam's concurrency mechanisms, while fundamentally changing its concept of time. In Toc, deadlines are specified directly in code, replacing occam's priority constructs as the method for controlling scheduling. Processes are scheduled lazily, in that code is not executed without an associated deadline. The deadlines propagate through channel communications, which means that a task blocked by a channel that is not ready will transfer its deadline through the channel to the dependent task. This allows the deadlines of dependent tasks to be inferred, and also creates a scheduling effect similar to priority inheritance. A compiler and run-time system has been implemented to demonstrate these principles.

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.

In the occam-π 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-π compiler using Honda's session types. These mechanisms would considerably simplify the implementation of complex, dynamic client-server systems.

Concurrent/reactive systems can be designed free of deadlock using prioritized service architecture (PSA), subject to simple, statically verified, design rules. The Honeysuckle Design Language (HDL) enables such service-oriented design to be expressed purely in terms of communication, while affording a process-oriented implementation, using the Honeysuckle Programming Language (HPL). A number of enhancements to the service model for system abstraction are described, along with their utility. Finally, a new graphical counterpart to HDL (HVDL) is introduced that incorporates all these enhancements, and which facilitates interactive stepwise refinement.

This paper considers the issues involved in translating specifications described in the CSP∥B formal method into Handel-C. There have previously been approaches to translating CSP descriptions to Handel-C, and the work presented in this paper is part of a programme of work to extend it to include the B component of a CSP∥B description. Handel-C is a suitable target language because of its capability of programming communication and state, and its compilation route to hardware. The paper presents two case studies that investigate aspects of the translation: a buffer case study, and an abstract arbiter case study. These investigations have exposed a number of issues relating to the translation of the B component, and have identified a range of options available, informing more recent work on the development of a style for CSP∥B specifications particularly appropriate to translation to Handel-C.

Most motion control systems for mechatronic systems are implemented on digital computers. In this paper we present an FPGA based solution implemented on a low cost Xilinx Spartan III FPGA. A Production Cell setup with multiple parallel operating units is chosen as a test case. The embedded control software for this system is designed in gCSP using a reusable layered CSP based software structure. gCSP is extended with automatic Handel-C code generation for configuring the FPGA. Many motion control systems use floating point calculations for the loop controllers. Low cost general purpose FPGAs do not implement hardware-based floating point units. The loop controllers for this system are converted from floating point to integer based calculations using a stepwise refinement approach. The result is a complete FPGA based motion control system with better performance figures than previous CPU based implementations.

The co-operative design methodology has significant advantages when used in safety-related systems. Coupled with the time-triggered architecture, the methodology can result in robust and predictable systems. Nevertheless, use of a co-operative design methodology may not always be appropriate especially when the system possesses tight resource and cost constraints. Under relaxed constraints, it might be possible to maintain a co-operative design by introducing additional software processing cores to the same chip. The resultant multi-core microcontroller then requires suitable design methodologies to ensure that the advantages of time-triggered co-operative design are maintained as far as possible. This paper explores the application of a time-triggered distributed-systems protocol, called “shared-clock”, on an eight-core microcontroller. The cores are connected in a mesh topology with no hardware broadcast capabilities and three implementations of the shared-clock protocol are examined. The custom multi-core system and the network interfaces used for the study are also described. The network interfaces share higher level serialising logic amongst channels, resulting in low hardware overhead when increasing the number of channels.

The refinement of a theoretical model which includes external choice over output and input of a channel transaction into an implementation model is a long-standing problem. In the theory of communicating sequential processes this type of external choice translates to resolving input and output guards. The problem arises from the fact that most implementation models incorporate only input guard resolution, known as alternation choice. In this paper we present the transaction request broker process which allows the designer to achieve external choice over channel ends by using only alternation. The resolution of input and output guards is refined into the resolution of input guards only. To support this statement we created two models. The first model requires resolving input and output guards to achieve the desired functionality. The second model incorporates the transaction request broker to achieve the same functionality by resolving only input guards. We use automated model checking to prove that both models are trace equivalent. The transfer request broker is a single entity which resolves the communication between multiple transmitter and receiver processes.

We prove the correctness of a two-way sliding window protocol with piggybacking, where the acknowledgements of the latest received data are attached to the next data transmitted back into the channel. The window sizes of both parties are considered to be finite, though they can be different. We show that this protocol is equivalent (branching bisimilar) to a pair of FIFO queues of finite capacities. The protocol is first modeled and manually proved for its correctness in the process algebraic language of μCRL. We use the theorem prover PVS to formalize and mechanically prove the correctness of the protocol. This implies both safety and liveness (under the assumption of fairness).

This paper establishes the security, stability and functionality of the reset-table receiver alternating bit protocol. This protocol creates a reliable and blocking channel between sender and receiver over unreliable non-blocking communication channels. Furthermore, this protocol permits the sender to be replaced at any time, but not under all conditions without losing a message. The protocol is an extension to the alternating bit protocol with the ability for the sender to synchronise the receiver and restart the transmission. The resulting protocol uses as few messages as possible to fulfil its duty, which makes its implementation lightweight and suitable for embedded systems. An unexpected outcome of this work is the large number of different messages needed to reset the receiver reliably.

IC2IC links introduce blocking functionality to a low latency high performance data link between independent processors. The blocking functionality was achieved with the so-called alternating bit protocol. Furthermore, the protocol hardens the link against message loss and message duplication. The result is a reliable way to transfer bit level information from one IC to another IC. This paper provides a detailed discussion of the link signals and the protocol layer. The practical part shows an example implementation of the IC2IC serial link. This example implementation establishes an IC2IC link between two configurable hardware devices. Each device incorporates a process network which implements the IC2IC transceiver functionality. This example implementation helped us to explore the practical properties of the IC2IC serial interconnect. First, we verified the blocking capability of the link and second we analysed different reset conditions, such as disconnect and bit-error.

Object Oriented languages have increased in popularity over the last two decades. The OO paradigm claims to model the way objects interact in the real world. All objects in the OO model are passive and all methods are executed synchronously in the thread of the caller. Active objects execute their methods in their own threads. The active object queues method invocations and executes them one at a time. Method invocations do not overlap, thus the object cannot be put into or seen to be in an inconsistent state. We propose an active object system implemented by extending the Java language with four new keywords: active, async, on and waitfor. We have modified Sun's open-source compiler to accept the new keywords and to translate them to regular Java code during desugaring phase. We achieve this through the use of RMI, which as a side effect, allows us to utilise a cluster of work stations to perform distributed computing.

JCSPre is a highly reduced version of the JCSP (Communicating Sequential Processes for Java) parallel programming environment. JCSPre has been implemented on a LEGO Mindstorms NXT brick using the LeJOS Java runtime environment. The LeJOS environment provides an abstraction for the NXT Robot in terms of Sensors, Sensor Ports and Motors, amongst others. In the implementation described these abstractions have been converted into the equivalent active component that is much easier to incorporate into a parallel robot controller. Their use in a simple line following robot is described, thereby demonstrating the ease with which robot controllers can be built using parallel programming principles. As a further demonstration we show how the line following robot controls a slave robot by means of Bluetooth communications.

We present a critical investigation of the current implementation of JCSP Networking, examining in detail the structure and behavior of the current architecture. Information is presented detailing the current architecture and how it operates, and weaknesses in the implementation are raised, particularly when considering resource constrained devices. Experimental work is presented that illustrate memory and computational demand problems and an outline on how to overcome these weaknesses in a new implementation is described. The new implementation is designed to be lighter weight and thus provide a framework more suited for resource constrained devices which are a necessity in the field of ubiquitous computing.

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-π 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-π applications, based on the Transterpreter virtual machine interpreter. By adding a set of extensions to the Transterpreter, we give occam-π 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-π by mediating the execution of one execution process from another.

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-π on top of an asynchronous messaging framework. We show how to make use of collective operations in distributed process-oriented applications. We also show how the process-oriented model can be used to increase concurrency in existing collective operation algorithms.

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.

This paper introduces a framework for building CSP based applications, targeted for clusters and next generation CPU designs. CPUs are produced with several cores today and every future CPU generation will feature increasingly more cores, resulting in a requirement for concurrency that has not previously been called for. The framework is CSP presented as a scientific workflow model, specialized for scientific computing applications. The purpose of the framework is to enable scientists to exploit large parallel computation resources, which has previously been hard due of the difficulty of concurrent programming using threads and locks.

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.

The Santa Claus problem provides an excellent exercise in concurrent programming and can be used to show the simplicity or complexity of solving problems using a particular set of concurrency mechanisms and offers a comparison of these mechanisms. Shared-memory constructs, message passing constructs, and process oriented constructs will be used in various programming languages to solve the Santa Claus Problem. Various concurrency mechanisms available will be examined and analyzed as to their respective strengths and weaknesses.