Abstract Concurrency is beginning to be accepted as a core knowledge area in the undergraduate CS curriculum—no longer isolated, for example, as a support mechanism in a module on operating systems or reserved as anadvanceddiscipline for later study. Formal verification of system properties is often considered adifficultsubject area, requiring significant mathematical knowledge and generally restricted to smaller systems employing sequential logic only. This paper presents materials, methods and experiences of teaching concurrency and verification as a unified subject, as early as possible in the curriculum, so that they becomefundamentalelements of our software engineering tool kit—to be used together every day as a matter of course. Concurrency and verification should live in symbiosis. Verification is essential for concurrent systems as testing becomes especially inadequate in the face of complex non-deterministic (and, therefore, hard to repeat) behaviours. Concurrency shouldsimplifythe expression of most scales and forms of computer system by reflecting the concurrency of the worlds in which they operate (and, therefore, have to model); simplified expression leads to simplified reasoning and, hence, verification. Our approach lets these skills be developed without requiring students to be trained in the underlying formal mathematics. Instead, we build on the work of those who have engineered that necessary mathematics into the concurrency models we use (CSP, π -calculus), the model checker (FDR) that lets us explore and verify those systems, and the programming languages/libraries (occam- π , Go, JCSP, ProcessJ) that let us design and build efficient executable systems within these models. This paper introduces a workflow methodology for the development and verification of concurrent systems; it also presents and reflects on two open-ended case studies, using this workflow, developed at the authors’ two universities. Concerns analysed include safety(don’t do bad things), liveness(do good things)and low probability deadlock(that testing fails to discover). The necessary technical background is given to make this paper self-contained and its work simple to reproduce and extend.

Abstract A fine‐grained massively parallel and process‐oriented architecture for the modelling of complex systems is presented. We propose that the concurrency in the model simplifies its design and construction by directly reflecting the processes in the natural world. The architecture is based on CSP, extended with mechanisms for process mobility from the pi‐calculus; implementations are presented using the occam‐pi language. A case study, modelling platelets (possibly artificial) within a blood vessel, is described. The aim for this model is to engineer emergent behaviour: the clotting of platelets in response to a wound in the blood vessel wall and the staunching of blood loss. A three‐dimensional model is constructed, along with mechanisms for visualization and interaction. Its expressiveness and efficiency relies strongly on the dynamic and mobile capabilities of occam‐pi. General principles for the design of large and complex system models are drawn. The described case study runs to millions of processes engaged in ever‐changing communication topologies. It is free from deadlock, livelock, race hazards and starvation by design, employing a small set of synchronization patterns for which we have proven safety theorems. Compiled occam‐π codes automatically and efficiently exploit all cores in a shared‐memory multiprocessor system. They are also straightforward to distribute over standard cluster architectures. Copyright © 2007 CG Ritson & PH Welch.

Abstract Communicating Sequential Processes for Java (JCSP) is a mature library that implements CSP‐derived concurrency primitives in Java. A JCSP system is a hierarchical network of autonomous processes communicating over synchronous (optionally buffered) channels, and multiway synchronising through barriers. This paper presents a significant extension to the barrier mechanism: the fast resolution of choice between any number of barrier events, channel communications (in either direction) and timeouts. Previously, and in line with all currently released libraries and languages offering the CSP concurrency model, choice was restricted to channel inputs and timeouts. The paper demonstrates an application of alting barriers and explains the mechanisms used in their implementation that enables their use as guards in a choice. It also shows how choice over channel outputs becomes possible, as a simple consequence of having choice over barriers. Finally, an efficient implementation of CSP's broadcasting channels is presented (using a phased barrier synchronisation pattern) and a mechanism for allowing choice over these is discussed. With this extended JCSP, almost all CSP‐specified systems can now be directly implemented. The new library is available under LGPL open source. Copyright © 2010 PH Welch, NCC Brown, J Moores, KV Chalmers & B Sputh.

With the commercial development of multicore processors, the challenges of writing multithreaded programs to take advantage of these new hardware architectures are becoming more and more pertinent. Concurrent programming is necessary to achieve the performance that the hardware offers. Traditional approaches present concurrency as an advanced topic: they have proven difficult to use, reason about with confidence, and scale up to high levels of concurrency. This article reviews process-oriented design , based on Hoare's algebra of Communicating Sequential Processes (CSP), and proposes that this approach to concurrency leads to solutions that are manageable by novice programmers; that is, they are easy to design and maintain, that they are scalable for complexity, obviously correct , and relatively easy to verify using formal reasoning and/or model checkers. These solutions can be developed in conventional programming languages (through CSP libraries) or specialized ones (such as occam-π) in a manner that directly reflects their formal expression. Systems can be developed without needing specialist knowledge of the CSP formalism, since the supporting mathematics is burnt into the tools and languages supporting it. We illustrate these concepts with the Santa Claus problem , which has been used as a challenge for concurrency mechanisms since 1994. We consider this problem as an example control system, producing external signals reporting changes of internal state (that model the external world). We claim our occam-π solution is correct-by-design , but follow this up with formal verification (using the FDR model checker for CSP) that the system is free from deadlock and livelock, that the produced control signals obey crucial ordering constraints, and that the system has key liveness properties.

This paper explores a process-oriented approach to complex systems design, using massive fine-grained concurrency, mobile channels and mobile processes. The complex systems studied are self-organising, with emergent and evolving behaviours (apparent at the global level) arising from massive interactions between relatively simple components (that have only local knowledge). Classical ant foraging is used as a case study. Processes are used to represent space, environmental factors and the ants themselves. Ant processes (like all processes) only have knowledge of their internal state (looking for food, looking for their nest) and what they can glean from their local neighbourhood (by interacting with the processes making up that neighbourhood). The networks constructed are dynamic, changing as the ants move around and environmental factors are introduced and modified. The paper reports on two mechanisms for achieving this: channel mobility and process mobility. The language for implementation is occam-pi, which has the necessary concurrency mechanisms built in as fundamental primitives and whose semantics is rooted in the process algebras of CSP and the pi-calculus. Performance figures are given, including speedup curves for multicores, and some conclusions drawn.

The authors present data-flow solutions on a pipeline of transputers for banded and dense systems of linear equations using Gauss elimination and the Gauss-Jordan method, respectively. These implementations, written in occam, are especially effective when there is a continuous supply of right-hand sides to be solved with the same coefficient matrix. Attention is paid to both load balancing and resource handling within the processor elements of the pipeline. When solving multiple right-hand sides, floating-point efficiency levels on 32-processor implementations range from 110% (for dense systems) down to 90% (for banded systems), where 100% represents the peak performance attainable from a single transputer applied to the same problem (effectively back-to-back floating-point operations on data in external memory). Some conclusions are drawn on efficiency issues arising from state-of-the-art massively parallel supercomputers.

Abstract The concept of truly parallel assignment is retrieved from obscurity. It is shown to be a natural technique for the expression of iterative algorithms that saves the programmer from being concerned with some ‘low‐level’ details imposed by the von Neumann machine. With their use, algorithms should be simpler to write, clearer to understand and contain fewer errors. The concept of history as a means for achieving the same purpose is criticized on the grounds of the new side‐effects that it introduces. An implementation method for truly parallel assignment on a conventional computer is described.