RFC: Effect Preconditions - or - the future of @inbounds

[Keno]

This proposal is an attempt to tie together some of the recent discussion around the future of @inbounds, formal interface checking (a long the lines of my proposal in https://github.com/Keno/InterfaceSpecs.jl), and --check-bounds.

Reviewing @inbounds

History

The @inbounds annotation has been in the langauge for a decade at this point [1]. It is a crictical tool to achieve machine performance in high-performance applications where the overhead of boundschecking is prohibitive [2]. At the same time, as Julia has matured, the dangers of this macro have become more clear. It is essentially impossible to use correctly in generic code and instances where code (including code in base from before we were culturally more careful about inbounds) are using @inbounds have become a not-uncommon complaint-point about the language as a whole [3]. In current practice, at least in Base, we have become extremely hesitant about the introduction of new @inbounds annotations (see e.g. discussion in #41200). At the same time, the ability to disable bounds checking remains a critical capability for several of our user communities (c.f. #50239 and related discussions). So how do we move forward here? I'm hoping we can find a way forward that achieves the same benefits of @inbounds but in a way where it is possible to re-establish soundness if desired.

When is inbounds still required?

LLVM's current capabilities

Let's look at a couple of examples. First:

function sum1(A::Vector{Int64})
	a = zero(eltype(A))
	for i in eachindex(A)
		a += A[i]
	end
	return a
end

Is inbounds required here in modern julia? The answer is no - LLVM's range analysis proves that the bounds check is dead and eliminates it. (The same holds true for the 1:length(A) version, although this was not always true).

What about the following:

function sum2(A::Vector{Int64}, B::Vector{Int64})
	a = zero(eltype(A))
	for i in eachindex(A, B)
		a += A[i] + B[i]
	end
	return a
end

Here, LLVM is again able to eliminate the boundscheck, though of course the eachindex introduces an additional check that the array shapes are compatible. Even this is still ok-ish:

# Noinline here just for illustration, think some big internal function that is
# not inlineable.
@noinline function sum_partial(A::Vector{Int64}, upto::Int)
	a = zero(eltype(A))
	for i in 1:upto
		a += A[i]
	end
	return a
end
sum3(A::Vector{Int64}) = sum_partial(A, length(A))

The generated code here runs through the loop. LLVM's vectorizer has support for bounds-like checks and can remove them from the vector body. However, in scalar code (e.g. Float64 without fastmath), LLVM does still perform the bounds check in every loop iteration rather than hoisting it outside. This is probably a bug somewhere. The IRCE pass is supposed to take care of this, so for the present purposes, let's assume that this will also go through eventually.

That said, the takeaway here is that, for simple cases, where everything is inlined, LLVM is reasonably powerful at eliminating these checks.

The effect-separation trick

Let's consider a case like this

function repeat_outer(a::AbstractMatrix, (m,n)::NTuple{2, Any})
    o, p = size(a,1), size(a,2)
    b = similar(a, o*m, p*n)
    for j=1:n
        d = (j-1)*p+1
        R = d:d+p-1
        for i=1:m
            c = (i-1)*o+1
            b[c:c+o-1, R] = a
        end
    end
    return b
end

The setindex! call in here goes through a few layers of dispatch, but eventually ends up at:

function _setindex!(l::IndexStyle, A::AbstractArray, x, I::Union{Real, AbstractArray}...)
    @inline
    @boundscheck checkbounds(A, I...)
    _unsafe_setindex!(l, _maybe_reshape(l, A, I...), x, I...)
    A
end

This is a very common pattern in our code, where we have an @inline function that first checks for the in-boundedness and then performs an unsafe operation that assumes everything is inbounds.

This pattern is quite good. By allowing the boundscheck itself to be inlined, LLVM can eliminate the boundscheck using local context from the calling function (in theory at least - in practice we still have an @inbounds there because LLVM isn't strong enough currently).

However, the pattern is somewhat hard to use consistently and correctly, so we generally only use it in the low level indexing code.

Effect-precondition synthesis

@inbounds motivations

In the previous section I said that the effect-separation was good but hard to do consistently and correctly. So can we have the compiler implement this for us. Suppose we had a macro @hoist_boundschecks that worked something like the following:

function _setindex!(l::IndexStyle, A::AbstractArray, x, I::Union{Real, AbstractArray}...)
    @inline
    @hoist_boundscheck _safe_setindex!(l, _maybe_reshape(l, A, I...), x, I...)
    A
end
# = Expands to =#
function _setindex!(l::IndexStyle, A::AbstractArray, x, I::Union{Real, AbstractArray}...)
    @inline
    #= All the boundschecks from _safe_setindex! hoisted =# checkbounds(A, I...)
    #= Switched to unsafe_setindex, but now proven correct =#
    _unsafe_setindex!(l, _maybe_reshape(l, A, I...), x, I...)
    A
end

Where essentially what the macro would do is go through the _safe_setindex! call and synthesize a check that ensures that all calls are inbounds. Of course such a synthesis is not always possible in general, but it's not that hard for simple cases (a trivial way to do it is to duplicate the function, delete all the side effects other than throwing boundserrors and then let LLVM go to town on it).

Generalizing

There is a few problems with the macro as suggested in the previous section. In particular, it changes the ordering of side effects and errors in the function, which may be desirable, but I would like have explicit control over. My proposal is to have a slight generalization of it that works roughly as follows:

function foo(A, I)
	@split_effects :nothrow bar(A, I)
end
#= Expands to =#
function foo(A, I)
	if precondition(Val{:nothrow}(), bar, A, I)
		@assume_effects :nothrow bar(A, I)
	else
		bar(A, I)
	end
end

Where precondition like the proposed macro above is some synthesized predicate that ensures that the resulting function does not throw. Of course this brings up many questions, such as the implementation of precondition and the statement-position @assume_effects, which we currently don't have, but let's explore the implications of this a bit further.

Precondition inference and composition

The question of coming up with these kinds of preconditions is a well-known problem in the compiler literature. The term to look for is "weakest precondition synthesis". How exactly do this best is somewhat outside the scope of this writeup, but I do want to highlight a the primary property that suggests the idea: functional composition of functions is boolean composition of preconditions:

function foo()
	bar()
	baz()
end

precondition(n::Val{:nothrow}, foo) = precondition(n, bar) && precondition(n, baz)

Also, if a function uses the @split_effects macro internally, then an outside @assume_effects can cause the precondition to be assumed to be true. This mirrors the @inbounds/@boundscheck interaction we have right now, but with an alternative that is provably safe.

Extensions to @assume_effects

So far, we have assumed that these preconditions are synthesized automatically, but getting this to work well, of course depends on the synthesis strength of the compiler. To still allow users to take advantage of this mechanism, even if the compiler's synthesis is not strong enough, we can extend @assume_effects to allow conditional effects:

@assume_effects (checkbounds(false, A, I) && :nothrow) setindex!(A, I)
	_safe_setindex!(A, I)
end

The idea here is that precondition is overriden by checkbounds(false, A, I), so any @split_effects of this function would use the checkbounds function for its check and if this returned true, could @assume_effects :nothrow this function, which as described above would allow the use of the unsafe function in the interior.

Call-site @assume_effects and effects-assumption specialization

In the foregoing we have, in a few places, used a call-site @assume_effects, without defining what it does. The idea here is pretty simple: We add a new specializaiton axis based on effects assumption. For example, if a function is @assume_effects :nothrow, then at codegen time, any path that throws an error (in particular bounds checks) becomes undefined behavior and LLVM is allowed to assume that it does not happen. Of course, this is macro is extremely dangerous (as the existing @assume_effects and @inbounds are).

However, one significant benefit of this design is that there is a very clear notion of what the assertion promises. This is not necessarily clear of @inbounds, which we did not give semantics beyond it's effect on the @boundscheck macro. As a result, even an infinitely-powerful prover could not check the correctness or non-correctness of @inbounds (as currenlty used - we could of course consider an alternative @inbounds design with stronger semantics). In contrast, the formal meaning of a conditional @assume_effects is well defined and could in principle be checked by a tool (#49273).

Implications for --check-bounds

In the whole, --check-bounds removal discussion, we had assumed that we did not want to keep two copies of all code just for the purposes of --check-bounds which thus required us disable constant propagation. However, in this proposal, the @assume_effects specialization is exactly such a copy set and could thus be used for this purpose. That said, this proposal would also hopefully provide a much stronger system for boundscheck removal that would allow us to make --check-bounds much less necessary.

Other uses

There are a few other places where domain checks can interfere with optimization. For exmaple, consider the following situation:

function sin_loop(n)
	for i = 1:n
		# Imagine there was a whole bunch of other code here that used this value,
		# but all that got DCE'd, but we can't in general DCE `sin`, because it
		# may throw.
		sin(Float64(i))
	end
end

julia> @time sin_loop(1_000_000_000)
 20.383584 seconds

With the support in this PR, we can:

# The actual condition here is `!isinf`, but we're allowed to overapproximate and
# LLVM can handle `isfinite` better.
# TODO: In a more complete version of this PR, this precondition would be synthesized
@Base.assume_effects (isfinite(x) && :nothrow) @noinline function mysin(x::Float64)
	sin(x)
end

function sin_loop_split(n)
	for i = 1:n
		Core.invoke_split_effects(:nothrow, mysin, Float64(i))
	end
end

julia> @code_llvm sin_loop_split(1_000_000_000)
;  @ REPL[19]:1 within `sin_loop_split`
define void @julia_sin_loop_split_428(i64 signext %"n::Int64") #0 {
top:
;  @ REPL[19]:4 within `sin_loop_split`
  ret void
}

julia> @time sin_loop_split(1_000_000_000)
  0.000000 seconds

Current status of this PR

This PR contains a complete sketch of this mechanism, including inference support for the new intrinsic, as well as codegen and runtime support for effect-assumption specialization. It also includes an (extremely incomplete) sketch of the supporting macros. It does not implement any precondition synthesis logic. My plan is to support synthesis for some of the simple @inbounds cases in Base, but then delagate fancier synthesis support for packages, since that can get arbitrarily complicated.

Implementation Plan

This PR itself is not suitable for merging, but if people like this direction, I would like to get the basic pieces in in relatively short order. To that end, I would suggest the following order of implementation as separate PRs once we've agreed on the overall plan:

1. New intrinsics, Method(Instance) fields, inference support
2. @assume_effects extensions
3. Codegen and specialization support, Code(Instance) fields
4. Basic Synthesis and @inbounds removal

[1] Introduced in 66ab577 for julia 0.2 [2] Note that it's usually not the boundschecking itself that is the problem,
but rather that the presence of the boundschecking inhibits other optimizations.
[3] E.g. https://yuri.is/not-julia/

[Seelengrab]

Thank you for the concrete proposal!

You mention that any incorrect use of @assume_effects is of course undefined behavior, and that the compiler is free to "optimize" this by removing the offending code, in an effort to make more programs accepted by the compiler. How, if at all, are users of @assume_effects notified of such a removal/optimization? I think in quite a lot of cases, people use this mechanism because they actually want the compiler to already be able to prove the asserted effects on its own, but for various reasons it might not be able to do so. It'd be a shame if people were to use the macro, and the compiler going "actually, just let me delete the code to make it conform to your contract" without notifying the user of that.

[Keno]

How, if at all, are users of @assume_effects notified of such a removal/optimization?

They're not.

I think in quite a lot of cases, people use this mechanism because they actually want the compiler to already be able to prove the asserted effects on its own, but for various reasons it might not be able to do so.

Yes, which is why it's a big problem when people get it wrong. The hope is that we could leverage tooling from the formal methods world to figure out when people got the annotations wrong to tell them about it (potentially by using significant amounts of compute in excess of what we would consider reasonable for the base compiler). #49273

Also, just to be clear, the hope here is that the automatic synthesis in Base would be sufficient to cover 90% of current uses of @inbounds, with the conditional assume effects, being required only very rarely.

[Seelengrab]

How good are the chances that such formal method proving techniques can distinguish cases of "the compiler is unable to prove it, but the use of the macro is sound" from "the compiler has proven the contraposition"? I.e., what's our target ratio of false positives?

To be clear, I'm personally in the camp of "have the compiler scream loudly at me" whenever it can notice that it thinks I've done something wrong (because the intention is usually to get some static guarantee that the code is relying on for correctness), but then again, I also don't tend to use @assume_effects because it's very easy to make human mistakes when using it.

[jakobnissen]

Thank you for such a well-thought out proposal. Even as I'm not qualified to understand all the implications of this proposal, it's clear that a macro like @assume_effects condition :effect expr will be a very useful addition to Julia.

However, I'm a bit worried about that the macro is even harder to use correctly than @inbounds is. In order to use @inbounds with my function f correctly, all I need to understand is the indexing that happens in f. Usually, that's easy enough. However, to use @assume_effects cond && :nothrow, I need to know all ways that f can terminate, including all the callees of f, and especially including all their edge cases, which is much harder. For example, I had no idea that sin(::Float64) in your example could throw.

Hence, I'm a bit worried that if the motivation for this new macro is to make user code more robust by recommending the new macro over @inbounds, then I worry the result would be even more buggy user code and more dangerous behaviour.

[Keno]

However, I'm a bit worried about that the macro is even harder to use correctly than @inbounds is.

Yes, it is unquestionably harder to use, because it is a stronger assertion.

In order to use @inbounds with my function f correctly, all I need to understand is the indexing that happens in f. Usually, that's easy enough.

Well, perhaps. The conditional @assume_effects is a replacement for the @boundscheck/@inbounds pattern, which has much of the same problem of having to understand a fairly abstract domain. It is true that @assume_effects :nothrow is broader than that, because it includes all errors, not just bounds errors, but there's no issue with just increasing the granularity to have @assume_effects :nobounds.

In particular, the replacement for call-site @inbounds from the user-perspective will generally be effect splitting, which is always safe.

Hence, I'm a bit worried that if the motivation for this new macro is to make user code more robust by recommending the new macro over @inbounds, then I worry the result would be even more buggy user code and more dangerous behaviour.

The hope is that the @assume_effects macro will be largely unnecessary since the compiler should be able to automatically synthesize in common cases. I'd also be in favor of a policy that requires all uses of @assume_effects in base and important packages to come with a formal correctness proof (#49273), which of course requires more tooling than we currently have, but I think that tooling can be built.

[vtjnash]

However, in this proposal, the @assume_effects specialization is exactly such a copy set and could thus be used for this purpose.

With --check-bounds=no, my understanding is that the split effect would be an unconditional true and the (still invalid) code. That is, as defined now, this does not help recover valid behavior (or inference) from code that has been changed to have undefined behavior by the flag. We can instead change the meaning of the flag not to introduce undefined behavior into previously valid Julia code (e.g. deprecate it so that it no longer introduces issues into code), but I don't see how we can both define that boundschecks are hard-coded to true and guaranteed to be skipped (not hoisted), but also that they can be relied upon to run when called.

That aside, I do like the proposal.

Since you mention the general literature on pre-conditions, how does this compare to having generalized pre-condition and post-condition guards (e.g. pre and post dispatch function call MethodTables), with explicit options to hoist/reorder those?

Lastly, what prevents inference of effects from becoming undecidable when you allow the user to hoist effects? For example, with code like this:

@inline function g()
    inferencebarrier(throw)()
    @hoist_boundscheck h()
end

Is it permitted to hoist side-effects from the boundscheck in h into the caller, by inventing values that cannot originally have existed at runtime, due to the uninferred throw (or other sort of branch / return that couldn't be evaluated precisely). Since this seems that it may break monotonicity of inference, what is possible to conclude from dataflow-inference when the optimizer is no longer is expected to preserve the dataflow? If it is legal to hoist errors, can I legally convert all code into error("nasal demon infection"), since you can't prove that wasn't going to be the next statement after the return call was reached in a different abstract interpretation session of the same code.

[Keno]

With --check-bounds=no, my understanding is that the split effect would be an unconditional true and the (still invalid) code. That is, as defined now, this does not help recover valid behavior (or inference) from code that has been changed to have undefined behavior by the flag. We can instead change the meaning of the flag not to introduce undefined behavior into previously valid Julia code (e.g. deprecate it so that it no longer introduces issues into code), but I don't see how we can both define that boundschecks are hard-coded to true and guaranteed to be skipped (not hoisted), but also that they can be relied upon to run when called.

The comment on --check-bounds was that the flag could change the runtime dispatch to always prefer the nothrow-specialized versions (assuming a sufficiently precise version of nothrow that only covers the bounds checks of interest) at runtime, but still allow the compiler to use the version without assumptions for constprop etc. I don't think it's a particularly good solution for this issue and I prefer #50239, but I wanted to note the connection.

Since you mention the general literature on pre-conditions, how does this compare to having generalized pre-condition and post-condition guards (e.g. pre and post dispatch function call MethodTables), with explicit options to hoist/reorder those?

The question is what do those pre-conditions guard. In a static system, you would prevent people from calling functions that don't have their preconditions satisfied. You could imagine a system where the preconditions/postconditions are semantically enforced dynamically and called everytime you enter or leave a function, but that would be a pretty different feature. The hope here is that the majority of preconditions would be compiler-enforced.

Is it permitted to hoist side-effects from the boundscheck

Preconditions are required to be :foldable, so in particular side-effect free.