A type system for jvm threads

Abstract. The current denition of the Java Bytecode Verier, as well as the proposals to formalize it, do not include any check about consis-tency of critical sections (those between 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 dene a se-mantics and a formal verier that enforces basic properties of threads and critical sections. The verier integrates well with previous formal-izations of the Java Bytecode Verier. Our analysis of critical sections reveals the presence of bugs in the current compilers from Sun and IBM.