WoTUG - The place for concurrent processes

BibTeX Proceedings details

BibTex html text dump of PaperDB database.

PaperDB is GPL Software, see: http://paperdb.sourceforge.net.

  title = "{F}ine-grain {C}oncurrency",
  author= "Hoare, Tony",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "1--20",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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 \&\#8211; both at Microsoft Research
     and in the University Computing Laboratory."
  title = "{C}ommunicating {P}rocess {A}rchitecture for {M}ulticores",
  author= "May, David",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "21--32",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{L}azy {E}xploration and {C}hecking of {CSP} {M}odels with {CSP}sim",
  author= "Brooke, Philip J and Paige, Richard F.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "33--50",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{T}he {C}ore {L}anguage of {A}ldwych",
  author= "Huntbach, Matthew",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "51--66",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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 \&\#8220;logic
     programming\&\#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."
  title = "{JCSP}ro{B}: {I}mplementing {I}ntegrated {F}ormal {S}pecifications in {C}oncurrent {J}ava",
  author= "Yang, Letu and Poppleton, Michael R.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "67--88",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{C}omponents with {S}ymbolic {T}ransition {S}ystems: a {J}ava {I}mplementation of {R}endezvous",
  author= "Fernandes, Fabricio and Passama, Robin and Royer, Jean-Claude",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "89--108",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{C}oncurrent/{R}eactive {S}ystem {D}esign with {H}oneysuckle",
  author= "East, Ian R.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "109--118",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{CSP} and {R}eal-{T}ime: {R}eality or {I}llusion?",
  author= "Orlic, Bojan and Broenink, Jan F.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "119--148",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{T}esting and {S}ampling {P}arallel {S}ystems",
  author= "Kerridge, Jon",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "149--162",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{M}obility in {JCSP}: {N}ew {M}obile {C}hannel and {M}obile {P}rocess {M}odels",
  author= "Chalmers, Kevin and Kerridge, Jon and Romdhani, Imed",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "163--182",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{C}++{CSP}2: {A} {M}any-to-{M}any {T}hreading",
  author= "Brown, Neil C.C.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "183--206",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  abstract= "The advent of mass-market multicore processors provides
     exciting new opportunities for parallelism on the desktop.
     The original C++CSP \&\#8211; a library providing
     concurrency in C++ \&\#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."
  title = "{D}esign {P}rinciples of the {S}ystem{CSP} {S}oftware {F}ramework",
  author= "Orlic, Bojan and Broenink, Jan F.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "207--228",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{P}y{CSP} - {C}ommunicating {S}equential {P}rocesses for {P}ython",
  author= "Bjørndalen, John Markus and Vinter, Brian and Anshus, Otto J.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "229--248",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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\&\#8217;s Extreme Multiprogramming
     Class at the CS department, university of Copenhagen with
     promising results."
  title = "{A} {P}rocess-{O}riented {A}rchitecture for {C}omplex {S}ystem {M}odelling",
  author= "Ritson, Carl G. and Welch, Peter H.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "249--266",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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 \&\#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
  title = "{C}oncurrency {C}ontrol and {R}ecovery {M}anagement for {O}pen e-{B}usiness {T}ransactions",
  author= "Razavi, Amir R. and Moschoyiannis, Sotiris K. and Krause, Paul J.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "267--286",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "trancell - an {E}xperimental {ETC} to {C}ell {BE} {T}ranslator",
  author= "Jørgensen, Ulrik Schou and Suenson, Espen",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "287--298",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{A} {V}ersatile {H}ardware-{S}oftware {P}latform for {I}n-{S}itu {M}onitoring {S}ystems",
  author= "Sputh, Bernhard H.C. and Faust, Oliver and Allen, Alastair R.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "299--312",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{H}igh {C}ohesion and {L}ow {C}oupling: the {O}ffice {M}apping {F}actor",
  author= "Teig, Øyvind",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "313--322",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  abstract= "This case observation describes how an embedded industrial
     software architecture was \&\#8220;mapped\&\#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
     \&\#8220;listen\&\#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."
  title = "{A} {P}rocess {O}riented {A}pproach to {USB} {D}river {D}evelopment",
  author= "Ritson, Carl G. and Barnes, Frederick R. M.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "323--338",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{A} {N}ative {T}ransterpreter for the {LEGO} {M}indstorms {RCX}",
  author= "Simpson, Jonathan and Jacobsen, Christian L. and Jadud, Matthew C.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "339--348",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{I}ntegrating and {E}xtending {JCSP}",
  author= "Welch, Peter H. and Brown, Neil C.C. and Moores, James and Chalmers, Kevin and Sputh, Bernhard H.C.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "349--369",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{H}ardware/{S}oftware {S}ynthesis and {V}erification {U}sing {E}sterel",
  author= "Singh, Satnam",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "371--378",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{M}odeling and {A}nalysis of the {AMBA} {B}us {U}sing {CSP} and {B}",
  author= "McEwan, Alistair A. and Schneider, Steve",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "379--398",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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\textbar\textbarB\&\#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."
  title = "{A} {S}tep {T}owards {R}efining and {T}ranslating {B} {C}ontrol {A}nnotations to {H}andel-{C}",
  author= "Ifill, Wilson and Schneider, Steve",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "399--424",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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\&\#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\&\#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."
  title = "{T}owards the {F}ormal {V}erification of a {J}ava {P}rocessor in {E}vent-{B}",
  author= "Grant, Neil and Evans, Neil",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "425--442",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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.
  title = "{A}dvanced {S}ystem {S}imulation, {E}mulation and {T}est ({ASSET})",
  author= "Wickstrom, Gregory",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "443--464",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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
  title = "{D}evelopment of a {F}amily of {M}ulti-{C}ore {D}evices {U}sing {H}ierarchical {A}bstraction",
  author= "Duller, Andrew and Gray, Alan and Towner, Daniel and Iles, Jamie and Panesar, Gajinder and Robbins, Will",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "465--478",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{D}omain {S}pecific {T}ransformations for {H}ardware {R}ay {T}racing",
  author= "Todman, Tim and Luk, Wayne",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "479--492",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{A} {R}econfigurable {S}ystem-on-{C}hip {A}rchitecture for {P}ico-{S}atellite {M}issions",
  author= "Vladimirova, Tanya and Wu, Xiaofeng",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "493--502",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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
  title = "{T}ransactional {CSP} {P}rocesses",
  author= "Cassar, Gail and Abela, Patrick",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "503--504",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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."
  title = "{A}lgebras of {A}ctions in {C}oncurrent {P}rocesses",
  author= "Burgin, Mark and Smith, Marc L.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "505--506",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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\&\#8217;s composition hierarchy
     corresponds to the reality that intermediate units of
     composition exist, and that these intermediate units
     don\&\#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\&\#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\&\#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."
  title = "{U}sing occam-pi {P}rimitives with the {C}ell {B}roadband {E}ngine",
  author= "Dimmich, Damian J.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "507--508",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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\&\#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."
  title = "{S}hared-{M}emory {M}ulti-{P}rocessor {S}cheduling {A}lgorithms for {CCSP}",
  author= "Ritson, Carl G.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "509--510",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  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 \&\#8211;
     and continues to evolve \&\#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."
  title = "{C}ompiling occam to {C} with {T}ock",
  author= "Sampson, Adam T.",
  editor= "McEwan, Alistair A. and Schneider, Steve and Ifill, Wilson and Welch, Peter H.",
  pages = "511--512",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn= "978-1-58603-767-3",
  year= "2007",
  month= "jul",
  abstract= "Tock is a new occam compiler from the University of Kent,
     the latest result of many years\&\#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\&\#8217;s output
     resembles handwritten CIF code; this eases debugging and
     takes better advantage of the C compiler\&\#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

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!