On Tue, Sep 15, 2015 at 6:29 PM, Caldarale, Charles R < chuck.caldar...@unisys.com> wrote:
> > From: Yilong Li [mailto:yilong...@runtimeverification.com] > > Subject: Re: RV-Predict bugs > > > So you are saying that the author of JMM misunderstands his own work? > > No, I'm saying that he's only looking at things from the point of view of > 17.4, and ignoring section 14.2 of the JLS. (BTW, prior to Sun being > acquired by Oracle, I had long discussions with HotSpot designers about the > C++ difference between "const uint64_t* p" and "uint64_t* const p"; they > never did get it. Don't assume anyone - Gosling, JSR authors, or me - is > infallible.) > > > I don't understand why you interpret JMM in a way that excludes > intra-thread semantics. > > I'm not excluding intra-thread semantics; section 17.4 is concerned with > inter-thread semantics while requiring that intra-thread semantics be > honored. > > > How is it possible for JMM to be of any use if it does not take into > account the intra- > > thread semantics? > > Because those are covered in Chapter 14; the concern of 17 is with > inter-thread operations ("This chapter describes the semantics of > multithreaded programs"). Note that there are no single-thread examples in > Chapter 17. > Single-threading is nothing but a degenerate case of multithreading. From what I have seen right now, JMM works equally well for single-thread programs. Yilong > > > OK, let's do the single-thread case: > > if (hashCode == 0) { > > hashCode = 1; > > } > > return hashCode; > > > L0: WRITE 0 (initial value put by JVM) > > L1: READ 0 > > L2: WRITE 1 > > L4: READ 1 > > A poor example on my part. Both the memory model and section 14.2 of the > JLS certainly do prevent the return of a zero value when the write occurs > in a non-concurrent situation. However, even with concurrent execution, > the JVM cannot legally generate the read at L4 prior to that of L1 due to > the aforementioned section 14.2. The memory model does theoretically > permit hardware to move L4 in front of L1 ("The actions of each thread in > isolation must behave as governed by the semantics of that thread, with the > exception that the values seen by each read are determined by the memory > model"), but AFAICT there are no JVM-supported CPUs that actually do that, > nor can I envision any useful hardware design that would. The x86 spec > expressly forbids it, other CPUs merge the reads together, with store > forwarding or check load instructions handling the write the thread may > generate. > > - 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 > >
