Basu and Smolka present a case study of modeling and verifying the Java metalocking algorithm using the XMC model checker. They verify the correctness of the metalocking algorithm by manually constructing a model of the algorithm, and then performing model checking on the derived model.
The Java Virtual Machine (JVM) is often used for implementing Internet-based applications using extensive synchronization operations. Metalocking is viewed as a two-tier scheme for achieving monitor-style synchronization in objects. For the metalocking algorithm, the upper tier is used as the metalock level, while the lower tier is used as the monitor-lock level. XMC, on the other hand, is a model checker for value-passing languages such as Java. The metalock level is used to access the object’s synchronization data, and the monitor-lock level is used to access the object data. In the metalocking algorithm, threads observe a certain protocol when manipulating an object’s synchronization data.
This paper is recommended for readers interested in theorem proving using the XMC model checker.