Re: RV-Predict bugs

2015-09-16 Thread Mark Thomas
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 didn’t think it meant it
> had to execute those particular instructions, I thought it could pick
> whatever instructions it wanted as long as the result would be the
> same as if the given instructions were executed in the given order.
> If there’s only one thread, Jeremy’s transformed code obviously
> produces the same result as the original.  To me saying it ‘has
> different logic” and “has a timing window” might be true but don’t
> directly mean that if violates the ch. 14 semantics.
> 
> Hoping to learn more….

Same here. I'm finding this discussion extremely useful. I'm not trying
to find reasons to dismiss or minimise the bugs reported by RV-Predict.
You'll notice that, with one exception that I currently believe is a
false positive, that all the bugs have been fixed. And if the basis for
declaring that issue false positive is found to be faulty it will get
fixed too.

I am trying to better understand a) exactly what the issue is and b) how
likely the issue is. That requires an understanding of both the theory
(JLS/JMM) and how the theory is applied in practice to produce a JVM.

To re-cap. The assertion is that

===

String foo;

doSomething() {
  if (foo == null) {
foo = calculateNewValue();
  }
  return foo;
}

===

can be transformed (by the complier?) to

===

String foo;
String bar;

doSomething() {
  bar = foo;
  if (foo == null) {
foo = calculateNewValue();
bar = foo;
  }
  return bar;
}

===

Ignoring re-ordering this transformation creates an obvious concurrency
issue (foo is changed from null to non-null after its value is copied to
bar and before foo is tested for null).

The questions I have are:

1. Is such a transformation legal? I assume the answer is yes but I've
been struggling to find the language in the JLS that permits this. Is it
17.4 "An implementation is free to produce any code it likes, as long as
all resulting executions of a program produce a result that can be
predicted by the memory model."?

2. Why would something make a transformation like this? This brings us
back to the question of theoretical issues vs. practical issues which
helps us judge the severity of any given issue.

Mark

-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org



Re: RV-Predict bugs

2015-09-16 Thread Mark Thomas
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 field are
>> going to see the same value rather than some of those reads seeing an
>> older value (assuming there are no further changes in other threads).
> 
> The memory model does permit out-of-order reads of the same location, but I 
> can't find any CPUs that would do this.  (Out-of-order reads of different 
> locations occur frequently, of course.)

OK. Thanks.

I think that wraps up this part of the discussion for me.

I think we are all agreed that, purely from a re-ordering of reads point
of view (deliberately ignoring transformations), there is a theoretical
issue here based purely on the rules of the JMM but in practise the
issue is never observed because no CPU takes advantage of what the JMM
allows.

Whether or not issues in the category above are worth fixing or not is a
different debate and not one I really want to get into here. I'll just
note that we did fix this bug in Tomcat.

I'll follow up with the questions I have on the transformation aspects
in that part of the thread.

Mark

-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org



Re: RV-Predict bugs

2015-09-16 Thread Mark Thomas
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) {
>> foo = calculateNewValue();
>>   }
>>   return foo;
>> }
>> ===
>> can be transformed (by the complier?) to
>> ===
>> String foo;
>> String bar;
>> doSomething() {
>>   bar = foo;
>>   if (foo == null) {
>> foo = calculateNewValue();
>> bar = foo;
>>   }
>>   return bar;
>> }
>> ===
> 
>> Ignoring re-ordering this transformation creates an obvious concurrency
>> issue (foo is changed from null to non-null after its value is copied to
>> bar and before foo is tested for null).
> 
> Correct.  That changed the original logic of the method, creating a timing 
> window that wasn't there before.  In compiler language (see below), it 
> rematerialized a load for a shared memory location.
> 
>> The questions I have are:
> 
>> 1. Is such a transformation legal? I assume the answer is yes but I've
>> been struggling to find the language in the JLS that permits this. Is it
>> 17.4 "An implementation is free to produce any code it likes, as long as
>> all resulting executions of a program produce a result that can be
>> predicted by the memory model."?
> 
>> 2. Why would something make a transformation like this? This brings us
>> back to the question of theoretical issues vs. practical issues which
>> helps us judge the severity of any given issue.
> 
> 1. No (at least not in the real world).
> 
> 2. Compiler bug.  An analogous example is the one-time gcc error that 
> transformed
> if (a == 0) a = 1;
> into
> temp = a;
> if (temp == 0) temp = 1;
> a = temp;
> This caused immense havoc, besides being a performance killer.
> 
> For reference, read the LLVM spec for concurrency handling:
> http://llvm.org/docs/Atomics.html
> In particular, this section on instruction ordering:
> http://llvm.org/docs/Atomics.html#atomic-orderings
> Note the difference in implementation between handling shared variables in 
> C/C++ (NotAtomic) and shared variables in Java (Unordered).
> 
> (For those not familiar with LLVM, it's the compilation tool chain used for 
> OS X, iOS, Android, PS4, and many other platforms.)
> 
> The key bit of information pertinent to Java is this:
> 
> "In terms of the optimizer, this prohibits any transformation that transforms 
> a single load into multiple loads, transforms a store into multiple stores, 
> narrows a store, or stores a value which would not be stored otherwise. Some 
> examples of unsafe optimizations are narrowing an assignment into a bitfield, 
> *rematerializing a load*, and turning loads and stores into a memcpy call. 
> Reordering unordered operations is safe, though, and optimizers should take 
> advantage of that because unordered operations are common in languages that 
> need them."
> 
> The above may go beyond the theoretical limitations of the memory model, but 
> is representative of what compilers must do in order to generate workable 
> programs in the real world.  This isn't academia, it's business.
> 
> I think I'm done here.

Thanks Chuck. Your input is much appreciated.

Thanks too to everyone else who has contributed to this thread. I know
I've learned a lot from it and I hope others have as well.

I think this puts the transformation issue in the same category as
re-ordering. In theory compilers / hardware can do this and still be
compliant with the JLS/JMM but in practice none do.

Mark


-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org



RE: RV-Predict bugs

2015-09-16 Thread Caldarale, Charles R
> 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 transformed (by the complier?) to
> ===
> String foo;
> String bar;
> doSomething() {
>   bar = foo;
>   if (foo == null) {
> foo = calculateNewValue();
> bar = foo;
>   }
>   return bar;
> }
> ===

> Ignoring re-ordering this transformation creates an obvious concurrency
> issue (foo is changed from null to non-null after its value is copied to
> bar and before foo is tested for null).

Correct.  That changed the original logic of the method, creating a timing 
window that wasn't there before.  In compiler language (see below), it 
rematerialized a load for a shared memory location.

> The questions I have are:

> 1. Is such a transformation legal? I assume the answer is yes but I've
> been struggling to find the language in the JLS that permits this. Is it
> 17.4 "An implementation is free to produce any code it likes, as long as
> all resulting executions of a program produce a result that can be
> predicted by the memory model."?

> 2. Why would something make a transformation like this? This brings us
> back to the question of theoretical issues vs. practical issues which
> helps us judge the severity of any given issue.

1. No (at least not in the real world).

2. Compiler bug.  An analogous example is the one-time gcc error that 
transformed
if (a == 0) a = 1;
into
temp = a;
if (temp == 0) temp = 1;
a = temp;
This caused immense havoc, besides being a performance killer.

For reference, read the LLVM spec for concurrency handling:
http://llvm.org/docs/Atomics.html
In particular, this section on instruction ordering:
http://llvm.org/docs/Atomics.html#atomic-orderings
Note the difference in implementation between handling shared variables in 
C/C++ (NotAtomic) and shared variables in Java (Unordered).

(For those not familiar with LLVM, it's the compilation tool chain used for OS 
X, iOS, Android, PS4, and many other platforms.)

The key bit of information pertinent to Java is this:

"In terms of the optimizer, this prohibits any transformation that transforms a 
single load into multiple loads, transforms a store into multiple stores, 
narrows a store, or stores a value which would not be stored otherwise. Some 
examples of unsafe optimizations are narrowing an assignment into a bitfield, 
*rematerializing a load*, and turning loads and stores into a memcpy call. 
Reordering unordered operations is safe, though, and optimizers should take 
advantage of that because unordered operations are common in languages that 
need them."

The above may go beyond the theoretical limitations of the memory model, but is 
representative of what compilers must do in order to generate workable programs 
in the real world.  This isn't academia, it's business.

I think I'm done here.

 - 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



Re: RV-Predict bugs

2015-09-16 Thread David Jencks
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 “rematerialization” chuck mentions is 
happening, although I don’t know what it is exactly.  I’m also not seeing why 
this transformation couldn’t be done by a JIT compiler rather than the cpu.

My uneducated mental model of the original is 

int foo (memory)

load foo into register r1
if r1 == 0 {
  write 42 into r1
  store r1 to foo
}
load foo into register r2
return r2

so the optimizer thinks, hmm, lets do all the loads at once to increase the 
chances that the cache won’t have to be reloaded…. flip a coin and pick r2 to 
load first….. hmm, we might be changing the value so we’ll update r2 if we do.

int foo (memory)

load foo into register r2
load foo into register r1
if  r1 == 0 {
   write 42 into r1
// better update r2 also
  copy r1 into r2
  store r1 to foo
}
return r2

Is there some reason the JIT compiler  can’t do this transformation? I don’t 
see how in-processor optimizations apply nor do I see how LLVM rules apply.  I 
thought JIT behavior was only controlled by what the JLS said.

Still hoping to learn more…
david jencks

> On Sep 16, 2015, at 4:50 AM, Mark Thomas  wrote:
> 
> 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 didn’t think it meant it
>> had to execute those particular instructions, I thought it could pick
>> whatever instructions it wanted as long as the result would be the
>> same as if the given instructions were executed in the given order.
>> If there’s only one thread, Jeremy’s transformed code obviously
>> produces the same result as the original.  To me saying it ‘has
>> different logic” and “has a timing window” might be true but don’t
>> directly mean that if violates the ch. 14 semantics.
>> 
>> Hoping to learn more….
> 
> Same here. I'm finding this discussion extremely useful. I'm not trying
> to find reasons to dismiss or minimise the bugs reported by RV-Predict.
> You'll notice that, with one exception that I currently believe is a
> false positive, that all the bugs have been fixed. And if the basis for
> declaring that issue false positive is found to be faulty it will get
> fixed too.
> 
> I am trying to better understand a) exactly what the issue is and b) how
> likely the issue is. That requires an understanding of both the theory
> (JLS/JMM) and how the theory is applied in practice to produce a JVM.
> 
> To re-cap. The assertion is that
> 
> ===
> 
> String foo;
> 
> doSomething() {
>  if (foo == null) {
>foo = calculateNewValue();
>  }
>  return foo;
> }
> 
> ===
> 
> can be transformed (by the complier?) to
> 
> ===
> 
> String foo;
> String bar;
> 
> doSomething() {
>  bar = foo;
>  if (foo == null) {
>foo = calculateNewValue();
>bar = foo;
>  }
>  return bar;
> }
> 
> ===
> 
> Ignoring re-ordering this transformation creates an obvious concurrency
> issue (foo is changed from null to non-null after its value is copied to
> bar and before foo is tested for null).
> 
> The questions I have are:
> 
> 1. Is such a transformation legal? I assume the answer is yes but I've
> been struggling to find the language in the JLS that permits this. Is it
> 17.4 "An implementation is free to produce any code it likes, as long as
> all resulting executions of a program produce a result that can be
> predicted by the memory model."?
> 
> 2. Why would something make a transformation like this? This brings us
> back to the question of theoretical issues vs. practical issues which
> helps us judge the severity of any given issue.
> 
> Mark
> 
> -
> To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
> For additional commands, e-mail: dev-h...@tomcat.apache.org
> 


-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org



RE: RV-Predict bugs

2015-09-15 Thread Caldarale, Charles R
> 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 = //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.

Correct; it's different logic, and thus a bit of a red herring.  It introduces 
a timing window not present in the original code; it's not an example of a 
speculative read.

 - 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



Re: RV-Predict bugs

2015-09-15 Thread David Jencks
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 didn’t think it meant it had to execute those particular 
instructions, I thought it could pick whatever instructions it wanted as long 
as the result would be the same as if the given instructions were executed in 
the given order.  If there’s only one thread, Jeremy’s transformed code 
obviously produces the same result as the original.  To me saying it ‘has 
different logic” and “has a timing window” might be true but don’t directly 
mean that if violates the ch. 14 semantics.

Hoping to learn more….

david jencks

> On Sep 15, 2015, at 9:58 PM, Yilong Li <yilong...@runtimeverification.com> 
> wrote:
> 
> Your argument seems to assume that reordering is the only code
> transformation that can be done by compiler or hardware. I don't agree that
> you call this transformation a red herring. It might not be practical but
> it's certainly valid. Does it violate the intra-thread semantics you
> mentioned 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 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;
>> 
>>> 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.
>> 
>> Correct; it's different logic, and thus a bit of a red herring.  It
>> introduces a timing window not present in the original code; it's not an
>> example of a speculative read.
>> 
>> - 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
>> 
>> 


-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org



RE: RV-Predict bugs

2015-09-15 Thread Caldarale, Charles R
> 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 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?

Only if the reads were reordered - not by the JVM, but by the CPU.  But I can't 
find any supported CPUs that do this (Alpha may have).

 - 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



Re: RV-Predict bugs

2015-09-15 Thread Yilong Li
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
>
>


Re: RV-Predict bugs

2015-09-15 Thread Yilong Li
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)
> >
> > 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
>
>


RE: RV-Predict bugs

2015-09-15 Thread Caldarale, Charles R
> 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



RE: RV-Predict bugs

2015-09-15 Thread Caldarale, Charles R
> 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 reads seeing an
> older value (assuming there are no further changes in other threads).

The memory model does permit out-of-order reads of the same location, but I 
can't find any CPUs that would do this.  (Out-of-order reads of different 
locations occur frequently, of course.)

 - 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



Re: RV-Predict bugs

2015-09-15 Thread Mark Thomas
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 not the
>> possibility of a write in some other thread?
> 
> Section 14.2 requires that statements appear to execute in order, so the 
> second read cannot be issued by the JVM until after the write could occur.  
> The Java compilers (javac, C1, and C2) are not aware of whether or not 
> multiple threads are in play unless volatile, synchronized, or atomic 
> operations are explicitly done.  So in this case, the reordering is 
> prohibited by the statement execution order requirement, not the memory model.

OK. I think my understanding is getting there slowly.

I take it that once T2R1 has read the new value that there is no way
that T2R4 is going to read an older value e.g. by reading the value from
a different, older/out-of-date memory location.

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 reads seeing an
older value (assuming there are no further changes in other threads).

Mark

-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org



Re: RV-Predict bugs

2015-09-15 Thread David Jencks
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  
> wrote:
> 
> 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)
>>> 
>>> 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
>> 
>> 



Re: RV-Predict bugs

2015-09-15 Thread Yilong Li
Your argument seems to assume that reordering is the only code
transformation that can be done by compiler or hardware. I don't agree that
you call this transformation a red herring. It might not be practical but
it's certainly valid. Does it violate the intra-thread semantics you
mentioned 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 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;
>
> > 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.
>
> Correct; it's different logic, and thus a bit of a red herring.  It
> introduces a timing window not present in the original code; it's not an
> example of a speculative read.
>
>  - 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
>
>


Re: RV-Predict bugs

2015-09-15 Thread Yilong Li
On Tue, Sep 15, 2015 at 2:33 PM, Mark Thomas <ma...@apache.org> wrote:

> On 15/09/2015 21:51, Yilong Li wrote:
> > On Tue, Sep 15, 2015 at 1:09 PM, Mark Thomas <ma...@apache.org> 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:
> >>>
> >>>> - The two reads in T2 may be re-ordered because, in T2, there is
> nothing
> >>>>   that requires a happens-before relationship between the two reads
> >>>
> >>> Depends on what was really meant by the ??? notation.  If it were
> >> another reference to st_200, then the example ignores the potential
> write
> >> to st_200.
> >>>
> >>>> - If T2 was executing in isolation the order of the reads wouldn't
> >>>>   matter
> >>>
> >>> Correct, assuming there is no write in T2's control flow.
> >>>
> >>>> - However, T1 is writing.
> >>>
> >>>> So if the writes
> >>>
> >>> I'll assume you meant "reads" there.
> >>
> >> I'd did. Thanks.
> >>
> >>>> in T2 are re-ordered and the write from T1 takes place between them
> the
> >> T2
> >>>> read for the line 'st_200 == null' could return a non-null value for
> >> st_200
> >>>> (the value after the write from T1) while the read for the line
> 'return
> >>>> st_200;' could return null (the value from before the write in T1).
> >>>
> >>> No - that would violate program order (intra-thread semantics).  The
> >> compiler cannot legally move the read for "return st_200" to a point
> before
> >> the potential write to st_200.  The CPU can speculatively read for the
> >> return value, but must discard such speculation if a write were to occur
> >> (or use store forwarding to update the read).
> >>
> >> Thanks for sticking with me on this. I'm finding it hugely helpful. I
> >> think I need a few more references to make things clearer so I'm going
> >> to restate the problem.
> >>
> >> 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=Write at line n
> >>
> >> So T2 has two reads, T2R1 and T2R4.
> >> Depending on the value read for T2R1 there may be a write at T2W2.
> >> If there is a write there is a happens before relationship between T2R1
> >> and T2R4.
> >>
> >> Consider the following sequence
> >>
> >> 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)
> >>
> >> Because T2R1 reads a non-null value there is no write in T2.
> >> Therefore there is no happens-before relationship between T2R1 and T2R4
> >> because there is no intervening write in that thread (the write happens
> >> in T1).
> >> Therefore the re-ordering is allowed to happen.
> >> And we get the unexpected result.
> >>
> >> Or
> >>
> >> The write at T1W2 is sufficient to enforce the happens before
> >> relationship between T2R1 and T2R4. In which case what is the point of
> >> volatile? What do I gain by using it?
> >>
> >
> > Again, as I mentioned in my previous message, I am afraid this is not the
> > correct way to use HB relationship. To make things more clear, I steal
> this
> > transformation from Jeremy Manson's article I sent before:
>
> That doesn't help my improve my understanding at all.
>
> What I'm looking for is an explanation - ideally using my example above
> - of exactly how T2R4 can return null while T2R1 reads a non-null value.
> "Because the JMM says it can" is not a sufficient explanation.  I
> believe that the JMM says it can but I don't understand how this can
> actually happen. What I am looking for is the explanation of how. Your
> message at 16.59 (UTC) was heading in the right direction but the
> explanation skipped over the crucial part.
>

Fine. Let's do your example:
T2R4 (out of order read returns null)
T1R1 (returns null)
T1W2 (writes

Re: RV-Predict bugs

2015-09-15 Thread Mark Thomas
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 }
>> L4 return st_200;
> 
>> Ln=Line n
>> Tx=Thread x
>> Rn=Read at line n
>> Wn=Write at line n
> 
>> So T2 has two reads, T2R1 and T2R4.
> 
>> Depending on the value read for T2R1 there may be a write at T2W2.
>> If there is a write there is a happens before relationship between T2R1
>> and T2R4.
> 
> There is also a happens-before relationship between T2R1 and T2R4 due to JLS 
> Section 14.2 (Blocks), not Section 17.4 (Memory Model).  The JMM cannot be 
> considered in a vacuum.
> 
>> Consider the following sequence
>> 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)
> 
> The above is not permitted due to Section 14.2 (although it would be by 
> 17.4).  The compiler must not move T2R4 in front of T2R1 because of the 
> potential of T2W2 occurring.  Correct operation is dependent on the CPU 
> observing the same value for T2R1 and T2R4, which is implemented in all 
> current hardware I'm aware of by not permitting reordering of accesses to the 
> same memory location (e.g., see Chapter 8 of the Intel 64 Architecture SDM, 
> Volume 3 - System Programming Guide).  Such accesses are usually just 
> combined when they occur.
> 
>> Because T2R1 reads a non-null value there is no write in T2.
> 
>> Therefore there is no happens-before relationship between T2R1 and T2R4
>> because there is no intervening write in that thread (the write happens
>> in T1).
>> Therefore the re-ordering is allowed to happen.
>> And we get the unexpected result.
> 
> If the JMM were the only controlling specification, that would be true.  
> Since the JVM must also conform to Section 14, the happens-before order 
> exists, and we don't have a problem.
> 
>> The write at T1W2 is sufficient to enforce the happens before
>> relationship between T2R1 and T2R4.
> 
> Yes, the potential of the write occurring is enough.

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?

Mark


-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org



Re: RV-Predict bugs

2015-09-15 Thread Mark Thomas
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

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

Mark

-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org



RE: RV-Predict bugs

2015-09-15 Thread Caldarale, Charles R
> 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.2 requires that statements appear to execute in order, so the second 
read cannot be issued by the JVM until after the write could occur.  The Java 
compilers (javac, C1, and C2) are not aware of whether or not multiple threads 
are in play unless volatile, synchronized, or atomic operations are explicitly 
done.  So in this case, the reordering is prohibited by the statement execution 
order requirement, not the memory model.

 - 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



Re: RV-Predict bugs

2015-09-15 Thread Yilong Li
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 events:
> > T1   T2
> > 1   READ  null
> > 2   WRITE s
> > 3 READ s
> > 4 READ ???
> > 5   READ  s
>
> > where s is the result of sm.getString("sc.200").
>
> > The question is what value T2 can read and then return in event 4.
>
> It's not clear what the READ ??? is intended to represent.
>

I put ??? there because I am trying to reason about what value this read
can see. Sorry for the confusion.


>
> > The question boils down to: does the write in event 2 prevent event 4
> from
> > reading the initial null value of st_200?
>
> It doesn't, but that's not the real problem.


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 prevent that read." In this case, there is no
HB ordering preventing event 3 to read the initial null value put by JVM.


> Let's expand the example a bit:
>
> T1   T2
> 1   READ  null from st_200
> 2a  allocate obj
> 2b  WRITE obj->field
> 2c  WRITE obj into st_200
> 3 READ obj from st_200
> 4 READ obj->field
>
> Since there is no actual ordering of steps 2b (object initialization) and
> 2c (object publication) in T1, T2 can observe them in the reverse order and
> pick up an unitialized value for field.
>

OK, now I see what you are talking about. But consider the following
hashcode example:
public int hashCode() {
  if (hashCode == 0) {
  hashCode = computeHashCode(); // no object creation involved
  }
  return hashCode;
}

There is no object initialization/publication involved at all but the
problem still exists: this method could return 0 even if the if-statement
sees a non-zero value.

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


RE: RV-Predict bugs

2015-09-15 Thread Caldarale, Charles R
> 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 prevent that read." In this case, there is no
> HB ordering preventing event 3 to read the initial null value put by JVM.

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

> But consider the following hashcode example:
> public int hashCode() {
>   if (hashCode == 0) {
>   hashCode = computeHashCode(); // no object creation involved
>   }
>   return hashCode;
> }

> There is no object initialization/publication involved at all but the
> problem still exists: this method could return 0 even if the if-statement
> sees a non-zero value.

No, it can't (unless computeHashCode() returns a zero, which presumably it 
won't).  This is all action within a single thread, and as such must obey 
intra-thread semantics (i.e., statements are executed in control flow order).
 
 - 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



Re: RV-Predict bugs

2015-09-15 Thread Yilong Li
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
> "Informally,
> > a read *r* is allowed to see the result of a write *w* if there is no
> > *happens-before* ordering to prevent that read." In this case, there is
> no
> > HB ordering preventing event 3 to read the initial null value put by JVM.
>
> 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 damage.
>

No, it's not right. It's possible (although very unlikely) that this method
could return null and results in a null pointer exception later.


>
> > But consider the following hashcode example:
> > public int hashCode() {
> >   if (hashCode == 0) {
> >   hashCode = computeHashCode(); // no object creation involved
> >   }
> >   return hashCode;
> > }
>
> > There is no object initialization/publication involved at all but the
> > problem still exists: this method could return 0 even if the if-statement
> > sees a non-zero value.
>
> No, it can't (unless computeHashCode() returns a zero, which presumably it
> won't).  This is all action within a single thread, and as such must obey
> intra-thread semantics (i.e., statements are executed in control flow
> order).
>

Yes, it can. You probably misunderstand intra-thread semantics.
Intra-thread semantics says that event 3 (the first read of the field
hashCode) happens before event 4 (the second read of field hashCode) but it
has no effect on the value event 4 can see (because event 3 is also a read
rather than a write).

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


RE: RV-Predict bugs

2015-09-15 Thread Caldarale, Charles R
> 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 damage.

> No, it's not right. It's possible (although very unlikely) that this method
> could return null and results in a null pointer exception later.

Again, that cannot happen; see below.

> Intra-thread semantics says that event 3 (the first read of the field
> hashCode) happens before event 4 (the second read of field hashCode) but it
> has no effect on the value event 4 can see (because event 3 is also a read
> rather than a write).

You're mixing up inter- and intra-thread semantics and completely ignoring the 
write to hashCode when the initially observed value is zero.  Intra-thread 
semantics require that operations occur in program order, so the initial zero 
(or null) check results in a non-zero (or non-null) write to the field of 
interest; control flow cannot be ignored here.  If your supposition were 
correct, a compiler (or CPU) would be free to migrate actions dependent on a 
conditional block to a spot prior to that conditional block - clearly that is 
nonsense.

 - 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



Re: RV-Predict bugs

2015-09-15 Thread Christopher Schultz
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 something that
>> appears to be working without issue for many, many users then you need
>> to provide a justification for why there is an issue to back up the
>> claims you are making.
>>
>>> The only thing matters is the Java memory model. And the article I
>>> refer to explain exactly why and how this can happen.
>>
>> No, it didn't. I read that article (and parts of the JMM). While the
>> article did state there was a problem it did not explain why there was a
>> problem.
>>
>> 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
>> explanation - and continues not to provide a clear explanation when
>> asked for one several times - then that is the point where we start to
>> think the problem is with the tool.
>>
> 
> Sorry, I should not assume that the concepts such as happens-before order
> and memory model are well understood. Let's talk about how this is allowed
> to happen under JMM. Consider the this example again:
> 
> if (st_200 == null ) {
> st_200 = sm.getString("sc.200");
> }
> return st_200;
> 
> The following is a valid execution trace consists of 5 events:
> T1   T2
> 1   READ  null
> 2   WRITE s
> 3 READ s
> 4 READ ???
> 5   READ  s
> 
> , where s is the result of sm.getString("sc.200").
> 
> T1 sees null in field st_200, initializes it, and return the initialized
> value, while T2 sees a non-null value in st_200 and skips the
> initialization. The question is what value T2 can read and then return in
> event 4. This is addressed in JLS $17.4.5 Happens-before Order (
> https://docs.oracle.com/javase/specs/jls/se8/html/jls-17.html#jls-17.4.5):

I think you are mistaking the above code with something more like this:

private String s;

public String getString()
{
  if(null == s)
s = new String("foo");

   return s;
}

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
5:   goto X
8:   new java.lang.String
10:  dup
11:  store s
13:  push "foo"
15:  call java.lang.String.

If T1 executes the instruction on line 11 and then T2 sees that
reference before T1 gets a change to call the String constructor, it's a
mess.

But, since the initialization of the String coming from
StringManager.getString is fully-constructed before any assignment can
take place, this is completely safe.

As Mark said, reference assignment is guaranteed to be atomic, so T1
while and T2 can disagree about the value of s, it will never be true
that either thread sees s as non-null but also not yet initialized.

In this particular case, the race condition does in fact exist, but
nobody cares: if s gets initialized more than once (to the same value,
in fact), it's no harm to the running program. Even if the values were
different (e.g. ResourceBundle hands-out String values that aren't
consistent), it wouldn't matter to client code.

I'm having trouble understanding Chuck's parallel response to this. :/

-chris



signature.asc
Description: OpenPGP digital signature


RE: RV-Predict bugs

2015-09-15 Thread Caldarale, Charles R
> 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 READ s
> 4 READ ???
> 5   READ  s

> where s is the result of sm.getString("sc.200").

> The question is what value T2 can read and then return in event 4.

It's not clear what the READ ??? is intended to represent.

> The question boils down to: does the write in event 2 prevent event 4 from
> reading the initial null value of st_200?

It doesn't, but that's not the real problem.  Let's expand the example a bit:

T1   T2
1   READ  null from st_200
2a  allocate obj
2b  WRITE obj->field
2c  WRITE obj into st_200
3 READ obj from st_200
4 READ obj->field

Since there is no actual ordering of steps 2b (object initialization) and 2c 
(object publication) in T1, T2 can observe them in the reverse order and pick 
up an unitialized value for field.

 - 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



Re: RV-Predict bugs

2015-09-15 Thread Christopher Schultz
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 object is redundantly created and then garbage
>>> collected later; no damage.
> 
>> No, it's not right. It's possible (although very unlikely) that this method
>> could return null and results in a null pointer exception later.
> 
> Again, that cannot happen; see below.
> 
>> Intra-thread semantics says that event 3 (the first read of the field
>> hashCode) happens before event 4 (the second read of field hashCode) but it
>> has no effect on the value event 4 can see (because event 3 is also a read
>> rather than a write).
> 
> You're mixing up inter- and intra-thread semantics and completely
> ignoring the write to hashCode when the initially observed value is
> zero.  Intra-thread semantics require that operations occur in
> program order, so the initial zero (or null) check results in a
> non-zero (or non-null) write to the field of interest; control flow
> cannot be ignored here.  If your supposition were correct, a compiler
> (or CPU) would be free to migrate actions dependent on a conditional
> block to a spot prior to that conditional block - clearly that is
> nonsense.

I haven't read much about this in many years, but when I was reading
everything surrounding the whole DCL debacle years ago, 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 memory barrier must not be interleaved with
statements inside the block, and likewise, nothing after the block can
be moved "inside" that block.

I'm not sure what that means these days (years later, with changes to
the JMM (which are presumably backward-compatible) and lots of other
things) and I'm not sure if/how that affects code that has no
synchronized block.

But it seems reasonable that the JIT would be allowed to perform some
otherwise "conditional" code execution *before* the condition is
actually evaluated, as long as that code doesn't have any side-effects
(such as assignment of the return value of, say, hashCode() or
StringManager.getString()). The JIT is free to "waste" the CPUs time on
a bet that the conditional branch will be reached, but can discard that
work if the conditional branch is skipped. I'm sure the rules for
"side-effects" include calling methods not yet proven to have any
side-effects which might be a giant rathole that nobody has decided to
jump into, and therefore method calls are always considered "side
effects" just to keep things safe and simple.

-chris



signature.asc
Description: OpenPGP digital signature


Re: RV-Predict bugs

2015-09-15 Thread Christopher Schultz
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
> 5:   goto X

This line should have of course been "goto 17"

> 8:   new java.lang.String
> 10:  dup
> 11:  store s
> 13:  push "foo"
> 15:  call java.lang.String.

... and of course

17: push s
19: return

Sorry for the sloppy (fake!) code.

-chris



signature.asc
Description: OpenPGP digital signature


Re: RV-Predict bugs

2015-09-15 Thread Yilong Li
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 many, many users then you need
> to provide a justification for why there is an issue to back up the
> claims you are making.
>
> > The only thing matters is the Java memory model. And the article I
> > refer to explain exactly why and how this can happen.
>
> No, it didn't. I read that article (and parts of the JMM). While the
> article did state there was a problem it did not explain why there was a
> problem.
>
> 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
> explanation - and continues not to provide a clear explanation when
> asked for one several times - then that is the point where we start to
> think the problem is with the tool.
>

Sorry, I should not assume that the concepts such as happens-before order
and memory model are well understood. Let's talk about how this is allowed
to happen under JMM. Consider the this example again:

if (st_200 == null ) {
st_200 = sm.getString("sc.200");
}
return st_200;

The following is a valid execution trace consists of 5 events:
T1   T2
1   READ  null
2   WRITE s
3 READ s
4 READ ???
5   READ  s

, where s is the result of sm.getString("sc.200").

T1 sees null in field st_200, initializes it, and return the initialized
value, while T2 sees a non-null value in st_200 and skips the
initialization. The question is what value T2 can read and then return in
event 4. This is addressed in JLS $17.4.5 Happens-before Order (
https://docs.oracle.com/javase/specs/jls/se8/html/jls-17.html#jls-17.4.5):

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

Informally, a read *r* is allowed to see the result of a write *w* if there
is no *happens-before* ordering to prevent that read.

The question boils down to: does the write in event 2 prevent event 4 from
reading the initial null value of st_200? No, because there is no
happens-before order involved here. So what kind of constructs introduce
happens-before order? This question is also addressed in the same section
of JLS:

It follows from the above definitions that:

   -

   An unlock on a monitor *happens-before* every subsequent lock on that
   monitor.
   -

   A write to a volatile field (§8.3.1.4
   
   ) *happens-before* every subsequent read of that field.
   -

   A call to start() on a thread *happens-before* any actions in the
   started thread.
   -

   All actions in a thread *happen-before* any other thread successfully
   returns from a join() on that thread.
   -

   The default initialization of any object *happens-before* any other
   actions (other than default-writes) of a program.


> I agree that such non-thread-safe lazy initialization rarely causes
> > problem. But, guys,
>
> 'guys' is not a gender neutral word. Do you really mean to suggest that
> only the male committers look at the other issues? I tend to avoid such
> phraseology where I can and use something like 'all' or 'folks' if
> necessary.
>

I apologize but 'guys' can be gender neutral which is what I meant.


> > please take a look at other issues I reported. There
> > are much more interesting concurrency bugs.
>
> Yes, there are a few more interesting / likely to have an impact bugs.
> The tribes issues I've fixed today look like they were reasonably likely
> to cause issues.
>
> > I am reporting these minor
> > issues only because they are clearly bugs.
>
> They are only clearly bugs once a clear explanation of the concurrency
> issue that underlies many of them has been explained clearly and
> understood.
>
> Opening a large number of bugs (even valid ones) without a clear
> justification is not the way to win friends and influence people. It
> would be far better to open a single, well explained bug, get that
> accepted and fixed and then tell the community that the tool has
> identified more bugs and ask the community how they would like to handle
> them.
>

Sorry, I wasn't aware that the community might not like that. However, I
would argue that many of the bug reports are clear enough for a Tomcat
developer to pinpoint the problem relatively easily. It has the stack
traces of the two 

Re: RV-Predict bugs

2015-09-15 Thread Mark Thomas
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
>> explanation - and continues not to provide a clear explanation when
>> asked for one several times - then that is the point where we start to
>> think the problem is with the tool.
>>
> 
> Sorry, I should not assume that the concepts such as happens-before order
> and memory model are well understood. Let's talk about how this is allowed
> to happen under JMM. Consider the this example again:
> 
> if (st_200 == null ) {
> st_200 = sm.getString("sc.200");
> }
> return st_200;
> 
> The following is a valid execution trace consists of 5 events:
> T1   T2
> 1   READ  null
> 2   WRITE s
> 3 READ s
> 4 READ ???
> 5   READ  s
> 
> , where s is the result of sm.getString("sc.200").
> 
> T1 sees null in field st_200, initializes it, and return the initialized
> value, while T2 sees a non-null value in st_200 and skips the
> initialization. The question is what value T2 can read and then return in
> event 4. This is addressed in JLS $17.4.5 Happens-before Order (
> https://docs.oracle.com/javase/specs/jls/se8/html/jls-17.html#jls-17.4.5):
> 
> 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)*).
> 
> Informally, a read *r* is allowed to see the result of a write *w* if there
> is no *happens-before* ordering to prevent that read.
> 
> The question boils down to: does the write in event 2 prevent event 4 from
> reading the initial null value of st_200? No, because there is no
> happens-before order involved here. So what kind of constructs introduce
> happens-before order? This question is also addressed in the same section
> of JLS:
> 
> It follows from the above definitions that:
> 
>-
> 
>An unlock on a monitor *happens-before* every subsequent lock on that
>monitor.
>-
> 
>A write to a volatile field (§8.3.1.4
>
>) *happens-before* every subsequent read of that field.
>-
> 
>A call to start() on a thread *happens-before* any actions in the
>started thread.
>-
> 
>All actions in a thread *happen-before* any other thread successfully
>returns from a join() on that thread.
>-
> 
>The default initialization of any object *happens-before* any other
>actions (other than default-writes) of a program.

Thank you. That helps fill in a few gaps. 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 reads

- If T2 was executing in isolation the order of the reads wouldn't
  matter

- However, T1 is writing.

So if the writes in T2 are re-ordered and the write from T1 takes place
between them the T2 read for the line 'st_200 == null' could return a
non-null value for st_200 (the value after the write from T1) while the
read for the line 'return st_200;' could return null (the value from
before the write in T1).

Is my understanding correct?

>> I don't have any particular issues in mind, just a suspicion that
>> concurrency issues lie behind some of the hard to reproduce bugs that
>> get reported from time to time. If I could produce the bug I would have
>> fixed it already.
>>
> 
> Technically speaking, RV-Predict doesn't require a developer to be able to
> produce the bug or data race in order to detect it. One can run RV-Predict
> on code that fails only intermittently and RV-Predict may still catch the
> bug. Perhaps it can be helpful to ask the bug reporter to run their code
> against RV-Predict if it's just too hard to extract a test case that can
> reproduce the failure consistently enough.

Good to know. That is certainly worth a try. I'll add something to the
bugs in question.

> Thanks again for the prompt responses and the quick fixes of the reported
> bugs. This has also helped RV-Predict to get into a better shape.

Thanks to you to. It has certainly helped Tomcat improve and the
discussion around these issues continues to help educate the community
as a whole about these issues.

Mark


-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org



RE: RV-Predict bugs

2015-09-15 Thread Caldarale, Charles R
> 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 that independent reads could be issued 
for the field, and that those reads are not necessarily ordered.  This would 
allow the second (in program order) read to observe an older value for the 
field.  However, that argument ignored the fact that if the first read observed 
a null (or zero), it would trigger action that invalidated the second read.  
The compiler (JIT) cannot move the second read to a spot prior to the first due 
to the potential of an intervening write.  An x86 CPU could move the read, but, 
if the write occurred, store forwarding would be used to update the second read 
before the value is materialized by instruction retirement.

> I don't think that T2 can read non-null and then later read null given
> the code we are discussing.

Correct - program order would be violated.

 - 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



RE: RV-Predict bugs

2015-09-15 Thread Caldarale, Charles R
> 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 memory barrier must not be interleaved with statements 
> inside 
> the block, and likewise, nothing after the block can be moved "inside" that 
> block.

Correct, mostly; the exceptions are that operations that can be proven to not 
have any dependencies on those within the block could theoretically be moved to 
inside or prior to the block (but compilers generally won't bother to do that 
when there's a memory barrier).

> But it seems reasonable that the JIT would be allowed to perform some
> otherwise "conditional" code execution *before* the condition is
> actually evaluated, as long as that code doesn't have any side-effects
> (such as assignment of the return value of, say, hashCode() or
> StringManager.getString()).

Yes, speculative executions are allowed, as long as program order isn't 
violated.

> I'm sure the rules for "side-effects" include calling methods not yet proven 
> to 
> have any side-effects which might be a giant rathole that nobody has decided 
> to
> jump into, and therefore method calls are always considered "side effects" 
> just 
> to keep things safe and simple.

Nope.  I spend much of my time inside LLVM these days, and a significant chunk 
of optimizations can be enabled when functions are known not to have side 
effects.  There's a lot of effort put into annotating function declarations to 
let the compiler know that they're safe.

 - 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



Re: RV-Predict bugs

2015-09-15 Thread Yilong Li
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
> >> problem is and the person raising the bug can't provide a clear
> >> explanation - and continues not to provide a clear explanation when
> >> asked for one several times - then that is the point where we start to
> >> think the problem is with the tool.
> >>
> >
> > Sorry, I should not assume that the concepts such as happens-before order
> > and memory model are well understood. Let's talk about how this is
> allowed
> > to happen under JMM. Consider the this example again:
> >
> > if (st_200 == null ) {
> > st_200 = sm.getString("sc.200");
> > }
> > return st_200;
> >
> > The following is a valid execution trace consists of 5 events:
> > T1   T2
> > 1   READ  null
> > 2   WRITE s
> > 3 READ s
> > 4 READ ???
> > 5   READ  s
> >
> > , where s is the result of sm.getString("sc.200").
> >
> > T1 sees null in field st_200, initializes it, and return the initialized
> > value, while T2 sees a non-null value in st_200 and skips the
> > initialization. The question is what value T2 can read and then return in
> > event 4. This is addressed in JLS $17.4.5 Happens-before Order (
> > https://docs.oracle.com/javase/specs/jls/se8/html/jls-17.html#jls-17.4.5
> ):
> >
> > 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)*).
> >
> > Informally, a read *r* is allowed to see the result of a write *w* if
> there
> > is no *happens-before* ordering to prevent that read.
> >
> > The question boils down to: does the write in event 2 prevent event 4
> from
> > reading the initial null value of st_200? No, because there is no
> > happens-before order involved here. So what kind of constructs introduce
> > happens-before order? This question is also addressed in the same section
> > of JLS:
> >
> > It follows from the above definitions that:
> >
> >-
> >
> >An unlock on a monitor *happens-before* every subsequent lock on that
> >monitor.
> >-
> >
> >A write to a volatile field (§8.3.1.4
> ><
> https://docs.oracle.com/javase/specs/jls/se8/html/jls-8.html#jls-8.3.1.4>
> >) *happens-before* every subsequent read of that field.
> >-
> >
> >A call to start() on a thread *happens-before* any actions in the
> >started thread.
> >-
> >
> >All actions in a thread *happen-before* any other thread successfully
> >returns from a join() on that thread.
> >-
> >
> >The default initialization of any object *happens-before* any other
> >actions (other than default-writes) of a program.
>
> Thank you. That helps fill in a few gaps. 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 reads
>
> - If T2 was executing in isolation the order of the reads wouldn't
>   matter
>
> - However, T1 is writing.
>
> So if the writes in T2 are re-ordered and the write from T1 takes place
> between them the T2 read for the line 'st_200 == null' could return a
> non-null value for st_200 (the value after the write from T1) while the
> read for the line 'return st_200;' could return null (the value from
> before the write in T1).
>
> Is my understanding correct?
>

Not really. I have been trying to avoid getting into the discussion about
the low-level stuffs such as instruction reordering and caching. Let's stay
on the abstraction level of JMM. When reasoning on the level of JMM, one
should not care about reordering or speculative read. The happens-before
order is the only thing that matters. I know it could be confusing because
of the name, but happens-before order is orthogonal to whether two
operations can be reordered. The latter is the low-level detail that JMM
abstracts away. The first read in T2 does happen-before the second read
because of the intra-thread semantics (sorry, I forgot to include
intra-thread semantics when I pasted the constructs that introduce HB
order). However, in order to reason about what value the second read can
see, one has to stick to the two rules specified by JMM I quoted in my
previous message. In short, when reasoning with JMM, just assume the
instructions are executed in the same order as in the source code and start
reasoning about what value a 

Re: RV-Predict bugs

2015-09-15 Thread Christopher Schultz
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 is and the person raising the bug can't provide a clear
>>> explanation - and continues not to provide a clear explanation when
>>> asked for one several times - then that is the point where we start to
>>> think the problem is with the tool.
>>>
>>
>> Sorry, I should not assume that the concepts such as happens-before order
>> and memory model are well understood. Let's talk about how this is allowed
>> to happen under JMM. Consider the this example again:
>>
>> if (st_200 == null ) {
>> st_200 = sm.getString("sc.200");
>> }
>> return st_200;
>>
>> The following is a valid execution trace consists of 5 events:
>> T1   T2
>> 1   READ  null
>> 2   WRITE s
>> 3 READ s
>> 4 READ ???
>> 5   READ  s
>>
>> , where s is the result of sm.getString("sc.200").
>>
>> T1 sees null in field st_200, initializes it, and return the initialized
>> value, while T2 sees a non-null value in st_200 and skips the
>> initialization. The question is what value T2 can read and then return in
>> event 4. This is addressed in JLS $17.4.5 Happens-before Order (
>> https://docs.oracle.com/javase/specs/jls/se8/html/jls-17.html#jls-17.4.5):
>>
>> 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)*).
>>
>> Informally, a read *r* is allowed to see the result of a write *w* if there
>> is no *happens-before* ordering to prevent that read.
>>
>> The question boils down to: does the write in event 2 prevent event 4 from
>> reading the initial null value of st_200? No, because there is no
>> happens-before order involved here. So what kind of constructs introduce
>> happens-before order? This question is also addressed in the same section
>> of JLS:
>>
>> It follows from the above definitions that:
>>
>>-
>>
>>An unlock on a monitor *happens-before* every subsequent lock on that
>>monitor.
>>-
>>
>>A write to a volatile field (§8.3.1.4
>>
>>) *happens-before* every subsequent read of that field.
>>-
>>
>>A call to start() on a thread *happens-before* any actions in the
>>started thread.
>>-
>>
>>All actions in a thread *happen-before* any other thread successfully
>>returns from a join() on that thread.
>>-
>>
>>The default initialization of any object *happens-before* any other
>>actions (other than default-writes) of a program.
> 
> Thank you. That helps fill in a few gaps. 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 reads
> 
> - If T2 was executing in isolation the order of the reads wouldn't
>   matter
> 
> - However, T1 is writing.
> 
> So if the writes in T2 are re-ordered and the write from T1 takes place
> between them the T2 read for the line 'st_200 == null' could return a
> non-null value for st_200 (the value after the write from T1) while the
> read for the line 'return st_200;' could return null (the value from
> before the write in T1).
> 
> Is my understanding correct?

That sounds crazy (but may actually be correct).

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. T1 can only
affect its own local views of the references and, of course, main
memory. Once T1 writes to main memory, T2 can see the changes. I don't
think the JMM allows threads to change other threads' references
directly without writing to main memory.

I don't think that T2 can read non-null and then later read null given
the code we are discussing. If T1 writes /null/ to main memory, then
this can happen,but I think we can all agree T1 is *not* gong to write null.

>>> I don't have any particular issues in mind, just a suspicion that
>>> concurrency issues lie behind some of the hard to reproduce bugs that
>>> get reported from time to time. If I could produce the bug I would have
>>> fixed it already.
>>>
>>
>> Technically speaking, RV-Predict doesn't require a developer to be able to
>> produce the bug or data race in order to detect it. One can run RV-Predict
>> on code that fails only intermittently and RV-Predict may still catch the
>> bug. Perhaps 

Re: RV-Predict bugs

2015-09-15 Thread Yilong Li
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
> happens
> > > in that case is the object is redundantly created and then garbage
> > > collected later; no damage.
>
> > No, it's not right. It's possible (although very unlikely) that this
> method
> > could return null and results in a null pointer exception later.
>
> Again, that cannot happen; see below.
>
> > Intra-thread semantics says that event 3 (the first read of the field
> > hashCode) happens before event 4 (the second read of field hashCode) but
> it
> > has no effect on the value event 4 can see (because event 3 is also a
> read
> > rather than a write).
>
> You're mixing up inter- and intra-thread semantics and completely ignoring
> the write to hashCode when the initially observed value is zero.
> Intra-thread semantics require that operations occur in program order, so
> the initial zero (or null) check results in a non-zero (or non-null) write
> to the field of interest; control flow cannot be ignored here.  If your
> supposition were correct, a compiler (or CPU) would be free to migrate
> actions dependent on a conditional block to a spot prior to that
> conditional block - clearly that is nonsense.


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.

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


RE: RV-Predict bugs

2015-09-15 Thread Caldarale, Charles R
> 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 reads

Depends on what was really meant by the ??? notation.  If it were another 
reference to st_200, then the example ignores the potential write to st_200.

> - If T2 was executing in isolation the order of the reads wouldn't
>   matter

Correct, assuming there is no write in T2's control flow.

> - However, T1 is writing.

> So if the writes

I'll assume you meant "reads" there.

> in T2 are re-ordered and the write from T1 takes place between them the T2 
> read for the line 'st_200 == null' could return a non-null value for st_200 
> (the value after the write from T1) while the read for the line 'return 
> st_200;' could return null (the value from before the write in T1).

No - that would violate program order (intra-thread semantics).  The compiler 
cannot legally move the read for "return st_200" to a point before the 
potential write to st_200.  The CPU can speculatively read for the return 
value, but must discard such speculation if a write were to occur (or use store 
forwarding to update the read).
 
 - 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



Re: RV-Predict bugs

2015-09-15 Thread Mark Thomas
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 nothing
>>   that requires a happens-before relationship between the two reads
> 
> Depends on what was really meant by the ??? notation.  If it were another 
> reference to st_200, then the example ignores the potential write to st_200.
> 
>> - If T2 was executing in isolation the order of the reads wouldn't
>>   matter
> 
> Correct, assuming there is no write in T2's control flow.
> 
>> - However, T1 is writing.
> 
>> So if the writes
> 
> I'll assume you meant "reads" there.

I'd did. Thanks.

>> in T2 are re-ordered and the write from T1 takes place between them the T2 
>> read for the line 'st_200 == null' could return a non-null value for st_200 
>> (the value after the write from T1) while the read for the line 'return 
>> st_200;' could return null (the value from before the write in T1).
> 
> No - that would violate program order (intra-thread semantics).  The compiler 
> cannot legally move the read for "return st_200" to a point before the 
> potential write to st_200.  The CPU can speculatively read for the return 
> value, but must discard such speculation if a write were to occur (or use 
> store forwarding to update the read).

Thanks for sticking with me on this. I'm finding it hugely helpful. I
think I need a few more references to make things clearer so I'm going
to restate the problem.

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=Write at line n

So T2 has two reads, T2R1 and T2R4.
Depending on the value read for T2R1 there may be a write at T2W2.
If there is a write there is a happens before relationship between T2R1
and T2R4.

Consider the following sequence

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)

Because T2R1 reads a non-null value there is no write in T2.
Therefore there is no happens-before relationship between T2R1 and T2R4
because there is no intervening write in that thread (the write happens
in T1).
Therefore the re-ordering is allowed to happen.
And we get the unexpected result.

Or

The write at T1W2 is sufficient to enforce the happens before
relationship between T2R1 and T2R4. In which case what is the point of
volatile? What do I gain by using it?

A still slightly confused,

Mark


-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org



Re: RV-Predict bugs

2015-09-15 Thread Mark Thomas
On 15/09/2015 21:51, Yilong Li wrote:
> On Tue, Sep 15, 2015 at 1:09 PM, Mark Thomas <ma...@apache.org> 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:
>>>
>>>> - The two reads in T2 may be re-ordered because, in T2, there is nothing
>>>>   that requires a happens-before relationship between the two reads
>>>
>>> Depends on what was really meant by the ??? notation.  If it were
>> another reference to st_200, then the example ignores the potential write
>> to st_200.
>>>
>>>> - If T2 was executing in isolation the order of the reads wouldn't
>>>>   matter
>>>
>>> Correct, assuming there is no write in T2's control flow.
>>>
>>>> - However, T1 is writing.
>>>
>>>> So if the writes
>>>
>>> I'll assume you meant "reads" there.
>>
>> I'd did. Thanks.
>>
>>>> in T2 are re-ordered and the write from T1 takes place between them the
>> T2
>>>> read for the line 'st_200 == null' could return a non-null value for
>> st_200
>>>> (the value after the write from T1) while the read for the line 'return
>>>> st_200;' could return null (the value from before the write in T1).
>>>
>>> No - that would violate program order (intra-thread semantics).  The
>> compiler cannot legally move the read for "return st_200" to a point before
>> the potential write to st_200.  The CPU can speculatively read for the
>> return value, but must discard such speculation if a write were to occur
>> (or use store forwarding to update the read).
>>
>> Thanks for sticking with me on this. I'm finding it hugely helpful. I
>> think I need a few more references to make things clearer so I'm going
>> to restate the problem.
>>
>> 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=Write at line n
>>
>> So T2 has two reads, T2R1 and T2R4.
>> Depending on the value read for T2R1 there may be a write at T2W2.
>> If there is a write there is a happens before relationship between T2R1
>> and T2R4.
>>
>> Consider the following sequence
>>
>> 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)
>>
>> Because T2R1 reads a non-null value there is no write in T2.
>> Therefore there is no happens-before relationship between T2R1 and T2R4
>> because there is no intervening write in that thread (the write happens
>> in T1).
>> Therefore the re-ordering is allowed to happen.
>> And we get the unexpected result.
>>
>> Or
>>
>> The write at T1W2 is sufficient to enforce the happens before
>> relationship between T2R1 and T2R4. In which case what is the point of
>> volatile? What do I gain by using it?
>>
> 
> Again, as I mentioned in my previous message, I am afraid this is not the
> correct way to use HB relationship. To make things more clear, I steal this
> transformation from Jeremy Manson's article I sent before:

That doesn't help my improve my understanding at all.

What I'm looking for is an explanation - ideally using my example above
- of exactly how T2R4 can return null while T2R1 reads a non-null value.
"Because the JMM says it can" is not a sufficient explanation.  I
believe that the JMM says it can but I don't understand how this can
actually happen. What I am looking for is the explanation of how. Your
message at 16.59 (UTC) was heading in the right direction but the
explanation skipped over the crucial part.

Providing the explanation of how is the difference between:
a) a bug being theoretically valid based on the JMM but a practically
never going to happen because JVMs aren't written that way
vs.
b) a bug that can happen with current JVMs.

We care a lot more about b) than we do a). And we may choose to not to
care at all about a).

Assuming the answer is b) then there is potentially a wider benefit if a
clear explanation of the why can be provided since that is the sort of
thing that makes it a lot easier to convince people there is a real
problem they need to fix.

Mark

-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org



Re: RV-Predict bugs

2015-09-15 Thread Yilong Li
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   - 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
>
>


RE: RV-Predict bugs

2015-09-15 Thread Caldarale, Charles R
> 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=Write at line n

> So T2 has two reads, T2R1 and T2R4.

> Depending on the value read for T2R1 there may be a write at T2W2.
> If there is a write there is a happens before relationship between T2R1
> and T2R4.

There is also a happens-before relationship between T2R1 and T2R4 due to JLS 
Section 14.2 (Blocks), not Section 17.4 (Memory Model).  The JMM cannot be 
considered in a vacuum.

> Consider the following sequence
> 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)

The above is not permitted due to Section 14.2 (although it would be by 17.4).  
The compiler must not move T2R4 in front of T2R1 because of the potential of 
T2W2 occurring.  Correct operation is dependent on the CPU observing the same 
value for T2R1 and T2R4, which is implemented in all current hardware I'm aware 
of by not permitting reordering of accesses to the same memory location (e.g., 
see Chapter 8 of the Intel 64 Architecture SDM, Volume 3 - System Programming 
Guide).  Such accesses are usually just combined when they occur.

> Because T2R1 reads a non-null value there is no write in T2.

> Therefore there is no happens-before relationship between T2R1 and T2R4
> because there is no intervening write in that thread (the write happens
> in T1).
> Therefore the re-ordering is allowed to happen.
> And we get the unexpected result.

If the JMM were the only controlling specification, that would be true.  Since 
the JVM must also conform to Section 14, the happens-before order exists, and 
we don't have a problem.

> The write at T1W2 is sufficient to enforce the happens before
> relationship between T2R1 and T2R4.

Yes, the potential of the write occurring is enough.

> In which case what is the point of volatile? What do I gain by using it?

In this particular case, nothing.  Volatile is often useful inside a loop where 
you want to make sure that the reference is not hoisted outside of the loop, 
effectively becoming a constant for the duration of the loop.

 - 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



Re: RV-Predict bugs

2015-09-15 Thread Yilong Li
On Tue, Sep 15, 2015 at 1:09 PM, Mark Thomas <ma...@apache.org> 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:
> >
> >> - The two reads in T2 may be re-ordered because, in T2, there is nothing
> >>   that requires a happens-before relationship between the two reads
> >
> > Depends on what was really meant by the ??? notation.  If it were
> another reference to st_200, then the example ignores the potential write
> to st_200.
> >
> >> - If T2 was executing in isolation the order of the reads wouldn't
> >>   matter
> >
> > Correct, assuming there is no write in T2's control flow.
> >
> >> - However, T1 is writing.
> >
> >> So if the writes
> >
> > I'll assume you meant "reads" there.
>
> I'd did. Thanks.
>
> >> in T2 are re-ordered and the write from T1 takes place between them the
> T2
> >> read for the line 'st_200 == null' could return a non-null value for
> st_200
> >> (the value after the write from T1) while the read for the line 'return
> >> st_200;' could return null (the value from before the write in T1).
> >
> > No - that would violate program order (intra-thread semantics).  The
> compiler cannot legally move the read for "return st_200" to a point before
> the potential write to st_200.  The CPU can speculatively read for the
> return value, but must discard such speculation if a write were to occur
> (or use store forwarding to update the read).
>
> Thanks for sticking with me on this. I'm finding it hugely helpful. I
> think I need a few more references to make things clearer so I'm going
> to restate the problem.
>
> 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=Write at line n
>
> So T2 has two reads, T2R1 and T2R4.
> Depending on the value read for T2R1 there may be a write at T2W2.
> If there is a write there is a happens before relationship between T2R1
> and T2R4.
>
> Consider the following sequence
>
> 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)
>
> Because T2R1 reads a non-null value there is no write in T2.
> Therefore there is no happens-before relationship between T2R1 and T2R4
> because there is no intervening write in that thread (the write happens
> in T1).
> Therefore the re-ordering is allowed to happen.
> And we get the unexpected result.
>
> Or
>
> The write at T1W2 is sufficient to enforce the happens before
> relationship between T2R1 and T2R4. In which case what is the point of
> volatile? What do I gain by using it?
>

Again, as I mentioned in my previous message, I am afraid this is not the
correct way to use HB relationship. To make things more clear, I steal this
transformation from Jeremy Manson's article I sent before:

r1 = hash;
if (hash == 0) {
  r1 = hash = // calculate hash
}
return r1;
This is a legal transformation w.r.t JMM (though really impractical) and it
is easy to see that this method can return 0 under certain interleaving.

Yilong


> A still slightly confused,
>
> Mark
>
>
> -
> To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
> For additional commands, e-mail: dev-h...@tomcat.apache.org
>
>


RE: RV-Predict bugs

2015-09-15 Thread Caldarale, Charles R
> 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.

 - 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



Re: RV-Predict bugs

2015-09-15 Thread Mark Thomas
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 there is an issue to back up the
claims you are making.

> The only thing matters is the Java memory model. And the article I
> refer to explain exactly why and how this can happen.

No, it didn't. I read that article (and parts of the JMM). While the
article did state there was a problem it did not explain why there was a
problem.

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
explanation - and continues not to provide a clear explanation when
asked for one several times - then that is the point where we start to
think the problem is with the tool.

> I agree that such non-thread-safe lazy initialization rarely causes
> problem. But, guys,

'guys' is not a gender neutral word. Do you really mean to suggest that
only the male committers look at the other issues? I tend to avoid such
phraseology where I can and use something like 'all' or 'folks' if
necessary.

> please take a look at other issues I reported. There
> are much more interesting concurrency bugs.

Yes, there are a few more interesting / likely to have an impact bugs.
The tribes issues I've fixed today look like they were reasonably likely
to cause issues.

> I am reporting these minor
> issues only because they are clearly bugs.

They are only clearly bugs once a clear explanation of the concurrency
issue that underlies many of them has been explained clearly and understood.

Opening a large number of bugs (even valid ones) without a clear
justification is not the way to win friends and influence people. It
would be far better to open a single, well explained bug, get that
accepted and fixed and then tell the community that the tool has
identified more bugs and ask the community how they would like to handle
them.

I'm still not completely happy that I understand why this is a bug. The
article Chunk provided a link to is a good start and if I make a few
assumptions about what I think the JMM means in a few places then it
does make sense. However, I'd still like to see a step-by-step guide to
how this goes wrong with references to the JMM to explain why each step
is legal.

> Mark, if you have a specific concurrency issue you would like to
> investigate, the best way is to run RV-Predict against the code that once
> revealed the problem.

I don't have any particular issues in mind, just a suspicion that
concurrency issues lie behind some of the hard to reproduce bugs that
get reported from time to time. If I could produce the bug I would have
fixed it already.

It will be interesting to see - once all these bugs have been fixed -
whether the stability of the CI test runs improves. There have been
issues around some of the async tests for example that might have a root
cause in one of these bugs.

> Even if the failure occurs rarely, RV-Predict may be
> able to identify the cause for you. I get all these race reports by running
> RV-Predict against the test suite so if the small unit test doesn't
> exercise the problematic code enough you may not get the specific answer
> you are looking for.

Once we have a test case and if concurrency issues are suspected then
I'd certainly try RV-Predict before trying to debug it manually.

Mark

> 
> Yilong
> 
> On Sun, Sep 13, 2015 at 1:30 PM, Mark Thomas  wrote:
> 
>> 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  > wrote:
>
> 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.
>
>
> I am going to stop here because these are all the bugs reported by
> RV-Predict in one run of the entire test suite.

 OK. Lets resolve these and then see where we stand.


>>> As far as I am concerned, I would prefer batch closing these "issues"
>>> nobody ever had.
>>
>> That is very tempting.
>>
>> Looking at the articles by the folks that are the experts in the field
>> (i.e. the authors of JSR-133) it looks like the issues raised are valid
>> - even if we don't see then very often / at all. Despite that, I'd be a
>> lot happier with a clearer explanation of what can go wrong and why/how.
>>
>> On the plus side, the issues I've looked at so far 

RV-Predict bugs

2015-09-13 Thread 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 report false positives. Each report needs to be looked at
evaluated by a human to determine if it is genuine or not.

2. Sometimes the tool might report something that is technically an
issue but the Tomcat developers have deliberately decided to code it
that way. BZ 58367 is an example of this. Again, each issue needs to be
evaluated by a human before adding it to Bugzilla.

The race condition in BZ 58367 can't cause any harm. At worst the code
may be slightly inefficient but the cost of the plumbing that would be
necessary to avoid the race condition was viewed as likely to add more
overhead than the problem it was trying to solve.

Many of these optimisation decisions were made several major versions
ago and Java performance and compiler optimization has changed
significantly since then. It may be time to revisit those decisions but
we are unlikely to unless the code is flagged up as causing a
performance bottleneck.

I suggest that you follow each of these bugs as we work through them to
get a sense of what the Tomcat team considers to be a bug and what it
considers not to be a bug. With that, you can do some filtering of these
reports before you add them to Bugzilla.

I don't want you to think I am completely against tools like RV-Predict.
Far from it. I know that there have been some tricky to find race
conditions in the connectors and I suspect a number of the open bugs in
Bugzilla have similar tricky to find race conditions as their root
cause. Having a tool that can find these would be a huge benefit. What
we need is to be able to filter out the noise and concentrate on the
important issues.

Mark

-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org



Re: RV-Predict bugs

2015-09-13 Thread Felix Schumacher

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 report false positives. Each report needs to be looked at
evaluated by a human to determine if it is genuine or not.

2. Sometimes the tool might report something that is technically an
issue but the Tomcat developers have deliberately decided to code it
that way. BZ 58367 is an example of this. Again, each issue needs to be
evaluated by a human before adding it to Bugzilla.
3. Probably many of those reports are already included in the coverity 
scans.


Regards,
 Felix


The race condition in BZ 58367 can't cause any harm. At worst the code
may be slightly inefficient but the cost of the plumbing that would be
necessary to avoid the race condition was viewed as likely to add more
overhead than the problem it was trying to solve.

Many of these optimisation decisions were made several major versions
ago and Java performance and compiler optimization has changed
significantly since then. It may be time to revisit those decisions but
we are unlikely to unless the code is flagged up as causing a
performance bottleneck.

I suggest that you follow each of these bugs as we work through them to
get a sense of what the Tomcat team considers to be a bug and what it
considers not to be a bug. With that, you can do some filtering of these
reports before you add them to Bugzilla.

I don't want you to think I am completely against tools like RV-Predict.
Far from it. I know that there have been some tricky to find race
conditions in the connectors and I suspect a number of the open bugs in
Bugzilla have similar tricky to find race conditions as their root
cause. Having a tool that can find these would be a huge benefit. What
we need is to be able to filter out the noise and concentrate on the
important issues.

Mark

-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org




-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org



Re: RV-Predict bugs

2015-09-13 Thread 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 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.
> 
> 
> I am going to stop here because these are all the bugs reported by
> RV-Predict in one run of the entire test suite.

OK. Lets resolve these and then see where we stand.



> BZ 58367 is clearly a data race bug that is harmful. So are 58368 &
> 58369. Consider the following code:
> 
> if(st_200 == null ) {
> st_200 = sm.getString("sc.200");
> }
> return st_200;
> 
> Since the field st_200 is in a data race, it's legal under JMM (Java
> memory model) for this method to return null even when the first read of
> st_200 returns a non-null value.

How? Writes to references are atomic. sm.getString("sc.200"); is always
going to return the same non-null String so once a thread has seen a
non-null value for st_200 how can it later see a null one?

> If you want it to be thread-safe, you
> have to ensure there is at most one memory read:
> 
> String s = st_200;
> if(s == null ) {
> st_200 = s = sm.getString("sc.200");
> }
> return s;
> 
> Only in this way, the data race becomes benign.

I can see this would help if something was changing the value of st_200
from non-null to null, but nothing is.

Mark

-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org



Re: RV-Predict bugs

2015-09-13 Thread Mark Thomas
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) into account when writing concurrent
> code. So it's generally a good idea to remove any data race.
> 
> In short, when st_200 is in a data race, the two reads of st_200 can
> happen out-of-order because of many tricky reasons (e.g., instruction
> reordering, caching effect, etc). Sequential consistency is only
> guaranteed for data-race-free program. Here is a more detailed article
> by Jeremy Manson explaining such non-thread-safe lazy
> initialization: 
> http://jeremymanson.blogspot.com/2008/12/benign-data-races-in-java.html.
> Jeremy is one of the authors of JMM.

While I'm prepared to believe there is a problem here I'd be a lot
happier with a clear explanation of what the problem is rather than some
vague hand-waving under the heading of 'tricky reasons'. What I am
looking for is a step by step description of how code like this can go
wrong with references to the JMM to explain why the behaviour that
causes the problem (e.g. re-ordering) is permitted. I have yet to find
such a description.

Mark



> 
> Yilong
> 
> On Sun, Sep 13, 2015 at 9:45 AM, Mark Thomas  > wrote:
> 
> 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
> > current set have been evaluated. To be honest it would have been 
> better
> > if you had paused after adding 58367-58379.
> >
> >
> > I am going to stop here because these are all the bugs reported by
> > RV-Predict in one run of the entire test suite.
> 
> OK. Lets resolve these and then see where we stand.
> 
> 
> 
> > BZ 58367 is clearly a data race bug that is harmful. So are 58368 &
> > 58369. Consider the following code:
> >
> > if(st_200 == null ) {
> > st_200 = sm.getString("sc.200");
> > }
> > return st_200;
> >
> > Since the field st_200 is in a data race, it's legal under JMM (Java
> > memory model) for this method to return null even when the first read of
> > st_200 returns a non-null value.
> 
> How? Writes to references are atomic. sm.getString("sc.200"); is always
> going to return the same non-null String so once a thread has seen a
> non-null value for st_200 how can it later see a null one?
> 
> > If you want it to be thread-safe, you
> > have to ensure there is at most one memory read:
> >
> > String s = st_200;
> > if(s == null ) {
> > st_200 = s = sm.getString("sc.200");
> > }
> > return s;
> >
> > Only in this way, the data race becomes benign.
> 
> I can see this would help if something was changing the value of st_200
> from non-null to null, but nothing is.
> 
> Mark
> 
> 


-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org



Re: RV-Predict bugs

2015-09-13 Thread Yilong Li
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 take a look at other issues I reported. There
are much more interesting concurrency bugs. I am reporting these minor
issues only because they are clearly bugs.

Mark, if you have a specific concurrency issue you would like to
investigate, the best way is to run RV-Predict against the code that once
revealed the problem. Even if the failure occurs rarely, RV-Predict may be
able to identify the cause for you. I get all these race reports by running
RV-Predict against the test suite so if the small unit test doesn't
exercise the problematic code enough you may not get the specific answer
you are looking for.

Yilong

On Sun, Sep 13, 2015 at 1:30 PM, Mark Thomas  wrote:

> 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  >>> > wrote:
> >>>
> >>> 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.
> >>>
> >>>
> >>> I am going to stop here because these are all the bugs reported by
> >>> RV-Predict in one run of the entire test suite.
> >>
> >> OK. Lets resolve these and then see where we stand.
> >>
> >>
> > As far as I am concerned, I would prefer batch closing these "issues"
> > nobody ever had.
>
> That is very tempting.
>
> Looking at the articles by the folks that are the experts in the field
> (i.e. the authors of JSR-133) it looks like the issues raised are valid
> - even if we don't see then very often / at all. Despite that, I'd be a
> lot happier with a clearer explanation of what can go wrong and why/how.
>
> On the plus side, the issues I've looked at so far have provided
> opportunities for clean-up in trunk.
>
> I'm hoping (but haven't look at all of them yet) that at least one of
> these reports is going to identify the root cause of one of those hard
> to reproduce / hard to track down concurrency issues.
>
> Mark
>
>
> -
> To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
> For additional commands, e-mail: dev-h...@tomcat.apache.org
>
>


Re: RV-Predict bugs

2015-09-13 Thread Rémy Maucherat
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 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.
> >
> >
> > I am going to stop here because these are all the bugs reported by
> > RV-Predict in one run of the entire test suite.
>
> OK. Lets resolve these and then see where we stand.
>
>
> As far as I am concerned, I would prefer batch closing these "issues"
nobody ever had.

Rémy


Re: RV-Predict bugs

2015-09-13 Thread Mark Thomas
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 >> > wrote:
>>>
>>> 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.
>>>
>>>
>>> I am going to stop here because these are all the bugs reported by
>>> RV-Predict in one run of the entire test suite.
>>
>> OK. Lets resolve these and then see where we stand.
>>
>>
> As far as I am concerned, I would prefer batch closing these "issues"
> nobody ever had.

That is very tempting.

Looking at the articles by the folks that are the experts in the field
(i.e. the authors of JSR-133) it looks like the issues raised are valid
- even if we don't see then very often / at all. Despite that, I'd be a
lot happier with a clearer explanation of what can go wrong and why/how.

On the plus side, the issues I've looked at so far have provided
opportunities for clean-up in trunk.

I'm hoping (but haven't look at all of them yet) that at least one of
these reports is going to identify the root cause of one of those hard
to reproduce / hard to track down concurrency issues.

Mark


-
To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org
For additional commands, e-mail: dev-h...@tomcat.apache.org