I'm trying something new today. I try to periodically read papers and such to stay on top of the latest research on things I'm interested in. Unfortunately, it's easy to read a paper and have it not really stick. To combat that, today I'm trying a paper review. We did this in some of my classes in grad school, where we'd have an assigned reading for each class period and before that we were supposed to write a couple paragraphs summarizing the paper, evaluating it, and asking a few questions. So, in what will hopefully become a regular feature of my blog, today I'm kicking off my first paper review.

Today I'm reviewing Safe, Flexible Aliasing with Deferred Borrows by Chris Fallin. This was published in ECOOP 2020. I found out about this paper from Yosh Wuyts who mentioned that it might be a good theoretical foundation for adding defer expressions to Rust.

What Problem Are They Trying to Solve?๐Ÿ”—

Rust's borrow checker has proven extremely successful in allowing the compiler to statically guarantee memory safety for many common pointer access patterns. That said, the borrow checker is rather conservative. Even with dramatic improvements such as non-lexical lifetimes, there are many patterns that are common in systems programming that run afoul of the borrow checker. For example, graphs are particularly challenging.

Programmers work around these limitations through several techniques. The most common is to use indices rather than pointers to refer to objects, which is one version of what the paper calls pseudo pointers. In the graph example, a graph might be represented as a vector of nodes, and the edges refer to nodes based on their index in the vector. This approach provides memory safety, but the paper argues that it does not provide logical memory safety.

Memory safety is roughly the idea "that any memory access by a Rust program must be valid memory and must be a valid, still-live instance of the object implied by the type of the pointer" (ยง3.3). Memory safety is sufficient to rule out undefined behavior, but it doesn't mean your program can't do unexpected or wrong things. For example, if you refer to graph nodes by their index in the nodes vector, there's nothing stopping you from using the index with another completely unrelated vector. The paper defines this property as logical memory safety, and ยง7.1 includes several examples of programs that violate this property in ways that would be easy to miss.

The problem this paper is trying to solve is to allow the compiler to guarantee logical memory safety in more of the common pointer access patterns, such as graphs.

What Is Their Approach to Solving the Problem?๐Ÿ”—

The approach is to extend the Rust type system with features necessary to support deferred borrows. Deferred borrows seem to me to be more of a design pattern enabled by a new type system feature than a feature in and of themselves. The enabling feature is static path-dependent types. In short, these extend Rust types with types that look like T/x, where T is an existing Rust type and the x part indicates that the value is rooted in a specific place.

In the author's own words, what this enables is a "separate 'bookmark' phase, in which an element is identified, from a 'use' phase, in which it is exposed for access" (ยง5).

I think the easiest way to describe how this works in practice is to quote from the AppendOnlyVec example in Figure 6:

pub struct AppendOnlyVec<T> {
    vec: Vec<T>,
}

impl AppendOnlyVec<T> {
    pub fn deferred(&self, index: usize) -> AppendOnlyVecRef<T>/0 {
        AppendOnlyVecRef { index }
    }
}

pub struct AppendOnlyVecRef<T> {
    index: usize,
    _phantom: PhantomData<T>,
}

impl DefBorrow<T, AppendOnlyVec<T>> for AppendOnlyVecRef<T> {
    fn def_borrow<'a>(&self/1, cont: &'a AppendOnlyVec<T>) -> &'a T {
        &cont.vec[self.index]
    }
}

This snippet defines an AppendOnlyVec type that has a two-step process to borrow entries in the vector. First you call vec.deferred(i), which gives you a AppendOnlyVecRef. The returned AppendOnlyVecRef is a path dependent type which indicates that it is rooted in the same place as the vector we are indexing into. In step two, we pass the AppendOnlyVecRef to def_borrow which converts it into a full borrow that can be used to access that storage location.

How Well Does It Work?๐Ÿ”—

It's hard to answer this question from reading a single paper, but so far it looks promising. It seems to deliver on providing tools to library writers to statically prevent certain classes of errors when using pseudo pointers.

My biggest concern about the approach is that it seems to require a lot of care on the part of a library author to use it correctly. Deferred borrows lets a library author expose an interface that, as long the library is correctly implemented, will make it impossible for the client to commit certain logical errors. For example, you won't be able to use a pseudo pointer from one vector to index into another. But as far as I can tell, the compiler has no way of verifying that the library has the properties it claims to have. In the AppendOnlyVec example, there's nothing stopping the implementation of push from clearing the vector instead. If this happened, when you went to promote a deferred borrow to a true borrow you would get a panic due to the index being out of bounds.

This is in contrast to memory safety. In Rust, as long as you do not use unsafe, there is no way you will have a memory safety error. This is true both for clients of a library and for implementing the library. In a sense, implementing a data structure like AppendOnlyVec using deferred borrows is like having to rely on unsafe in the implementation (maybe we'd call it logical unsafe to distinguish from memory unsafety) while presenting a logically safe interface to callers.

Is this a deal breaker? Not really. Type systems give programmers tools to express certain properties they want their programs to have, and the check whether those properties hold. More powerful type systems can describe and prove richer properties, but it's still up to the programmer to correctly define the properties they want. Looking at it this way, deferred borrows allows the programmer to say and check more things in the type system.

What Further Questions Does This Paper Raise?๐Ÿ”—

This is really my version of a future work section for this paper. I want to be clear that I don't mean these as criticisms, like "Ugh, why didn't the author also do X?" Research papers are about incrementally advancing the state of the art, so just because there are more things to do (including things we hopefully didn't know about beforehand) doesn't mean the paper's contributions aren't valuable on their own.

I'm curious about what this looks like at scale. I'd like to see some of the examples of the paper fleshed out more fully, and see whether a real project could effectively use deferred borrows. In reading the paper I had some questions about the syntax and ergonomics, but I think these are questions that could be answered and addressed with more real world experience.

Another question I have is what other applications there are for this. I mentioned at the beginning that this paper might be helpful for defer expressions, so this would be interesting to explore more. You can almost add defer as a macro, without any language support. I don't know how the macro I linked there works, but I would do this by making a struct that wraps a closure that it calls in its drop function. The problem with this approach is that anything that's borrowed in your defer block would be borrowed for the remainder of the function body, which is a problem if wither the defer block or the function want to mutate anything. Deferred borrows would give us a theory for how to work around this, by creating a deferred borrow when the defer block is created and converting it to a true borrow when the defer block is executed. Of course, there are probably other ways to solve this problem, but this approach may enable other patterns as well. In general, I'm a fan of making it so features can be implemented as libraries instead of needing special language support.

I think there may be other applications as well. The end of ยง7.3 mentions that path-dependent types give a way to create unforgeable values. These end up being useful in a lot of cases, such as in capability systems. I'd love to see work exploring these too.

Conclusion๐Ÿ”—

So there's my first and hopefully not last paper review. I thought the paper was an interesting read and had good ideas that I'd like to see explored more!