A Type System for JVM ThreadsCosimo Laneve
Department of Computer Science
University of Bologna
The current definition of the Java Bytecode Verifier, as well as the proposals to formalize it, do not include any check about consistency of critical sections (those between monitorenter and monitorexit instructions). So code is run, even if the nesting of critical sections is corrupted.
In this talk 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 critical sections. Our verifier integrates well with previous formalizations of the Java Bytecode Verifier.
Authors: Gaetano Bigliardi, Cosimo Laneve