Refine LimitedAccuracy's ⊑ semantics #48045

Keno · 2022-12-30T13:17:34Z

As discussed in #48030, this is a different attempt to fix the semantics of LimitedAccuracy. This fixes the same test case as #48030, but keeps LimitedAccuracy ε smaller than its wrapped lattice element. The primary change here is that now all lattice elements that are strictly ⊑ T are now also ⊑ LimitedAccuracy(T), whereas before that was only true for other LimitedAccuracy elements.

Quoting the still relevant parts of #48030's commit message:

I was investigating some suboptimal inference in Diffractor
(which due to its recursive structure over the order of the
taken derivative likes to tickle recursion limiting) and
noticed that inference was performing some constant propagation,
but then discarding the result. Upon further investigation,
it turned out that inference had determined the function to be
`LimitedAccuracy(...)`, but constprop found out it actually
returned `Const`. Now, ordinarily, we don't constprop functions
that inference determined to be `LimitedAccuracy`, but this
function happened to have `@constprop :aggressive` annotated.

Of course, if constprop determines that the function actually
terminates, we do want to use that information. We could hardcode
this in abstract_call_gf_by_type, but it made me take a closer look
at the lattice operations for `LimitedAccuracy`, since in theory
`abstract_call_gf_by_type` should prefer a more precise result.

base/compiler/typelimits.jl

vtjnash · 2022-12-30T14:42:10Z

base/compiler/typelimits.jl

+            issimplertype(lattice, typeb, typea) && return LimitedAccuracy(typeb, causesb)
+        elseif suba
+            issimplertype(lattice, typeb, typea) && return LimitedAccuracy(typeb, causesb)
+            causes = causesnb


vtjnash · 2022-12-30T14:42:35Z

base/compiler/typelimits.jl

+            causes = causesnb
+            # `a`'s causes may be discarded
+        elseif subb
+            causes = causesb


symmetry?

Suggested change

causes = causesb

issimplertype(lattice, typea, typeb) && return LimitedAccuracy(typea, causesa)

causes = causesa

The issimplertype test is below, but yes this should have been causesa.

vtjnash · 2022-12-30T14:51:36Z

base/compiler/typelattice.jl

@@ -368,7 +404,8 @@ ignorelimited(typ::LimitedAccuracy) = typ.typ
 function ⊑(lattice::InferenceLattice, @nospecialize(a), @nospecialize(b))
    if isa(b, LimitedAccuracy)
        if !isa(a, LimitedAccuracy)
-            return false
+            # epsilon smaller
+            return ⊑(widenlattice(lattice), a, b.typ) && !⊑(widenlattice(lattice), b.typ, a)
        end
        if b.causes ⊈ a.causes
            return false


This should reflect the epsilon case too, though I think that means refactoring part of this code for better ordering than this

Suggested change

return false

if ⊑(widenlattice(lattice), a.typ, b.typ)

return true

end

return false

(This also must be reflected now in the type-complexity tests. Where this is meaning the comparison of the length of causes.)

the type-complexity tests

You mean issimplertype? In the current design, that's not reached for LimitedAccuracy and before we were just passing those arguments through ignorelimited.

Yeah. It seems a little odd for tmerge_fast_path not to be legal anymore for this type, but I guess that looks right. We should perhaps assert there since we know LimitedAccuracy may be handled wrong there now?

We were correct before, since it was already implied by the precondition of suba or subb. That assumed implication is no longer valid after this change.

Let me remove the ignorelimited in issimplertype then. We'll get an appropriate assertion if somebody accidentally uses it.

Keno · 2022-12-30T17:11:01Z

@nanosoldier runtests()

nanosoldier · 2022-12-31T11:20:13Z

Your package evaluation job has completed - possible new issues were detected. A full report can be found here.

As discussed in #48030, this is a different attempt to fix the semantics of LimitedAccuracy. This fixes the same test case as #48030, but keeps `LimitedAccuracy` ε smaller than its wrapped lattice element. The primary change here is that now all lattice elements that are strictly `⊑ T` are now also `⊑ LimitedAccuracy(T)`, whereas before that was only true for other `LimitedAccuracy` elements. Quoting the still relevant parts of #48030's commit message: ``` I was investigating some suboptimal inference in Diffractor (which due to its recursive structure over the order of the taken derivative likes to tickle recursion limiting) and noticed that inference was performing some constant propagation, but then discarding the result. Upon further investigation, it turned out that inference had determined the function to be `LimitedAccuracy(...)`, but constprop found out it actually returned `Const`. Now, ordinarily, we don't constprop functions that inference determined to be `LimitedAccuracy`, but this function happened to have `@constprop :aggressive` annotated. Of course, if constprop determines that the function actually terminates, we do want to use that information. We could hardcode this in abstract_call_gf_by_type, but it made me take a closer look at the lattice operations for `LimitedAccuracy`, since in theory `abstract_call_gf_by_type` should prefer a more precise result. ```

Tests currently depend on JuliaLang/julia#48045 and JuliaLang/julia#48059, so we should either get those merged first, or mark them here as broken.

base/compiler/abstractinterpretation.jl

base/compiler/typelattice.jl

base/compiler/typelimits.jl

Co-authored-by: Shuhei Kadowaki <40514306+aviatesk@users.noreply.github.com>

Keno · 2023-01-02T11:30:02Z

I think this should be good to go. PkgEval looks good.

vtjnash · 2023-01-02T19:14:23Z

base/compiler/typelattice.jl

+
+    # a and b's unlimited types are equal.
+    isa(a, LimitedAccuracy) || return false # b is limited, so ε smaller
+    return a.causes ⊆ b.causes


The old code used to have the inverse check here

Suggested change

return a.causes ⊆ b.causes

return b.causes ⊆ a.causes

Was this supposed to get switched here? I think that is incorrect now, as the wider result should have fewer causes, but this does the opposite.

Let me double check. I don't think I intended to switch it - it's possible I got my cases mixed up.

vtjnash · 2023-01-02T19:17:50Z

base/compiler/typelimits.jl

+        # Approximated types are lattice equal. Merge causes.
+        if suba && subb
+            causes = merge_causes(causesa, causesb)
+            issimplertype(lattice, typeb, typea) && return LimitedAccuracy(typeb, causesb)


Suggested change

issimplertype(lattice, typeb, typea) && return LimitedAccuracy(typeb, causesb)

issimplertype(lattice, typeb, typea) && return LimitedAccuracy(typeb, causes)

I think symmetry and equality demands that you are not supposed to check issimplertype in this case (see tmerge_fast_path)

Well, we are still changing the lattice element here potentially if the causes are different, but yes fair enough, I'll drop the issimplertype check.

Good point though. Is this new tmerge algorithm monotonic and convergent? In particular, this merge call here (with the heuristic towards shorter lengths but calling union if undecidable) seems like it might make inference non-terminating as it repeatedly merged and dropped causes lists here in a loop

As discussed in #48045: 1. Switch the order of `causes` inclusion to make wider elements have fewer causes. 2. Fix two typos 3. Restore property that equal ulimited types will be preserved (though with potentially updated `causes` lists).

* Hookup demand-driven forward mode to the Diffractor runtime Tests currently depend on JuliaLang/julia#48045 and JuliaLang/julia#48059, so we should either get those merged first, or mark them here as broken. * Mark test as broken

As discussed in #48045: 1. Switch the order of `causes` inclusion to make wider elements have fewer causes. 2. Fix two typos 3. Restore property that equal ulimited types will be preserved (though with potentially updated `causes` lists).

Keno requested review from vtjnash and aviatesk December 30, 2022 13:17

Keno mentioned this pull request Dec 30, 2022

Switch where LimitedAccuracy sits in the ⊑ lattice #48030

Closed

vtjnash reviewed Dec 30, 2022

View reviewed changes

Keno force-pushed the kf/limaccpos2 branch from be9bd9a to eaa1d81 Compare December 30, 2022 17:09

Keno force-pushed the kf/limaccpos2 branch from eaa1d81 to 0c131e9 Compare December 31, 2022 16:10

Keno mentioned this pull request Dec 31, 2022

Hookup demand-driven forward mode to the Diffractor runtime JuliaDiff/Diffractor.jl#99

Merged

aviatesk reviewed Jan 1, 2023

View reviewed changes

base/compiler/abstractinterpretation.jl Outdated Show resolved Hide resolved

base/compiler/typelattice.jl Outdated Show resolved Hide resolved

base/compiler/typelimits.jl Outdated Show resolved Hide resolved

Apply suggestions from code review

0c6df0b

Co-authored-by: Shuhei Kadowaki <40514306+aviatesk@users.noreply.github.com>

Keno merged commit fe45f01 into master Jan 2, 2023

Keno deleted the kf/limaccpos2 branch January 2, 2023 18:56

vtjnash reviewed Jan 2, 2023

View reviewed changes

Keno mentioned this pull request Jan 4, 2023

Further tweaks to LimitedAccuracy lattice operations #48126

Merged

vtjnash mentioned this pull request Jan 22, 2023

tmerge for LimitedAccuracy is not convergent #48376

Open

aviatesk mentioned this pull request Jan 11, 2024

inference: always bail out const-prop' with non-const result limited #52836

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refine LimitedAccuracy's ⊑ semantics #48045

Refine LimitedAccuracy's ⊑ semantics #48045

Keno commented Dec 30, 2022

vtjnash Dec 30, 2022

vtjnash Dec 30, 2022

Keno Dec 30, 2022

vtjnash Dec 30, 2022

vtjnash Dec 30, 2022

Keno Dec 30, 2022

vtjnash Dec 30, 2022

vtjnash Dec 30, 2022

Keno Dec 31, 2022

Keno commented Dec 30, 2022

nanosoldier commented Dec 31, 2022

Keno commented Jan 2, 2023

vtjnash Jan 2, 2023

Keno Jan 2, 2023

vtjnash Jan 2, 2023

vtjnash Jan 2, 2023

Keno Jan 4, 2023

vtjnash Jan 5, 2023

	causes = causesb
	issimplertype(lattice, typea, typeb) && return LimitedAccuracy(typea, causesa)
	causes = causesa

	issimplertype(lattice, typeb, typea) && return LimitedAccuracy(typeb, causesb)
	issimplertype(lattice, typeb, typea) && return LimitedAccuracy(typeb, causes)

Refine LimitedAccuracy's ⊑ semantics #48045

Refine LimitedAccuracy's ⊑ semantics #48045

Conversation

Keno commented Dec 30, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Keno commented Dec 30, 2022

nanosoldier commented Dec 31, 2022

Keno commented Jan 2, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment