[concurrency-interest] back again to final fields semantics

Valentin Kovalenko valentin.male.kovalenko at gmail.com
Mon May 5 11:51:34 EDT 2014


Consider the following simplest example where final fields semantics works:
class A {
   final int fx;
   A() {fx = 42;} // [w]
}
A a; //shared

//T1:
a = new A();

//T2:
A localA = a; // read a via data race
if(localA != null) {
        print(localA.fx); // [r]
} else {
        print("none");
}

We all know final semantics guarantees that in this example the only
possible outcomes are "42" and "none"; "0" (default value) is forbidden.

"JLS 17.5.1. Semantics of final Fields" introduces a new partial order hb*
(while refers to it as normal hb), which "does not transitively close with
other happens-before orderings" (this means that the introduced hb* is
definitely not the same hb defined in "JLS 17.4.5. Happens-before Order"
because partial order is transitive by definition).

We can formally show that there is a hb*(w, r) in the example above - no
questions here. But what conclusions can we derive from this fact? "JLS
17.5.1" specifies that hb*(w, r) is useful "when determining which values
can be seen by r", and that's all.

Here are the questions:
(Q1) How exactly it's supposed to "determine" values that can be seen by r?
(Q2) How can we formally show that final fields semantics forbids to see
the default value?

Please provide your answers to the questions Q1 and Q2
and/or confirm/refute the vision of the answers:


Let's assume that visibility rules for hb* are the same as for hb (i.e. in
the following statements we can use hb* and hb interchangeably):
- JLS only considers well-formed executions ("JLS 17.4.7. Well-Formed
Executions")
- well-formed execution is happens-before consistent ("JLS 17.4.7.
Well-Formed Executions"), which means that its set of actions is
happens-before consistent ("JLS 17.4.6. Executions")
-(1) in a happens-before consistent set of actions, each read sees a write
that it is allowed to see by the happens-before ordering ("JLS 17.4.5.
Happens-before Order")
- a read r of a variable fx is allowed to observe a write w to fx if, in
the happens-before partial order of the execution trace ("JLS 17.4.5.
Happens-before Order"):
--- r is not ordered before w (i.e., it is not the case that hb(r, w)), and
--- there is no intervening write w' to fx (i.e. no write w' to fx such
that hb(w, w') and hb(w', r))

In our example we have the following orderings:
(a) hb(wDefault, w) // because "the write of the default value (zero,
false, or null) to each variable synchronizes-with the first action in
EVERY thread" ("JLS 17.4.4. Synchronization Order"), so we have
so(wDefault, firstAction_T1), po(firstAction_T1, w) and hence hb(wDefault,
w)
(b) hb*(w, r) //because of final semantics
(c) hb(wDefault, r) // similarly to hb(wDefault, w), because so(wDefault,
firstAction_T2), po(firstAction_T2, r) and hence hb(wDefault, r)

Let's try to answer Q2.
According to the mentioned visibility rules r is not hb-ordered before
wDefault because of (c), but if w is an intervening write to fx then r
isn't allowed to observe wDefault. In order w to be an intervening write we
need hb(wDefault, w) and hb(w, r), but because we have assumed that we can
use hb* and hb interchangeably in visibility rules we should think that
hb(wDefault, w) and hb*(w, r) also means that w is an intervening write and
therefore r isn't allowed to observe wDefault.

Let's try to answer Q1.
According to the mentioned visibility rules r is not hb*-ordered before w
because of (b), and there is no intervening write to fx such that hb(w, w')
and hb(w', r) because the only candidate for such a write is wDefault which
isn't hb(w, wDefault) because of (a). So r is hb-ordered after w (actually
hb*-ordered, but remember the assumption is that we can use hb and hb*
interchangeably in the visibility rules) and there is no intervening write,
therefore r is allowed to see w and hence it sees w because of (1).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs.oswego.edu/pipermail/concurrency-interest/attachments/20140505/d8aea5e2/attachment.html>


More information about the Concurrency-interest mailing list