Proceedings details

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
Title: Communicating Process Architectures 2007
Editors: db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
Publisher: IOS Press, Amsterdam
ISBN: 978-1-58603-767-3
ISSN: 1383-7575
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Keynote presentations

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Fine-grain Concurrency
Authors:	Tony Hoare
Abstract:	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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Communicating Process Architecture for Multicores
Authors:	David May
Abstract:	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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Papers

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Lazy Exploration and Checking of CSP Models with CSPsim
Authors:	Philip J Brooke, Richard F. Paige
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	The Core Language of Aldwych
Authors:	Matthew Huntbach
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	JCSProB: Implementing Integrated Formal Specifications in Concurrent Java
Authors:	Letu Yang, Michael R. Poppleton
Abstract:	The ProB model checker provides tool support for an integrated formal specification approach, combining the classical state-based B language with the event based 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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Components with Symbolic Transition Systems: a Java Implementation of Rendezvous
Authors:	Fabricio Fernandes, Robin Passama, Jean-Claude Royer
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Concurrent/Reactive System Design with Honeysuckle
Authors:	Ian R. East
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	CSP and Real-Time: Reality or Illusion?
Authors:	Bojan Orlic, Jan F. Broenink
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Testing and Sampling Parallel Systems
Authors:	Jon Kerridge
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Mobility in JCSP: New Mobile Channel and Mobile Process Models
Authors:	Kevin Chalmers, Jon Kerridge, Imed Romdhani
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	C++CSP2: A Many-to-Many Threading
Authors:	Neil C.C. Brown
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-processor machines. 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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Design Principles of the SystemCSP Software Framework
Authors:	Bojan Orlic, Jan F. Broenink
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	PyCSP - Communicating Sequential Processes for Python
Authors:	John Markus Bjørndalen, Brian Vinter, Otto J. Anshus
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	A Process-Oriented Architecture for Complex System Modelling
Authors:	Carl G. Ritson, Peter H. Welch
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Concurrency Control and Recovery Management for Open e-Business Transactions
Authors:	Amir R. Razavi, Sotiris K. Moschoyiannis, Paul J. Krause
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	trancell - an Experimental ETC to Cell BE Translator
Authors:	Ulrik Schou Jørgensen, Espen Suenson
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	A Versatile Hardware-Software Platform for In-Situ Monitoring Systems
Authors:	Bernhard H.C. Sputh, Oliver Faust, Alastair R. Allen
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	High Cohesion and Low Coupling: the Office Mapping Factor
Authors:	Øyvind Teig
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	A Process Oriented Approach to USB Driver Development
Authors:	Carl G. Ritson, Frederick R. M. Barnes
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	A Native Transterpreter for the LEGO Mindstorms RCX
Authors:	Jonathan Simpson, Christian L. Jacobsen, Matthew C. Jadud
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Integrating and Extending JCSP
Authors:	Peter H. Welch, Neil C.C. Brown, James Moores, Kevin Chalmers, Bernhard H.C. Sputh
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 significant 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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Hardware/Software Synthesis and Verification Using Esterel
Authors:	Satnam Singh
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Modeling and Analysis of the AMBA Bus Using CSP and B
Authors:	Alistair A. McEwan, Steve Schneider
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 CSP\|\|B—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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	A Step Towards Refining and Translating B Control Annotations to Handel-C
Authors:	Wilson Ifill, Steve Schneider
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Towards the Formal Verification of a Java Processor in Event-B
Authors:	Neil Grant, Neil Evans
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 Virtual Machine in hardware. Thus, refinement-based verification of the Score processor begins with a formal specification 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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Advanced System Simulation, Emulation and Test (ASSET)
Authors:	Gregory Wickstrom
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Development of a Family of Multi-Core Devices Using Hierarchical Abstraction
Authors:	Andrew Duller, Alan Gray, Daniel Towner, Jamie Iles, Gajinder Panesar, Will Robbins
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Domain Specific Transformations for Hardware Ray Tracing
Authors:	Tim Todman, Wayne Luk
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-dimensional 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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	A Reconfigurable System-on-Chip Architecture for Pico-Satellite Missions
Authors:	Tanya Vladimirova, Xiaofeng Wu
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.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Fringe presentations

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Transactional CSP Processes
Authors:	Gail Cassar, Patrick Abela
Abstract:	Long-lived transactions (LLTs) are transactions intended to be executed over an extended period of time ranging from seconds to days. Traditional transactions maintain data integrity through ACID properties which ensure that: a transaction will achieve an "all-or-nothing" effect (atomicity); system will be in a legal state before a transaction begins and after it ends (consistency); a transaction is treated independently from any other transactions (isolation); once a transaction commits, its effects are not lost (durability). However, it is impractical and undesirable to maintain full ACID properties throughout the whole duration of a long lived transaction. Transaction models for LLTs, relax the ACID properties by organizing a long-lived transaction as a series of activities. Each activity is a discrete transactional unit of work which releases transactional locks upon its execution. Activities are executed in sequence and can either commit, rollback or suspend execution of the transaction. The long-lived transaction commits if all its activities complete successfully. If any of the activities fail, the long lived transaction should roll back by undoing any work done by already completed activities. Unless an activity requires the result of a previously committed activity, there is no constraint which specifies that the various activities belonging to a long lived transaction execute sequentially. Our proposed research focuses on combining long lived transactions and CSP such that independent activities execute in parallel thus achieving flexibility and better performance for long lived transactions. Very much as the occam CSP-based constructs, SEQ and PAR, allow processes to be executed sequentially or concurrently, the proposed SEQ_LLT and PAR_LLT constructs can be used to specify the sequential or concurrent execution of transactions. Two activities that are coordinated with the SEQ_LLT construct are evaluated in such a way that the second activity is executed only after the first activity commits. This corresponds to the SEQ construct which, from a concurrency perspective, executes in such a way that the second process starts its execution after the first process is complete. Similarly, PAR_LLT specifies that activities can start their execution, independently from whether any other activities have committed their transaction or not. We also use the same synchronization mechanisms provided by CSP to have concurrent activities communicate with one another. An activity which "waits" on a channel for communication with another concurrent activity is automatically suspended (and its transactional locks released) until it receives a message from another activity. A prototype implementation of the described constructs and some example applications have been implemented on SmartPay LLT (a platform loosely based on JSR95 developed by Ixaris Systems). This work has been part of an undergraduate dissertation at the University of Malta.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Algebras of Actions in Concurrent Processes
Authors:	Mark Burgin, Marc L. Smith
Abstract:	We introduce a high-level metamodel, EAP (event-action-process), for reasoning about concurrent processes. EAP shares with CSP notions of observable events and processes, but as its name suggests, EAP is also concerned with actions. Actions represent an intermediate level of event composition that provide the basis for a hierarchical structure that builds up from individual, observable events, to processes that may themselves be units of composition. EAP’s composition hierarchy corresponds to the reality that intermediate units of composition exist, and that these intermediate units don’t always fall neatly within process boundaries. One prominent example of an intermediate unit of composition, or action, is threads. Threads of execution are capable of crossing process boundaries, and one popular programming paradigm, object-oriented programming, encourages this approach to concurrent program design. While we may advocate for more disciplined, process-oriented design, the demand for better models for reasoning about threads remains. On a more theoretical level, traces of a computation are also actions. Traces are event structures, composed by the CSP observer, according to a set of rules for recording the history of a computation. In one of the author’s model for viewcentric reasoning (VCR), the CSP observer is permitted to record simultaneous events without interleaving; and in previous joint work by the authors, the extended VCR (EVCR) model permits the CSP observer to record events with duration, so that events may overlap entirely, partially, or not at all. Sequential composition may be viewed as a special case of parallel composition—one of many forms of composition we wish to be better able to reason about. Since such diverse types of composition exist, at the event, action, and process levels; and because such problematic actions as threads exist in real systems, we must find more appropriate models to reason about such systems. To this end, we are developing algebras at different levels of compositionality to address these goals. In particular, we are interested in a corresponding hierarchy of algebras, at the event, action, and process levels. The present focus of our efforts is at the action level, since these are the least well understood. This talk presents fundamental notions of actions and examples of actions in the context of real systems. A diversity of possible compositions at the action level will be revealed and discussed, as well as our progress on the action algebra itself.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Using occam-pi Primitives with the Cell Broadband Engine
Authors:	Damian J. Dimmich
Abstract:	The Cell Broadband Engine has a unique non-heterogeneous archi- tecture, consisting of an on-chip network of one general purpose PowerPC pro- cessor (the PPU), and eight dedicated vector processing units (the SPUs). These processors are interconnected by a high speed ring bus, enabling the use of different logical network topologies. When programming the Cell Broadband Engine using languages such as C, a developer is faced with a number of chal- lenges. For instance, parallel execution and synchronisation between proces- sors, as well as concurrency on individual processors, must be explicitly, and carefully, managed. It is our belief that languages explicitly supporting concur- rency are able to offer much better abstractions for programming architectures such as the Cell Broadband Engine. Support for running occam- programs on the Cell Broadband Engine has existed in the Transterpreter for some time. This support has however not featured efficient inter-processor communication and barrier synchronisation, or automatic deadlock detection. We discuss some of the changes required to the occam- scheduler to support these features on the Cell Broadband Engine. The underlying on-chip communication and synchronisation mechanisms are explored in the development of these new scheduling algorithms. Benchmarks of the communications performance are provided, as well as a discussion of how to use the occam- language to distribute a program onto a Cell Broadband Engine’s processors. The Transterpreter runtime, which already has support for the Cell Broadband Engine, is used as the platform for these experiments. The Transterpreter can be found at www.transterpreter.org.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Shared-Memory Multi-Processor Scheduling Algorithms for CCSP
Authors:	Carl G. Ritson
Abstract:	CCSP is a monolithic C library which acts as the run-time kernel for occam- programs compiled with the Kent Retargetable occam Compiler (KRoC). Over the past decade, it has grown to encompass many new and powerful features to support the occam-pi language as that has evolved – and continues to evolve – from classical occam. However, despite this wealth of development, the general methodology by which processes are scheduled and executed has changed little from its transputer inspired origins. This talk looks at applying previous research and new ideas to the CCSP scheduler in an effort to exploit fully the potential of new mass-market multicore processor systems. The key objective is to introduce support for shared-memory multicore systems, whilst maintaining the low scheduling overheads that occam-pi users have come to expect. Fundamental to this objective are wait-free data-structures, per-processor run-queues, and a strong will to consolidate and simplify the existing code base.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"

Title:	Compiling occam to C with Tock
Authors:	Adam T. Sampson
Abstract:	Tock is a new occam compiler from the University of Kent, the latest result of many years’ research into compiling concurrent languages. The existing occam compiler generates bytecode which is then translated into native instructions; this reduces opportunities for native code optimisation and limits portability. Tock translates occam into C using the CIF concurrent runtime interface, which can be compiled to efficient native code by any compiler supporting the C99 language standard. The resulting programs combine the safety and featherweight concurrency of occam with the performance and portability of C. Unlike previous attempts at translating occam to C, Tock’s output resembles handwritten CIF code; this eases debugging and takes better advantage of the C compiler’s optimisation facilities. Written in the purely functional language Haskell, Tock uses monadic combinator parsing and generic data structure traversal to provide a flexible environment for experimenting with new compiler and language features.
Bibliography:	Web page:BibTEX, Refer Plain text: BibTEX, Refer
Files:	PDF

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.