Refer Proceedings details

%T Finitary Refinement Checks for Infinitary Specifications
%A A. W. Roscoe
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X We see how refinement against a variety of infinite\-state
   CSP specifications can be translated into finitary
   refinement checks. Methods used include turning a process
   into its own specification inductively, and we recall
   Wolper\[rs]s discovery that data independence can be used
   for this purpose.

%T An Automatic Translation of CSP to Handel\-C
%A Jonathan D. Phillips, G. S. Stiles
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X We present tools that convert a subset of CSP into Handel\-C
   code. Handel\-C is similar to the standard C programming
   language, and can be itself converted to produce files to
   program an FPGA. We thus now have a process that can
   directly generate hardware from a verified high\-level
   description. The CSP to Handel\-C translator makes use of
   the Lex and Yacc programming tools. The Handel\-C code
   produced is functional, but not necessarily optimized for
   all situations. The translator has been tested using several
   CSP scripts of varying complexity. The functionality of the
   resulting Handel\-C programs has been verified with
   simulations, and two scripts were further checked with
   successful implementations on an FPGA.

%T On Linear Time and Congruence in Channel\-Passing Calculi
%A Frederic Peschanski
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X Process algebras such as CSP or the Pi\-calculus are
   theories to reason about concurrent software. The
   Pi\-calculus also introduces channel passing to address
   specific issues in mobility. Despite their similarity, the
   languages expose salient divergences at the formal level.
   CSP is built upon trace semantics while labelled transition
   systems and bisimulation are the privileged tools to discuss
   the Pi\-calculus semantics. In this paper, we try to bring
   closer both approaches at the theoretical level by showing
   that proper trace semantics can be built upon the
   Pi\-calculus. Moreover, by introducing locations, we obtain
   the same discriminative power for both the trace and
   bisimulation equivalences, in the particular case of early
   semantics. In a second part, we propose to develop the
   semantics of a slightly modified language directly in terms
   of traces. This language retains the full expressive power
   of the Pi\-calculus and most notably supports channel
   passing. Interestingly, the resulting equivalence, obtained
   from late semantics, exhibits a nice congruence property
   over process expressions.

%T Prioritised Service Architecture
%A Ian R. East
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X Previously, Martin gave formal conditions under which a
   simple design rule guarantees deadlock\-freedom in a system
   with service (client\-server) architecture. Both conditions
   and design rule may be statically verified. Here, they are
   re\-arranged to define service protocol, service network
   (system), and service network component, which together form
   a model for system abstraction. Adding mutual exclusion of
   service provision and dependency between service connections
   enriches abstraction and is shown to afford
   compositionality. Prioritised alternation of service
   provision further enriches abstraction while retaining
   deadlock\-freedom and denying priority conflict, given
   appropriate new design rules.

%T Debugging and Verification of Parallel Systems \- the picoChip Way
%A Andrew Duller, Gajinder Panesar, Daniel Towner
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X This paper describes the methods that have been developed
   for debugging and verifying systems using devices from the
   picoArray(TM) family. In order to increase the computational
   ability of these devices the hardware debugging support has
   been kept to a minimum and the methods and tools described
   take this into account. An example of how some of these
   methods have been used to produce an 802.16 system is given.
   The important features of the new PC102 device are outlined.

%T Active Serial Port: A Component for JCSPNet Embedded Systems
%A Sarah Clayton, Jon Kerridge
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X The javax.comm package provides basic low\-level access
   between Java programs and external input\-output devices, in
   particular, serial devices. Such communications are handled
   using event listener technology similar to that used in the
   AWT package. Using the implementation of active AWT
   components as a model we have constructed an active serial
   port (ASP), using javax.comm, that gives a channel interface
   that is more easily incorporated into a JCSPNet collection
   of processes. The ASP has been tested in a real\-time
   embedded system used to collect data from infrared detectors
   used to monitor the movement of pedestrians. The collected
   data is transferred across an Ethernet from the serial port
   process to the data manipulation processes. The performance
   of the JCSPNet based system has been compared with that
   supplied by the manufacturer of the detector and we conclude
   by showing how a complete monitoring system could be
   constructed in a scalable manner.

%T The Transterpreter: A Transputer Interpreter
%A Christian L. Jacobsen, Matthew C. Jadud
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X We have written the Transterpreter, a virtual machine for
   executing the transputer instruction set. This interpreter
   is a small, portable, and extensible run\-time, intended to
   be easily ported to handheld computers, mobile phones, and
   other embedded contexts. In striving for this level of
   portability, occam programs compiled to Transputer
   byte\-code can currently be run on desktop computers,
   handhelds, and even the LEGO Mindstorms robotics kit.

%T Adding Mobility to Networked Channel\-Types
%A Mario Schweigler
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X This paper reports the specification of a sound concept for
   the mobility of network\-channel\-types in KROC.net. The
   syntax and semantics of KROC.net have also been modified in
   order to integrate it more seamlessly into the occam\-pi
   language. These new features are currently in the process of
   being implemented. Recent developments in occam\-pi and KROC
   (such as mobile processes and live / dead
   channel\-type\-ends) are described, together with their
   impact on KROC.net. This paper gives an overview of the
   recent developments in KROC.net, and presents its proposed
   final semantics, as well as the proposed interface between
   the KROC.net infrastructure and the KROC compiler.

%T A Comparison of Three MPI Implementations
%A Brian Vinter, John Markus Bjørndalen
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X Various implementations of MPI are becoming available as MPI
   is slowly emerging as the standard API for parallel
   programming on most platforms. The open source
   implementations LAM\-MPI and MPICH are the most widely used,
   while commercial implementations are usually tied to special
   hardware platforms. This paper compares these two
   open\-source MPI\-implementations to one of the commercially
   available implementations, MESH\-MPI from
   MESH\-Technologies. We find that the commercial
   implementation is significantly faster than the open\-source
   implementations, though LAM\-MPI does come out on top in
   some benchmarks.

%T An Evaluation of Inter\-Switch Connections
%A Hans Henrik Happe, Brian Vinter
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X In very large clusters it is not possible to get Ethernet
   switches that are large enough to support the whole cluster,
   thus a configuration with multiple switches are needed. This
   work seeks to evaluate the interconnection strategies for a
   new 300+ CPU cluster at the University of Southern Denmark.
   The focal point is a very inexpensive switch from D\-Link
   which unfortunately offers only 24 Gb ports. We investigate
   different inter\-switch connections and their impact at
   application level.

%T Observing Processes
%A Adrian E. Lawrence
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X This paper discusses the sorts of observations of processes
   that are appropriate to capture priority. The standard
   denotational semantics for CSP are based around observations
   of traces and refusals. Choosing to record a little more
   detail allows extensions of CSP which describe some very
   general processes including those that include priority. A
   minimal set of observations yields a language and semantics
   remarkably close to the standard Failures\-Divergences model
   of CSP which is described in a companion paper. A slightly
   richer set of observations yields a somewhat less abstract
   language.

%T Triples
%A Adrian E. Lawrence
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X The most abstract form of acceptance semantics for a variant
   of CSPP is outlined. It encompasses processes which may
   involve priority, but covers a much wider class of systems
   including real time behaviour. It shares many of the
   features of the standard Failures\-Divergences treatment:
   thus it is only a Complete Partial Order when the alphabet
   of events is finite.

%T C++CSP Networked
%A Neil C.C. Brown
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X One year ago, the Kent C++CSP Library was presented at this
   conference. C++CSP is an implementation of CSP ideas in C++.
   After it was presented, C++CSP was released to the world at
   large under the Lesser GNU Public Licence. It had always
   been the author\[rs]s intention to develop a network
   capability in the library. This paper details the
   development of a network capability for the library and the
   results of benchmarks, which are encouragingly fast.

%T Communicating Mobile Processes
%A Frederick R. M. Barnes, Peter H. Welch
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X This paper presents a new model for mobile processes in
   occam\-pi. A process, embedded anywhere in a dynamically
   evolving network, may suspend itself mid\-execution, be
   safely disconnected from its local environment, moved (by
   communication along a channel), reconnected to a new
   environment and reactivated. Upon reactivation, the process
   resumes execution from the same state (i.e. data values and
   code positions) it held when it suspended. Its view of its
   environment is unchanged, since that is abstracted by its
   synchronisation (e.g. channels and barriers) interface and
   that remains constant. The environment behind that interface
   will (usually) be completely different. The mobile process
   itself may contain any number of levels of dynamic
   sub\-network. This model is simpler and, in some ways, more
   powerful than our earlier proposal, which required a process
   to terminate before it could be moved. Its formal semantics
   and implementation, however, throw up extra challenges. We
   present details and performance of an initial
   implementation.

%T Dynamic BSP: Towards a Flexible Approach to Parallel Computing over the Grid
%A Jeremy M. R. Martin, Alex V. Tiskin
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X The Bulk Synchronous model of parallel programming has
   proved to be a successful paradigm for developing portable,
   scalable, high performance software. Originally developed
   for use with traditional supercomputers, it was later
   applied to networks of workstations. Following the emergence
   of grid computing, new programming models are needed to
   exploit its potential. We consider the main issues relating
   to adapting BSP for this purpose, and propose a new model
   Dynamic BSP, which brings together many elements from
   previous work in order to deal with quality\-of\-service and
   heterogeneity issues. Our approach uses a task\-farmed
   implementation of supersteps.

%T CSP: The Best Concurrent\-System Description Language in the World \- Probably!
%A Michael Goldsmith
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X CSP, Hoare\[rs]s Communicating Sequential Processes, is one
   of the formalisms that underpins the antecedents of CPA, and
   this year celebrates its Silver Jubilee. Formal Systems\[rs]
   own FDR refinement checker is among the most powerful
   explicit exhaustive finite\-state exploration tools, and is
   tailored specifically to the CSP semantics. The CSPm ASCII
   form of CSP, in which FDR scripts are expressed, is the
   de\-facto standard for CSP tools. Recent work has
   experimentally extended the notation to include a
   probabilistic choice construct, and added functionality into
   FDR to produce models suitable for analysis by the
   Birmingham University PRISM tool.

%T Graphical Tool for Designing CSP Systems
%A Jan F. Broenink, Dusko S. Jovanovic
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X For a broad acceptance of an engineering paradigm, a
   graphical notation and supporting design tool seem
   inevitable. This paper discusses certain issues of
   developing a design environment for building systems based
   on CSP. Some of the issues discussed depend specifically on
   the underlying theory of CSP, while a number of them are
   common for any graphical notation and supporting tools, such
   as provisions for complexity management and design overview.

%T Towards a Semantics for Prioritized Alternation
%A Ian R. East
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X A new prioritised alternation programming construct and CSP
   operator have previously been suggested by the author to
   express behaviour that arises with machine\-level
   prioritised vectored interruption. The semantics of each is
   considered, though that of prioritisation is deferred given
   the current lack of consensus regarding a suitable domain.
   Defining axioms for the operator are tentatively proposed,
   along with possible laws regarding behaviour. Lastly, the
   issue of controlled termination of component and construct
   is explored. This is intended as only a first step towards a
   complete semantics.

%T Refining Industrial Scale Systems in Circus
%A Marcel Oliveira, Ana Cavalcanti, Jim Woodcock
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X Circus is a new notation that may be used to specify both
   data and behaviour aspects of a system, and has an
   associated refinement calculus. Although a few case studies
   are already available in the literature, the industrial fire
   control system presented in this paper is, as far as we
   know, the largest case study on the Circus refinement
   strategy. We describe the refinement and present some new
   laws that were needed. Our case study makes extensive use of
   mutual recursion; a simplified notation for specifying such
   systems and proving their refinements is proposed here.

%T K\-CSP Component Based Development of Kernel Extensions
%A Bernhard H.C. Sputh
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X Kernel extension development suffers from two problems.
   Firstly, there is little to no code reuse. This is caused by
   the fact that most kernel extensions are coded in the C
   programming language. This language only allows code reuse
   either by using `copy and paste\[rs] or by using libraries.
   Secondly, the poor separation of synchronisation and
   functionality code makes it difficult to change one without
   affecting the other. It is, therefore, difficult to use the
   synchronisation mechanisms correctly. The approach proposed
   in this paper tries to solve these problems by introducing a
   component based programming model for kernel extensions, and
   a system based on this proposal is implemented for the Linux
   kernel. The language used for the implementation is
   Objective\-C, and as a synchronisation mechanism
   Communicating Sequential Processes is used. This model
   allows the functionality and synchronisation of a component
   to be developed separately. Furthermore, due to the use of
   Communicating Sequential Processes it is possible to verify
   the correctness of the synchronisation. An example given in
   this paper illustrates how easy it is to use the K\-CSP
   environment for development.

%T Chaining Communications Algorithms with CSP
%A Oliver Faust, Bernhard H.C. Sputh, David Endler
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X Software Defined Radio (SDR) requires a reliable, fast and
   flexible method to chain parameterisable algorithms.
   Communicating Sequential Processes (CSP) is a design
   methodology, which offers exactly these properties. This
   paper explores the idea of using a Java implementation of
   CSP (JCSP) to model a flexible algorithm chain for Software
   Defined Radio. JCSP offers the opportunity to distribute
   algorithms on different processors in a multiprocessor
   environment, which gives a speed up and keeps the system
   flexible. If more processing power is required another
   processor can be added. In order to cope with the high data
   rate requirement of SDR, optimized data transfer schemes
   were developed. The goal was to increase the overall system
   efficiency by reducing the synchronisation overhead of a
   data transfer between two algorithms. To justify the use of
   CSP in SDR, a system incorporating CSP was compared with a
   conventional system, in single and multiprocessor
   environments.

%T Using CSP to Verify Aspects of an Occam\-to\-FPGA Compiler
%A Roger M. A. Peel, Wong Han Feng Javier
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X This paper reports on the progress made in developing
   techniques for the verification of an occam to FPGA
   compiler.The compiler converts occam programs into logic
   circuits that are suitable for loading into
   field\-programmable gate arrays (FPGAs). Several levels of
   abstraction of these circuits provide links to conventional
   hardware implementations. Communicating Sequential Processes
   (CSP) has then been used to model these circuits. This CSP
   has been subjected to tests for deadlock and livelock
   freedom using the Failures\-Divergence Refinement tool
   (FDR). In addition, FDR has been used to prove that the
   circuits emitted have behaviours equivalent to CSP
   specifications of the original occam source codes.

%T Focussing on Traces to Link VCR and CSP
%A Marc L. Smith
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X View\-Centric Reasoning (VCR) replaces CSP\[rs]s perfect
   observer with multiple, possibly imperfect observers. To
   employ view\-centric reasoning within existing CSP models
   requires a bookkeeping change. Specifically, VCR introduces
   parallel events as a new primitive for constructing traces,
   and distinguishes two types of event traces: histories and
   views. Previously, we gave the operational semantics of VCR,
   and demonstrated the utility of parallel event traces to
   reason for the first time unambiguously about the meaning of
   the Linda predicate operations rdp() and inp(). The choice
   of using an operational semantics to describe VCR makes
   direct comparison with CSP difficult; therefore, work is
   ongoing to recast VCR denotationally, then link it with the
   other CSP models within Hoare and He\[rs]s Unifying Theories
   of Programming. Initial efforts in this direction led to a
   comparison of VCR with Lawrence\[rs]s HCSP. In this paper,
   we present some recent insights and abstractions \- inspired
   by modern quantum physics \- that have emerged whilst
   contemplating parallel event traces in light of the unifying
   theories. These insights lead to a more natural expression
   of VCR traces, in the sense that they more closely resemble
   CSP traces, thus forming a basis for linking VCR and CSP.

%T Design of a Transputer Core and Implementation in an FPGA
%A Makoto Tanaka, Naoya Fukuchi, Yutaka Ooki, Chikara Fukunaga
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X We have made an IP (Intellectual Property) core for the T425
   transputer. The same machine instructions as the transputer
   are executable in this IP core (we call it TPCORE). To
   create an IP code for the transputer has two aspects. On one
   hand, if we could succeed in building our own one and put it
   in an FPGA, we could apply it as a core processor in a
   distributed system. We also intend to put it in a VLSI chip.
   On the other hand, if we can extend our transputer
   development starting from a very conventional one to more
   sophisticated ones, as Inmos proceeded to the T9000, we will
   eventually find our technological breakthrough for the
   bottlenecks that the original transputer had, such as the
   restriction of the number of communication channels. It is
   important to have an IP core for the transputer. Although
   TPCORE uses the same register set with the same
   functionality as transputer and follows the same mechanisms
   for link communication between two processes and interrupt
   handling, the implementation must be very different from
   original transputer. We have extensively used the
   micro\-code ROM to describe any states that TPCORE must
   take. Using this micro code ROM for the state transition
   description, we could implement TPCORE economically on FPGA
   space and achieve efficient performance.

%T Reconfigurable Hardware Synthesis of the IDEA Cryptographic Algorithm
%A Ali E. Abdallah, I. W. Damaj
%E Ian R. East, David Duce, Mark Green, Jeremy M. R. Martin, Peter H. Welch
%B Communicating Process Architectures 2004
%X The paper focuses on the synthesis of a highly parallel
   reconfigurable hardware implementation for the International
   Data Encryption Algorithm (IDEA). Currently, IDEA is well
   known to be a strong encryption algorithm. The use of such
   an algorithm within critical applications, such as military,
   requires efficient, highly reliable and correct hardware
   implementation. We will stress the affordability of such
   requirements by adopting a methodology that develops
   reconfigurable hardware circuits by following a
   transformational programming paradigm. The development
   starts from a formal functional specification stage. Then,
   by using function decomposition and provably correct data
   refinement techniques, powerful high\-order functions are
   refined into parallel implementations described in
   Hoare\[rs]s communicating sequential processes
   notation(CSP). The CSP descriptions are very closely
   associated with Handle\-C hardware description language
   (HDL) program fragments. This description language is
   employed to target reconfigurable hardware as the final
   stage in the development. The targeted system in this case
   is the RC\-1000 reconfigurable computer. In this paper
   different designs for the IDEA corresponding to different
   levels of parallelism are presented. Moreover,
   implementation, realization, and performance analysis and
   evaluation are included.

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.