Stacked Borrows as lock inference

stackedborrows-lockinference.md

Stacked Borrows as lock inference

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:

1. 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.
2. Thinking of the code as containing invisible lock and unlock 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.
3. It suggests some ways in which Stacked Borrows might be relaxed while (hopefully) still justifying important optimizations.

The lock

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:

1. A reference needs to hold the lock (i.e. you must have called lock without calling unlock after) in order to access the memory location (i.e. call the use function).
2. 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 using create_ref. (Similar to retagging in Stacked Borrows and the borrow stack)
3. 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)
4. You can only hold the lock once: i.e., once you unlock you can never lock 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).

How Stacked Borrows approximates 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.

Possible relaxation

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 uses 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 unlocks and locks to get it to where it needs to go. This means unlocking to get to the nearest common ancestor of the current lock owner and the new lock owner, and then locking to "bubble" up the lock to the new owner.

Dealing with SharedRO and SharedRW

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.

Dealing with untagged / raw pointers

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 uses that you see and the locks and unlocks (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.

Program logic / relation to "ghost popping / ghost forgetting"

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).