effects: separate `:noub` effect bit from `:consistent` #50808

aviatesk · 2023-08-06T04:12:49Z

The current :consistent effect bit carries dual meanings:

"the return value is always consistent"
"this method does not cause any undefined behavior".

This design makes the effect bit unclear and hard to manage. Specifically, the current design prevents a post-inference analysis (as discussed in #50805) from safely refining "consistent"-cy using post-optimization state IR. This is because it is impossible to tell whether the :consistent-cy has been tainted by the first or second meaning.

To address this, this commit splits them into two distinct effect bits: :consistent for consistent return values and :noub for no undefined behavior.

This commit also introduces an override mechanism for :noub as it is necessary for @assume_effects to concrete-evaluate the annotated methods. While this might sound risky and not in line with the existing designs of :nonoverlayed and :noinbounds, where their overrides are prohibited, but we already have an override mechanism in place for :consistent, which implicitly overrides :noub. Given this precedent, the override for :noub should probably be justified.

@nanosoldier runbenchmarks("inference", vs=":master")

aviatesk · 2023-08-06T04:39:36Z

base/compiler/abstractinterpretation.jl

            # function that uses `@inbounds`. However, if this `:boundscheck` is itself within an
            # `@inbounds` region, its value depends on `--check-bounds`, so we need to taint
-            # `:consistent`-cy here also.
+            # `:noub`-cy here also.


Just took another look at this comment, and it got me wondering. Why are we checking if the current statement is inside the @inbounds region and then tainting it with :noub? Isn't necessary now as we separate caches based on --check-bounds?

Also, if we do need to taint it, probably we should taint :consistent instead?

nanosoldier · 2023-08-06T05:05:37Z

Your benchmark job has completed - possible performance regressions were detected. A full report can be found here.

Keno · 2023-08-06T06:30:43Z

test/compiler/effects.jl

@@ -346,7 +346,7 @@ function A1_inbounds()
    end
    return r
 end
-@test !Core.Compiler.is_consistent(Base.infer_effects(A1_inbounds))
+@test !Core.Compiler.is_noub(Base.infer_effects(A1_inbounds))


No, this should taint consistent. :boundscheck is still inconsistent, but getfield with boundscheck off (or unknown) taints ub.

Well, could you tell me why we even need to taint :consistent and/or :noub at all? As far as I understand, it would be fine if only :noinbounds is tainted, as the @inbounds does not have any effect on the @boundscheck (, which syntactically appears within the @inbounds block).

It still has an effect of check-bounds=yes is used, so in the current design :bounds check always needs to taint consistent. Of course with the path dependency I'm adding in the other PR, we may recover consistency for the whole function, but locally, it's inconsistent

It still has an effect of check-bounds=yes is used, so in the current design :bounds check always needs to taint consistent.

Could you please elaborate this please? When --check-bounds=[yes|no] is specified, aren't :boundscheck regarded as consistent (and thus can be inferred to return Const([true|false]))? I guess your concern is that sysimage is not separated by the flag?

Yes, that's right. In the current design there's no guarantee that the inference check-bounds matches the runtime check-bounds, so we can't use it for IPO. We may change things around there in the near future, but for the time being that needs to be the semantics.

Shouldn't we taint :consistent whenever we see :boundscheck except the special cased getfield call then?

vtjnash · 2023-08-08T00:23:46Z

Can we call this speculatable, which I think is the existing LLVM name for this property? The current name is both a negative and an acronym, which reduces readability.

Keno · 2023-08-08T05:42:12Z

speculatable also includes :effect_free. in general, I'm in favor of naming things the way you would explain them, and in this case I would explain this as "this promises that the function does not exhibit undefined behavior for any arguments". Undefined Behavior is a term of art that I think is important to preserve in the name here.

oscardssmith · 2023-08-08T12:48:02Z

what about defined? That is a fairly simple description of what we require (nothing that's undefined)

vtjnash · 2023-08-08T13:14:30Z

Or safe?

Keno · 2023-08-10T05:40:10Z

I don't like defined, because we already use that term for isdefined, which is something completely different. safe is ok, but also very non-specific. Does it really make sense that f() = run(`rm -rf /`) is safe?

vtjnash · 2023-08-10T12:32:43Z

It would be somewhat more specific in that it is a property of effect.safe, not just a bare keyword

stdlib/REPL/test/replcompletions.jl

oscardssmith · 2023-08-18T20:14:56Z

we have agreement between Jeff and Jameson on the noub name.

The current `:consistent` effect bit carries dual meanings: 1. "the return value is always consistent" 2. "this method does not cause any undefined behavior". This design makes the effect bit unclear and hard to manage. Specifically, the current design prevents a post-inference analysis (as discussed in #50805) from safely refining `:consistent`-cy using post-optimization state IR. This is because it is impossible to tell whether the `:consistent`-cy has been tainted by the first or second meaning. To address this, this commit splits them into two distinct effect bits: `:consistent` for consistent return values and `:noub` for no undefined behavior. This commit also introduces an override mechanism for `:noub` as it is necessary for `@assume_effects` to concrete-evaluate the annotated methods. While this might sound risky and not in line with the existing designs of `:nonoverlayed` and `:noinbounds`, where their overrides are prohibited, but we already have an override mechanism in place for `:consistent`, which implicitly overrides `:noub`. Given this precedent, the override for `:noub` should probably be justified.

aviatesk requested a review from Keno August 6, 2023 04:12

aviatesk force-pushed the avi/noub branch from d1d8ae6 to 79aedf8 Compare August 6, 2023 04:30

aviatesk commented Aug 6, 2023

View reviewed changes

Keno reviewed Aug 6, 2023

View reviewed changes

brenhinkeller added the compiler:effects effect analysis label Aug 6, 2023

aviatesk force-pushed the avi/noub branch 2 times, most recently from 19a82ef to 7938f7e Compare August 17, 2023 02:46

aviatesk commented Aug 17, 2023

View reviewed changes

stdlib/REPL/test/replcompletions.jl Outdated Show resolved Hide resolved

aviatesk force-pushed the avi/noub branch 2 times, most recently from ef8fb69 to 36fc4d9 Compare August 17, 2023 23:16

Keno approved these changes Aug 18, 2023

View reviewed changes

aviatesk force-pushed the avi/noub branch from 36fc4d9 to 6b6334a Compare August 19, 2023 07:52

oscardssmith merged commit 0d544cc into master Aug 19, 2023

oscardssmith deleted the avi/noub branch August 19, 2023 15:47

vtjnash mentioned this pull request Aug 16, 2024

f_boundscheck_elim tests passes, for the wrong reason #49107

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

effects: separate `:noub` effect bit from `:consistent` #50808

effects: separate `:noub` effect bit from `:consistent` #50808

aviatesk commented Aug 6, 2023 •

edited

Loading

aviatesk Aug 6, 2023 •

edited

Loading

nanosoldier commented Aug 6, 2023

Keno Aug 6, 2023

aviatesk Aug 7, 2023

Keno Aug 7, 2023

aviatesk Aug 7, 2023

Keno Aug 7, 2023

aviatesk Aug 17, 2023

vtjnash commented Aug 8, 2023

Keno commented Aug 8, 2023

oscardssmith commented Aug 8, 2023

vtjnash commented Aug 8, 2023

Keno commented Aug 10, 2023

vtjnash commented Aug 10, 2023

oscardssmith commented Aug 18, 2023

effects: separate :noub effect bit from :consistent #50808

effects: separate :noub effect bit from :consistent #50808

Conversation

aviatesk commented Aug 6, 2023 • edited Loading

aviatesk Aug 6, 2023 • edited Loading

Choose a reason for hiding this comment

nanosoldier commented Aug 6, 2023

Keno Aug 6, 2023

Choose a reason for hiding this comment

aviatesk Aug 7, 2023

Choose a reason for hiding this comment

Keno Aug 7, 2023

Choose a reason for hiding this comment

aviatesk Aug 7, 2023

Choose a reason for hiding this comment

Keno Aug 7, 2023

Choose a reason for hiding this comment

aviatesk Aug 17, 2023

Choose a reason for hiding this comment

vtjnash commented Aug 8, 2023

Keno commented Aug 8, 2023

oscardssmith commented Aug 8, 2023

vtjnash commented Aug 8, 2023

Keno commented Aug 10, 2023

vtjnash commented Aug 10, 2023

oscardssmith commented Aug 18, 2023

effects: separate `:noub` effect bit from `:consistent` #50808

effects: separate `:noub` effect bit from `:consistent` #50808

aviatesk commented Aug 6, 2023 •

edited

Loading

aviatesk Aug 6, 2023 •

edited

Loading