> 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.
> 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
