Communicating Process Architectures 2012 (CPA 2012)


  Editors: Peter H. Welcha, Frederick R. M. Barnesa, Kevin Chalmersb, Jan Bækgaard Pedersenc, Adam T. Sampsond
      (a) School of Computing, University of Kent, UK
      (b) School of Computing, Edinburgh Napier University, UK
      (c) Department of Computer Science, University of Nevada Las Vegas, USA
      (d) School of Arts, Media and Computer Games, Abertay University, UK
 
  Publisher: Open Channel Publishing Ltd., Bicester, UK
  ISBN: 978-0956540959

  Held at University of Abertay Dundee in Dundee, Scotland, August 26 - 29, 2012 (Local chair: Adam T. Sampson)
 
  Conference Program
 
 Papers
 
 Title: Designing a Concurrent File Server
 Authors: James WhiteHead II
Department of Computer Science, University of Oxford
 Abstract: In this paper we present a design and architecture for a concurrent file system server. This architecture is a compromise between the fully concurrent V6 UNIX implementation, and the simple sequential implementation in the MINIX operating system. The design of the server is made easier through the use of a disciplined model of concurrency, based on the CSP process algebra. By viewing the problem through this restricted lens, without traditional explicit locking mechanisms, we can construct the system as a process network of components with explicit connections and dependencies. This provides us with insight into the problem domain, and allows us to analyse the issues present in concurrent file system implementation.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation: [PDF] 
 
 Title: JCircus 2.0: an Extension of an Automatic Translator from Circus to Java
 Authors: S. L. M. Barrocas, Marcel V. M. Oliveira
Universidade Federal do Rio Grande do Norte
 Abstract: The use of formal methods in the development of concurrent systems considerably reduces the complexity of specifying their behaviour and verifying properties that are inherent to them. Development, however, targets the generation of executable programs; hence, translating the final specification into a practical programming language becomes imperative. This translation is usually rather problematic due to the high probability of introducing errors in manual translations: the mapping from some of the original concepts in the formal concurrency model into a corresponding construct in the programming language is non-trivial. In recent years, there is a growing effort in providing automatic translation from formal specifications into programming languages. One of these efforts, JCircus, translates specifications written in Circus (a combination of Z and CSP) into Java programs that use JCSP, a library that implements most of the CSP constructs. The subtle differences between JCSP and Circus implementation of concurrency, however, imposed restrictions to the translation strategy and, consequently, to JCircus. In this paper, we extend JCircus by providing: (1) a new optimised translation strategy to multi-way synchronisation; (2) the translation of complex communications, and; (3) the translation of CSP sharing parallel and interleaving. A performance analysis of the resulting code is also in the context of this paper and provides important insights into the practical use of our results.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation: [PDF] 
 
 Title: A Distributed Multi-Agent Control System for Power Consumption in Buildings
 Authors: Anna Magdalena Kosek, Oliver Gehrke
Department of Electrical Engineering, Technical University of Denmark
 Abstract: This paper presents a distributed controller for adjusting the electrical consumption of a residential building in response to an external power setpoint in Watts. The controller is based on a multi-agent system and has been implemented in JCSP. It is modularly built, capable of self-configuration and adapting to a dynamic environment. The paper describes the overall architecture and the design of the individual agents. Preliminary results from proof-of-concept tests on a real building are included.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation: [PDF] 
 
 Title: Specification of APERTIF Polyphase Filter Bank in CλaSH
 Authors: Rinse Westera, Dimitrios Sarakiotisa, Eric Kooistraa, Jan Kuperb
(a) Department of Computer Science, University of Twente
(b) ASTRON
 Abstract: CλaSH, a functional hardware description language based on Haskell, has several abstraction mechanisms that allow a hardware designer to describe architectures in a short and concise way. In this paper we evaluate CλaSH on a complex DSP application, a Polyphase Filter Bank as it is used in the ASTRON APERTIF project. The Polyphase Filter Bank is implemented in two steps: first in Haskell as being close to a standard mathematical specification, then in CλaSH which is derived from the Haskell formulation by applying only minor changes. We show that the CλaSH formulation can be directly mapped to hardware, thus exploiting the parallelism and concurrency that is present in the original mathematical specification.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation: [PDF] 
 
 Title: Schedulability Analysis of Timed CSP Models Using the PAT Model Checker
 Authors: Oguzcan Oguza, Jan F. Broeninka, Angelika Maderb
(a) Robotics and Mechatronics, CTIT Institute, University of Twente
(b) Research Group Human Media Interaction (HMI), University of Twente
 Abstract: Timed CSP can be used to model and analyse real-time and concurrent behaviour of embedded control systems. Practical CSP implementations combine the CSP model of a real-time control system with prioritized scheduling to achieve efficient and orderly use of limited resources. Schedulability analysis of a timed CSP model of a system with respect to a scheduling scheme and a particular execution platform is important to ensure that the system design satisfies its timing requirements. In this paper, we propose a framework to analyse schedulability of CSP-based designs for non-preemptive fixed-priority multiprocessor scheduling. The framework is based on the PAT model checker and the analysis is done with dense-time model checking on timed CSP models. We also provide a schedulability analysis workflow to construct and analyse, using the proposed framework, a timed CSP model with scheduling from an initial untimed CSP model without scheduling. We demonstrate our schedulability analysis workflow on a case study of control software design for a mobile robot. The proposed approach provides non-pessimistic schedulability results.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation: [PDF] 
 
 Title: Supporting Timed CSP Operators in CSP++
 Authors: William B. Gardner, Yuriy Solovyov
School of Computer Science, University of Guelph
 Abstract: CSP++ is an open-source code synthesis tool consisting of a translator for a subset of CSPm and a C++ run-time framework. Version 5.0 now supports Timed CSP operators--timed interrupt, timed timeout, and timed prefix--as well as untimed variants of interrupt and timeout, with only 1% additional execution and memory overhead, though using interrupts is more costly. We describe the implementation and performance of the new operators, illustrating their use with a robot-vacuum cleaner case study. The tool thus becomes more useful for specifying the behaviour of soft real-time systems, and generating a timing-enabled executable program from its formal model.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation: [PDF] 
 
 Title: A Comparison of Message Passing Interface and Communicating Process Architecture Networking Communication Performance
 Authors: Kevin Chalmers
School of Computing, Edinburgh Napier University
 Abstract: Message Passing Interface (MPI) is a popular approach to enable Single Process, Multiple Data (SPMD) style parallel computing, particularly in cluster computing environments. Communicating Process Architecture (CPA) Networking on the other hand, has been developed to enable channel based semantics across a communication mechanism in a transparent manner. However, in both cases the concept of a message passing infrastructure is fundamental. This paper compares the performance of both of these frameworks at a base communication level, also discussing some of the similarities between the two mechanisms. From the experiments, it can be seen that although MPI is a more mature technology, in many regards CPA Networking can perform comparably if the correct communication is used.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation: [PDF] 
 
 Title: Beauty And The Beast: Exploiting GPUs In Haskell
 Authors: Alex Colea, Alistair A. McEwana, Geoff Mainlandb
(a) Department of Engineering, University of Leicester
(b) Microsoft Research
 Abstract: In this paper we compare a Haskell system that exploits a GPU back end using Obsidian against a number of other GPU/parallel processing systems. Our examples demonstrate two major results. Firstly they show that the Haskell system allows the applications programmer to exploit GPUs in a manner that eases the development of parallel code by abstracting from the hardware. Secondly we show that the performance results from generating the GPU code from Haskell are acceptably comparable to expert hand written GPU code in most cases; and permit very significant performance benefits over single and multi-threaded implementations whilst maintaining ease of development. Where our results differ from expert hand written GPU (CUDA) code we consider the reasons for this and discuss possible developments that may mitigate these differences. We conclude with a discussion of a domain specific example that benefits directly and significantly from these results.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation: [PDF] 
 
 Title: A Debugger for Communicating Scala Objects
 Authors: Andrew Bate, Gavin Lowe
Department of Computer Science, University of Oxford
 Abstract: This paper presents a software tool for visualising and reasoning about the behaviour of message-passing concurrent programs built with the CSO library for the Scala programming language. It describes the models needed to represent the construction of process networks and the runtime behaviour of the resulting program. We detail the manner in which information is extracted from the use of concurrency primitives in order to maintain these models and how these models are diagrammed. Our implementation of dynamic deadlock detection is explained. The tool can produce a sequence diagram of process communications, the communication network depicting the pairs of processes which share a communication channel, and the trees resulting from the composition of processes. Furthermore, it allows for behavioural specifications to be defined and then checked at runtime, and guarantees to detect the illegal usage of concurrency primitives that could otherwise lead to deadlock or data loss. Our implementation imposes only a small overhead on the program under inspection.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation: [PDF] 
 
 Title: XCHANs: Notes on a New Channel Type
 Authors: Øyvind Teig
Autronica Fire and Security AS
 Abstract: Single Event Upsets (SEU) are a primary reliability concern for electronics in high radiation, highly hostile environments such as space. In the case of Field Programmable Gate Arrays, the concern is firstly that data stored in RAM can be corrupted, and secondly that configurable logic blocks can become damaged or corrupted. In this talk we will present our considerations of this problem in the context of an SRAM-based high reliability flash file system. We will firstly demonstrate our test harness where we simulate the injection of SEUs into our FPGA. We will then discuss how we propose to build a self repairing configuration using triple modular redundancy and partial dynamic reconfiguration. Finally we will discuss how the reliability of the system may be tested and measured such that it can be used with confidence in either data acquisition or control system applications in rad-hard environments.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation: [PDF] 
 
 Title: A High Performance Reconfigurable Architecture for Flash File Systems
 Authors: Irfan Mir, Alistair A. McEwan, Neil J. Perrins
Department of Engineering, University of Leicester
 Abstract: NAND flash memory is widely adopted as the primary storage medium in embedded systems. The design of the flash translation layer, and exploitation of parallel I/O architectures, are crucial in achieving high performance within a flash file system. In this paper we present our new FPGA based flash management framework using reconfigurable computing that supports high performance flash storage systems. Our implementation is in Verilog, and as such enables us to design a highly concurrent system at a hardware level in both the flash translation layer and the flash controller. Results demonstrate that implementing the flash translation layer and flash controller directly in hardware, by exploiting reconfigurable computing, permits us to exploit a highly concurrent architecture that leads to fast response times and throughput in terms of read/write operations.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation: [PDF] 
 
 Title: Design and Use of CSP Meta-Model for Embedded Control Software Development
 Authors: Maarten M. Bezemer, Robert J. W. Wilterdink, Jan F. Broenink
Robotics and Mechatronics, CTIT Institute, University of Twente
 Abstract: Software that is used to control machines and robots must be predictable and reliable. Model-Driven Design (MDD) techniques are used to comply with both the technical and business needs. This paper introduces a CSP meta-model that is suitable for these MDD techniques. The meta-model describes the structure of CSP models that are designed; using this meta-model it is possible to use all regular CSP constructs when constructing a CSP model. The paper also presents a new tool suite, called TERRA, based on Eclipse and its frameworks. TERRA contains a graphical CSP model editor (using the new CSP meta-model), model validation tools and code generation tools. The model validation tools check whether the model conforms to the meta-model definition as well as to additional rules. Models without any validation problems result in proper code generation, otherwise the developer needs to address the found problems to be sure code generation will succeed. The code generation tools are able to generate CSPm code that is readable by FDR and to generate C++/LUNA code that is executable on embedded targets. The meta-model and the TERRA tool suite are tested by designing CSP models for several of our laboratory setups. The generated C++/LUNA code for the laboratory setups is able to control them as expected. Additionally, the paper contains an example model containing all supported CSP constructs to show the CSPm code generation results. So it can be concluded that the meta-model and TERRA are usable for these kind of tasks.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation: [PDF] 
 
 Title: Exception Handling and Checkpointing in CSP
 Authors: Mads Ohm Larsena, Brian Vinterb
(a) Department of Computer Science, University of Copenhagen
(b) Niels Bohr Institute, University of Copenhagen
 Abstract: This paper describes work in progress. It presents a new way of looking at some of the basics of CSP. The primary contributions is exception handling and checkpointing of processes and the ability to roll back to a known checkpoint. Channels are discussed as communication events which is monitored by a supervisor process. The supervisor process is also used to formalise poison and retire events. Exception handling and checkpointing are used as means of recovering from an catastrophe. The supervisor process is central to checkpointing and recovery as well. Three different kind of exception handling is discussed: fail-stop, retire-like fail-stop, and check pointing. Fail-stop works like poison, and retire-like fail-stop works like retire. Checkpointing works by telling the supervisor process to roll back both participants in a communication event, to a state immediately after their last successful communication. Only fail-stop exceptions have been implemented in PyCSP to this point.
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation: [PDF] 
 
 Title: occam Obviously
 Authors: Peter H. Welch
School of Computing, University of Kent
 Abstract: This talk explains and tries to justify a range of questions for which its title is the answer. It reviews the history of occam: its underlying philosophy (Occam's Razor), its semantic foundation on Hoare's CSP, its principles of process oriented design and its development over almost three decades into occam-pi (which blends in the concurrency dynamics of Milner's pi-calculus). Also presented will be its urgent need for rationalisation -- occam-pi 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, how do we avoid the following question being final: which language had the most theoretically sound semantics, the most efficiently engineered implementation, the simplest and most pragmatic concurrency model for building complex systems ... and was mostly forgotten (even as its ideas are slowly and expensively and painfully being reinvented piece-by-piece, as they must be)?
 Bibliography:   [BibTeX]
 Paper: [PDF] 
 Presentation: [Power Point]  [PDF] 
 
 
 Fringe Presentations
 
 Title: Cancellable Servers - a Pattern for Curiousity
 Authors: Peter H. Welch
School of Computing, University of Kent
 Abstract:
 Bibliography:   [BibTeX]
 Abstract:
 Presentation: [Power Point]  [PDF] 
 
 Title: A CPA Series
 Authors: Ian East
Open Channel Publishing Ltd.
 Abstract:
 Bibliography:   [BibTeX]
 Abstract:
 Presentation:
 
 Title: Polyphonic Processors - Fantasy on an FPGA
 Authors: Richard Miller
Miller Research, Oxford, England, Miller Research
 Abstract:
 Bibliography:   [BibTeX]
 Abstract:
 Presentation:
 
 Title: Developing JIWY using TERRA
 Authors: Maarten M. Bezemer, Robert J. W. Wilterdink, Jan F. Broenink
Robotics and Mechatronics, CTIT Institute, University of Twente
 Abstract:
 Bibliography:   [BibTeX]
 Abstract:
 Presentation: [PDF] 
 
 Title: JCircus Demo
 Authors: S. L. M. Barrocas, Marcel V. M. Oliveira
Universidade Federal do Rio Grande do Norte
 Abstract:
 Bibliography:   [BibTeX]
 Abstract:
 Presentation:
 
 Title: Unfinished Business - occam-pi²
 Authors: Peter H. Welch
School of Computing, University of Kent
 Abstract:
 Bibliography:   [BibTeX]
 Abstract:
 Presentation:
 
 Title: Implementation of an Agent-based Model with TBB Technique
 Authors: Ye Li
Institute of Arts, Media and Computer Games, University of Abertay
 Abstract:
 Bibliography:   [BibTeX]
 Abstract:
 Presentation: [PDF] 
 
 Title: Handel-C++ - Adding Syntactic Support to C++ 
 Authors: Alex Cole
Department of Engineering, University of Leicester
 Abstract:
 Bibliography:   [BibTeX]
 Abstract:
 Presentation: [PDF] 
 
 Title: Process-Oriented Building Blocks
 Authors: Adam T. Sampson
School of Arts, Media and Computer Games, Abertay University
 Abstract: Intel's Threading Building Blocks library provides an efficient, work-stealing lightweight task scheduler, along with a high-level task-based API for parallel programming in C++. This presentation shows how TBB's scheduler can be used (without modification) to implement blocking process-oriented concurrent systems, and discusses the advantages and disadvantages of this approach.
 Bibliography:   [BibTeX]
 Abstract: [PDF] 
 Presentation: [PDF] 
 
 Title: Data Escape Analysis for Process Oriented Systems
 Authors: Martin Ellis, Frederick R. M. Barnes
School of Computing, University of Kent
 Abstract: Escape analysis, the technique of discovering the boundaries of dynamically allocated objects, is a well explored technique for object-orientated languages (such as Java and C++) and stems from the functional programming community. It provides an insight into which objects interact directly (and indirectly) and can inform program correctness checking, or be used for directing optimisations (e.g. determining which objects can safely be allocated on a function-local stack). For process-oriented languages such as occam-pi and Google's Go, we have explored mobile escape analysis, that provides concise information about the movement of objects (mobiles) within networks of communicating processes. Because of the distinction between processes (as execution contexts) and objects (dynamically allocated data, channels and processes), combined with strict typing and aliasing rules, the analysis is somewhat simpler then for less strict languages. This analysis is only concerned with dynamically allocated blocks of memory -- it does not give any consideration for the data contained within these. However, knowing the extent to which data (statically or dynamically allocated) escapes within a network of communicating processes is arguably useful -- and is not necessarily a superset of mobile escape. The fringe presentation describes an extension to the mobile escape model that seeks to capture semantic information about the data escape of a process-oriented system. This provides richer semantic information about a process's behaviour (that can be used in verification) and has clear application to security (e.g. by demonstrating that particular data does not escape a set of communicating processes).
 Bibliography:   [BibTeX]
 Abstract: [PDF] 
 Presentation: [PDF] 
 
 Title: SEU Protection for High-Reliability Flash File Systems
 Authors: Neil J. Perrins, Alistair A. McEwan
Department of Engineering, University of Leicester
 Abstract: Single Event Upsets (SEU) are a primary reliability concern for electronics in high radiation, highly hostile environments such as space. In the case of Field Programmable Gate Arrays, the concern is firstly that data stored in RAM can be corrupted, and secondly that configurable logic blocks can become damaged or corrupted. In this talk we will present our considerations of this problem in the context of an SRAM-based high reliability flash file system. We will firstly demonstrate our test harness where we simulate the injection of SEUs into our FPGA. We will then discuss how we propose to build a self repairing configuration using triple modular redundancy and partial dynamic reconfiguration. Finally we will discuss how the reliability of the system may be tested and measured such that it can be used with confidence in either data acquisition or control system applications in rad-hard environments.
 Bibliography:   [BibTeX]
 Abstract: [PDF] 
 Presentation: [PDF]