Opened 3 years ago

Closed 3 years ago

#13027 closed bug (fixed)

The let/app invariant, evaluated-ness, and reallyUnsafePtrEquality#

Reported by: erikd Owned by: dfeuer
Priority: normal Milestone: 8.2.1
Component: Compiler Version: 8.1
Keywords: Cc: dfeuer, simonmar
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Building GHC failed Test Case: simplCore/should_compile/T13027
Blocked By: Blocking:
Related Tickets: #11444 Differential Rev(s):
Wiki Page:

Description

Git HEAD of containers compiles fine with ghc-8.0.1, but when compiling with GHC git HEAD gives core lint errors:

*** Core Lint errors : in result of Float out(FOS {Lam = Just 0,
                                                   Consts = True,
                                                   OverSatApps = False}) ***
<no location info>: warning:
    In the expression: tagToEnum#
                         @ Bool (reallyUnsafePtrEquality# @ (Set a) l'_a4Fk l_a4Fi)
    This argument does not satisfy the let/app invariant:
      reallyUnsafePtrEquality# @ (Set a) l'_a4Fk l_a4Fi
*** Offending Program ***
Rec {
$dTypeable_s9vn :: Proxy# Set -> TypeRep

This issue can be reproduced using:

(cd libraries/containers ; git checkout master ; git pull)
perl boot && ./configure && make clean && make -j

Change History (38)

comment:1 Changed 3 years ago by RyanGlScott

Cc: dfeuer added

I'm not entirely sure if this is a GHC bug. For one thing, you don't need GHC HEAD to reproduce this - you could just as well use GHC 8.0.1. Here is a minimized test case (taken from the source code of containers HEAD):

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE MagicHash #-}
module Containers (insert) where

import GHC.Exts (isTrue#, reallyUnsafePtrEquality#)

data Set a = Bin {-# UNPACK #-} !Size !a !(Set a) !(Set a)
           | Tip

type Size = Int

insert :: Ord a => a -> Set a -> Set a
insert = go
  where
    go :: Ord a => a -> Set a -> Set a
    go !x Tip = Bin 1 x Tip Tip
    go !x t@(Bin sz y l r) = case compare x y of
        LT | l' `ptrEq` l -> t
           | otherwise -> undefined -- balanceL y l' r
           where !l' = go x l
        GT | r' `ptrEq` r -> t
           | otherwise -> undefined -- balanceR y l r'
           where !r' = go x r
        EQ | x `ptrEq` y -> t
           | otherwise -> Bin sz x l r
{-# INLINABLE insert #-}

ptrEq :: a -> a -> Bool
ptrEq x y = isTrue# (reallyUnsafePtrEquality# x y)
{-# INLINE ptrEq #-}

If you compile this with /opt/ghc/8.0.1/bin/ghc Containers.hs -dcore-lint -O2, you'll get a very similar Core Lint error.

The culprit seems to be the suspicious use of reallyUnsafePtrEquality# in ptrEq. Any thoughts on this, David?

comment:2 Changed 3 years ago by dfeuer

Based on my extremely naive reading of the let/app invariant note, I'm *guessing* that the simplifier may be doing something weird like

ptrEq x y = let r = reallyUnsafePtrEquality# x y
            in isTrue# r

when it really should be doing

ptrEq x y = case reallyUnsafePtrEquality# x y of
              r -> isTrue# r

comment:3 Changed 3 years ago by RyanGlScott

A workaround is to define your own isTrue# function:

isTrue# :: Int# -> Bool
isTrue# 1# = True
isTrue# _  = False
{-# INLINE isTrue# #-}

comment:4 Changed 3 years ago by rwbarton

It also gives a core lint error as early as 7.10.1.

I found that early on the simplifier produces

    case x_a3Iw of x_X3IE { __DEFAULT ->
    ...
            case GHC.Prim.tagToEnum#
                   @ Bool (reallyUnsafePtrEquality# @ a x_X3IE y_a3IA)
            of {
            ...
            }
    }

This is apparently okay: the application of tagToEnum# to the reallyUnsafePtrEquality# call is okay because reallyUnsafePtrEquality# is safe for speculation and the arguments x_X3IE and y_a3IA are known to be evaluated (x_X3IE came from evaluating the scrutinee of a case and y_a3IA came from the strict field of Bin).

However the FloatOut pass does a "binder swap" (https://github.com/ghc/ghc/blob/master/compiler/simplCore/SetLevels.hs#L37) where it turns the reference to x_X3IE into a reference to x_a3Iw. Now x_a3Iw is not known to be evaluated so reallyUnsafePtrEquality# is no longer considered to be safe for speculation. (Even though reallyUnsafePtrEquality# doesn't actually evaluate its arguments.)

comment:5 Changed 3 years ago by rwbarton

It doesn't fail before 7.10.1 because earlier versions didn't check the let/app invariant in core lint.

comment:6 Changed 3 years ago by dfeuer

I want to be able to test for equal thunks too. Is there something I can do to make this just work? Should I work around it by using case instead of isTrue#?

comment:7 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 75e8c305/ghc:

Propagate evaluated-ness a bit more faithfully

This was provoked by Trac #13027.

The fix in Simplify actually cures the reported bug; see
Note [Case binder evaluated-ness] in Simplify.

The fix in CoreTidy looks like an omission that I fixed while I
was at it.

comment:8 Changed 3 years ago by simonpj

Test Case: simplCore/should_compile/T13027

Probably not worth merging to 8.0... I think it's only a Lint complaint and it's fine without.

Thanks for reporting this!

comment:9 in reply to:  7 Changed 3 years ago by dfeuer

Replying to Simon Peyton Jones <simonpj@…>:

In 75e8c305/ghc:

Propagate evaluated-ness a bit more faithfully

This was provoked by Trac #13027.

The fix in Simplify actually cures the reported bug; see
Note [Case binder evaluated-ness] in Simplify.

The fix in CoreTidy looks like an omission that I fixed while I
was at it.

If this is about tracking that the arguments to reallyUnsafePtrEquality# have been evaluated, then I fear it may not fix the problem in all contexts. The equality test should be seen as safe to speculate even when its arguments have not been evaluated.

comment:10 Changed 3 years ago by dfeuer

That is, if the bang pattern on x is removed, I fear we'll still have an error, although the code is reasonable.

comment:11 Changed 3 years ago by simonpj

Its not about that. Lint is just blindly checking the let/app invariant.

We might additionally want to check that the arguments to reallyUnsafePtrEquality# are indeed guaranteed evaluated... Lint could do that I suppose but it might well be a USER error not a GHC error. We don't have a good way to check for that; hence really unsafe.

But I have fixed GHC's internal consistency check, which is what Lint is about

comment:12 in reply to:  11 Changed 3 years ago by dfeuer

Replying to simonpj:

We might additionally want to check that the arguments to reallyUnsafePtrEquality# are indeed guaranteed evaluated... Lint could do that I suppose but it might well be a USER error not a GHC error. We don't have a good way to check for that; hence really unsafe.

Why would we want to check that? One nice thing about the equality test us that it can be applied to things not known to be evaluated, and sometimes even catch equality between thunks.

comment:13 Changed 3 years ago by simonpj

Resolution: fixed
Status: newclosed

I agree. Fine, so we can close this ticket.

comment:14 Changed 3 years ago by erikd

I tried building with 75e8c305/ghc and it still fails. Does that meant this needs to be fixed in containers?

comment:15 Changed 3 years ago by simonpj

That's odd. I didn't test with containers, only with the test in comment:1. In pinrciple I can try to look, but not over Christmas. Anything anyone can do to narrow it down to a repro case would be very helpful.

Does that meant this needs to be fixed in containers?

No: Lint errors are alwyas GHC bugs.

comment:16 Changed 3 years ago by simonpj

Resolution: fixed
Status: closednew

Erik says not fixed

comment:17 Changed 3 years ago by RyanGlScott

Here's the offending part of containers this time:

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE MagicHash #-}
module Containers (partition) where

import GHC.Exts (isTrue#, reallyUnsafePtrEquality#)

data Set a = Bin {-# UNPACK #-} !Size !a !(Set a) !(Set a)
           | Tip

type Size = Int

data StrictPair a b = !a :*: !b

infixr 1 :*:

-- | Convert a strict pair to a standard pair.
toPair :: StrictPair a b -> (a, b)
toPair (x :*: y) = (x, y)
{-# INLINE toPair #-}

partition :: (a -> Bool) -> Set a -> (Set a,Set a)
partition p0 t0 = toPair $ go p0 t0
  where
    go _ Tip = (Tip :*: Tip)
    go p t@(Bin _ x l r) = case (go p l, go p r) of
      ((l1 :*: l2), (r1 :*: r2))
        | p x       -> (if l1 `ptrEq` l && r1 `ptrEq` r
                        then t
                        else link x l1 r1) :*: merge l2 r2
        | otherwise -> merge l1 r1 :*:
                       (if l2 `ptrEq` l && r2 `ptrEq` r
                        then t
                        else link x l2 r2)

merge :: Set a -> Set a -> Set a
merge = undefined

link :: a -> Set a -> Set a -> Set a
link  = undefined

ptrEq :: a -> a -> Bool
ptrEq x y = isTrue# (reallyUnsafePtrEquality# x y)
{-# INLINE ptrEq #-}

And here's the Core Lint error:

$ ghc/inplace/bin/ghc-stage2 Containers2.hs -fforce-recomp -dcore-lint -O2
[1 of 1] Compiling Containers       ( Containers2.hs, Containers2.o )
*** Core Lint errors : in result of Simplifier ***
<no location info>: warning:
    In the expression: tagToEnum#
                         @ Bool (reallyUnsafePtrEquality# @ (Set a) ww_s4m3 l_a2PV)
    This argument does not satisfy the let/app invariant:
      reallyUnsafePtrEquality# @ (Set a) ww_s4m3 l_a2PV
*** Offending Program ***
merge :: forall a. Set a -> Set a -> Set a
[LclId,
 Str=x,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
         WorkFree=False, Expandable=False, Guidance=NEVER}]
merge =
  \ (@ a_a3Sm) ->
    raise#
      @ SomeException
      @ 'PtrRepLifted
      @ (Set a -> Set a -> Set a)
      (noinline
         @ ([Char] -> CallStack -> SomeException)
         errorCallWithCallStackException
         undefined9
         (PushCallStack
            undefined8
            undefined1
            (PushCallStack
               (unpackCString# "undefined"#)
               (SrcLoc
                  (unpackCString# "main"#)
                  (unpackCString# "Containers"#)
                  (unpackCString# "Containers2.hs"#)
                  (I# 36#)
                  (I# 9#)
                  (I# 36#)
                  (I# 18#))
               EmptyCallStack)))

link :: forall a. a -> Set a -> Set a -> Set a
[LclId,
 Str=x,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
         WorkFree=False, Expandable=False, Guidance=NEVER}]
link =
  \ (@ a_a3S7) ->
    raise#
      @ SomeException
      @ 'PtrRepLifted
      @ (a -> Set a -> Set a -> Set a)
      (noinline
         @ ([Char] -> CallStack -> SomeException)
         errorCallWithCallStackException
         undefined9
         (PushCallStack
            undefined8
            undefined1
            (PushCallStack
               (unpackCString# "undefined"#)
               (SrcLoc
                  (unpackCString# "main"#)
                  (unpackCString# "Containers"#)
                  (unpackCString# "Containers2.hs"#)
                  (I# 39#)
                  (I# 9#)
                  (I# 39#)
                  (I# 18#))
               EmptyCallStack)))

lvl_s4aT :: forall a. StrictPair (Set a) (Set a)
[LclId,
 Str=m,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 30}]
lvl_s4aT =
  \ (@ a_a3Sv) -> :*: @ (Set a) @ (Set a) (Tip @ a) (Tip @ a)

Rec {
poly_go_s4aS [InlPrag=INLINE[0]]
  :: forall a. (a -> Bool) -> Set a -> StrictPair (Set a) (Set a)
[LclId,
 Arity=2,
 CallArity=2,
 Str=<L,C(U)><S,U>m,
 Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=2,unsat_ok=True,boring_ok=False)
         Tmpl= \ (@ a_s4lW)
                 (w_s4lX [Occ=Once] :: a -> Bool)
                 (w_s4lY [Occ=Once] :: Set a) ->
                 case $wpoly_go_s4m1 @ a w_s4lX w_s4lY of
                 { (# ww_s4m3 [Occ=Once], ww_s4m4 [Occ=Once] #) ->
                 :*: @ (Set a) @ (Set a) ww_s4m3 ww_s4m4
                 }}]
poly_go_s4aS =
  \ (@ a_s4lW) (w_s4lX :: a -> Bool) (w_s4lY :: Set a) ->
    case $wpoly_go_s4m1 @ a w_s4lX w_s4lY of
    { (# ww_s4m3, ww_s4m4 #) ->
    :*: @ (Set a) @ (Set a) ww_s4m3 ww_s4m4
    }

$wpoly_go_s4m1 [InlPrag=[0], Occ=LoopBreaker]
  :: forall a. (a -> Bool) -> Set a -> (# Set a, Set a #)
[LclId,
 Arity=2,
 Str=<L,C(U)><S,1*U>,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [60 30] 194 30}]
$wpoly_go_s4m1 =
  \ (@ a_s4lW) (w_s4lX :: a -> Bool) (w_s4lY :: Set a) ->
    case w_s4lY of wild_Xo {
      Bin dt_d44n [Dmd=<B,U>] x_a2PU [Dmd=<B,U>] l_a2PV [Dmd=<B,U>]
          r_a2PW [Dmd=<B,U>] ->
        case $wpoly_go_s4m1 @ a w_s4lX l_a2PV of
        { (# ww_s4m3, ww_s4m4 #) ->
        case $wpoly_go_s4m1 @ a w_s4lX r_a2PW of
        { (# ww_X4mP, ww_X4mR #) ->
        case w_s4lX x_a2PU of {
          False -> case merge of wild_00 { };
          True ->
            case case tagToEnum#
                        @ Bool (reallyUnsafePtrEquality# @ (Set a) ww_s4m3 l_a2PV)
                 of {
                   False -> case link of wild_00 { };
                   True ->
                     case tagToEnum#
                            @ Bool (reallyUnsafePtrEquality# @ (Set a) ww_X4mP r_a2PW)
                     of {
                       False -> case link of wild_00 { };
                       True -> wild_Xo
                     }
                 }
            of dt_X3KG [Dmd=<B,U>]
            { __DEFAULT ->
            case merge of wild_00 { }
            }
        }
        }
        };
      Tip -> (# Tip @ a, Tip @ a #)
    }
end Rec }

partition :: forall a. (a -> Bool) -> Set a -> (Set a, Set a)
[LclIdX,
 Arity=2,
 Str=<L,C(U)><S,1*U>m,
 Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=2,unsat_ok=True,boring_ok=False)
         Tmpl= \ (@ a_a3Sv)
                 (p0_a2PP [Occ=Once] :: a -> Bool)
                 (t0_a2PQ [Occ=Once] :: Set a) ->
                 case poly_go_s4aS @ a p0_a2PP t0_a2PQ of
                 { :*: x_a2PN [Occ=Once] y_a2PO [Occ=Once] ->
                 (x_a2PN, y_a2PO)
                 }}]
partition =
  \ (@ a_a3Sv) (p0_a2PP :: a -> Bool) (t0_a2PQ :: Set a) ->
    case $wpoly_go_s4m1 @ a p0_a2PP t0_a2PQ of
    { (# ww_s4m3, ww_s4m4 #) ->
    (ww_s4m3, ww_s4m4)
    }

$trModule_s4a3 :: TrName
[LclId,
 Str=m1,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 30 20}]
$trModule_s4a3 = TrNameS "main"#

$trModule_s4a4 :: TrName
[LclId,
 Str=m1,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 50 20}]
$trModule_s4a4 = TrNameS "Containers"#

$trModule :: Module
[LclIdX,
 Str=m,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 30}]
$trModule = Module $trModule_s4a3 $trModule_s4a4

$tc'Tip_s4a5 :: TrName
[LclId,
 Str=m1,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 30 20}]
$tc'Tip_s4a5 = TrNameS "'Tip"#

$tc'Tip :: TyCon
[LclIdX,
 Str=m,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 50}]
$tc'Tip =
  TyCon
    2793269457193232401## 14910929446856376197## $trModule $tc'Tip_s4a5

$tc'Bin_s4a6 :: TrName
[LclId,
 Str=m1,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 30 20}]
$tc'Bin_s4a6 = TrNameS "'Bin"#

$tc'Bin :: TyCon
[LclIdX,
 Str=m,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 50}]
$tc'Bin =
  TyCon
    4548370254528349800## 3424913680517968384## $trModule $tc'Bin_s4a6

$tcSet_s4a7 :: TrName
[LclId,
 Str=m1,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 30 20}]
$tcSet_s4a7 = TrNameS "Set"#

$tcSet :: TyCon
[LclIdX,
 Str=m,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 50}]
$tcSet =
  TyCon
    3037255313641890014## 1627524838438604808## $trModule $tcSet_s4a7

$tc':*:_s4a8 :: TrName
[LclId,
 Str=m1,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 30 20}]
$tc':*:_s4a8 = TrNameS "':*:"#

$tc':*: :: TyCon
[LclIdX,
 Str=m,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 50}]
$tc':*: =
  TyCon
    9247104382896135333## 1281726570460431133## $trModule $tc':*:_s4a8

$tcStrictPair_s4a9 :: TrName
[LclId,
 Str=m1,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 50 20}]
$tcStrictPair_s4a9 = TrNameS "StrictPair"#

$tcStrictPair :: TyCon
[LclIdX,
 Str=m,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 50}]
$tcStrictPair =
  TyCon
    18371072474651713953##
    8175359178144728928##
    $trModule
    $tcStrictPair_s4a9

*** End of Offense ***


<no location info>: error: 
Compilation had errors

comment:18 Changed 3 years ago by dfeuer

I suspect it will be helpful to enhance let/app error reporting to make it explain why it believes the let/app invariant is being violated. I can start looking into doing so today, unless Simon disagrees. One vague possibility is that evaluatedness tracking breaks down when the pairs are unboxed, but I still don't see why evaluatedness should have anything to do with let/app in this context.

comment:19 Changed 3 years ago by rwbarton

Evaluatedness matters because the let/app invariant says that an argument of an application of unlifted type should be ok for speculation. And an application of a primop foo# bar baz is only considered ok for speculation if bar and baz are known to be evaluated, since otherwise evaluating foo# bar baz might evaluate bar and baz which could diverge. Actually reallyUnsafePtrEquality# never evaluates its arguments but the ok for speculation check does not know that; and if it did then the real underlying issue would still not be solved.

I'm guessing that the expression tagToEnum# @ Bool (reallyUnsafePtrEquality# @ (Set a) ww_s4m3 l_a2PV) was produced at an earlier stage when the first argument was known to be evaluated. Looks like it might have been before worker/wrapper, since go produces a StrictPair whose fields are known to be evaluated. But (# , #) can hold unevaluated things so w/w causes us to lose the information that ww_s4m3 is evaluated.

comment:20 Changed 3 years ago by simonpj

Thank you! Sigh.

Several things.

First (1). Consider

data T a = MkT !a a

f :: Int -> T Int
f x = MkT (x+1) x

We'll generate a wrapper for MkT, called $WMkT, that does the evaluation. So the Core looks like this:

$WMkT :: a -> T a
$WMkT = /\a. \x:a y:a. case x of z { DEFAULT -> MkT y z }

f = \x. $WMkT (x+1) x

After inlining the wrapper we get

f x = case x+1 of y -> MkT y x

Here in Core the MkT is the "worker" constructor. It does not perform evaluation (that is done by the wrapper); it is purely passive.

But when we pattern match against a MkT we know that the payload is already evaluated. So if we started with

g (MkT x y) = MkT x (y+1)

we would initially get

g = \v. case v of
          MkT x y -> case x of r { DEFAULT ->
                       MkT r (y+1)

But since x is surely evaluated (since it is gotten from MkT) we can drop the case x to get

g = \v. case v of
          MkT x y -> MkT r (y+1)

So far so good.

But if GHC went wrong, we could construct the expression

MkT (x+1) y

in which the first argument is not evaluated. That is not supposed to happen! And arguably Lint should, thereore, check that the argument of a strict data constructor (the constructor not the wrapper!) is definitely evaluated. But Lint doesn't check that check. Yet.

Second (2). The same applies to the argument to dataToTag#. The argument should be evaluated, and Lint should really check that it is. I don't know if there are any other primops with this property. I think probably not.

Third (3). Should the arguments to reallyUnsafePtrEq' be evaluated? Probably not. Maybe it's ok to compare unevaluated thunks. But then in fact reallyUnsafePtrEq# is ok-for-speculation evan if its args are not evaluated. But exprOkForSpeculation doesn't understand that.

Fourth (4). The Lint error in comment:17 is to do with propagation of evaluated-ness. Consider this Core

f = \x. case x of y { DEFAULT -> MkT y y }

This is fine. But now CPR analyis spots that f has the CPR property and does a worker/wrapper split (it would need to have a bigger body for this to actually happen, but you get the idea):

$wf = \x -> case x of y { DEFAULT -> (# y, y #) }
f = \x. case $wf x of (# a, b #) -> MkT a b  -- Wrapper

Now this is NOT fine. Look at that application of MkT in the wrapper for f: we know that a will be evaluated (because it's a result of $wf) but that is not immediately apparent. We need to mark a as evaluated somehow.

We have a way to do that: just grep for `setIdUnfolding` evaldUnfolding in the compiler. But we aren't doing that right now.

Now, Lint doesn't complain about f's wrapper because of (1) above (although I argue that it should). But it does complain in this example program, when exprOkForSpeculation fails.

comment:21 Changed 3 years ago by simonpj

Conclusions

  • ToDo: augument Lint to check that args to strict data cons are evaluated. Ditto dataToTag#.
  • ToDo: (maybe) make exprOkForSpeculation more lenient for lazy primpops.
  • ToDo: make worker/wrapper produce eval'd flags on the wrapper for CPR. Will silence the Lint error in comment:17

There is no actual bug here, if you have Lint off. The problem is that Lint is reporting a non-error.

comment:22 Changed 3 years ago by dfeuer

Is there a reason not to make exprOkForSpeculation more lenient for reallyUnsafePtrEquality#? Having it otherwise seems inconsistent, but it's also possible that it doesn't enable useful floating or that it's too much trouble to make it happen. I dug around just a bit, and the only other lazy primitives I could find that might be safe for speculation were unpackClosure# and (under certain circumstances, maybe) seq.

I'm somewhat concerned about the fact that the problem tracking evaluatedness was only revealed "by chance", because exprOkForSpeculation is (seemingly) too conservative about reallyUnsafePtrEquality#. Is there some way to make this tracking more robust? I understand that you and Max Bolingbroke worked on some possibly-related ideas in "Types are Calling Conventions". What's your intuition about whether the type system can help here without making life horrible?

comment:23 Changed 3 years ago by simonpj

Is there some way to make this tracking more robust?

Yes: (1) and (2) are precisely about ensuring that when something is supposed to be evaluated, it really is.

Is there a reason not to make exprOkForSpeculation more lenient for reallyUnsafePtrEquality#

No, no big reason. We could consult the primops strictness info; or we could have a special case in CoreUtils.app_ok.


HOWEVER, in answering this question I also came across this (in CoreUtils):

Note [dataToTag speculation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Is this OK?
   f x = let v::Int# = dataToTag# x
         in ...
We say "yes", even though 'x' may not be evaluated.  Reasons

  * dataToTag#'s strictness means that its argument often will be
    evaluated, but FloatOut makes that temporarily untrue
         case x of y -> let v = dataToTag# y in ...
    -->
         case x of y -> let v = dataToTag# x in ...
    Note that we look at 'x' instead of 'y' (this is to improve
    floating in FloatOut).  So Lint complains.

    Moreover, it really *might* improve floating to let the
    v-binding float out

  * CorePrep makes sure dataToTag#'s argument is evaluated, just
    before code gen.  Until then, it's not guaranteed

The plot thickens. When I wrote this I clearly intended that (contrary to (2)) Core would not guarantee that the argument to dataToTag# is evaluated. Instead, we arrange that it is evaluated to being with; accept that may not be true forever; but re-establish it in CorePrep if necessary.

That is indeed a viable path. Moreover, the first bullet of the above Note is persuasive: guaranteeing evaluated-ness is quite hard!

But if we follow that path (an alternative to the to-dos in comment:21), then we should do consistently:

  • Ensure that exprOkForSpeculation on any primop does not look at lifted arguments (like the current special case for dataToTag#)

What about strict constructors? We could use CorePrep to ensure that arguments to strict constructors are evaluated, just as we do for dataToTag#. But for dataToTag# the actual argument must be a pointer to the evaluated object, otherwise dataToTag# will fail (give a bogus answer). But for strict constructors all we care about is that the argument has been evaluated (a semantic property), and that is ensured by the wrapper. To be sure, a bogus Core-to-Core pass could apply the constructor to a non-evaluated argument, but nothing would actually go wrong. So arguably it'd be redundant to add extra evals in CorePrep.

The third to-do in comment:21 would still be useful. Knowing evaluated-ness is always a good thing.

Bottom line: this alternative path looks attractive. In summary it would entail

  • Make exprOkForSpeculation treat all primops with boxed arguments like dataToTag#. More precisely, in a primop application, exprOkForSpeculation should skip over any arguments of lifted type.
  • Documenting the reasoning along the lines above.
  • Make worker/wrapper produce eval'd flags on the wrapper for CPR.
Last edited 3 years ago by simonpj (previous) (diff)

comment:24 Changed 3 years ago by RyanGlScott

Another reallyUnsafePtrEquality#-related Core Lint error popped up in https://ghc.haskell.org/trac/ghc/ticket/11444#comment:8.

comment:25 Changed 3 years ago by dfeuer

comment:26 Changed 3 years ago by simonpj

Summary: Core lint errors compiling containers HEAD with GHC HEADThe let/app invariant, evaluated-ness, and reallyUnsafePtrEquality#

comment:27 Changed 3 years ago by simonpj

Yes, taking the "alternative path" in comment:23 will fix #11444 as well.

comment:28 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 6b976eb8/ghc:

Record evaluated-ness on workers and wrappers

In Trac #13027, comment:20, I noticed that wrappers created after
demand analysis weren't recording the evaluated-ness of strict
constructor arguments.  In the ticket that led to a (debatable)
Lint error but in general the more we know about evaluated-ness
the better we can optimise.

This commit adds that info both in the worker (on args) and in
the wrapper (on CPR result patterns).

See Note [Record evaluated-ness in worker/wrapper] in WwLib

On the way I defined Id.setCaseBndrEvald, and used it to shorten
the code in a few other places

comment:29 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 5a9a173/ghc:

Refine exprOkForSpeculation

This patch implements two related changes, both inspired by
the discussion on Trac #13027, comment:23:

* exprOkForSpeculation (op# a1 .. an), where op# is a primop,
  now skips over arguments ai of lifted type.  See the comments
  at Note [Primops with lifted arguments] in CoreUtils.

  There is no need to treat dataToTag# specially any more.

* dataToTag# is now treated as a can-fail primop.  See
  Note [dataToTag#] in primops.txt.pp

I don't expect this to have a visible effect on anything, but
it's much more solid than before.

comment:30 Changed 3 years ago by rwbarton

What about seq# and seq? I'm not sure what it means for seq to be a "pseudoop", but seq# is a primop that takes a lifted argument and as far as I know it does evaluate that argument. Does it need can_fail too then?

If there's a new invariant that primops that take lifted arguments must either not examine them or have some flag(s) set (such as can_fail), a reference to Note [Primops with lifted arguments] at the top of primops.pp would be nice.

comment:31 Changed 3 years ago by dfeuer

I imagine seq# is already marked as having side effects, which should also block float-out. I haven't checked though.

comment:32 Changed 3 years ago by dfeuer

Actually, I'm wrong. I don't know what the deal is with seq#.

comment:33 Changed 3 years ago by simonpj

Owner: set to dfeuer
  • seq# is mis-named. It should really be evaluate# because it's the primop version of evaluate:
    seq# ::   a -> State# s -> (# State# s, a #)
    
    evaluate :: a -> IO a
    evaluate a = IO $ \s -> seq# a s -- NB. see #2273, #5129
    
    I don't think it needs any can_fail or has_side_effects attributes, because it is totally constrained by the threaded state. I wish I could be 100.00% certain, but that's how it looks to me.

comment:34 Changed 3 years ago by rwbarton

Lots of other primops with IO-ish type do have can_fail and has_side_effects set though, even "read-only" ones like

readMutVar# :: MutVar# s a -> State# s -> (# State# s, a #)

I know that it's not exactly a convincing argument that seq# needs the flags, but it makes me wonder...

comment:35 Changed 3 years ago by simonpj

Cc: simonmar added

Yes, but they really do have side effects. It matters when they are executed, and it matters if they are not executed at all.

That said, I doubt it would matter if the (badly named) seq# also had these attributes.

I wish I could think of an obviously-correct way to reason about this, rather than simply not being able to see a problem. Simon Marlow may be able to help.

comment:36 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 596dece/ghc:

Record evaluated-ness on workers and wrappers

Summary:
This patch is a refinement of the original commit (which
was reverted):

  commit 6b976eb89fe72827f226506d16d3721ba4e28bab
  Date:   Fri Jan 13 08:56:53 2017 +0000
      Record evaluated-ness on workers and wrappers

In Trac #13027, comment:20, I noticed that wrappers created after
demand analysis weren't recording the evaluated-ness of strict
constructor arguments.  In the ticket that led to a (debatable)
Lint error but in general the more we know about evaluated-ness
the better we can optimise.

This commit adds that info
  * both in the worker (on args)
  * and in the wrapper (on CPR result patterns).
See Note [Record evaluated-ness in worker/wrapper] in WwLib

On the way I defined Id.setCaseBndrEvald, and used it to shorten
the code in a few other places

Then I added test T13077a to test the CPR aspect of this patch,
but I found that Lint failed!

Reason: simpleOptExpr was discarding evaluated-ness info on
lambda binders because zapFragileIdInfo was discarding an
Unfolding of (OtherCon _).  But actually that's a robust
unfolding; there is no need to discard it. To fix this:

* zapFragileIdInfo only zaps fragile unfoldings

* Replace isClosedUnfolding with isFragileUnfolding (the latter
  is just the negation of the former, but the nomenclature is
  more consistent).  Better documentation too
       Note [Fragile unfoldings]

* And Simplify.simplLamBndr can now look at isFragileUnfolding
  to decide whether to use the longer route of simplUnfolding.

For some reason perf/compiler/T9233 improves in compile-time
allocation by 10%.  Hooray

Nofib: essentially no change:

--------------------------------------------------------------------------------
        Program           Size    Allocs   Runtime   Elapsed  TotalMem
--------------------------------------------------------------------------------
      cacheprof          +0.0%     -0.3%     +0.9%     +0.4%     +0.0%
--------------------------------------------------------------------------------
            Min          +0.0%     -0.3%     -2.4%     -2.4%     +0.0%
            Max          +0.0%     +0.0%     +9.8%    +11.4%     +2.4%
 Geometric Mean          +0.0%     -0.0%     +1.1%     +1.0%     +0.0%

comment:37 Changed 3 years ago by David Feuer <David.Feuer@…>

In b3576ed/ghc:

Mark reallyUnsafePtrEquality# as can_fail

As described in the note, floating `reallyUnsafePtrEquality#`
out can make it much less precise. Marking it `can_fail` will
prevent it from floating out, which I believe is particularly
important in light of 5a9a1738023aeb742e537fb4a59c4aa8fecc1f8a,
and should also help prevent let/app invariant failures as seen
in #11444 and #13027.

Reviewers: simonpj, austin, bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D2987

GHC Trac Issues: #13027, #11444

comment:38 Changed 3 years ago by bgamari

Resolution: fixed
Status: newclosed

I believe this should now be resolved.

Note: See TracTickets for help on using tickets.