Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.c++ > #6777 > unrolled thread

Threading question - read-read coherency almost, sort of, with seq_cst fences

Back to article view | Back to comp.lang.c++

Contents

  Threading question - read-read coherency almost, sort of, with seq_cst fences Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-15 16:56 -0700
    Re: Threading question - read-read coherency almost, sort of, with seq_cst fences "Chris M. Thomasson" <cristom@charter.net> - 2011-06-16 00:28 -0700
      Re: Threading question - read-read coherency almost, sort of, with seq_cst fences "Chris M. Thomasson" <cristom@charter.net> - 2011-06-16 00:41 -0700
        Re: Threading question - read-read coherency almost, sort of, with seq_cst fences Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-16 02:47 -0700
          Re: Threading question - read-read coherency almost, sort of, with seq_cst fences Anthony Williams <anthony.ajw@gmail.com> - 2011-06-16 11:45 +0100
            Re: Threading question - read-read coherency almost, sort of, with seq_cst fences "Chris M. Thomasson" <cristom@charter.net> - 2011-06-16 14:32 -0700
    Re: Threading question - read-read coherency almost, sort of, with seq_cst fences Anthony Williams <anthony.ajw@gmail.com> - 2011-06-16 09:42 +0100
      Re: Threading question - read-read coherency almost, sort of, with seq_cst fences Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-16 02:50 -0700
        Re: Threading question - read-read coherency almost, sort of, with seq_cst fences Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-16 02:53 -0700

#6777 — Threading question - read-read coherency almost, sort of, with seq_cst fences

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"
http://groups.google.com/group/comp.programming.threads/browse_thread/thread/0158f1f2bca1019e#

Consider the following code.

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

// Thread 1:
y.store(1, memory_order_release);
atomic_thread_fence(memory_order_seq_cst); //fence 1
r1 = x.load(memory_order_acquire);

// Thread 2:
x.store(1, memory_order_release);

// Thread 3:
r2 = x.load(memory_order_acquire);
atomic_thread_fence(memory_order_seq_cst); //fence 3
r3 = y.load(memory_order_acquire);
/***************/

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

[toc] | [next] | [standalone]

#6778

"Joshua Maurice" <joshuamaurice@gmail.com> wrote in message 
news:c4891256-0c18-4eab-a227-ba819263d133@v11g2000prk.googlegroups.com...
> 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"
> http://groups.google.com/group/comp.programming.threads/browse_thread/thread/0158f1f2bca1019e#
>
> 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

[...] 

[toc] | [prev] | [next] | [standalone]

#6779

"Chris M. Thomasson" <cristom@charter.net> wrote in message 
news:fgiKp.1272$tp.587@newsfe06.iad...
> "Joshua Maurice" <joshuamaurice@gmail.com> wrote in message 
> news:c4891256-0c18-4eab-a227-ba819263d133@v11g2000prk.googlegroups.com...
>> 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"
>> http://groups.google.com/group/comp.programming.threads/browse_thread/thread/0158f1f2bca1019e#
>>
>> 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 

[toc] | [prev] | [next] | [standalone]

#6789

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
> >news:c4891256-0c18-4eab-a227-ba819263d133@v11g2000prk.googlegroups.com...
> >> 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"
> >>http://groups.google.com/group/comp.programming.threads/browse_thread...
>
> >> 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.

[toc] | [prev] | [next] | [standalone]

#6795

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::thread C++0x thread library             http://www.stdthread.co.uk
Just Software Solutions Ltd       http://www.justsoftwaresolutions.co.uk
15 Carrallack Mews, St Just, Cornwall, TR19 7UL, UK. Company No. 5478976

[toc] | [prev] | [next] | [standalone]

#6824

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

[toc] | [prev] | [next] | [standalone]

#6782

Joshua Maurice <joshuamaurice@gmail.com> writes:

> Consider the following code.
>
> /*** code 1 ***/
> // Initially
> atomic<int> x(0), y(0);
>
> // Thread 1:
> y.store(1, memory_order_release);
> atomic_thread_fence(memory_order_seq_cst); //fence 1
> r1 = x.load(memory_order_acquire);
>
> // Thread 2:
> x.store(1, memory_order_release);
>
> // Thread 3:
> r2 = x.load(memory_order_acquire);
> atomic_thread_fence(memory_order_seq_cst); //fence 3
> r3 = y.load(memory_order_acquire);
> /***************/
>
> 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::thread C++0x thread library             http://www.stdthread.co.uk
Just Software Solutions Ltd       http://www.justsoftwaresolutions.co.uk
15 Carrallack Mews, St Just, Cornwall, TR19 7UL, UK. Company No. 5478976

[toc] | [prev] | [next] | [standalone]

#6790

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);
>
> > // Thread 1:
> > y.store(1, memory_order_release);
> > atomic_thread_fence(memory_order_seq_cst); //fence 1
> > r1 = x.load(memory_order_acquire);
>
> > // Thread 2:
> > x.store(1, memory_order_release);
>
> > // Thread 3:
> > r2 = x.load(memory_order_acquire);
> > atomic_thread_fence(memory_order_seq_cst); //fence 3
> > r3 = y.load(memory_order_acquire);
> > /***************/
>
> > 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-
threads?

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.

[toc] | [prev] | [next] | [standalone]

#6791

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

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.

[toc] | [prev] | [standalone]

Back to top | Article view | comp.lang.c++

csiph-web