Relacy 2.3 is missing a data race...

[Chris M. Thomasson]

I found an anomaly in which Relacy 2.3 fails to find the data race in
the following code using the `rl::fair_full_search_scheduler_type'
scheduler:

http://relacy.pastebin.com/f6999d103
(simple asymmetric synchronization example...)

The odd thing is that Relacy picks up the data race if I uncomment the
`DATA_RACE_YIELD' macro definition. This macro introduces a simple
`rl::yield()' in between the stores to the `g_flag' variable:
________________________________________________________
VAR(g_state1) = 1234;
g_flag.store(1, std::memory_order_relaxed);

# if defined (DATA_RACE_YIELD)
rl::yield(DATA_RACE_YIELD, $);
# endif

VAR(g_state2) = 4567;
g_flag.store(2, std::memory_order_relaxed);
________________________________________________________

It seems that the fair full search scheduler is not able to work the
threads into a position that will trigger the data race. If you
comment the `DATA_RACE' macro definition then the program is race free
and everything works. However, I wanted Relacy to be able to detect
the race condition I purposely added.

[Dmitriy Vyukov]

Hi Chris,

Thank you for reporting the bug.

I see where is the problem. The problem is that accesses to plain VAR
variables are NOT preemption points as opposed to accesses to atomic
variables.

Atomic var access pseudo-code is:
T atomic::foo(..)
{
call_scheduler(); // possible preemption point
foo_impl();
}

While plain var access is:
T var::foo(...)
{
check_for_races(); // purely local action
foo_impl();
}

So in your example first thread can be preempted only after it does
the store to g_state2 (more precisely: either does nothing, or does
both store to g_flag and g_state2). Consequently, when second thread
executes FlushProcessWriteBuffers(), he inevitably acquires visibility
over g_state2.

You may try to replace:
rl::yield(DATA_RACE_YIELD, $);
with just:
g_foo.store(0, std::memory_order_relaxed);
Atomic store to completely unrelated var will introduce preemption
point between stores to g_flag and g_state2, and thus race will be
detected.

The straightforward solution will be to introduce preemption points to
accesses to plain vars. However it will blow up search space
ineffably. So not an option.

I need to think more on this.

--
Dmitriy V'jukov

[Ronald Landheer-Cieslak]

On Feb 19, 5:45 am, Dmitriy Vyukov <dvyu...@gmail.com> wrote:
> On Feb 12, 10:03 pm, "Chris M. Thomasson" <cris...@charter.net> wrote:
> > I found an anomaly in which Relacy 2.3 fails to find the data race in
> > the following code using the `rl::fair_full_search_scheduler_type'
> > scheduler:

<snip>

> The straightforward solution will be to introduce preemption points to
> accesses to plain vars. However it will blow up search space
> ineffably. So not an option.

Though I understand that this solution will "blow up" the search
space, I don't see why it's not an option. Would it be possible to
implement it as a temporary solution, perhaps with a macro
(RL_VAR_PREEMPTABLE) to turn it off (e.g. if #define
RL_VAR_PREEMPTABLE 0) if need be?

I've started using Relacy to test my algorithms (great tool, by the
way!) and I would personally be much more worried about a false
negative than about a huge search space. If need be, I'll leave my
tests running for an extra month on my test machine ;)

Thanks for the great job you've done!

rlc