Refer Proceedings details

%T Semantics of prialt in Handel\-C (tm)
%A Andrew Butterfield
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X This paper discusses the semantics of the prialt construct
   in Handel\-C. The language is essentially a static subset of
   C, augmented with a parallel construct and channel
   communication, as found in CSP. All assignments and channel
   communication events take one clock cycle, with all updates
   synchronised with the clock edge marking the cycle end. The
   behaviour of prialt in Handel\-C is similar in concept to
   that of occam, and to the p\-priority concept of Adrian
   Lawrence\[rs]s CSPP. However, we have to contend with both
   input and output guards in Handel\-C, unlike the situation
   in occam, although prialts with conflicting priority
   requirements are not legal in Handel\-C. This makes our
   problem simpler than the more general case including such
   conflicts considered by Lawrence. We start with an informal
   discussion of the issues that arise when considering the
   semantics of Handel\-C\[rs]s prialt construct. We define a
   resolution function (R) that determines which requests in a
   collection of prialts become active. We describe a few
   properties that we expect to hold for resolution, and
   discuss the issue of compositionality.

%T Acceptances, Behaviours and Infinite Activity in CSPP
%A Adrian E. Lawrence
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X The denotational semantics presented here defines an
   extension of CSP called CSPP. It includes a full description
   of infinite behaviour in one simple model using only finite
   traces. This is true for both finite and infinite alphabets.
   The structure is a complete lattice, and so also a complete
   partial order, under refinement. Thus recursion is defined
   by fixed points in the usual way. It is also a complete
   restriction metric space so this provides an alternative
   treatment of recursion for contraction mappings.

%T HCSP: Imperative State and True Concurrency
%A Adrian E. Lawrence
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X HCSP is an extension of CSPP which captures the semantics of
   hardware compilation. Because it is a superset of CSPP, it
   can describe both hardware and software and so is useful for
   co\-design. The extensions beyond CSPP include: true
   concurrency; new hardware constructors; and a simple and
   natural way to represent imperative state. Both CSPP and
   HCSP were invented to cope with problems that arose while
   the author was trying to prove that the hardware that he had
   designed correctly implemented channels between a processor
   and an FPGA. Standard CSP did not capture priority, yet the
   circuits in the FPGA and the occam processes in the
   transputer both depended on priority for their correctness.
   The attempt to extend CSP rigorously to handle such problems
   of co\-design has led to develoments that seem to have a
   much wider significance including a new way of unifying
   theories for imperative programming. This paper reports on
   the current state of HCSP and focuses on handling imperative
   state and true concurrency. The acceptance denotational
   semantics is described briefly.

%T Consolidating The Agreement Problem Protocol Verification Environment
%A James S. Pascoe, Roger J. Loader
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X The Agreement Problem Protocol Verification Environment
   (APPROVE) has become a mature and robust platform for the
   automated verification of proposed solutions to agreement
   problems. APPROVE is based on the Spin model checker and
   leverages the literate programming tool noweb to provide
   Promela code supplied with LATEX documentation. The APPROVE
   discussion opened in Communicating Process Architectures
   2001 and described the initial project phases and summarised
   some preliminary results. This paper presents a follow up,
   providing a canonical report on the development, application
   and insight gained from the project.

%T On the Complexity of Buffer Allocation in Message Passing Systems
%A Alex Brodsky, Jan Bækgaard Pedersen, Alan Wagner
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X In modern cluster systems message passing functionality is
   often off\-loaded to the network interface card for
   efficiency reasons. However, this limits the amount of
   memory available for message buffers. Unfortunately, buffer
   insufficiency can cause an otherwise correct program to
   deadlock, or at least slow down. Hence, given a program
   trace from an execution in an unrestricted environment,
   determining the minimum number of buffers needed for a safe
   execution is an important problem. We present three related
   problems, all concerned with buffer allocation for safe and
   efficient execution. We prove intractability results for the
   first two problems and present a polynomial time algorithm
   for the third.

%T Java PastSet \- A Structured Distributed Shared Memory System
%A Kei Simon Pedersen, Brian Vinter
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X The architecture and performance of a Java implementation of
   a structured distributed shared memory system, PastSet, is
   described. The PastSet abstraction allows programmers to
   write applications that run efficiently on different
   architectures, from clusters to widely distributed systems.
   PastSet is a tuple\-based three\-dimensional structured
   distributed shared memory system, which provides the
   programmer with operations to perform causally ordered reads
   and writes of tuples to a virtual structured memory space
   called the PastSet. It has been shown that the original,
   native code, PastSet was able to outperform MPI and PVM when
   running real applications and we show that the design
   translates into Java so that Java PastSet is a qualified
   competitor to other cluster application programming
   interfaces for Java.

%T Synchronous Active Objects Introduce CSP\[rs]s Primitives in Java
%A Claude Petitpierre
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X This paper presents a proposal of a language, based on
   synchronous active objects that introduces the CSP
   primitives into Java. The proposal does not use channels to
   realise the inter\-process communications, but is shown to
   offer the same expressive power as the channel based
   solutions. The paper also shows that the rendezvous defined
   by CSP or our synchronous objects are very well adapted to
   the industrial development of event driven applications,
   handling simultaneously GUIs and accesses to remote
   applications.

%T Configurable Collective Communication in LAM\-MPI
%A John Markus Bjørndalen, Otto J. Anshus, Tore Aarsen, Brian Vinter
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X In another paper, we observed that PastSet (our experimental
   tuple space system) was 1.83 times faster on global
   reductions than LAM\-MPI. Our hypothesis was that this was
   due to the better resource usage of the PATHS framework (an
   extension to PastSet that supports orchestration and
   configuration) due to a mapping of the communication and
   operations which matched the computing resources and cluster
   topology better. This paper reports on an experiment to
   verify this and represents on\-going work to add some of the
   same configurability of PastSet and PATHS to MPI. We show
   that by adding run\-time configurable collective
   communication, we can reduce the latencies without
   recompiling the application source code. For the same
   cluster where we experienced the faster PastSet, we show
   that Allreduce with our configuration mechanism is 1.79
   times faster than the original LAM\-MPI Allreduce. We also
   experiment with the configuration mechanism on 3 different
   cluster platforms with 2\-, 4\-, and 8\-way nodes. For the
   cluster of 8\-way nodes, we show an improvement by a factor
   of 1.98 for Allreduce.

%T Cache\-Affinity Scheduling for Fine Grain Multithreading
%A Kurt Debattista, Kevin Vella, Joseph Cordina
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X Cache utilisation is often very poor in multithreaded
   applications, due to the loss of data access locality
   incurred by frequent context switching. This problem is
   compounded on shared memory multiprocessors when dynamic
   load balancing is introduced and thread migration disrupts
   cache content. In this paper, we present a technique, which
   we refer to as *batching*, for reducing the negative impact
   of fine grain multithreading on cache performance. Prototype
   schedulers running on uniprocessors and shared memory
   multiprocessors are described, and finally experimental
   results which illustrate the improvements observed after
   applying our techniques are presented.

%T A Predicate Transformer Semantics for a Concurrent Language of Refinement
%A Ana Cavalcanti, Jim Woodcock
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X Circus is a combination of Z and CSP; its chief
   distinguishing feature is the inclusion of the ideas of the
   refinement calculus. Our main objective is the definition of
   refinement methods for concurrent programs. The original
   semantic model for Circus is Hoare and He\[rs]s unifying
   theories of programming. In this paper, we present an
   equivalent semantics based on predicate transformers. With
   this new model, we provide a more adequate basis for the
   formalisation of refinement and verification\-condition
   generation rules. Furthermore, this new framework makes it
   possible to include logical variables and angelic
   nondeterminism in Circus. The consistency of the relational
   and predicate transformer models gives us confidence in
   their accuracy.

%T Reconnetics: A System for the Dynamic Implementation of Mobile Hardware Processes in FPGAs
%A Ralph Moseley
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X The capacity to utilise FPGA designs in such a way that they
   are compositional, mobile, and *interactive*, offers many
   new possibilities. This holds true for both research and
   commercial applications. With the system described here,
   hardware becomes as easy to distribute as software and the
   mediating links between the two domains allow for
   manipulation of physical resources in real time. Designs are
   no longer monolithic *images* downloaded at one time, but
   mobile entities that can be communicated over a distance and
   dynamically installed at run\-time many times and at many
   places. Such twin domain designs can be as complex as a
   processor, or as small in scale as a few logic gates. The
   run\-time system, Reconnetics, provides an environment of
   high\-level control over such elements, which requires
   little knowledge of the underlying hardware technology.

%T Performance Analysis and Behaviour Tuning for Optimisation of Communicating Systems
%A Mark Green, Ali E. Abdallah
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X Improving performance is the main driving force behind the
   use of parallel systems. Models for performance evaluation
   and techniques for performance optimisation are crucial for
   effectively exploiting the computational power of parallel
   systems. This paper focuses on methods for evaluating the
   performance of parallel applications built from components
   using the software architecture methodology. Minor
   differences in the low\-level behaviour of functionally
   equivalent processing elements can have a dramatic effect
   upon the performance of the overall system; this confounds
   attempts to predict performance at any step prior to
   implementation. VisualNets is a tool supporting the
   construction and graphical manipulation of interacting
   systems built from components. It makes use of
   specifications in the formal method CSP, which enables the
   relevant component behaviours and the linkage between
   components to be concisely described. The tool allows the
   behaviour of the whole system over time, and the patterns of
   interaction between the components, to be visualised through
   graphical animation. The graphical display produced
   facilitates the analysis and evaluation of performance, and
   highlights areas where performance could be improved via
   better utilisation of parallel resources. VisualNets also
   allows the timing properties of the components and of the
   architecture that underlies them to be changed, to represent
   different component implementations or platform
   configurations. A case study, based on the dual pipeline
   architecture, is presented to show how the graphical
   animation capability of VisualNets can be used, firstly to
   evaluate performance, and secondly to guide the development
   of more efficient versions of the parallel system.

%T Configuration Discovery and Mapping of a Home Network
%A Keith Pugh
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X A home network comprising many heterogeneous devices
   requires a scaleable interconnect capable of satisfying the
   often vastly different network resource demands of the
   devices. In addition, it is likely that over time the
   configuration of the network will change as new devices are
   added to the network and older ones removed or replaced.
   While it is acceptable for enterprise networks to be managed
   by a trained network administrator it is unreasonable to
   expect a home owner to have such expertise. Consequently, a
   free topology network coupled with a capacity for plug and
   play that allows nodes to be added anywhere, and at any time
   without interruption to the operation of the networked
   system are essential requirements. IEEE 1355 standard
   technology has the potential to satisfy these criteria. The
   demand for a free topology and a capacity for plug and play
   require that the configuration of the network is
   re\-discovered and mapped automatically, and at regular
   intervals. This paper describes such a configuration mapping
   process.

%T Cluster Computing and JCSP Networking
%A Peter H. Welch, Brian Vinter
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X Hoare\[rs]s algebra of Communicating Sequential Processes
   (CSP) enables a view of systems as layered networks of
   concurrent components, generating and responding to events
   communicated to each other through channels, barriers and
   other (formally defined) synchronisation primitives. The
   resulting image and discipline is close to hardware design
   and correspondingly easy to visualise, reason about, compose
   and scale. JCSP is a library of Java packages providing an
   (occam) extended version of this model that may be used
   alongside, or as a replacement for, the very different
   threads\-and\-monitors concurrency mechanisms built into
   Java. The current release (JCSP 1.0) supports concurrency
   within a single Java Virtual Machine (which may be
   multi\-processor). This paper reports early experiments with
   JCSP.net, an extension of JCSP for the dynamic construction
   of CSP networks across distributed environments. The aims of
   JCSP.net are to simplify the construction and programming of
   dynamically distributed and parallel systems. It provides
   high\-level support for CSP architectures, unifying
   concurrency logic within and between processors. The
   experiments are on some classical HPC problems, an area of
   work for which JCSP.net was not primarily designed. However,
   low overheads in the supporting infrastructure were a
   primary consideration * along with an intuitive and
   high\-level distributed programming model (based on CSP).
   Results reported show JCSP holding up well against * and
   often exceeding * the performance obtained from existing
   tools such as mpiJava and IBM*s TSpaces. The experimental
   platform was a cluster of 16 dual\-processor PIII Linux
   machines. It is expected that future optimisations in the
   pipeline for the JCSP.net infrastructure will improve the
   results presented here. JCSP and JCSP.net were developed at
   the University of Kent.

%T View\-Centric Reasoning for Linda and Tuple Space Computation
%A Marc L. Smith, Rebecca J. Parsons, Charles E. Hughes
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X In contrast to sequential computation, concurrent
   computation gives rise to parallel events. Efforts to
   translate the history of concurrent computations into
   sequential event traces result in the potential uncertainty
   of the observed order of these events. Loosely coupled
   distributed systems complicate this uncertainty even further
   by introducing the element of multiple imperfect observers
   of these parallel events. Properties of such systems are
   difficult to reason about, and in some cases, attempts to
   prove safety or liveness lead to ambiguities. We present a
   survey of challenges of reasoning about properties of
   concurrent systems. We then propose a new approach,
   view\-centric reasoning, that avoids the problem of
   translating concurrency into a se\-quential representation.
   Finally. we demonstrate the usefulness of view\-centric
   reasoning as a framework for disambiguating the meaning of
   tuple space predicate operations, versions of which exist
   commercially in IBM*s T Spaces and Sun*s JavaSpaces.

%T A Graphical Modeling Language for Specifying Concurrency based on CSP
%A Gerald H. Hilderink
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X In this paper, we introduce a graphical specification
   language for modeling concurrency in software design. The
   language notations are derived from CSP and the resulting
   designs form so\-called CSP diagrams. The notations reflect
   data\-flow aspects, control\-flow aspects, and they reflect
   CSP algebraic expressions that can be used for formal
   analysis. The designer does not have to be aware of the
   underlying mathematics. The techniques and rules presented
   provide guidance to the development of concurrent software
   architectures. One can detect and reason about compositional
   conflicts (errors in design), potential deadlocks (errors at
   run\-time), and priority inversion problems (performance
   burden) at a high level of abstraction. The CSP diagram
   collaborates with object\-oriented and structured methods.
   The CSP diagram is UMLable and can be presented as a new
   process diagram for the UML to capture concurrent,
   real\-time, and event\-flow oriented software architectures.
   The extension to the UML is not presented in this paper.

%T The \[rs]Honeysuckle\[rs] Programming Language: Event and Process
%A Ian R. East
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X A new language for programming systems with Communicating
   Process Architecture is introduced which builds upon the
   success of occam. Some of the principal objectives are
   presented and justified. The means employed to express
   behaviour are then described, including a transfer
   primitive, which conveys object ownership as well as value,
   and an alternation construct. The latter replaces PRI PAR
   and PRI ALT, and affords explicit expression of
   conflict\-free prioritized reactive (event\-driven)
   behaviour, including exception response. HPL also offers
   source\-code modularity, object encapsulation, and the
   recursive definition of both object and process. Despite
   such ambition, a primary aim has been to retain simplicity
   in abstraction, expression, and implementation.

%T A Communicating Threads Case Study: JIWY
%A Jan F. Broenink, Gerald H. Hilderink, Dusko S. Jovanovic
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X We strive to allow a control system designer the power of
   designing control computer code concurrently and generating
   it efficiently, in spite of her or his lack of skills in
   software engineering. This is important for many reasons.
   Nowdays, it is impossible to separate control engineering
   from software engineering. There is no way of implementing
   control strategies other than to transform them into
   computer code for the chosen processing target. Usually,
   there are not so many general\-purpose programmers available
   in control engineering research teams in companies and
   universities. In these cases, software development
   techniques suffer from insufficient knowledge in disciplines
   of software modelling, concurrency, reusability and testing.
   This paper develops a case study whose solution is based
   upon the CSP principles supported by the Communicating
   Threads libraries developed at Twente and argues why the
   techniques are accessible to non\-computing\-specialist
   control engineers.

%T Prioritised Dynamic Communicating Processes \- Part I
%A Frederick R. M. Barnes, Peter H. Welch
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X This paper reports continuing research on language design,
   compilation and kernel support for highly dynamic concurrent
   reactive systems. The work extends the occam multiprocessing
   language, which is both sufficiently small to allow for easy
   experimentation and sufficiently powerful to yield results
   that are directly applicable to a wide range of industrial
   and commercial practice. Classical occam was designed for
   embedded systems and enforced a number of constraints * such
   as statically pre\-determined memory allocation and
   concurrency limits * that were relevant to that generation
   of application and hardware technology. Most of these
   constraints have been removed in this work and a number of
   new facilities introduced (channel structures, mobile
   channels, channel ends, dynamic process creation, extended
   rendezvous and process priorities) that significantly
   broaden occam*s field of application and raise the level of
   concurrent system design directly supported. Four principles
   were set for modifications/enhancements of the language.
   They must be useful and easy to use. They must be
   semantically sound and policed (ideally, at compile\-time)
   to prevent mis\-use. They must have very lightweight and
   fast implementation. Finally, they must be aligned with the
   concurrency model of the original core language, must not
   damage its security and must not add (significantly) to the
   ultra\-low overheads. These principles have all been
   observed. All these enhancements are available in the latest
   release (1.3.3) of KRoC, freely available (GPL/open source)
   from: http://www.cs.ukc.ac.uk/projects/ofa/kroc/.

%T Prioritised Dynamic Communicating Processes \- Part II
%A Frederick R. M. Barnes, Peter H. Welch
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X This paper illustrates the work presented in \[rs]Part
   I\[rs], giving additional examples of use of channel\-types,
   extended rendezvous and FORKs that lean towards real
   applications. Also presented are a number of other additions
   and extensions to the occam language that correct, tidy up
   or complete facilities that have long existed. These include
   fixing the PRI ALT bug, allowing an unconditional SKIP guard
   as the last in a PRI ALT, replicator STEP sizes, run\-time
   computed PAR replication counts, RESULT parameters and
   abbreviations, nested PROTOCOL definitions, inline array
   constructors and parallel recursion. All are available in
   the latest release (1.3.3) of KRoC, freely available
   (GPL/open source) from:
   http://www.cs.ukc.ac.uk/projects/ofa/kroc/.

%T Implementing a Distributed Algorithm for Detection of Local Knots and Cycles in Directed Graphs
%A Geraldo Pereira de Souza, Gerson Henrique Pfitscher
%E James S. Pascoe, Roger J. Loader, Vaidy S. Sunderam
%B Communicating Process Architectures 2002
%X In general, most deadlocks take form of cycles (in database
   systems) and knots (in communication systems). Boukerche and
   Tropper have proposed a distributed algorithm to detect
   cycles and knots in generic graphs. Their algorithm has a
   message complexity of 2m vs. (at least) 4m for the Chandy
   and Misra algorithm, where m is the number of links in the
   graph, and requires O (n log n) bits of memory, where n is
   the number of nodes. We have implemented Boukerche\[rs]s
   algorithm. Our implementation of the algorithm is based on
   the construction of processes of the CSP model. The
   implementation was done using JCSP, an implementation of CSP
   for Java.

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.