A Type System for JVM Threads

Gaetano Bigliardi, Cosimo Laneve

To appear at ACM SIGPLAN Workshop on Types in Compilation (TIC00), Montreal, Canada, 21 September 2000


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 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 critical sections. Our verifier integrates well with previous formalizations of the Java Bytecode Verifier.

Server START Conference Manager
Update Time 27 Jul 2000 at 15:10:31
Maintainer rwh+tic@cs.cmu.edu.
Start Conference Manager
Conference Systems