Threading question - read-read coherency almost, sort of, withseq_cst fences

Discussion in 'C++' started by Joshua Maurice, Jun 16, 2011.

  1. 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.
    Joshua Maurice, Jun 16, 2011
    #1
    1. Advertising

  2. Re: Threading question - read-read coherency almost, sort of, with seq_cst fences

    "Joshua Maurice" <> wrote in message
    news:...
    > 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

    [...]
    Chris M. Thomasson, Jun 16, 2011
    #2
    1. Advertising

  3. Re: Threading question - read-read coherency almost, sort of, with seq_cst fences

    "Chris M. Thomasson" <> wrote in message
    news:fgiKp.1272$...
    > "Joshua Maurice" <> wrote in message
    > news:...
    >> 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
    Chris M. Thomasson, Jun 16, 2011
    #3
  4. Re: Threading question - read-read coherency almost, sort of, with seq_cst fences

    Joshua Maurice <> 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
    Anthony Williams, Jun 16, 2011
    #4
  5. On Jun 16, 12:41 am, "Chris M. Thomasson" <> wrote:
    > "Chris M. Thomasson" <> wrote in messagenews:fgiKp.1272$...
    >
    >
    >
    >
    >
    >
    >
    >
    >
    > > "Joshua Maurice" <> wrote in message
    > >news:....
    > >> 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.
    Joshua Maurice, Jun 16, 2011
    #5
  6. On Jun 16, 1:42 am, Anthony Williams <> wrote:
    > Joshua Maurice <> 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.
    Joshua Maurice, Jun 16, 2011
    #6
  7. On Jun 16, 2:50 am, Joshua Maurice <> 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.
    Joshua Maurice, Jun 16, 2011
    #7
  8. Re: Threading question - read-read coherency almost, sort of, with seq_cst fences

    Joshua Maurice <> writes:

    > On Jun 16, 12:41 am, "Chris M. Thomasson" <> wrote:
    >> "Chris M. Thomasson" <> wrote in messagenews:fgiKp.1272$...
    >> 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
    Anthony Williams, Jun 16, 2011
    #8
  9. Re: Threading question - read-read coherency almost, sort of, with seq_cst fences

    "Anthony Williams" <> wrote in message
    news:...
    [...]

    > 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!
    Chris M. Thomasson, Jun 16, 2011
    #9
    1. Advertising

Want to reply to this thread or ask your own question?

It takes just 2 minutes to sign up (and it's free!). Just click the sign up button to choose a username and then you can ask your own questions on the forum.
Similar Threads
  1. Roedy Green

    Fragile Fences

    Roedy Green, Jul 5, 2005, in forum: Java
    Replies:
    88
    Views:
    1,923
    Dale King
    Jul 22, 2005
  2. Replies:
    9
    Views:
    1,015
    Mark Space
    Dec 29, 2007
  3. c
    Replies:
    9
    Views:
    769
    Seebs
    Apr 26, 2010
  4. alcondor
    Replies:
    0
    Views:
    1,022
    alcondor
    Apr 26, 2010
  5. Navin
    Replies:
    1
    Views:
    674
    Ken Schaefer
    Sep 9, 2003
Loading...

Share This Page