Welch, P.H. and Martin, J.M.R.
(2000)
Formal Analysis of Concurrent Java Systems.
In: Communicating Process Architectures 2000, sep, 2000, Canterbury, UK.
Abstract
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 dif�culties 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
con�dence boost. Further, automated model-checking tools can be used to root
out dangerous states (such as deadlock and livelock), �nd overlooked race hazards
and prove equivalence between algorithms (e.g. between optimised and unoptimised
versions). A case study using the CSP model to prove the correctness of the JCSP
and CTJ channel implementations (which are built using standard Java monitor synchronisation)
is presented. In addition, the JCSP mechanism for ALTing (i.e. waiting
for and, then, choosing between multiple events) is veri�ed. Given the history of
erroneous implementations of this key primitive, this is a considerable relief.
- Depositors only (login required):
![[img]](http://kar.kent.ac.uk/style/images/fileicons/application_pdf.png)
