WoTUG - The place for concurrent processes

Refer Proceedings details


%T Fine\-grain Concurrency
%A Tony Hoare
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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 &\[sh]8211; both at Microsoft
   Research and in the University Computing Laboratory.


%T Communicating Process Architecture for Multicores
%A David May
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T Lazy Exploration and Checking of CSP Models with CSPsim
%A Philip J Brooke, Richard F. Paige
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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\[rs]s usage with
   examples from the model. The tool\[rs]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.


%T The Core Language of Aldwych
%A Matthew Huntbach
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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
   &\[sh]8220;logic programming&\[sh]8221;. 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.


%T JCSProB: Implementing Integrated Formal Specifications in Concurrent Java
%A Letu Yang, Michael R. Poppleton
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T Components with Symbolic Transition Systems: a Java Implementation of Rendezvous
%A Fabricio Fernandes, Robin Passama, Jean-Claude Royer
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T Concurrent/Reactive System Design with Honeysuckle
%A Ian R. East
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T CSP and Real\-Time: Reality or Illusion?
%A Bojan Orlic, Jan F. Broenink
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T Testing and Sampling Parallel Systems
%A Jon Kerridge
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T Mobility in JCSP: New Mobile Channel and Mobile Process Models
%A Kevin Chalmers, Jon Kerridge, Imed Romdhani
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T C++CSP2: A Many\-to\-Many Threading
%A Neil C.C. Brown
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X The advent of mass\-market multicore processors provides
   exciting new opportunities for parallelism on the desktop.
   The original C++CSP &\[sh]8211; a library providing
   concurrency in C++ &\[sh]8211; 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.


%T Design Principles of the SystemCSP Software Framework
%A Bojan Orlic, Jan F. Broenink
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T PyCSP \- Communicating Sequential Processes for Python
%A John Markus Bjørndalen, Brian Vinter, Otto J. Anshus
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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&\[sh]8217;s Extreme
   Multiprogramming Class at the CS department, university
   of Copenhagen with promising results.


%T A Process\-Oriented Architecture for Complex System Modelling
%A Carl G. Ritson, Peter H. Welch
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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 &\[sh]8211;
   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.


%T Concurrency Control and Recovery Management for Open e\-Business Transactions
%A Amir R. Razavi, Sotiris K. Moschoyiannis, Paul J. Krause
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T trancell \- an Experimental ETC to Cell BE Translator
%A Ulrik Schou Jørgensen, Espen Suenson
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T A Versatile Hardware\-Software Platform for In\-Situ Monitoring Systems
%A Bernhard H.C. Sputh, Oliver Faust, Alastair R. Allen
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T High Cohesion and Low Coupling: the Office Mapping Factor
%A Øyvind Teig
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X This case observation describes how an embedded industrial
   software architecture was
   &\[sh]8220;mapped&\[sh]8221; 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 &\[sh]8220;listen&\[sh]8221; 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.


%T A Process Oriented Approach to USB Driver Development
%A Carl G. Ritson, Frederick R. M. Barnes
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T A Native Transterpreter for the LEGO Mindstorms RCX
%A Jonathan Simpson, Christian L. Jacobsen, Matthew C. Jadud
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T Integrating and Extending JCSP
%A Peter H. Welch, Neil C.C. Brown, James Moores, Kevin Chalmers, Bernhard H.C. Sputh
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X This paper presents the extended and re\-integrated JCSP
   library of CSP packages for Java. It integrates the
   differing advances made by Quickstone\[rs]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.


%T Hardware/Software Synthesis and Verification Using Esterel
%A Satnam Singh
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T Modeling and Analysis of the AMBA Bus Using CSP and B
%A Alistair A. McEwan, Steve Schneider
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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&\[sh]8212;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.


%T A Step Towards Refining and Translating B Control Annotations to Handel\-C
%A Wilson Ifill, Steve Schneider
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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&\[sh]8217; 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&\[sh]8217;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.


%T Towards the Formal Verification of a Java Processor in Event\-B
%A Neil Grant, Neil Evans
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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\[rs] 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.


%T Advanced System Simulation, Emulation and Test (ASSET)
%A Gregory Wickstrom
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T Development of a Family of Multi\-Core Devices Using Hierarchical Abstraction
%A Andrew Duller, Alan Gray, Daniel Towner, Jamie Iles, Gajinder Panesar, Will Robbins
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T Domain Specific Transformations for Hardware Ray Tracing
%A Tim Todman, Wayne Luk
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T A Reconfigurable System\-on\-Chip Architecture for Pico\-Satellite Missions
%A Tanya Vladimirova, Xiaofeng Wu
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T Transactional CSP Processes
%A Gail Cassar, Patrick Abela
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.


%T Algebras of Actions in Concurrent Processes
%A Mark Burgin, Marc L. Smith
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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&\[sh]8217;s
   composition hierarchy corresponds to the reality that
   intermediate units of composition exist, and that these
   intermediate units don&\[sh]8217;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&\[sh]8217;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&\[sh]8212;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.


%T Using occam\-pi Primitives with the Cell Broadband Engine
%A Damian J. Dimmich
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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&\[sh]8217;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.


%T Shared\-Memory Multi\-Processor Scheduling Algorithms for CCSP
%A Carl G. Ritson
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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
   &\[sh]8211; and continues to evolve &\[sh]8211; 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.


%T Compiling occam to C with Tock
%A Adam T. Sampson
%E Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X Tock is a new occam compiler from the University of Kent,
   the latest result of many years&\[sh]8217; 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&\[sh]8217;s output resembles handwritten CIF code;
   this eases debugging and takes better advantage of the C
   compiler&\[sh]8217;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.


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

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

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

Valid HTML 4.01!