Opened 4 years ago

Closed 3 months ago

Last modified 5 weeks ago

#8091 closed bug (fixed)

retry# lacks strictness information

Reported by: parcs Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.6.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The retry# primop should be marked as returning bottom since it never actually returns anything as far as the simplifier is concerned. This change would help the simplifier eliminate unreachable code inside STM transactions.

Change History (13)

comment:1 Changed 4 years ago by parcs

Status: newpatch

The patch (validated):

  • compiler/prelude/primops.txt.pp

    diff --git a/compiler/prelude/primops.txt.pp b/compiler/prelude/primops.txt.pp
    index 3d3518b..e12c1a5 100644
    a b primop AtomicallyOp "atomically#" GenPrimOp 
    16141614primop  RetryOp "retry#" GenPrimOp
    16151615   State# RealWorld -> (# State# RealWorld, a #)
    16161616   with
     1617   strictness  = { \ _arity -> mkStrictSig (mkTopDmdType [topDmd] botRes) }
    16171618   out_of_line = True
    16181619   has_side_effects = True
    16191620

The unfoldings in Control.Concurrent.STM.TSem and .TQueue are improved as a result of this change due to the aforementioned dead code elimination.

comment:2 Changed 4 years ago by simonpj

I like the idea, but it does have strictness consequences too. For example:

f :: TVar Int -> Int -> STM Int
f r y = do { v <- readTVar r
           ; if v>0 then retry
                    else if y>0 then return 0 else return y
           }

I have not checked but I think this will not be strict in y because the then branch doesn't evaluate y. With your change it'll become strict in y, just as it would if you replace retry with throw exn. I think that's probably fine, and no one will even notice; just saying.

Simon

comment:3 in reply to:  2 Changed 4 years ago by parcs

Ah, subtle..

But in this particular example , f seems to be lazy in y even when retry is replaced with throw Overflow: its strictness signature is <S,1*U(U)><L,1*U(U)><L,U> either way..

(It would be incorrect, I think, to have f strict in y since that could potentially elide the side-effect-having call to readTVar.)

I found an example of a function whose strictness does change due to this patch (courtesy of the comments for RaiseIOOp in primops.txt.pp):

g :: Int -> Int -> STM Int
g x y | x>0       = retry
      | y>0       = return 1
      | otherwise = return 2

This function is now strict in y, where it originally wasn't. It looks like this change will only have strictness implications in fairly contrived functions where retry is used in such a way that the transaction could not possibly make any progress; and in that case behaving as if retry returns bottom makes a good amount of sense.

Version 0, edited 4 years ago by parcs (next)

comment:4 Changed 4 years ago by parcs

To be clear, the form of dead code elimination that this change enables is

replacing

case retry# s1 of
    (# s2, a #) -> ...inaccessible..

with simply

retry# s1

Such Core can appear after performing case-of-case on code like

s <- readTVar v
when (s > 0) retry
...

where everything after the when statement might get inlined under the scrutinization of retry.

comment:5 Changed 4 years ago by thoughtpolice

Resolution: fixed
Status: patchclosed

Thanks Patrick. Committed in

commit e2b72cadce3ae799a74981f9957b40bb201f1ba1
Author: Austin Seipp <aseipp@pobox.com>
Date:   Sat Aug 10 22:39:15 2013 -0500

    Mark retry# as returning bottom.
    
    This change helps the simplifier eliminate unreachable code, since
    retry# technically doesn't return.
    
    This closes ticket #8091.
    
    Authored-by: Patrick Palka <patrick@parcs.ath.cx>
    Signed-off-by: Austin Seipp <aseipp@pobox.com>

comment:6 Changed 4 years ago by simonpj

I wonder if we might have a regression test here... Perhaps a -ddump-simpl and check that a function in the ...inaccessible... part no longer appears? Simon

comment:7 Changed 3 months ago by bgamari

#13916 leads me to believe this is strictness signature is too strong. Consider this program,

loop :: [TMVar a] -> STM a -> STM a
loop []     m = m
loop (x:xs) m = loop xs (m `orElse` takeTMVar x)

doIt :: [TMVar Int] -> STM Int
doIt xs = atomically $ loop xs retry

GHC will currently give loop a strictness signature of <S,1*U><C(S),1*C1(U(U,U))>. So this means that if we give retry# a divergent result demand GHC incorrectly assume that loop xs retry will itself diverge, which is clearly not true (since the orElse allows us to "catch" this divergence and instead return a value).

In the case of #13916, we had a case like the following,

f :: [TMVar Int] -> STM (Either Int ())
f xs = do
    x <- doIt xs
    case x of
      x -> return (Left x)

Since GHC incorrectly concluded that doIt diverges, it took the liberty of dropping the case alternatives. The code generator then instead emitted just doIt xs in place of the case analysis. This is, of course, ill-typed: the caller of f expects to receive an Either Int (), but f will in actuality return an Int since the result of the case analysis was inappropriately dropped.

Last edited 3 months ago by bgamari (previous) (diff)

comment:8 Changed 3 months ago by bgamari

Resolution: fixed
Status: closednew

comment:9 Changed 3 months ago by bgamari

Actually, comment:7 isn't quite right: The fact that loop doesn't diverge should be accounted for by the ExnStr of the first argument of orElse. I would have thought that the ExnStr should propagate to the second argument of loop during demand analysis but it doesn't. That seems to be the issue. See #13977.

Last edited 3 months ago by bgamari (previous) (diff)

comment:10 Changed 3 months ago by bgamari

Resolution: fixed
Status: newclosed

It turns out that the root cause was #13977, which was fixed by Phab:D3756. Closing.

comment:11 Changed 3 months ago by simonpj

Do we have a regression test?

comment:12 Changed 3 months ago by bgamari

Do you mean for #13977? I intend on adding the case from #13916 to the testsuite. It's imperfect but better than nothing.

comment:13 Changed 5 weeks ago by Ben Gamari <ben@…>

In 10a1a47/ghc:

Model divergence of retry# as ThrowsExn, not Diverges

The demand signature of the retry# primop previously had a Diverges
result.  However, this caused the demand analyser to conclude that a
program of the shape,

    catchRetry# (... >> retry#)

would diverge. Of course, this is plainly wrong; catchRetry#'s sole
reason to exist is to "catch" the "exception" thrown by retry#. While
catchRetry#'s demand signature correctly had the ExnStr flag set on its
first argument, indicating that it should catch divergence, the logic
associated with this flag doesn't apply to Diverges results. This
resulted in #14171.

The solution here is to treat the divergence of retry# as an exception.
Namely, give it a result type of ThrowsExn rather than Diverges.

Updates stm submodule for tests.

Test Plan: Validate with T14171

Reviewers: simonpj, austin

Subscribers: rwbarton, thomie

GHC Trac Issues: #14171, #8091

Differential Revision: https://phabricator.haskell.org/D3919
Note: See TracTickets for help on using tickets.