The list sync(q) of objects the thread q is synchronized on can be reconstructed from the context of q. We start in the bottom frame of the stack of q with an empty list. The bottom frame contains a position _ and a restbody.
Starting at the root position of the restbody we go downwards to _.
Each time we encounter a synchronized (ref ) phrase; where the path to _ leads into phrase, we prepend the object ref to the list.
When we reach the position _, we continue with the second frame, and so on, including the current frame. The list we obtain, on the way up in the frame stack and down in the restbodies, is called syncFromCont(q) and will always be the same as sync(q).
For the formulation of the invariants we use several predicates. The predicate synchronizing(q; ref ) means that thread q is synchronizing on the object ref . Thread q does not yet hold the lock of ref and is competing for it with other threads. The predicate waiting(q; ref ) means that thread q has called the wait method of the object ref and is waiting to be noti_ed. The predicate noti_ed(q; ref ) means that another thread has called the notify method of the object ref and thread q has been chosen to be noti_ed.
What does it mean that a thread holds the lock of an object? If q is synchronized on ref , thenq holds the lock of ref . However, if q is waiting for ref or has been noti_ed by ref , then q temporarily releases the lock of the object ref .
This is expressed by the predicate locked(q; ref ).locked(q;ref )=ref2sync(q)^:waiting(q;ref )^:noti_ed(q;ref)
We say that an object ref is locked, if there exists a thread q holding the lock of ref .locked(ref)= 9q 2 dom(exec)(locked(q;ref ))
In JavaT , the following invariants are satis_ed (they are formalized in the theorem below):
Theorem (Synchronization). The following invariants are satis_ed for each thread q:
Proof. By induction on the number of steps in the run of the ASM. The predicates synchronizing, waiting, noti_ed, and locked depend on the dynamic functions sync, exec, syncObj , and waitObj only. These functions as well as the dynamic functions cont, thread, locks and waitSet are not updated in execJava, except in execJavaT or when new instances of objects are created. Hence the critical cases are in execJavaThread and execJavaT.
JVM Related Interview Questions
|Java Script Interview Questions||Adv Java Interview Questions|
|Core Java Interview Questions||AJAX Interview Questions|
|Android Interview Questions||Java applet Interview Questions|
|Java 8 Interview Questions||JBOSS Interview Questions|
|Advanced jQuery Interview Questions||Apache Tomcat Interview Questions|
|Application Virtualization Interview Questions||Java 9 Interview Questions|
The Imperative Core Javai Of Java
The Procedural Extension Javac Of Javai
The Object-oriented Extension Javao Of Javac
The Exception-handling Extension Javae Of Javao
The Concurrent Extension Javat Of Javae
Java Is Type Safe
The Jvmi Submachine
The Procedural Extension Jvmc Of Jvmi
The Object-oriented Extension Jvmo Of Jvmc
The Exception-handling Extension Jvme Of Jvmo
Correctness Of The Compiler
The Defensive Virtual Machine
Bytecode Type Assignments
The Diligent Virtual Machine
The Dynamic Virtual Machine
All rights reserved © 2018 Wisdom IT Services India Pvt. Ltd
Wisdomjobs.com is one of the best job search sites in India.