A type system for JVM threads

AbstractThe current definition of the Java bytecode verifier, as well as the proposals to formalize it, does not include any check about the structured use of locks by monitorenter and monitorexit instructions. So code is run, even if critical sections are corrupted. In this paper, we isolate a sublanguage of the Java Virtual Machine with thread creation and mutual exclusion. For this subset, we define a semantics and a formal verifier that enforces basic properties of threads and lock and unlock operations. The verifier integrates well with previous formalizations of the Java bytecode verifier. Our analysis of structured use of locks reveals the presence of bugs in the current compilers from Sun, IBM and Microsoft