Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

10

ECBS
2000
IEEE

favoriteEmaildiscussreport

70views Hardware» more ECBS 2000»

Model Checking the Java Meta-Locking Algorithm

13 years 9 months ago

Model Checking the Java Meta-Locking Algorithm

Download www.cs.sunysb.edu

We apply the XMC model checker to the Java metalocking algorithm, a highly optimized technique for ensuring mutually exclusive access by threads to object monitor queues. Our abstract speciﬁcation of the meta-locking algorithm is fully parameterized, both on M, the number of threads, and N, the number of objects. Using XMC, we show that for a variety of values of M and N, the algorithm indeed provides mutual exclusion and freedom from lockout.

Samik Basu, Scott A. Smolka, Orson R. Ward

Real-time Traffic

ECBS 2000 | Hardware | Meta-locking Algorithm | Mutually Exclusive | XMC Model Checker |

claim paper

Related Content

» Model Checking of Concurrent Algorithms From Java to C

» Using Runtime Analysis to Guide Model Checking of Java Programs

» ModelChecking Multithreaded Distributed Java Programs

» Data Flow Analysis for Checking Properties of Concurrent Java Programs

» Efficient Detection of Errors in Java Components Using Random Environment and Restarts

» Checking determinism of XML Schema content models in optimal time

» Model Checking of Linearizability of Concurrent List Implementations

» Test input generation with java PathFinder

» Efficient modular glass box software model checking

Post Info
More Details (n/a)

Added	31 Jul 2010
Updated	31 Jul 2010
Type	Conference
Year	2000
Where	ECBS
Authors	Samik Basu, Scott A. Smolka, Orson R. Ward

Comments (0)