WoTUG - The place for concurrent processes

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 <i>arbitrary</i> choice and does
   not obviously extend to <i>prioritised</i>
   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\-&pi;, that removes most, if not all, of the
   leg\-work involved in checking programs manually &ndash;
   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 <i>client\-server</i> architectures,
   and, based on this, define a notion of
   <i>orthogonality</i> 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
   <i>components</i>, which provide some services
   to the environment, and require others from it. We identify
   the key notion of <i>composition</i> 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 <i>Cut
   rule</i>, a fundamental principle of logic, and that
   it can be enriched with a suitable notion of
   <i>behavioural types</i> 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
   <i>structured interfaces</i> 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 <i>names</i> (as in the
   &pi;\-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
   &mdash; a <i>fixed</i> 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.


%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) &mdash; 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 &mdash; the ownership rule
   &mdash; 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 &mdash; 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\-&pi;
%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\-&pi; 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\-&pi; 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 <i>pair of FIFO</i>
   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).


%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\-&pi;
%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\-&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,
   <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\-&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.


%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\-&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.


%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
   <i>process\-oriented language</i>, it is often
   introduced through a visual representation of programs in
   the form of <i>process network diagrams</i>.
   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
   <i>POPed</i>, 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\-&pi;\[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\-&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
   Tock\[rs]s test suite, developed more efficient tree
   traversals using generic programming &ndash; 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\-&pi;\[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\-&pi; mobiles, we can arrange that processes
   simply do not have those channels until they get into the
   right state &ndash; 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\[rs]s classical <i>Santa
   Claus Problem</i>. 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 &ndash;
   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 (<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.

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

Valid HTML 4.01!