Virtual Places and Borrow Checker Integration

10~20min

In this blog post, I present an idea on how we can specify the borrow checker behavior in the context of the field projection design effort. This work builds upon the blog post The Algebra of Loans in Rust by Nadrieril. I will give a more field projection focused proposal, whereas that blog post looked at the general way the borrow checker works.

published

In this blog post, I present an idea on how we can specify the borrow checker behavior in the context of the field projection design effort. This work builds upon the blog post The Algebra of Loans in Rust by Nadrieril. I will give a more field projection focused proposal, whereas that blog post looked at the general way the borrow checker works.

Jump to The Table.

The main proposal for field projection is focused on virtual places, which were introduced by Nadrieril. Similarly now, I will give a way to specify the borrow checker behavior of the built-in reference types as well as custom types with places at the focal point.

Additionally, I will present an idea on how to better include the borrow checker's lifetime into our proposal.

There are several issues/open questions with the current design :

I hope to answer all of these with this blog post. And additionally provide a simpler explanation of borrowing in Rust.

# Informal Writeup

The Algebra of Loans in Rust is a prerequisite of this post, it gives a good overview of the basic concepts, such as what a place is, taking a borrow and loans. The post also gives three tables, which specify what kind of operations each reference has available. In this post I will replicate the latter two tables ; not via specifying them directly, but rather by specifying an underlying mechanism.

This underlying mechanism consists of two concepts:

  1. What kind of access are we granting to the place. For example, &mut requires exclusive access, & only needs shared access and *const doesn't need any kind of access .
  2. What state should the place be in when the borrow starts and should it be changed when the borrow ends? For example, & requires the place to be initialized. &mut requires that the place is not pinned. *const doesn't require anything. As a last important example there is &own, which requires the state to be initialized, not pinned and transform that state on expiry to uninitialized.

These concepts also explain how all place operations interact with the borrow checker:

# Formal Explanation

This part essentially is like the "reference-level explanation" section of an RFC. We model the access kind and place state using enums:

// also called `BorrowKind` in previous proposals
pub enum PlaceAccess {
    Shared,
    Exclusive,
    Untracked,
}

pub enum PlaceState {
    Initialized(PinnedState),
    Uninitialized,
}

pub enum PinnedState {
    NotPinned,
    Pinned,
}

We can now add two constants on PlaceBorrow or even on HasPlace:

pub trait HasPlace {
    const ACCESS: PlaceAccess;

    const STATE: PlaceState;

    type Target: ?Sized;
}

(Note that to properly support places that allow several states, we'd probably need a set or another enum instead of PlaceState.)

We then also need a constant AFTER: PlaceState in PlaceBorrow, which specifies the state the place should be in after the borrow ends.

To obtain the second table "If a loan was taken and is live, what can I still do to the place", we only need to consider the ACCESS constants of the two custom pointers (types that implement HasPlace). If one of them is Untracked or both are Shared, they may coexist; otherwise, a borrow check error is thrown.

Examples:

For the third table, one only needs to consider the state of the place after the borrow expires. In this model, it is useful to make Untracked borrows expire immediately.

Examples:

# The Table

(Smart) pointer or operationPlaceAccessPlaceState before PlaceState after
&TSharedInitialized(_)unchanged
&mut TExclusiveInitialized(NotPinned)unchanged
&own TExclusiveInitialized(NotPinned)Uninitialized
&uninit TExclusiveUninitialized???
*const TUntracked_unchanged
&pin TSharedInitialized(Pinned)unchanged
&pin mut TExclusiveInitialized(Pinned)unchanged
&pin own TExclusiveInitialized(Pinned)Uninitialized
ArcMap<T, U>UntrackedInitialized(_)unchanged
UniqueArcMap<T, U>UntrackedInitialized(_)Uninitialized
PlaceDropExclusiveInitialized(_)Uninitialized
PlaceReadShared Initialized(_) unchanged
PlaceMoveExclusiveInitialized(NotPinned) Uninitialized
PlaceWriteExclusiveUninitializedInitialized(NotPinned)
PlaceInitExclusiveUninitializedInitialized(NotPinned)
PlacePinInitExclusiveUninitializedInitialized(Pinned)
PlaceBorrowcustomcustomcustom
PlaceDeref?????????

A couple of notes:

# Conclusion

I believe that this idea is very much on the right track, since it has many great properties at the same time:

If we had a Move trait instead of making pin a place state, we'd have an even simpler picture. Another piece of evidence in favor of making Move a reality.

# Open Questions

# Bonus: Lifetime in PlaceAccess

Taking inspiration from Nadrieril , we can try to make the lifetime available depending on whether the access kind is untracked. My idea is to just use the type system instead of an enum:

#[sealed]
pub trait PlaceAccess {}

pub struct Owned;
impl PlaceAccess for Owned {}

pub struct Shared<'a>(PhantomData<&'a ()>);
impl PlaceAccess for Shared<'_> {}

pub struct Exclusive<'a>(PhantomData<&'a mut ()>);
impl PlaceAccess for Exclusive<'_> {}

When we now implement HasPlace, we must give a lifetime in shared and exclusive cases:

impl<'a, T> HasPlace for &'a mut T {
    type Access = Exclusive<'a>;
    const STATE: PlaceState = PlaceState::Initialized { pinned: false };
    type Target = T;
}

But in the untracked case, we now do not have a lifetime at all:

impl<T> HasPlace for *const T {
    type Access = Untracked;
    const STATE: PlaceState = PlaceState::Any;
    type Target = T;
}

impl<P: Projection> PlaceBorrow<P, *const P::Target> for *const P::Source {
    // ...
}

This conditional binding of the lifetime to PlaceAccess also allows us to allow the borrow checker to choose that lifetime. It essentially acts as a marker of the borrow-checker-controlled lifetime. This way, we get lifetime shortening, since we can now write the following impl:

impl<'a, 'b, P> PlaceBorrow<P, &'a mut P::Target> for &'b mut P::Source
where
    'b: 'a,
    P: Projection,
{
    // ...
}

And since &'a mut P::Target has Access = Exclusive<'a>, the borrow checker can shorten that lifetime as is appropriate.