Title :
Model checking the Java meta-locking algorithm
Author :
Basu, Samik ; Smolka, Scott A. ; Ward, Orson R.
Author_Institution :
Dept. of Comput. Sci., State Univ. of New York, Stony Brook, NY, USA
Abstract :
We apply the XMC model checker to the Java meta-locking 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
Keywords :
Java; formal specification; synchronisation; Java meta-locking algorithm; XMC model checker; abstract specification; highly optimized technique; model checking; mutual exclusion; mutually exclusive access; object monitor queues; Computer science; Electrical capacitance tomography; Internet; Java; Libraries; Monitoring; Production; Reactive power; Virtual machining; Yarn;
Conference_Titel :
Engineering of Computer Based Systems, 2000. (ECBS 2000) Proceedings. Seventh IEEE International Conference and Workshopon the
Conference_Location :
Edinburgh
Print_ISBN :
0-7695-0604-6
DOI :
10.1109/ECBS.2000.839894
