Model checking the Java meta-locking algorithm

Samik Basu; Scott A. Smolka; Orson R. Ward

Model checking the Java meta-locking algorithm

Samik Basu
, Scott A. Smolka
, Orson R. Ward

Computer Science

Stony Brook University

Stony Brook University

Research output: Contribution to conference › Paper › peer-review

16 Scopus citations

Abstract

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.

Original language	English
Pages	342-350
Number of pages	9
State	Published - 2000
Event	7th IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2000) - Edinburgh, UK Duration: Apr 3 2000 → Apr 7 2000

Conference

Conference	7th IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2000)
City	Edinburgh, UK
Period	04/3/00 → 04/7/00

Cite this

@conference{7dd5135ed86943f09da7521163000394,

title = "Model checking the Java meta-locking algorithm",

abstract = "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.",

author = "Samik Basu and Smolka, \{Scott A.\} and Ward, \{Orson R.\}",

year = "2000",

language = "English",

pages = "342--350",

note = "7th IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2000) ; Conference date: 03-04-2000 Through 07-04-2000",

}

TY - CONF

T1 - Model checking the Java meta-locking algorithm

AU - Basu, Samik

AU - Smolka, Scott A.

AU - Ward, Orson R.

PY - 2000

Y1 - 2000

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

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

UR - https://www.scopus.com/pages/publications/0033871814

M3 - Paper

SP - 342

EP - 350

T2 - 7th IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2000)

Y2 - 3 April 2000 through 7 April 2000

ER -

Model checking the Java meta-locking algorithm

Abstract

Conference

Other files and links

Fingerprint

Cite this