Should we have provenance?

[JakobDegen]

Summary

The goal of this meeting is to lay out the arguments for and against the existence of pointer provenance, and hopefully arrive at a place where we can decide whether Rust should or should not have it. It is explicitly not the goal of this meeting to discuss what kind of provenance we should have if we do have it.

Time allowing, if people generally come to the conclusion that we should have provenance, we can additionally start some discussion as to whether or not we should stabilize (possibly a subset of) the strict provenance APIs. This is not the core goal of the meeting though.

Background reading

I plan on putting together a write-up for the meeting presenting the reasons for and against provenance. Strictly speaking, the intent is that it will be self-contained. That being said, some familiarity with the surroundings is probably good to have for any attendees that are entirely new to the concept of provenance; a good starting point here is Ralf's article on the need for pointer provenance or the section on this topic in the standard library documentation.

About this issue

This issue corresponds to a lang-team design meeting proposal. It corresponds to a possible topic of discussion that may be scheduled for deeper discussion during one of our design meetings.

[joshtriplett]

It is explicitly not the goal of this meeting to discuss what kind of provenance we should have if we do have it.

I think it would be appropriate to also present one of the (current) leading models, namely the looser provenance model that includes expose_addr and from_exposed_addr and similar. At the very least, I found it helpful to have that model in mind as contrasted with the strict provenance model.

[RalfJung]

MiniRust already specifies a model of provenance that supports expose_addr and from_exposed_addr. So it might be useful to look over the relevant parts of the code, maybe that can help clarify some lingering questions:

• the memory interface, defining things like "what is a pointer" but leaving the notion of provenance abstract
• a basic model of provenance that is not sufficient for our aliasing rules (e.g. Stacked Borrows) but gives a concrete example for what provenance can look like and fully models the rules of offset and wrapping_offset.
• the model for expose_addr and from_exposed_addr, which is actually independent of the concrete choice of provenance

[RalfJung]

a good starting point here is Ralf's article on the need for pointer provenance or the section on this topic in the standard library documentation.

That blog-post has some follow-up posts:

• part 2 contains a concrete example of a series of optimizations that go wrong because one of them implicitly requires provenance while another implicitly assumes the absence of provenance.
• part 3 shows that when adding restrict/noalias to the mix, things become even more subtle, and viewing a ptr2int cast merely as an operation that changes the value is plain wrong. We have to consider these casts as having some permanent side-effect on the abstract machine state that needs to be preserved even if the value returned by the cast is unused.

[eddyb]

I still stand by my "you can't really avoid provenance" (https://github.com/rust-lang/rust/issues/95228#issuecomment-1084028786) reasoning, but to account for certain things @RalfJung brought up at the time I need to add some extra caveats:

• to make less absolute claims, I suppose one could say that one average, when people say "no provenance", they don't mean "no high-level concept of memory, no memory-related optimizations, only low-level access as if the memory was an array" (which is how I would interpret the "no"), but rather they're arguing for some (fuzzily) weaker provenance model, or against specific provenance models being discussed
• regarding @RalfJung's specific example, (click to open rant)

  I'm not very attached to any specific interpretation, *but* I am mildly amused at the thought of reframing the non-deterministic allocated addresses model as "oracle provenance": that is, there is a "multiverse oracle" that can turn an integer into a pointer by giving you valid provenance iff the "coherent universe group" uniformly each provides the oracle their own respective integer for that allocation (though the only effect can be the presence vs absence of UB, not some kind of `-> bool`, because you don't *actually* have the "multiverse" and the "oracle" as part of execution, just like outside or CHERI or miri there is not really any physical encoding of provenance). I would also expect it to be possible to have an isomorphism between the non-deterministic allocation addresses and a fully deterministic model where every value of any kind carries with it non-trivial "reified multiverse structure", i.e. *provenance* (interestingly, much more complex than most provenance models, quite definitely "not flat", more like extending models meant to handle e.g. xorlists, to their logical extreme). These two views almost feels like comparing interpretations of quantum mechanics, though the closest equivalents would be "many-worlds" and "hidden variables", which AFAIK have their respective issues, and are less "canonical" than the few that "follow the math strictly" (Copenhagen, Transactional, not sure of others). Another similarity to that field is that you should be able to have "entanglement" and "strange spooky action at a distance", that most other provenance models either don't have at all, or they have less extreme forms of.

[RalfJung]

I don't know which "specific example" you mean. I think there is an interesting experiment to be made for how far one can get with just allocator non-determinism, but certainly this will not give us anything like noalias or Stacked Borrows. If we want optimizations based on aliasing rules for references, we need provenance.

[DavidVonDerau]

My 2 cents as a bystander:

• I discovered the strict provenance API and the "tower of weakenings" blog post earlier this week.
• I've read through all of the replies to the strict provenance tracking issue.
• I have 10+ years of embedded C/C++ experience, including in environments with requirements for extensive static analysis.

I think strict provenance is probably one of the most important developments I've seen in Rust's design, as it pertains to safety and correctness. I am incredibly excited for it!

I also think that the "tower of weakenings" concept is a brilliant escape hatch for the debates I've seen thus far -- teach strict provenance, provide the APIs for it, check it with Miri and/or the compiler, and we all accept that there's a weaker memory model that people can fall back to when they need to commit some crimes with pointers, e.g. due to an FFI boundary or some memory-mapped I/O at an absolute address on an embedded platform.

[alercah]

I got here while trying to catch up on Zulip and while I eventually gave up trying to read the whole thhead, I think there was far more ink spilled than necessary on things like LLVM, optimizations, C/C++, etc. when there is already aliasing rules in Rust that very heavily constrain our ability to do anything other than provenance. I'm not sure you really need to talk about anything else in the conversation.

[saethlin]

when there is already aliasing rules in Rust

What aliasing rules are you referring to?

[nikomatsakis]

Meeting minutes

and Zulip discussion