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 library was developed over the past two years by Peter Welch (P.H.Welch@ukc.ac.uk) and Paul Austin (email@example.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).
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.