Relacy: read/read and read/write reordering

[Dmitriy Vyukov]

Hi,

I would like to thank you for sharing Relacy in the first place.

Now I have a question... I'm perhaps wrong, but it seems that Relacy
does not simulate reordering of read/read and read/write, which I
imagine that could lead to bugs being missed. Example follows. Sorry
for the noobish code, I don't have a lot of experience using Relacy
yet.

// read/write reordering
struct my_test : rl::test_suite<my_test, 2> {
std::atomic<int> x;
std::atomic<int> y;

void before() {
x($) = 0;
y($) = 0;
}

void thread(unsigned index) {
if(index == 0) {
if(x.load(std::memory_order_relaxed)) {
y.store(1, std::memory_order_relaxed);
}
}
else {
if(y.load(std::memory_order_relaxed)) {
x.store(1, std::memory_order_relaxed);
}
}
}

void after() {
std::cout << x << " " << y << std::endl;
// outcome x = y = 1 is possible
}
};

// read/read reordering
struct my_test2 : rl::test_suite<my_test2, 2> {
std::atomic<int> x;
int a;
int b;

void before() {
x($) = 0;
}

void thread(unsigned index) {
if(index == 0) {
x.store(1, std::memory_order_relaxed);
x.store(2, std::memory_order_relaxed);
}
else {
a = x.load(std::memory_order_relaxed);
b = x.load(std::memory_order_relaxed);
}
}

void after() {
std::cout << a << " " << b << std::endl;
// outcome a = 2 and b = 1 is possible
}
};

--
You received this message because you are subscribed to the Google Groups "Relacy Race Detector" group.
To post to this group, send email to rel...@googlegroups.com.
To unsubscribe from this group, send email to relacy+un...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/relacy?hl=en.

[Dmitriy Vyukov]

On May 20, 11:48 pm, Dmitriy Vyukov <dvyu...@gmail.com> wrote:
> Hi,
>
> I would like to thank you for sharing Relacy in the first place.

Thanks.

> Now I have a question... I'm perhaps wrong, but it seems that Relacy
> does not simulate reordering of read/read and read/write, which I
> imagine that could lead to bugs being missed. Example follows. Sorry
> for the noobish code, I don't have a lot of experience using Relacy
> yet.
>
> // read/write reordering
> struct my_test : rl::test_suite<my_test, 2> {
>   std::atomic<int> x;
>   std::atomic<int> y;
>
>   void before() {
>      x($) = 0;
>      y($) = 0;
>   }
>
>   void thread(unsigned index) {
>      if(index == 0) {
>         if(x.load(std::memory_order_relaxed)) {
>            y.store(1, std::memory_order_relaxed);
>         }
>      }
>      else {
>         if(y.load(std::memory_order_relaxed)) {
>            x.store(1, std::memory_order_relaxed);
>         }
>      }
>   }
>
>   void after() {
>      std::cout << x << " " << y << std::endl;
>      // outcome x = y = 1 is possible
>   }
>
> };

I believe (not completely sure, though) that outcome "x = y = 1" is
impossible because of the control dependencies.
May you show that the outcome is legal in C++0x?

--
Dmitriy V'jukov

[Dmitriy Vyukov]

On May 20, 11:48 pm, Dmitriy Vyukov <dvyu...@gmail.com> wrote:

>

> // read/read reordering
> struct my_test2 : rl::test_suite<my_test2, 2> {
>   std::atomic<int> x;
>   int a;
>   int b;
>
>   void before() {
>      x($) = 0;
>   }
>
>   void thread(unsigned index) {
>      if(index == 0) {
>         x.store(1, std::memory_order_relaxed);
>         x.store(2, std::memory_order_relaxed);
>      }
>      else {
>         a = x.load(std::memory_order_relaxed);
>         b = x.load(std::memory_order_relaxed);
>      }
>   }
>
>   void after() {
>      std::cout << a << " " << b << std::endl;
>      // outcome a = 2 and b = 1 is possible
>   }
>
> };

The outcome "a = 2 and b = 1" is illegal in C++0x.
x=1 happens before x=2, thus modification order of a is "1, 2".
Then, a=x happens before b=x, C++0x says that:
"Furthermore, if a value computation A of an atomic object M happens
before a value computation B of M, and the value computed by A
corresponds to the value stored by side effect X, then the value
computed by B shall either equal the value computed by A, or be the
value stored by side effect Y, where Y follows X in the modification
order of M. [ Note: This effectively disallows compiler reordering of
atomic operations to a single object, even if both operations are
“relaxed” loads..."

So if a=2, then b can't be equal to 1.

--
Dmitriy V'jukov

[Giovanni Funchal]

> The outcome "a = 2 and b = 1" is illegal in C++0x.

You are right. I now finally understand that there is a total order
for each address (what they call modification order). Hmmm...
"relaxed" ordering is not that relaxed after all. I imagine that this
will cause relaxed loads and stores to be quite complex to implement
in some architectures. In Sparc RMO for instance, I believe an atomic
load will have to be ld + membar #LoadLoad because reads to the same
address are not always performed in order. Similar for PowerPC and
ARM.

-- Giovanni

[Giovanni Funchal]

> I believe (not completely sure, though) that outcome "x = y = 1" is
> impossible because of the control dependencies.

Such outcome is not ruled out according to the latest C++0x draft, page 1112.

http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2010/n3092.pdf

> May you show that the outcome is legal in C++0x?

On each thread, the load and the store are relaxed and to unrelated
addresses, so reordering is allowed. Yes there is a "control
dependency", but this is not part of the definition of the ordering
guarantees. I believe that most hardware have stronger guarantees and
will not actually produce this outcome, though some might (and I
suspect ARM does).

-- Giovanni

[Dmitriy Vyukov]

On May 24, 6:36 pm, Giovanni Funchal <gafunc...@gmail.com> wrote:
> > The outcome "a = 2 and b = 1" is illegal in C++0x.
>
> You are right. I now finally understand that there is a total order
> for each address (what they call modification order). Hmmm...
> "relaxed" ordering is not that relaxed after all. I imagine that this
> will cause relaxed loads and stores to be quite complex to implement
> in some architectures. In Sparc RMO for instance, I believe an atomic
> load will have to be ld + membar #LoadLoad because reads to the same
> address are not always performed in order. Similar for PowerPC and
> ARM.

Relaxed load on POWER is plain ld:
http://www.rdrop.com/users/paulmck/scalability/paper/N2745r.2009.02.22a.html
I believe the same for SPARC RMO.

--
Dmitriy V'jukov

[Dmitriy Vyukov]

On May 24, 5:47 pm, Giovanni Funchal <gafunc...@gmail.com> wrote:
> > I believe (not completely sure, though) that outcome "x = y = 1" is
> > impossible because of the control dependencies.
>
> Such outcome is not ruled out according to the latest C++0x draft, page 1112.
>
> http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2010/n3092.pdf
>
> > May you show that the outcome is legal in C++0x?
>
> On each thread, the load and the store are relaxed and to unrelated
> addresses, so reordering is allowed. Yes there is a "control
> dependency", but this is not part of the definition of the ordering
> guarantees. I believe that most hardware have stronger guarantees and
> will not actually produce this outcome, though some might (and I
> suspect ARM does).

Yes, I see, the result is allowed, however the standard says that
"implementations should not allow such behavior":

29.3/10
[ Note: The requirements do allow r1 == r2 == 42 in the following
example, with x and y initially zero:
// Thread 1:
r1 = x.load(memory_order_relaxed);
if (r1 == 42) y.store(r1, memory_order_relaxed);
// Thread 2:
r2 = y.load(memory_order_relaxed);
if (r2 == 42) x.store(42, memory_order_relaxed);
However, implementations should not allow such behavior.—end note ]


Unfortunately Relacy is unable to model such reordering. The problem
is deeply in the work principle: Relacy does not have any information
about a program structure, it only observes sequences of loads/stores
(and other sync operations) from each thread.

--
Dmitriy V'jukov