Verification for Java’s reentrant multithreading concept

Abstract

Besides the features of a class-based object-oriented language, Java integrates concurrency via its thread-classes, allowing for a multithreaded flow of control. The concurrency model offers coordination via lock-synchronization, and communication by synchronous message passing, including re-entrant method calls, and by instance variables shared amongthreads. To reason about multithreaded programs, we introduce in this paper an assertional proof method for JavaMT (“Multi-Threaded Java”), a small concurrent sublanguage of Java, coveringthe mentioned concurrency issues as well as the object-based core of Java, i.e., object creation, side effects, and aliasing, but leaving aside inheritance and subtyping.