Implementing Generalised Alt
Gavin LOWE, Department of Computer Science, Oxford University, England

Abstract. In this paper we describe the design and implementation of a generalised alt operator for the Communicating Scala Objects library. The alt operator provides a choice between communications on different channels. Our generalisation removes previous restrictions on the use of alts that prevented both ends of a channel from being used in an alt. The cost of the generalisation is a much more difficult implementation, but one that still gives very acceptable performance. In order to support the design, and greatly increase our confidence in its correctness, we build CSP models corresponding to our design, and use the FDR model checker to analyse them.

Adding Formal Verification to occam-π
Peter H. WELCH (a), Jan B. PEDERSEN (b), Frederick R.M. BARNES (a), Carl G. RITSON (a) and Neil C.C. BROWN (a)
(a) School of Computing, University of Kent, England
(b) School of Computer Science, University of Nevada, USA

Abstract. This is a proposal for the formal verification of occam-π programs to be managed entirely within occam-π. The language is extended with qualifiers on types and processes (to indicate relevance for verification and/or execution) and assertions about refinement (including deadlock, livelock and determinism). The compiler abstracts a set of CSPm equations and assertions, delegates their analysis to the FDR2 model checker and reports back in terms related to the occam-π source. The rules for mapping the extended occam-π to CSPm are given. The full range of CSPm assertions is accessible, with no knowledge of CSP formalism required by the occam-π programmer. Programs are proved just by writing and compiling programs. A case-study analysing a new (and elegant) solution to the Dining Philosophers problem is presented. Deadlock-freedom for colleges with any number of philosphers is established by verifying an induction argument (the base and induction steps). Finally, following guidelines laid down by Roscoe, the careful use of model compression is demonstrated to verify directly the deadlock-freedom of an occam-π college with 10^2000 philosphers (in around 30 seconds). All we need is a universe large enough to contain the computer on which to run it.

The Flying Gator: Towards Aerial Robotics in occam-π
Ian ARMSTRONG, Michael PIRRONE-BRUSSE, Anthony SMITH and Matthew C. JADUD, Department of Computer Science, Allegheny College, USA

Abstract. The Flying Gator is an unmanned aerial vehicle developed to support investigations regarding concurrent and parallel control for robotic and embedded systems. During ten weeks in the summer of 2010, we designed, built, and tested an airframe, control electronics, and a concurrent firmware capable of sustaining autonomous level flight. Ultimately, we hope to have a robust, open source control system capable of supporting interesting research questions exploring concurrency in real time systems as well as current issues in sustainable agriculture.

LUNA: Hard Real-Time, Multi-Threaded, CSP-Capable Execution Framework
Maarten M. BEZEMER, Robert J.W. WILTERDINK and Jan F. BROENINK, Control Engineering, Faculty EE-M-CS, University of Twente, The Netherlands

Abstract. Modern embedded systems have multiple cores available. The CTC++ library is not able to make use of these cores, so a new framework is required to control the robotic setups in our lab. This paper first looks into the available frameworks and compares them to the requirements for controlling the setups. It concludes that none of the available frameworks meet the requirements, so a new framework is developed, called LUNA. The LUNA architecture is component based, resulting in a modular structure. The core components take care of the platform related issues. For each supported platform, these components have a different implementation, effectively providing a platform abstraction layer. High-level components take care of platform-independent tasks, using the core components. Execution engine components implement the algorithms taking care of the execution flow, like a CSP implementation. The paper describes some interesting architectural challenges encountered during the LUNA development and their solutions. It concludes with a comparison between LUNA, C++CSP2 and CTC++. LUNA is shown to be more efficient than CTC++ and C++CSP2 with respect to switching between threads. Also, running a benchmark using CSP constructs, shows that LUNA is more efficient compared to the other two. Furthermore, LUNA is also capable of controlling actual robotic setups with good timing properties.

Performance of the Distributed CPA Protocol and Architecture on Traditional Networks
Kevin CHALMERS, School of Computing, Edinburgh Napier University, Scotland

Abstract. Performance of communication mechanisms is very important in distributed systems frameworks, especially when the aim is to provide a particular type of behavior across a network. In this paper, performance measurements of the distributed Communicating Process Architectures networking protocol and stack is presented. The results presented show that for general communication, the distributed CPA architecture is close to the baseline network performance, although when dealing with parallel speedup for the Mandelbrot set, little performance is gained. A discussion into the future direction of the distributed CPA architecture and protocol in relation to occam-π and other runtimes is also presented.

A Comparison Of Data-Parallel Programming Systems With Accelerator
Alex COLE (a), Alistair A. MCEWAN (a) and Satnam SINGH (b)
(a) Department of Engineering, University of Leicester, England
(b) Microsoft Research, Cambridge, England

Abstract. Data parallel programming provides an accessible model for exploiting the power of parallel computing elements without resorting to the explicit use of low level programming techniques based on locks, threads and monitors. The emergence of GPUs with hundreds or thousands of processing cores has made data parallel computing available to a wider class of programmers. GPUs can be used not only for accelerating the processing of computer graphics but also for general purpose data-parallel programming. Low level data-parallel programming languages based on the CUDA provide an approach for developing programs for GPUs but these languages require explicit creation and coordination of threads and careful data layout and movement. This has created a demand for higher level programming languages and libraries which raise the abstraction level of data-parallel programming and increase programmer productivity. The Accelerator system was developed by Microsoft for writing data parallel code in a high level manner which can execute on GPUs, multicore processors using SSE3 vector instructions and FPGA chips. This paper compares the performance and development effort of the high level Accelerator system against lower level systems which are more difficult to use but may yield better results. Specifically, we compare against the NVIDIA CUDA compiler and sequential C++ code considering both the level of abstraction in the implementation code and the execution models. We compare the performance of these systems using several case studies. For some classes of problems, Accelerator has a performance comparable to CUDA, but for others its performance is significantly reduced however in all cases it provides a model which is easier to use and allows for greater programmer productivity.

Verification of a Dynamic Channel Model using the SPIN Model-Checker
Rune Møllegaard FRIBORG and Brian VINTER, eScience Center, Niels Bohr Institute, University of Copenhagen, Denmark

Abstract. This paper presents the central elements of a new dynamic channel leading towards a flexible CSP design suited for high-level languages. This channel is separated into three models: a shared-memory channel, a distributed channel and a dynamic synchronisation layer. The models are described such that they may function as a basis for implementing a CSP library, though many of the common features known in available CSP libraries have been excluded from the models. The SPIN model checker has been used to check for the presence of deadlocks, livelocks, starvation, race conditions and correct channel communication behaviour. The three models are separately verified for a variety of different process configurations. This verification is performed automatically by doing an exhaustive verification of all possible transitions using SPIN. The joint result of the models is a single dynamic channel type which supports both local and distributed any-to-any communication. This model has not been verified and the large state-space may make it unsuited for exhaustive verification using a model checker. An implementation of the dynamic channel will be able to change the internal synchronisation mechanisms on-the-fly, depending on the number of channel-ends connected or their location.

Fast Distributed Process Creation with the XMOS XS1 Architecture
James HANLON and Simon J. HOLLIS, Department of Computer Science, University of Bristol, England

Abstract. The provision of mechanisms for processor allocation in current distributed parallel programming models is very limited. This makes difficult, or even prohibits, the expression of a large class of programs which require a run-time assessment of their required resources. This includes programs whose structure is irregular, composite or unbounded. Efficient allocation of processors requires a process creation mechanism able to initiate and terminate remote computations quickly. This paper presents the design, demonstration and analysis of an explicit mechanism to do this, implemented on the XMOS XS1 architecture, as a foundation for a more dynamic scheme. It shows that process creation can be made efficient so that it incurs only a fractional overhead of the total runtime and that it can be combined naturally with recursion to enable rapid distribution of computations over a system.

A Model for Concurrency Using Single-Writer Single-Assignment Variables
Matthew HUNTBACH, School of Electronic Engineering and Computer Science, Queen Mary, University of London, England

Abstract. This is a description of a model for concurrent computation based on single-writer single-assignment variables. The description is primarily graphical, resembling the interaction nets formalism. The model embodies rules in a process which may require two or more communications from other processes to respond. However, these are managed by a partial evaluation response on receiving a single communication.

CONPASU-tool: A Concurrent Process Analysis Support Tool based on Symbolic Computation
Yoshinao ISOBE, National Institute of Advanced Industrial Science and Technology, Japan

Abstract. This paper presents an analysis-method of concurrent processes with value-passing which may cause infinite-state systems. The method consists of two steps: sequentialisation and state-reduction. In the sequentialisation, the symbolic transition graph of a given concurrent process is derived by symbolic operational semantics. In the state-reduction, the number of states in the symbolic transition graph is reduced by removing needless internal transitions. Furthermore, this paper introduces an analysis-tool called CONPASU, which implements the analysis-method, and demonstrates how CONPASU can be used for automatically analyzing concurrent processes. For example, it can extract abstract behaviors, which are useful for understanding complex behaviors, by focusing on some interesting events.

Concurrent Event-driven Programming in occam-π for the Arduino
Christian L. JACOBSEN (a), Matthew C. JADUD (b), Omer KILIC (c) and Adam T. SAMPSON (d)
(a) Department of Computer Science, University of Copenhagen, Denmark
(b) Department of Computer Science, Allegheny College, USA
(c) School of Electronics and Digital Arts, University of Kent, England
(d) Institute of Arts, Media and Computer Games, University of Abertay Dundee, Scotland

Abstract. The success of the Arduino platform has made embedded programming widely accessible. The Arduino has seen many uses, for example in rapid prototyping, hobby projects, and in art installations. Arduino users are often not experienced embedded programmers however, and writing correct software for embedded devices can be challenging. This is especially true if the software needs to use interrupts in order to interface with attached devices. Insight and careful discipline are required to avoid introducing race hazards when using interrupt routines. Instead of programming the Arduino in C or C++ as is the custom, we propose using occam-π as a language as that can help the user manage the concurrency introduced when using interrupts and help in the creation of modular, well-designed programs. This paper will introduce the Arduino, the software that enables us to run occam-π on it, and a case study of an environmental sensor used in an Environmental Science course.

Experiments in Multicore and Distributed Parallel Processing using JCSP
Jon KERRIDGE, School of Computing, Edinburgh Napier University, Scotland

Abstract. It is currently very difficult to purchase any form of computer system be it, notebook, laptop, desktop server or high performance computing system that does not contain a multicore processor. Yet the designers of applications, in general, have very little experience and knowledge of how to exploit this capability. Recently, the Scottish Informatics and Computer Science Alliance (SICSA) issued a challenge to investigate the ability of developers to parallelise a simple Concordance algorithm. Ongoing work had also shown that the use of multicore processors for applications that have internal parallelism is not as straightforward as might be imagined. Two applications are considered: calculating pi using Monte Carlo methods and the SICSA Concordance application. The ease with which parallelism can be extracted from a single application using both single multicore processors and distributed networks of such multicore processors is investigated. It is shown that naive application of parallel programming techniques does not produce the desired results and that considerable care has to be taken if multicore systems are to result in improved performance. Meanwhile the use of distributed systems tends to produce more predictable and reasonable benefits resulting from parallelisation of applications.

The Computation Time Process Model
Martin KORSGAARD and Sverre HENDSETH, Department of Engineering Cybernetics, Norwegian University of Science and Technology, Norway

Abstract. In traditional real-time multiprocessor schedulability analysis it is required that all tasks are entirely serial. This implies that if a task is written in a parallel language such as occam, all parallelism in the task must be suppressed to enable schedulability analysis. Part of the reason for this restriction is the difficulty in analysing execution times of programs with a complex parallel structure. In this paper we introduce an abstract model for reasoning about the temporal properties of such programs. Within this model, we define what it means for a process to be easier to schedule than another, and the notion of upper bounds on execution times. Counterintuitive temporal behaviour is demonstrated to be inherent in all systems where processes are allowed an arbitrary parallel structure. For example, there exist processes that are guaranteed to complete on some schedule, that may not complete if executing less than the expected amount of computation. Not all processes exhibit such counterintuitive behaviour, and we identify a subset of processes that are well-behaved in this respect. The results from this paper is a necessary prerequisite for a complete schedulability analysis of systems with an arbitrary parallel structure.

Evaluating An Emergent Behaviour Algorithm for Energy Conservation in Lighting Systems Using JCSP
Anna KOSEK (a), Aly SYED (b) and Jon KERRIDGE (c)
(a) Risoe DTU National Laboratory of Sustainable Energy, Denmark
(b) NXP Semiconductors, Eindhoven, The Netherlands
(c) School of Computing, Edinburgh Napier University, Scotland

Abstract. Since the invention of the light bulb, artificial light is accompanying people all around the world every day and night. As the light bulb itself evolved a lot through years, light control systems are still switch-based and require users to make most of the decisions about its behaviour. This paper presents an algorithm for emergent behaviour in a lighting system to achieve stable, user defined light level, while saving energy. The algorithm employs a parallel design and was tested using JCSP.

Static Scoping and Name Resolution for Mobile Processes with Polymorphic Interfaces
Jan B. PEDERSEN and Matthew SOWDERS, School of Computer Science, University of Nevada, USA

Abstract. In this paper we consider a refinement of the concept of mobile processes in a process oriented language. More specifically, we investigate the possibility of allowing resumption of suspended mobile processes with different interfaces. This is a refinement of the approach taken currently in languages like occam-π. The goal of this research is to implement varying resumption interfaces in ProcessJ, a process oriented language being developed at UNLV.

Process-Oriented Subsumption Architectures in Swarm Robotic Systems
Jeremy C. POSSO (a), Adam T. SAMPSON (b), Jonathan SIMPSON (c) and Jon TIMMIS (d)
(a) Department of Computer Science, University of York, England
(b) Institute of Arts, Media and Computer Games, University of Abertay Dundee, Scotland
(c) School of Computing, University of Kent, England
(d) Department of Electronics, University of York, England

Abstract. Previous work has demonstrated the feasibility of using process-oriented programming to implement simple subsumption architectures for robot control. However, the utility and scalability of process-based subsumption architectures for more complex tasks and those involving multiple robots has not been proven. We report our experience of applying these techniques to the implementation of a standard foraging problem in swarm robotics, using occam-π to implement a subsumption control system. Through building a system with a realistic level of complexity, we have discovered both advantages and disadvantages to the process-oriented subsumption approach for larger robot control systems.

Object Store Based Simulation Interworking
Carl G. RITSON (a), Paul S. ANDREWS (b) and Adam T. SAMPSON (c)
(a) School of Computing, University of Kent, England
(b) Department of Computer Science, University of York, England
(c) Institute of Arts, Media and Computer Games, University of Abertay Dundee, Scotland

Abstract. The CoSMoS project is building generic modelling tools and simulation techniques for complex systems. As part of this project a number of simulations have been developed in many programming languages. This paper describes a framework for interconnecting simulation components written in different programming languages. These simulation components are synchronised and coupled using a shared object space. This approach allows us to combine highly concurrent agent-based simulations written in occam-π, with visualisation and analysis components written in flexible scripting languages such as Python and domain specific languages such as MATLAB.

SystemVerilogCSP: Modeling Digital Asynchronous Circuits Using SystemVerilog Interfaces
Arash SAIFHASHEMI and Peter A. BEEREL, Ming Hsieh Department of Electrical Engineering, University of Southern California, USA

Abstract. This paper describes how to model channel-based digital asynchronous circuits using SystemVerilog interfaces that implement CSP-like communication events. The interfaces enable explicit handshaking of channel wires as well as abstract CSP events. This enables abstract connections between modules that are described at different levels of abstraction facilitating both verification and design. We explain how to model one-to-one, one-to-many, one-to-any, any-to-one, and synchronized channels. Moreover, we describe how to split communication actions into multiple parts to more accurately model less concurrent handshaking protocols that are commonly found in many asynchronous pipelines.

Programming the CELL-BE using CSP
Kenneth SKOVHEDE, Morten N. LARSEN and Brian VINTER, eScience Center, Niels Bohr Institute, University of Copenhagen, Denmark

Abstract. The current trend in processor design seems to focus on using multiple cores, similar to a cluster-on-a-chip model. These processors are generally fast and power efficient, but due to their highly parallel nature, they are notoriously difficult to program for most scientists. One such processor is the CELL broadband engine (CELL-BE) which is known for its high performance, but also for a complex programming model which makes it difficult to exploit the architecture to its full potential. To address this difficulty, this paper proposes to change the programming model to use the principles of CSP design, thus making it simpler to program the CELL-BE and avoid livelocks, deadlocks and race conditions. The CSP model described here comprises a thread library for the synergistic processing elements (SPEs) and a simple channel based communication interface. To examine the scalability of the implementation, experiments are performed with both scientific computational cores and synthetic workloads. The implemented CSP model has a simple API and is shown to scale well for problems with significant computational requirements.

A Systems Re-engineering Case Study: Programming Robots with occam and Handel-C
Dan SLIPPER and Alistair A. MCEWAN, Department of Engineering, University of Leicester, England

Abstract. This paper introduces a case study exploring some of the legacy issues that may be faced when redeveloping a system. The case study is a robotics system programmed in occam and Handel-C, allowing us to draw comparisons between software and hardware implementations in terms of program architecture, ease of program code verification, and differences in the behaviour of the robot. The two languages used have been selected because of their model of concurrency and their relation to CSP. The case study contributes evidence that re-implementing a system from an abstract model may present implementation specific issues despite maintaining the same underlying program control structure. The paper identifies these problems and suggests a number of steps that could be taken to help mitigate some of the issues.

Prioritised Choice over Multiway Synchronisation
Douglas N. WARREN, School of Computing, University of Kent, England

Abstract. Previous algorithms for resolving choice over multiway synchronisations have been incompatible with the notion of priority. This paper discusses some of the problems resulting from this limitation and offers a subtle expansion of the definition of priority to make choice meaningful when multiway events are involved. Presented in this paper is a prototype extension to the JCSP library that enables prioritised choice over multiway synchronisations and which is compatible with existing JCSP Guards. Also discussed are some of the practical applications for this algorithm as well as its comparative performance.

Serving Web Content with Dynamic Process Networks in Go
James WHITEHEAD, Department of Computer Science, Oxford University, England

Abstract. This paper introduces webpipes, a compositional web server toolkit written using the Go programming language as part of an investigation of concurrent software architectures. This toolkit utilizes an architecture where multiple functional components respond to requests, rather than the traditional monolithic web server model. We provide a classification of web server components and a set of type definitions based on these insights that make it easier for programmers to create new purpose-built components for their systems. The abstractions provided by our toolkit allow servers to be deployed using several concurrency strategies. We examine the overhead of such a framework, and discuss possible enhancements that may help to reduce this overhead.

Development of an ML based Verification Tool for Timed CSP Processes
Takeshi YAMAKAWA, Tsuneki OHASHI and Chikara FUKUNAGA, Tokyo Metropolitan University, Japan

Abstract. We report the development of a verification tool for Timed CSP processes. The tool has been built on the functional programming language ML. The tool interprets processes described in both timed and untimed CSP, converting them to ML functions, and executing those functions for the verification of refinement in the timed traces and timewise traces models. Using the programmability of higher order functionality, the description of CSP processes with ML has been synthesised naturally. The effectiveness of the tool is demonstrated with an example analysing implementations of Fischer's algorithm for the exclusive control of a shared resource in a multi-processor environment.

Guppy
Frederick R.M. BARNES, School of Computing, University of Kent, England

Mobile Processes and Call Channels with Variant Interfaces (a Duality)
Eric BONNICI and Peter H. WELCH, School of Computing, University of Kent, England

Abstract. The current model of mobile processes in occam-π implements a single interface for host processes to use. However, different hosts holding different kinds of resource will naturally require different interfaces to interact with their visitors. So, current occam-π mobiles have to offer a single union of all the interfaces needed and hosts must provide dummy arguments for those irrelevant to its particular calls. This opens the possibilty of programming errors in both hosts and mobile should those dummies mistakenly be used. This talk considers a revised model for mobile processes that allows many interfaces. The talk also proposes a concept of variant call channels, that expands on a mechanism proposed for the occam3 language, and shows a simple duality between the revised mobile processes and mobile variant call channels. An implementation of mobile variant call channels, via source-code transformation to standard occam-π mobile channel bundles, has been devised – which gives an implementation route for the revised mobile process model and an operational semantics. If time, the ideas will be illustrated with a case study based on the Santa Claus problem, where the elves and reindeer are mobile processes.

Parallel Usage Checking - an Observation
Barry M. COOK, 4Links Limited, Bletchley Park, Milton Keynes, England

Abstract. One of the great strengths of CSP based concurrent programming languages (such as occam) is the support provided to the programmer in avoiding the creation of erroneous programs. One such support – parallel usage checking – detects program behaviours that may leave a variable in an unpredictable state. Current implementations of this check are safe but can lead to inefficient program implementations. In some cases, a simple program transformation can be used to demonstrate the safety of programs that would otherwise fail existing tests. By presenting a simple (but generic) example, I will show that using such a transformation allows the creation of more efficient programs.

Formal Analysis of Concurrent OS (RMoX) Device Drivers
Martin ELLIS, School of Computing, University of Kent, England

Abstract. Many tools exists for writing safe and correct device drivers for conventional operating systems, from runtime driver management layers (that try to detect errors and recover from them) to static analysis systems like SLAM. Unfortunately, these tools do not map well to the concurrent drivers we write for RMoX. This presentation will look at how we can build safe and correct device drivers, using traditional occam analysis approaches (such as CSP) and tools (such as FDR). Experiments in generating formal models of hardware/driver interfaces from our occam implementations will be described, along with how we intend to use these models to prove correctness properties for our drivers.

Distributing Concurrent Simulation
Adam T. SAMPSON, Institute of Arts, Media and Computer Games, University of Abertay Dundee, Scotland

This is a Parallel Parrot
Adam T. SAMPSON, Institute of Arts, Media and Computer Games, University of Abertay Dundee, Scotland

Exploring Peer-to-Peer Virtualized Multithreaded Services
Kevin VELLA, Department of Computer Science and Artificial Intelligence, University of Malta, Malta

Demonstration of the LUNA Framework
Robert J.W. WILTERDINK, Maarten M. BEZEMER and Jan F. BROENINK, Control Engineering, Faculty EE-M-CS, University of Twente, The Netherlands

Abstract. In this demonstration of the LUNA hard real-time, multi-threaded, CSP-capable execution framework, we use the JIWY-II pan-tilt camera robotic setup. The webcam can rotate horizontally and vertically, driven by two electromotors, controlled by software written as LUNA concurrent processes. The loop control algorithms are designed and generated by 20-sim, a tool for modeling and designing (controlled) mechatronic systems. This way, all code is generated, i.e. a model-driven approach. The demo will show that the LUNA library is capable of controlling setups in hard real-time, and that the implemented real-time logger provides valuable insight in the applications behaviour, i.e. control algorithms and LUNA framework.