A New Type System for JVM Lock Primitives

13 years 4 months ago
A New Type System for JVM Lock Primitives
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. Keywords Type System, Java Bytecode Verifier, Lock
Futoshi Iwama, Naoki Kobayashi
Added 14 Dec 2010
Updated 14 Dec 2010
Type Journal
Year 2008
Where NGC
Authors Futoshi Iwama, Naoki Kobayashi
Comments (0)