[Haskell-cafe] Can reallyUnsafePtrEquality give false positives?

Theodore Lief Gannon tanuki at gmail.com
Sat Nov 25 00:51:58 UTC 2017


Zemlya, I think you dropped this.

[1]
https://hackage.haskell.org/package/base-4.10.0.0/docs/System-Mem-StableName.html

On Thu, Nov 23, 2017 at 8:03 PM, Zemyla <zemyla at gmail.com> wrote:

> In that case, you probably want to use StableNames [1], which are
> unique and persistent even across GCs, and give you something you can
> use for a hash table.
>
> On Thu, Nov 23, 2017 at 6:48 AM, Michael Walker <mike at barrucadu.co.uk>
> wrote:
> > Thanks for the feedback, all.
> >
> > For some more context, I have a concurrency testing library[1], which
> > uses an algorithm called DPOR to reduce the space of possible
> > schedules it needs to explore.  There's an algorithm called MCR which
> > has the potential to reduce this space significantly further.  One of
> > the differences in MCR is taking into account reference equality of
> > values written to shared mutable variables.
> >
> > I can't just use Eq because (a) putMVar/etc doesn't have an Eq
> > constraint in the type, and (b) that would change strictness.  So I
> > looked to reallyUnsafePtrEquality# as a possible solution.  In this
> > setting, false negatives are fine.  If the algorithm thinks two equal
> > values are distinct, then it doesn't run as fast as it could
> > potentially do, but should still outperform DPOR due to its other
> > improvements.  But false positives are not fine, and lead to
> > unsoundness.
> >
> > An alternative is just using "\_ _ -> False", but if
> > reallyUnsafePtrEquality# will sometimes identify two equal things
> > without false positives, then it's effectively a free performance
> > boost in the cases where it happens to work.
> >
> >> - Extending the previous scenario, if purity is violated in the
> >>   evaluation of the initially shared thunk, then x and y may become
> >>   distinct values later on.
> >
> > Fortunately, I don't need to worry about impure actions leading to a
> > shared thunk evaluating to different things in different places, as
> > any nondeterminism beyond scheduler nondeterminism and relaxed memory
> > is already explicitly out of scope.
> >
> > [1] http://hackage.haskell.org/package/dejafu
> >
> > --
> > Michael Walker (http://www.barrucadu.co.uk)
> > _______________________________________________
> > Haskell-Cafe mailing list
> > To (un)subscribe, modify options or view archives go to:
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> > Only members subscribed via the mailman list are allowed to post.
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20171124/8a395833/attachment.html>


More information about the Haskell-Cafe mailing list