{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:38:30Z","timestamp":1750307910249,"version":"3.41.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2007,7,1]],"date-time":"2007-07-01T00:00:00Z","timestamp":1183248000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2007,7]]},"abstract":"<jats:p>\n            We report on our efforts to use the XMC model checker to model and verify the Java metalocking algorithm. XMC [Ramakrishna et al. 1997] is a versatile and efficient model checker for systems specified in XL, a highly expressive value-passing language. Metalocking [Agesen et al. 1999] 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. Metalocking can be viewed as a two-tiered scheme. At the upper level, the\n            <jats:italic>metalock<\/jats:italic>\n            level, a thread waits until it can enqueue itself on an object's monitor queue in a mutually exclusive manner. At the lower level, the\n            <jats:italic>monitor-lock<\/jats:italic>\n            level, enqueued threads race to obtain exclusive access to the object. Our abstract XL specification of the metalocking algorithm is fully parameterized, both on the number of threads\n            <jats:italic>M<\/jats:italic>\n            , and the number of objects\n            <jats:italic>N<\/jats:italic>\n            . It also captures a sophisticated optimization of the basic metalocking algorithm known as\n            <jats:italic>extra-fast<\/jats:italic>\n            locking and unlocking of uncontended objects. Using XMC, we show that for a variety of values of\n            <jats:italic>M<\/jats:italic>\n            and\n            <jats:italic>N<\/jats:italic>\n            , the algorithm indeed provides mutual exclusion and freedom from deadlock and lockout at the metalock level. We also show that, while the monitor-lock level of the protocol preserves mutual exclusion and deadlock-freedom, it is not lockout-free because the protocol's designers chose to give equal preference to awaiting threads and newly arrived threads.\n          <\/jats:p>","DOI":"10.1145\/1243987.1243990","type":"journal-article","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T13:44:55Z","timestamp":1189777495000},"page":"12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Model checking the Java metalocking algorithm"],"prefix":"10.1145","volume":"16","author":[{"given":"Samik","family":"Basu","sequence":"first","affiliation":[{"name":"Iowa State University, Ames, IA"}]},{"given":"Scott A.","family":"Smolka","sequence":"additional","affiliation":[{"name":"State University of New York at Stony Brook, Stony Brook, NY"}]}],"member":"320","published-online":{"date-parts":[[2007,7]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"ACL2. 2002. Applicative Common Lisp ACL2 v2.7. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/.  ACL2. 2002. Applicative Common Lisp ACL2 v2.7. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/320384.320402"},{"volume-title":"TAME: A PVS interface to simplify proofs for automata models. User Interfaces for Theorem Provers.","year":"1998","author":"Archer M.","key":"e_1_2_1_3_1"},{"volume":"2318","volume-title":"9th International SPIN Workshop on Model Checking of Software","author":"Basin D.","key":"e_1_2_1_4_1"},{"volume-title":"Proceedings of 7th IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS'00)","author":"Basu S.","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. 1999. Model Checking. MIT Press Cambridge MA.   Clarke E. M. Grumberg O. and Peled D. 1999. Model Checking. MIT Press Cambridge MA."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/645880.672076"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0092-3"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Dong Y. Ramakrishnan C. R. and Smolka S. A. 2003. Evidence explorer: A tool for exploring model-checking proofs. In Computer-Aided Verification (CAV'03).  Dong Y. Ramakrishnan C. R. and Smolka S. A. 2003. Evidence explorer: A tool for exploring model-checking proofs. In Computer-Aided Verification (CAV'03).","DOI":"10.1007\/978-3-540-45069-6_22"},{"volume-title":"Handbook of Theoretical Computer Science","author":"Emerson E.","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Groote J. F. and Rem M. Eds. 1997. Science of Computer Programming Special Issue on Verification and Validation Methods for Formal Descriptions. Vol. 29(1-2).  Groote J. F. and Rem M. Eds. 1997. Science of Computer Programming Special Issue on Verification and Validation Methods for Formal Descriptions. Vol. 29(1-2).","DOI":"10.1016\/S0167-6423(96)00026-3"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Havelund K. and Shankar N. 1996. Experiments in theorem proving and model checking for protocol verification. In Industrial Benefit and Advances in Formal Methods (FME'96). Springer-Verlag 662--681.   Havelund K. and Shankar N. 1996. Experiments in theorem proving and model checking for protocol verification. In Industrial Benefit and Advances in Formal Methods (FME'96). Springer-Verlag 662--681.","DOI":"10.1007\/3-540-60973-3_113"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"e_1_2_1_14_1","unstructured":"Holzmann G. 2004. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley.  Holzmann G. 2004. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_2_1_16_1","unstructured":"Milner R.\n     1989.\n      \n  \n   \n  Communication and Concurrency\n  . \n  International Series in Computer Science\n  . \n  Prentice Hall\n  .   Milner R. 1989. Communication and Concurrency. International Series in Computer Science. Prentice Hall."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514189"},{"key":"e_1_2_1_18_1","unstructured":"Murphi. 2006. Murphi description language and verifier. http:\/\/verify.stanford.edu\/dill\/murphi.html.  Murphi. 2006. Murphi description language and verifier. http:\/\/verify.stanford.edu\/dill\/murphi.html."},{"key":"e_1_2_1_19_1","series-title":"Lecture Notes in Computer Science","volume-title":"PVS: Combining specification, proof checking, and model checking. In Proceedings of 8th International Conference on Computer Aided Verification (CAV'96)","author":"Owre S.","year":"1996"},{"volume-title":"Proceedings of the Spring EurOpen Conference","author":"Pike R.","key":"e_1_2_1_20_1"},{"key":"e_1_2_1_21_1","unstructured":"PVS. 2003. The PVS specification and verification system v1.3. http:\/\/pvs.csl.sri.com\/.  PVS. 2003. The PVS specification and verification system v1.3. http:\/\/pvs.csl.sri.com\/."},{"volume-title":"Proceedings of the 9th International Conference on Computer-Aided Verification (CAV'97)","author":"Ramakrishna Y. S.","key":"e_1_2_1_22_1"},{"volume":"1785","volume-title":"Eds. Lecture Notes in Computer Science","author":"Roychoudhury A.","key":"e_1_2_1_23_1"},{"volume":"2102","volume-title":"13th International Conference on Computer Aided Verification (CAV'01)","author":"Roychoudhury A.","key":"e_1_2_1_24_1"},{"volume":"1490","volume-title":"Proceedings of PLILP\/ALP'98","author":"Smolka S.","key":"e_1_2_1_25_1"},{"key":"e_1_2_1_26_1","unstructured":"SMV. 2006. Symbolic model verifier 2.5. http:\/\/www.cs.cmu.edu\/~modelcheck\/smv.html.  SMV. 2006. Symbolic model verifier 2.5. http:\/\/www.cs.cmu.edu\/~modelcheck\/smv.html."},{"key":"e_1_2_1_27_1","unstructured":"Tanenbaum A. S. 1996. Computer Networks 3rd ed. Prentice Hall.   Tanenbaum A. S. 1996. Computer Networks 3rd ed. Prentice Hall."},{"volume-title":"International Conference on Automated Software Engineering","author":"Visser W.","key":"e_1_2_1_28_1"},{"key":"e_1_2_1_29_1","unstructured":"XSB. 2001. The XSB logic programming system v2.4. Available by anonymous ftp from ftp.cs.sunysb.edu.  XSB. 2001. The XSB logic programming system v2.4. Available by anonymous ftp from ftp.cs.sunysb.edu."}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1243987.1243990","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1243987.1243990","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:47:49Z","timestamp":1750258069000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1243987.1243990"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,7]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,7]]}},"alternative-id":["10.1145\/1243987.1243990"],"URL":"https:\/\/doi.org\/10.1145\/1243987.1243990","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2007,7]]},"assertion":[{"value":"2007-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}