WoTUG - The place for concurrent processes

Refer Proceedings details


%T Handel\-C++ \- Adding Syntactic Support to C++
%A Alex Cole
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012


%T Implementation of an Agent\-based Model with TBB Technique
%A Ye Li
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012


%T Unfinished Business \- occam\-pi²
%A Peter H. Welch
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012


%T JCircus Demo
%A S.L.M. Barrocas, Marcel Oliveira
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012


%T Developing JIWY using TERRA
%A Maarten M. Bezemer, Robert J.W. Wilterdink, Jan F. Broenink
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012


%T Polyphonic Processors \- Fantasy on an FPGA
%A Richard Miller
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012


%T A CPA Series
%A Ian R. East
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012


%T Cancellable Servers \- a Pattern for Curiousity
%A Peter H. Welch
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012


%T Designing a Concurrent File Server
%A James Whitehead
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X In this paper we present a design and architecture for a
   concurrent file system server. This architecture is a
   compromise between the fully concurrent V6 UNIX
   implementation, and the simple sequential implementation in
   the MINIX operating system. The design of the server is made
   easier through the use of a disciplined model of
   concurrency, based on the CSP process algebra. By viewing
   the problem through this restricted lens, without
   traditional explicit locking mechanisms, we can construct
   the system as a process network of components with
   explicit connections and dependencies. This provides us with
   insight into the problem domain, and allows us to analyse
   the issues present in concurrent file system implementation.


%T JCircus 2.0: an Extension of an Automatic Translator from Circus to Java
%A S.L.M. Barrocas, Marcel Oliveira
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X The use of formal methods in the development of concurrent
   systems considerably reduces the complexity of specifying
   their behaviour and verifying properties that are inherent
   to them. Development, however, targets the generation of
   executable programs; hence, translating the final
   specification into a practical programming language
   becomes imperative. This translation is usually rather
   problematic due to the high probability of introducing
   errors in manual translations: the mapping from some of the
   original concepts in the formal concurrency model into a
   corresponding construct in the programming language
   is non\-trivial. In recent years, there is a growing effort
   in providing automatic translation from formal
   specifications into programming languages. One of these
   efforts, JCircus, translates specifications written in
   Circus (a combination of Z and CSP) into Java programs
   that use JCSP, a library that implements most of the CSP
   constructs. The subtle differences between JCSP and Circus
   implementation of concurrency, however, imposed restrictions
   to the translation strategy and, consequently, to JCircus.
   In this paper, we extend JCircus by providing: (1) a new
   optimised translation strategy to
   multi\-way synchronisation; (2) the translation of complex
   communications, and; (3) the translation of CSP sharing
   parallel and interleaving. A performance analysis of the
   resulting code is also in the context of this paper
   and provides important insights into the practical use of
   our results.


%T A Distributed Multi\-Agent Control System for Power Consumption in Buildings
%A Anna Kosek, Oliver Gehrke
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X This paper presents a distributed controller for adjusting
   the electrical consumption of a residential building in
   response to an external power setpoint in Watts. The
   controller is based on a multi\-agent system and has been
   implemented in JCSP. It is modularly built, capable of
   self\-configuration and adapting to a dynamic environment.
   The paper describes the overall architecture and the
   design of the individual agents. Preliminary results from
   proof\-of\-concept tests on a real building are included.


%T Specification of APERTIF Polyphase Filter Bank in ClaSH
%A Rinse Wester, Dimitrios Sarakiotis, Eric Kooistra, Jan Kuper
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X ClaSH, a functional hardware description language based on
   Haskell, has several abstraction mechanisms that allow a
   hardware designer to describe architectures in a short and
   concise way. In this paper we evaluate ClaSH on a complex
   DSP application, a Polyphase Filter Bank as it is used in
   the ASTRON APERTIF project. The Polyphase Filter Bank
   is implemented in two steps: first in Haskell as being close
   to a standard mathematical specification, then in ClaSH
   which is derived from the Haskell formulation by applying
   only minor changes. We show that the ClaSH formulation can
   be directly mapped to hardware, thus exploiting the
   parallelism and concurrency that is present in the
   original mathematical specification.


%T Schedulability Analysis of Timed CSP Models Using the PAT Model Checker
%A Oguzcan Oguz, Jan F. Broenink, Angelika Mader
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X Timed CSP can be used to model and analyse real\-time and
   concurrent behaviour of embedded control systems. Practical
   CSP implementations combine the CSP model of a real\-time
   control system with prioritized scheduling to achieve
   efficient and orderly use of limited
   resources. Schedulability analysis of a timed CSP model of a
   system with respect to a scheduling scheme and a particular
   execution platform is important to ensure that the system
   design satisfies its timing requirements. In this paper, we
   propose a framework to analyse schedulability of CSP\-based
   designs for non\-preemptive fixed\-priority
   multiprocessor scheduling. The framework is based on the PAT
   model checker and the analysis is done with dense\-time
   model checking on timed CSP models. We also provide a
   schedulability analysis workflow to construct and analyse,
   using the proposed framework, a timed CSP model with
   scheduling from an initial untimed CSP model without
   scheduling. We demonstrate our schedulability analysis
   workflow on a case study of control software design for a
   mobile robot. The proposed approach
   provides non\-pessimistic schedulability results.


%T Supporting Timed CSP Operators in CSP++
%A W. B. Gardner, Yuriy Solovyov
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X CSP++ is an open\-source code synthesis tool consisting of a
   translator for a subset of CSPm and a C++ run\-time
   framework. Version 5.0 now supports Timed CSP
   operators\-\-timed interrupt, timed timeout, and
   timed prefix\-\-as well as untimed variants of interrupt and
   timeout, with only 1% additional execution and memory
   overhead, though using interrupts is more costly. We
   describe the implementation and performance of the
   new operators, illustrating their use with a robot\-vacuum
   cleaner case study. The tool thus becomes more useful for
   specifying the behaviour of soft real\-time systems, and
   generating a timing\-enabled executable program from its
   formal model.


%T A Comparison of Message Passing Interface and Communicating Process Architecture Networking Communication Performance
%A Kevin Chalmers
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X Message Passing Interface (MPI) is a popular approach to
   enable Single Process, Multiple Data (SPMD) style parallel
   computing, particularly in cluster computing environments.
   Communicating Process Architecture (CPA) Networking on the
   other hand, has been developed to enable channel
   based semantics across a communication mechanism in a
   transparent manner. However, in both cases the concept of a
   message passing infrastructure is fundamental. This paper
   compares the performance of both of these frameworks at a
   base communication level, also discussing some of
   the similarities between the two mechanisms. From the
   experiments, it can be seen that although MPI is a more
   mature technology, in many regards CPA Networking can
   perform comparably if the correct communication is used.


%T Beauty And The Beast: Exploiting GPUs In Haskell
%A Alex Cole, Alistair A. McEwan, Geoff Mainland
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X In this paper we compare a Haskell system that exploits a
   GPU back end using Obsidian against a number of other
   GPU/parallel processing systems. Our examples demonstrate
   two major results. Firstly they show that the Haskell
   system allows the applications programmer to exploit GPUs in
   a manner that eases the development of parallel code
   by abstracting from the hardware. Secondly we show that the
   performance results from generating the GPU code from
   Haskell are acceptably comparable to expert hand written GPU
   code in most cases; and permit very significant performance
   benefits over single and multi\-threaded implementations
   whilst maintaining ease of development. Where our results
   differ from expert hand written GPU (CUDA) code we consider
   the reasons for this and discuss possible developments that
   may mitigate these differences. We conclude with a
   discussion of a domain specific example that benefits
   directly and significantly from these results.


%T A Debugger for Communicating Scala Objects
%A Andrew Bate, Gavin Lowe
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X This paper presents a software tool for visualising and
   reasoning about the behaviour of message\-passing concurrent
   programs built with the CSO library for the Scala
   programming language. It describes the models needed to
   represent the construction of process networks and the
   runtime behaviour of the resulting program. We detail the
   manner in which information is extracted from the use of
   concurrency primitives in order to maintain these models and
   how these models are diagrammed. Our implementation of
   dynamic deadlock detection is explained. The tool
   can produce a sequence diagram of process communications,
   the communication network depicting the pairs of processes
   which share a communication channel, and the trees resulting
   from the composition of processes. Furthermore, it allows
   for behavioural specifications to be defined and then
   checked at runtime, and guarantees to detect the illegal
   usage of concurrency primitives that could otherwise lead to
   deadlock or data loss. Our implementation imposes only a
   small overhead on the program under inspection.


%T XCHANs: Notes on a New Channel Type
%A Øyvind Teig
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X This paper proposes a new channel type, XCHAN, for
   communicating messages between a sender and receiver.
   Sending on an XCHAN is asynchronous, with the sending
   process informed as to its success. XCHANs may be buffered,
   in which case a successful send means the message has got
   into the buffer. A successful send to an unbuffered XCHAN
   means the receiving process has the message. In either case,
   a failed send means the message has been discarded. If
   sending on an XCHAN fails, a built\-in feedback channel (the
   x\-channel, which has conventional channel semantics) will
   signal to the sender when the channel is ready for input
   (i.e., the next send will succeed). This x\-channel may be
   used in a select or ALT by the sender side (only
   input guards are needed), so that the sender may passively
   wait for this notification whilst servicing other events.
   When the x\-channel signal is taken, the sender should send
   as soon as possible \-\- but it is free to send something
   other than the message originally attempted (e.g.
   some freshly arrived data). The paper compares the use of
   XCHAN with the use of output guards in select/ALT
   statements. XCHAN usage should follow a design pattern,
   which is also described. Since the XCHAN never blocks, its
   use contributes towards deadlock\- avoidance. The XCHAN
   offers one solution to the problem of overflow handling
   associated with a fast producer and slow consumer in message
   passing systems. The claim is that availability of XCHANs
   for channel based systems gives the designer and programmer
   another means to simplify and increase quality.


%T A High Performance Reconfigurable Architecture for Flash File Systems
%A Irfan Mir, Alistair A. McEwan, Neil J. Perrins
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X NAND flash memory is widely adopted as the primary storage
   medium in embedded systems. The design of the flash
   translation layer, and exploitation of parallel I/O
   architectures, are crucial in achieving high performance
   within a flash file system. In this paper we present our new
   FPGA based flash management framework using
   reconfigurable computing that supports high performance
   flash storage systems. Our implementation is in Verilog, and
   as such enables us to design a highly concurrent system at a
   hardware level in both the flash translation layer and the
   flash controller. Results demonstrate that implementing the
   flash translation layer and flash controller directly in
   hardware, by exploiting reconfigurable computing, permits us
   to exploit a highly concurrent architecture that leads to
   fast response times and throughput in terms of read/write
   operations.


%T Design and Use of CSP Meta\-Model for Embedded Control Software Development
%A Maarten M. Bezemer, Robert J.W. Wilterdink, Jan F. Broenink
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X Software that is used to control machines and robots must be
   predictable and reliable. Model\-Driven Design (MDD)
   techniques are used to comply with both the technical and
   business needs. This paper introduces a CSP meta\-model that
   is suitable for these MDD techniques. The
   meta\-model describes the structure of CSP models that are
   designed; using this meta\-model it is possible to use all
   regular CSP constructs when constructing a CSP model. The
   paper also presents a new tool suite, called TERRA, based on
   Eclipse and its frameworks. TERRA contains a graphical CSP
   model editor (using the new CSP meta\-model),
   model validation tools and code generation tools. The model
   validation tools check whether the model conforms to the
   meta\-model definition as well as to additional rules.
   Models without any validation problems result in proper code
   generation, otherwise the developer needs to address
   the found problems to be sure code generation will succeed.
   The code generation tools are able to generate CSPm code
   that is readable by FDR and to generate C++/LUNA code that
   is executable on embedded targets. The meta\-model and the
   TERRA tool suite are tested by designing CSP models for
   several of our laboratory setups. The generated C++/LUNA
   code for the laboratory setups is able to control them as
   expected. Additionally, the paper contains an example model
   containing all supported CSP constructs to show the CSPm
   code generation results. So it can be concluded that the
   meta\-model and TERRA are usable for these kind of tasks.


%T Exception Handling and Checkpointing in CSP
%A Mads Ohm Larsen, Brian Vinter
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X This paper describes work in progress. It presents a new way
   of looking at some of the basics of CSP. The primary
   contributions is exception handling and checkpointing of
   processes and the ability to roll back to a known
   checkpoint. Channels are discussed as communication
   events which is monitored by a supervisor process. The
   supervisor process is also used to formalise poison and
   retire events. Exception handling and checkpointing are
   used as means of recovering from an catastrophe.
   The supervisor process is central to checkpointing and
   recovery as well. Three different kind of exception handling
   is discussed: fail\-stop, retire\-like fail\-stop, and check
   pointing. Fail\-stop works like poison, and retire\-like
   fail\-stop works like retire. Checkpointing works
   by telling the supervisor process to roll back both
   participants in a communication event, to a state
   immediately after their last successful communication. Only
   fail\-stop exceptions have been implemented in PyCSP to this
   point.


%T occam Obviously
%A Peter H. Welch
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X This talk explains and tries to justify a range of questions
   for which its title is the answer. It reviews the history of
   occam: its underlying philosophy (Occam\[rs]s Razor), its
   semantic foundation on Hoare\[rs]s CSP, its principles of
   process oriented design and its development over
   almost three decades into occam\-pi (which blends in the
   concurrency dynamics of Milner\[rs]s pi\-calculus). Also
   presented will be its urgent need for rationalisation \-\-
   occam\-pi is an experiment that has demonstrated significant
   results, but now needs time to be spent on careful
   review and implementing the conclusions of that review.
   Finally, the future is considered. In particular, how do we
   avoid the following question being final: which language had
   the most theoretically sound semantics, the most efficiently
   engineered implementation, the simplest and most pragmatic
   concurrency model for building complex systems ... and
   was mostly forgotten (even as its ideas are slowly and
   expensively and painfully being reinvented piece\-by\-piece,
   as they must be)?


%T Process\-Oriented Building Blocks
%A Adam T. Sampson
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X Intel\[rs]s Threading Building Blocks library provides an
   efficient, work\-stealing lightweight task scheduler, along
   with a high\-level task\-based API for parallel programming
   in C++. This presentation shows how TBB\[rs]s scheduler can
   be used (without modification) to implement blocking
   process\-oriented concurrent systems, and discusses the
   advantages and disadvantages of this approach.


%T Data Escape Analysis for Process Oriented Systems
%A Martin Ellis, Frederick R. M. Barnes
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X Escape analysis, the technique of discovering the boundaries
   of dynamically allocated objects, is a well explored
   technique for object\-orientated languages (such as Java and
   C++) and stems from the functional programming community. It
   provides an insight into which objects interact directly
   (and indirectly) and can inform program correctness
   checking, or be used for directing optimisations
   (e.g. determining which objects can safely be allocated on a
   function\-local stack). For process\-oriented languages such
   as occam\-pi and Google\[rs]s Go, we have explored mobile
   escape analysis, that provides concise information about the
   movement of objects (mobiles) within networks
   of communicating processes. Because of the distinction
   between processes (as execution contexts) and objects
   (dynamically allocated data, channels and processes),
   combined with strict typing and aliasing rules, the analysis
   is somewhat simpler then for less strict languages.
   This analysis is only concerned with dynamically allocated
   blocks of memory \-\- it does not give any consideration for
   the data contained within these. However, knowing the extent
   to which data (statically or dynamically allocated) escapes
   within a network of communicating processes is arguably
   useful \-\- and is not necessarily a superset of mobile
   escape. The fringe presentation describes an extension to
   the mobile escape model that seeks to capture semantic
   information about the data escape of a process\-oriented
   system. This provides richer semantic information about a
   process\[rs]s behaviour (that can be used in verification)
   and has clear application to security (e.g. by demonstrating
   that particular data does not escape a set of communicating
   processes).


%T SEU Protection for High\-Reliability Flash File Systems
%A Neil J. Perrins, Alistair A. McEwan
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X Single Event Upsets (SEU) are a primary reliability concern
   for electronics in high radiation, highly hostile
   environments such as space. In the case of Field
   Programmable Gate Arrays, the concern is firstly that data
   stored in RAM can be corrupted, and secondly
   that configurable logic blocks can become damaged or
   corrupted. In this talk we will present our considerations
   of this problem in the context of an SRAM\-based high
   reliability flash file system. We will firstly demonstrate
   our test harness where we simulate the injection of
   SEUs into our FPGA. We will then discuss how we propose to
   build a self repairing configuration using triple modular
   redundancy and partial dynamic reconfiguration. Finally we
   will discuss how the reliability of the system may be tested
   and measured such that it can be used with confidence in
   either data acquisition or control system applications
   in rad\-hard environments.


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!