WoTUG - The place for concurrent processes

CPA 2008 Programme

The CPA 2008 programme comprises two full day, one half day, and two evening sessions. A late bar each evening and a conference dinner provides ample opportunity to relax, socialize, and discuss issues informally. An overview of the academic programme, some history, motivation and a welcome can be found in the Preface to the CPA 2008 Proceedings.

The conference opens on Sunday evening with registration, an evening meal, and the first of the informal Fringe sessions. Monday morning will open with a short welcome address by Professor Peter Welch (University of Kent), current WoTUG Chair, and Professor Susan Stepney (University of York), CPA 2008 Chair. Two keynote talks, from Colin O'Halloran (Director, Systems Assurance Programme, QinetiQ) and Professor Samson Abramsky (FRS, Oxford University Computing Laboratory), will lead off the Monday and Tuesday sessions respectively. The second Fringe is on Monday evening. The conference dinner is on Tuesday evening. The conference will close after lunch on Wednesday.

Associated with the conference this year is the first CoSMoS Workshop and this follows on the Thursday.

Abstracts for all the papers are linked from the timetable to further down this page.

CPA 2008 Timetable

Sunday / September 7th, 2008
18:00 Registration at the York Marriott Hotel
18:30 Buffet Supper
20:00 Fringe Session 1
Note: because of the nature of the Fringe, the following items are provisional. More may take place and the ordering may change.
Tock: One Year On (Abstract)
Adam T. Sampson and Neil C.C. Brown, Computing Laboratory, University of Kent
Lego Robots using JCSP (Abstract)
Jon Kerridge, School of Computing, Napier University
How to Make a Process Invisible (Abstract)
Neil C.C. Brown, Computing Laboratory, University of Kent
Handel-C Source Level Debugging (Abstract)
Herman Roebbers, TASS Software Professionals
Towards Guaranteeing Process Oriented Program Behaviour (Abstract)
Fred Barnes, Computing Laboratory, University of Kent
PICOMS: Prioritised Inferred Choice Over Multiway Synchronisation (Abstract)
Doug Warren, Computing Laboratory, University of Kent
23:00 Late bar ...
Monday / September 8th, 2008
08:50 Welcome
Session 1 Chair: Jan Broenink
09:00 Keynote Address: How to Soar with CSP (Abstract)
Colin O'Halloran, Director Systems Assurance Programme, QinetiQ
10:00 Experiments in Translating CSP || B to Handel-C (Abstract)
Steve Schneider (a), Helen Treharne (a), Alistair McEwan (b) and Wilson Ifill (c),
(a) University of Surrey
(b) University of Leicester
(c) AWE Aldermaston
10:30 Coffee/Tea
Session 2 Chair: Fiona Polack
11:00 YASS: a Scalable Sensornet Simulator for Large Scale Experimentation (Abstract)
Jonathan Tate and Iain Bate, Department of Computer Science, University of York
11:30 Modelling a Multi-Core Media Processor using JCSP (Abstract)
Anna Kosek (a), Jon Kerridge (a) and Aly Syed (b)
(a) School of Computing, Napier University
(b) NXP Semiconductors Research, Eindhoven
12:00 Representation and Implementation of CSP and VCR Traces (Abstract)
Neil Brown (a) and Marc L. Smith (b),
(a) Computing Laboratory, University of Kent
(b) Computer Science Department, Vassar College, Poughkeepsie, New York
12:30 Lunch
Session 3 Chair: Herman Roebbers
14:00 Shared-Clock Methodology for Time-Triggered Multi-Cores (Abstract)
Keith F. Athaide (a), Michael J. Pont (a) and Devaraj Ayavoo (b),
(a) Embedded Systems Laboratory, University of Leicester
(b) TTE Systems Ltd, 106 New Walk, Leicester LE1 7EA
14:30 FPGA Based Control of a Production Cell System (Abstract)
Marcel A. Groothuis, Jasper Van Zuijlen and Jan F. Broenink, Control Engineering, Faculty EEMCS, University of Twente
15:00 Transfer Request Broker: Resolving Input-Output Choice (Abstract)
Oliver Faust, Bernhard H.C. Sputh and Alastair R. Allen, Department of Engineering, University of Aberdeen
15:30 Tea/Coffee
Session 4 Chair: Brian Vinter
16:00 A Critique of JCSP Networking (Abstract)
Kevin Chalmers, Jon Kerridge and Imed Romdhani, School of Computing, Napier University
16:30 JCSPre: the Robot Edition To Control LEGO NXT Robots (Abstract)
Jon Kerridge, Alex Panayotopoulos and Patrick Lismore, School of Computing, Napier University
17:00 Solving the Santa Claus Problem: a Comparison of Various Concurrent Programming Techniques (Abstract)
Jason Hurt and Jan B. Pedersen, School of Computer Science, University of Nevada
18:30 Dinner
20:00 Fringe Session 2
Note: because of the nature of the Fringe, the following items are provisional. More may take place and the ordering may change.
Designing with Software Defined Silicon (Abstract)
Ali Dixon, XMOS Semiconductor
Designing Animation Facilities for gCSP (Abstract)
Hans T.J. Van Der Steen, Marcel A. Groothuis and Jan F. Broenink, Control Engineering, Faculty EEMCS, University of Twente
Introducing JCSP Networking 2.0 (Abstract)
Kevin Chalmers, School of Computing, Napier University
Santa's Groovy Helper (Abstract)
Jon Kerridge, School of Computing, Napier University
Santa Claus – with Mobile Reindeer and Elves (Abstract)
Peter H. Welch (a) and Jan B. Pedersen (b),
(a) Computing Laboratory, University of Kent
(b) School of Computer Science, University of Nevada, Las Vegas
Mobile Processes in an Ant Simulation (Abstract)
Eric Bonnici, Computing Laboratory, University of Kent
23:00 Late bar ...
Tuesday / September 9th, 2008
Session 5 Chair: Peter Welch
09:00 Keynote Address: Types, Orthogonality and Genericity: Some Tools for Communicating Process Architectures (Abstract)
Samson Abramsky, Oxford University Computing Laboratory
10:00 Prioritized Service Architecture: Refinement and Visual Design (Abstract)
Ian East, Department for Computing, Oxford Brookes University
10:30 Coffee/Tea
Session 6 Chair: Roger Peel
11:00 Communicating Scala Objects (Abstract)
Bernard Sufrin, Oxford University Computing Laboratory
11:30 Visual Process-Oriented Programming for Robotics (Abstract)
Jonathan Simpson and Christian L. Jacobsen, Computing Laboratory, University of Kent
12:00 Asynchronous Active Objects in Java (Abstract)
George Oprean and Jan B. Pedersen, School of Computer Science, University of Nevada
12:30 Lunch
Session 7 Chair: Alistair McEwan
14:00 Two-Way Protocols for occam-pi (Abstract)
Adam T. Sampson, Computing Laboratory, University of Kent
14:30 Combining EDF Scheduling with occam using the Toc Programming Language (Abstract)
Martin Korsgaard and Sverre Hendseth, Department of Engineering Cybernetics, Norwegian University of Science and Technology
15:00 Communicating Haskell Processes: Composable Explicit Concurrency using Monads (Abstract)
Neil Brown, Computing Laboratory, University of Kent
15:30 Tea/Coffee
Session 8 Chair: Fred Barnes
16:00 Virtual Machine Based Debugging for occam-pi (Abstract)
Carl G. Ritson and Jonathan Simpson, Computing Laboratory, University of Kent
16:30 CSPBuilder – CSP based Scientific Workflow Modeling (Abstract)
Rune Møllegård Friborg and Brian Vinter, Department of Computer Science, University of Copenhagen
17:00 Process-Oriented Collective Operations (Abstract)
John Markus Bjørndalen (a) and Adam T. Sampson (b),
(a) Department of Computer Science, University of Tromsø
(b) Computing Laboratory, University of Kent
20:00 Conference Dinner
22:00 Late bar ...
Wednesday / September 10th, 2008
Session 9 Chair: Barry Cook
09:00 Mechanical Verification of a Two-Way Sliding Window Protocol (Abstract)
Bahareh Badban (a), Wan Fokkink (b) and Jaco van de Pol (c),
(a) Department of Computer and Information Science, University of Konstanz
(b) Department of Computer Science, Vrije Universiteit Amsterdam
(c) Department of EEMCS, University of Twente
09:30 RRABP: Point-to-Point Communication over Unreliable Components (Abstract)
Bernhard H.C. Sputh, Oliver Faust and Alastair R. Allen, School of Engineering, University of Aberdeen
10:00 IC2IC: a Lightweight Serial Interconnect Channel for Multiprocessor Networks (Abstract)
Oliver Faust, Bernhard H.C. Sputh, and Alastair R. Allen, Department of Engineering, University of Aberdeen
10:30 Coffee/Tea
Session 10 Chair: Ruth Ivimey-Cook
11:00 A CSP Model for Mobile Channels (Abstract)
Peter H. Welch and Frederick R.M. Barnes, Computing Laboratory, University of Kent
11:30 Mobile Agents and Processes using Communicating Process Architectures (Abstract)
Jon Kerridge, Jens-Oliver Haschke and Kevin Chalmers, School of Computing, Napier University
12:00 CPA 2008 Best Paper Awards
WoTUG Annual General Meeting
13:00 Lunch
14:00 End of CPA 2008

Abstracts – Keynote Presentations

Types, Orthogonality and Genericity: Some Tools for Communicating Process Architectures
Samson ABRAMSKY, Oxford University Computing Laboratory
 
Abstract. We shall develop a simple and natural formalization of the idea of client-server architectures, and, based on this, define a notion of orthogonality between clients and servers, which embodies strong correctness properties, and exposes the rich logical structure inherent in such systems. Then we generalize from pure clients and servers to components, which provide some services to the environment, and require others from it. We identify the key notion of composition of such components, in which some of the services required by one component are supplied by another. This allows complex systems to be built from ultimately simple components. We show that this has the logical form of the Cut rule, a fundamental principle of logic, and that it can be enriched with a suitable notion of behavioural types based on orthogonality, in such a way that correctness properties are preserved by composition. We also develop the basic ideas of how logical constructions can be used to develop structured interfaces for systems, with operations corresponding to logical rules. Finally, we show how the setting can be enhanced, and made more robust and expressive, by using names (as in the pi-calculus) to allow clients to bind dynamically to generic instances of services.
How to Soar with CSP
Colin O'HALLORAN, Director Systems Assurance Programme, QinetiQ
 
Abstract. In this talk, I shall discuss work on the necessary technology required for flight clearance of Autonomous Aircraft employing Agents by reducing the certification problem to small verifiable steps that can be carried out by a machine. The certification of such Agents falls into two parts: the validation of the safety of the Agent; and the verification of the implementation of the agent. The work focuses on the Soar agent language and the main results are:
  • a language subset for Soar, designed for formal analysis;
  • a formal model of the Soar subset written in CSP;
  • a prototype translator "Soar2Csp" from Soar to the CSP model;
  • a framework for static analysis of Soar agents through model checking using FDR2;
  • the identification of "healthiness conditions" required of any Soar Agent;
  • a verifiable implementation of the CSP based Soar agents on an FPGA.

Abstracts – Accepted Papers

A CSP Model for Mobile Channels
Peter H. WELCH and Frederick R.M. BARNES, Computing Laboratory, University of Kent
 
Abstract. CSP processes have a static view of their environment — a fixed set of events through which they synchronise with each other. In contrast, the pi-calculus is based on the dynamic construction of events (channels) and their distribution over pre-existing channels. In this way, process networks can be constructed dynamically with processes acquiring new connectivity. For the construction of complex systems, such as Internet trading and the modeling of living organisms, such capabilities have an obvious attraction. The occam-pi multiprocessing language is built upon classical occam, whose design and semantics are founded on CSP. To address the dynamics of complex systems, occam-pi extensions enable the movement of channels (and multiway synchronisation barriers) through channels, with constraints in line with previous occam discipline for safe and efficient programming. This paper reconciles these extensions by building a formal (operational) semantics for mobile channels entirely within CSP. These semantics provide two benefits: formal analysis of occam-pi systems using mobile channels and formal specification of implementation mechanisms for mobiles used by the occam-pi compiler and run-time kernel.
Communicating Scala Objects
Bernard SUFRIN, Oxford University Computing Laboratory
 
Abstract. In this paper we introduce the core features of CSO (Communicating Scala Objects) – a notationally convenient embedding of the essence of occam in a modern, generically typed, object-oriented programming language that is compiled to Java Virtual Machine (JVM) code. Initially inspired by an early release of JCSP, CSO goes beyond JCSP expressively in some respects, including the provision of a unitary extended rendezvous notation and appropriate treatment of subtype variance in channels and ports. Similarities with recent versions of JCSP include the treatment of channel ends (we call them ports) as parameterized types. Ports and channels may be transmitted on channels (including inter-JVM channels), provided that an obvious design rule – the ownership rule – is obeyed. Significant differences with recent versions of JCSP include a treatment of network termination that is significantly simpler than the “poisoning” approach (perhaps at the cost of reduced programming convenience), and the provision of a family of type-parameterized channel implementations with performance that obviates the need for the special-purpose scalar-typed channel implementations provided by JCSP. On standard benchmarks such as Commstime, CSO communication performance is close to or better than that of JCSP and Scala’s Actors library.
Combining EDF Scheduling with occam using the Toc Programming Language
Martin KORSGAARD and Sverre HENDSETH, Department of Engineering Cybernetics, Norwegian University of Science and Technology
 
Abstract. A special feature of the occam programming language is that its concurrency support is at the very base of the language. However, its ability to specify scheduling requirements is insufficient for use in some real-time systems. Toc is an experimental programming language that builds on occam, keeping occam’s concurrency mechanisms, while fundamentally changing its concept of time. In Toc, deadlines are specified directly in code, replacing occam’s priority constructs as themethod for controlling scheduling. Processes are scheduled lazily, in that code is not executed without an associated deadline. The deadlines propagate through channel communications, which means that a task blocked by a channel that is not ready will transfer its deadline through the channel to the dependent task. This allows the deadlines of dependent tasks to be inferred, and also creates a scheduling effect similar to priority inheritance. A compiler and run-time system has been implemented to demonstrate these principles.
Communicating Haskell Processes: Composable Explicit Concurrency using Monads
Neil BROWN, Computing Laboratory, University of Kent
 
Abstract. Writing concurrent programs in languages that lack explicit support for concurrency can often be awkward and difficult. Haskell’s monads provide a way to explicitly specify sequence and effects in a functional language, and monadic combinators allow composition of monadic actions, for example via parallelism and choice – two core aspects of Communicating Sequential Processes (CSP).We show how the use of these combinators, and being able to express processes as first-class types (monadic actions) allow for easy and elegant programming of process-oriented concurrency in a new CSP library for Haskell: Communicating Haskell Processes.
Shared-Clock Methodology for Time-Triggered Multi-Cores
Keith F. ATHAIDE (a), Michael J. PONT (a) and Devaraj AYAVOO (b),
(a) Embedded Systems Laboratory, University of Leicester
(b) TTE Systems Ltd, 106 New Walk, Leicester LE1 7EA
 
Abstract. The co-operative design methodology has significant advantages when used in safety-related systems. Coupled with the time-triggered architecture, the methodology can result in robust and predictable systems. Nevertheless, use of a co-operative design methodology may not always be appropriate especially when the system possesses tight resource and cost constraints. Under relaxed constraints, it might be possible to maintain a co-operative design by introducing additional software processing cores to the same chip. The resultant multi-core microcontroller then requires suitable design methodologies to ensure that the advantages of time-triggered co-operative design are maintained as far as possible. This paper explores the application of a time-triggered distributed-systems protocol, called “shared-clock”, on an eight-core microcontroller. The cores are connected in a mesh topology with no hardware broadcast capabilities and three implementations of the shared-clock protocol are examined. The custom multi-core system and the network interfaces used for the study are also described. The network interfaces share higher level serialising logic amongst channels, resulting in low hardware overhead when increasing the number of channels.
Experiments in Translating CSP || B to Handel-C
Steve SCHNEIDER (a), Helen TREHARNE (a), Alistair McEWAN (b) and Wilson IFILL (c),
(a) University of Surrey
(b) University of Leicester
(c) AWE Aldermaston
 
Abstract. This paper considers the issues involved in translating specifications described in the CSP || B formal method into Handel-C. There have previously been approaches to translating CSP descriptions to Handel-C, and the work presented in this paper is part of a programme of work to extend it to include the B component of a CSP || B description. Handel-C is a suitable target language because of its capability of programming communication and state, and its compilation route to hardware. The paper presents two case studies that investigate aspects of the translation: a buffer case study, and an abstract arbiter case study. These investigations have exposed a number of issues relating to the translation of the B component, and have identified a range of options available, informing more recent work on the development of a style for CSPkB specifications particularly appropriate to translation to Handel-C.
FPGA Based Control of a Production Cell System
Marcel A. GROOTHUIS, Jasper VAN ZUIJLEN and Jan F. BROENINK, Control Engineering, Faculty EEMCS, University of Twente
 
Abstract. Most motion control systems for mechatronic systems are implemented on digital computers. In this paper we present an FPGA based solution implemented on a low cost Xilinx Spartan III FPGA. A Production Cell setup with multiple parallel operating unit is chosen as test case. The embedded control software for this system is designed in gCSP using a reusable layered CSP based software structure. gCSP is extended with automatic Handel-C code generation for configuring the FPGA. Many motion control systems use floating point calculations for the loop controllers. Low cost general purpose FPGAs do not implement hardware-based floating point units. The loop controllers for this system are converted from floating point to integer-based calculations using a stepwise refinement approach. The result is a completely FPGAbased motion control system with better performance figures than previous CPUbased implementations.
YASS: a Scalable Sensornet Simulator for Large Scale Experimentation
Jonathan TATE and Iain BATE, Department of Computer Science, University of York
 
Abstract. Sensornets have been proposed consisting of thousands or tens of thousands of nodes. Economic and logistical considerations imply predeployment evaluation must take place through simulation rather than field trials. However, most current simulators are inadequate for networks with more than a few hundred nodes. In this paper we demonstrate some properties of sensornet application and protocols that only emerge when considered at scale, and cannot be effectively addressed by representative small-scale simulation. We propose a novel multi-phase approach to radio propagation modelling which substantially reduces computational overhead without significant loss in accuracy.
Mechanical Verification of a Two-Way Sliding Window Protocol
Bahareh BADBAN (a), Wan FOKKINK (b) and Jaco van de POL (c),
(a) Department of Computer and Information Science, University of Konstanz
(b) Department of Computer Science, Vrije Universiteit Amsterdam
(c) Department of EEMCS, University of Twente
 
Abstract. We prove the correctness of a two-way sliding window protocol with piggybacking, where the acknowledgments of the latest received data are attached to the next data transmitted back into the channel. The window size of both parties are considered to be finite, though they can be of different sizes. We show that this protocol is equivalent (branching bisimilar) to a pair of FIFO queues of finite capacities. The protocol is first modeled and manually proved for its correctness in the process algebraic language of mu-CRL. We use the theorem prover PVS to formalize and to mechanically prove the correctness. This implies both safety and liveness (under the assumption of fairness).
Two-Way Protocols for occam-pi
Adam T. SAMPSON, Computing Laboratory, University of Kent
 
Abstract. In the occam-pi programming language, the client-server communication pattern is generally implemented using a pair of unidirectional channels. While each channel’s protocol can be specified individually, no mechanism is yet provided to indicate the relationship between the two protocols; it is therefore not possible to statically check the safety of client-server communications. This paper proposes two-way protocols for individual channels, which would both define the structure of messages and allow the patterns of communication between processes to be specified.We show how conformance to two-way protocols can be statically checked by the occam-pi compiler using Honda’s session types. These mechanisms would considerably simplify the implementation of complex, dynamic client-server systems.
A Critique of JCSP Networking
Kevin CHALMERS, Jon KERRIDGE and Imed ROMDHANI, School of Computing, Napier University
 
Abstract. We present a critical investigation of the current implementation of JCSP Networking, examining in detail the structure and behavior of the current architecture. Information is presented detailing the current architecture and how it operates, and weaknesses in the implementation are raised, particularly when considering resource constrained devices. Experimental work is presented that illustrate memory and computational demand problems and an outline on how to overcome these weaknesses in a new implementation is described. The new implementation is designed to be lighter weight and thus provide a framework more suited for resource constrained devices which are a necessity in the field of ubiquitous computing.
RRABP: Point-to-Point Communication over Unreliable Components
Bernhard H.C. SPUTH, Oliver FAUST and Alastair R. ALLEN, School of Engineering, University of Aberdeen
 
Abstract. This paper establishes the security, stability and functionality of the resettable receiver alternating bit protocol. This protocol creates a reliable and blocking channel between sender and receiver over unreliable non-blocking communication channels. Furthermore, this protocol permits the sender to be replaced at any time, but not under all conditions without losing a message. The protocol is an extension to the alternating bit protocol with the ability for the sender to synchronise the receiver and restart the transmission. The resulting protocol uses as few messages as possible to fulfil its duty, which makes its implementation lightweight and suitable for embedded systems. An unexpected outcome of this work is the large number of different messages needed to reset the receiver reliably.
Asynchronous Active Objects in Java
George OPREAN and Jan B. PEDERSEN, School of Computer Science, University of Nevada
 
Abstract. Object Oriented languages have increased in popularity over the last two decades. The OO paradigm claims to model the way objects interact in the real world. All objects in the OO model are passive and all methods are executed synchronously in the thread of the caller. Active objects execute their methods in their own threads. The active object queues method invocations and executes them one at a time. Method invocations do not overlap, thus the object cannot be put into or seen to be in an inconsistent state. We propose an active object system implemented by extending the Java language with four new keywords: active, async, on and waitfor. We have modified Sun's open-source compiler to accept the new keywords and to translate them to regular Java code during desugaring phase. We achieve this through the use of RMI, which as a side effect, allows us to utilize a cluster of work stations to perform distributed computing
Virtual Machine Based Debugging for occam-pi
Carl G. RITSON and Jonathan SIMPSON, Computing Laboratory, University of Kent
 
Abstract. While we strive to create robust language constructs and design patterns which prevent the introduction of faults during software development, an inevitable element of human error still remains.We must therefore endeavor to ease and accelerate the process of diagnosing and fixing software faults, commonly known as debugging. Current support for debugging occam-pi programs is fairly limited. At best the developer is presented with a reference to the last known code line executed before their program abnormally terminated. This assumes the program does in fact terminate, and does not instead live-lock. In cases where this support is not sufficient, developers must instrument their own tracing support, “printf style”. An exercise which typically enlightens one as to the true meaning of concurrency ...   In this paper we explore previous work in the field of debugging occam programs and introduce a new method for run-time monitoring of occam-pi applications, based on the Transterpreter virtual machine interpreter. By adding a set of extensions to the Transterpreter, we give occam-pi processes the ability to interact with their execution environment. Use of a virtual machine allows us to expose program execution state which would otherwise require non-portable or specialised hardware support. Using a model which bears similarities to that applied when debugging embedded systems with a JTAG connection, we describe debugging occam-pi by mediating the execution of one execution process from another.
Visual Process-Oriented Programming for Robotics
Jonathan SIMPSON and Christian L. JACOBSEN, Computing Laboratory, University of Kent
 
Abstract. When teaching concurrency, using a process-oriented language, it is often introduced through a visual representation of programs in the form of process network diagrams. These diagrams allow the design of and abstract reasoning about programs, consisting of concurrently executing communicating processes, without needing any syntactic knowledge of the eventual implementation language. Process network diagrams are usually drawn on paper or with general-purpose diagramming software, meaning the program must be implemented as syntactically correct program code before it can be run. This paper presents POPed, an introductory parallel programming tool leveraging process network diagrams as a visual language for the creation of process-oriented programs. Using only visual layout and connection of pre-created components, the user can explore process orientation without knowledge of the underlying programming language, enabling a “processes first” approach to parallel programming. POPed has been targeted specifically at basic robotic control, to provide a context in which introductory parallel programming can be naturally motivated.
JCSPre: the Robot Edition To Control LEGO NXT Robots
Jon KERRIDGE, Alex PANAYOTOPOULOS and Patrick LISMORE, School of Computing, Napier University
 
Abstract. JCSPre is a highly reduced version of the JCSP (Communicating Sequential Processes for Java) parallel programming environment. JCSPre has been implemented on a LEGO Mindstorms NXT brick using the LeJOS Java runtime environment. The LeJOS environment provides an abstraction for the NXT Robot in terms of Sensors, Sensor Ports and Motors, amongst others. In the implementation described these abstractions have been converted into the equivalent active component that is much easier to incorporate into a parallel robot controller. Their use in a simple line following robot is described, thereby demonstrating the ease with which robot controllers can be built using parallel programming principles. As a further demonstration we show how the line following robot controls a slave robot by means of Bluetooth communications.
Solving the Santa Claus Problem: a Comparison of Various Concurrent Programming Techniques
Jason HURT and Jan B. PEDERSEN, School of Computer Science, University of Nevada
 
Abstract. The Santa Claus problem provides an excellent exercise in concurrent programming. It can be used to show the simplicity or complexity of solving problems using a particular set of concurrency mechanisms and offers a comparison of these mechanisms. Shared-memory constructs, message passing constructs, and process oriented constructs will be used in various programming languages to solve the Santa Claus Problem. Various concurrency mechanisms available will be examined and analyzed as to their respective strengths and weaknesses.
IC2IC: a Lightweight Serial Interconnect Channel for Multiprocessor Networks
Oliver FAUST, Bernhard H.C. SPUTH, and Alastair R. ALLEN, Department of Engineering, University of Aberdeen
 
Abstract. IC2IC links introduce blocking functionality to a low latency high performance data link between independent processors. The blocking functionality was achieved with the so-called alternating bit protocol. Furthermore, the protocol hardens the link against message loss and message duplication. This paper provides a detailed discussion of the link signals and the protocol layer. The practical part shows an example implementation of the IC2IC serial link. This example implementation establishes an IC2IC link between two configurable hardware devices. Each device incorporates a process network which implements the IC2IC transceiver functionality. This example implementation helped us to explore the practical properties of the IC2IC serial interconnect. First, we verified the blocking capability of the link and second we analysed different reset conditions, such as disconnect and bit-error.
Mobile Agents and Processes using Communicating Process Architectures
Jon KERRIDGE, Jens-Oliver HASCHKE and Kevin CHALMERS, School of Computing, Napier University
 
Abstract. The mobile agent concept has been developed over a number of years and is widely accepted as one way of solving problems that require the achievement of a goal that cannot be serviced at a specific node in a network. The concept of a mobile process is less well developed because implicitly it requires a parallel environment within which to operate. In such a parallel environment a mobile agent can be seen as a specialization of a mobile process and both concepts can be incorporated into a single application environment, where both have well defined requirements, implementation and functionality. These concepts are explored using a simple application in which a node in a network of processors is required to undertake some processing of a piece of data for which it does not have the required process. It is known that the required process is available somewhere in the network. The means by which the required process is accessed and utilized is described. As a final demonstration of the capability we show how a mobile meeting organizer could be built that allows friends in a social network to create meetings using their mobile devices given that they each have access to the others’ on-line diaries.
Process-Oriented Collective Operations
John Markus BJØRNDALEN (a) and Adam T. SAMPSON (b),
(a) Department of Computer Science, University of Tromsø
(b) Computing Laboratory, University of Kent
 
Abstract. Distributing process-oriented programs across a cluster of machines requires careful attention to the effects of network latency. The MPI standard, widely used for cluster computation, defines a number of collective operations: efficient, reusable algorithms for performing operations among a group of machines in the cluster. In this paper, we describe our techniques for implementing MPI communication patterns in process-oriented languages, and how we have used them to implement collective operations in PyCSP and occam-pi on top of an asynchronous messaging framework. We show how to make use of collective operations in distributed processoriented applications. We also show how the process-oriented model can be used to increase concurrency in existing collective operation algorithms.
Representation and Implementation of CSP and VCR Traces
Neil BROWN (a) and Marc L. SMITH (b),
(a) Computing Laboratory, University of Kent
(b) Computer Science Department, Vassar College, Poughkeepsie, New York
 
Abstract. Communicating Sequential Processes (CSP) was developed around a formal algebra of processes and a semantics based on traces (and failures and divergences). A trace is a record of the events engaged in by a process. Several programming languages use, or have libraries to use, CSP mechanisms to manage their concurrency. Most of these lack the facility to record the trace of a program. A standard trace is a flat list of events but structured trace models are possible that can provide more information such as the independent or concurrent engagement of the process in some of its events. One such trace model is View-Centric Reasoning (VCR), which offers an additional model of tracing, taking into account the multiple, possibly imperfect views of a concurrent computation. This paper also introduces “structural” traces, a new type of trace that reflects the nested parallelism in a CSP system. The paper describes the automated generation of these three trace types in the Communicating Haskell Processes (CHP) library, using techniques which could easily be applied in other libraries such as JCSP and C++CSP2. The ability to present such traces of a concurrent program assists in understanding the behaviour of real CHP programs and for debugging when the trace behaviours are wrong. These ideas and tools promote a deeper understanding of the association between practicalities of real systems software and the underlying CSP formalism.
Prioritized Service Architecture: Refinement and Visual Design
Ian EAST, Department for Computing, Oxford Brookes University
 
Abstract. Concurrent/reactive systems can be designed free of deadlock using prioritized service architecture (PSA), subject to simple, statically verified, design rules. The Honeysuckle Design Language (HDL) enables such service-oriented design to be expressed purely in terms of communication, while affording a process-oriented implementation, using the Honeysuckle Programming Language (HPL). A number of enhancements to the service model for system abstraction are described, along with their utility. Finally, a new graphical counterpart to HDL (HVDL) is introduced that incorporates all these enhancements, and which facilitates interactive stepwise refinement.
CSPBuilder – CSP based Scientific Workflow Modeling
Rune Møllegård FRIBORG and Brian VINTER, Department of Computer Science, University of Copenhagen
 
Abstract. This paper introduces a framework for building CSP based applications, targeted for clusters and next generation CPU designs. CPUs are produced with several cores today and every next CPU generation will feature even more cores, resulting in a requirement for concurrency not previously demanded. The framework is CSP-presented as a scientific workflow model, specialized for scientific computing application. The purpose of the framework is to enable scientists to gain access to large parallel computation resources, which have been off limits because of the difficulty of concurrent programming using threads and locks.
Transfer Request Broker: Resolving Input-Output Choice
Oliver FAUST, Bernhard H.C. SPUTH and Alastair R. ALLEN, Department of Engineering, University of Aberdeen
 
Abstract. The refinement of a theoretical model which includes external choice over output and input of a channel transaction into an implementation model is a longstanding problem. In the theory of communicating sequential processes this type of external choice translates to resolving input and output guards. The problem arises from the fact that most implementation models incorporate only input guard resolution, known as alternation choice. In this paper we present the transaction request broker process which allows the designer to achieve external choice over channel ends by using only alternation. The resolution of input and output guards is refined into the resolution of input guards only. To support this statement we created two models. The first model requires resolving input and output guards to achieve the desired functionality. The second model incorporates the transaction request broker to achieve the same functionality by resolving only input guards.We use automated model checking to prove that both models are trace equivalent. The transfer request broker is a single entity which resolves the communication between multiple transmitter and receiver processes.
Modelling a Multi-Core Media Processor using JCSP
Anna KOSEK (a), Jon KERRIDGE (a) and Aly SYED (b)
(a) School of Computing, Napier University
(b) NXP Semiconductors Research, Eindhoven
 
Abstract. Manufacturers are creating multi-core processors to solve specialized problems. This kind of processor can process tasks faster by running them in parallel. This paper explores the usability of the Communicating Sequential Processes model to create a simulation of a multi-core processor aimed at media processing in hand-held mobile devices. Every core in such systems can have different capabilities and can generate different amounts of heat depending on the task being performed. Heat generated reduces the performance of the core. We have used mobile processes in JCSP to implement the allocation of tasks to cores based upon the work the core has done previously.

Abstracts – Fringe Presentations

Note: by the nature of the Fringe, the following list of presentations is provisional and incomplete. Following the conference, this list will be updated to reflect what actually happened!

Designing with Software Defined Silicon
Ali DIXON, XMOS Semiconductor
 
Abstract. This talk will introduce the XMOS XS1-G4 multi-core device and the associated development kit. The design tools and the XC language which can be used to write concurrent software, including direct access to physical input and output pins, will be presented. The concurrency support in XC has its roots in CSP and occam. The flexibility of the XS1 architecture will be shown by demonstrating a number of applications; these include interfacing, communications, motor control and media processing.
How to Make a Process Invisible
Neil C.C. BROWN, Computing Laboratory, University of Kent
 
Abstract. Sometimes it is useful to be able to invisibly splice a process into a channel, allowing it to observe (log or present to a GUI) communications on the channel without breaking the synchronous communication semantics. occam-pi's extended rendezvous when reading from a channel made this possible; the invisible process could keep the writer waiting until the real reader had accepted the forwarded communication. This breaks down when it is possible to have choice on outputs (also known as output guards). An extended rendezvous for writing to a channel fixes this aspect but in turn does not support choice on the input. It becomes impossible to keep your process invisible in all circumstances. This talk explains the problem, and proposes a radical new feature that would solve it.
Designing Animation Facilities for gCSP
Hans T.J. VAN DER STEEN, Marcel A. GROOTHUIS and Jan F. BROENINK, Control Engineering, Faculty EEMCS, University of Twente
 
Abstract. To improve feedback on how concurrent CSP-based programs run, the graphical CSP design tool (gCSP) has been extended with animation facilities. The state of processes, constructs, and channel ends are indicated with colours both in the gCSP diagrams and in the composition tree (hierarchical tree showing the structure of the total program). Furthermore, the contents of the channels are also shown. In this Fringe session, we will present and demonstrate this prototype animation facility, being the result of the MSc project of Hans van der Steen, and ask for feedback.
Tock: One Year On
Adam T. SAMPSON and Neil C.C. BROWN, Computing Laboratory, University of Kent
 
Abstract. Tock is a compiler for concurrent programming languages under development at the University of Kent. It translates occam-pi and Rain into portable, high-performance C or C++. It is implemented in Haskell using the nanopass approach, and aims to make it easy to experiment with new language and compiler features. Since our initial presentation of Tock at CPA 2007, we have added new frontends and backends, implemented a parallel usage checker based on the Omega test, improved the effectiveness of Tocks test suite, developed more efficient tree traversals using generic programming – and more besides! In this fringe session, we will describe our recent work on Tock, discuss our plans for the project, and show how it can be of use to other process-oriented programming researchers.
Introducing JCSP Networking 2.0
Kevin CHALMERS, School of Computing, Napier University
 
Abstract. The original implementation of JCSP Networking is based on the T9000 model of virtual channels across a communications mechanism, and can be considered sufficiently adequate for applications which are not resource constrained or liable to connection failure. However, work undertaken has revealed a number of limitations due to excessive resource usage, lack of sufficient error handling, reliance on Java serialization, and reliance on now deprecated features of JCSP. These problems reflect badly when considering JCSP Networking in a broader sense beyond the normal desktop. In this talk, a brief overview on how these problems have been overcome is presented. This will be followed by some tutorial examples on how to use JCSP Networking 2.0. This should be familiar to current JCSP Networking users, but new additions to the library should make it easier for novices to get started. The new underlying protocol is also presented, which should enable interoperability between various platforms beyond the Java desktop environment. The new version of JCSP Networking is currently available from the JCSP Subversion repository, under the Networking-2 branch. Details are available at http://www.cs.kent.ac.uk/projects/ofa/jcsp/.
Mobile Processes in an Ant Simulation
Eric BONNICI, Computing Laboratory, University of Kent
 
Abstract. The term self-organisation, or emergent behaviour, may be used to describe behaviour structures that emerge at the global level of a system due to the interactions between lower level components. Components of the system have no knowledge about global state; each component has only private internal data and data that it can observe from its immediate locality (such as environmental factors and the presence of other components). Resulting global phenomena are, therefore, an emergent property of the system as a whole. An implication of this when creating artificial systems is that we should not attempt to program such kinds of complex behaviour explicitly into the system. It may also help if the programmer approaches the design from a radically different perspective than that found in traditional methods of software engineering. This talk outlines a process-oriented approach, using massive fine-grained concurrency, and explores the use of occam-pi's mobile processes in the simulation of a classical ant colony.
Santa's Groovy Helper
Jon KERRIDGE, School of Computing, Napier University
 
Abstract. This talk is prompted by the paper on the Santa Claus problem, presented elsewhere in this conference by Jason Hurt and Matt Pedersen. A compact version of their solution, using the Groovy macro-extensions to Java and JCSP, will be shown. Listeners should first have attended the presentation of the referenced paper.
Santa Claus – with Mobile Reindeer and Elves
Peter H. WELCH (a) and Jan B. PEDERSEN (b),
(a) Computing Laboratory, University of Kent
(b) School of Computer Science, University of Nevada, Las Vegas
 
Abstract. Mobile processes, along with mobile channels, enable process networks to be dynamic: they may change their size (number of processes, channels, barriers) and shape (connection topology) as they run much like living organisms. One of the benefits is that all connections do not have to be established statically, in advance of when they are needed and open to abuse. In classical occam, care had to be taken by processes not to use channels when they were not in the right state to use them. With occam-pi mobiles, we can arrange that processes simply do not have those channels until they get into the right state – and not having such channels means that their misuse cannot even be expressed! Of course, it is a natural consequence of mobile system design that the arrivals of channels (or barriers or processes) are the very events triggering their exploitation. In our explorations so far with occam-pi, we have taken advantage of the mobility of data, channels and barriers and seen very good results. Very little work has been done with mobile processes: the ability to send and receive processes through channels, plug them into local networks, fire them up, stand them down and move them on again. This talk illustrates mobile process design through a solution to Trono's classical {\em Santa Claus Problem}. The reindeer and elves are modeled as mobile processes that move through holiday resorts, stables, work, waiting rooms, Santa's Grotto and back again. All those destinations are also processes – though static ones. As the reindeer and elves arrive at each stage, they plug in and do business. We will show the occam-pi mechanisms supporting mobile processes, confess to one weakness and consider remedies. The occam-pi solution did, of course, run correctly the first time it passed the stringent safety checks of the compiler and is available as open source (http://www.santaclausproblem.net).
Lego Robots using JCSP
Jon KERRIDGE, School of Computing, Napier University
 
Abstract. This talk will demonstrate Lego Mindstorms (TM) robots programmed using leJOS, JCSP and Java. It previews the presentation of the paper on JCSPre, later in the conference.
Handel-C Source Level Debugging
Herman ROEBBERS, TASS Software Professionals
 
Abstract. Until now, there has been no real source level debugger for Handel-C on the FPGA, such as we are used to having for standard CPUs. As the result of a student graduation project, we now have a possibility to do just that: setting/removing breakpoints, inspecting variables, etc. The talk will provide an impression of what has been achieved and looks a little into the future.
Towards Guaranteeing Process Oriented Program Behaviour
Fred BARNES, Computing Laboratory, University of Kent
 
Abstract. Though we have language guarantees for avoiding race-hazards, and design-rules and formal-methods for guaranteeing freedom from deadlock, livelock and starvation, the work involved in checking the latter typically discourages their use. This talk briefly examines a new approach to guaranteeing process behaviour in occam-pi, that removes most, if not all, of the leg-work involved in checking programs manually – a process that itself is error prone. Behaviour specifications are given in-program, that our experimental compiler checks against the actual implementation. Furthermore, the compiler is capable of generating the behavioural specification of any process, which it does using a CSP-like language, for use with separate compilation or for other formal verification.
PICOMS: Prioritised Inferred Choice Over Multiway Synchronisation
Doug WARREN, Computing Laboratory, University of Kent
 
Abstract. The ability to make a choice over multiway synchronisations (COMS) has always been an integral part of CSP. However, it is something that has been conspicuous by its absence from many concurrent languages, limiting their expressive power. Implementation of a 2-phase commit protocol to resolve such choice can result in large overheads, caused by synchronisation offers having to be withdrawn. The recent Oracle (single-phase) algorithm resolves COMS efficiently, for shared memory concurrency at least. However, the Oracle only deals with arbitrary choice and does not obviously extend to prioritised choice (where we assume the priorities of the participating processes are not in conflict). PICOMS is a proposed efficient method for resolving COMS that honours non-conflicting priorities, with only a modest increase in complexity over the Oracle method.

Pages © WoTUG, or the indicated author. All Rights Reserved.
Comments on these web pages should be addressed to: www at wotug.org