Model Checking the Java Meta-Locking Algorithm

Edinburgh, Scotland April 03-April 07

DOI Bookmark:

http://doi.ieeecomputersociety.org/10.1109/ECBS.2000.839894

7th IEEE International Conference and ...

	This Article
	PURCHASE ARTICLE: $19 PDF HTML IEEE Xplore Subscribers
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Samik Basu Articles by Scott A. Smolka Articles by Orson R. Ward

	ASCII Text	x
	Samik Basu, Scott A. Smolka, Orson R. Ward, "Model Checking the Java Meta-Locking Algorithm," Engineering of Computer-Based Systems, IEEE International Conference on the, pp. 342, 7th IEEE International Conference and Workshop on the Engineering of Computer Based Systems, 2000.

	BibTex	x
	@article{ 10.1109/ECBS.2000.839894, author = {Samik Basu and Scott A. Smolka and Orson R. Ward}, title = {Model Checking the Java Meta-Locking Algorithm}, journal ={Engineering of Computer-Based Systems, IEEE International Conference on the}, volume = {0}, year = {2000}, isbn = {0-7695-0604-6}, pages = {342}, doi = {http://doi.ieeecomputersociety.org/10.1109/ECBS.2000.839894}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Engineering of Computer-Based Systems, IEEE International Conference on the TI - Model Checking the Java Meta-Locking Algorithm SN - 0-7695-0604-6 SP EP A1 - Samik Basu, A1 - Scott A. Smolka, A1 - Orson R. Ward, PY - 2000 KW - Java KW - model checking KW - mutual exclusion KW - objects KW - specification and verification KW - threads KW - synchronization VL - 0 JA - Engineering of Computer-Based Systems, IEEE International Conference on the ER -

Samik Basu, State University of New York at Stony Brook

Scott A. Smolka, State University of New York at Stony Brook

Orson R. Ward, State University of New York at Stony Brook

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.

Index Terms:

Java, model checking, mutual exclusion, objects, specification and verification, threads, synchronization

Citation:

Samik Basu, Scott A. Smolka, Orson R. Ward, "Model Checking the Java Meta-Locking Algorithm," ecbs, pp.342, 7th IEEE International Conference and Workshop on the Engineering of Computer Based Systems, 2000

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.