Thread invariants - JVM

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):

  1. The current thread is a valid thread.
  2. The elements of the domain of exec are threads.
  3. If the execution state of a thread is NotStarted, then the thread is not synchronized on any object and is not in the wait set of any object.
  4. If a thread is synchronized on an object, then the object is a valid reference in the heap.
  5. If the state of a thread is synchronizing, then the thread is not already synchronized on the object it is competing for. It can hold the lock of other objects, and therefore block other threads from execution.
  6. The list of synchronized objects, obtained from the context of a thread, is the same as the sync list of the thread.
  7. If a thread is waiting for an object, then it is synchronized on the object and is in the wait set of the object. By de_nition, it does not hold the lock of the object it is waiting for. However, it can hold the lock of other objects, and therefore block other threads from execution.
  8. A thread cannot be in the wait set of two di_erent objects.
  9. If a thread has been noti_ed on an object, then it is no longer in the wait set of the object. It is still synchronized on the object, but it does not hold the lock of the object. It can hold the lock of other objects, and therefore block other threads from execution.
  10. If a thread has terminated normally or abruptly, then it does not hold the lock of any object.
  11. If a thread holds the lock of an object, then the lock counter of the object is exactly the number of occurrences of the object in the list of synchronized objects of the thread. It follows that, if the lock counter of an object is zero, then no thread holds the lock of the object.
  12. It is not possible that two di_erent threads hold the lock of the same object.
  13. If the lock counter of an object is greater than zero, then there exists a thread which holds the lock of the object.

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.


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

JVM Topics