CSP for Java CSP for Java (JCSP) Background Communicating Sequential Processes (CSP) is a mathematical theory for specifying and verifying complex patterns of behaviour arising from interactions between concurrent objects. It has a formal, and compositional, semantics that is in line with our intuition about the way things work It encapsulates fundamental principles of processes, networks and communication. It is semantically defined in terms of a structured mathematical model and sufficiently expressive to enable reasoning about deadlock and livelock. Abstraction and refinement are central to the underlying theory, so that CSP models can track the full life-cycle of systems - including those where software and hardware developments are interdependent. Robust and commercially supported software engineering tools exist for formal verification. Ultra-lightweight kernels have been developed for CSP primitives yielding sub-microsecond overheads for context switching, process creation and shutdown, synchronised channel communication and safe shared-memory locks. And, finally, some mainstream programming languages directly support the CSP model, whilst CSP-style libraries are available for other languages (such as Java). Support for this last aspect is the subject of this note. The monitor-threads model provided by Java, whilst easy to understand, proves very difficult to apply safely in any system above a modest level of complexity. One problem is that monitor methods are tightly interdependent, so that their semantics compose in non-trivial ways - indeed, the whole skill in multi-threaded Java programming lies in setting up and staying in control of these complex interactions. On the other hand, parallel composition of CSP processes is mathematically clean, yields no engineering surprises and scales well with system complexity. Java textbooks, on-line tutorials and other web sites (e.g. those associated with the Java Swing library) go out of their way to emphasise the difficulties of its multithreading - race hazards, deadlock, livelock and process starvation. Engineers are warned off using it if they possibly can. However, to enable high performance and low latency responses, concurrency cannot always be avoided. We contend that concurrency is too natural a concept and too good a tool to be set aside in system design and implementation and that we should not be frightened to use it to simplify both these tasks. If concurrency is making life harder, maybe we are using the wrong kind of concurrency ... The JCSP Library JCSP is a (100% pure) Java class library providing a base range of CSP primitives plus a rich set of extensions - some of the latter being experimental at the moment. Also included is a package providing CSP process wrappers giving a channel interface to all Java AWT widgets and graphics operations. It is extensively (javadoc)umented and includes much teaching. The library was developed over the past two years by Peter Welch (P.H.Welch@ukc.ac.uk) and Paul Austin (p_d_austin@hotmail.com), from the University of Kent at Canterbury, in consultation with the CSP and occam/transputer communities. An early version (0.5beta) was released in June 1998. The latest version (1.0-rc1) is available from http://www.cs.ukc.ac.uk/projects/ofa/jcsp/. This represents a significant advance on 0.5beta in terms of facilities, formal verification, documentation, demonstration and educational support. JCSP 1.0 (Release Candidate 1) was released in early November, 1999, coinciding with publication of the 2nd. edition of Doug Lea's book: `Concurrent Programming in Java : Design Principles and Patterns (Java Series) ' - the bible for people wrestling with multithreading problems/patterns in Java. This 2nd. edition has a new final section presenting the fundamental CSP concepts and uses the JCSP library for its examples. The formal 1.0 release will happen soon, following a short external review. Teaching material will be available from the above web-site giving a non-mathematician's overview of the CSP model and its use for system design and implementation. JCSP shows how the model has been bound into the Java programming language. Implemented as a library of packages, this enables multithreaded systems to be designed, implemented and reasoned about entirely in terms of CSP synchronisation primitives (channels, events, etc.) and constructors (parallel, choice, etc.). This allows 20 years of theory, design patterns (with formally proven good properties - such as the absence of race hazards, deadlock, livelock and thread starvation), tools supporting those design patterns, education and experience to be deployed in support of Java-based multithreaded applications. There are two considerations to make when building this kind of infrastructure. The first is the quality of the model given to end-users: how easy is it to use and how easy is it to use safely (precluding nasty things like race hazards etc.). The second is the lightness of that model: too heavy a model (e.g. Ada tasking) and it can only be used in restricted circumstances. Parallel composition of CSP processes is mathematically clean, yields no engineering surprises and scales well with system complexity. We do not have to be mathematically sophisticated to use CSP. That sophistication is pre-engineered into the primitives and operators of CSP. The user gains automatically from this, noticing through simpler designs that are quicker to build and easier to maintain. CSP rates serious consideration as a basis for concurrent applications in Java - especially if there are real-time or safety-critical demands. It scores well for both quality (robustness, ease of use, management of complexity) and lightness (CSP kernels with sub-microsecond overheads exist - ongoing work is binding this into JVMs to support JCSP). A CSP Model for Standard Java Monitors A CSP model for the standard Java monitor/threads operations (synchronized, wait, notify and notifyAll) has been developed - this will also be made available from the JCSP web site. This enables any Java threaded system to be analysed in CSP terms. In particular, it opens Java systems to formal verification of deadlock/livelock freedom - employing, if necessary commercially supported CSP verification tools (such as FDR from Formal Systems Ltd., a spin-off company from Oxford University Computing Laboratory - see http://www.formal.demon.co.uk/FDR2.html). Confidence has been gained in this model through the formal proof of correctness of the JCSP channel implementation. The latter is a non-trivial application of Java monitors. The model transforms this into an even more complex system of CSP processes. Using FDR, that system has been proved to be a refinement of a simple CSP channel and vice versa. Hence, a JCSP channel and CSP channel are equivalent. Thanks are owed to Jeremy Martin (Jeremy.Martin@comlab.ox.ac.uk) for this proof. So far, only the JCSP channel has been subject to this formal analysis. It would be a great boost to confidence to extend this to other JCSP primitives. It would also be interesting to subject other Java libraries (or applications) and see how they stand up. That might also have financially interesting consequences. Of course, the analysis of CSP designs implemented in Java by a formally proven correct JCSP library would be simple and direct. www.cs.ukc.ac.uk/projects/ofa/jcsp/
