-
-
Notifications
You must be signed in to change notification settings - Fork 5.5k
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.
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
Add devdocs on UB #54099
base: master
Are you sure you want to change the base?
Add devdocs on UB #54099
Changes from 2 commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
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 invocation of the same operation inside of that macro, even on the same values, is 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 perform 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. | ||||||||||||
fingolfin marked this conversation as resolved.
Show resolved
Hide resolved
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. It is perhaps worth a note here that the term "unsafe", when it appears in julia documentation or function names, is typically intended to be interpreted exactly in these terms: of causing UB if any of the arguments do not carefully follow the contract of that function |
||||||||||||
|
||||||||||||
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. | ||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe 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 `@assume_effects` 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 every actually being reached). | ||||||||||||
fingolfin marked this conversation as resolved.
Show resolved
Hide resolved
|
||||||||||||
|
||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
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). There was a problem hiding this comment. Choose a reason for hiding this commentThe 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 There was a problem hiding this comment. Choose a reason for hiding this commentThe 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 mimize impact as a user convenience, but the behavior is not defined. | ||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. "is not defined" -> "it may cause undefined behavior"? Should we try to be consistent in calling it exactly UB, or are various equivalent phrases also acceptable? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
I think equivalent phrases are ok if when it's clear we're talking about Julia-the-language — writing it as the above I think might have helped Matt-from-three-days-ago. |
||||||||||||
- Various modification of global state during precompile. Where possible, this is detected and yields an error, but detection is incomplete. | ||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. We might want to add an asterisk here that the intent is to detect all forms of this in the future, but the current implementation does not? A lemma of this maybe worth adding here is that any observation of mutable state from inside a generated function also will trigger UB (such as accessing a global Dict, or similar other examples that are documented already as forbidden) |
||||||||||||
- 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] | ||||||||||||
fingolfin marked this conversation as resolved.
Show resolved
Hide resolved
|
||||||||||||
- Retention of pointers to GC-tracked objects outside of a `@GC.preserve` region | ||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Observation and retention? E.g.
VS
If we ever want to allow for a moving GC. There was a problem hiding this comment. Choose a reason for hiding this commentThe 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 The other significant behavior of note here is that
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I assume you mean |
||||||||||||
- 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) | ||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. If the memory model has been specified by now, can this link to the definition and #46739 be closed? Also, how should provenance be established for globally constant pointers, e.g. for MMIO-based hardware interactions (e.g. a UART device on a raspberry pi, which lives at a fixed location in memory)? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The memory model is not fully specified, it's been a longstanding item on Jameson's docket.
fingolfin marked this conversation as resolved.
Show resolved
Hide resolved
|
||||||||||||
- Violations of TBAA guarantees (e.g. using `unsafe_wrap`) | ||||||||||||
oscardssmith marked this conversation as resolved.
Show resolved
Hide resolved
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The documentation for
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 | ||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
There was a problem hiding this comment. Choose a reason for hiding this commentThe 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. There was a problem hiding this comment. Choose a reason for hiding this commentThe 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 There was a problem hiding this comment. Choose a reason for hiding this commentThe 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 There was a problem hiding this comment. Choose a reason for hiding this commentThe 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. There was a problem hiding this comment. Choose a reason for hiding this commentThe 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.) | ||||||||||||
Keno marked this conversation as resolved.
Show resolved
Hide resolved
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. ...including overloading key functions such as |
||||||||||||
- 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. | ||||||||||||
fingolfin marked this conversation as resolved.
Show resolved
Hide resolved
|
||||||||||||
|
||||||||||||
## 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`. | ||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think this is referring to cases like 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 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 julia> @enum Foo A=0x0 B C D
julia> reinterpret(Foo, Int32(0xff))
<invalid #255>::Foo = 255 There was a problem hiding this comment. Choose a reason for hiding this commentThe 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). There was a problem hiding this comment. Choose a reason for hiding this commentThe 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 Line 2493 in d8b9810
There was a problem hiding this comment. Choose a reason for hiding this commentThe 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):
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Wait, if it's assured that an undefined There was a problem hiding this comment. Choose a reason for hiding this commentThe 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. | ||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
I think as far as most regular users are concerned, ALL of this information may as well be "as of 1.12" There was a problem hiding this comment. Choose a reason for hiding this commentThe 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
Suggested change
|
||||||||||||
|
||||||||||||
- 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. |
There 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.
There 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.
Should this say parallel executions rather than asynchronous operations? I suppose those are basically the same thing, but we do make a fairly good number of defined behaviors of async calls (memory order for when they start, what random number they start with, etc)