Abstract
A bytecode verifier for the Java virtual machine language (JVML)
statically checks that bytecode does not cause any fatal error.
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 guarantees 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.
We have implemented a prototype
Java bytecode verifier based on the type system.
We have tested the verifier for several classes in the Java run time library
and confirmed that the verifier runs efficiently and gives correct answers.