I will argue that Stacked Borrows can be viewed as an approximation of a
special kind of re-entrant (reader-writer) lock, where the calls to lock
and
unlock
are hidden, and Stacked Borrows attempts to infer
where they happen. The locking intuition seems like it might be useful for several reasons:
- It directly expresses "aliasing XOR mutability" by the fact that at most one user can hold the write lock at any moment, and any number of users can hold the read lock.
- Thinking of the code as containing invisible
lock
andunlock
calls can make it easier to reason about whether the code satisfies the aliasing rules, because you don't have to understand how Stacked Borrows does the approximation. - It suggests some ways in which Stacked Borrows might be relaxed while (hopefully) still justifying important optimizations.
This section describes how the lock works, and in the next section I will explain how Stacked Borrows can be seen as an approximation of it. In fact, I will not describe the lock in its full generality now, but I will only consider an ordinary exclusive lock instead of a reader-writer lock.
The lock has the following API:
impl Lock {
fn init() -> (ReferenceId, Lock);
fn create_ref(&mut self, parent: ReferenceId) -> ReferenceId;
fn lock(&mut self, r: ReferenceId);
fn unlock(&mut self, r: ReferenceId);
fn use(&mut self, r: ReferenceId);
}
The implementation of the lock is based on the following rules:
- A reference needs to hold the lock (i.e. you must have called
lock
without callingunlock
after) in order to access the memory location (i.e. call theuse
function). - References are organized in a "borrow tree" of parent-child relations
determined by reborrowing (the parent is the original reference and the child is
the reference created by reborrowing). This tree is rooted at the initial
reference returned by
init
and additional children are created usingcreate_ref
. (Similar to retagging in Stacked Borrows and the borrow stack) - It is an error to attempt to take the lock while some other references holds it, unless the current owner is your parent, in which case you temporarily "borrow" the lock from your parent: the parent loses the lock, and gets it back once you call unlock. (This is the "re-entrant" part)
- You can only hold the lock once: i.e., once you
unlock
you can neverlock
again.
Note that it is obvious from these rules that at most one reference holds the lock at each moment in time. Moreover, the borrow tree (rule 2), in combination with rules 3 and 4 ensures that memory accesses are well-bracketed/well-nested for mutable references (i.e. XYXY writes are prevented when X and Y are siblings, because X must release the lock forever in order for Y to grab it).
The API for Stacked Borrows (for just Unique
references) is as follows:
impl StackedBorrows {
fn init() -> (ReferenceId, StackedBorrows);
fn create_ref(&mut self, parent: ReferenceId) -> ReferenceId;
fn use(&mut self, r: ReferenceId);
}
The API for Stacked Borrows is a subset of that for the lock, because the calls
to lock
and unlock
are hidden from Stacked Borrows, and instead Stacked
Borrows tries to infer them to catch as many violations of the locking
discipline as possible. (This is just one way to view it, and not necessarily
the "correct" way, of course)
The borrow stack in Stacked Borrows can be viewed as a stack of calls to lock
without matching calls to unlock
. The topmost item in the borrow stack
represents the current holder of the lock, and the items below it represent the
borrowing path from the root of the borrow tree to the current holder of the
lock.
Stacked Borrows is somewhat restrictive in its implementation of create_ref
.
When you create a reference by retagging, it immediately removes some items from
the stack (i.e., calls unlock
for the references on top of your parent) in order to "return" the
lock to your parent, and then it calls lock
for the new reference, pushing it
onto the borrow stack. But if the new reference never use
s the lock, then it
seems unnecessary to give them the lock straight away.
It seems like it might be possible to relax this behavior, by having
create_ref
merely add a new child to the borrow tree. That is, you don't insert
any calls to lock
or unlock
when someone does a create_ref
. Instead, you
only call lock
or unlock
once someone calls use
: if they are calling
use
, they need to have the lock, and therefore you have to (conservatively)
insert calls to unlock
and lock
to get the lock to the reference that wants
to use it. Basically, at that moment you choose the cheapest path of unlock
s
and lock
s to get it to where it needs to go. This means unlock
ing to get to
the nearest common ancestor of the current lock owner and the new lock owner,
and then lock
ing to "bubble" up the lock to the new owner.
In order to deal with SharedRO, the basic idea would be to replace the above lock by a reader-writer lock, and have it be "re-entrant" in a similar way. Except for read-only locking, your parent doesn't need to actually give up the lock in order for you to get it.
The idea for SharedRW would be to turn it into a reader-exclusivewriter-sharedwriter lock, where you can have either N readers, 1 writer, or N writers, and a mutable reference would refuse to write in the "N writer" state of the lock, and instead require the "1 writer" lock.
One way of dealing with untagged based on this "approximation" approach is to
selectively "hide" the reference IDs of certain references, so you no longer
have exact parent-child information and you also don't know exactly which
reference ID is being used for certain references. Then you could conservatively
try to "reconstruct" reference identity based on the pattern of use
s that you
see and the lock
s and unlock
s (and parent-child information) that you can
infer based on that.
If you do this, you end up with something slightly different (but similar to) what the current Stacked Borrows does.
It seems like the program logic that I came up with for my thesis already had the "unlocking" transition in the form of "ghost forgetting", allowing items to be removed from the ghost borrow stack before they are actually removed from the physical borrow stack. Now I think it might have made more sense to think of it as "ghost unlocking" and to add a corresponding "ghost locking" action as well. I think that would even be possible for the current Stacked Borrows (at least, for the version that doesn't have the tagged SharedRW issue).