Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Model checking the Java metalocking algorithm
Basu S., Smolka S. ACM Transactions on Software Engineering and Methodology16 (3):12-es,2007.Type:Article
Date Reviewed: Jan 10 2008

Basu and Smolka present a case study of modeling and verifying the Java metalocking algorithm using the XMC model checker. They verify the correctness of the metalocking algorithm by manually constructing a model of the algorithm, and then performing model checking on the derived model.

The Java Virtual Machine (JVM) is often used for implementing Internet-based applications using extensive synchronization operations. Metalocking is viewed as a two-tier scheme for achieving monitor-style synchronization in objects. For the metalocking algorithm, the upper tier is used as the metalock level, while the lower tier is used as the monitor-lock level. XMC, on the other hand, is a model checker for value-passing languages such as Java. The metalock level is used to access the object’s synchronization data, and the monitor-lock level is used to access the object data. In the metalocking algorithm, threads observe a certain protocol when manipulating an object’s synchronization data.

This paper is recommended for readers interested in theorem proving using the XMC model checker.

Reviewer:  Rosziati Ibrahim Review #: CR135093 (0811-1083)
Bookmark and Share
 
Correctness Proofs (D.2.4 ... )
 
 
Formal Methods (D.2.4 ... )
 
 
Concurrent Programming (D.1.3 )
 
Would you recommend this review?
yes
no
Other reviews under "Correctness Proofs": Date
Using symbolic execution for verification of Ada tasking programs
Dillon L. (ed) ACM Transactions on Programming Languages and Systems 22(6): 643-669, 2000. Type: Article
Jul 1 1991
Reasoning about programs (videotape)
Dijkstra E. (ed), University Video Communications, Stanford, CA, 1990. Type: Book
Dec 1 1992
Error-free software
Baber R., John Wiley & Sons, Inc., New York, NY, 1991. Type: Book (9780471930167)
May 1 1994
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy