Sorry, I am confused. So you are saying that the author of JMM misunderstands his own work? Well, I highly doubt that. I don't understand why you interpret JMM in a way that excludes intra-thread semantics. How is it possible for JMM to be of any use if it does not take into account the intra-thread semantics?
On Tue, Sep 15, 2015 at 2:01 PM, Caldarale, Charles R < chuck.caldar...@unisys.com> wrote: > > From: Yilong Li [mailto:yilong...@runtimeverification.com] > > Subject: Re: RV-Predict bugs > > > Nope, I know what I am doing. Let's first see what the expert says. > Please > > check out the last section in this article ( > > http://jeremymanson.blogspot.com/2008/12/benign-data-races-in-java.html) > > which starts with "let's break the code". Here, we are talking about T2 > in > > the above example. The second read of the field hashCode is not > > control-flow-dependent on the first read (the zero-check). Again, > > intra-thread semantics introduces HB order between the event 3 and event > 4. > > But it doesn't ensure that event 4 must see the same value as event 3. > > The above article is limited specifically to the memory model and > inter-thread semantics. While it's true that the memory model does not > preclude reordering of the reads, the HB of intra-thread semantics does > (Chapter 14 of the JLS): > > "A block is executed by executing each of the local variable declaration > statements and other statements in order from first to last (left to > right)." > > Otherwise, a single-thread program using the hashCode() example could > return zero, and that clearly does not happen. > OK, let's do the single-thread case: if (hashCode == 0) { hashCode = 1; } return hashCode; T1 L0: WRITE 0 (initial value put by JVM) L1: READ 0 L2: WRITE 1 L4: READ 1 Let me demonstrate why the last read cannot return 0 according to JMM. First of all, L0 <hb L1 <hb L2 <hb L4 (<hb means happens-before) due to intra-thread semantics. Second, list all the values L4 might see. There are two possibilities in this case: 0 (the initial value put by JVM) and 1 (the value written by L2). Third, check if value L4 is allowed to see 0 based on the following two rules (quoted from JLS$17.4.5 again): We say that a read *r* of a variable *v* is allowed to observe a write *w* to *v* if, in the *happens-before* partial order of the execution trace: - *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 *v* (i.e. no write *w*' to *v* such that *hb(w, w')* and *hb(w', r)*). The first condition is trivially satisfied because L0 <hb L4. However, the second condition fails because there is L2 (w' in the second rule) which satisfies L0 <hb L2 <hb L4. So L4 can only see the value written by L2, which is 1. Yilong > - Chuck > > > THIS COMMUNICATION MAY CONTAIN CONFIDENTIAL AND/OR OTHERWISE PROPRIETARY > MATERIAL and is thus for use only by the intended recipient. If you > received this in error, please contact the sender and delete the e-mail and > its attachments from all computers. > > > --------------------------------------------------------------------- > To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org > For additional commands, e-mail: dev-h...@tomcat.apache.org > >
