UB does not time travel

[RalfJung]

Fixes rust-lang/unsafe-code-guidelines#407 by saying that our UB does not have time travel semantics (in relation to observable behavior such as I/O and volatile accesses).

This does not require any compiler changes. The compiler already does not do time-traveling UB, we just need to change the docs to turn this into a promise for our users.
Note that this relies on LLVM 23. With LLVM 22, UB can time travel across volatile reads. We use LLVM 23 but still allow compiling with LLVM 22, though we also document that

The one or two preceding major versions are usually supported in the sense that they are expected to build successfully and pass most tests. However, fixes for miscompilations often do not get backported to past LLVM versions, so using rustc with older versions of LLVM comes with an increased risk of soundness bugs. We strongly recommend using the latest version of LLVM.

I don't know to what extent we consider inofficial builds of Rust (with different LLVM versions) as being governed by the Reference.
Cc @rust-lang/opsem @rust-lang/lang

[joshlf]

What is the advantage of providing this guarantee? Since everyone (as far as I'm aware) aspires to produce code which is entirely UB-free, I can't imagine someone wanting to rely on this.

Plus, as you say, it constrains us to specific versions of LLVM (and presumably to LLVM, period – what about Cranelift or other future backends?).

Maybe we could weaken this to say that we don't currently have time-traveling UB when compiling with the standard LLVM backend, but that this isn't a stability promise, and that it may not apply to other backends?

[RalfJung]

The advantage is that if you do

dbg!(...);
some_function_that_maybe_has_ub();

then you will reliably see that debug output before the UB. It is quite frustrating when you can't debug your null ptr deref because the dbg! that would print the pointer value is swallowed by time-traveling UB. The classic example from C is the equivalent of

eprintln!("going to load from {ptr:p}");
let _val = ptr.read();

and then seeing a crash without the print. Now you may think that the crash occurs from some other operation before the print. But actually the read is where it crashes, the compiler just moved the read above the print so you can't tell any more where the crash originates from.

Of course you don't rely on this for an actually deployed program. But you are not unlikely to rely on this while debugging a program and figuring out what the heck it is doing and where it is going wrong.

[joshlf]

That's a good point, but presumably it'd still be useful to those users for us to document this without documenting it as a stable guarantee?

I'd need to think more to convince myself that this is actually true, but I think that this guarantee would make it harder for Aeneas and Anneal to model UB (AeneasVerif/aeneas#1225). Currently the proposal is to model UB as a kind of "absorbing state" in which, once you reach UB, that's all that Aeneas says about your execution. If pre-UB effects are observable, then we'd need to expose those effects in addition.

I suppose could just say "Aeneas's model is strictly weaker than – but not inconsistent with – what Rust itself guarantees", but I'd like to avoid that, at least for Anneal, if possible. It makes it harder to keep straight the correspondence between Aeneas/Anneal and upstream Rust, makes it harder for us to explain to users, etc.

cc @sonmarcho @protz @mdittmer @Nadrieril

[RalfJung]

That's a good point, but presumably it'd still be useful to those users for us to document this without documenting it as a stable guarantee?

I feel quite strongly that time-traveling UB is something we don't want to do. Time-traveling UB defies people's intuition and is often used as an example for "look at this silly thing the compiler did" (and I can't even really argue that people are wrong when saying that). Even C finally got rid of time-traveling UB by accepting N3128, albeit as a recommendation rather than a normative requirement (IIUC).

Time-traveling UB is a disservice to our users. Therefore, we shouldn't do it, and we should promise not to do it.

I'd need to think more to convince myself that this is actually true, but I think that this guarantee would make it harder for Aeneas and Anneal to model UB (AeneasVerif/aeneas#1225). Currently the proposal is to model UB as a kind of "absorbing state" in which, once you reach UB, that's all that Aeneas says about your execution. If pre-UB effects are observable, then we'd need to expose those effects in addition.

Note that this model is already wrong. Consider a program like this:

fn main() {
    let mut buffer = String::new();
    let _ignore = io::stdin().read_line(&mut buffer);
    unsafe { std::hint::unreachable_unchecked() };
}

If I run this program and then hit Ctrl-C when it waits for input, that's an entirely well-defined execution. The compiler must create code that handles that execution correctly. It seems you are saying Aeneas would model this execution as equivalent to a program that always has UB; that is an incorrect model.

The only operations where UB as a sort of "absorbing" state is a correct model are operations that are guaranteed to always return. Many I/O operations are already allowed to never return and models have to deal with that.

[RalfJung]

@rustbot label +I-lang-nominated

[RalfJung]

I suppose could just say "Aeneas's model is strictly weaker than – but not inconsistent with – what Rust itself guarantees", but I'd like to avoid that, at least for Anneal, if possible. It makes it harder to keep straight the correspondence between Aeneas/Anneal and upstream Rust, makes it harder for us to explain to users, etc.

I think it would be a sad outcome if trying to support more formal reasoning tools would lead to Rust making fewer useful (and formally meaningful) promises to its users.

It is true that this can complicate modeling Rust programs with observable behavior. But I think that complication is well-invested effort to make Rust behavior better aligned with people's intuitions and with what we actually want the compiler to do.

If Aeneas/Anneal anyway proves that a program cannot reach UB on any path then I don't think it should cause significant complications. Complications mostly arise if you want to define the semantics of programs that sometimes do and sometimes do not have UB, and what it means to correctly compile such a program.

[traviscross]

Interesting. For my part, I see why this makes sense. Probably the most surprising consequence, that I see, is that it prevents hoisting loop-invariant code such as this:

/// Sample a device register, scaling each sample by a
/// configurable value read through `cfg`.
pub unsafe fn sample(reg: *const u64, cfg: *const u64, out: &mut Vec<u64>) {
    for slot in out.iter_mut() {
        let v = unsafe { reg.read_volatile() }; // Observable.
        *slot = v.wrapping_mul(unsafe { *cfg }); // `*cfg` is loop-invariant.
    }
}

But there are other ways this could be optimized.

[traviscross]

Presumably we mean to define this in terms of execution order (as the C folks did) rather than source code order. E.g.:

for i in 0..10 {
    unsafe { maybe_ub(i) }; // UB only when `i == 5`.
    println!("{i}"); // After the UB point in the source code.
}

View changes since the review

[RalfJung]

Yes that is what I meant. I concur that "source code order" is a bad term, but "execution order" begs the question -- which execution? The one in the Abstract Machine or the one on the Concrete Machine? Not all things happen in the same order in both.

In the memory model this is often called "program order", not sure if that is more clear. C++ calls it "sequenced-before".

[RalfJung]

That example could be hoisted by unrolling the first iteration. Also note that LLVM 23 already stopped doing that optimization as it considers volatile reads to maybe-trap, so we'd have to put in some effort to get it back if we truly caree about it.

[niluxv]

Time-traveling UB is a disservice to our users. Therefore, we shouldn't do it, and we should promise not to do it.

That sounds more like a Quality of Life issue than something that needs to be a stable language guarantee to me. Or something that could be controlled by some compiler flag, like digama0 proposed.

Also, regarding IO, this seems more of a library guarantee than a language guarantee. Or would you say that a rust crate which exposes a safe function which writes to a file would be unsound if it were implemented with an asm! syscall specifying a (hypothetical) willreturn option? I would be strongly opposed to that; it should be the library's choice whether it wants UB to time-travel over its IO (syscalls).¹

Footnotes

1. Just imagine an unsafe function with safety precondition: "The caller must ensure no UB occurs after this function is called". ↩

[RalfJung]

Whether UB is properly ordered wrt observable behavior is a core property of the very notion of execution of the AM. It is not a "quality of life" issue. It will affect what definitions one has to put into Rocq/Lean to model what a correct compilation of Rust even is.

would you say that a rust crate which exposes a safe function which writes to a file would be unsound if it were implemented with an asm! syscall specifying a (hypothetical) willreturn option?

Yes. Libraries don't get to break basic language properties such as how observable behavior and UB interact.

The only such option we have currently are various forms of things called "pure", and obviously it's UB to do I/O in anything called "pure".

[RalfJung]

After many years of people making fun for how silly C is to have time-traveling UB (me included), I am honestly quite shocked that anyone would argue in favor of such an extreme interpretation of UB. I have not the faintest idea why that is. In an alternative universe where UB has always interacted with observable events in a proper way I cannot imagine a proposal to make UB "swallow" previous I/O would have even the slightest chance of acceptance. The only reason Rust ever had time-traveling UB is because we were forced into it by LLVM.

In other words, I expected this to be a slam dunk with people celebrating the great news that we got rid of this wart in the language. Oh well, looks like I'll have to actually argue for this. And argue I shall :)

[mattheww]

Where should that argument happen? A Reference PR doesn't seem like the right place.

[chorman0773]

Probably on the UCG issue and/or the UCG thread for this.

[RalfJung]

Where should that argument happen? A Reference PR doesn't seem like the right place.

Why not? It's where I planned to propose FCP.
But it doesn't really matter, as long as there's just one place.

That sounds more like a Quality of Life issue than something that needs to be a stable language guarantee to me. Or something that could be controlled by some compiler flag, like digama0 proposed.

Note that @digama0 proposed this in a time when it seemed like we'd have to actually change what the compiler does not get no-timetravel. That's not the case any more. The latest rustc nightlies (since the LLVM 23 update) do not have time-traveling UB. The compiler already respects the stricter semantics. I don't think a flag makes sense here.

If anyone can ever make a convincing case in favor of time-traveling UB (which I haven't seen yet, even the much more sane ffi_pure has been unstable since forever which I interpret as there not being enough benefit to such an attribute that anyone bothered trying to stabilize it), we can consider a flag to let people opt-in to such extreme optimizations. If we must have a flag, that seems like the way better default.

[mattheww]

Why not? It's where I planned to propose FCP.

Because it mixes up deciding what the model is and deciding how to describe the model in the Reference.

[traviscross]

Speaking as a Reference maintainer, I think it's OK to debate the desired guarantees here, just as we'd debate desired semantics on a rust-lang/rust PR.

But I don't expect this to be controversial.

[traviscross]

Let's propose to do this (modulo wording tweaks to clarify this is about the execution order).

@rfcbot fcp merge lang,opsem

[rust-rfcbot]

@traviscross has proposed to merge this. The next step is review by the rest of the tagged team members:

• @CAD97
• @RalfJung
• @digama0
• @joshlf
• @joshtriplett
• @nikomatsakis
• @saethlin
• @scottmcm
• @tmandry
• @traviscross

No concerns currently listed.

Once a majority of reviewers approve (and at most 2 approvals are outstanding), this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up!

cc @rust-lang/lang-advisors: FCP proposed for lang, please feel free to register concerns.
See this document for info about what commands tagged team members can give me.

[saethlin]

@rust-rfcbot reviewed

[CAD97]

@rfcbot reviewed

[chorman0773]

I put a note on ucg#407, which should probably be considered before we go off.

[RalfJung]

@rfcbot reviewed