JCircus 2.0: an Extension of an Automatic Translator from Circus to Java
S.L.M. BARROCAS and M.V.M. OLIVEIRA, Universidade Federal do Rio Grande do Norte, Brazil

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.

A Debugger for Communicating Scala Objects
Andrew BATE and Gavin LOWE, Department of Computer Science, University of Oxford, England

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.

Design and Use of CSP Meta-Model for Embedded Control Software Development
Maarten M. BEZEMER, Robert J.W. WILTERDINK and Jan F. BROENINK, Faculty EEMCS, University of Twente, The Netherlands

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.

A Comparison of Message Passing Interface and Communicating Process Architecture Networking Communication Performance
Kevin CHALMERS, School of Computing, Edinburgh Napier University, UK

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.

Beauty And The Beast: Exploiting GPUs In Haskell
Alex COLE (a), Alistair A. MCEWAN (a) and Geoff MAINLAND (b)
(a) Department of Engineering, University of Leicester, England
(b) Microsoft Research, Cambridge, England

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.

Supporting Timed CSP Operators in CSP++
William B. GARDNER and Yuriy SOLOVYOV, School of Computer Science, University of Guelph, Canada

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.

Designing a Concurrent File Server
James WHITEHEAD II, Department of Computer Science, University of Oxford, England

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.

A Distributed Multi-Agent Control System for Power Consumption in Buildings
Anna Magdalena KOSEK and 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.

Exception Handling and Checkpointing in CSP
Mads Ohm LARSEN (a) and Brian VINTER (b)
(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.

A High Performance Reconfigurable Architecture for Flash File Systems
Irfan MIR, Alistair A. MCEWAN and Neil J. PERRINS, Department of Engineering, University of Leicester, England

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.

Schedulability Analysis of Timed CSP Models Using the PAT Model Checker
Oguzcan OGUZ, Jan F. BROENINK and Angelika MADER, Faculty EEMCS, University of Twente, The Netherlands

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.

XCHANs: Notes on a New Channel Type
Øyvind TEIG, Autronica Fire and Security AS, Trondheim, Norway

Abstract. This paper proposes a new channel type, XCHAN, for communicating messages between a sender and receiver. Sending on an XCHAN is asynchronous, with the sending process informed as to its success. XCHANs may be buffered, in which case a successful send means the message has got into the buffer. A successful send to an unbuffered XCHAN means the receiving process has the message. In either case, a failed send means the message has been discarded. If sending on an XCHAN fails, a built-in feedback channel (the x-channel, which has conventional channel semantics) will signal to the sender when the channel is ready for input (i.e., the next send will succeed). This x-channel may be used in a select or ALT by the sender side (only input guards are needed), so that the sender may passively wait for this notification whilst servicing other events. When the x-channel signal is taken, the sender should send as soon as possible -- but it is free to send something other than the message originally attempted (e.g. some freshly arrived data). The paper compares the use of XCHAN with the use of output guards in select/ALT statements. XCHAN usage should follow a design pattern, which is also described. Since the XCHAN never blocks, its use contributes towards deadlock- avoidance. The XCHAN offers one solution to the problem of overflow handling associated with a fast producer and slow consumer in message passing systems. The claim is that availability of XCHANs for channel based systems gives the designer and programmer another means to simplify and increase quality.

Specification of APERTIF Polyphase Filter Bank in ClaSH
Rinse WESTER (a), Dimitrios SARAKIOTIS (a), Eric KOOISTRA (b) and Jan KUPER (b)
(a) Department of Computer Science, University of Twente, The Netherlands
(b) ASTRON, Dwingelo, The Netherlands

Abstract. ClaSH, 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 ClaSH 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 ClaSH which is derived from the Haskell formulation by applying only minor changes. We show that the ClaSH formulation can be directly mapped to hardware, thus exploiting the parallelism and concurrency that is present in the original mathematical specification.

JCircus Demo
S.L.M. BARROCAS and M.V.M. OLIVEIRA, Universidade Federal do Rio Grande do Norte, Brazil

Developing JIWY using TERRA
Maarten M. BEZEMER, Robert J.W. WILTERDINK and Jan F. BROENINK, Faculty EEMCS, University of Twente, The Netherlands

Handel-C++ - Adding Syntactic Support to C++
Alex COLE, Department of Engineering, University of Leicester, England

A CPA Series
Ian EAST, Open Channel Publishing Ltd., England

Data Escape Analysis for Process Oriented Systems
Martin ELLIS and Fred BARNES, School of Computing, University of Kent, England

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).

Implementation of an Agent-based Model with TBB Technique
Ye LI, Institute of Arts, Media and Computer Games, University of Abertay Dundee, UK

Polyphonic Processors - Fantasy on an FPGA
Richard MILLER, Miller Research Ltd., Oxford, England

SEU Protection for High-Reliability Flash File Systems
Neil J. PERRINS and Alistair A. MCEWAN, Department of Engineering, University of Leicester, England

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.

Process-Oriented Building Blocks
Adam SAMPSON, Institute of Arts, Media and Computer Games, University of Abertay Dundee, UK

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.

Cancellable Servers - a Pattern for Curiousity
Peter H. WELCH, School of Computing, University of Kent, England

Unfinished Business - occam-pi²
Peter H. WELCH, School of Computing, University of Kent, England

occam Obviously
Peter H. WELCH, School of Computing, University of Kent, England

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)?