Communicating Process Architectures 2006 (CPA 2006)


  Editors: Peter H. Welcha, Jon Kerridgeb, Frederick R. M. Barnesa
      (a) School of Computing, University of Kent, UK
      (b) School of Computing, Edinburgh Napier University, UK
 
  Publisher: IOS Press, Amsterdam, The Netherlands
  ISBN: 978-1586036713

  Held at Edinburg Napier University in Edinburgh, Scotland, September 17 - 20, 2006 (Local chair: Jon Kerridge)
 
 Keynote Presentations
 
 Title: A Fast Resolution of Choice between Multiway Synchronisations
 Authors: Peter H. Welch
School of Computing, University of Kent
 Abstract: Communicating processes offer a natural and scaleable architecture for many computational systems: networks-within-networks, explicit dependencies (through 'visible plumbing', i.e. shared events), and explicit independencies (through 'air gaps', i.e. no shared events). CSP is a process algebra enabling the formal specification of such systems and their refinement to executable implementation. It allows the description of complex patterns of synchronisation between component processes and provides semantics sufficiently powerful to reason about non-determinism, multiway synchronisation, channel communication, deadlock and divergence.

However, programming languages (such as occam-pi) and libraries (JCSP, CTJ, C++CSP, etc.), offering CSP primitives and operators, have always restricted certain combinations from use. The reasons were solely pragmatic: implementation overheads. The main restriction lies in the set of events that a process may offer - and non-deterministically choose between if more that one becomes available. The constraint is that if one process is choosing between event e and some other events, other processes offering e must do so only in a committed way - i.e. not as part of a choice of their own. The choice can then be resolved with a simple handshake. Hence, only the process on the input side of a channel may offer it within a choice construct (ALT) - an outputting process always commits. Similarly, choice between multiway synchronisations is banned; since symmetry allows no one process the privilege.

This is unfortunate since free-wheeling choices between all kinds of event are routinely specified by CSP designers and they must be transformed into systems that meet the constraints. Because any process making such a choice withdraws all bar one of its offers to synchronise as it makes that choice, resolution is usually managed through a 2-phase commit protocol. This introduces extra channels, processes and serious run-time overheads. Without automated tools, that transformation is error prone. The resulting system is expressed at a lower level that is hard to maintain. Maintenance, therefore, takes place at the higher level and the transformations have continually to be re-applied.

This talk presents a fast resolution of choice between multiway synchronisation (the most general form of CSP event). It does not involve 2-phase commit logic and its cost is linear in the number of choice events offered by the participants. A formal proof of its correctness (that the resolution is a traces-failures-divergences refinement of the specified CSP) has not been completed, but we are feeling confident. Preliminary bindings of this capability have been built into the JCSP library (version 1.0 rc6) and an experimental (read complete re-write) occam-pi compiler. This will remove almost all of the constraints in the direct and efficient realisation of CSP designs as executable code. An example of its use in a (very) simple model of blood clotting (from our TUNA project) will be presented.
 Bibliography:   [BibTeX]
 Abstract: [PDF] 
 Presentation:
 
 
 Papers
 
 Title: SpaceWire - DS-Links Reborn
 Authors: Barry Cook, Paul Walker
4Links Ltd.
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: An Introduction to CSP.NET
 Authors: Alex A. Lehmberg, Martin N. Olsen
Department of Computer Science, University of Copenhagen
 Abstract: 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 multicomputers 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: Performance Evaluation of JCSP Micro Edition: JCSPme
 Authors: Kevin Chalmers, Jon Kerridge, Imed Romdhani
School of Computing, Edinburgh Napier University
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: Ubiquitous Access to Site Specific Services by Mobile Devices: the Process View
 Authors: Jon Kerridge, Kevin Chalmers
School of Computing, Edinburgh Napier University
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: CSP for .NET Based on JCSP
 Authors: Sarah Clayton
School of Computing, Edinburgh Napier University
 Abstract: 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 multicomputers 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: pony - The occam-pi Network Environment
 Authors: Mario Schweigler, Adam T. Sampson
Computing Laboratory, University of Kent
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: A Study of Percolation Phenomena in Process Networks
 Authors: Oliver Faust, Bernhard H. C. Sputh, Alastair Allen
Department of Engineering, University of Aberdeen
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: Portable CSP Based Design for Embedded Multi-Core Systems
 Authors: Bernhard H. C. Sputh, Oliver Faust, Alastair Allen
Department of Engineering, University of Aberdeen
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: A JCSP.net Implementation of a Massively Multiplayer Online Game
 Authors: Shyam Kumara, Gardiner S. Stilesb
(a) Electrical and Computer Engineering Department, Utah State University
(b) Electrical and Computer Engineering, Utah State University
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: SystemCSP - Visual Notation
 Authors: Bojan Orlica, Jan F. Broeninkb
(a) Control Engineering, Faculty of EE-Math-CS, University of Twente
(b) Robotics and Mechatronics, CTIT Institute, University of Twente
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: Interacting Components
 Authors: Bojan Orlica, Alastair Allenb
(a) Control Engineering, Faculty of EE-Math-CS, University of Twente
(b) Department of Engineering, University of Aberdeen
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: TCP Input Threading in High Performance Distributed Systems
 Authors: Hans H. Happe
Department of Mathematics and Computer Science, University of Southern Denmark
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: A Cell Transterpreter
 Authors: Damian J. Dimmich, Christian L. Jacobsen, Matthew C. Jadud
Computing Laboratory, University of Kent
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: Mobile Robot Control: The Subsumption Architecture and occam-pi
 Authors: Jonathan L. Simpson, Christian L. Jacobsen, Matthew C. Jadud
Computing Laboratory, University of Kent
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: Rain: A New Concurrent Process-Oriented Programming Language
 Authors: Neil C. C. Brown
Computing Laboratory, University of Kent
 Abstract: This paper details the design of a new concurrent process-oriented programming language, Rain. The language borrows heavily from occam-p 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: Rain VM: Portable Concurrency through Managing Code
 Authors: Neil C. C. Brown
Computing Laboratory, University of Kent
 Abstract: A long-running recent trend in computer programming is the growth in 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: Native Code Generation using the Transterpreter
 Authors: Christian L. Jacobsen, Damian J. Dimmich, Matthew C. Jadud
Computing Laboratory, University of Kent
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: Compositions of Concurrent Processes
 Authors: Mark Burgina, Kevin Chalmersb
(a) Department of Computer Science, University of California, Los Angeles
(b) School of Computing, Edinburgh Napier University
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: Software Specification Refinement and Verification Method with I-Mathic Studio
 Authors: Gerald H. Hilderink
Imtech ICT Technical Systems
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: Video Processing in occam-pi.
 Authors: Carl G. Ritson, Adam T. Sampson, Frederick R. M. Barnes
Computing Laboratory, University of Kent
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: No Blocking on Yesterday's Embedded CSP Implementation (the Rubber Band of Getting it Right and Simple)
 Authors: Øyvind Teig
Autronica Fire and Security AS
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: A Circus Development and Verification of an Internet Packet Filter
 Authors: Alistair A. McEwan
Department of Computer Science, University of Surrey
 Abstract: 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: Classification of Programming Errors in Parallel Message Passing Systems
 Authors: Jan Bækgaard Pedersen
School of Computer Science, University of Nevada Las Vegas
 Abstract: In this paper we investigate two major topics; firstly, through a 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 provide some 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.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation:
 
 Title: Compiling CSP
 Authors: Frederick R. M. Barnes
Computing Laboratory, University of Kent
 Abstract: 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. Themain motivation for this work is in providing a means to experimentwith relatively large CSP systems, possibly consisting millions of concurrent processes - something that is hard to achieve with the tools currently available.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation: