Proceedings details
Title: Communicating Process Architectures 2008
Editors: Peter H. Welch, S. Stepney, F.A.C Polack, Frederick R. M. Barnes, Alistair A. McEwan, G. S. Stiles, Jan F. Broenink, Adam T. Sampson
Publisher: IOS Press, Amsterdam
ISBN: 978-1-58603-907-3
ISSN: 1383-7575
Keynote presentations
| Title: |
Types, Orthogonality and Genericity: Some Tools for Communicating Process Architectures
|
| Authors: |
Samson Abramsky |
| 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 π-calculus) to allow clients to bind dynamically to generic
instances of services. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF) |
| Title: |
How to Soar with CSP
|
| Authors: |
Colin O'Halloran |
| 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.
|
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Abstract (PDF) |
Papers
| Title: |
A CSP Model for Mobile Channels
|
| Authors: |
Peter H. Welch, Frederick R. M. Barnes |
| 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 π-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-π multiprocessing
language is built upon classical occam, whose design and semantics
are founded on CSP. To address the dynamics of complex systems,
occam-π 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-π systems using mobile channels and formal specification of
implementation mechanisms for mobiles used by the occam-π compiler
and run-time kernel. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF) |
| Title: |
Communicating Scala Objects
|
| Authors: |
Bernard Sufrin |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Combining EDF Scheduling with occam using the Toc Programming Language
|
| Authors: |
Martin Korsgaard, Sverre Hendseth |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF) |
| Title: |
Communicating Haskell Processes: Composable Explicit Concurrency Using Monads
|
| Authors: |
Neil C.C. Brown |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF) |
| Title: |
Two-Way Protocols for occam-π
|
| Authors: |
Adam T. Sampson |
| Abstract: |
In the occam-π 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-π compiler using Honda's session types. These mechanisms
would considerably simplify the implementation of complex, dynamic
client-server systems. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Prioritized Service Architecture: Refinement and Visual Design
|
| Authors: |
Ian R. East |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (Flash) |
| Title: |
Experiments in Translating CSP||B to Handel-C
|
| Authors: |
Steve Schneider, Helen Treharne, Alistair A. McEwan, Wilson Ifill |
| 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 CSP||B
specifications particularly appropriate to translation to Handel-C. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
FPGA Based Control of a Production Cell System
|
| Authors: |
Marcel A. Groothuis, Jasper J.P. Van Zuijlen, Jan F. Broenink |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF) |
| Title: |
Shared-Clock Methodology for Time-Triggered Multi-Cores
|
| Authors: |
Keith F. Athaide, Michael J. Pont, Devaraj Ayavoo |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Transfer Request Broker: Resolving Input-Output Choice
|
| Authors: |
Oliver Faust, Bernhard H.C. Sputh, Alastair R. Allen |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Mechanical Verification of a Two-Way Sliding Window Protocol
|
| Authors: |
Bahareh Badban, Wan Fokkink, Jaco Van De Pol |
| 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 μ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). |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF) |
| Title: |
RRABP: Point-to-Point Communication over Unreliable Components
|
| Authors: |
Bernhard H.C. Sputh, Oliver Faust, Alastair R. Allen |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF) |
| Title: |
IC2IC: a Lightweight Serial Interconnect Channel for Multiprocessor Networks
|
| Authors: |
Oliver Faust, Bernhard H.C. Sputh, Alastair R. Allen |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF) |
| Title: |
Asynchronous Active Objects in Java
|
| Authors: |
George Oprean, Jan Bækgaard Pedersen |
| 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 |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
JCSPre: the Robot Edition To Control LEGO NXT Robots
|
| Authors: |
Jon Kerridge, Alex Panayotopoulos, Patrick Lismore |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
A Critique of JCSP Networking
|
| Authors: |
Kevin Chalmers, Jon Kerridge, Imed Romdhani |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Virtual Machine Based Debugging for occam-π
|
| Authors: |
Carl G. Ritson, Jonathan Simpson |
| 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-π 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-π applications, based on the Transterpreter virtual machine
interpreter. By adding a set of extensions to the Transterpreter,
we give occam-π 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-π by mediating
the execution of one execution process from another. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF) |
| Title: |
Process-Oriented Collective Operations
|
| Authors: |
John Markus Bjørndalen, Adam T. Sampson |
| 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-π 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Representation and Implementation of CSP and VCR Traces
|
| Authors: |
Neil C.C. Brown, Marc L. Smith |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF) |
| Title: |
CSPBuilder - CSP based Scientific Workflow Modeling
|
| Authors: |
Rune Møllegard Friborg, Brian Vinter |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF) |
| Title: |
Visual Process-Oriented Programming for Robotics
|
| Authors: |
Jonathan Simpson, Christian L. Jacobsen |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF) |
| Title: |
Solving the Santa Claus Problem: a Comparison of Various Concurrent Programming Techniques
|
| Authors: |
Jason Hurt, Jan Bækgaard Pedersen |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
Mobile Agents and Processes using Communicating Process Architectures
|
| Authors: |
Jon Kerridge, Jens-Oliver Haschke, Kevin Chalmers |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
| Title: |
YASS: a Scalable Sensornet Simulator for Large Scale Experimentation
|
| Authors: |
Jonathan Tate, Iain Bate |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF) |
| Title: |
Modelling a Multi-Core Media Processor Using JCSP
|
| Authors: |
Anna Kosek, Jon Kerridge, Aly Syed |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Paper (PDF), Slides (PDF) |
Fringe presentations
| Title: |
How to Make a Process Invisible
|
| Authors: |
Neil C.C. Brown |
| 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-π'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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Abstract (PDF) |
| Title: |
Designing Animation Facilities for gCSP
|
| Authors: |
Hans T.J. van der Steen, Marcel A. Groothuis, Jan F. Broenink |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Abstract (PDF) |
| Title: |
Tock: One Year On
|
| Authors: |
Adam T. Sampson, Neil C.C. Brown |
| Abstract: |
Tock is a compiler for concurrent programming languages under
development at the University of Kent. It translates occam-π 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 Tock's 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Abstract (PDF), Slides (PDF) |
| Title: |
Introducing JCSP Networking 2.0
|
| Authors: |
Kevin Chalmers |
| 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/. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Abstract (PDF), Slides (PDF) |
| Title: |
Mobile Processes in an Ant Simulation
|
| Authors: |
Eric Bonnici |
| 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-π's mobile processes
in the simulation of a classical ant colony. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Abstract (PDF) |
| Title: |
Santa Claus - with Mobile Reindeer and Elves
|
| Authors: |
Peter H. Welch, Jan Bækgaard Pedersen |
| 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-π 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-π, 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 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-π mechanisms supporting mobile processes, confess to
one weakness and consider remedies. The occam-π 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). |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Slides (PDF), Slides (PowerPoint) |
| Title: |
Lego Robots Using JCSP
|
| Authors: |
Jon Kerridge |
| Abstract: |
This talk will demonstrate Lego Mindstorms (TM) robots programmed
using leJOS, JCSP and Java. It previews the presentation of
JCSPre: the Robot Edition To Control LEGO NXT Robots later in
the conference. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Slides (PDF) |
| Title: |
Handel-C Source Level Debugging
|
| Authors: |
Herman Roebbers |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Slides (PDF) |
| Title: |
Towards Guaranteeing Process Oriented Program Behaviour
|
| Authors: |
Frederick R. M. Barnes |
| 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-π, 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Title: |
PICOMS: Prioritised Inferred Choice Over Multiway Synchronisation
|
| Authors: |
Douglas N. Warren |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Title: |
Designing with Software Defined Silicon
|
| Authors: |
A. Dixon |
| 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Title: |
Santa's Groovy Helper
|
| Authors: |
Jon Kerridge |
| Abstract: |
This talk is prompted by the work 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. |
| Bibliography: |
Web page:BibTEX,
Refer
Plain text: BibTEX,
Refer
|
| Files: | Slides (PDF) |
|
