A new type system for JVM lock primitives

摘要

A bytecode verifier for the Java virtual machine language (JVML) checks that bytecode does not cause any fatal error before the code is executed. However, the present verifier does not check correctness of the usage of lock primitives. To solve this problem, we extend Stata and Abadi's type system for JVML by augmenting types with information about how each object is locked and unlocked. The resulting type system can guarantee that when a thread terminates it has released all the locks it has acquired and that a thread releases a lock only if it has acquired the lock previously.