Re: [powerpc64le] seq_cst memory order possibly not honored

[Jonathan Wakely <jwakely dot gcc at gmail dot com>]

On 14 August 2015 at 10:54, Andrey Semashev <andrey.semashev@gmail.com> wrote:
> On 14.08.2015 11:51, Jonathan Wakely wrote:
>>
>> On 14 August 2015 at 01:37, Andrey Semashev wrote:
>>>
>>> 1. Is my test valid or is there a flaw that I'm missing?
>>
>>
>> The cppmem tool at http://svr-pes20-cppmem.cl.cam.ac.uk/cppmem/ shows
>> that there are consistent executions where (x==0 && y==0) is true. I
>> used this code:
>>
>> int main() {
>>    atomic_int a = 0;
>>    atomic_int b = 0;
>>    int x, y;
>>    {{{
>>      {
>>        a.store(1,mo_seq_cst);
>>        a.load(mo_relaxed);
>>        x = b.load(mo_relaxed);
>>      }
>>    |||
>>      {
>>        b.store(1, mo_seq_cst);
>>        b.load(mo_relaxed);
>>        y = a.load(mo_relaxed);
>>      }
>>    }}}
>>    return 0;
>> }
>
>
> I'm not familiar with that tool and not sure how to interpret its output,

Then you should study it :-)

> but I think it misses one point that is present in the original test and I
> failed to mention. The Boost.Atomic test uses Boost.Thread barriers to
> ensure that both threads have executed the store-load-load region before
> checking for x and y.


You can add

  int xx = x;
  int yy = y;

just before the return from main(), which executes after joining both
threads doing the store-load-load. You will still see that xx==0 &&
yy==0 is possible.

> Otherwise I cannot see how (x==0 && y==0) could happen. The last load in
> each thread is sequenced after the first seq_cst store and both stores are
> ordered with respect to each other, so one of the threads should produce 1.

The tool evaluates the possible executions according to a formal model
of the C++ memory model, so is invaluable for answering questions like
this.

It shows that there is no sychronizes-with (shown as "sw")
relationship between the seq_cst store and the relaxed load for each
atomic object. There is a total order of sequentially consistent
operations, but the loads are not sequentially consistent and do not
synchronize with the stores.