Blog post: Thoughts on trusting types and unsafe code

[nikomatsakis]

I.e. If you don’t understand what’s going on, don’t type unsafe, ever.

I really see it differently. If nothing else, I think interfacing to C is going to be very common. I also think that writing unsafe code doesn’t have to be (and shouldn’t be) a “wizards-only” activity.

But more than that, I think we just want to be careful in our assumptions of what we know. The region inferencer surprises me sometimes and I wrote the dang thing. I also worry that if our rules are too tightly tied to the type system we will wind up unable to make improvements and changes.

---

I feel lifetimes don’t offer any optimization potential relative to optimizing “traces” (like @arialb1 mentioned), and make writing unsafe code a lot harder. Plus, this doesn’t solve certain issues of optimization, like the example with collaborator.

So, since writing that post (actually sort of in parallel), I have been toying around with thoughts about traces. Actually I was pursuing a model very much like the one you described in an earlier comment:

If you get a reference, that reference is live. Any unsafe operations derived from this reference means you can’t use the reference again until you stop doing so. A reference derived from non-reference data borrows all of that data; if you want to perform unsafe operations you need to derive it once again from the reference, or wait until the reference is no longer used.

I agree that in a certain sense this is a very natural foundation. In trying to pursue it further, I definitely found some edge cases that I will try to write up soon. But I do think it imposes some limits on our optimization ability. For example, you wrote that my patsy example can be optimized, but I don’t think so:

fn patsy(v: &usize) -> usize {
    let l = *v;
    collaborator();
    use(l);
}

The problem here is that we do not see a use of *v after the first line. So while we know that v guarantees us a borrow of the data, that guarantee only extends as long as v is live. And the reference is only live until you stop using it. So who’s to say that let l = *v isn’t the point where we stop using it?

Put another way, patsy could be seen as outlining part of my alloc_free snippet:

fn alloc_free() {
    unsafe {
        let p: *mut i32 = allocate_an_integer();

        // fn patsy(x: &usize) -> usize {
        let q: &i32 = &*p;
        let r = *q; // let l = *v
        free(p); // <-- this is the body of collabator()
        use(r); // use(l)
    }
}

(Of course you’d have to thread the data around and so forth, but I don’t think that causes an issue.)

---

However, I don’t think giving function or module or crate boundaries any special significant w.r.t. unsafe is the right thing to do, because it doesn’t match people’s mental model of how programs work

This may well be, but keep in mind that the goal with the Tootsie Pop Model is not to make just any old function call significant – but rather those that cross over abstraction boundaries. I would like to think that there is a certain intuition about those particular boundaries. (For example, that there is a difference between the implementation of Vec and its users.)

I think assuming equivalence between a function call and inlining the function’s code is common thinking among programmers.

Yeah, that makes sense. On the other hand, my fear is that all of the things which are “common thinking” cannot be mutually reconciled.

---

Interesting, would you see this kind of thing going in the memory model or elsewhere?

I have been trying to shift to the terminology of “unsafe code guidelines” for just this reason. The notion of a “memory model” is one small (but important) part of it.

On the subject of trusting types, some invariants seem necessary even in unsafe code - lack of trust may not be absolute.

Absolutely!

---

I am still missing the answer to what is for me the most important fundamental question: why should that unsafe code be legal?

Sorry, I think you’re asking me this question, but I feel like I don’t know which unsafe code you meant. =) To be honest, I’m a bit confused by your comment overall.

For example:

So… I guess my stand on the whole topic is that I am fine with undefined behavior in unsafe code, and I am fine with broken unsafe code producing crashes in safe code, which is the situation we have today.

It seems obvious that under any model there will exist the potential for unsafe code to create crashes that manifest in safe code. I didn’t mean to imply otherwise. Perhaps my talk of “blame” was confusing? I did not mean to suggest by blame that this is where a crash would occur – merely that I’m interested in seeing if there are rules that can help us to decide which bit of code is wrong (as opposed to UB, which simply states that “something bad happened”). I’m not sure yet if it is helpful to think about blame.

---

When and how far can we trust function types?

Yes, definitely related.

---

UB is only defined on traces. Therefore, trusting types can only mean trusting properties that can be discovered from these traces.

I’ve been going back and forth on this. On the one hand, I like the idea of having a kind of “base layer” that is UB defined over traces and ignores fn boundaries and many other artifacts of the source code.

Then you can imagine that unsafe code must layer on top of this some way of proving that this UB will never happen. To claim to be a “safe interface”, this proof must have some modularity to it, to allow for arbitrary safe code to execute (e.g., to invoke the methods in any order, or to take arbitrary (safe) actions in a callback).

But of course some of those arbitrary safe actions that safe code can do might involve other unsafely implemented interfaces. So for there to be any kind of composition, there has to be some notion of permissions – that is, we have to think “safe code can do anything within these boundaries”. This is exactly the logical system that @RalfJung has been trying to model, of course.

But these permissions are, I think, something that we as the language have to be involved with. After all, as I wrote above, they are a kind of “common currency” that unsafe code uses to interoperate. To a large extent they probably follow from the safe type system.

But I am coming around to the POV that it makes sense to have some “base” notion of UB over traces, even if it doesn’t seem to be the end of the story. But of course even that base notion requires thinking about the optimizations the compiler might do and incorporating them. (It’s not like it’s purely derived from the behavior of the O/S and hardware etc)

---

As a user of the language, here are some of my expectations

This is a helpful list, thanks. =) Many of these are already issues in the rust-memory-model repo, but I will try to come back and make sure that all are present (as things to evaluate, iow).

it would be particularly bad if the presence of pointer-unrelated unsafe to contaminated the module (or anything nearby) with pessimistic assumptions about pointer aliasing.

Yeah, I think this is (roughly) the point of the unchecked-get example, and it makes sense. Of course, the point of this post is that many alternative models will wind up being more pessimistic about pointer aliasing EVERYWHERE, rather than just (by default) in the vicinity of unsafe code. =)

Which would make unsafe even more subtle in terms of UB than C.

I’ll repeat my belief that there should be a way to write unsafe code that is simple to get right, even if it not as well optimized. I am not sure that the Tootsie Pop Model strikes the right balance here – I can clearly see that it has few fans – but I think that its heart is in the right place. All I mean by “simple way to write unsafe code”, mind you, is that there is some set of rules. For example, I would probably be satisfied with a system where one could say, "if in doubt, use a *mut instead of a &". Then, starting from this base substrate, one can add in optimization by using more Rust types (presuming we have some clear rules for when that’s ok).

[arielb1]

But of course some of those arbitrary safe actions that safe code can do might involve other unsafely implemented interfaces. So for there to be any kind of composition, there has to be some notion of permissions – that is, we have to think “safe code can do anything within these boundaries”. This is exactly the logical system that @RalfJung has been trying to model, of course.

Sure - we need some kind of behavioural typing. But it is subtle - see e.g. crossbeam vs. coroutines or even more pedestrianly set_len vs. get.

But I am coming around to the POV that it makes sense to have some “base” notion of UB over traces, even if it doesn’t seem to be the end of the story.

Everybody (e.g. the C standard, LLVM) defines UB as something over traces. Therefore, if we want to be interoperable, we ought to do that ourselves.

[Veedrac]

So while we know that v guarantees us a borrow of the data, that guarantee only extends as long as v is live.

I view it slightly differently; there’s a trace for each function, not one global trace. Each local trace is conservative and function-granular. The optimiser also knows that other functions are based on these conservative traces, so can assume they play nice.

Any caller cannot make the assumption that patsy relinquishes its borrow partway through execution. This makes sense, because we want to be able to juggle dereferences within a function. From any patsy_caller's point of view, v is borrowed for the whole of patsy, and only then up until the next time it’s used.

This means patsy can be confident in its borrow up until the moment it returns. (Unsafe code might even be confident for longer, if you know the function is always followed by something else before further use of v, but the optimiser does not get to assume that.)

---

Also, I think the the optimiser has to act locally if we want mere humans to be able to predict what’s safe. A global trace doesn’t sound like something I could reason about reliably.

[ahmedcharles]

I really see it differently. If nothing else, I think interfacing to C is going to be very common. I also think that writing unsafe code doesn’t have to be (and shouldn’t be) a “wizards-only” activity.

But more than that, I think we just want to be careful in our assumptions of what we know. The region inferencer surprises me sometimes and I wrote the dang thing. I also worry that if our rules are too tightly tied to the type system we will wind up unable to make improvements and changes.

I’m not suggesting that interfacing with C will be uncommon and I’m not suggesting that it should be hard or wizards only. I’d never want such things to be true. But it turns out that I happen to be (or want to be) a wizard. I want to know everything I can about the languages I care about. I want to be in a situation where if I learn more, I have more control over my code, whether it be performance or data layout or whatever is important at the time. So, what I don’t want to happen, is for Rust to cater to programmers that lack knowledge of Rust over catering to ones that do. I can’t prove that these two goals have to be in opposition, though.

More importantly, I’m not sure why this process isn’t starting with trying to understand the minimum semantic guarantees required (or provided) by unsafe operations currently? It seems that the cart (talking about optimizations) is coming before the horse (discussing of semantics).

[rkjnsn]

However, just to explicitly point it out, trusting types at either the function or safe<->unsafe boundary means that the “refcell-ref” example in the TPM post is invalid and the & in Ref must be a pointer.

I’ve stated this elsewhere, but I think the “refcell-ref” example should be invalid.

[RalfJung]

Everybody (e.g. the C standard, LLVM) defines UB as something over traces. Therefore, if we want to be interoperable, we ought to do that ourselves.

Do they? I don’t know about LLVM, but I grepped the C11 standard for “trace” and didn’t get a single hit. Their concurrent memory model is a complex beast consisting of a dozen relations and a dozen consistency axioms. Other than that, UB is defined by well over a hundred rules spread all over the document that describe how to evaluate the various operators. This seems reasonable enough when only considering one operator at a time, but when it comes to multiple features interacting, there can be long arguments about what the standard says and what it means and what it should say – as witnessed by various examples. There have been attempts at a formal definition, but I would still not dare to say that UB in C is “defined” – and most of what I saw does not involve traces.

It is true that in the literature, (sets of) traces are often used to “summarize” a program’s behavior. But for defining their semantics, other methods like operational semantics are just as common, and I personally will always prefer the latter over the former.

[Fylwind]

I’m with @ahmedcharles on this. I don’t believe the examples are correct, even if they might appear to be. A good rule of thumb would be: If you have a reference to X within the current scope, then X must remain alive until the end of the scope. The correct way to write the code should be:

fn alloc_free() {
    unsafe {
        // allocates and initializes an integer
        let p: *mut i32 = allocate_an_integer();

        // create a safe reference to `*p` and read from it
        let r = {
            let q: &i32 = &*p;
            *q
        };

        // free `p`
        free(p);

        // use the value we loaded
        use(r); // but could we move the load down to here?
    }
}

[nikomatsakis]

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.