RV-Predict bugs

Please do not add any more RV-Predict bug reports to Bugzilla until the current set have been evaluated. To be honest it would have been better if you had paused after adding 58367-58379. There are two primary issues with automated tools. 1. They can report false positives. Each report needs to b

Re: RV-Predict bugs

Am 13.09.2015 um 13:08 schrieb Mark Thomas: Please do not add any more RV-Predict bug reports to Bugzilla until the current set have been evaluated. To be honest it would have been better if you had paused after adding 58367-58379. There are two primary issues with automated tools. 1. They can

Re: RV-Predict bugs

Yilong, You need to be subscribed to the dev list in order to post to it. On 13/09/2015 14:08, Yilong Li wrote: > Hi Mark, > > On Sun, Sep 13, 2015 at 4:08 AM, Mark Thomas > wrote: > > Please do not add any more RV-Predict bug reports to Bugzilla until the > cu

Re: RV-Predict bugs

2015-09-13 18:45 GMT+02:00 Mark Thomas : > Yilong, > > You need to be subscribed to the dev list in order to post to it. > > On 13/09/2015 14:08, Yilong Li wrote: > > Hi Mark, > > > > On Sun, Sep 13, 2015 at 4:08 AM, Mark Thomas > > wrote: > > > > Please do not add an

Re: RV-Predict bugs

On 13/09/2015 18:02, Yilong Li wrote: > Hi Mark, > > Atomicity is just one aspect of concurrency. You have to take visibility > (i.e., when the effects of one thread can be seen by another) and > ordering (i.e., when actions in one thread can be seen to occur out of > order with respect to another

Re: RV-Predict bugs

On 13/09/2015 19:02, Rémy Maucherat wrote: > 2015-09-13 18:45 GMT+02:00 Mark Thomas : > >> Yilong, >> >> You need to be subscribed to the dev list in order to post to it. >> >> On 13/09/2015 14:08, Yilong Li wrote: >>> Hi Mark, >>> >>> On Sun, Sep 13, 2015 at 4:08 AM, Mark Thomas >>

Re: RV-Predict bugs

Sorry about the vague explanation. But the actual reasons are not the point here. The only thing matters is the Java memory model. And the article I refer to explain exactly why and how this can happen. I agree that such non-thread-safe lazy initialization rarely causes problem. But, guys, please

Re: RV-Predict bugs

On 13/09/2015 21:59, Yilong Li wrote: > Sorry about the vague explanation. But the actual reasons are not the point > here. No, that is exactly the point. When you claim that something that appears to be working without issue for many, many users then you need to provide a justification for why th

Re: RV-Predict bugs

On Tue, Sep 15, 2015 at 7:19 AM, Mark Thomas wrote: > On 13/09/2015 21:59, Yilong Li wrote: > > Sorry about the vague explanation. But the actual reasons are not the > point > > here. > > No, that is exactly the point. When you claim that something that > appears to be working without issue for m

RE: RV-Predict bugs

> From: Yilong Li [mailto:yilong...@runtimeverification.com] > Subject: Re: RV-Predict bugs > The following is a valid execution trace consists of 5 events: > T1 T2 > 1 READ null > 2 WRITE s > 3

Re: RV-Predict bugs

On Tue, Sep 15, 2015 at 10:58 AM, Caldarale, Charles R < chuck.caldar...@unisys.com> wrote: > > From: Yilong Li [mailto:yilong...@runtimeverification.com] > > Subject: Re: RV-Predict bugs > > > The following is a valid execution trace consists of 5

RE: RV-Predict bugs

> From: Yilong Li [mailto:yilong...@runtimeverification.com] > Subject: Re: RV-Predict bugs > Well, it is the problem (at least part of it) because JLS says "Informally, > a read *r* is allowed to see the result of a write *w* if there is no > *happens-before* ordering to pr

Re: RV-Predict bugs

On Tue, Sep 15, 2015 at 11:32 AM, Caldarale, Charles R < chuck.caldar...@unisys.com> wrote: > > From: Yilong Li [mailto:yilong...@runtimeverification.com] > > Subject: Re: RV-Predict bugs > > > Well, it is the problem (at least part of it) because JLS says > "In

RE: RV-Predict bugs

> From: Yilong Li [mailto:yilong...@runtimeverification.com] > Subject: Re: RV-Predict bugs > > True, but as Mark previously pointed out, no one cares. All that happens > > in that case is the object is redundantly created and then garbage > > collected later; no damag

Re: RV-Predict bugs

Yilong, On 9/15/15 12:59 PM, Yilong Li wrote: > On Tue, Sep 15, 2015 at 7:19 AM, Mark Thomas wrote: > >> On 13/09/2015 21:59, Yilong Li wrote: >>> Sorry about the vague explanation. But the actual reasons are not the >> point >>> here. >> >> No, that is exactly the point. When you claim that som

Re: RV-Predict bugs

Chuck, On 9/15/15 3:06 PM, Caldarale, Charles R wrote: >> From: Yilong Li [mailto:yilong...@runtimeverification.com] >> Subject: Re: RV-Predict bugs > >>> True, but as Mark previously pointed out, no one cares. All that happens >>> in that case is the objec

Re: RV-Predict bugs

All, On 9/15/15 3:07 PM, Christopher Schultz wrote: > In the above case, the reference "s" may for a short time be a reference > to an uninitialized object of type String. This can be problematic. > Imagine the psusdo-bytecode below generated by the compiler: > > 1: push s > 3: ifnull goto 8

Re: RV-Predict bugs

On 15/09/2015 17:59, Yilong Li wrote: > On Tue, Sep 15, 2015 at 7:19 AM, Mark Thomas wrote: >> Long experience has lead us to be sceptical of bugs reported by >> automated tools. When looking at such bugs and we can't see what the >> problem is and the person raising the bug can't provide a clear

RE: RV-Predict bugs

> From: Mark Thomas [mailto:ma...@apache.org] > Subject: Re: RV-Predict bugs > Putting it into my own words to check my understanding: > - The two reads in T2 may be re-ordered because, in T2, there is nothing > that requires a happens-before relationship between the two re

Re: RV-Predict bugs

Mark, On 9/15/15 3:29 PM, Mark Thomas wrote: > On 15/09/2015 17:59, Yilong Li wrote: >> On Tue, Sep 15, 2015 at 7:19 AM, Mark Thomas wrote: > >>> Long experience has lead us to be sceptical of bugs reported by >>> automated tools. When looking at such bugs and we can't see what the >>> problem i

RE: RV-Predict bugs

> From: Christopher Schultz [mailto:ch...@christopherschultz.net] > Subject: Re: RV-Predict bugs > I don't see why a thread would read one value from memory and then have > that value change locally without going back to main memory. The point that was trying to be made was

RE: RV-Predict bugs

> From: Christopher Schultz [mailto:ch...@christopherschultz.net] > Subject: Re: RV-Predict bugs > I discovered that within a synchronized block, the JIT is allowed to re-order > statements if it determines it is safe to do so -- and that statements that > occur before the memo

Re: RV-Predict bugs

On Tue, Sep 15, 2015 at 12:06 PM, Caldarale, Charles R < chuck.caldar...@unisys.com> wrote: > > From: Yilong Li [mailto:yilong...@runtimeverification.com] > > Subject: Re: RV-Predict bugs > > > > True, but as Mark previously pointed out, no one cares. All that >

Re: RV-Predict bugs

On 15/09/2015 20:42, Caldarale, Charles R wrote: >> From: Mark Thomas [mailto:ma...@apache.org] >> Subject: Re: RV-Predict bugs > >> Putting it into my own words to check my understanding: > >> - The two reads in T2 may be re-ordered because, in T2, there is nothin

Re: RV-Predict bugs

On Tue, Sep 15, 2015 at 12:29 PM, Mark Thomas wrote: > On 15/09/2015 17:59, Yilong Li wrote: > > On Tue, Sep 15, 2015 at 7:19 AM, Mark Thomas wrote: > > >> Long experience has lead us to be sceptical of bugs reported by > >> automated tools. When looking at such bugs and we can't see what the >

Re: RV-Predict bugs

On Tue, Sep 15, 2015 at 1:09 PM, Mark Thomas wrote: > On 15/09/2015 20:42, Caldarale, Charles R wrote: > >> From: Mark Thomas [mailto:ma...@apache.org] > >> Subject: Re: RV-Predict bugs > > > >> Putting it into my own words to check my understanding: >

RE: RV-Predict bugs

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

Re: RV-Predict bugs

On 15/09/2015 21:51, Yilong Li wrote: > On Tue, Sep 15, 2015 at 1:09 PM, Mark Thomas wrote: > >> On 15/09/2015 20:42, Caldarale, Charles R wrote: >>>> From: Mark Thomas [mailto:ma...@apache.org] >>>> Subject: Re: RV-Predict bugs >>> >>>&g

Re: RV-Predict bugs

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 th

RE: RV-Predict bugs

> From: Mark Thomas [mailto:ma...@apache.org] > Subject: Re: RV-Predict bugs > st_200 is non-volatile > L1 if (st_200 == null ) { > L2st_200 = sm.getString("sc.200"); > L3 } > L4 return st_200; > Ln=Line n > Tx=Thread x > Rn=Read at line n > Wn=W

Re: RV-Predict bugs

On Tue, Sep 15, 2015 at 2:33 PM, Mark Thomas wrote: > On 15/09/2015 21:51, Yilong Li wrote: > > On Tue, Sep 15, 2015 at 1:09 PM, Mark Thomas wrote: > > > >> On 15/09/2015 20:42, Caldarale, Charles R wrote: > >>>> From: Mark Thomas [mailto:ma...@apache.o

Re: RV-Predict bugs

On 15/09/2015 22:34, Caldarale, Charles R wrote: >> From: Mark Thomas [mailto:ma...@apache.org] >> Subject: Re: RV-Predict bugs > >> st_200 is non-volatile > >> L1 if (st_200 == null ) { >> L2st_200 = sm.getString("sc.200"); >> L3 } >&

Re: RV-Predict bugs

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

RE: RV-Predict bugs

> From: Mark Thomas [mailto:ma...@apache.org] > Subject: Re: RV-Predict bugs > To make sure I understand this it is the possibility of the write T2W2 > that is sufficient to ensure T2R1 and T2R4 are not re-ordered not the > possibility of a write in some other thread? Section 14.

Re: RV-Predict bugs

On 15/09/2015 23:09, Caldarale, Charles R wrote: >> From: Mark Thomas [mailto:ma...@apache.org] >> Subject: Re: RV-Predict bugs > >> To make sure I understand this it is the possibility of the write T2W2 >> that is sufficient to ensure T2R1 and T2R4 are not re-ordered

Re: RV-Predict bugs

On Tue, Sep 15, 2015 at 3:09 PM, Mark Thomas 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)

Re: RV-Predict bugs

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; Obviou

RE: RV-Predict bugs

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

RE: RV-Predict bugs

> From: David Jencks [mailto:david_jen...@yahoo.com.INVALID] > Subject: Re: RV-Predict bugs > 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 = /

RE: RV-Predict bugs

> From: Mark Thomas [mailto:ma...@apache.org] > Subject: Re: RV-Predict bugs > I understand that the JMM allows this behaviour. I don't understand how > this could happen in a JVM implementation. I don't believe it can, on any supported hardware. > If T2R1 has read a n

RE: RV-Predict bugs

> From: Mark Thomas [mailto:ma...@apache.org] > Subject: Re: RV-Predict bugs > My expectation is that once T2 has seen the updated value (originated > from another thread) all subsequent reads in T2 of the same field are > going to see the same value rather than some of those

Re: RV-Predict bugs

ned in JLS Chaptor 14? No. Is it possible for the transformed method to return 0? Yes. Yilong On Tue, Sep 15, 2015 at 6:39 PM, Caldarale, Charles R < chuck.caldar...@unisys.com> wrote: > > From: David Jencks [mailto:david_jen...@yahoo.com.INVALID] > > Subject: Re: RV-Predict bug

Re: RV-Predict bugs

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? > &

Re: RV-Predict bugs

ossible for the transformed method > to return 0? Yes. > > Yilong > > On Tue, Sep 15, 2015 at 6:39 PM, Caldarale, Charles R < > chuck.caldar...@unisys.com> wrote: > >>> From: David Jencks [mailto:david_jen...@yahoo.com.INVALID] >>> Subject: Re: RV-Pred

Re: RV-Predict bugs

On 16/09/2015 02:49, Caldarale, Charles R wrote: >> From: Mark Thomas [mailto:ma...@apache.org] >> Subject: Re: RV-Predict bugs > >> My expectation is that once T2 has seen the updated value (originated >> from another thread) all subsequent reads in T2 of the same fi

Re: RV-Predict bugs

On 16/09/2015 06:38, David Jencks wrote: > At this point I tend to agree with Ylong and Jeremy. I’m very far > from being an expert but I thought 14.2 meant that the result of > execution of a single thread had to be the same as if it executed the > given instructions in the order supplied. I did

RE: RV-Predict bugs

> From: Mark Thomas [mailto:ma...@apache.org] > Subject: Re: RV-Predict bugs > To re-cap. The assertion is that > === > String foo; > doSomething() { > if (foo == null) { > foo = calculateNewValue(); > } > return foo; > } > === > can be transform

Re: RV-Predict bugs

On 16/09/2015 14:01, Caldarale, Charles R wrote: >> From: Mark Thomas [mailto:ma...@apache.org] >> Subject: Re: RV-Predict bugs > >> To re-cap. The assertion is that >> === >> String foo; >> doSomething() { >> if (foo == null) { >>

Re: RV-Predict bugs

I don’t understand your transformation. foo is certainly a class member. I thought bar was a local variable, thus inaccessible to anything outside the method and thread being executed. Your transformation makes them look like they are the same kind of thing? I’m also not quite sure where the