Blog post: observatonal equivalence and unsafe code

[pythonesque]

One concern I have with this article is that I feel like it doesn’t explicitly state that these rules only apply to abstraction boundaries between safe and unsafe code. That is, I should hope that setjmp / longjmp are usable within an unsafe function (since the caller is then responsible for making sure that it doesn’t do anything like what Rayon does).

I also think you are missing some useful unsafe abstractions. Page table remapping can allow two physical addresses to point to the same memory, an important optimization in some new in-memory databases (breaks various sorts of optimizations that depend on exact address comparison, among other things). Nontemporal streaming loads and stores, as well as burst mode writes, have extremely weird consistency semantics and are probably also not replicable in safe code. Certain types of DMA likely enforce new restrictions on unsafe code. And so on.

I recall that mem::swap also adds a new capability (the ability to call drop on a type T when you only have &mut T, possibly? It was a while ago). Not sure if something else in your article already implies it (it wouldn’t surprise me if Vec can emulate swap).

I also think there are a handful of hardware features that can increase the amount you can safely abstract. In particular, on hardware with known cycle-accurate timing and/or direct-mapped scratchpads, you can safely interleave instructions across hardware threads on the same data without the possibility of data races (especially if you can know that you’re the only process pinned to a core–something else that it is currently not possible to express in safe Rust, to my knowledge).

To be clear, I’m not convinced all of these can be wrapped in a completely safe abstraction (at least, not a process-level abstraction), but I definitely think they are useful things to be able to do in Rust.

[Diggsey]

I’m not sure it makes sense to talk about these things as “levels” - Cell does not require heap allocation for example. They are separate “features” which go above and beyond Rust0, and in some cases they are related. It could be the case that one feature builds upon another, but it could equally be the case that two features are mutually exclusive, and that you can only choose one.

For example, scoped_thread_local, as it was implemented, was unsafe in the presence of coroutines, and yet both of those things are “valid” extensions to Rust0 on their own. To avoid an explosion of marker traits like Send, rust will either have to become opinionated (via the unsafe code guidelines) about which of these exclusive features are valid, or else have it be configured at compile time and accept that you can’t combine two libraries relying on incompatible features.

[asajeffrey]

A minor nitpick: rather than observational equivalence, I think we might want to work with observational refinement. This defined in a very similar way to observational equvalence: P ⊑ Q whevever, for any context C, any observable behaviour of C[Q] is an observable bahvaviour of C[P].

The reason for being interested in observational refinement is that there are some optimizations that are only valid in one direction, for example let x=a.load(Relaxed); let y = a.load(Relaxed); ... ⊑ let x=a.load(Relaxed); let y = x; ... is a perfectly valid optimization, as it is removing possible behaviour.

A possible way to go would be to say P appears safe if there is some safe Q such that Q ⊑ P. This depends on language level in two ways: a) we are asking Q to be safe, and b) when we are quantifying over C, we might want to restrict ourselves to safe contexts.

One nice property of this defn is that (er I think) it’s compositional: if P appears safe and Q appears safe, then P∥Q appears safe.

Also, if we define CHAOS to be the most nondeterministic safe program, then any safe Q has CHAOS ⊑ Q, which means that P appears safe iff CHAOS ⊑ P.

[nikomatsakis]

On another note, if I understood some recent discussion about async/await properly, then this is incompatible with scoped threads. That would then be another example of two extensions to what is deemed “safe” (i.e., neither of them can be simulated with just safe Rust5) that are mutually exclusive.

I feel like the details matter here a lot. Do you have a link to said discussion, or can you say more about what made async/await incompatible? Maybe you are referring to this Reddit thread talking about coroutines? (which I also linked to from the post)

In any case, what @Amanieu wrote seems correct:

If you are using stackful coroutines then all you need to do is make sure you unwind the coroutine’s stack before you destroy it. This will run the scope destructor, which will in turn block until scoped threads have finished running.

This seems right. You can’t free the stack frames until you unwind, though you could leak them forever.

[nikomatsakis]

[T] is, of course, already special in itself, but replacing it with a trait containing only len and index_mut should enable safe Rust to provide observationally equivalent impls of it.

This confuses me a bit. [T] is not “unsafe” Rust, right? I guess you mean the various methods that exist (like len()) on [T], which are implemented unsafely? You’re right that I overlooked those, I considered them part of Rust0 I suppose. =)

mem::swap is probably more interesting because it feels like we could just make it a trait fn and auto-implement it for any safe type, which would work except for anything containing &mut.

Yes, it seems like there are a small number of such functions (similar to len) that are probably a better Rust1 than “access to the heap”.

By using the latter to create a singly-linked list type, and given the abstracted [T] trait I’ve described above, shouldn’t contiguous and non-contiguous lists be observationally equal to safe Rust (except for pointer comparisons, which I assume would break many other supposed equalities)?

Well, my point was that you can (in Rust0 – with no unsafe code at all) create a &[T] and dereference into it, like so:

fn foo() {
    let x: [i32; 5] = [0, 1, 2, 3, 4];
    bar(&x);
}

fn bar(x: &[i32]) {
    x[2]
}

Doing this coercion requires implementing the Unsize trait, but that is not unsafe to do. The actual code for performing said coercion is builtin into the core Rust language (Rust0), as is the code for bounds checking and indexing. So it seems to me that you really do have to provide adjacent memory, at least if you want to mirror the current setup. But it seems to me to be a minor point – and I could imagine some of this code moving out of the compiler, if we ever found a nice way to do it.

Moving up to Rust2 would be as easy as assuming Rc<T> = Arc<T> = T for me, which, again assuming T does not contain any &mut, should be a safe axiomatization.

I’m confused by a few things here. First, why can you assume T does not contain &mut? Also, how do you address the point I raised in my post: that Rc<T> can be applied to any T, not just T: Clone, and that this cannot be implemented in general without true sharing?

Maybe I don’t really understand your project though =). I guess it is trying to axiomatize a subset of Rust, more than the full Rust language?

[nikomatsakis]

Heh, I had forgotten that (again), but yes. =) Still, you could (in principle) change the signature, if you wanted. It’s just probably a bad idea.

[nikomatsakis]

The problem is that there’s a trade off between different language extensions, which are safe in the presence of the base language (RustN of some N) but not safe in the presence of each other.

Are you saying that this is a problem with my post? I think this is precisely what I was trying to get at. I also think that in drafting unsafe code guidelines, we are going to have to make some choices. I don’t yet know how to deal with irreconcilable unsafe code (e.g., setjmp vs rayon). I can imagine that in some projects one or the other might be essential, so it’s not entirely clear that we can pick a winner (and, as I pointed out, some constraints might not be relevant in all contexts).

But perhaps drilling more into these areas can give us a framework by which unsafe code can declare its compatibility requirements, so we can at least tell you when two extensions are incompatible. And then we might have a kind of “core set” of unsafe abstractions that programs opt into by default – if you are incompatible with this level, that will narrow the set of people that can use you.

This seems to me to be not unlike libstd or any other similar portability hazard. I feel like I keep coming back to this same basic approach in a number of contexts.

[nikomatsakis]

One concern I have with this article is that I feel like it doesn’t explicitly state that these rules only apply to abstraction boundaries between safe and unsafe code. That is, I should hope that setjmp / longjmp are usable within an unsafe function (since the caller is then responsible for making sure that it doesn’t do anything like what Rayon does).

Ah yes, I actually meant to write about that specific point, but I guess I forgot to do so. =) Perhaps in a follow-up.

I also think you are missing some useful unsafe abstractions.

Indeed, I made no claim to completeness. =) Those are good examples though. It seems obvious that we won’t want to include every random memory model thing that hardware can produce though.

I also think there are a handful of hardware features that can increase the amount you can safely abstract. In particular, on hardware with known cycle-accurate timing and/or direct-mapped scratchpads, you can safely interleave instructions across hardware threads on the same data without the possibility of data races…To be clear, I’m not convinced all of these can be wrapped in a completely safe abstraction (at least, not a process-level abstraction), but I definitely think they are useful things to be able to do in Rust.

It seems like here you are talking about tricks unsafe code could play without fear of “detection” by safe code? Statements like this last one feel a bit ambiguous to me. =)

In any case, diving into some of the more esoteric frontiers of what hardware has to offer like this seems interesting to me. I was not aware of a number of these extensions you mention. Certainly my biggest concern with trying to enumerate what unsafe code can do is that we limit ourselves – and yet if we don’t enumerate what unsafe code can do, then of course we are also limiting ourselves.

Having some notion that we will describe ways for unsafe code to declare its compatibility does seem to offer an escape valve.

It’s not clear to me how urgent this problem is, but then again it has already arisen (in the form of coroutines). Perhaps a reasonable starting point would be to try and enumerate the various capabilities we know of across libstd and unsafe code, and encourage people to think about which of those capabilities would be sufficient to model the unsafe code in question, even if this is just documentation to start. This would be a starting point at least.

[nikomatsakis]

I’m not sure it makes sense to talk about these things as “levels” - Cell does not require heap allocation for example.

Agreed, it’s more of a DAG.

[withoutboats]

I think I was really just re-stating your post more than anything else.

[Kha]

[quote=“nikomatsakis, post:13, topic:4148”]

[T] is, of course, already special in itself, but replacing it with a trait containing only len and index_mut should enable safe Rust to provide observationally equivalent impls of it.

This confuses me a bit. [T] is not “unsafe” Rust, right?[/quote] I’d argue it’s still special in that there’s no safe way to construct a &[T] (except for the array coercion, I forgot about that). If we replaced it with the mentioned trait, we could safely implement [T] for [T; $N] in Rust0 and for Vec<T> in Rust1, with trait object coercion replacing the builtin array/Vec’s Deref coercion. This might not be very useful (even if safe Rust cannot distinguish it from contiguous memory, we’d still like to have that assumption for unsafe code) and, as you said, a minor point, it’s just something I was thinking about to make Rust0 smaller.

Maybe I don’t really understand your project though =). I guess it is trying to axiomatize a subset of Rust, more than the full Rust language?

Yeah, I’m focusing on a reasonable subset of safe Rust that actually allows me to verify a few programs in 6 months’ time. If I ever have the chance in the future, I’d love to do something like seL4’s AutoCorres project, starting at a full semantics and memory model of Rust (as soon as we have those things ), then doing verified transformations to a simpler and simpler language. But for this masters’ thesis, I’ll just start at the topmost abstraction level and see how far I can get without an explicit heap.

Moving up to Rust2 would be as easy as assuming Rc<T> = Arc<T> = T for me, which, again assuming T does not contain any &mut, should be a safe axiomatization.

I’m confused by a few things here. First, why can you assume T does not contain &mut? Also, how do you address the point I raised in my post: that Rc<T> can be applied to any T, not just T: Clone, and that this cannot be implemented in general without true sharing?

I’m not sure why I mentioned &mut here. As long as T doesn’t contain any UnsafeCell (which it won’t, since there’s no way it can axiomatize that one), I can assume it’s immutable inside Rc/Arc and axiomatize Rc::clone as just returning self - there are no affine types in my target language Lean.

All in all, my project probably isn’t too relevant to the Rust semantics discussions since it only touches the parts of the semantics everyone is already agreeing on. Still, I wanted to show that there basically exists an implementation of the language levels design, so (to me) it’s not a purely theoretic discussion (though still academic ).

[nikomatsakis]

A minor nitpick: rather than observational equivalence, I think we might want to work with observational refinement. This defined in a very similar way to observational equvalence: P ⊑ Q whevever, for any context C, any observable behaviour of C[Q] is an observable bahvaviour of C[P].

I have more questions, but let me start here to buy myself time to think. =) Do you have this backwards: “any observable behavior of C[Q] is an observable behavior of C[P]”? I am just surprised because the P ⊑ Q notation suggests “P subset of Q” to me, but it seems that the behavior of Q is in fact a subset of P?

[asajeffrey]

There’s an annoying clash of notation here, P ⊑ Q is read as “P is less deterministic than Q”, or “P is less defined than Q”, which rather annoyingly means it has more behaviour. In many models, P ⊑ Q iff ⟦P⟧ ⊇ ⟦Q⟧. Sigh. (If you want the history for this, it’s essentially the Smyth powerdomain https://en.wikipedia.org/wiki/Power_domains which is the model of nondeterminism you get for observational refinement.)

[NXTangl]

There’s an annoying clash of notation here, P ⊑ Q is read as “P is less deterministic than Q”, or “P is less defined than Q”, which rather annoyingly means it has more behaviour. In many models, P ⊑ Q iff ⟦P⟧ ⊇ ⟦Q⟧. Sigh. (If you want the history for this, it’s essentially the Smyth powerdomain https://en.wikipedia.org/wiki/Power_domains which is the model of nondeterminism you get for observational refinement.)

Good point. I vote we try to refer to this with the standard powerdomain notation, or it’ll be lifetime bound variance all over again…

I guess the way to think of it is that a safe Rust N is isomorphic to a function F: P -> B that maps programs to observed behavior, and thus is naturally contravariant over what types of programs are allowed.

(Of course, as Rust is Turing-complete, we can think of any number of whole-program transforms that allow Rust N to simulate Rust N + 1 , such as rewriting the program into continuation-passing style to avoid using the heap–but obviously that’s a non-local transformation and breaks all our guarantees about what’s allowed and what isn’t.)

[leonardo]

You can restrict the power of a system language to make it easier prove the correctness of the code, keeping the performance reasonable enough to write file systems for a microkernel OS. As explained in this talk, “Refinement through Restraint: Bringing Down the Cost of Verification”:

I think it’s quite related to the tower of Rust0, Rust1, Rust2, etc, you write about.

[nikomatsakis]

You responded too fast. That was supposed to take longer.

So the major thing I have to turn over in my head in this “asymmetric” model is of course that unsafe code wants to assume limits on its context (e.g., my caller won’t be able to observe that I use setjmp/longjmp, because they are not poking about at my stack; or, my caller won’t use setjmp/longjmp themselves). I guess that in your post this is what you meant by part (B) here, right?

A possible way to go would be to say P appears safe if there is some safe Q such that Q ⊑ P. This depends on language level in two ways: a) we are asking Q to be safe, and b) when we are quantifying over C, we might want to restrict ourselves to safe contexts.

[asajeffrey]

I’ll try to be more sluggish in the future.

Yes, when proving that some unsafe code appears safe, we would like to able to do this just quantifying over safe contexts, e.g. which can’t mess around with the call stack. We’d like to know that if P is apparently safe wrt safe contexts, then P is apparently safe to apparently safe contexts.

[RalfJung]

There’s another ingredient typically used when doing refinement – not only does the context have to be safe, it also has to use the “hole” (i.e., the unsafe code) at a particular type. The same piece of code can be safe at one type and unsafe at another type. The type, in some sense, describes the interface between the safe and the unsafe code, it says what the safe code is allowed to do. (This is btw. how I often describe the virtue of Rust to type system people – even though the type checker is fairly limited in what it can understand, and there’s lot of code you can’t write if you follow its rule, the type system is actually pretty expressive without being excessive in terms of number of concepts or so. It can concisely describe complicated contracts like “As you iterate over the Vec, you must not mutate it” or “After you release the Mutex, you must no longer use any pointers you acquires to its interior while you held it”. Then we can put those types at the holes of a safe context and fill the hole with unsafe code that we merely claim has this type; the type checker can check that the user follows the interface we write without having any clue about the subtle invariants it expresses. To me, that’s the true power of Rust.)

There’s an annoying clash of notation here, P ⊑ Q is read as “P is less deterministic than Q”, or “P is less defined than Q”, which rather annoyingly means it has more behaviour. In many models, P ⊑ Q iff ⟦P⟧ ⊇ ⟦Q⟧. Sigh. (If you want the history for this, it’s essentially the Smyth powerdomain https://en.wikipedia.org/wiki/Power_domains which is the model of nondeterminism you get for observational refinement.)

In all the papers I read on contextual refinement, P ⊑ Q means "Every behavior of P is also a behavior of Q" / “P has fewer behaviors than Q” (which is why P is “more refined”), so it corresponds to ⟦P⟧ ⊆ ⟦Q⟧ and the two inclusion actually match up (assuming those semantic brackets give the set of possible behaviors of the program). For example, see page 7 of this paper. A typical way to use this would be start from a “rough sketch” of the program you want, maybe just pre- and postconditions, and then you stepwise refine this until you got a program with the efficiency you want. (There’s people literally doing that in a proof assistant, with the proofs going all the way up to some assembly code.) Clearly, if you do this, you’d only want to remove behaviors and hence make sure that your final program actually satisfies the spec you started with. So, “more refined = fewer behaviors”.

However, I “grew up” in a world dominated by operational, small-step semantics. It is possible that domain theorists use an inverted notation.

[asajeffrey]

Yes, observational refinement/equivalence are typed notions, in that you care about the type of the hole. Part of the challenge here is that unsafe code can bypass the type system, which is part of why unsafe contexts are more powerful than safe ones.

You can probably tell I grew up in a denotational world, I probably got the inverted ordering on refinements from the failures-divergences model of CSP, e.g. p. 5 of Brookes and Roscoe (1985).

[nikomatsakis]

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