CPA 2008 - Programme

2008: YORK, UK

CPA Conference Programme

CoSMoS Workshop Programme

Keynote Presentations

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

Accepted Papers (Provisional)

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