Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Take purity modeling seriously (#43852)
* Implement new effect system
* 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 `:foreigncall`s. 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.
** `:idempotent`
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. 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:
- `:idempotent`
- `: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
* Make INV_2PI a tuple
Without this, the compiler cannot assume that the range reduction
is idempotent to make use of the new fast constprop code path.
In the future this could potentially be an ImmutableArray, but
since this is relatively small, a tuple is probably fine.
* Evalute :total function in the proper world
* Finish effects implementation for ccall
* Add missing `esc`
* Actually make use of terminates_locally override
* Mark ^(x::Float64, n::Integer) as locally terminating
* Shove effects into calling convention field
* Make inbounds taint consistency
Inbounds and `--check-bounds=no` basically make the assertion:
If this is dynamically reached during exceution then the index
will be inbounds. However, effects on a function are a stronger
statement. In particular, for *any* input values (not just the
dynamically reached ones), the effects need to hold. This is
in particular true, because inference can run functions that
are dynamically dead, e.g.
```
if unknown_bool_return() # false at runtime, but inference doesn't know
x = sin(1.0)
end
```
Inference will (and we want it to) run the `sin(1.0)` even
though it is not dynamically reached.
For the moment, make any use of `--check-bounds=no` or `@inbounds`
taint the consistency effect, which is semantically meaningful and
prevents inference from running the function. In the future, we
may want more precise tracking of inbounds that would let us
recover some precision here.
* Allow constprop to refine effects
* Properly taint unknown call in apply
* Add NEWS and doc anchor
* Correct effect modeling for arraysize
* Address Shuhei's review
* Fix regression on inference time benchmark
The issue wasn't actually the changes here, they just added additional
error paths which bridged inference into the Base printing code, which
as usual takes a fairly long time to infer. Add some judicious barriers
and nospecialize statements to bring inference time back down.
* refine docstrings of `@assume_effects`
This commit tries to render the docstring of `@assume_effects` within
Documenter.jl-generated HTML:
- render bullet points
- codify the names of settings
- use math syntax
- use note admonitions
* improve effect analysis on allocation
Improves `:nothrow` assertion for mutable allocations.
Also adds missing `IR_FLAG_EFFECT_FREE` flagging for non-inlined callees
in `handle_single_case!` so that we can do more dead code elimination.
* address some reviews
* Address Jameson's review feedback
* Fix tests - address rebase issues
Co-authored-by: Shuhei Kadowaki <aviatesk@gmail.com>- Loading branch information
f090992There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@nanosoldier
runbenchmarks(ALL, isdaily = true)f090992There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@nanosoldier
runbenchmarks(ALL, isdaily = true)