Verification for Java's Reentrant Multithreading Concept

Erika Ábrahám-Mumm Frank S. de Boer Willem-Paul de Roever Martin Steffen

To appear at Foundations of Software Science and Computation Structures (FOSSACS02), Grenoble, France, 6-14 April, 2002


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 among threads. 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, covering the 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.

Server START Conference Manager
Update Time 14 Dec 2001 at 14:02:38
Start Conference Manager
Conference Systems