Today, if you do a mutable borrow of a local variable, you lose the ability to write to that variable except through the new reference you just created:
let mut x = 3;
let p = &mut x;
x += 1; // Error
*p += 1; // OK
However, you retain the ability to read the original variable:
let mut x = 3;
let p = &mut x;
print(x); // OK
print(*p); // OK
I would like to change the borrow checker rules so that both writes
and reads through the original path x are illegal while x is
mutably borrowed. This change is not motivated by soundness, as I
believe the current rules are sound. Rather, the motivation is that
this change gives strong guarantees to the holder of an &mut
pointer: at present, they can assume that an &mut referent will not
be changed by anyone else. With this change, they can also assume
that an &mut referent will not be read by anyone else. This enable
more flexible borrowing rules and a more flexible kind of data
parallelism API than what is possible today. It may also help to
create more flexible rules around moves of borrowed data. As a side
benefit, I personally think it also makes the borrow checker rules
more consistent (mutable borrows mean original value is not usable
during the mutable borrow, end of story). Let me lead with the
motivation.
In a previous post I outlined a plan for data parallelism in Rust based on closure bounds. The rough idea is to leverage the checks that the borrow checker already does for segregating state into mutable-and-non-aliasable and immutable-but-aliasable. This is not only the recipe for creating memory safe programs, but it is also the recipe for data-race freedom: we can permit data to be shared between tasks, so long as it is immutable.
The API that I outlined in that previous post was based on a fork_join
function that took an array of closures. You would use it like this:
fn sum(x: &[int]) {
if x.len() == 0 {
return 0;
}
let mid = x.len() / 2;
let mut left = 0;
let mut right = 0;
fork_join([
|| left = sum(x.slice(0, mid)),
|| right = sum(x.slice(mid, x.len())),
]);
return left + right;
}
The idea of fork_join was that it would (potentially) fork into N
threads, one for each closure, and execute them in parallel. These
closures may access and even mutate state from the containing scope --
the normal borrow checker rules will ensure that, if one closure
mutates a variable, the other closures cannot read or write it. In
this example, that means that the first closure can mutate left so
long as the second closure doesn't touch it (and vice versa for
right). Note that both closures share access to x, and this is
fine because x is immutable.
This kind of API isn't safe for all data though. There are things that
cannot be shared in this way. One example is Cell, which is Rust's
way of cheating the mutability rules and making a value that is
always mutable. If we permitted two threads to touch the same
Cell, they could both try to read and write it and, since Cell
does not employ locks, this would not be race free.
To avoid these sorts of cases, the closures that you pass to to
fork_join would be bounded by the builtin trait Share. As I
wrote in issue 11781, the trait Share indicates data that
is threadsafe when accessed through an &T reference (i.e., when
aliased).
Most data is sharable (let T stand for some other sharable type):
- POD (plain old data) types are forkable, so things like
intetc. &Tand&mut T, because both are immutable when aliased.~Tis sharable, because is is not aliasable.- Structs and enums that are composed of sharable data are sharable.
ARC, because the reference count is maintained atomically.- The various thread-safe atomic integer intrinsics and so on.
Things which are not sharable include:
- Many types that are unsafely implemented:
CellandRefCell, which have non-atomic interior mutabilityRc, which uses non-atomic reference counting
- Managed data (
Gc<T>) because we do not wish to maintain or support a cross-thread garbage collector
There is a wrinkle though. With the current borrow checker rules, forkable data is only safe to access from a parallel thread if the main thread is suspended. Put another way, forkable closures can only run concurrently with other forkable closures, but not with the parent, which might not be a forkable thing.
This is reflected in the API, which consisted of a function
fork_join function that both spawned the threads and joined them.
The natural semantics of a function call would thus cause the parent
to block while the threads executed. For many use cases, this is just
fine, but there are other cases where it's nice to be able to fork off
threads continuously, allowing the parent to keep running in the
meantime.
Note: This is a refinement of the previous proposal, which was more complex. The version presented here is simpler but equally expressive. It will work best when combined with my (ill documented, that's coming) plans for unboxed closures, which are required to support convenient array map operations and so forth.
If we made the change that I described above -- that is, we prohibit
reads of data that is mutably borrowed -- then we could adjust the
fork_join API to be more flexible. In particular, we could support
an API like the following:
fn sum(x: &[int]) {
if x.len() == 0 {
return 0;
}
let mid = x.len() / 2;
let mut left = 0;
let mut right = 0;
fork_join_section(|sched| {
sched.fork(|| left = sum(x.slice(0, mid)));
sched.fork(|| right = sum(x.slice(mid, x.len())));
});
return left + right;
}
The idea here is that we replaced the fork_join() call with a call
to fork_join_section(). This function takes a closure argument and
passes it a an argument sched -- a scheduler. The scheduler offers a
method fork that can be invoked to fork off a potentially parallel
task. This task may begin execution immediately and will be joined
once the fork_join_section ends.
In some sense this is just a more verbose replacement for the previous
call, and I imagine that the fork_join() function I showed
originally will remain as a convenience function. But in another sense
this new version is much more flexible -- it can be used to fork off
any number of tasks, for example, and it permits the main thread to
continue executing while the fork runs.
An aside: it should be noted that this API also opens the door (wider) to a kind of anti-pattern, in which the main thread quickly enqueues a ton of small tasks before it begins to operate on them. This is the opposite of what (e.g.) Cilk would do. In Cilk, the processor would immediately begin executing the forked task, leaving the rest of the "forking" in a stealable thunk. If you're lucky, some other proc will come along and do the forking for you. This can reduce overall overhead. But anyway, this is fairly orthogonal.
The stronger guarantee concerning &mut will be useful in other
scenarios. One example that comes to mind are moves: for example,
today we do not permit moves out of borrowed data. In principle,
though, we should be able to permit moves out of &mut data, so long
as the value is replaced before anyone can read it.
Without the rule I am proposing here, though, it's really hard to prevent reads at all without tracking what pointers point at (which we do not do nor want to do, generally). Consider even a simple program like the following:
let x = ~3;
let y = &mut x;
let z = *y; // Moves out of `*y` (and `*x`, therefore)
let _ = *x; // Error! `*x` is invalid.
*y = ~5; // Replaces `*y`
I don't want to dive into the details of moves here, because permitting rules from borrowed pointers is a complex topic of its own (we must consider, for example, failure and what happens when destructors run). But without the proposal here, I think we can't even get started.
Speaking more generally and mildly more theoretically, this rule helps
to align Rust logic with separation logic. Effectively, &mut
references are known to be separated from the rest of the heap. This is
similar to what research languages like Mezzo do. (By the way,
if you are not familiar with Mezzo, check it out. Awesome stuff.)
It's hard to say what quantity of existing code relies on the current rules. My gut tells me "not much" but without implementing the change I can't say for certain.
Implementing this rule requires a certain amount of refactoring in the borrow checker (refactoring that is needed for other reasons as well, however). In the interest of actually completing this blog post, I'm not going to go into more details (the post has been sitting for some time waiting for me to have time to write this section). If you think you might like to implement this change, though, let me know. =)