I have been having a hard time believing the reordering claims, but finally I
went to Jeremy’s blog post. To recap, he says
if (hash == 0) {
int h = //compute hash
hash = h;
}
return hash;
can be reordered to
r1 = hash;
if (hash == 0) {
r1 = hash = // calculate hash
}
return r1;
Obviously this last version is susceptible to returning 0.
It looks to me like the 2nd version is not a reordering of the java statements
of the first version. I conclude that you cannot reason about reordering based
on java, you have to look at reordering at the byte code level. I’m not that
familiar with the byte code but can easily believe that byte code for the 2nd
version is a reordering of byte code for the first version.
I’ve gotten pretty good at recognizing double checked locking and checking to
see if the variable is synchronized, but I have some doubts I’ll be able to
recognize patterns like this consistently. I think that the only practical way
to detect these is through analysis tooling, so I’m glad to see it exists.
thanks
david jencks
> On Sep 15, 2015, at 6:33 PM, Yilong Li <yilong...@runtimeverification.com>
> wrote:
>
> On Tue, Sep 15, 2015 at 3:09 PM, Mark Thomas <ma...@apache.org> wrote:
>
>> On 15/09/2015 22:55, Yilong Li wrote:
>>
>>> Fine. Let's do your example:
>>> T2R4 (out of order read returns null)
>>> T1R1 (returns null)
>>> T1W2 (writes non-null value)
>>> T1R4 (reads new non-null value)
>>> T2R1 (reads new non-null value)
>>>
>>> First of all, when reasoning with JMM, you should not move T2R4 to the
>>> front. This is forbidden by the intra-thread semantics so I move it back
>> to
>>> the bottom:
>>> T1R1 (returns null)
>>> T1W2 (writes non-null value)
>>> T1R4 (reads new non-null value)
>>> T2R1 (reads new non-null value)
>>> T2R4 (out of order read returns null)
>>>
>>> Intra-thread semantics ensures the following HB order:
>>> T1R1 < T2W2 < T1R4
>>> T2R1 < T2R4
>>
>> I assume you mean:
>> T1R1 < T*1*W2 < T1R4
>> above
>>
>
> correct
>
>
>>
>>> T2R4 is allowed to read null because 1) T2R4 is not ordered before the
>>> write of null (let's call it INIT) by JVM during object initialization;
>> and
>>> 2) there is no intervening write w' such that INIT < w' < T2R4. You see,
>>> T1W2 is *not* an intervening write because there is no HB order between
>>> T1W2 & T2R4.
>>>
>>> Let me know if it is still not clear enough.
>>
>> Sorry, still not clear enough.
>>
>> I understand that the JMM allows this behaviour. I don't understand how
>> this could happen in a JVM implementation.
>>
>> If T2R1 has read a non-null value how could a T2R4, a read from the same
>> thread that happens at some later point in time, read a previous value
>> for the same field?
>>
>> That would imply that the two reads were implemented differently since
>> they would have to be looking at different memory locations. What is
>> going on here?
>>
>
> Please go back and check the compiler transformation I stole from Jeremy's
> article. That transformation actually introduces a new shared memory
> location (i.e., field r1). How likely is a compiler going to take advantage
> of such transformation? I don't know, probably very unlikely. But let me
> clarify something: I am not trying to prove that this is a very harmful
> data race in order to justify the importance/usefulness of RV-Predict from
> the beginning. It's on the your discretion whether you care more about the
> JLS or the JVM implementation. I am simply trying to explain two things: 1)
> this *is* a bug according to JMM and 2) there is a correct version that is
> at least as efficient as the original (buggy) one.
>
> Yilong
>
>
>>
>> Mark
>>
>> ---------------------------------------------------------------------
>> To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
>> For additional commands, e-mail: dev-h...@tomcat.apache.org
>>
>>
