Static semantics of JavaT - JVM

Vocabulary of JavaT

Threads are concurrent, independent processes, running within a single program. We describe them as elements of a universe Thread, i.e., the domain of objects belonging to the class Thread through which threads are represented and controlled in Java. Since threads are objects, the universe Thread is a subset of Ref . A pointer q is in Thread i_ q 2 dom(heap) and classOf (q) _h Thread. Every thread q executes the machine execJava, but it does it on its own continuation cont(q), consisting of its frame stack frames and its current frame (meth; restbody; pos; locals). The continuation is local to the thread and cannot be accessed by other threads. It is used to restore the values of meth, restbody, pos, locals and frames, when q becomes the current thread.

cont: Thread ! (Frame_; Frame)

Threads exchange information among each other by operating on objects residing in shared main memory, which is modeled by the functions globals and heap.

The extension of the syntax of JavaE in JavaT by synchronization statements is given in Fig. below. The type of the expression Exp in a synchronized statement must be a reference type.

To synchronize threads, Java uses monitors, a mechanism for allowing only one thread at a time to execute a region of code protected by the monitor.

The behavior of monitors is formulated in terms of locks, which are uniquely associated with objects. When a synchronized statement is processed, the executing thread must grab the lock which is associated with the target reference, to become the owner of the lock, before the thread can continue.

Upon completion of the block, the mechanism releases that very same lock.We use a dynamic function sync to keep track of the dynamic nestings of synchronized statements; sync(q) denotes the stack of all references grabbed by thread q. Since a single thread can hold a lock more than once, we have to de_ne also dynamic lock counters.

To assist communication between threads, each object also has an associated wait set of threads, which are waiting for access to this object. Wait sets are used by the wait and notify methods of class Object. The wait method allows a thread to wait for a noti_cation condition. Executing wait adds the current thread to the wait set for this object and releases the lock|which is reacquired, to continue processing, after the thread has been noti_ed by another thread. Wait sets are modeled by a dynamic function

waitSet:Ref ! Powerset(Thread)

Every thread can be in one of _ve execution modes. This is modeled using the following dynamic function:

exec: Thread ! ThreadState

where the universe ThreadState of thread execution modes is de_ned by data ThreadState = NotStarted j Active j Synchronizing j Waiting j Noti_ed j Dead

As will be de_ned below, a thread T is in the state exec(T) = NotStarted, from the moment it is created, until the start method of the Thread object is called, whereby it becomes Active. A thread gets into the Synchronizing state by execution of a synchronization statement on an object of which it does not have a lock. The object it is competing for is stored using the dynamic function syncObj .

syncObj : Thread ! Ref

A thread in the Waiting state cannot be run, because a wait method has been called. The thread is waiting for the noti_cation of an object. The object it is waiting for is given by the dynamic function waitObj .

waitObj : Thread ! Ref

A thread who is waiting for regaining the abandoned locks on an object gets Noti_ed (and thereby leaves its waiting mode and can compete for being selected again for execution) through the action of another thread, who executes the notify method. A thread in the Noti_ed state is re-enabled for thread scheduling. A thread becomes Dead when it has terminated the execution of its code.

The interrupt method is an asynchronous method which may be invoked by one thread to a_ect the execution of another thread. We use a dynamic function to signal if a thread has been interrupted:

interruptedFlag: Thread ! Bool

The Java reference manual leaves the scheduling strategy open. Although the language designers had a pre-emptive priority-based scheduler in mind, they explicitly say that there is no guarantee for threads with highest priority to be always running. Therefore we abstract from priority based scheduling and formalize the scheduling strategy by a not furthermore speci_ed selection function choose", which is used in the machine execJavaThread below. That machine will call the submachine execJava, to be executed by the thread which has been chosen to be the currently running active thread and is kept in the dynamic constant thread. To achieve this goal we de_ne in the next section the submachine execJavaT of execJava, which provides the semantics for the new statement appearing in JavaT .


All rights reserved © 2018 Wisdom IT Services India Pvt. Ltd DMCA.com Protection Status

JVM Topics