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