Changes between Version 26 and Version 27 of NestedCPR


Ignore:
Timestamp:
Jan 10, 2014 11:46:09 AM (19 months ago)
Author:
nomeata
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NestedCPR

    v26 v27  
    1515=== TODOs ===
    1616
    17  * Does Nick Frisby’s late λ-lifting alleviate problems when CPR’ing join-points?
    18    * Need to see if his branch can be merged onto master.
    1917 * Paper-Writeup of CPR
    2018 * Shouldn’t nested CPR help a lot with Complex-heavy code? Is there something in nofib?
     
    2220 * Use ticky-profiling to learn more about the effects of nested CPR.
    2321 * Look at !DmdAnal-related [SLPJ-Tickets] and see which ones are affected by nested-cpr.
    24  * Do not destroy join points (see below).
    25  * Can we make sure more stuff gets the `Converging` flag, e.g. after a `case` of an unboxed value? Should case binders get the `Converging` flag? What about pattern match variables in strict data constructors? Unboxed values?
    26  * Why does nested CPR make some stuff so bad?
    27   * Possibly because of character reboxing. Try avoiding CPR’ing `C#` alltogether!
     22 * Do not destroy join points or improve the code genrator (see below).
     23 * Can we make sure more stuff gets the `Converging` flag, e.g. after a `case` of an unboxed value? Should case binders get the `Converging` flag? What about pattern match variables in strict data constructors? Unboxed values? See below.
    2824
    2925=== Degradation exploration and explanation ===
     
    4541Nested CPR is only sound if we know that the nested values are known to converge for sure. The semantics is clear: If `f` has CPR `<...>m(tm(),)`, then in the body of `case f x of (a,b)`, when entering `a`, we are guaranteed termination.
    4642
    47 What is the semantics of an outer `t`? Given `f` with CPR `<L>tm()` and `g` with CPR `<S>tm()`? Does the latter even make sense? If so, should `f undefined` have CPR `m()` or `tm()`? Two possibilities:
     43What is the semantics of an outer `t`? Given `f` with CPR `<L>tm()` and `g` with CPR `<S>tm()`? Does the latter even make sense? If so, should `f undefined` have CPR `m()` or `tm()`? Three possibilities:
    4844 1. The convergence information a function is what holds if its strictness annotations are fulfilled: So if `g x`  has `tm()` if `x` has `t` (possibly because it has previously been evaluated by the caller), otherwise `m()`. `f x` always has `m ()` (presumably because `x` is _never_ entered when evaluating `f`.
    4945 2. The convergence information a function is what holds always. This would in effect prevent `<S>tm()` from happening.
    50 
    51 Clearly, 1. holds strictly more information than 2.: Under variant `2`, `<S>tm()` would not occur, while under variant 1 that would be usefully different from `<S>m()`.
    52 
    53 Also, under 2, `I#` would not be known to terminate for sure, as it is strict. This would destroy any hope for nested CPR for things like `(Int, Int)`.
    54 
    55 For the implementation this implies that we need to be careful when `lub`’ing: If one branch is lazy, but not absent in an argument or free variable), and the other branch is strict, then even if both branches claim to terminate, we need to remove the termination flag (as one had the termination under a stronger hypothesis as the hole result) (Feels inelegant.)
    56 
    57 Similar thought needs to be considered whenever one goes up in the lattice (better always go up by using `lub` then...)
    58 
    59 In pictures: This is the lattice, which is not a simple product lattice any more:
    60 {{{
    61        ------ <L><L>------
    62      /          | \       \
    63     /           | <L><L>t  \
    64 <S><L>          |           <S><L> 
    65  |  \ \         |           |  |  \
    66  |   \ <S><L>t  |          /   |   <S><L>t
    67  |    \         |         /    |
    68  \     \        |        /     | 
    69   \     ----- <S><S>-----      |
    70    \           |    \          |
    71     \          |     <S><S>t   /
    72      \         |              /
    73       ---------⊥-------------/
    74 }}}
     46 3. The convergence information always holds, but special care is taken for unlifted types: `I#`, like any function expecting an unlifted parameter or free variable, would get `<S>tm()`. (For unlifted types, `<L>` and `<S>` are identical. One might turn that into a third way `<#>`, but unless there is more use to that than just clarification, we do not do that).
    7547
    7648
    77 When evaluating a demand type as a demand transformer, we need to compare the convergence flags of the argument expressions with the strictness demands, and possibly adjust the termination information. I believe can be done using `deferAndUse` as before.
     49Clearly, 1. and 3. hold strictly more information than 2.: Under variant `2`, `<S>tm()` would not occur, while the other variants allow that. Also, under 2, `I#` would not be known to terminate for sure, as it is strict. This would destroy any hope for nested CPR for things like `(Int, Int)`.
    7850
    79 What about nested strictness annotations? For now the hypothesis of the demand transformer only requires the arguments (and free variables) to be terminating; if there is a `<S(S)>`, then it should not be marked as converging. Maybe this can be improved later, using nested CPR.
    80 
    81 Some implementation implications:
    82  * There is no unit for `lubDmdType` any more. So for case, use `botDmdType` for no alternatives, and `foldr1` if there are multiple.
    83  * Unlifted variables (e.g. `Int#`) are tricky. Everything is strict in them, so for an *unlifted* argument, `<L>t` implies `<S>t` and hence `<S>t ⊔ <L>t = <S>t`, and we really want to make use of that stronger equation. But when lub’ing, we don’t know any more if this is the demand for an unlifted type. So instead, the demand type of `x :: Int#` itself is `{x ↦ <L>} t`, while `x :: Int` continues to have type `{x ↦ <S>} t`.
    84  * It is important that functions (including primitive operations and constructors like `I#`) have a strict demand on their unlifted argument. But it turned out to be easier to enforce this in the demand analyser: So even if `f` claims to have a lazy demand on a argument of unlifted type, we make this demand strict before feeding it into the argument.
    85  * **It is no longer safe to remove variables from the demand environment**, if the demand on them is strict. There must be so many bugs lurking around...
    86 
    87 Unfortunate example:
    88 {{{
    89 g :: Int -> Int
    90 g 1 = 0
    91 g x = x
    92 }}}
    93 What should its signature be? We want `<S>t`, but we get `<S>`. Why? Because the branches have signatures `t` and `{x ↦ S} t`. So their lub is going to be `{x ↦ L}`. In a later step, the demand on `x` will be strict again, but that is not easily visible here.
    94 
    95 Can we avoid this? Not if we want to keep using the strictness demand as the hypothesis for the termination information. The alternative would be to to track the demand required separately from strictness. Then the lub of `t` and `{x ↦ required} t` would be `{x ↦ required} t`, and this case would work fine. That would turn it into a completely separate analysis, it seems.
     51I worked on 1, but it turned out to be too complicated. Notes at [wiki:./AdvancedConverges]. So I’ll proceed with 3. now.
    9652
    9753=== join points ===
    9854
    99 CPR can kill join points.
     55CPR can kill join points. Attempts to mitigate that:
    10056
    10157==== Common Context ====
     
    11672 * Enabling sum types inside nested CPR: TBD
    11773
     74Unfortunately, naive approaches are not possible: We need to know if `j` is a joint point not only for `let j = .. in ... j ..`, but also for expressions further out. Not nice.
     75
     76==== Improvement to the code generator ====
     77
     78It seems feasible to make the code generate generate better code for local functions that are not quite join-points any more, by jumping, passing both a continuation and a stack delta to the live variables. To be investigated.
     79
     80==== Late lambda lifting ====
     81
     82Might also help. Need to see if his branch can be merged onto master. (But I like the code generator idea better.)
     83
     84
    11885=== Side tracks ===
    11986