Model checking the Java metalocking algorithm

ABSTRACT

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 metalock 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 monitor-lock 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 M, and the number of objects N. It also captures a sophisticated optimization of the basic metalocking algorithm known as extra-fast locking and unlocking of uncontended objects. Using XMC, we show that for a variety of values of M and 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.

REFERENCES

• 1: ACL2. 2002. Applicative Common Lisp ACL2 v2.7. http://www.cs.utexas.edu/users/moore/acl2/.
• 2: Ole Agesen , David Detlefs , Alex Garthwaite , Ross Knippel , Y. S. Ramakrishna , Derek White, An efficient meta-lock for implementing ubiquitous synchronization, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.207-222, November 01-05, 1999, Denver, Colorado, United States
• 3: Archer, M., Heitmeyer, C., and Sims, S. 1998. TAME: A PVS interface to simplify proofs for automata models. User Interfaces for Theorem Provers. Eindhoven, The Netherlands.
• 4: David A. Basin , Stefan Friedrich , Marek Gawkowski , Joachim Posegga, Bytecode Model Checking: An Experimental Analysis, Proceedings of the 9th International SPIN Workshop on Model Checking of Software, p.42-59, April 11-13, 2002
• 5: Basu, S., Smolka, S. A., and Ward, O. R. 2000. Model checking the Java Metalocking algorithm. In Proceedings of 7th IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS'00). Edinburgh, Scotland.
• 6: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 7: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Robby, A Language Framework for Expressing Checkable Properties of Dynamic Software, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.205-223, August 30-September 01, 2000
• 8: Dong, Y., Du, X., Holzmann, G., and Smolka, S. A. 2003. Fighting livelock in the i-Protocol: A case study in explicit-state model checking. Softw. Tools Techn. Transfer 4, 4, 505--528.
• 9: 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).
• 10: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 11: 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).
• 12: Klaus Havelund , Natarajan Shankar, Experiments in Theorem Proving and Model Checking for Protocol Verification, Proceedings of the Third International Symposium of Formal Methods Europe on Industrial Benefit and Advances in Formal Methods, p.662-681, March 18-22, 1996
• 13: Matthew Hennessy , Robin Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM (JACM), v.32 n.1, p.137-161, Jan. 1985 [doi>10.1145/2455.2460]
• 14: Holzmann, G. 2004. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley.
• 15: Kozen, D. 1983. Results on the propositional μ-calculus. Theoret. Comput. Sci. 27, 333--354.
• 16: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 17: J. Strother Moore , George Porter, The apprentice challenge, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.3, p.193-216, May 2002 [doi>10.1145/514188.514189]
• 18: Murphi. 2006. Murphi description language and verifier. http://verify.stanford.edu/dill/murphi.html.
• 19: Sam Owre , S. Rajan , John M. Rushby , Natarajan Shankar , Mandayam K. Srivas, PVS: Combining Specification, Proof Checking, and Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.411-414, August 03, 1996
• 20: Pike, R., Presotto, D., Thompson, K., and Holzmann, G. 1991. Process sleep and wake-up on a shared-memory multiprocessor. In Proceedings of the Spring EurOpen Conference. Tromso, Norway, 161--166.
• 21: PVS. 2003. The PVS specification and verification system v1.3. http://pvs.csl.sri.com/.
• 22: Y. S. Ramakrishna , C. R. Ramakrishnan , I. V. Ramakrishnan , Scott A. Smolka , Terrance Swift , David Scott Warren, Efficient Model Checking Using Tabled Resolution, Proceedings of the 9th International Conference on Computer Aided Verification, p.143-154, June 22-25, 1997
• 23: Abhik Roychoudhury , K. Narayan Kumar , C. R. Ramakrishnan , I. V. Ramakrishnan , Scott A. Smolka, Verification of Parameterized Systems Using Logic Program Transformations, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.172-187, March 25-April 02, 2000
• 24: Abhik Roychoudhury , I. V. Ramakrishnan, Automated Inductive Verification of Parameterized Protocols, Proceedings of the 13th International Conference on Computer Aided Verification, p.25-37, July 18-22, 2001
• 25: Baoqiu Cui , Yifei Dong , Xiaoqun Du , K. Narayan Kumar , C. R. Ramakrishnan , I. V. Ramakrishnan , Abhik Roychoudhury , Scott A. Smolka , David Scott Warren, Logic Programming and Model Checking, Proceedings of the 10th International Symposium on Principles of Declarative Programming, p.1-20, September 16-18, 1998
• 26: SMV. 2006. Symbolic model verifier 2.5. http://www.cs.cmu.edu/~modelcheck/smv.html.
• 27: Andrew S. Tanenbaum, Computer networks (3rd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1996
• 28: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000
• 29: XSB. 2001. The XSB logic programming system v2.4. Available by anonymous ftp from ftp.cs.sunysb.edu.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods; Model checking

Keywords:
Java, XMC, metalocking, monitor queues, mutual exclusion, synchronized methods