A CSP model for Java']Java multithreading

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 paper remedies this with a simple and formal CSP model. In view of the difficulties encountered in reasoning about any non-trivial interactions between Java threads, being able to perform that reasoning in a formal context (where careless errors can be highlighted by mechanical checks) should be a considerable confidence boost. Further automated model-checking tools can be used to root out dangerous states (such as deadlock and livelock), find overlooked race hazards and prove equivalence between algorithms (e.g. between optimised and un-optimised versions). A case study using the CSP model to prove the correctness of the JCSP channel implementation (which is built in terms of standard Java monitor synchronisations) is presented.