Relacy 2.3 is missing a data race...

[Dmitriy Vyukov]

On Feb 21, 6:59 am, Ronald Landheer-Cieslak <blytkerc...@gmail.com>
wrote:
> 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 ;)

Hi Ronald,

I just hope I will find another way to solve the issue (actually I
found it, but already forget it).
Since we are talking about NP-hard problem, it's actually a matter of
an extra... maybe zillion of years or so :) I agree that false
negatives are really unpleasant here, but I can't just ignore state
space size, it's one of the fundamentals problems for verificators.
Since NP-hard problems are practically unsolvable, there is always a
possibility that Relacy will miss a defect. Plus there is a not less
serious source of false negatives - unit test, it's a users
responsibility to build a test on which a defect is observable.
A lot of things in Relacy are about sensible compromise between
verification soundness and verification time.

> Thanks for the great job you've done!

Thanks.

--
Dmitriy V'jukov

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