2004 Proceedings details

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's discovery that data independence can be used for this purpose.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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'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.

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.

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.

CSP, Hoare's Communicating Sequential Processes, is one of the formalisms that underpins the antecedents of CPA, and this year celebrates its Silver Jubilee. Formal Systems' 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.

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.

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.

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.

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' 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.

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.

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.

View-Centric Reasoning (VCR) replaces CSP'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's Unifying Theories of Programming. Initial efforts in this direction led to a comparison of VCR with Lawrence'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.

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.

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'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.