DocumentCode
1969470
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
fYear
2000
fDate
2000
Firstpage
342
Lastpage
350
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/ECBS.2000.839894
Filename
839894
Link To Document