WoTUG - CPA 2007

CPA 2007 Accepted papers and abstracts

27 out of 56 submissions to the conference have been accepted into the conference programme, for publication in the proceedings. The full conference programme is given below.

CPA 2007 Programme and events

Sunday / July 8, 2007
17:00	Registration (Oak Suite)
18:00	Buffet dinner (Oak Suite)
20:00	Fringe Session I (Oak Suite)
Monday / July 09, 2007
08:15	Registration
Session 1	Chair: Steve Schneider
08:50	Welcome
09:00	Fine-grain concurrency Tony HOARE, Microsoft Research, Cambridge.
10:00	Lazy Exploration and Checking of CSP Models with CSPsim Phillip J. BROOKE(a) and Richard F. PAIGE(b), (a)School of Computing, University of Teesside, U.K. (b)Department of Computer Science, University of York, U.K.
10:30	Coffee break
Session 2	Chair: Neil Evans
11:00	Hardware/Software Synthesis and Verification Using Esterel Satnam SINGH, Microsoft Research, Cambridge, CB3 0FB, United Kingdom.
11:30	A Step Towards Refining and Translating B Control Annotations to Handel-C Wilson IFILL(a), and Steve SCHNEIDER(b), (a)AWE Aldermaston, Reading, Berks, England; (b)Department of Computing, University of Surrey, Guildford, Surrey, England.
12:00	A Process Oriented Approach to USB Driver Development Carl G. RITSON and Frederick R.M. BARNES, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NF, England.
12:30	Lunch (Lakeside Restaurant)
Session 3	Chair: Jon Kerridge
14:00	The Core Language of Aldwych Matthew HUNTBACH, Department of Computer Science, Queen Mary University of London, Mile End Road, London E1 4NS, UK.
14:30	Concurrent/Reactive System Design with Honeysuckle Ian EAST, Dept. for Computing, Oxford Brookes University, Oxford OX33 1HX, England.
15:00	CSP and Real-Time: Reality or Illusion? Bojan ORLIC and Jan F. BROENINK, Control Engineering, Faculty of EE-Math-CS, University of Twente P.O.Box 217, 7500AE Enschede, the Netherlands.
15:30	Coffee break
Session 4	Chair: Wilson Ifill
16:00	Advanced System Simulation, Emulation and Test (ASSET) Gregory L. WICKSTROM, Sandia National Laboratories, Albuquerque NM, USA.
16:30	Towards the Formal Verification of a Java Processor in Event-B Neil GRANT and Neil EVANS, AWE, Aldermaston, UK.
17:00	Modeling and Analysis of the AMBA Bus Using CSP and B Alistair A. McEWAN and Steve SCHNEIDER, University of Surrey, U.K..
19:00	Dinner (Oak Suite)
20:00	Fringe Session II (Oak Suite)
Tuesday / July 10, 2007
Session 1	Chair: Peter Welch
09:00	Communicating Process Architectures for Multicores David MAY, University of Bristol.
10:00	Development of a Family of Multi-Core Devices Using Hierarchical Abstraction Andrew DULLER 1, Alan GRAY, Daniel TOWNER, Jamie ILES, Gajinder PANESAR, and Will ROBBINS, (a)School of Computing, University of Teesside, U.K. (b)picoChip Designs Ltd., Bath, UK.
10:30	Coffee break
Session 2	Chair: Alistair McEwan
11:00	A Reconfigurable System-on-Chip Architecture for Pico-Satellite Missions Tanya VLADIMIROVA and Xiaofeng WU, Surrey Space Centre Department of Electronic Engineering University of Surrey, Guildford, GU2 7XH, UK.
11:30	Domain Specific Transformations for Hardware Ray Tracing Tim TODMAN and Wayne LUK, Imperial College, London, U.K.
12:00	trancell - an Experimental ETC to Cell BE Translator Ulrik SCHOU J.RGENSEN and Espen SUENSON, Department of Computer Science, University of Copenhagen, Universitetsparken 1, 2100 Kbh. ., Denmark.
12:30	Lunch (Management School)
Session 3	Chair: Jan Broenink
14:00	JCSProB: Implementing Integrated Formal Specifications in Concurrent Java Letu YANG and Michael R. POPPLETON, Dependable Systems and Software Engineering, Electronics and Computer Science, University of Southampton, Southampton, SO17 1BJ, UK.
14:30	Integrating and Extending JCSP Peter WELCH(a), Neil BROWN(a), James MOORES(b), Kevin CHALMERS(c) and Bernhard SPUTH(d), School of Computing, Napier University, Edinburgh, EH10 5DT.
15:00	Mobility in JCSP: New Mobile Channel and Mobile Process Models Kevin CHALMERS, Jon KERRIDGE, and Imed ROMDHANI, School of Computing, Napier University, Edinburgh, EH10 5DT.
15:30	Coffee break
Session 4	Chair: Bill Gardner
16:00	Testing and Sampling Parallel Systems Jon KERRIDGE, School of Computing, Napier University, Edinburgh, EH10 5DT.
16:30	Design Principles of the SystemCSP Software Framework Bojan ORLIC, Jan F. BROENINK, Control Engineering, Faculty of EE-Math-CS, University of Twente P.O.Box 217, 7500AE Enschede, the Netherlands.
17:00	Components with Symbolic Transition Systems: a Java Implementation of Rendezvous Fabricio FERNANDES, Robin PASSAMA and Jean-Claude ROYER, OBASCO Group, . Ecole des Mines de Nantes INRIA, LINA 4 rue Alfred Kastler, 44307 Nantes cedex 3, France.
19:00	Conference Dinner (Lakeside Restaurant)
21.30	Annual exhumation of dead parrot joke (Lakeside Restaurant)
Wednesday / July 11, 2007
Session 1	Chair: Roger Peel
09:00	A Process-Oriented Architecture for Complex System Modelling Carl G. RITSON and Peter H. WELCH, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NF, England.
09:30	C++CSP2: A Many-to-Many Threading Model for Multicore Architectures Neil BROWN, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NF, UK.
10:00	Concurrency Control and Recovery Management for Open e-Business Transactions Amir R. RAZAVI, Sotiris K. MOSCHOYIANNIS and Paul J. KRAUSE, Department of Computing, School of Electronics and Physical Sciences, University of Surrey, Guildford, Surrey, GU2 7XH, UK.
10:30	Coffee break
Session 2	Chair: Barry Cook
11:00	PyCSP - Communicating Sequential Processes for Python John Markus BJ.RNDALEN(a), Brian VINTER(b) and Otto ANSHUS(a), (a)Department of Computer Science, University of Troms., (b)Department of Computer Science, University of Copenhagen.
11:30	A Versatile Hardware-Software Platform for In-Situ Monitoring Systems Bernhard H. C. SPUTH, Oliver FAUST, and Alastair R. ALLEN, Department of Engineering, University of Aberdeen, Aberdeen AB24 3UE, UK.
12:00	A Native Transterpreter for the LEGO Mindstorms RCX Jonathan SIMPSON, Christian L. JACOBSEN and Matthew C. JADUD, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NZ, England.
12:30	Wotug AGM and closing remarks Peter WELCH, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NZ, England.
13:00	Lunch (Management School)

Invited papers

Fine-grain concurrency: Professor Sir Tony Hoare, Microsoft Research, Cambridge

I have been interested in concurrent programming since about 1963, when its associated problems contributed to the failure of the largest software project that I have managed. When I moved to an academic career in 1968, I hoped that I could find a solution to the problems by my research. Quite quickly I decided to concentrate on coarse-grained concurrency, which does not allow concurrent processes to share main memory. The only interaction between processes is confined to explicit input and output commands. This simplification led eventually to the exploration of the theory of Communicating Sequential Processes.

Since joining Microsoft Research in 1999, I have plucked up courage at last to look at fine-grain concurrency, involving threads which interleave their access to main memory at the fine granularity of single instruction execution. By combining the merits of a number of different theories of concurrency, one can paint a relatively simple picture of a theory for the correct design of concurrent systems. Indeed, pictures are a great help in conveying the basic understanding. This paper presents some on-going directions of research that I have been pursuing with colleagues in Cambridge -- both at Microsoft Research and in the University Computing Laboratory.

Communicating Process Architectures for Multicores: Professor David May, University of Bristol

Communicating process architecture can be used to build efficient multicore chips scaling to hundreds of processors. Concurrent processing, communications and input-output are supported directly by the instruction set of the cores and by the protocol used in the on-chip interconnect. Concurrent programs are compiled directly to the chip exploiting novel compiler optimisations. The architecture supports a variety of programming techniques, ranging from statically configured process networks to dynamic reconfiguration and mobile processes.

Regular Papers

Concurrent/Reactive System Design with Honeysuckle, Ian EAST, Dept. for Computing, Oxford Brookes University, Oxford OX33 1HX, England (Abstract).
The Core Language of Aldwych,Matthew HUNTBACH,Department of Computer Science, Queen Mary University of London, Mile End Road, London E1 4NS, UK (Abstract).
CSP and Real-Time: Reality or Illusion?, Bojan ORLIC and Jan F. BROENINK,Control Engineering, Faculty of EE-Math-CS, University of Twente P.O.Box 217, 7500AE Enschede, the Netherlands (Abstract).
Design Principles of the SystemCSP Software Framework, Bojan ORLIC, Jan F. BROENINK, Control Engineering, Faculty of EE-Math-CS, University of Twente P.O.Box 217, 7500AE Enschede, the Netherlands (Abstract).
Testing and Sampling Parallel Systems, Jon KERRIDGE, School of Computing, Napier University, Edinburgh, EH10 5DT (Abstract).
Mobility in JCSP: New Mobile Channel and Mobile Process Models, Kevin CHALMERS, Jon KERRIDGE, and Imed ROMDHANI, School of Computing, Napier University, Edinburgh, EH10 5DT (Abstract).
Integrating and Extending JCSP, Peter WELCH(a), Neil BROWN(a), James MOORES(b), Kevin CHALMERS(c) and Bernhard SPUTH(d)(a)Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NF, UK. (b)23 Tunnel Avenue, London, SE10 0SF, UK. (c)School of Computing, Napier University, Edinburgh, EH10 5DT, UK. (d)Department of Engineering, University of Aberdeen, Scotland, AB24 3UE, UK. (Abstract).
JCSProB: Implementing Integrated Formal Specifications in Concurrent Java, Letu YANG and Michael R. POPPLETON, Dependable Systems and Software Engineering, Electronics and Computer Science, University of Southampton, Southampton, SO17 1BJ, UK. (Abstract).
trancell - an Experimental ETC to Cell BE Translator, Ulrik SCHOU J.RGENSEN and Espen SUENSON, Department of Computer Science, University of Copenhagen, Universitetsparken 1, 2100 Kbh. ., Denmark. (Abstract).
Lazy Exploration and Checking of CSP Models with CSPsim, Phillip J. BROOKE(a) and Richard F. PAIGE(b)(a)School of Computing, University of Teesside, U.K. (b)Department of Computer Science, University of York, U.K. (Abstract).
Components with Symbolic Transition Systems: a Java Implementation of Rendezvous, Fabricio FERNANDES, Robin PASSAMA and Jean-Claude ROYER, OBASCO Group, . Ecole des Mines de Nantes INRIA, LINA 4 rue Alfred Kastler, 44307 Nantes cedex 3, France. (Abstract).
C++CSP2: A Many-to-Many Threading Model for Multicore Architectures, Neil BROWN, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NF, UK. (Abstract).
PyCSP - Communicating Sequential Processes for Python, John Markus BJ.RNDALEN(a), Brian VINTER(b) and Otto ANSHUS(a), (a)Department of Computer Science, University of Troms., (b)Department of Computer Science, University of Copenhagen (Abstract).
A Process-Oriented Architecture for Complex System Modelling, Carl G. RITSON and Peter H. WELCH, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NF, England. (Abstract).
Concurrency Control and Recovery Management for Open e-Business Transactions, Amir R. RAZAVI, Sotiris K. MOSCHOYIANNIS and Paul J. KRAUSE, Department of Computing, School of Electronics and Physical Sciences, University of Surrey, Guildford, Surrey, GU2 7XH, UK. (Abstract).
High Cohesion and Low Coupling: the Office Mapping Factor, .yvind TEIG, Autronica Fire and Security (A UTC Fire and Security company) Trondheim, Norway (Abstract).
A Process Oriented Approach to USB Driver Development, Carl G. RITSON and Frederick R.M. BARNES, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NF, England. (Abstract).
A Native Transterpreter for the LEGO Mindstorms RCX, Jonathan SIMPSON, Christian L. JACOBSEN and Matthew C. JADUD, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NZ, England. (Abstract).

Codesign Papers

Modeling and Analysis of the AMBA Bus Using CSP and B, Alistair A. McEWAN and Steve SCHNEIDER, University of Surrey, U.K. (Abstract).
A Step Towards Refining and Translating B Control Annotations to Handel-C, Wilson IFILL(a), and Steve SCHNEIDER(b), (a)AWE Aldermaston, Reading, Berks, England; (b)Department of Computing, University of Surrey, Guildford, Surrey, England. (Abstract).
Towards the Formal Verification of a Java Processor in Event-B, Neil GRANT and Neil EVANS, AWE, Aldermaston, UK. (Abstract).
Advanced System Simulation, Emulation and Test (ASSET), Gregory L. WICKSTROM, Sandia National Laboratories, Albuquerque NM, USA (Abstract).
Development of a Family of Multi-Core Devices Using Hierarchical Abstraction, Andrew DULLER 1, Alan GRAY, Daniel TOWNER, Jamie ILES, Gajinder PANESAR, and Will ROBBINSpicoChip Designs Ltd., Bath, UK (Abstract).
Hardware/Software Synthesis and Verification Using Esterel, Satnam SINGH, Microsoft Research, Cambridge, CB3 0FB, United Kingdom (Abstract).
Domain Specific Transformations for Hardware Ray Tracing, Tim TODMAN and Wayne LUK, Imperial College, London, U.K. (Abstract).
A Reconfigurable System-on-Chip Architecture for Pico-Satellite Missions, Tanya VLADIMIROVA and Xiaofeng WU, Surrey Space Centre Department of Electronic Engineering University of Surrey, Guildford, GU2 7XH, UK (Abstract).
A Versatile Hardware-Software Platform for In-Situ Monitoring Systems, Bernhard H. C. SPUTH, Oliver FAUST, and Alastair R. ALLEN, Department of Engineering, University of Aberdeen, Aberdeen AB24 3UE, UK, UK (Abstract).

Abstracts

Concurrent/Reactive System Design with Honeysuckle Ian EASTDept. for Computing, Oxford Brookes University, Oxford OX33 1HX, England
	Abstract. Honeysuckle is a language in which to describe systems with prioritized service architecture (PSA), whereby processes communicate values and (mobile) objects deadlock-free under client-server protocol. A novel syntax for the description of service (rather than process) composition is presented and the relation to implementation discussed. In particular, the proper separation of design and implementation becomes possible, allowing independent abstraction and verification.
Top
The Core Language of Aldwych Matthew HUNTBACH, Department of Computer Science, Queen Mary University of London, Mile End Road, London E1 4NS, UK
	Abstract. Aldwych is a general purpose programming language which we have developed in order to provide a mechanism for practical programming which can be thought of in an inherently concurrent way. We have described Aldwych elsewhere in terms of a translation to a concurrent logic language. However, it would be more accurate to describe it as translating to a simple operational language which, while able to be represented in a logic-programming like syntax, has lost much of the baggage associated with logic programming . This language is only a little more complex than foundational calculi such as the pi-calculus. Its key feature is that all variables are moded with a single producer, and some are linear allowing a reversal of polarity and hence interactive communication.
Top
CSP and Real-Time: Reality or Illusion? Bojan ORLIC and Jan F. BROENINK, Control Engineering, Faculty of EE-Math-CS, University of Twente P.O.Box 217, 7500AE Enschede, the Netherlands
	Abstract. This paper deals with the applicability of CSP in general and SystemCSP, as a notation and design methodology based on CSP, in particular in the application area of real-time systems. The paper extends SystemCSP by introducing time-related operators as a way to specify time properties. Since SystemCSP aims to be used in practice of real-time systems development, achieving real-time in practice is also addressed. The mismatch between the classical scheduling theories and CSP paradigm is explored. Some practical ways to deal with this mismatch are presented.
Top
Design Principles of the SystemCSP Software Framework Bojan ORLIC, Jan F. BROENINK, Control Engineering, Faculty of EE-Math-CS, University of Twente P.O.Box 217, 7500AE Enschede, the Netherlands
	Abstract. SystemCSP is a graphical design specification language aimed to serve as a basis for the specification of formally verifiable component-based designs. This paper defines a mapping from SystemCSP designs to a software implementation. The possibility to reuse existing practical implementations was analyzed. Comparison is given for different types of execution engines usable in implementing concurrent systems. The main part of the text introduces and explains the design principles behind the software implementation. A synchronization mechanism is introduced that can handle CSP kind of events with event ends possibly scattered on different nodes and OS threads, and with any number of participating event ends, possibly guarded by alternative constructs.
Top
Testing and Sampling Parallel Systems Jon KERRIDGE, School of Computing, Napier University, Edinburgh, EH10 5DT
	Abstract. The testing of systems using tools such as JUnit is well known to the sequential programming community. It is perhaps less well known to the parallel computing community because it relies on systems terminating so that system outputs can be compared with expected outputs. A highly parallel architecture is described that allows the JUnit testing of non-terminating MIMD process based parallel systems. The architecture is then extended to permit the sampling of a continuously running system. It is shown that this can be achieved using a small number of additional components that can be easily modified to suit a particular sampling situation. The system architectures are presented using a Groovy implementation of the JCSP and JUnit packages.
Top
Mobility in JCSP: New Mobile Channel and Mobile Process Models Kevin CHALMERS, Jon KERRIDGE, and Imed ROMDHANI School of Computing, Napier University, Edinburgh, EH10 5DT
	Abstract. The original package developed for network mobility in JCSP, although useful, revealed some limitations in the underlying models permitting code mobility and channel migration. In this paper, we discuss these limitations, as well as describe the new models developed to overcome them. The models are based on two different approaches to mobility in other fields, mobile agents and Mobile IP, providing strong underlying constructs to build upon, permitting process and channel mobility in networked JCSP systems in a manner that is transparent to the user.
Top
Integrating and Extending JCSP Peter WELCH(a), Neil BROWN(a), James MOORES(b), Kevin CHALMERS(c) and Bernhard SPUTH(d), (a)Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NF, UK. (b) 23 Tunnel Avenue, London, SE10 0SF, UK. (c) School of Computing, Napier University, Edinburgh, EH10 5DT, UK. (d)Department of Engineering, University of Aberdeen, Scotland, AB24 3UE, UK.
	Abstract. This paper presents the extended and re-integrated JCSP library of CSP packages for Java. It integrates the differing advances made by Quickstone s JCSP Network Edition and the core library maintained at Kent. A more secure API for connecting networks and manipulating channels is provided, requiring signifi- cant internal re-structuring. This mirrors developments in the occam-pi language for mandated direction specifiers on channel-ends. For JCSP, promoting the concept of channel-ends to first-class entities has both semantic benefit (the same as for occampi) and increased safety. Major extensions include alting barriers (classes supporting external choice over multiple multi-way synchronisations), channel output guards (straightforward once we have the alting barriers), channel poisoning (for the safe and simple termination of networks or sub-networks) and extended rendezvous on channel communications (that simplify the capture of several useful synchronisation design patterns). Almost all CSP systems can now be directly captured with the new JCSP. The new library is available under the LGPL open source license.
Top
JCSProB: Implementing Integrated Formal Specifications in Concurrent Java Letu YANG and Michael R. POPPLETON, Dependable Systems and Software Engineering, Electronics and Computer Science, University of Southampton, Southampton, SO17 1BJ, UK.
	Abstract. The ProB model checker provides tool support for an integrated formal specification approach, combining the classical state-based B language with the eventbased process algebra CSP. In this paper, we present a developing strategy for implementing such a combined ProB specification as a concurrent Java program. A Java implementation of the combined B and CSP model has been developed using a similar approach to JCSP. A set of translation rules relates the formal model to its Java implementation, and we also provide a translation tool JCSProB to automatically generate a Java program from a ProB specification. To demonstrate and exercise the tool, several B/CSP models, varying both in syntactic structure and behavioural/concurrency properties, are translated by the tool. The models manifest the presence and absence of various safety, deadlock, and bounded fairness properties; the generated Java code is shown to faithfully reproduce them. Run-time safety and bounded fairness checking is also demonstrated. The Java programs are discussed to demonstrate our implementation of the abstract B/CSP concurrencymodel in Java. In conclusion we consider the effectiveness and generality of the implementation strategy.
Top
trancell - an Experimental ETC to Cell BE Translator Ulrik SCHOU J.RGENSEN and Espen SUENSON, Department of Computer Science, University of Copenhagen, Universitetsparken 1, 2100 Kbh. ., Denmark.
	Abstract. This paper describes trancell, a translator and associated runtime environment that allows programs written in the occam programming language to be run on the Cell BE microarchitecture. trancell cannot stand alone, but requires the front end from the KRoC/Linux compiler for generating Extended Transputer Code (ETC), which is then translated into native Cell SPU assembly code and linked with the trancell runtime. The paper describes the difficulties in implementing occam on the Cell, notably the runtime support required for implementing channel communications and true parallelism. Various benchmarks are examined to investigate the success of the approach.
Top
Lazy Exploration and Checking of CSP Models with CSPsim Phillip J. BROOKE(a) and Richard F. PAIGE(b), (a) School of Computing, University of Teesside, U.K. (b)Department of Computer Science, University of York, U.K.
	Abstract. We have recently constructed a model, and carried out an analysis, of a concurrent extension to an object-oriented language at a level of abstraction above threads. The model was constructed in CSP. We subsequently found that existing CSP tools were unsuitable for reasoning about and analysing this model, so it became necessary to create a new tool to handle CSP models: CSPsim. We describe this tool, its capabilities and algorithms, and compare it with the related tools, FDR2 and ProBE. We illustrate CSPsim s usage with examples from the model. The tool s on-the-fly construction of successor states is important for exhaustive and non-exhaustive state exploration. Thus we found CSPsim to be particularly useful for parallel compositions of components with infinite states that reduce to finite-state systems.
Top
Components with Symbolic Transition Systems: a Java Implementation of Rendezvous Fabricio FERNANDES, Robin PASSAMA and Jean-Claude ROYER, OBASCO Group, . Ecole des Mines de Nantes INRIA, LINA 4 rue Alfred Kastler, 44307 Nantes cedex 3, France.
	Abstract. Component-based software engineering is becoming an important approach for system development. A crucial issue is to fill the gap between high-level models, needed for design and verification, and implementation. This paper introduces first a component model with explicit protocols based on symbolic transition systems. It then presents a Java implementation for it that relies on a rendezvous mechanism to synchronize events between component protocols. This paper shows how to get a correct implementation of a complex rendezvous in presence of full data types, guarded transitions and, possibly, guarded receipts.
Top
C++CSP2: A Many-to-Many Threading Model for Multicore Architectures Neil BROWN, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NF, UK.
	Abstract. The advent of mass-market multicore processors provides exciting new opportunities for parallelism on the desktop. The original C++CSP a library providing concurrency in C++ used only user-threads, which would have prevented it taking advantage of this parallelism. This paper details the development of C++CSP2, which has been built around a many-to-many threading model that mixes user-threads and kernel-threads, providing maximum flexibility in taking advantage of multicore and multi-processormachines. New and existing algorithms are described for dealing with the run-queue and implementing channels, barriers and mutexes. The latter two are benchmarked to motivate the choice of algorithm.Most of these algorithms are based on the use of atomic instructions, to gain maximal speed and efficiency. Other issues related to the new design and related to implementing concurrency in a language like C++ that has no direct support for it, are also described. The C++CSP2 library will be publicly released under the LGPL before CPA 2007.
Top
PyCSP - Communicating Sequential Processes for Python John Markus BJ.RNDALEN(a), Brian VINTER(b) and Otto ANSHUS(a) (a)Department of Computer Science, University of Troms., (b)Department of Computer Science, University of Copenhagen
	Abstract. The Python programming language is effective for rapidly specifying programs and experimenting with them. It is increasingly being used in computational sciences, and in teaching computer science. CSP is effective for describing concurrency. It has become especially relevant with the emergence of commodity multi-core architectures. We are interested in exploring how a combination of Python and CSP can benefit both the computational sciences and the hands-on teaching of distributed and parallel computing in computer science. To make this possible, we have developed PyCSP, a CSP library for Python. PyCSP presently supports the core CSP abstractions. We introduce the PyCSP library, its implementation, a few performance benchmarks, and show example code using PyCSP. An early prototype of PyCSP has been used in this year s Extreme Multiprogramming Class at the CS department, university of Copenhagen with promising results.
Top
A Process-Oriented Architecture for Complex System Modelling Carl G. RITSON and Peter H. WELCH, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NF, England.
	Abstract. A fine-grained massively-parallel process-oriented model of platelets (potentially artificial) within a blood vessel is presented. This is a CSP inspired design, expressed and implemented using the occam-pi language. It is part of the TUNA pilot study on nanite assemblers at the universities of York, Surrey and Kent. The aim for this model is to engineer emergent behaviour fromthe platelets, such that they respond to a wound in the blood vessel wall in a way similar to that found in the human body i.e. the formation of clots to stem blood flow from the wound and facilitate healing. An architecture for a three dimensional model (relying strongly on the dynamic and mobile capabilities of occam-pi) is given, along with mechanisms for visualisation and interaction. The biological accuracy of the current model is very approximate. However, its process-oriented nature enables simple refinement (through the addition of processes modelling different stimulants/inhibitors of the clotting reaction, different platelet types and other participating organelles) to greater and greater realism. Even with the current system, simple experiments are possible and have scientific interest (e.g. the effect of platelet density on the success of the clotting mechanism in stemming blood flow: too high or too low and the process fails). General principles for the design of large and complex system models are drawn. The described case study runs to millions of processes engaged in ever-changing communication topologies. It is free from deadlock, livelock, race hazards and starvation by design, employing a small set of synchronisation patterns for which we have proven safety theorems.
Top
Concurrency Control and Recovery Management for Open e-Business Transactions Amir R. RAZAVI, Sotiris K. MOSCHOYIANNIS and Paul J. KRAUSE, Department of Computing, School of Electronics and Physical Sciences, University of Surrey, Guildford, Surrey, GU2 7XH, UK.
	Abstract. Concurrency control mechanisms such as turn-taking, locking, serialization, transactional locking mechanism, and operational transformation try to provide data consistency when concurrent activities are permitted in a reactive system. Locks are typically used in transactional models for assurance of data consistency and integrity in a concurrent environment. In addition, recovery management is used to preserve atomicity and durability in transaction models. Unfortunately, conventional lock mechanisms severely (and intentionally) limit concurrency in a transactional environment. Such lock mechanisms also limit recovery capabilities. Finally, existing recovery mechanisms themselves afford a considerable overhead to concurrency. This paper describes a new transaction model that supports release of early results inside and outside of a transaction, decreasing the severe limitations of conventional lock mechanisms, yet still warranties consistency and recoverability of released resources (results). This is achieved through use of a more flexible locking mechanism and by using two types of consistency graph. This provides an integrated solution for transaction management, recovery management and concurrency control. We argue that these are necessary features for management of long-term transactions within digital ecosystems of small to medium enterprises
Top
High Cohesion and Low Coupling: the Office Mapping Factor .yvind TEIG, Autronica Fire and Security (A UTC Fire and Security company) Trondheim, Norway
	Abstract. This case observation describes how an embedded industrial software architecture was mapped onto an office layout. It describes a particular type of program architecture that does this mapping rather well. The more a programmer knows what to do, and so may withdraw to his office and do it, the higher the cohesion or completeness. The less s/he has to know about what is going on in other offices, the lower the coupling or disturbance. The project, which made us aware of this, was an embedded system built on the well-known process data-flow architecture. All interprocess communication that carried data was on synchronous, blocking channels. In this programming paradigm, it is possible for a process to refuse to listen on a channel while it is busy doing other things. We think that this in a way corresponds to closing the door to an office. When another process needs to communicate with such a process, it will simply be blocked (and descheduled). No queuing is done. The process, or the programmer, need not worry about holding up others. The net result seems to be good isolation of work and easier implementation. The isolation also enables faster pinpointing of where an error may be and, hence, in fixing the error in one place only. Even before the product was shipped, it was possible to keep the system with close to zero known errors. The paradigm described here has become a valuable tool in our toolbox. However, when this paradigm is used, one must also pay attention should complexity start to grow beyond expectations, as it may be a sign of too high cohesion or too little coupling.
Top
A Process Oriented Approach to USB Driver Development Carl G. RITSON and Frederick R.M. BARNES, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NF, England.
	Abstract. Operating-systems are the core software component of many modern computer systems, ranging from small specialised embedded systems through to large distributed operating-systems. The demands placed upon these systems are increasingly complex, in particular the need to handle concurrency: to exploit increasingly parallel (multi-core) hardware; support increasing numbers of user and system processes; and to take advantage of increasingly distributed and decentralised systems. The languages and designs that existing operating-systems employ provide little support for concurrency, leading to unmanageable programming complexities and ultimately errors in the resulting systems; hard to detect, hard to remove, and almost impossible to prove correct.Implemented in occam-p, a CSP derived language that provides guarantees of freedom from race-hazards and aliasing error, the RMoX operating-system represents a novel approach to operating-systems, utilising concurrency at all levels to simplify design and implementation. This paper presents the USB (universal serial bus) device-driver infrastructure used in the RMoX system, demonstrating that a highly concurrent process-orientated approach to device-driver design and implementation is feasible, efficient and results in systems that are reliable, secure and scalable.
Top
A Native Transterpreter for the LEGO Mindstorms RCX Jonathan SIMPSON, Christian L. JACOBSEN and Matthew C. JADUD, Computing Laboratory, University of Kent, Canterbury, Kent, CT2 7NZ, England.
	Abstract. The LEGO Mindstorms RCX is a widely deployed educational robotics platform. This paper presents a concurrent operating environment for the Mindstorms RCX, implemented natively using occam-pi running on the Transterpreter virtual machine. A concurrent hardware abstraction layer aids both the developer of the operating system and facilitates the provision of process-oriented interfaces to the underlying hardware for students and hobbyists interested in small robotics platforms.
Top
Modeling and Analysis of the AMBA Bus Using CSP and B Alistair A. McEWAN and Steve SCHNEIDER, University of Surrey, U.K.
	Abstract. In this paper, we present a formal model and analysis of the AMBA Advanced High-performance Bus (AHB) on-chip bus. The model is given in CSPkB an integration of the process algebra CSP and the state-based formalism B. We describe the theory behind the integration of CSP and B. We demonstrate how the model is developed from the informal ARM specification of the bus. Analysis is performed using the model-checker ProB. The contribution of this paper may be summarised as follows: presentation of work in progress towards a formal model of the AMBA AHB protocol such that it may be used for inclusion in, and analysis of, co-design systems incorporating the bus, an evaluation of the integration of CSP and B in the production of such a model, and a demonstration and evaluation of the ProB tool in performing this analysis. The work in this paper was carried out under the Future Technologies for Systems Design Project at the University of Surrey, sponsored by AWE.
Top
A Step Towards Refining and Translating B Control Annotations to Handel-C Wilson IFILL(a), and Steve SCHNEIDER(b), (a)AWE Aldermaston, Reading, Berks, England; (b)Department of Computing, University of Surrey, Guildford, Surrey, England.
	Abstract. Research augmenting B machines presented at B2007 has demonstrated how fragments of control flow expressed as annotations can be added to associated machine operations, and shown to be consistent. This enables designers understanding about local relationships between successive operations to be captured at the point the operations are written, and used later when the controller is developed. This paper introduces several new annotations and I/O into the framework to take advantage of hardware s parallelism and to facilitate refinement and translation. To support the new annotations additional CSP control operations are added to the control language that now includes: recursion, prefixing, external choice, if-then-else, and sequencing. We informally sketch out a translation to Handel-C for prototyping.
Top
Towards the Formal Verification of a Java Processor in Event-B Neil GRANT and Neil EVANS, AWE, Aldermaston, UK.
	Abstract. Formal verification is becoming more and more important in the production of high integrity microprocessors. The general purpose formal method called Event-B is the latest incarnation of the B Method: it is a proof-based approach with a formal notation and refinement technique for modelling and verifying systems. Refinement enables implementation-level features to be proven correct with respect to an abstract specification of the system. In this paper we demonstrate an initial attempt to model and verify Sandia National Laboratories Score processor using Event-B. The processor is an (almost complete) implementation of a Java Virtua l Machine in hardware. Thus, refinement-based verification of the Score processor begins with a formal speci- fication of Java bytecode. Traditionally, B has been directed at the formal development of software systems. The use of B in hardware verification could provide a means of developing combined software/hardware systems, i.e. codesign.
Top
Advanced System Simulation, Emulation and Test (ASSET) Gregory L. WICKSTROM, Sandia National Laboratories, Albuquerque NM, USA
	Abstract. Maturing embeddable real-time concepts into deployable high consequence systems faces numerous challenges. Although overcoming these challenges can be aided by commercially available processes, toolsets, and components, they often fall short of meeting the needs at hand. This paper will review the development of a framework being assembled to address many of the shortcomings while attempting to leverage commercial capabilities as appropriate.
Top
Development of a Family of Multi-Core Devices Using Hierarchical Abstraction Andrew DULLER, Alan GRAY, Daniel TOWNER, Jamie ILES, Gajinder PANESAR, and Will ROBBINS, picoChip Designs Ltd., Bath, UK
	Abstract. picoChip has produced a range of commercially deployed multi-core devices, all of which have the same on-chip deterministic communications structure (the picoBus) but vary widely in the number and type of cores which make up the devices. Systems are developed from processes connected using unidirectional signals. Individual processes are described using standard C or assembly language and are grouped together in a hierarchical description of the overall system. This paper discusses how families of chips may be developed by hardening structures in the hierarchy of an existing software system. Hardening is the process of replacing sets of communicating processes with an equivalent hardware accelerator, without changing the interface to that sub-system. Initial development is performed using a completely software implementation, which has advantages in terms of time to market . When cost/power reductions are required, the proposed hardening process can be used to convert certain parts of a design into fixed hardware. These can then be included in the next generation of the device. The same tool chain is used for all devices and this means that verification of the hardware accelerator against the original system is simplified. The methodology discussed has been used to produce a family of devices which have been deployed in a wide range of wireless applications around the world.
Top
Hardware/Software Synthesis and Verification Using Esterel Satnam SINGH, Microsoft Research, Cambridge, CB3 0FB, United Kingdom
	Abstract. The principal contribution of this paper is the demonstration of a promising technique for the synthesis of hardware and software from a single specification which is also amenable to formal analysis. We also demonstrate how the notion of synchronous observers may provide a way for engineers to express formal assertions about circuits which may be more accessible then the emerging grammar based approaches. We also report that the semantic basis for the system we evaluate pays dividends when formal static analysis is performed using model checking
Top
Domain Specific Transformations for Hardware Ray Tracing Tim TODMAN and Wayne LUK, Imperial College, London, U.K.
	Abstract. We present domain-specific transformations of the ray-tracing algorithm targeting reconfigurable hardware devices. Ray tracing is a computationally intensive algorithm used to produce photorealistic images of three-diemnsional scenes.We show how the proposed transformations can adapt the basic ray-tracing algorithm to a breadth-first style, and give estimates for the hardware needed for realtime raytracing.
Top
A Reconfigurable System-on-Chip Architecture for Pico-Satellite Missions Tanya VLADIMIROVA and Xiaofeng WU, Surrey Space Centre Department of Electronic Engineering University of Surrey, Guildford, GU2 7XH, UK
	Abstract. Spacecraft operate in the unique space environment and are exposed to various types of radiation. Radiation effects can damage the on-board electronic circuits, particularly silicon devices. There is a pressing need for a remote upgrading capability which will allow electronic circuits on-board satellites to self-repair and evolve their functionality. One approach to addressing this need is to utilize the hardware reconfigurability of Field Programmable Gate Arrays. FPGAs nowadays are suitable for implementation of complex on-board system-on-chip designs. Leading-edge technology enables innovative solutions, permitting lighter picosatellite systems to be designed. This paper presents a reconfigurable system-onchip architecture for pico-satellite on-board data processing and control. The SoC adopts a modular bus-centric architecture using the AMBA bus and consists of soft intellectual property cores. In addition the SoC is capable of remote partial reconfiguration at run time.
Top
A Versatile Hardware-Software Platform for In-Situ Monitoring Systems Bernhard H. C. SPUTH, Oliver FAUST, and Alastair R. ALLEN, Department of Engineering, University of Aberdeen, Aberdeen AB24 3UE, UK
	Abstract. In-Situ Monitoring systems measure and relay environmental parameters. From a system design perspective such devices represent one node in a network. This paper aims to extend the networking idea from the system level towards the design level. We describe In-Situ Monitoring systems as network of components. In the proposed design these components can be implemented in either hardware or software. Therefore, we need a versatile hardware-software platform to accommodate the particular requirements of a wide range of In-Situ Monitoring systems. The ideal testing ground for such a versatile hardware-software platform are FPGAs (Field Programmable Gate Arrays) with embedded CPUs. The CPUs execute software processes which represent software components. The FPGA part can be used to implement hardware components in the form of hardware processes and it can be used to interface to other hardware components external to the processor. In effect this setup constitutes a network of communicating sequential processes within a chip. This paper presents a design flow based on the theory of CSP. The idea behind this design flow is to have a CSP model which is turned into a network of hardware and software components. With the proposed design flow we have extended the networking aspect of sensor networks towards the system design level. This allows us to treat In-Situ Measurement systems as sub-networks within a sensor network. Furthermore, the CSP based approach provides abstract models of the functionality which can be tested. This yields more reliable system designs.
Top