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/