-
-
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
Conversation
This adds some basic devdocs for undefined behavior, since there keep being complaints that it's not written down anywhere. The list of UB is just what I remembered off the top of my head, it's probably incomplete, since we haven't historically been particularly careful about this. This way, at least when people add new sources of UB, they'll have a centralized place to write that down.
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.
Thank you for writing this down! I've added some comments/fixed some typos.
It's great to see this being written down in the context of julia :)
doc/src/devdocs/ub.md
Outdated
- 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 | ||
- 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 comment
The 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 comment
The 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.
|
||
## 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 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
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.
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).
Co-authored-by: Sukera <11753998+Seelengrab@users.noreply.github.com>
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.
Thanks so much for this writeup.
doc/src/devdocs/ub.md
Outdated
|
||
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. |
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.
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. | |
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. |
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)
doc/src/devdocs/ub.md
Outdated
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 comment
The reason will be displayed to describe this comment to others. Learn more.
- 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. | |
- 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. |
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.
"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 comment
The reason will be displayed to describe this comment to others. Learn more.
- 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. | |
- Replacement of `const` values. While the language itself does not define this behavior and the compiler may assume `const` values are never redefined, the compiler does take some care to minimize impact in interactive mode for user convenience. |
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.
doc/src/devdocs/ub.md
Outdated
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. | ||
- 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 comment
The reason will be displayed to describe this comment to others. Learn more.
- Various modification of global state during precompile. Where possible, this is detected and yields an error, but detection is incomplete. | |
- Various modifications 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 comment
The 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)
|
||
## 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 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
Line 2493 in d8b9810
if !(length(argtypes) ≥ 2 && getfield_notundefined(obj, argtypes[2])) |
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.
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)
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.
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?
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.
A specific, known allocation always returns the same value when observed, but a specific call / allocation site does not
I really don't like this, but thank you. My previous — obviously wrong — understanding was that the Julia compiler was trying to guard us from LLVM's undefined behaviors via I think part of my issue here is just how aggressively and adversarially other compiler teams have historically used a very legalistic reading of UB to do absurd things. For example, my mental model was that changing a const was just putting me at risk of using the old value in some places — and those places simply aren't specified. That's just fine. Now, sure, you might not decide to make entire function bodies no-ops when they contain a changed-const var, but another compiler dev could look at this list and see a juicy spot for a great optimization. |
@mbauman there are already cases where changing a const can lead to a method being optimized out. Consider, for example
Despite the fact that Since we have had the ability to define typed globals, I wonder if we should make redefining a |
That matches my expectations, though. It's just fine that Edit to add: I fully understand your point about how inconsistencies like these can "bubble up" to larger unexpected behaviors, but to my understanding the distinction between an undefined behavior and an unspecified behavior is exactly how the language behaves in doing that "bubbling up." If the value of |
- 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 |
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.
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.
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.
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))
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.
I assume you mean unsafe_pointer_to_objref
That is not so - admittedly, without a specified memory model it's a bit hard to do for everything in this PR (things involving pointers in particular, though those operations generally inherit the semantics of C by necessity), but in principle everything here can be justified as being in this document through Julia semantics alone. Undefined behavior is not something that bubbles up from a lower level of abstraction, but is inherent to every level of abstraction, to some extent (and with sometimes more disliked behavior than other times). Getting an error when calling This difficulty is part of the reason why I want to get away from the term "undefined behavior", because people generally think "ah, this is this nasty C business with pointers and boundschecking and stuff" instead of "I'm relying on behavior that is not specified/guaranteed to continue to exist". |
*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. | ||
|
||
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 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)
- 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`) | ||
- 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 comment
The reason will be displayed to describe this comment to others. Learn more.
- Data races | |
- Data races, although some limits are still placed upon the allowable behavior, per the memory model. |
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.
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 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
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.
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.
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.
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 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
- Violations of TBAA guarantees (e.g. using `unsafe_wrap`) | ||
- Mutation of data promised to be immutable (e.g. in `Base.StringVector`) | ||
- Data races | ||
- Modification of julia-internal mutable state (e.g. task schedulers, data types, etc.) |
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.
...including overloading key functions such as getproperty(::Type{T}, ...)
, or show(io::IO, ::Type{T})
😅
In C standards and related common usage, the former is called "unspecified behavior", not undefined behavior and makes a precise distinction between them. However it is also true that many UTF-8 decoders are unsound if they encounter any malformed data and therefore they will cause undefined behavior (but this is not true of the Julia decoder). |
doc/src/devdocs/ub.md
Outdated
|
||
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. |
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.
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
I don't disagree with any of the things in this PR being marked as unspecified or implementation-defined or flat-out invalid. What I dislike is the term UB and the privilege that it traditionally grants the compiler — it's not generic "nasty C pointer stuff," it's the way in which UB wrecks mayhem around it. It's how UB propagates not just forwards in the execution context but also backwards in how it affects the entire function's compilation. It's how C compilers will notoriously delete error checks that were naively (and, yes, improperly) trying to "catch" some UB. It's how, if invalid string codeunits were included in this list as UB, it'd grant Julia the license to skip the error entirely. And how that might only happen in some contexts. And how trying to test for invalid codeunits would itself be invalid and eligible for deletion. Even if the UB is scoped to This document cuts two ways: it sets guardrails for users, and it grants license to the compiler devs. The guardrails for user APIs need to be in user docs, not devdocs. |
Doing an example to turn this into launching space invaders is left as an exercise to the reader. |
Clearly they're not |
Clearly, I know. That const replacement crash is a good example, thanks. But it still feels different to me than how UB has traditionally been exploited by other compilers. Maybe it’s just my feels, but even in that crash the compiler seems doing something reasonable — albeit problematic. I know that reasonable is in the eye of the beholder, but that’s at the crux of it — users and compiler devs have historically had very different views on what reasonable behaviors might be. I just don’t want to have to argue with a legalistic and maliciously compliant compiler. I dunno, obviously this ship has already sailed. It’s definitely better to have it written down. |
I guess to be clear, we exploit similar things in julia i.e assuming consts don't change. It's just that our UB surface area is a lot smaller than C's which is the issue with C in itself. Any code with UB is a code with bugs, most of those become runtime errors for us, but C doesn't have that so it just assumes they never happen. We could create a new term for it, but it would mean exactly the same as UB |
You're right, it's unspecified behavior, not undefined behavior. The exact definition of what that is though is also not consistent across languages, so it seems to me we'd be in need of a definition for that as well...
Note that I haven't claimed either "invalid string codeunits" nor "malformed string codeunits" (very different things!) themselves to be UB -
Yes, I agree with that! One caveat though: since Julia doesn't have a spec, writing this down doesn't grant more license to compiler devs than they already had, since the current compiler is the exact "guaranteed" semantics. What I'd love to see is a longer list of "these things are guaranteed NOT to be UB (i.e., they are always allowed/guaranteed by the language semantics)", because that is what ultimately restricts the sorts of optimizations that are possible/valid. |
IMO anything that is
should error, rather than warn? maybe also applies to the |
|
||
- 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`. | ||
|
||
- 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 comment
The reason will be displayed to describe this comment to others. Learn more.
- 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"
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.
I get what you're saying, but this is still valuable. Perhaps they could be expressed with !!! compat
s.
- 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. |
Should the associativity within |
No, I think that's a different sort of thing; every single function needs to specify the behaviors its callers can expect and its methods need to satisfy. Or similarly grant leeway. This is more about the semantics of the language itself. I think I can finally express why I so strongly dislike the language of "undefined behavior." I've known forever that you shouldn't rely on And that's at the core of why I don't like the terminology of Undefined Behavior — in particular in a language without a standard to define behaviors. Undefined Behavior turns around the "above don't do that" into a threat. UB is "you can do that, but I'll trash your program and it'll be your fault, because it was invalid." It is jargon, because of how it typically differs from an unspecified behavior, or even a plain reading of "the behavior is undefined." The value from So back to const redefinitions. Redefining const, even in that segfaulting example, is currently ok if I also redefine all the functions that use that binding, too. It makes no sense to say it's full-on UB and at the same time "minimize impact" to preserve some behaviors. There are some behaviors that are defined — the warning is even documented! So what does it mean to me that it appears on this list? All this to say, this is a great list. We need to do more of this. Other candidates include return types and |
It's not UB
It now is, because it's no longer UB. That was a language specification change as a result of #26764.
No, it's not guaranteed - there could have been world age capture.
UB is about guarantees. After UB occurs the system can no longer make any guarantees about the future behavior the system, basically because a proof of Also finally, I don't know why people keep interpreting what I'm saying as trying to add UB everywhere. If you look at both the issues where we've removed significant sources of UB (#26764, #40009) and the one I mentioned above that may remove more (#40399), both of them were filed by me, as was the work that actually made #40009 not a disaster performance-wise (the termination tracking in the effect system). I think any reasonable observer would conclude that I'm in favor of removing as much UB as possible without compromising the overall performance of the system ;). |
That's not at all what I'm doing here. This whole thing started because I didn't understand what UB meant for Julia and because I thought others wouldn't understand the term. I've seen and so much appreciate how you've been removing it. Turns out, I still don't understand it — to the point that I can't communicate cogently with you (let alone the compiler). I mean, I get LLVM's But I don't understand UB in higher-level Julia terms. I've used the words "the behavior is undefined" in docstrings before, probably inappropriately. Am I using my words correctly if I describe The feedback I hope you hear is that this is a very specific term of art that I don't understand. |
Kind of? I think part of the problem is the focusing on the behavior of There's additional confusion, because some choices of the semantics of So what do we do in those cases? In some cases we, we change the semantics of the language to something that is suboptimal but reasonable (integer overflow overflows silently, does not error). In other cases, we change the semantics to produce an error, but in a small set of cases, an error is not feasible or desirable so the semantics are " So the question then is, what happens if the third case does happen? Basically, the answer is 🤷. From the moment any undefined behavior is executed, Maybe think of |
free of undefined behavior. | ||
|
||
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). | ||
|
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.
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).
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.
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 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.
The view that "if there is UB then anything goes" is incompatible with the real world where UB is prevalent. For example, according to that semantic, For folks who are skeptical that Base has UB, I decided to find an example in the latest stable release (1.10.2). This function is marked as :total, which includes :nothrow, which applies to all possible arguments, not just semantic executions: julia/base/reinterpretarray.jl Lines 729 to 731 in bd47eca
And on some arguments it does throw: julia> Base.array_subpadding(1, 2)
ERROR: MethodError: no method matching Base.CyclePadding(::Int64)
Closest candidates are:
Base.CyclePadding(::P, ::Int64) where P
@ Base reinterpretarray.jl:681
Base.CyclePadding(::DataType)
@ Base reinterpretarray.jl:719
Stacktrace:
[1] array_subpadding(S::Int64, T::Int64)
@ Base ./reinterpretarray.jl:731
[2] top-level scope
@ REPL[23]:1 To continue the train example, if I'm sitting around in the back yard of a nuclear power plant and suddenly a train runs over my clover garden, that's bad. It's reasonable for me to say "hey, there aren't tracks over here, please keep your trains on the tracks". The presence of a bit of "undefined tracks" in the train manufacturing plant (Base) does not not give the train driver license to careen their train into my clover garden unannounced. Now, I understand that it's hard for train drivers to keep trains well behaved when they drive over "undefined tracks". But in a world where undefined tracks are everywhere, it is a part of the train driver's professional responsibilities. "Julia is fast" is not in the spec, and is not promised by any legalistic agreements, but we still do a pretty good job, provided users write reasonable code. I think we should treat "Julia doesn't have crazy UB behaviors" similarly. If users are not going out of their way to construct pathological UB exploits, they shouldn't see crazy UB behaviors. And I think we should document that aspiration. This is not blocking and I'd be happy to add this note (with compiler folks' approval) in a separate PR after this one merges. |
UB triggers only if the user executes it. The compiler is not allowed to speculatively insert UB. (Well, except possibly nothrow as we haven't decided yet if that annotation allows the compiler to invent UB if it does actually throw or if it does not permit hoisting call and only allows eliminating calls) |
Ahhh, thank you @Keno. OK, now I can much better understand what's written in this PR. I had this backwards — that This is a subtle shift in my own understanding of Julia, and I still don't quite fully appreciate why this distinction is valuable, but now I get what UB means in the context of Julia the language and how it affects |
It's a very subtle thing, yeah - in Python, quite a lot of behavior from cpython has been "adopted" into Python-the-language, which makes it very hard to do meaningful changes. There's this very good talk by Armin Ronacher (How Python was shaped by leaky internals) that gets into some details about a similar distinction there. Hopefully the distinction between "Julia-The-Language" and " |
That definitely needs to be fixed. |
Should we split this into 2 cases? A case where any throw is UB (so hoisting is permitted without introducing UB), and a case where throwing is fine, but relying on that throw to exist is UB (so call elimination is fine without introducing UB, but hoisting is not fine)? |
One thing that's a little fuzzy to me is the various concepts and the wordings that are used for them:
Let me try to use what I've learned:
But then the programs I write can define (or not define) and constrain (or not) what behaviors subtypes should have or what functions mean or what method implementations must do. This is not the Language's UB or implementation-defined, it's just a program. One question I still have: are the "non-unique allowable behaviors" things from the beginning ( |
They are something else entirely (except for rng stream which is implementation defined). They define equivalence classes on what is allowable by the as-if rule. |
Minor nitpick to try and reduce further confusion: based on #53873, people can be confused by what |
Co-authored-by: Shuhei Kadowaki <40514306+aviatesk@users.noreply.github.com> Co-authored-by: Sukera <11753998+Seelengrab@users.noreply.github.com>
This implements world-age partitioning of bindings as proposed in #40399. In effect, much like methods, the global view of bindings now depends on your currently executing world. This means that `const` bindings can now have different values in different worlds. In principle it also means that regular global variables could have different values in different worlds, but there is currently no case where the system does this. # Motivation The reasons for this change are manifold: 1. The primary motivation is to permit Revise to redefine structs. This has been a feature request since the very begining of Revise (timholy/Revise.jl#18) and there have been numerous attempts over the past 7 years to address this, as well as countless duplicate feature request. A past attempt to implement the necessary julia support in #22721 failed because the consequences and semantics of re-defining bindings were not sufficiently worked out. One way to think of this implementation (at least with respect to types) is that it provides a well-grounded implementation of #22721. 2. A secondary motivation is to make `const`-redefinition no longer UB (although `const` redefinition will still have a significant performance penalty, so it is not recommended). See e.g. the full discussion in #54099. 3. Not currently implemented, but this mechanism can be used to re-compile code where bindings are introduced after the first compile, which is a common performance trap for new users (#53958). 4. Not currently implemented, but this mechanism can be used to clarify the semantics of bindings import and resolution to address issues like #14055. # Implementation In this PR: - `Binding` gets `min_world`/`max_world` fields like `CodeInstance` - Various lookup functions walk this linked list using the current task world_age as a key - Inference accumulates world bounds as it would for methods - Upon binding replacement, we walk all methods in the system, invalidating those whose uninferred IR references the replaced GlobalRef - One primary complication is that our IR definition permits `const` globals in value position, but if binding replacement is permitted, the validity of this may change after the fact. To address this, there is a helper in `Core.Compiler` that gets invoked in the type inference world and will rewrite the method source to be legal in all worlds. - A new `@world` macro can be used to access bindings from old world ages. This is used in printing for old objects. - The `const`-override behavior was changed to only be permitted at toplevel. The warnings about it being UB was removed. Of particular note, this PR does not include any mechanism for invalidating methods whose signatures were created using an old Binding (or types whose fields were the result of a binding evaluation). There was some discussion among the compiler team of whether such a mechanism should exist in base, but the consensus was that it should not. In particular, although uncommon, a pattern like: ``` f() = Any g(::f()) = 1 f() = Int ``` Does not redefine `g`. Thus to fully address the Revise issue, additional code will be required in Revise to track the dependency of various signatures and struct definitions on bindings. # Demo ``` julia> struct Foo a::Int end julia> g() = Foo(1) g (generic function with 1 method) julia> g() Foo(1) julia> f(::Foo) = 1 f (generic function with 1 method) julia> fold = Foo(1) Foo(1) julia> struct Foo a::Int b::Int end julia> g() ERROR: MethodError: no method matching Foo(::Int64) The type `Foo` exists, but no method is defined for this combination of argument types when trying to construct it. Closest candidates are: Foo(::Int64, ::Int64) @ Main REPL[6]:2 Foo(::Any, ::Any) @ Main REPL[6]:2 Stacktrace: [1] g() @ Main ./REPL[2]:1 [2] top-level scope @ REPL[7]:1 julia> f(::Foo) = 2 f (generic function with 2 methods) julia> methods(f) # 2 methods for generic function "f" from Main: [1] f(::Foo) @ REPL[8]:1 [2] f(::@world(Foo, 0:26898)) @ REPL[4]:1 julia> fold @world(Foo, 0:26898)(1) ``` # Performance consideration On my machine, the validation required upon binding replacement for the full system image takes about 200ms. With CedarSim loaded (I tried OmniPackage, but it's not working on master), this increases about 5x. That's a fair bit of compute, but not the end of the world. Still, Revise may have to batch its validation. There may also be opportunities for performance improvement by operating on the compressed representation directly. # Semantic TODO - [ ] Do we want to change the resolution time of bindings to (semantically) resolve them immediately? - [ ] Do we want to introduce guard bindings when inference assumes the absence of a binding? # Implementation TODO - [ ] Precompile re-validation - [ ] Various cleanups in the accessors - [ ] Invert the order of the binding linked list to make the most recent one always the head of the list - [ ] CodeInstances need forward edges for GlobalRefs not part of the uninferred code - [ ] Generated function support
This implements world-age partitioning of bindings as proposed in #40399. In effect, much like methods, the global view of bindings now depends on your currently executing world. This means that `const` bindings can now have different values in different worlds. In principle it also means that regular global variables could have different values in different worlds, but there is currently no case where the system does this. The reasons for this change are manifold: 1. The primary motivation is to permit Revise to redefine structs. This has been a feature request since the very begining of Revise (timholy/Revise.jl#18) and there have been numerous attempts over the past 7 years to address this, as well as countless duplicate feature request. A past attempt to implement the necessary julia support in #22721 failed because the consequences and semantics of re-defining bindings were not sufficiently worked out. One way to think of this implementation (at least with respect to types) is that it provides a well-grounded implementation of #22721. 2. A secondary motivation is to make `const`-redefinition no longer UB (although `const` redefinition will still have a significant performance penalty, so it is not recommended). See e.g. the full discussion in #54099. 3. Not currently implemented, but this mechanism can be used to re-compile code where bindings are introduced after the first compile, which is a common performance trap for new users (#53958). 4. Not currently implemented, but this mechanism can be used to clarify the semantics of bindings import and resolution to address issues like #14055. In this PR: - `Binding` gets `min_world`/`max_world` fields like `CodeInstance` - Various lookup functions walk this linked list using the current task world_age as a key - Inference accumulates world bounds as it would for methods - Upon binding replacement, we walk all methods in the system, invalidating those whose uninferred IR references the replaced GlobalRef - One primary complication is that our IR definition permits `const` globals in value position, but if binding replacement is permitted, the validity of this may change after the fact. To address this, there is a helper in `Core.Compiler` that gets invoked in the type inference world and will rewrite the method source to be legal in all worlds. - A new `@world` macro can be used to access bindings from old world ages. This is used in printing for old objects. - The `const`-override behavior was changed to only be permitted at toplevel. The warnings about it being UB was removed. Of particular note, this PR does not include any mechanism for invalidating methods whose signatures were created using an old Binding (or types whose fields were the result of a binding evaluation). There was some discussion among the compiler team of whether such a mechanism should exist in base, but the consensus was that it should not. In particular, although uncommon, a pattern like: ``` f() = Any g(::f()) = 1 f() = Int ``` Does not redefine `g`. Thus to fully address the Revise issue, additional code will be required in Revise to track the dependency of various signatures and struct definitions on bindings. ``` julia> struct Foo a::Int end julia> g() = Foo(1) g (generic function with 1 method) julia> g() Foo(1) julia> f(::Foo) = 1 f (generic function with 1 method) julia> fold = Foo(1) Foo(1) julia> struct Foo a::Int b::Int end julia> g() ERROR: MethodError: no method matching Foo(::Int64) The type `Foo` exists, but no method is defined for this combination of argument types when trying to construct it. Closest candidates are: Foo(::Int64, ::Int64) @ Main REPL[6]:2 Foo(::Any, ::Any) @ Main REPL[6]:2 Stacktrace: [1] g() @ Main ./REPL[2]:1 [2] top-level scope @ REPL[7]:1 julia> f(::Foo) = 2 f (generic function with 2 methods) julia> methods(f) [1] f(::Foo) @ REPL[8]:1 [2] f(::@world(Foo, 0:26898)) @ REPL[4]:1 julia> fold @world(Foo, 0:26898)(1) ``` On my machine, the validation required upon binding replacement for the full system image takes about 200ms. With CedarSim loaded (I tried OmniPackage, but it's not working on master), this increases about 5x. That's a fair bit of compute, but not the end of the world. Still, Revise may have to batch its validation. There may also be opportunities for performance improvement by operating on the compressed representation directly. - [ ] Do we want to change the resolution time of bindings to (semantically) resolve them immediately? - [ ] Do we want to introduce guard bindings when inference assumes the absence of a binding? - [ ] Precompile re-validation - [ ] Various cleanups in the accessors - [ ] Invert the order of the binding linked list to make the most recent one always the head of the list - [ ] CodeInstances need forward edges for GlobalRefs not part of the uninferred code - [ ] Generated function support
- Retention of pointers to GC-tracked objects outside of a `@GC.preserve` region | ||
- 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`) |
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.
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?
The metaprogramming docs on generated functions say:
Sounds like UB, right? So maybe Also xref: #55332 |
This adds some basic devdocs for undefined behavior, since there keep being complaints that it's not written down anywhere. The list of UB is just what I remembered off the top of my head, it's probably incomplete, since we haven't historically been particularly careful about this. This way, at least when people add new sources of UB, they'll have a centralized place to write that down.