Paper Details

%T Formal Analysis of Concurrent Java Systems
%A Peter H. Welch, Jeremy M. R. Martin
%E Peter H. Welch, André W. P. Bakkers
%B Communicating Process Architectures 2000
%X Java threads are synchronised through primitives based upon
   monitor concepts developed in the early 1970s. The semantics
   of Java\[rs]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
   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 verified. Given the history of
   erroneous implementations of this key primitive, this is a
   considerable relief.

If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.

Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.