A CSP Model for Java Multithreading

Welch, P.H. and Martin, J.M.R. (2000) A CSP Model for Java Multithreading. In: 5th International Symposium on Software Engineering for Parallel and Distributed Systems (PDSE 2000), Jun 10-11, 2000 , Limerick, Ireland. (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL
http://dx.doi.org/10.1109/PDSE.2000.847856

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 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.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: Threads, Monitors, CSP, Concurrency
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 30 Aug 2009 17:36
Last Modified: 30 Aug 2009 17:36
Resource URI: http://kar.kent.ac.uk/id/eprint/22014 (The current URI for this page, for reference purposes)
  • Depositors only (login required):