static checker for numerical instability

[Roger-luo]

just posting the idea here, I just realize one could check the potential numerical instability using an abstract interpreter, so instead of creating a new package, I feel it might fit better here, e.g

1. a program is using the x>0 branch of exp, instead of converting it to exp(-x) form for x > 0 etc.
2. 1/x and x can be a Julia expression that can potentially be zero

I guess there could be more cases for this type of error, but I didn't find any literature on this, I guess it's because instead of the Julia community, not many programming language folks focus on checking numerical programs?

[aviatesk]

Hi, sorry for my delayed response.

a program is using the x>0 branch of exp, instead of converting it to exp(-x) form for x > 0 etc.

Maybe you meant log, right ?

I guess it's because instead of the Julia community, not many programming language folks focus on checking numerical programs?

Maybe ? Well, numerical validation check can certainly be a target of abstract-interpretation based analysis. Julia's type lattice already includes some of those cases as a form of constant-folded element, and JET can report an error when the value is known to be constant, e.g.:

julia> report_call() do
           log(-10)
       end
═════ 1 possible error found ═════
┌ @ REPL[14]:2 Main.log(-10)
│┌ @ math.jl:1221 Base.Math.log(xf)
││┌ @ special/log.jl:269 Base.Math._log(x, Base.Math.Val(:ℯ), :log)
│││┌ @ special/log.jl:304 Base.Math.throw_complex_domainerror(func, x)
││││┌ @ math.jl:32 Base.Math.throw_complex_domainerror(::Symbol, ::Float64)
│││││ may throw: Base.Math.throw(Base.Math.DomainError(x::Float64, Base.Math.string(Base.string(f::Symbol, " will only return a complex result if called with a ")::String, Base.string("complex argument. Try ", f::Symbol, "(Complex(x)).")::String)::String)::DomainError)
││││└──────────────
Union{}

The problem here is that Julia's type lattice implementation is not designed for validation of numerical computing, but for type inference for better performance. So for example, Julia's type inference (and JET's analysis) can't understand numerical range well since there is no lattice element to express that:

julia> report_call((Int,)) do n
           if n < 0
               return log(n)
           end
           return 0.0
       end
No errors !
Float64

In the compiler, n after the n < 0 branch is still represented as Int, not as NumericalRange(typemin(Int), -1) or something like that, since we think the latter would not be so useful for type inference. In other word, useful analysis for checking validation of numerical computation may require another dedicated lattice implementation, which probably well-expresses numerical range and such. And another lattice implementation means re-implementation of most parts of abstract interpretation routines implemented within the Julia compiler, since it's tightly bound to its own lattice implementation.

So in conclusion validation of numerical computation might be better to be implemented as another package, unless we refactor Julia's abstract interpretation implementation so that we can plug-in another lattice implementation (I'm not sure even it's possible).

[AriMKatz]

unless we refactor Julia's abstract interpretation implementation so that we can plug-in another lattice implementation (I'm not sure even it's possible).

@Keno and @femtomc were discussing just that

[aviatesk]

Interesting, any link or reference ?

[femtomc]

No link or reference other than our convo on JuliaCompilerPlugins -- I think we do need to take a principled approach to extending the lattice. AbstractInterpreter is likely not enough -- because of the comments you made about logic which is specific to standard inference.

I'm not sure what this looks like, as I'm pretty new to abstractinterpretation.jl.

[Roger-luo]

I think there were some discussion between @Keno and @femtomc in slack channel compiler-plug-in.

On the other hand I recently realize I also need the ability to insert custom type lattice to infer if a number is multiple of pi which is useful for optimization in our quantum compiler.

Might be good to start an issue under julialang/Julia?

[aviatesk]

Yeah, that sounds good.