Concurrency is thought to be an advanced topic – much harder than
serial computing which, therefore, needs to be mastered first. This paper
contends that this tradition is wrong, which has radical implications for
the way we educate people in Computer Science – and on how we apply what
we have learnt.
A process-oriented design pattern for concurrency is presented with a specific binding for Java. It is based on the algebra of Communicating Sequential Processes (CSP) [1, 2, 3] as captured by the JCSP [4, 5, 6, 7, 8, 9] library of Java classes. No mathematical sophistication is needed to master it. The user gets the benefit of the sophistication underlying CSP simply by using it. Those benefits include the simplification wins we always thought concurrency should generate.
Although the Java binding is new, fifteen years of working with students at Kent have shown that the ideas within process-oriented design can be quickly absorbed and applied. Getting the ideas across as soon as possible pays dividends – the later it's left, the more difficult it becomes to wean people off serial ways of thought that fit the world so badly. Concurrency for all (and for everyday use) in the design and implementation of most kinds of computer system is both achievable and necessary.
Safety critical systems, however, need some mechanical backup to intuitive reasoning about design - even when that design is based on CSP principles. Fortunately, CSP algebra of allows us to make formal specifications of systems (and all their components) and to verify the correctness of a range of increasingly refined implemenations. This tutorial describes how this is done and also presents two commercially available tools (Probe and the FDR model checker from Formal Systems Europe). Experience of undergraduate teaching using these tools is given.
Keywords: components, processes, channels, design patterns, Java™, CSP, JCSP, CTJ, Probe, FDR.