Lecture 32: Resources

1 Purpose

Discuss logics for resources (affine & linear ownership systems)

2 Outline

When confronted with the challenge of aliasing, explored in Lecture 23: Reasoning about Mutable State, Lecture 24: Value Mutation, and Lecture 25: More Pointer Equality, one solution adopted by some systems, most successfully the Rust Programming Language, is to rule it out. Or at least, to prevent aliasing in combination with mutation. While the borrow checker at the heart of Rust is well beyond the scope of this class, and indeed is quite a complicated abstraction, the logical techniques that underly Rust have broader implications, and there is a runtime realization that we can implement and experiment with in LSL.

The key insight is the idea that certain objects should only be able to be used in a restricted manner. In the version we will implement, that will mean that they can be used either once or not at all. Such a system, termed "affine", can ensure that aliasing is harmless, since two different parts of the program are prevented from using the same object.

The ideas that underly affine systems go back to linear logic, created in the 1980s by French logician Jean-Yves Girard. This was a logical system where each proposition had to be used exactly once. Affine logics, which have ended up more commonly implemented, relax that slightly to at-most-once, rather than exactly-once.

The original efforts to translate this into programming languages suffered from being too inflexible, or alternately, from requiring too many values to be copied. As if you cannot alias, but you need the same value in two different places, the only option is to copy it. If the value is large, that copying may be quite expensive, both in time and space. Much of subsequent efforts were in figuring out how to relax, in controlled ways, the invariant so that "bad" aliasing could be ruled out, but "good" aliasing would be okay. The choice Rust made was to distinguish between references that allowed mutation, and ones that did not. Then, any number of aliases could exist, as long as none of them allow mutation. If there is to be any reference that allows mutation, it must be the only one in the entire program at a certain "moment in time".

We will do something slightly simpler. Rather than ruling out aliasing statically, we will create a value that will protect a value, and only allow the value inside to be accessed once. Thus, once we have wrapped an object up in this way, we know that it will only ever be accessed once, even if many aliases exist to the value that would allow access.

How do we accomplish this? Through a combination of functions as values and mutable variables:

(define-struct affine-error (v))

(define-struct affine-container (thk))

(define (affine v)   (let ([used? #f])     (make-affine-container       (lambda ()         (if used?             (raise (make-affine-error v))             (begin (set! used? #t)                    v))))))

i.e., when we do (affine 10), we end up with a zero-argument function that, the first time it is called, will give us back 10, but on all future calls, will error. Since "getting" a value out of an affine container amounts to extracting the function and invoking it, we can define a helper for ourselves as:

(define (affine-get a)   ((affine-container-thk a)))

We can create a contract for these:

(define-contract (Single T)   (Immediate (check affine-container?)              (generate (lambda (fuel)                          (affine (contract-generate T fuel))))))

Now you can try using them.

Exercise: First thing to try is defining a function that swaps the contents, but increments thim. Notice what happens if you call it with the same value. When we implemented this before (using mutation), we ruled this case out by using eq? to check if the values passed in were the same; here it is ruled out by nature of the values themselves: there is no need to implement anything extra.

(: swap-and-inc (-> (Tuple (Single Real) (Single Real)) (Tuple (Single Real) (Single Real))))

(define (swap cs)   (let* ([c1 (first cs)]          [c2 (second cs)])     (list (affine (add1 (affine-get c2))) (affine (add1 (affine-get c1))))))

Limitations: clearly, this doesn’t prevent aliasing that circumvents our affine construct. We could put the same reference into two different affine. Usually, how these systems are implemented, a primitive like affine is combined with abstraction (a la Lecture 18: Programming Against Interfaces) to only expose alias free references.

For example, if we think back to our second example from Lecture 25: More Pointer Equality:

(define-struct cell [value])

(: f (-> (Cell Natural) (Cell Natural) False))

(define (f x y)   (if (<= (cell-value x) (cell-value y))       (begin (set-cell-value! x (add1 (cell-value x)))              (f x y))       #f))

If we tried to fix this by just wrapping Single around the two arguments, this wouldn’t really work. We could do something:

(: f (-> (Single (Cell Natural)) (Single (Cell Natural)) False))

(define (f sx sy)   (let ([x (affine-get sx)]         [y [affine-get sy]])     (if (<= (cell-value x) (cell-value y))         (begin (set-cell-value! x (add1 (cell-value x)))                (f (affine x) (affine y)))         #f)))

But we could just call it as:

(define x (make-cell 10)) (f (affine x) (affine x))

Completely circumventing the entire mechanism. Better would be to not expose the cell constructor at all, and only provide what is often called a "smart" constructor, i.e.:

(: smart-make-cell (-> Natural (Single (Cell Natural))))

(define (smart-make-cell n)   (affine (make-cell n)))

This gets us half the way there. The other problem is that if we directly expose affine-get, then even if we only expose smart-make-cell, once we call affine-get, we get back a Cell and can alias that into two different Single values. So, again, the answer is abstraction: lift the operations that operate on Cells to operate on Single Cells:

(: smart-cell-value (-> (Single (Cell Natural)) (Tuple (Single (Cell Natural)) Natural)))

(define (smart-cell-value sc)   (let ([c (affine-get sc)])     (list (affice c) (cell-value c))))

(: smart-set-cell-value! (-> (Single (Cell Natural)) Natural (Tuple (Single (Cell Natural)) False)))

(define (smart-set-cell-value! sc v)   (let ([c (affine-get sc)])     (begin (set-cell-value! c v)            (list (affine c) #f))))

Note that for both, we actually changed the api to return the value again – because if we didn’t, it would be consumed and we could never access the changed value again! In general, operations over affine values will often have this flavor: returning changed values along with whatever other output, because once you pass in the input, you cannot use it again.

Exercise: rewrite f above using the smart- variants. Test that it works.