Personal tools
You are here: Home Events Abstract Archives 2000 Model checking the Java meta-locking algorithm

Model checking the Java meta-locking algorithm

Samik Basu and Orson Ward SUNY, Stony Brook 4pm Monday 10 April 2000 Room 2511, JCMB, King's Buildings

We apply the XMC tabled-logic-programming-based model checker to the Java meta-locking algorithm. Meta-locking is a highly optimized technique for ensuring mutually exclusive access by threads to object monitor queues, and therefore plays an essential role in allowing Java to offer concurrent access to objects. 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. Collectively, our results provide strong testimony to the correctness of the meta-locking algorithm.

Document Actions