This post is about an aspect of the RustBelt paper.
Concretely, I’d like to share some of our thoughts on the nature of types and shared references.
Let’s see how well this goes. 
Shared references are an extremely powerful mechanism in the Rust type system, and we’ve had quite some trouble fining a good way for handling them in our formal model. In this post, I will present the model that we came up with.
https://www.ralfj.de/blog/2018/01/31/sharing-for-a-lifetime.html
Well done! I feel like this is a good summary for someone who is unfamiliar with how exactly you go about proving this stuff. A step closer to reading the actual paper, I hope.
I’m especially interested in the bit at the end about Cell and modes. A few ideas have been floating around in my head for a while: You can get back most “normal”-feeling shared mutation by wrapping leaf fields of structs in Cell (and the rest by using Rc around allocations and enums). You can safely convert &Cell<[T]> to &[Cell<T>], and other forms of “pushing Cell in a layer,” because not all internal references can be invalidated by shared mutation. And, Cell (really UnsafeCell) is truly a language primitive and not just something you can do yourself with unsafe code.
So I started thinking about the implications of a &cell reference type. Ideally you’d be able to call methods on shared mutable data without sprinkling Cell into your actual data structures. The obstacle is that &cell Ts and &Ts to the same value can’t coexist, which means every method would have to pick one or the other, losing the nice property of &T as a relatively “universal” argument type.
Backwards incompatibly, you could go farther and add a &const reference type, which could coexist with &cell, and could replace &T as a good default choice. But compatibility aside, that’s still a lot of reference types…
I’m curious if you’ve had any thoughts in this direction as part of your research. I would love to figure out some ways to make Cell more applicable and easier to use.
Great post as always. One thing that I found interesting was your discussion around different kinds of variance – one for owning and one for borrowing. I too have thought about that from time to time. Because & freezes, it so happens that – in the absence of Cell – using the “sharing variance” for everything mostly works out, but when it doesn’t, it can be annoying.
One particularly annoying case I have found involves the use &mut, which winds up forcing you to gradually accumulate more and more lifetime parameters. For example, in the compiler, we have this base context, the query context. Let’s say it’s type was this &'cx QueryContext<'qcx> (the actual type is different, but this version is better for the purposes of this exposition). Here 'qcx represents the lifetime of the global memory arena, and things tend to be invariant in it due to shared mutability and so forth. Note that this is a shared reference – this is because the qcx is used so omnipresently.
Now we want to make some analysis, and it needs to keep a reference to the tcx. So it looks like this:
struct TypeCheckContext<'cx, 'qcx> {
qcx: &'cx QueryContext<'qcx>,
}
Now, often, it turns out that the TypeCheckContext might need to store some additional references. For example, maybe it accumulates a list of errors. These references can also be given the 'cx lifetime. In effect, 'cx becomes kind of the lifetime of the “type check context” (which is shorter than the lifetime of the QueryContext as a whole):
struct TypeCheckContext<'cx, 'qcx> {
qcx: &'cx QueryContext<'qcx>,
errors: &'cx mut Vec<Error>,
}
This means I can create and use a type-check context like so, which is convenient:
fn type_check(qcx: &QueryContext<'_>) {
let mut errors = vec![];
let typeckcx = TypeCheckContext { qcx, errors: &mut errors };
...
}
Now maybe I wind up creating another layer of context, let’s call it the MethodCallContext. Let’s say, moreover, that I am trying to pass the TypeCheckContext using &mut – this is likely true, because otherwise I wouldn’t be able to (say) push things onto the &mut Vec<Error> contained within. If I try to use the same pattern, though, where I have the “named, invariant” lifetime 'tcx and the “temporary lifetime” 'cx, things go wrong:
struct MethodCallContext<'cx, 'qcx> {
typeck_context: &'cx mut TypeCheckContext<'cx, 'qcx>,
...
}
But here I run into trouble! The problem is that &mut T is invariant with respect to T, and hence 'cx is invariant. Therefore, I can’t re-use it as the “lifetime of this inner context”. I need to make a separate parameter:
struct MethodCallContext<'cx, 'cx1, 'qcx> {
typeck_context: &'cx mut TypeCheckContext<'cx1, 'qcx>,
...
}
You start to see why this is annoying now. =) These can really build up.
So why is &mut T invariant with respect to T? It’s different from Cell<T> – sort of the inverse. After all, you can mutate an &mut T only when you have a unique path (and then, the alias we are concerned about is the original owner, who expects to recover the referent with its original type).
Sometimes I tinker with the idea of &uniq references. These would be like &mut but with a crucial difference – you cannot mutate the referent directly. Instead, you can declare mut fields in structs, and those fields can be mutated. So if I had:
struct Foo {
a: u32,
mut b: u32,
}
and a variable foo: &uniq Foo, then foo.a += 1 is an error, but foo.b += 1 is ok.
If we had this scheme and we combined it with a notion of multiple kinds of variance, then conceivably we could do:
struct MethodCallContext<'cx, 'qcx> {
typeck_context: &'cx uniq TypeCheckContext<'cx, 'qcx>,
...
}
where TypeCheckContext would not be invariant with respect to 'cx, because it too avoids mut fields.
This is where I start to go off the rails. It seems to me that this notion of &uniq would be very, very useful – in fact, most of the times we take an &mut, we probably only need &uniq. But if you really chase this road, though, I think you arrive at a place where &mut ought to be basically removed from the language and replaced with &uniq. Instead of let mut x = 3 you would have some kind of UniqCell, more like the Ref type in Ocaml:
struct UniqCell<T> {
pub mut value: T
}
so that I would do let x = UniqCell::new(3); and then x.value += 1. Maybe we could do some syntactic sugar.
And here ends my fever dream. I haven’t figured out any path from “here to there” that doesn’t involve massive churn. (Maybe there’s a way to do a transition over various epochs, haven’t thought that hard about it.)
Another reason I would like this scheme:
If you had
struct Foo {
x: X,
mut y: Y
}
and foo: &uniq Foo, then a shared borrow of &foo.x could overlap with &foo without danger (UPDATE: this isn't quite right, see responses below). This would make code like this work out fine:
impl Foo {
fn compute_y(&uniq self, data: &X) {
self.y = ...;
}
fn invokes(&uniq self) {
self.compute_y(&self.x);
}
}
Here, the borrow of &self.x doesn't conflict with the &uniq *self. However, I realize now that this does not permit the following, which I think is what you actually want:
impl Foo {
fn get_x(&self) -> &X { &self.x }
fn compute_y(&uniq self, data: &X) {
self.y = ...;
}
fn invokes(&uniq self) {
self.compute_y(self.get_x());
}
}
For that, we want something else (as has been discussed in other threads).
@nikomatsakis Interesting!
Can you elaborate on how/why it is simultaneously true that (a) &uniq would get to be covariant and (b) replacing &mut with &uniq plus mut fields would not lose any expressiveness? This seems vaguely surprising to me ("something for nothing"). The individual pieces make sense, but I need a bit of help following them to the conclusions. : )
Is this because shared references would not be permitted to read from mut fields, or...?
&uniq would be covariant for fields not tagged as mut. The thing you are giving up is the ability to do *x = ... with a x: &uniq T.
Sorry, I had a typo there. I should have said &foo.x does not have to conflict with &uniq *foo, presuming x is not a mut field. However, I now see that this is somewhat bogus =) it only works if the value itself has no mut fields transitively. Interesting.
Well, one more strike against uniq...
Oh, no, I remember now. I think that &uniq foo.x would also be illegal if the field itself is not mut. Or at least that would have to be. Seems odd now though =) although it is somewhat similar to the way that you can only do &x borrow of a non-mut local variable.
Sorry, maybe I'm being dense: what does it mean to be... covariant for fields? I thought we were talking about &uniq T being covariant in T. That has to hold (or not) independently of what fields T may have...?
Hmm, I see. And since assignment cannot change the type of a field, the type of the whole result cannot possibly change. And one thing you're giving up is that non-mut fields must be truly immutable, and can't be mutated any way, any how? (Is that the only thing? I'm thinking less in terms of "operations you can't perform", and more "things you simply cannot express".)
Okay... &uniq *foo is a reborrow of foo... what's the difference that that's making here?
And... I think I made some kind of brain fart mixing up x and y in my earlier question. (Oops, sorry!) If x is non-mut and "truly immutable" then of course it makes sense why & and &uniq references to it could coexist. (Unless of course it in turn has mut fields, as you point out - forbidding either &uniq references to non-mut fields or & references to mut ones could work there, I think, as I accidentally suggested).
Well, maybe I'm off my rocker, but I think the idea was something like...
&uniq would be covariant with respect to T. But within a struct, when we compute its variance with respect to its type/lifetime parameters, those parameters that appear in mut fields would be invariant, but those that appear in non-mut fields could be covariant. Hence e.g. in:
struct Foo<'a, 'b> {
foo: &'a u32,
mut bar: &'b u32,
}
Foo would be invariant with respect to 'b but contravariant with respect to 'a. So overall &uniq Foo<'x, 'y> would be invariant with respect to 'y but contravariant with respect to 'x.
But anyway the variance terminology needs a bit of updating to make this work best -- as @RalfJung said, you kind of want distinct variance for a type Foo when it (a) is owned vs (b) shared ref vs (c) unique ref (mut ref is just invariant, that's easy enough I guess).
Sorry to interrupt this conversation, but @RalfJung this is a very, very good post. Multiple good insights here. I have not read the RustBelt paper.
Hmm… I wonder if there’s a less disruptive way to add this functionality.
Suppose that instead of marking mut fields, you mark const fields, and then regular old &mut references become variant in the way you want &uniq to be.
The problem would be the expectation that given x: &mut T and y: T, you can always say *x = y, or swap(x, &mut y), etc. But that sounds a lot like the existing need for immovable types! Perhaps a type with const fields is automatically immovable, using whatever solution we end up with for that, and then there’s some way to get a movable (but invariant) ‘view’ of the type if you really need it…
Just a thought.
@rpjohnst was kind enough to bring your post to my attention, as he knows I have been working on similar issues via a different approach. I admire the clarity of your writing and the insights you make. I have several observations to offer…
Applying this thought process back to Rust, we can now detect “type safety” holes in the large. Imagine a struct of two elements: a and b, both i32, but with the semantic dependency constraint that a<=b. Semantically, the Rust compiler is unaware of the constraint and cannot protect us from its violation. However, I could use Cell or private fields/methods to program an isolation layer. However, if a dependency exists between data in different structs, the challenge for the compiler becomes a lot more complicated.
The reason that we are more careful protecting dependency constraints with references, Vec and sum types is because the consequences of failure is more obvious and potentially catastrophic: bad pointers and truly nonsensical data. But from a broader perspective, if we want to slowly improve the type safety of our compilers to these other forms of dependent types, it could be potentially valuable to at least mark the dependencies between data fields, so that the compiler can protect or warn us of operations that could violate these constraints, enabling us to be careful in isolating those operations behind some barrier.
The variations of reference “modes” that you and others have mentioned (e.g. &cell, &const, &uniq) reminds me of work from the Pony language and the Midori project. In Pony, a comparable concept is its reference capabilities - roughly &cell corresponds to ref, &mut to iso and & to box (and there are three others: val, tag and trn). Sylvan Clebsch actually did a formal proof of the correctness of his reference capabilities as part of his PhD, followed on by later refinements by George ?. There are important differences between Pony and Rust that simplified the problem for him: a) restrictions on what a reference may point to within an object b) no borrowed references and a very simplified lifetime construct - the lexical recover block and c) the lack of cross-thread mutable synchronization mechanisms.
I am working on my own language (Cone) which is attempting to marry together many great ideas in Rust with those found in Pony. Instead of what I call onion typing using wrappers (e.g., Rc<RefCell>), I am exploring an approach where references carry three pieces of type information side-by-side: <allocator or lifetime, permission, and value type>. My permissions are roughly analogous to what you call reference modes and Pony’s reference capabilities, but also include thread-synchronized permissions.
Since I want Cone to dive deeper in systems programming than Pony did, I - like Rust - need to handle precisely the safety issues you raise here, via built-in constraints to permissions. The choice of value types (e.g., sum types) restricts which permissions are safe (e.g., unconstrained shared mutability). It was an interesting and surprising result for me as well, but an unavoidable one.
So, with Cone, the aggregate constraints on a reference are those distinctly contributed by its individual parts: permissions, value types and allocator/lifetime, mostly but not entirely orthogonally. I would be happy to share more details if it interests you, to the degree that I have worked it out. I am in the middle of building the compiler to verify the approach is feasible. A lot of the design is in place, however I am quite sure I will know for sure how it needs to work only when I get to the other side of that work.
Thanks for a fascinating read.
Thanks a lot for all your thoughtful replies. 
Would this be meaningfully different from &Cell<T>? Sounds to me like this would mostly let the compiler automatically apply all sorts of structural properties of Cell propagating into arrays and structs (but NOT enums!), without actually changing what the type "means".
Thinking about it, the same is true for Cell<Rc<T>>::clone and Cell<Option<T>>::is_none, I think. So maybe this is not as much a mode as a type with plenty of structural properties that we cannot currently exploit.
I'm not so sure it would be a good choice. I actually really like the fact that &T means I can rely on it not being changed (at least if I know a bit about T and hence can exclude interior mutability). That makes reasoning about the code so much easier. It also enables optimizations. Reverting back to C's "you can't mutate but others can" is much weaker.
On the other hand, whenever you do have a Cell, this lack of available operations could be very annoying. I'm imagining Option::is_none taking a &const and then automagically working for &T and &Cell<T> in a safe way; that seems quite neat. Similar for Rc::clone.
I don't think I understand what you are saying here. Cells are sharing-invariant, so using the "sharing variance" also works out here...? It's just inconvenient if you're not actually sharing.
I'm right now wondering the same thing. If I think of a situation where all fields are mut, then &uniq and &mut still have different rules (&uniq is covariant), but I can implement *x = y (with x: &uniq) by just copying all the fields individually. I guess this would not work because UniqCell is (uniq-)invariant wrt. T? So we'd actually lose covariance of (mutable fields of) products/struct in this "mode"! But, this doesn't actually lose much because this only applies below &uniq, and if it were &mut instead we'd have complete invariance.
So, I think I'd describe this mode as "&uniq of a struct is essentially the shared mode for all non-mut fields, and a mutable borrow of mut fields". We'd have to think about cases like &uniq &mut (probably essentially the same as &uniq &uniq?), &uniq & (very similar to &&?), &uniq Box (like &uniq &uniq?).
With such a model it seems reasonable to have &uniq foo coexist with &foo.x if x is non-mut (but NOT with &uniq foo.x, as you noted). The name uniq is somewhat... misleading though in this case. 
(I find this one easier to think and reason about "check structurally if there's any nested mut; such a syntactic check would not go well with generic types. We'd need a new type bound saying "The uniq mode of this type is actually completely shared" and all sorts of infrastructure like that...)
I have been giving some thought to "is &mut a mode?", and so far I've managed to avoid that -- it's not a mode in my current model, but uniformly defined in terms of full ownership. However, some time this year I plan to come back to mut as a mode because at least in the current formal model I'm using, I'll probably need to do something like that to be able to handle pointer dereferences in paths. (I will try to liken &'static mut with full ownership... let's see how that works out.) The thing that will restrict this mode is something like a "universal property" which falls out of the fact that *x = ... has to work whenever x: &mut -- but if it weren't for these universal operations, one could actually have a type whose &mut mode has some fields read-only and in their "shared" mode. Not sure if that's related to your question about how to go from "here to there", just came to my mind.
I agree with your observation. However, I don't think I understand what it is that you think should be done. Vec is already an unsafely implemented library type, demonstrating that having invariants whose violation results in undefined behavior is supported by Rust. Are you saying we should have a type system that's expressive enough to actually implement Vec without unsafe? You brought up dependent types, so I guess that's what you are thinking about here. I think it would indeed be great if that was possible, but with the current state of research I also think these proofs are still way too complicated to be realistically performed as part of normal development. We'd have to make some great advances in automated and interactive program verification to make this usable, I think. I agree with the goal though
Have you heard of the "unsafe fields" proposal? This doesn't tell the compiler about dependencies between fields, it just informs the compiler that some fields are special in that something depends on them so "please be careful". That already goes a long way though I think; I don't see right now how mere dependency information (as opposed to actual invariants) could help.
Thanks, I'll check those out! Capabilities usually refer to something slightly different and don't structurally depend on a type, but maybe they've extended the concept to this extend.
Sounds like you are doing some exciting language design and research and Cone, awesome! If you've written anything up, feel free to send it to me though I can't promise I will be able to give any in-depth comments. So, if it's still all in flux, it may make more sense to wait a bit until you're more certain of the overall design.
Yes, that's pretty much how I think about it as well. Propagating Cell into structs feels like the general case of Cell<Rc<T>>::clone and Cell<Option<T>>::is_none- they just so happen to restrict themselves from using the full abilities of &T, and only create internal references that remain safe in the case of the overall structure being overwritten.
One extension that might move &cell T closer to a mode than syntactic sugar for &Cell<T> would be to allow it to propagate into enums (and things like Box and Vec). This would restrict its ability to mutate those values, and in return grant the ability to mutate their contents. I'm not totally sure how useful this is, because it prevents a lot of useful operations, and you can get closer to "normal" mutability by wrapping/replacing those things with Rc instead anyway.
Agreed completely. One thing I just realized is &const would need to have the same structural properties as &Cell<T>, so it wouldn't be able to propagate into enums either without the above extension... making it significantly less useful than &T as a "universal" argument type than I initially imagined.
Can you elaborate on what you mean here? Just outright forbidding &cell from mutating any enums or Boxes would be problematic of course (due to generics if nothing else). But you also can't say "just not that particular Box" like with &mut borrowing ("propagation") due to aliasing.
The former. The mechanics of enforcing it certainly aren't trivial- I imagine you might use a trait to mark whether something can be safely overwritten in the presence of internal references, making the interaction between &cell and generic types somewhat tedious. And regardless of how easy/possible it is to enforce, it's a pretty big restriction anyway.
I can see that for is_none, but for clone I disagree that propagating into structs is a generalization. Rc has custom private invariants on its field; those types would not get automatic structural rules as that could well be unsound (imagine someone implementing something enum like on a struct wrapping a byte array). This is similar to how structural derivation of auto traits on types with private invariants can be harmful.
&const could still allow inspecting the discriminant of the enum, so it'd be enough to implement is_none. However, for Rc::clone, you should still need some unsafe code asserting that this actually does not break Rc's invariants.
In fact, &const could even allow copying out Copy data from enum variants, or from Vec fields, or similar; but not getting any references into them. So, in some sense this another kind of restriction that shared C-like pointers can have to make them safe:
&T.Send) and disallow getting references to data that could "go away", like below an enum. This is &cell T.How would that work? Are you thinking of types having the property "if you overwrite data of this type, all internal pointers that were previously valid are still valid"? i32 and friends have that property; struct preserves it, enum does not if any variant contains data. I can imagine this could be made sound, but when would it be useful?
I'm not sure it would, it was just a variation that came to mind. It would be even less useful in the presence of what you described here:
I suppose that would mean somehow separating the ability to read/write something from the ability to take a reference to it, moreso than they already are.
This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.