What does `unsafe` mean?


#1

This thread is intended to be a followup discussion to one started here: https://github.com/rust-lang/rfcs/pull/2316#issuecomment-362038934. I’m moving it here to avoid derailing the RFC discussion in that thread. You might want to read the comments by @withoutboats, @eternaleye, and me in that thread first…

The problem

It’s not at all clear what unsafe really means. Does it means that someone is upholding an invariant? A precondition or postcondition? Some combination? Also who is doing so? The user or implementor of some unsafe item? Or both?

There are a few possible ways of viewing unsafe

  • @withoutboats proposes a model in this blog post in which unsafe is a statement about invariants.
  • @eternaleye proposes that unsafe is part of Rust’s effect system here and here and refers to the terminology from this paper.
  • I proposed a model where unsafe is a statement purely about preconditions, rather than invariants. This is less useful but seems closer to what our actual usage of unsafe.

The common intuition seems to be that unsafe means someone is upholding an invariant (something that is always true) that is not checked by the compiler (e.g. TrustedLen says that the iterator size_hint returns the exact length). However, the usage of the unsafe keyword seems to be inconsistent (see here and here) with that definition.

The end goal of this thread

  • Come up with a precise definition of what unsafe means in all of the various places it could be used - hopefully one that is useful and intuitive. That is, what does unsafe mean in all of these places? Who has what obligations? Who gives guarantees to whom?
    • unsafe trait
    • unsafe fn (functions and methods)
    • unsafe impl
    • unsafe blocks
  • Consistently apply it across the language
    • That is, when should someone design an API as an unsafe trait vs fn vs method

#2

I’m going to be a bit picky here - there are four things we might refer to when we say unsafe:

  1. The behavior of unsafe fn
  2. The behavior of unsafe {}
  3. The behavior of unsafe trait/unsafe impl
  4. The keyword unsafe

The first three I would say are all part of Rust’s effect system (in distinct ways), alongside const. The last I would not, or would say that it is only inasmuch as it’s a really poorly considered syntax for interacting with the effect system.

My impression is that you’ve been, largely, syntax-directed in your view - taking the stance that unsafe means one thing, and we just have to pin it down carefully enough. I strongly disagree, and consider the first three items in that list to be very distinct meanings. As a result, if by “what unsafe really means” you intend to find a single definition of (4), I think you’re on a snipe hunt.

I feel that a clearer syntax for pedagogical purposes would be as follows:

// Any Foo implementation must uphold invariants
// that `unsafe` code is allowed to trust
trusted Trait Foo {
    fn foo() -> bool;
}

// This implementation of Foo agrees to uphold said invariants
trusted impl Foo for () {
    fn foo() -> bool { ... }
}

// This function may violate memory safety if its assumptions are violated
//
// Note that these may be invariants, not just preconditions -
// consider threading, which could modify a `static mut` or
// `atomic` while this function is executing.
unsafe fn bar() -> Whatever {
    // This code may invoke primitive `unsafe` effects 
    // (dereferencing raw pointers, accessing `static mut`s)
    // and may call other `unsafe fn`s
    ...
}

// This function will not ever violate memory safety, and
// may rely upon `trusted` code's behavior in ensuring
// that this is the case (such as `T::foo()`)
fn baz<T: trusted Foo>() -> Option<Whatever> {
    if T::foo() {
        None
    } else {
        // The enclosed `unsafe` code has had its assumptions upheld
        Some(mask<unsafe> bar())
    }
}

Here,

  • trusted is the restriction-form (inwards-propagating) dual of the untrusted effect,

    • untrusted denotes “the right to violate your documented properties without memory-safety consequences”
    • Thus, trusted denotes “the restriction that violating documented properties is morally equivalent to violating memory safety”
  • unsafe is the effect that permits dereferencing raw pointers and accessing mutable statics

    • Being an effect, the “calling unsafe functions” power is covered by the central “effects are infectious outwards” property, and isn’t anything special - an effectful context can always call other functions with the same effect; that’s just how it works.
  • mask<e: Maskable> is a generalized tool for masking effects and restrictions. For effects (like unsafe), it allows putting code that should need the marker inside code that lacks it. For restrictions (like trusted), it allows putting the marker on code that contains calls that lack it. In short:

  • unsafe fn a() {}; fn b() { mask<unsafe> a() } with “effect” polarity

  • fn a() {}; trusted fn b() { mask<trusted> a() } with “restriction” polarity

Personally, I would love to be able to use trusted on functions (to say that unsafe code is allowed to rely on them) rather than it only being possible to ascribe to traits. Similarly, there exists an RFC to allow attaching const to traits and impls, so they may be constrained on in bounds.

The current syntax isn’t something with a single behavior we need to illuminate; it’s a consequence of shoehorning multiple behaviors into a limited set of keywords to avoid breaking changes.


#3

It seems to me like quite a lot of libraries would end up putting ‘trusted’ on all their public APIs, just in case the library turned to be useful to some future unsafe or trusted code. I realize that in your proposal, unsafe/trusted code could still make calls to untrusted code by surrounding them with mask<trusted>. But as I understand it, you’re only supposed to do that if you think you can uphold your own invariants in the face of totally arbitrary incorrect behavior from the untrusted code. Is that often something one can really guarantee?


#4

I think that a function could “upgrade” to trusted at a later point as a non-breaking change, the same as one could theoretically change to const as a non-breaking change?


#5

Hm, I don’t think so - for one, adding trusted (like removing unsafe or adding const) is never a breaking change, and thus it can always be done in a revbump or even patch release. This is one of the reasons in favor of Centril’s proposals to allow const impl (and fn in place of unsafe fn on impls) - it makes that workflow simpler.

In addition, trusted is as much of a burden as unsafe {} in its own way - in essence, trusted promotes “merely” not fulfilling the promises made in documentation to full-on memory unsafety (in potentia). It just doesn’t itself perform unsafe operations.

Yes, although trusted is intimately related to unsafe - the closest analogy to masking trusted right now, in fact, is #[may_dangle] T, stating that we don’t actually rely on T's validity. So that’s a great example right there. The validity in question (that references are valid) isn’t expressed as a trait, but similar things could be.


#6

I feel like this comment summarizes it pretty well (slightly extended by me to also cover unsafe blocks):

Any time unsafe is on a Trait or a block the implementer must verify it for safety, any time unsafe is on a function or method (trait or inherent) the caller must verify it for safety at each use.

So, I agree that there are “two polarities” here, and there’s no fundamental reason these should have the same keyword. IIRC there actually was a proposal once to change unsafe blocks into trusted {} (and then unsafe traits should require a trusted impl) to convey the idea that this block doesn’t actually do anything bad – it’s just that we have to trust it to not do anything bad because the compiler can’t check it. I also feel it may have been a mistake to permit the entire body of an unsafe fn to perform unsafe operations; just because we rely on additional invariants doesn’t mean we want to accidentally deref a raw pointer somewhere.


I do not see how unsafe blocks can be seen as an effect. Effects are characterized operationally, things like “this function will not read from or write to the heap in any way”. unsafe cannot be characterized that way. Quite the opposite, actually: One important use-case of unsafe blocks is to make some function or method go fast without changing behavior compared to the slower safe implementation (think of using get_unchecked_mut). The fact that this function uses unsafe is not observable from the outside at all, so it’s not an effect.

The fact that unsafety is typically encapsulated where effects are “infectious” as you said, also indicates to me that viewing unsafe as an effect is not very useful. unsafe fn foo(x: u32) indicates a precondition not expressible in the type-system ("x must be even"). If a caller can guarantee that that precondition always holds (by calling foo(2*y)), the precondition is discharged and any unsafety taken care of and perfectly hidden from the sight of the caller. This is in strong contrast to the “outwards propagation” of effects.

I think of unsafe code as being essentially untyped: We have a language that allows all sorts of dangerous operations, and we have a type system that syntactically carves out a well-behaved subset of functions and data structures. However, the set of all well-behaved functions cannot be characterized syntactically; there are data structures that are well-behaved but the reasons for this are subtle (like “we got this RefCell counter right”). unsafe {} is a mechanism saying “even though this looks fishy, I promise that this function actually is well-behaved”; whereas unsafe fn is an indication saying “this function is well-behaved only if some non-machine-checked preconditions are met”.

Never are you allowed to write an ill-behaved function. What you call trusted fn above, if I understand it correctly, applies to all functions. Violating documented properties when calling foreign code is morally equivalent to violating memory safety.


#7

Ah, a few nits - one, ‘will not’ is more ‘restriction’; effect is ‘may’ anywhere I’ve seen it. Two, I’d call unsafe blocks the masking construct of an effect, rather than the effect itself. Three, the actual effect - the additional power granted at runtime - is the power to cause memory unsafety. This is like how the partiality effect allows one to diverge, when the totality checker is overly restrictive - even though the code in reality should not diverge. However, just like unsafe, the partiality effect can be masked (in that case, by evaluating only to a bounded number steps, and returning the option monad).

See http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.73.4916&rep=rep1&type=pdf for more on the ‘masking’ terminology.

EDIT: To put it another way, the effect is a static over-approximation of the dynamic behavior of the effectful function.


#8

Sorry for the late response… Things are getting busy for me …

Well, I guess I wanted the minimum number of possible meanings. I definitely agree that unsafe blocks have a different meaning from the others, but it would be nice if the others could be unified somehow…

Also, for posterity, re: your point in the previous thread:

I have consistently seen unsafe trait described as upholding extra invariants. This is a very specific term: An invariant is true at all points, as compared to a precondition (true before, but not necessarily within or after) or a postcondition (true after, but not necessarily before or within).

This point is well taken. I guess what I am wondering is unsafe is actually used that way by the language. i.e. We want it to say something about invariants and that what we mean intuitively when we use it, but do the semantics of unsafe actually work that way? That was the intent of my “preconditions-only” idea…


#9

Yup; unsafe impl Sync for T {} means that T can always be shared between threads, regardless of what may have been implemented for it before or after, or what’s currently mid-execution.


#10

You’re right. The effect would be sth. like “heap”, saying “this may access the heap”; what I described would be the absence of the “heap” effect.

the actual effect - the additional power granted at runtime - is the power to cause memory unsafety.

But the code is not allowed to cause memory safety! The “partiality” effect as you call it (I’d call it divergence) usually means that such functions are actually allowed to diverge. This is a way of talking about diverging computations in an otherwise total language. This is very different from “disabling the totality checker” in cases where the function is terminating, but the checker doesn’t understand. I have not seen this described as an effect before either; I’ll check your reference once I have more reliable connectivity.

To summarize: I agree “This function may diverge” is an effect. It means that it’s actually okay for this function to diverge, just like it’s okay for possibly-heap-accessing functions to access and mutate the heap and behave impurely. “This function does not diverge but the compiler didn’t check that” is something very different; it’s an unchecked assertion (akin to calling untyped code from typed code, aka FFI).


#11

I very much think unsafe in all of its forms is a lot about invariants. That’s the approach we’ve been using in the RustBelt paper; it is powerful enough to explain why Rc and other unsafely implemented data structures make sense. I’ve been writing about it here and here.

What do you mean by “semantics of unsafe”? In terms of operational semantics, unsafe has to effect whatsoever.


#12

Coming back from reading this (and sorry for the multi-reply): I think I can see better now where you are coming from. There is indeed some similarity behind this “masking of effects” and “hiding unsafety”. However:

  • In the paper, this masking is actually verified by the type system. So this does not capture the unchecked nature of unsafe, which IMHO is its most important aspect.
  • The masked effects in the paper are actually allowed to occur in other contexts. A heap-manipulating function is just fine; being able to mask its effect makes stronger guarantees (which is nice) but has no bearing on whether the program is “legal”.

It seems possible to describe unsafe blocks as some form of unchecked masking, but that still leaves the point that the “effect” this masks is not actually allowed to occur, ever. There is no “unmasked unsafety”. Given that, I do not see the value in introducing the terminology of an effect system.

What is wrong with the straight-forward summary at the beginning of first post in this thread? TBH I have not even seen the need to discuss this issue previously because I felt like this sentence says all there is to say. I was clearly wrong though, as this discussion shows :slight_smile:


#13

In the current ecosystem, this is correct - there is no "transitive #[deny(unsafe)]", nor the ability to declare an unsafe entry point (in stable, at least). However, I do think that is an interesting design point to consider, along the lines of Safe Haskell.


#14

That’s not what I have been talking about. Also, I used the wrong word – I meant to say “unmasked memory-unsafety” (matching your definition of the “unsafe” effect). “unmasked (memory-)unsafety” would be a function that, when called, exhibits (or may exhibit) memory unsafety – matching “unmasked divergence”, a function that, when called, may diverge. For divergence that’s a reasonable thing to do; for memory unsafety, it is not.


#15

Yes, I actually just watched your POPL talk :slight_smile: I think that makes a lot of sense.

By “semantics” I mean its “actual meaning”, rather than what we intuitively hope it means. For example, is there any place in Rust where it is possible to introduce memory unsafety/data races but unsafe is not required syntactically? My understanding after watching your talk is that the answer is “no” for the subset of rust you checked. A related (but less critical) question is “is unsafe usage minimal?”. i.e. are there places where we require unsafe today but where the compiler can already prove the code is safe? https://github.com/rust-lang/rfcs/pull/2316 seems to imply there are.

If I understand you correctly, what you are saying is that talking about “masking unsafety” is roughly equivalent to talking about “masking bugginess”? It’s not meaningful because we have assume that unsafe code is correct anyway?

I think I sort of see @eternaleye’s point though: there is a lot of usefulness in seeing what code needs to worry about additional unchecked invariants beyond what safe Rust give you… I’m not fully convinced that effects are the right way to reason about it though.


#16

That would be a bug, by definition.

Possible, but the policy is that these should be changed to no longer require unsafe. unsafe is not supposed to be used as a lint for “dangerous”, it’s supposed to be directly related to memory safety.

https://github.com/rust-lang/rfcs/pull/2316 is what started this discussion (AFAIK); in my view what happened here is that some people were confused above which party has a proof obligation when there is an unsafe keyword (and admittedly, the fact that we use the same keyword for “the implementor has to be careful” and “the caller has to be careful” is not helping).

Oh, absolutely. This is crucial to explaining the unsafe keyword and its interaction with memory unsafety. I’ve actually written a blog post about it :wink:

Notice that this previously quoted comment also focuses exactly on that aspect.


#17

So it makes sense to me that unsafe is not an effect semantically because memory safety is never OK morally. Might it still make sense to call unsafe an effect syntactically in terms of effect polymorphism and bounds such as: T: unsafe Trait?


#18

I guess? My question is how that’s useful, given that we’d always want the masked version of this.

What’s T: unsafe Trait? Do you mean T: Trait where unsafe trait Trait { ... } ? That’s not at all an unsafe bound though! Quite the contrary, it means the function can rely on additional invariants, specific to the trait at hand.


#19

Nope; T: unsafe Trait would make calling any of T as Traits methods unsafe. The item that says T: unsafe Trait is now obliged to define, such as in documentation, the conditions under which calling Ts method leads to memory unsafety and what invariants the caller must uphold… It may be a bad idea, but it’s an idea =)


#20

After reading @RalfJung’s excellent blog post (linked above, too), I think I have a better understanding of unsafe.

However, I would still differ with @Lokathor’s summary slightly:

So, could we summarize that whole thing with “Any time unsafe is on a Trait the implementer must verify it for safety, any time unsafe is on a function or method (trait or inherent) the caller must verify it for safety at each use.” Is that correct?

I still feel that all unsafe items behave basically the same way:

  • unsafe (on a trait or fn) indicates that the corresponding code has the potential to be unsafe by violating an invariant, and the compiler cannot check it.
  • The invariant is not necessarily defined by the code marked unsafe. i.e. unsafe doesn’t mean "I’m introducing a new invariant. (I was somewhat missing this.)
  • unsafe (on a trait of fn) indicates that usage of the trait or fn should be safe (assuming no bugs) iff the user of said trait or fn also upholds said invariants.
  • The user makes this promise by using unsafe blocks (for an unsafe fn) or unsafe impl (an unsafe trait).
    • I find it easier to think of unsafe impl as a user than an implementor of unsafe trait (contrary to the name “impl”).

So in the end, code that uses code that uses something unsafe doesn’t have to worry about safety, because the unsafe-ness is hidden behind an abstraction boundary. For example,

  • If fn foo uses unsafe fn bar in an unsafe block, callers of foo can assume that foo is safe because foo upholds the invariants of bar, and bar is safe iff foo does so.
  • If struct Foo uses (unsafe impls) unsafe trait Bar, then users of type Foo can assume that Foo is safe because Foo upholds the invariants of Bar, and Bar is safe iff Foo does so.

My point is that traits, methods, and functions are more similar than @Lokathor’s summary suggests…