Event: Logic and Semantics Seminar, University of Cambridge Computer Laboratory  (16th. March, 2000)

Title: "A CSP Model for Java Threads (and Vice-Versa)"

Speaker: Peter Welch, University of Kent at Canterbury


[This talk aims at *practical* help for those trying to work with Java's given concurrency model - threads and monitors.  I tried and it hurt and I really needed this kind of help.  The talk will present some basic CSP ideas, Java's threads ideas and map them on to each other.  This will be done mainly through pictures ... only a very few special symbols and only a very few CSP equations (which, in any case, will be presented as simple serial programming).  The final proofs of correctness of the various JCSP (the CSP class library for Java) primitives will be presented entirely by picture.  This talk is not aimed at mathematicians ...]

Java threads are synchronised through primitives based upon monitor concepts developed in the early 1970s.  The semantics of Java's primitives have only been presented in natural language - this talk offers a simple and formal CSP model.  In view of the difficulties encountered in reasoning about almost any non-trivial interactions between Java threads, being able to perform that reasoning in a formal context (where careless errors can be exposed by mechanical checks) should be a considerable confidence boost.  Further, model-checking tools can root out dangerous states (such as deadlock and livelock), find overlooked race hazards and prove equivalence between algorithms.

This work was motivated be pressing practical concerns.  The JCSP library, which provides an occam3-like communicating process model for Java, builds channel, choice and parallel constructs on top of Java monitors (it is 100% pure Java and runs on any JVM).  The original implementation logic was published, presented many times to Java-literate seminars and unchallenged. Yet, after two years trouble-free use, its ALTing mechanism (which waits for and chooses between multiple events) was found to contain a race condition that led (in very rare and highly stressed circumstances) to erroneous deadlock.  Analysis of the code, using the FDR model checker and this CSP definition for Java monitor operations, shows up the deadlock in seconds. This talk outlines how this is done, together with a formal verification of the now "corrected" implementation.

Ideas from this talk are relevant to other threading libraries and languages, such as Microsoft's new C#.  Open questions challenging some of the basic principles of Object Orientation (from the point-of-view of communicating processes) will be raised ... if time allows.

[The work reported in this talk is joint with Jeremy Martin, who used to work  for the Oxford Supercomputing Centre and is now at Oxagen, Oxford.]

The latest version of JCSP may be downloaded from http://www.cs.ukc.ac.uk/projects/ofa/jcsp/


This talk is based upon the following two papers: The second paper extends the first to include verification of the 2-way ALT primitive of JCSP.  Source code for the full n-way ALT is given in that paper.