Introduction
Concurrency is important to much of computation:from computing in the
large (networks and their distributed systems−like an airline-reservation system) to computing in the small (VLSI chips and their parallel algorithms
like image-processing chips). Because of the complex manner in which coordinating components interact, we use formal methods for the specification,
development and simulation of such systems.
This course introduces and uses Hoare's notation CSP (for Communicating Sequential Processes), a kind of process algebra. The syntax of CSP is
shown to be natural and convenient for describing reactive state-based behaviour and for combining those behaviours in parallel. Emphasis is given
to the use of laws for deciding when two behaviours are equivalent, which
results in an algebraic theory of processes. But to complement that algebraic
approach, a hierarchy of semantic models is studied to provide progressively
more-detailed information about the way a process interacts with its environment. A system can be specified by a semantic property (at an appropriate
level of abstraction) and implemented by an algebraic process meeting that
property. The tool FDR (for failures/divergences refinement) enables such
implementations to be model checked. This part of the course is supported by
a set of exercises and practicals, integral to an understanding of the material.
The last part of the course−if time and number of participants allow
consists of case studies, worked through and presented by participants in
groups, either from papers, the texts, or by applying the ideas of the course
to their own work. Examples might be chosen from communication protocols, hardware design, deadlock analysis, real time, transaction processing,
security, or a variety of design studies.
Synopsis
Introduction and Overview
Identifying the issues that confront the study of concurrency; overview of the
course, demonstrated on the example of an interactive game.
Processes
Alphabets, events, prefix, recursion, choice, mutual recursion, state machines, laws.
Exercise Session 1 (preliminary).
Internal and external choice
Internal (nondeterministic) choice, distributivity, external (deterministic) choice,
conditional choice.
Traces
Finite traces, catenation, head, tail, star, prefix, length, laws, after, process
specifications, the domain of traces.
Exercise Session 2.
Concurrency
Interaction, concurrency, laws, dining philosophers, deadlock.
Interleaving and Relabelling
Interleaving, generalised parallel composition, change of symbol, process relabelling, dining philosophers resolved.
Exercise Session 3.
Abstraction
Hiding (concealment), timeout, divergence, laws.
Semantics of Nondeterministic Processes
Specifications, divergence, failure semantics, refinement, the domain of processes.
Exercise Session 4.
Communication
Input, output, communication, buffers, pipes, laws.
Sequential Processes
Termination, tick, sequential composition, grammars, assignment, laws.
Exercise Session 5.
Case Study: Communications protocols
The stop-and-wait, alternating-bit and sliding-window protocols.
Exercise Session 6.
FDR model checking.
Exercise Session 7: FDR practical.
Group case studies.
Presentation of case studies by groups.
References
Lecture overheads on CSP.
J. W. Sanders.
Communicating Sequential Processes.
C. A. R. Hoare,
Prentice-Hall International, 1985.
Available free on-line.
The Theory and Practice of Concurrency.
A. W. Roscoe,
Prentice-Hall, 1998.
Available free on-line.
Lecturer: J. W. Sanders
J.W. Sanders is Principal Research Fellow at the International Institute for Software Technology, United Nations University, Macao, China. His interests lie largely in the application of rigorous methods to model, and hence reason about, novel and/or intractible forms of Computation: concurrency, probabilism, security, time, asynchronicity, quantum computation and multi-agent systems.Dr Sanders holds degrees in Mathematics from Monash University and the Australian National University. He has taught across the range of undergraduate and graudate courses in Pure Mathematics and Computer Science, and has taught courses in China, Africa, Iran and Malaysia. He has supervised numerous MSc and PhD students. Before moving to Macao he spent 22 years at the Programming Research Group, Oxford, and is now an emeritus fellow of Lady Margaret Hall, Oxford.
