worker-wrapper correctness

[Joachim Breitner]

Hi,

I first planned to post this to
https://ghc.haskell.org/trac/ghc/ticket/1600 but it might be of wider
interest, and is not only related to CPR.

SPJ pointed me to this¹ paper by Graham Hutton (thanks for that). It
lists three sufficient conditions for the w/w-wrapper to be semantically
correct:

        (1) wrap ◦ unwrap = id
        (2) wrap ◦ unwrap ◦ body = body
        (3) fix (wrap ◦ unwrap ◦ body) = fix body
        
The first one is often not true when we do w/w in GHC. The third one
seems to be out of reach: Arguing about a recursive function in this way
smells like solving the halting problem. So it seems that we should be
aiming for

        (2) wrap ◦ unwrap ◦ body = body

With this in mind, setting the CPR info of recursive things to ⊤, i.e.
“we don’t know anything” _when analyzing their RHS_ should do the right
thing: If we assume nothing about the argument of `body`, the result
will hold for all, which precisely is `wrap ◦ unwrap ◦ body = body`.

And this should be the case not only for CPR, but for anything that does
a w/w-transformation, i.e. Demand analysis as well.

But what about strictness analysis? Clearly, for

        f :: Int -> Int -> Int
        f n m = if n == 0 then m else f (n-1) m
        
we want to know (as we do in 7.6. and in HEAD) that it is strict in m...

Interesting fact here: GHC-7.6 will find this worker signature

    wf :: Int# -> Int -> Int

(which is compatible with condition (2)), but GHC HEAD will do

    wf :: Int# -> Int# -> Int#

where equation (2) is no longer holds. In this case (3) happens to hold
(at least wrt to a semantics that does not distinguish non-termination
of other kinds of ⊥).


Conclusion: The correctness of GHC’s w/w-transformation is currently not
formally well supported, and it only works due to delicate and
non-obvious² interaction between the analysis and the transformation
(see comment 20 of #1600 for an example how easily it breaks). But if we
systematically ensure the correctness, by always guaranteeing (2), we
are losing existing chances for optimization.


Some more less consistent thoughts:

There seems to be a conceptual difference between the CPR
w/w-transformation and the others: Unboxing arguments pulls work out of
the worker to be done _before_ it is being called. Clearly, this will
never make the recursive call to the work diverge, unless it would
diverge anyways. And if the work pulled out diverges (e.g. if m =
undefined in the example above), then either the worker would have
diverged (but that is fine) or, assuming the analysis is correct, would
have performed the work. So for these transformations it is ok to use
the full information in the recursive case.

But the CPR transformation is different: The w/w transformation forces
the evaluation of the result of the recursive call and in that sense
moves work into it. And if this again triggers work to be moved into the
next recursive calls, we can cause divergence.

So by this handwavy argument, we are fine for unboxing arguments and
strictness analysis, but for CPR we really should forget what we know
about the f when analyzing f’s body.



Thanks for your attention,
Joachim

¹ http://www.cs.nott.ac.uk/~gmh/wrapper.pdf
² to me at least – I might be missing something
-- 
Joachim “nomeata” Breitner
  mail at joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20131128/b65888ee/attachment.sig>