Velocity Reviews (http://www.velocityreviews.com/forums/index.php)
-   C++ (http://www.velocityreviews.com/forums/f39-c.html)

 Joshua Maurice 06-15-2011 11:56 PM

talking about C++0x. (You don't need to review it. I'll provide the
relevant context here.)

Consider the following code.

/*** code 1 ***/
// Initially
atomic<int> x(0), y(0);

y.store(1, memory_order_release);

x.store(1, memory_order_release);

/***************/

Q1. First, am I right in concluding that in the above code, all of the
loads and stores might as well be memory_order_relaxed, right?

Q2. Second, is the following end condition possible?
r1 == 0 && r2 == 1 && r3 == 0

Let's try a simple proof.

Sequentially consistent memory operations exist in a single global
total order S. (29.3 / 3)
Thus fence 1 precedes fence 2 in S, or fence 2 precedes fence 1 in S.

Case 1 - fence 1 precedes fence 3 in S.

I believe that 29.3/6 means, in my own translation:
[]
If atomic write A on M is sequenced-before seq_cst fence X, and
seq_cst fence X precedes seq_cst fence Y in the total order S, and
seq_cst fence Y is sequenced-before atomic read B on M,
then B sees the value of the write A, or B sees a write later in the
modification order.
[/]
We know that:
"y.store(1, memory_order_release);" is sequenced-before fence 1,
and
fence 1 precedes fence 3 in S, and
fence 3 is sequenced-before "r3 = y.load(memory_order_acquire);"
Thus we can use 29.3/6 to conclude: r3 sees the value from "y.store(1,
memory_order_release);", or it sees a writer later in the modification
order. There is no such later write, and thus r3 must be 1.

Case 2 - fence 3 precedes fence 1 in S.

Now, if we could prove that NOT (r1 == 0 && r2 == 1), then we would be
done with the proof overall. The difficulty is in trying to prove
this.

The most relevant text appears to be 29.3/7. The exact text from n3242
is:
[]
For atomic operations A and B on an atomic object M, if there are
memory_order_seq_cst fences X and Y such that A is sequenced before X,
Y is sequenced before B, and X precedes Y in S, then B occurs later
than A in the modification order of M.
[/]

There is a typo, or at least an ambiguity. Only writes (or read-modify-
write operations) appear in a modification order. Reads do not. I
initially thought that the intention was the following reading:
[]
For atomic >>write (and/or atomic read-modify-write operations)<< A
and B on an atomic object M, if there are memory_order_seq_cst fences
X and Y such that A is sequenced before X, Y is sequenced before B,
and X precedes Y in S, then B occurs later than A in the modification
order of M.
[/]

With that understanding, we cannot prove NOT (r1 == 0 && r2 == 1) with
just 29.3/7.

Anthony Williams in the comp.programming.threads (who is apparently on
the concurrency working group), initially had a different
interpretation. I just reread it several times, and I'm not quite sure
what he's trying to say. He initially thought that you can use it
directly to prove that NOT (r1 == 0 && r2 == 1).

I /think/ I might be able to phrase Anthony's interpretation in the
following way. Here's Q3:
For
seq_cst fences X and Y,
atomic reads A and B on atomic object M,
if
A sees the value from an atomic write C, and
B sees the value from an atomic write D (which may be C), and
A is sequenced-before X, and
X precedes Y in the total order S on seq_cst operations, and
Y is sequenced-before B,
then
Can D precede C in the modification order of M?

I /think/ Anthony is interpreting 29.3/7 as meaning that: D must be
the same write as C, or C must precede D in the modification order of
M. If we have that, then we can prove that NOT (r1 == 0 && r2 == 1).
Is that the intent of 29.3/7? Should we submit this as a defect?

PS: As normal please forgive me for any mistakes or typos, and please
point them out. Non-sequentially consistent stuff is /really hard/ to

 Chris M. Thomasson 06-16-2011 07:28 AM

"Joshua Maurice" <joshuamaurice@gmail.com> wrote in message
> talking about C++0x. (You don't need to review it. I'll provide the
> relevant context here.)
>
>
> Consider the following code.

[...]

> Q1. First, am I right in concluding that in the above code, all of the
> loads and stores might as well be memory_order_relaxed, right?

I think you are correct.

> Q2. Second, is the following end condition possible?
> r1 == 0 && r2 == 1 && r3 == 0

FWIW, Relacy Race Detector says that the condition is indeed possible; here
is a test case:

http://pastebin.com/G4yDLyRy

[...]

 Chris M. Thomasson 06-16-2011 07:41 AM

"Chris M. Thomasson" <cristom@charter.net> wrote in message
> "Joshua Maurice" <joshuamaurice@gmail.com> wrote in message
>> talking about C++0x. (You don't need to review it. I'll provide the
>> relevant context here.)
>>
>>
>> Consider the following code.

> [...]
>
>> Q1. First, am I right in concluding that in the above code, all of the
>> loads and stores might as well be memory_order_relaxed, right?

>
> I think you are correct.
>
>
>> Q2. Second, is the following end condition possible?
>> r1 == 0 && r2 == 1 && r3 == 0

>
> FWIW, Relacy Race Detector says that the condition is indeed possible;
> here is a test case:
>
> http://pastebin.com/G4yDLyRy

ARGHGHGHGHGH! I posted a version with a damn typo! I need to say that:

Relacy Race Detector is NOT reporting that is condition is possible!

Fixed code:

http://pastebin.com/tE1TX1sx

DAMN IT!!!!

SORRY!

;^o

 Anthony Williams 06-16-2011 08:42 AM

Joshua Maurice <joshuamaurice@gmail.com> writes:

> Consider the following code.
>
> /*** code 1 ***/
> // Initially
> atomic<int> x(0), y(0);
>
> y.store(1, memory_order_release);
>
> x.store(1, memory_order_release);
>
> /***************/
>
> Q1. First, am I right in concluding that in the above code, all of the
> loads and stores might as well be memory_order_relaxed, right?

Yes.

> Q2. Second, is the following end condition possible?
> r1 == 0 && r2 == 1 && r3 == 0

Yes.

> Anthony Williams in the comp.programming.threads (who is apparently on
> the concurrency working group), initially had a different
> interpretation. I just reread it several times, and I'm not quite sure
> what he's trying to say. He initially thought that you can use it
> directly to prove that NOT (r1 == 0 && r2 == 1).

But I now believe I'm mistaken. After checking my notes, we discussed
requiring that seq_cst fences ordered loads as in this example, but
decided against it. 29.3p7 is intended to apply only to writes.

Anthony
--
Author of C++ Concurrency in Action http://www.stdthread.co.uk/book/
Just Software Solutions Ltd http://www.justsoftwaresolutions.co.uk
15 Carrallack Mews, St Just, Cornwall, TR19 7UL, UK. Company No. 5478976

 Joshua Maurice 06-16-2011 09:47 AM

On Jun 16, 12:41*am, "Chris M. Thomasson" <cris...@charter.net> wrote:
> "Chris M. Thomasson" <cris...@charter.net> wrote in messagenews:fgiKp.1272\$tp.587@newsfe06.iad...
>
>
>
>
>
>
>
>
>
> > "Joshua Maurice" <joshuamaur...@gmail.com> wrote in message
> >> Ok. This is coming from a recent thread in comp.programming.threads,
> >> talking about C++0x. (You don't need to review it. I'll provide the
> >> relevant context here.)

>
> >> "questions about memory_order_seq_cst fence"

>
> >> Consider the following code.

> > [...]

>
> >> Q1. First, am I right in concluding that in the above code, all of the
> >> loads and stores might as well be memory_order_relaxed, right?

>
> > I think you are correct.

>
> >> Q2. Second, is the following end condition possible?
> >> *r1 == 0 && r2 == 1 && r3 == 0

>
> > FWIW, Relacy Race Detector says that the condition is indeed possible;
> > here is a test case:

>
> >http://pastebin.com/G4yDLyRy

>
> ARGHGHGHGHGH! I posted a version with a damn typo! I need to say that:
>
> Relacy Race Detector is NOT reporting that is condition is possible!
>
> Fixed code:
>
> http://pastebin.com/tE1TX1sx
>
> DAMN IT!!!!
>
> SORRY!

No problem.

When you say "Relacy Race Detector is NOT reporting that is condition
is possible!", that means that it reports that the end condition is
not possible, right? Perhaps semantic quibbling, but I want to be
sure.

However, we seem to have a problem then. Anthony else-thread has
stated that his notes seem to indicate that C++0x 29.3/7 does not
apply, and I assume - please correct me here if need be - that neither
of us knows of another rule that would disallow the following end
conditions:
r1 == 0 && r2 == 1 && r3 == 0

Thus, we have a problem. Anthony and my understanding, and Relacy Race
Detector, cannot be both right here. Either that end condition is
possible from an allowed execution according to the C++0x spec, or
it's not. I suppose alternatively that there's a bug or ambiguity in
the standard, and in which case we would need to identify that and fix
that defect in the standard.

 Joshua Maurice 06-16-2011 09:50 AM

On Jun 16, 1:42*am, Anthony Williams <anthony....@gmail.com> wrote:
> Joshua Maurice <joshuamaur...@gmail.com> writes:
> > Consider the following code.

>
> > /*** code 1 ***/
> > // Initially
> > atomic<int> x(0), y(0);

>
> > y.store(1, memory_order_release);

>
> > x.store(1, memory_order_release);

>
> > /***************/

>
> > Q1. First, am I right in concluding that in the above code, all of the
> > loads and stores might as well be memory_order_relaxed, right?

>
> Yes.
>
> > Q2. Second, is the following end condition possible?
> > * r1 == 0 && r2 == 1 && r3 == 0

>
> Yes.
>
> > Anthony Williams in the comp.programming.threads (who is apparently on
> > the concurrency working group), initially had a different
> > interpretation. I just reread it several times, and I'm not quite sure
> > what he's trying to say. He initially thought that you can use it
> > directly to prove that NOT (r1 == 0 && r2 == 1).

>
> But I now believe I'm mistaken. After checking my notes, we discussed
> requiring that seq_cst fences ordered loads as in this example, but
> decided against it. 29.3p7 is intended to apply only to writes.
>
> Anthony

What is the proper etiquette on here anyway, replying to all relevant
posts, or presuming that the other person will read all related sub-

So, in short, what do you think Anthony? Which is broken, Relacy Race
Detector and/or Chris's use of it, or are we missing some obscure rule
or combination of rules from C++0x?

Oh... this is why I hate English prose for what ought to be symbolic
logic definitions. Silly ISO.

 Joshua Maurice 06-16-2011 09:53 AM

On Jun 16, 2:50*am, Joshua Maurice <joshuamaur...@gmail.com> wrote:
> What is the proper etiquette on here anyway, replying to all relevant
> posts, or presuming that the other person will read all related sub-

Speaking of etiquette, I just got the distinct idea that cross posting
may have been a good plan, but for some reason I've gotten the
distinct idea from lurking here that cross posting is frowned upon.

 Anthony Williams 06-16-2011 10:45 AM

Joshua Maurice <joshuamaurice@gmail.com> writes:

> On Jun 16, 12:41Â*am, "Chris M. Thomasson" <cris...@charter.net> wrote:
>> "Chris M. Thomasson" <cris...@charter.net> wrote in messagenews:fgiKp.1272\$tp.587@newsfe06.iad...
>> Relacy Race Detector is NOT reporting that is condition is possible!
>>
>> Fixed code:
>>
>> http://pastebin.com/tE1TX1sx

> When you say "Relacy Race Detector is NOT reporting that is condition
> is possible!", that means that it reports that the end condition is
> not possible, right? Perhaps semantic quibbling, but I want to be
> sure.

When I ran Chris's code through relacy, the assert on r1==0 && r2==1 &&
r3 ==0 did not fire, even with the full search scheduler => this state
did not occur.

> However, we seem to have a problem then. Anthony else-thread has
> stated that his notes seem to indicate that C++0x 29.3/7 does not
> apply, and I assume - please correct me here if need be - that neither
> of us knows of another rule that would disallow the following end
> conditions:
> r1 == 0 && r2 == 1 && r3 == 0
>
> Thus, we have a problem. Anthony and my understanding, and Relacy Race
> Detector, cannot be both right here. Either that end condition is
> possible from an allowed execution according to the C++0x spec, or
> it's not. I suppose alternatively that there's a bug or ambiguity in
> the standard, and in which case we would need to identify that and fix
> that defect in the standard.

I think there is a bug in relacy.

Anthony
--
Author of C++ Concurrency in Action http://www.stdthread.co.uk/book/
Just Software Solutions Ltd http://www.justsoftwaresolutions.co.uk
15 Carrallack Mews, St Just, Cornwall, TR19 7UL, UK. Company No. 5478976

 Chris M. Thomasson 06-16-2011 09:32 PM

"Anthony Williams" <anthony.ajw@gmail.com> wrote in message
news:87y612dpgs.fsf@justsoftwaresolutions.co.uk...
[...]

> I think there is a bug in relacy.

Luckily, Relacy can, and should be fixed because it's such a wonderful tool!

I "love" that damn thing!

 All times are GMT. The time now is 09:52 AM.