Refer Proceedings details

%T Santa\[rs]s Groovy Helper
%A Jon Kerridge
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T Designing with Software Defined Silicon
%A A. Dixon
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T PICOMS: Prioritised Inferred Choice Over Multiway Synchronisation
%A Douglas N. Warren
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T Towards Guaranteeing Process Oriented Program Behaviour
%A Frederick R. M. Barnes
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T Handel\-C Source Level Debugging
%A Herman Roebbers
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T Lego Robots Using JCSP
%A Jon Kerridge
%E 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
%B Communicating Process Architectures 2008
%X This talk will demonstrate Lego Mindstorms (TM) robots
 programmed using leJOS, JCSP and Java. It previews the
 presentation of <q>JCSPre: the Robot Edition To
 Control LEGO NXT Robots</q> later in the conference.

%T Types, Orthogonality and Genericity: Some Tools for Communicating Process Architectures
%A Samson Abramsky
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T How to Soar with CSP
%A Colin O'Halloran
%E 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
%B Communicating Process Architectures 2008
%X 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: <ul> <li>a language subset for Soar,
 designed for formal analysis; <li>a formal model of
 the Soar subset written in CSP; <li>a prototype
 translator \[dq]Soar2Csp\[dq] from Soar to the CSP
 model; <li>a framework for static analysis of Soar
 agents through model checking using FDR2; <li>the
 identification of \[dq]healthiness conditions\[dq] required
 of any Soar Agent; <li>a verifiable implementation of
 the CSP based Soar agents on an FPGA. </ul>

%T A CSP Model for Mobile Channels
%A Peter H. Welch, Frederick R. M. Barnes
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T Communicating Scala Objects
%A Bernard Sufrin
%E 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
%B Communicating Process Architectures 2008
%X 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
 <q>poisoning</q> 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\[rs]s Actors library.

%T Combining EDF Scheduling with occam using the Toc Programming Language
%A Martin Korsgaard, Sverre Hendseth
%E 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
%B Communicating Process Architectures 2008
%X 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\[rs]s concurrency mechanisms,
 while fundamentally changing its concept of time. In Toc,
 deadlines are specified directly in code, replacing
 occam\[rs]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.

%T Communicating Haskell Processes: Composable Explicit Concurrency Using Monads
%A Neil C.C. Brown
%E 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
%B Communicating Process Architectures 2008
%X Writing concurrent programs in languages that lack explicit
 support for concurrency can often be awkward and difficult.
 Haskell\[rs]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.

%T Two\-Way Protocols for occam\-π
%A Adam T. Sampson
%E 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
%B Communicating Process Architectures 2008
%X In the occam\-π programming language, the
 client\-server communication pattern is generally
 implemented using a pair of unidirectional channels. While
 each channel\[rs]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\[rs]s session
 types. These mechanisms would considerably simplify the
 implementation of complex, dynamic client\-server systems.

%T Prioritized Service Architecture: Refinement and Visual Design
%A Ian R. East
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T Experiments in Translating CSP||B to Handel\-C
%A Steve Schneider, Helen Treharne, Alistair A. McEwan, Wilson Ifill
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T FPGA Based Control of a Production Cell System
%A Marcel A. Groothuis, Jasper J.P. Van Zuijlen, Jan F. Broenink
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T Shared\-Clock Methodology for Time\-Triggered Multi\-Cores
%A Keith F. Athaide, Michael J. Pont, Devaraj Ayavoo
%E 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
%B Communicating Process Architectures 2008
%X 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
 <q>shared\-clock</q>, 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.

%T Transfer Request Broker: Resolving Input\-Output Choice
%A Oliver Faust, Bernhard H.C. Sputh, Alastair R. Allen
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T Mechanical Verification of a Two\-Way Sliding Window Protocol
%A Bahareh Badban, Wan Fokkink, Jaco Van De Pol
%E 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
%B Communicating Process Architectures 2008
%X 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).

%T RRABP: Point\-to\-Point Communication over Unreliable Components
%A Bernhard H.C. Sputh, Oliver Faust, Alastair R. Allen
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T IC2IC: a Lightweight Serial Interconnect Channel for Multiprocessor Networks
%A Oliver Faust, Bernhard H.C. Sputh, Alastair R. Allen
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T Asynchronous Active Objects in Java
%A George Oprean, Jan Bækgaard Pedersen
%E 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
%B Communicating Process Architectures 2008
%X 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:
 <code>active</code>, <code>async</code>,
 <code>on</code> and
 <code>waitfor</code>. We have modified Sun\[rs]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

%T JCSPre: the Robot Edition To Control LEGO NXT Robots
%A Jon Kerridge, Alex Panayotopoulos, Patrick Lismore
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T A Critique of JCSP Networking
%A Kevin Chalmers, Jon Kerridge, Imed Romdhani
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T Virtual Machine Based Debugging for occam\-π
%A Carl G. Ritson, Jonathan Simpson
%E 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
%B Communicating Process Architectures 2008
%X 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,
 <q><code>printf</code> style</q>. 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.

%T Process\-Oriented Collective Operations
%A John Markus Bjørndalen, Adam T. Sampson
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T Representation and Implementation of CSP and VCR Traces
%A Neil C.C. Brown, Marc L. Smith
%E 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
%B Communicating Process Architectures 2008
%X 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 <q>structural</q> 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.

%T CSPBuilder \- CSP based Scientific Workflow Modeling
%A Rune Møllegard Friborg, Brian Vinter
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T Visual Process\-Oriented Programming for Robotics
%A Jonathan Simpson, Christian L. Jacobsen
%E 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
%B Communicating Process Architectures 2008
%X 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
 <q>processes first</q> 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.

%T Solving the Santa Claus Problem: a Comparison of Various Concurrent Programming Techniques
%A Jason Hurt, Jan Bækgaard Pedersen
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T Mobile Agents and Processes using Communicating Process Architectures
%A Jon Kerridge, Jens-Oliver Haschke, Kevin Chalmers
%E 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
%B Communicating Process Architectures 2008
%X 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\[rs] on\-line diaries.

%T YASS: a Scalable Sensornet Simulator for Large Scale Experimentation
%A Jonathan Tate, Iain Bate
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T Modelling a Multi\-Core Media Processor Using JCSP
%A Anna Kosek, Jon Kerridge, Aly Syed
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T How to Make a Process Invisible
%A Neil C.C. Brown
%E 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
%B Communicating Process Architectures 2008
%X 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\-π\[rs]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.

%T Designing Animation Facilities for gCSP
%A Hans T.J. van der Steen, Marcel A. Groothuis, Jan F. Broenink
%E 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
%B Communicating Process Architectures 2008
%X 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.

%T Tock: One Year On
%A Adam T. Sampson, Neil C.C. Brown
%E 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
%B Communicating Process Architectures 2008
%X 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\[rs]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.

%T Introducing JCSP Networking 2.0
%A Kevin Chalmers
%E 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
%B Communicating Process Architectures 2008
%X 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
 <tt>http://www.cs.kent.ac.uk/projects/ofa/jcsp/</tt>.

%T Mobile Processes in an Ant Simulation
%A Eric Bonnici
%E 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
%B Communicating Process Architectures 2008
%X 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\-π\[rs]s mobile processes in the simulation of
 a classical ant colony.

%T Santa Claus \- with Mobile Reindeer and Elves
%A Peter H. Welch, Jan Bækgaard Pedersen
%E 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
%B Communicating Process Architectures 2008
%X 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\[rs]s classical Santa
 Claus Problem. The reindeer and elves are modeled
 as mobile processes that move through holiday resorts,
 stables, work, waiting rooms, Santa\[rs]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 (<tt>http://www.santaclausproblem.net</tt>).

If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.

Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.