Model Checking the Java Meta-Locking Algorithm

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

• Type: Conference
• Year: 2000
• Where: ECBS
• Authors: Samik Basu, Scott A. Smolka, Orson R. Ward
• Keywords: ECBS 2000, Hardware, Meta-locking Algorithm, Mutually Exclusive, XMC Model Checker