Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/41610
Title: Specifying multithreaded Java semantics for program verification
Authors: Roychoudhury, A. 
Mitra, T. 
Issue Date: 2002
Source: Roychoudhury, A.,Mitra, T. (2002). Specifying multithreaded Java semantics for program verification. Proceedings - International Conference on Software Engineering : 489-499. ScholarBank@NUS Repository.
Abstract: The Java programming language supports multithreading where the threads interact among themselves via read/write of shared data. Most current work on multithreaded Java program verification assumes a model of execution that is based on interleaving of the operations of the individual threads. However, the Java language specification (which any implementations of Java multithreading must follow) supports a weaker model of execution, called the Java Memory Model (JMM). The JMM allows certain reordering of operations within a thread and thus permits more behaviors than the interleaving based execution model. Therefore, programs verified by assuming interleaved thread execution may not behave correctly for certain Java multithreading implementations. The main difficulty with the JMM is that it is informally described in an abstract rule-based declarative style, which is unsuitable for formal verification. In this paper, we develop an equivalent formal executable specifications of the JMM. Our specification is operational and uses guarded commands. We then use this executable model to verify popular software construction idioms (commonly used program fragments/patterns) for multithreaded Java. Our prototype verifier tool detects a bug in the widely used "Double-Checked Locking" idiom, which verifiers based on interleaving execution model cannot possibly detect.
Source Title: Proceedings - International Conference on Software Engineering
URI: http://scholarbank.nus.edu.sg/handle/10635/41610
ISSN: 02705257
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Page view(s)

26
checked on Dec 9, 2017

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.