Skip to content

Add devdocs on UB #54099

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Add devdocs on UB #54099

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8a9e249
Add devdocs on UB
Keno Apr 16, 2024
81e6bfd
Apply suggestions from code review
Keno Apr 16, 2024
c2237a5
Apply suggestions from code review
fingolfin May 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions doc/make.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -202,6 +202,7 @@ DevDocs = [
"devdocs/init.md",
"devdocs/ast.md",
"devdocs/types.md",
"devdocs/ub.md",
"devdocs/object.md",
"devdocs/eval.md",
"devdocs/callconv.md",
Expand Down
52 changes: 52 additions & 0 deletions doc/src/devdocs/ub.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
# Undefined Behavior

In programming language design, it is prudent to separate the concepts of a language's semantics, and the behavior of a language's implementation. A language's semantics define the allowable set of *observable* behaviors (including defining what it means to be observable). A correct implementation will ensure that the actual behavior of executing a program has observable behavior that is allowable according to the language semantics. This is often referred to as the **as-if** rule in other languages.

To illustrate the distinction, consider a statement like `print(Ref(1).x)`. The language semantics may specify that the observable behavior of this statement is that the value `1` is printed to `stdout`. However, whether or not the object `Ref` is actually allocated may not be semantically observable (even though it may be implicitly observable by looking at memory use, number of allocations, generated code, etc.). Because of this, the implementation is allowed to replace this statement with `print(1)`, which preserves all semantically observable behaviors.

Additionally, the allowable behaviors for a given program are not unique. For example, the `@fastmath` macro gives wide semantic latitude for floating point math rearrangements and two subsequent invocations of the same operation inside of that macro, even on the same values, are not semantically required to produce the same answer. The situation is similar for asynchronous operations, random number generation, etc.

*Undefined Behavior* (UB) occurs when a julia program semantically performs an operation that is assumed to never happen. In such a situation, the language semantics do not constrain the behavior of the implementation, so any behavior of the program is allowable, including crashes, memory corruption, incorrect behavior, etc. As such, it is very important to avoid writing programs that semantically execute undefined behavior.

Note that this explicitly applies to *semantically executed* undefined behavior. While julia's compiler is allowed to and does aggressively perform speculative execution of pure functions. Since the execution point is not semantically observable (though again indirectly observable through execution performance), this is allowable by the as-if rule. As such, speculative execution is inhibited unless the code in question is proven to be
free of undefined behavior.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Technically, I think we only require (and implement) the slightly weaker form that it does not execute the undefined behavior, not that it is entire free of it (basically what the first point said of the runtime, but reiterated from the perspective of the compiler calling speculating the call)


The presence of undefined behavior is modeled as part of julia's effect system using the `:noub` effect bit. See the documentation for [`Base.@assume_effects`](@ref) for more information on querying the compiler's effect model or overriding it for specific situations (e.g. where a dynamic check precludes potential UB from ever actually being reached).

Copy link
Member

@LilithHafner LilithHafner Apr 18, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
While the language semantics do allow, for example, formatting your hard drive if you redefine a const, we nevertheless try to make the behavior of the `julia` executable reasonable and user friendly wherever possible. Even in the presence of undefined behavior, we make an effort—though not always a successful one—to produce intuitive and predictable results.

In the spirit of @mbauman's comments, I'd like to amend "we can't promise anything" to "we can't promise anything, but we'll still try to be nice if we can". No semantic change, just a friendly reminder that we're all on the same team trying to make user experience better. This also documents an effort we already do make (c.f. the constant redefinition example which works pretty well in practice).

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

if for no other reason than to avoid SEO-association of "ransomware" with "Julia", I might use another description

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Switched to the less extreme, more canonical "format your hard drive" example.

## List of sources of undefined behavior

The following is a list of sources of undefined behavior,
though it should currently not be considered exhaustive:

- Replacement of `const` values. Note that in interactive mode the compiler will issue a warning for this and some care is taken to minimize the impact as a user convenience, but the behavior is not defined.
- Various modifications of global state during precompile. Where possible, this is detected and yields an error, but detection is incomplete.
- Incorrect implementation of a `Core.OptimizedGenerics` interface [1]
- Any invocation of undefined behavior in FFI code (e.g. `ccall`, `llvmcall`) according to the semantics of the respective language
- Incorrect signature types in `ccall` or `cfunction`, even if those signatures happen to yield the correct ABI on a particular platform
- Incorrect use of annotations like `@inbounds`, `@assume_effects` in violation of their requirements [^1]
- Retention of pointers to GC-tracked objects outside of a `@GC.preserve` region
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Observation and retention?

E.g.

GC.@preserve x begin
    p = Base.pointer_from_objref(x)
end

VS

p1 = Base.pointer_from_objref(x) # UB
GC.@preserve x begin
    p2 = Base.pointer_from_objref(x)
    @assert p1 == p2 # May not be true.
end

If we ever want to allow for a moving GC.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Retention may be okay, since I am not certain the GC implements that anyways. In particular, if the only use of an object is ===, and we turn that into a pointer equality check later, does GC rooting know to preserve that pointer?

The other significant behavior of note here is that unsafe_pointer_from_objref does not "recover" the GC-tracked safety property, such that this is UB code as well, in all its forms, since the Base.pointer_from_objref(x) is allowed to escape the preserve region (via Base.unsafe_pointer_from_objref), which is not permitted:

x = GC.@preserve x Base.unsafe_pointer_from_objref(Base.pointer_from_objref(x))

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I assume you mean unsafe_pointer_to_objref

- Memory modification of GC-tracked objects without appropriate write barriers from outside of julia (e.g. in native calls, debuggers, etc.)
- Violations of the memory model using `unsafe_` operations (e.g. `unsafe_load` of an invalid pointer, pointer provenance violations, etc)
- Violations of TBAA guarantees (e.g. using `unsafe_wrap`)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The documentation for unsafe_store! says this:

Unlike C, storing memory region allocated as different type may be valid provided that that the types are compatible.

What does "compatible" mean there? Also, could that be documented here?

- Mutation of data promised to be immutable (e.g. in `Base.StringVector`)
- Data races
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
- Data races
- Data races, although some limits are still placed upon the allowable behavior, per the memory model.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems very vague to me, to the point of not really being helpful 🤔 Even Rust doesn't give more justification to data races being UB other than calling them out for being UB.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Rust puts a limit that data races therefore are impossible because they would be UB if possible. Ours is closer to the Java memory model: while they are possible, they are not full UB, since we do define some limits on their (mis)behaviors

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hm.. It's pretty easy to construct data races that result in UB though, e.g. with a function that vectorizes a loop over a Vector while simultaneously push!ing to that vector from another task. The reallocation results in OOB reads (and possibly writes) once the original Memory is GCed.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It cannot be GCd while there remains a reference to the Memory. The question there is whether we force MemoryRef to always use double-word atomic relaxed loads and stores to make sure even the concurrent update is safe. Otherwise you could get a partially torn read/write there currently.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

And because Array uses inbounds annotations internally, it is already covered by that bullet point on the correctness of that

- Modification of julia-internal mutable state (e.g. task schedulers, data types, etc.)
Copy link
Member

@vtjnash vtjnash Apr 16, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

...including overloading key functions such as getproperty(::Type{T}, ...), or show(io::IO, ::Type{T}) 😅

- A value other than `false` (`reinterpret(UInt8, b) == 0x00`) or `true` (`reinterpret(UInt8, b) == 0x01`) for a `Bool` `b`.
- Invoking undefined behavior via compiler intrinsics.

[^1] Incorrect use here may be UB, even if not semantically executed, please see the specific documentation of the feature.

## Implementation-defined behavior
Some behavior is technically forbidden by the semantics of the language, but required in certain parts of the implementation and thus allowed as long as implementation-defined constraints are obeyed. Nevertheless, these constructs should be avoided when possible, as the implementation-defined constraints may not be stable across julia versions.

- Construction of objects using `eval(Expr(:new))` rather than their constructors

## Special cases explicitly NOT undefined behavior

- As of Julia 1.11, access to undefined bits types is no longer undefined behavior. It is still allowed to return an arbitrary value of the bits type, but the value returned must be the same for every access and use thereof is not undefined behavior. In LLVM terminology, the value is `freeze undef`, not `undef`.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is referring to cases like x = Ref{Int}(); println(x[]), right? Does this imply that e.g. padding can be assumed to be constant too?

Moreover, not all bitpatterns are necessarily valid values of the bitstype - e.g. a type such as

struct MaskedByte
    byte::UInt8
    MaskedByte(b::UInt8) = new(b & 0x0f)
end

doesn't have the same valid bitpatterns as UInt8, so Ref{MaskedByte}()[] can't guarantee to produce an arbitrary (valid) value of that type without going through the constructor:

julia> reinterpret(UInt8, Ref{MaskedByte}()[])
0x70

It's infeasible to guarantee calling a constructor for such uses though, so maybe the values produced like that (if not undefined) should have their own name? This would of course also cover invalid values of @enum, which currently uses the term invalid for this:

julia> @enum Foo A=0x0 B C D

julia> reinterpret(Foo, Int32(0xff))
<invalid #255>::Foo = 255

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Accessing padding is UB, as mentioned in the other comment. Violating inner constructor constraints for bits types is currently not UB or even disallowed, although I would like to clamp down on that in the future (by adding a bit in the type that disallows this).

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you remember when this change was implemented? It might mean we are now able to remove the check at

julia/base/compiler/tfuncs.jl

Line 2493 in d8b9810

if !(length(argtypes) ≥ 2 && getfield_notundefined(obj, argtypes[2]))

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, you're right, that should be removable. We already taint the consistency when allocating the object, so there is no longer any UB with accessing an object (since #52169 in November):

julia> struct A; b::Int; A() = new(); end
julia> Base.infer_effects(()) do; A(); end
(!c,+e,+n,+t,+s,+m,+u)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wait, if it's assured that an undefined isbitstype-field consistently returns the same value, shouldn't those allocations also be considered :consistent, unless they are mutable?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A specific, known allocation always returns the same value when observed, but a specific call / allocation site does not


- As of Julia 1.12, loops that do not make forward progress are no longer considered undefined behavior.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
- As of Julia 1.12, loops that do not make forward progress are no longer considered undefined behavior.
+ Loops that do not make forward progress are not considered undefined behavior.

I think as far as most regular users are concerned, ALL of this information may as well be "as of 1.12"

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I get what you're saying, but this is still valuable. Perhaps they could be expressed with !!! compats.

Suggested change
- As of Julia 1.12, loops that do not make forward progress are no longer considered undefined behavior.
!!! compat "Julia 1.12"
Loops that do not make forward progress are no longer considered undefined behavior.


- Signed integer overflow is not undefined behavior. See also the manual section on [Overflow Behavior](https://docs.julialang.org/en/v1/manual/integers-and-floating-point-numbers/#Overflow-behavior).

- Revival of objects inside finalizers is permitted though discouraged.