Take purity modeling seriously

[Keno]

TLDR

Before:

julia> let b = Expr(:block, (:(y += sin($x)) for x in randn(1000))...)
           @eval function f_sin_perf()
               y = 0.0
               $b
               y
           end
       end
f_sin_perf (generic function with 1 method)

julia> @time @code_typed f_sin_perf()
 15.707267 seconds (25.95 M allocations: 1.491 GiB, 3.30% gc time)
[lots of junk]

After:

julia> @time @code_typed f_sin_perf()
  0.016818 seconds (187.35 k allocations: 7.901 MiB, 99.73% compilation time)
CodeInfo(
1 ─     return 27.639138714768546
) => Float64

so roughly a 1000x improvement in compile time performance for const-prop heavy functions.

There are also run time improvements for functions that have patterns like:

function some_function_to_big_to_be_inlined_but_pure(x)
....
end

function foo(x)
some_function_to_big_to_be_inlined_but_pure(x)
return x
end

The inliner will now be able to see that some_function_to_big_to_be_inlined_but_pure is effect free, even without inlining it and just delete it, improving runtime performance (if some_function_to_big_to_be_inlined_but_pure is small enough to be inlined, there is a small compile time throughput win, by being able to delete it without inlining, but that's a smaller gain than the compile time gain above).

Motivation / Overview

There are two motivations for this work. The first is the above mentioned improvement in compiler performance for const-prop heavy functions. This comes up a fair bit in various Modeling & Simulation codes we have where Julia code is often auto-generated from some combination of parameterized model codes and data. This ends up creating enormous functions with significant need for constant propagation (~50k statements with ~20k constant calls are not uncommon). Our current compiler was designed for people occasionally throwing a sqrt(2) or something in a function, not 20k of them, so performance is quite bad.

The second motivation is to have finer grained control over our purity modeling. We have @Base.pure, but that has somewhat nebulous semantics and is quite a big hammer that is not appropriate in most situations.

These may seem like orthogonal concerns at first, but they are not. The compile time issues fundamentally stem from us running constant propagation in inference's abstract interpreter. However, for simple, pure functions, that is entirely unnecessary, because we have a super-fast, JIT compiler version of that function just laying around in general. The issue is that we currently, we generally do not know when it is legal to run the JIT-compiled version of the function and when we need to abstractly interpret it. However, if the compiler were able to figure out an appropriate notion of purity, it could start doing that (which is what it does now for @Base.pure functions).

This PR adds that kind of notion of purity, converges it along with type information during inference and then makes use of it to speed up evaluation of constant propagation (where it is legal to do so), as well as improving the inliner.

The new purity notions

The new purity model consists of four different kinds flags per code instance. For builtins and intrinsics the existing effect free and nothrow models are re-used. There is also a new macro @Base.assume_effects available, which can set the purity base case for methods or :foreigncalls. Here is the docstring for that macro, which also explains the semantics of the new purity flags:

    @assume_effects setting... ex
    @assume_effects(setting..., ex)

`@assume_effects` overrides the compiler's effect modeling for the given method.
`ex` must be a method definition.

WARNING: Improper use of this macro causes undefined behavior (including crashes,
incorrect answers, or other hard to track bugs). Use with care an only if absolutely
required.

In general, each `setting` value makes an assertion about the behavior of the
function, without requiring the compiler to prove that this behavior is indeed
true. These assertions are made for all world ages. It is thus advisable to limit
the use of generic functions that may later be extended to invalidate the
assumption (which would cause undefined behavior).

The following `settings` are supported.
# `:consistent`

The `:consistent` setting asserts that for egal inputs:
    - The manner of termination (return value, exception, non-termination) will always be the same.
    - If the method returns, the results will always be egal.

Note: This in particular implies that the return value of the method must be
      immutable. Multiple allocations of mutable objects (even with identical
      contents) are not egal.

Note: The idempotency assertion is made world-arge wise. More formally, write
      fₐ for the evaluation of `f` in world-age `a`, then we require:

          ∀ a, x, y: x === y → fₐ(x) === fₐ(y)

      However, for two world ages `a, b` s.t. `a != b`, we may have `fₐ(x) !== fₐ(y)``

Note: A further implication is that idempontent functions may not make their
      return value dependent on the state of the heap or any other global state
      that is not constant for a given world age.

Note: The idempontency includes all legal rewrites performed by the optimizizer.
      For example, floating-point fastmath operations are not considered idempotent,
      because the optimizer may rewrite them causing the output to not be idempotent,
      even for the same world age (e.g. because one ran in the interpreter, while
      the other was optimized).

# `:effect_free`

The `:effect_free` setting asserts that the method is free of externally semantically
visible side effects. The following is an incomplete list of externally semantically
visible side effects:

 - Changing the value of a global variable.
 - Mutating the heap (e.g. an array or mutable value), except as noted below
 - Changing the method table (e.g. through calls to eval)
 - File/Network/etc. I/O
 - Task switching

However, the following are explicitly not semantically visible, even if they
may be observable:

 - Memory allocations (both mutable and immutable)
 - Elapsed time
 - Garbage collection
 - Heap mutations of objects whose lifetime does not exceed the method (i.e.
   were allocated in the method and do not escape).
 - The returned value (which is externally visible, but not a side effect)

The rule of thumb here is that an externally visible side effect is anything
that would affect the execution of the remainder of the program if the function
were not executed.

Note: The effect free assertion is made both for the method itself and any code
      that is executed by the method. Keep in mind that the assertion must be
      valid for all world ages and limit use of this assertion accordingly.

# `:nothrow`

The `:nothrow` settings asserts that this method does not terminate abnormally
(i.e. will either always return a value or never return).

Note: It is permissible for :nothrow annotated methods to make use of exception
      handling internally as long as the exception is not rethrown out of the
      method itself.

Note: MethodErrors and similar exceptions count as abnormal termination.

# `:terminates_globally`

The `:terminates_globally` settings asserts that this method will eventually terminate
(either normally or abnormally), i.e. does not infinite loop.

Note: The compiler will consider this a strong indication that the method will
      terminate relatively *quickly* and may (if otherwise legal), call this
      method at compile time. I.e. it is a bad idea to annotate this setting
      on a method that *technically*, but not *practically*, terminates.

Note: The `terminates_globally` assertion, covers any other methods called by
      the annotated method.

# `:terminates_locally`

The `:terminates_locally` setting is like `:terminates_globally`, except that it only
applies to syntactic control flow *within* the annotated method. It is this
a much weaker (and thus safer) assertion that allows for the possibility of
non-termination if the method calls some other method that does not terminate.

Note: `terminates_globally` implies `terminates_locally`.

# `:total`

The `setting` combines the following other assertions:
    - `:consistent`
    - `:effect_free`
    - `:nothrow`
    - `:terminates_globally`
and is a convenient shortcut.

Note: `@assume_effects :total` is similar to `@Base.pure` with the primary
      distinction that the idempotency requirement applies world-age wise rather
      than globally as described above. However, in particular, a method annotated
      `@Base.pure` is always total.

Changes to data structures

• Each CodeInstance gains two sets of four flags corresponding to the notions above (except terminates_locally, which is just a type inference flag). One set of flags tracks IPO-valid information (as determined by inference), the other set of flags tracks optimizer-valid information (as determined after optimization). Otherwise they have identical semantics.

• Method and CodeInfo each gain 5 bit flags corresponding 1:1 to the purity notions defined above. No separate distinction is made between IPO valid and optimizer valid flags here. We might in the future want such a distinction, but I'm hoping to get away without it for now, since the IPO-vs-optimizer distinction is a bit subtle and I don't really want to expose that to the user.

• :foreigncall gains an extra argument (after cconv) to describe the effects of the call.

Algorithm

Relatively straightforward.

• Every call or builtin accumulates its effect information into the current frame.
• Finding an effect (throw/global side effect/non-idempotenct, etc.) taints the entire frame. Idempotency is technically a dataflow property, but that is not modeled here and any non-idempotent intrinsic will taint the idempotency flag, even if it does not contribute to the return value. I don't think that's a huge problem in practice, because currently we only use idempotency if effect-free is also set and in effect-free functions you'd generally expect every statement to contribute to the return value.
• Any backedge taints the termination effect, as does any recursion
• Unknown statements (generic calls, things I haven't gotten around to) taint all effects

TODO

• Constant Evaluation needs to be moved into the correct world age
• Cleanup
• PkgEval

[simeonschaub]

Two quick questions:

Note: The idempontency includes all legal rewrites performed by the optimizizer. For example, floating-point fastmath operations are not considered idempotent, because the optimizer may rewrite them causing the output to not be idempotent, even for the same world age (e.g. because one ran in the interpreter, while the other was optimized).

Does this include code calling back into the optimizer, e.g. via return_type? Might be good to make that explicit in the docs.

:effect_free

The :effect_free setting asserts that the method is free of externally semantically
visible side effects. The following is an incomplete list of externally semantically
visible side effects:

Does :effect_free always imply :nothrow? Since that's technically externally visible IIUC.

[tkf]

The :idempotent setting asserts that for egal inputs:

• The manner of termination (return value, exception, non-termination) will always be the same.
• If the method returns, the results will always be egal.

Note: This in particular implies that the return value of the method must be immutable.

How does one show the implication? A function f defined as

const C = []
f() = C

seems to satisfy the assertions but C is not immutable.

Also, since :idempotent does not mention mutation, I wonder if

const COUNTER = Ref(0)

function g!(arg::RefValue{Int})
    arg[] = COUNTER[] += 1
    return 0
end

is considered :idempotent? Calling g! idempotent is counter-intuitive to me but is it a standard notation for this type of property? Or do I misread the conditions?

[Keno]

Two quick questions:

Note: The idempontency includes all legal rewrites performed by the optimizizer. For example, floating-point fastmath operations are not considered idempotent, because the optimizer may rewrite them causing the output to not be idempotent, even for the same world age (e.g. because one ran in the interpreter, while the other was optimized).

Does this include code calling back into the optimizer, e.g. via return_type? Might be good to make that explicit in the docs.

return_type is considered idempotent whenever its tfunc returns Const. Const also implies IPO safety. It is possible that return_type sometimes violates this, but that's already a soundness bug, c.f.

julia/base/compiler/tfuncs.jl

Lines 1836 to 1838 in 294b0df

	# TODO: this function is a very buggy and poor model of the return_type function
	# since abstract_call_gf_by_type is a very inaccurate model of _method and of typeinf_type,
	# while this assumes that it is an absolutely precise and accurate and exact model of both

:effect_free

The :effect_free setting asserts that the method is free of externally semantically
visible side effects. The following is an incomplete list of externally semantically
visible side effects:

Does :effect_free always imply :nothrow? Since that's technically externally visible IIUC.

No, the thrown value is treated like the return value, I can write that down explicitly.

[Keno]

The :idempotent setting asserts that for egal inputs:

• The manner of termination (return value, exception, non-termination) will always be the same.
• If the method returns, the results will always be egal.

Note: This in particular implies that the return value of the method must be immutable.

How does one show the implication? A function f defined as

const C = []
f() = C

seems to satisfy the assertions but C is not immutable.

You are correct, this is :idempotent - what I meant was that if you allocate a new mutable object, even if the same content, it will not be considered idempotent, because the identity is different. I'll clean up the comment.

Also, since :idempotent does not mention mutation, I wonder if

const COUNTER = Ref(0)

function g!(arg::RefValue{Int})
    arg[] = COUNTER[] += 1
    return 0
end

is considered :idempotent? Calling g! idempotent is counter-intuitive to me but is it a standard notation for this type of property? Or do I misread the conditions?

Yes, it's considered :idempotent, but not :effect_free. Idempotency ignores side effects (in our definition).

[tkf]

In what sense :idempotent relates to the standard usages of idempotent? I can't find any similar usages in https://en.wikipedia.org/wiki/Idempotence.

[Keno]

You're correct. I named these before I had nailed down the exact semantics I wanted. I'll think about a better name, I'm thinking stable might work or maybe something else.

[oscardssmith]

stable seems bad some 3 it has nothing to do with your stability

[tkf]

I think I get why :stable makes sense but I find it a bit less descriptive than the names used for other notions of purity. I wonder if more descriptive names like :returns_same/:returns_egal/:transparent_result/... can work.

[ianatol]

Re :idempotency naming, the definition in base/expr.jl seems a bit like observational equivalence to me. So maybe :obs_equiv?

[Keno]

Re :idempotency naming, the definition in base/expr.jl seems a bit like observational equivalence to me. So maybe :obs_equiv?

Observational equivalence is the definition of the egality property, but here you're not really asserting observational equivalence. There may be observable side effects. Maybe just :preserves_egal? Though there are more conditions than just that - e.g. if it throws, the property requires it to always throw. Other options are :consistent, or :independent (it behaves the same independent of the environment it executes in).

[tkf]

:preserves_egal, :consistent, and :independent all LGTM. I find :independent puzzling at first but then it feels most adequate among them.

BTW, does it also require the thrown exceptions to be egal? I guess not (as not specified)?

[Keno]

BTW, does it also require the thrown exceptions to be egal? I guess not (as not specified)?

It does not. I considered requiring it, but it's usually false. E.g. MethodErrors get freshly allocated every time.

[jonas-schulze]

Just some typos in the docstring

[Keno]

:preserves_egal, :consistent, and :independent all LGTM. I find :independent puzzling at first but then it feels most adequate among them.

I'm gonna go with :state_independent for now, because I think it captures what I mean best: The return/exit behavior is independent of the state of the system.

[Keno]

I'm gonna go with :state_independent for now, because I think it captures what I mean best: The return/exit behavior is independent of the state of the system.

Although actually, now that I'm doing the replacement, I don't like it anymore, since it also says something about optimizer behavior, which doesn't really have anything to do with the state.

[Keno]

Let's go with :consistent then. If I look that up in the dictionary, it says

"unchanging in nature, standard, or effect over time."

which seems like it fits well.

[Keno]

Rebased our everything that got merged independently and squashed the history.

[Keno]

I think this is in a reasonable state now. There's more that could be done with this, but I think this is a pretty good place to pause.