[pre-RFC] linear type modifier


#1
  • Start Date: 2015-01-08
  • RFC PR: (leave this empty)
  • Rust Issue: (leave this empty)

Summary

Add a linear type modifier. A drop of a linear type will cause a drop of its owned data, but do not allow scope-based drops of linear types: For compilation to succeed, users must explicitly move data out of these types before end-of-scope. As such, the only way a linear type can be implicitly dropped is through unwinding following a panic!. In the absence of a panic!, these types force users to explicitly consider resource clean-up.

Motivation

Scope-based drop is an implicit mechanism for ensuring that Rust programs do not leak resources. For the most part, this implicit mechanism works very well. However, when drop has side-effects that are important for program correctness (for example, a MutexGuard that releases a shared mutex when it is dropped), implicit drops will not communicate developer intent as effectively as explicit action.

linear types provide a means for library authors to communicate to library clients that resource clean-up will have side-effects that are important for program correctness, and will document in client code the explicit design considerations that have been made regarding resource clean-up.

I have seen some resistance to the idea that scope-based clean-up may be inadequate, so I’ll try to address that here.

When is scope-based drop inappropriate?

Scope-based drop is inappropriate in scenarios where resource clean-up has side-effects whose timing can affect program correctness. For example, a MutexGuard will release a shared mutex when it is dropped. The scope of time in which a shared mutex is locked is a highly important consideration in writing correct multi-threaded code, and highly important considerations such as this should be explicitly reflected in code.

Example: Force explicit mutex drop.

To take an example from RFC #210:

        let (guard, state) = self.lock(); // (`guard` is mutex `LockGuard`)
        ...
        if state.disconnected {
            ...
        } else {
            ...
            match f() {
                Variant1(payload) => g(payload, guard),
                Variant2          => {}
            }

            ... // (***)

            Ok(())
        }

(source)

In this code, it is impossible to discern whether the author intended or did not intend for the MutexGuard to be held in the ... // (***) code region. Developer intent could be properly signalled in two ways:

  1. If the developer intended that the lock possibly be held for the (***) code, he could wrap the guard in an Option. This solution is well understood, I don’t feel I need to spend more time on it here.
  2. If the developer intended that the lock not be held, he should enforce that each branch of the match above cause a drop.

There is currently no way for rust to help the programmer to enforce case 2. With linear types, this could be handled as follows:

        let (guard, state) = self.lock(); // (`guard` is mutex `LockGuard`)
        ...
        if state.disconnected {
            ...
        } else {
            ...
            let linear_guard: linear MutexGuard = guard; // (`guard` moved into linear_guard)
            match f() {
                Variant1(payload) => g(payload, linear_guard),
                Variant2          => {
                    // Unless the `drop` is uncommented, compilation will
                    // fail with:
                    // ERROR: linear type `linear_guard` not fully consumed by block.
                    //drop(linear_guard)
                }
            }

            ... // (***)

            Ok(())
        }
        // existing drop rules enforce that `guard` would be dropped
        // as it leaves scope.

This signals developer intention much more clearly, and allows the compiler to help the developer prevent a bug in the old code.

Example: Force explicit variable lifetime for FFI.

Consider this example:

extern {
  fn set_callback(cb:|c_int|, state:*const c_void);
  fn check(a:c_int, b:c_int);
}

fn main() {
  let r = |x:c_int, data:*const c_void| {
    let foo:&mut Foo = transmute(data);
    foo.add(x as int);
    println!("{} was the output", x as int);
  };
  let data = Foo::new();
  unsafe { set_callback(r, &data as *const Foo as *const c_void); }
  for i in range(0, 10) {
    unsafe {
      check(10, i);
    }
  }
  // Now we must manually drop(data); and drop(r) here, othewise check will segfault.      
  // because data will already be dropped. 
}

((source)[https://github.com/rust-lang/rfcs/pull/239#issuecomment-56261758])

Having the C FFI interact with rust structures requires an explicit model of how the lifetime of rust structures that may cross the FFI boundary interact with the lifetime of the C representations of those structures. (In other words, both C and Rust need to have some agreement about the lifetimes of shared data structures.) At present, there is no way to explicitly enforce the relationship between the lifetimes of two representations of the same data structure, so that code like the above must rely on a deep understanding of Rust’s and C’s allocation semantics in order to work correctly. A linear type provides a means of documenting that variable lifetime has been explicitly considered:

extern {
  fn set_callback(cb:|c_int|, state:*const c_void);
  fn check(a:c_int, b:c_int);
}

fn main() {
  let r = |x:c_int, data:*const c_void| {
    let foo:&mut Foo = transmute(data);
    foo.add(x as int);
    println!("{} was the output", x as int);
  };
  let r: linear |x:c_int, data:*const c_void| = r;
  let data = Foo::new();
  let data: linear Foo = data;
  unsafe { set_callback(r, data as *const Foo as *const c_void); }
  for i in range(0, 10) {
    unsafe {
      check(10, i);
    }
  }
  // compilation will fail unless we manually drop(data); and drop(r) here.
  // using linear types prevented a segfault.
  //drop(r);
  //drop(data);
}

Isn’t this just like sprinkling free() calls through the code?

Sort of, but it’s much safer than C’s free(). There are two major problems with explicit resource clean-up in C-like languages:

  1. Failure to free.
  2. Use after free.

This proposal continues to prevent both issues in rust:

  1. The obligation that data be moved out of a linear type means that it is impossible to fail to free resources (compilation will fail if the linear pointer is not explicitly moved from); AND
  2. Rust’s borrow-checker continues to enforce that use-after-free is prevented.

This design is intended to bring back some benefits of explicit resource management, without inflicting their costs.

But linear types don’t interact well with unwinding?

The linear type as described here is not a true linear type: when unwinding past a linear type, the linear modifier is effectively dropped, so that the contained value will be dropped appropriately. Supporting unwinding means that Rust’s linear types would in effect still be affine. However, if we ever allow a post-1.0 subset of rust without unwinding, Rust’s linear types would become true linear types.

Detailed design

Add a linear type modifier. Types defined with this modifier are not allowed to be in a “maybe-dropped” state.

Instantiating a linear type:

A linear type is created by a move operation into a linear type. This will be supported by defining an implicit coercion from a type T to linear T. A linear type can be defined as a receiver for any operation that causes a move, and will evaluate to the same underlying code. For example:

struct Foo { f: int }

fn f1() {
    let f = Foo { f: 3 };
    let g = f;
    drop(g);
}

fn f2() {
    let f = Foo { f: 3 };
    let g: linear Foo = f;
    drop(g);
}

f1 and f2 should compile to precisely the same code. In a similar way:

struct Foo { f: int }

fn g1(foo: Foo) {
    drop(foo);
}

fn g2(foo: linear Foo) {
    drop(foo);
}

g1 and g2 should compile to precisely the same code. Linear types could also be returned from functions. The following two routines should compile to identical code, but impose different requirements on callers:

struct Foo { f: int }

fn h1(foo1: Foo, foo2: Foo, select: bool) -> Foo {
  let linear_foo: mut linear Foo;

  linear_foo = if select { foo1 } else { foo2 };
  linear_foo
}

fn h2(foo1: Foo, foo2: Foo, select: bool) -> linear Foo {
  let linear_foo: mut linear Foo;

  linear_foo = if select { foo1 } else { foo2 };
  linear_foo
}

In particular, h2 requires that the caller capture the returned value in a variable of type linear Foo, while h1 has no such requirement.

Dropping a linear type.

A linear type must be explicitly dropped by causing a move from the linear variable. Support this by adding an implicit coercion from linear T to T.

struct Foo { f: int }

fn my_drop(foo: Foo) { }
fn call_drop() {
    let f: linear Foo = Foo { f: 3 };
    my_drop(f);
}

Further, linear types are not allowed to be in a “maybe dropped” state - in the case of a conditional, their ownership must be explicitly known at each merge point. Failure to unambiguously resolve ownership should result in a compilation error. Taking inspiration from the notation in RFC #210:

struct S;

fn test() -> bool { ... }

fn f1() {
    //                                     LINEAR OBJECT STATE
    //                                  ------------------------
    let p1: linear S = ...;
    let p2: linear S = ...;
    //                                  {p1: owned,   p2: owned}
    if test() {
        drop(p1);
        //                              {p1: dropped, p2: owned}
    } else {
        drop(p2);
        //                              {p1: owned,   p2: dropped}
    }
    // MERGE POINT: linear object state must match on all incoming
    // control-flow paths. That it does *not* match here means that
    // an attempt to compile this function should result in a
    // compilation failure.
}

Drawbacks

Compiler complexity to support another data type modifier.

More implicit coercion rules.

The described mechanism for creating linear types prevents applying a linear modifier to Copy types. I can’t imagine a case where you would want a Copy type to be linear, but this is a potential drawback.

Another reserved keyword (linear).

Alternatives

We could not do this, and live with the status quo. I tried to show why this is disadvantageous in the Motivation above, but it is probably not a show-stopping issue. On the other hand, it seems like this facility could make a static drop semantics more usable.

I considered using a modification of pointers to represent linear ownership. This had the advantage of not requiring new implicit coercions, but ran into several corner cases in the design that this RFC addresses.

Unresolved questions

Can linear types be heap-allocated, or 'static?

Possibly not (though this deserves more investigation), but even as a stack-only construct, I consider linear types likely to be highly useful.

How should linear types interact with “copy” objects?

This proposal punts on this question. We start out possibly more conservative than necessary, disallowing the linear modifier from being applied to Copy types. In the future, this restriction could possibly be relaxed.


#2

The motivation seems reasonable, but the mechanism seems a bit heavyweight. Especially considering that we cannot prevent drops-while-unwinding, and so these cannot really be linear types, this would serve more as a best-effort nudge in the direction of preventing more mistakes, rather than as a way to add any new correctness guarantees.

So, my feeling is that a more economic solution might be an attribute (#[linear], or #[explicit_drops]) which can be applied to types which would benefit from it, such as MutexGuard, and an accompanying lint which indicates where values of such types fall out of scope. Its severity level could be set to warn by default, and people could push it in either direction locally depending on their priorities.

(Also, I don’t see if you’ve considered the rules around “inheriting linearity”, i.e. around linear types as components of compound types, linear types as generics arguments, etc.? Seems like we would need to do it similarly to Copy, if we wanted to get it “fully correct”.)

(I think types which can’t be dropped but can be copied might be called “relevant”? But I think I don’t really understand any of it.)


#3

@glaebhoerl These types would become true linear types if we can guarantee that unwind won’t occur (which will ultimately be a critical feature for some parts of rust’s core audience). One way to do guarantee no unwind is through a no-unwind flag, though I hope other mechanisms will be added in the future to make such guarantees in a narrower scope, maybe a nounwind marker that could be placed wherever unsafe is placed, today.

The difficulty I had with type attributes was that it was difficult to see how to explicitly cause a drop to occur: even the drop function ultimately works by moving a variable into drop's scope, then relying on implicit drop as that scope is cleaned up. That implicit drop must be used would still cause the lint to fire, wouldn’t it? The way I saw around this was to define multiple related types (one marked linear, and one not), and to define a way to convert between the two.

You’re probably right that there are other cases I haven’t considered. I did think a little about compound types, but did not put discussion of that in the text above, as the case I considered (stack allocation of a compound type containing linear fields) seemed to fall out pretty naturally from the rest of the text. But the ideas deserve a more explicit treatment.


#4

Well, you could turn the lint off for that one function. : )

(Not sure how I feel about relying on some kind of nounwind flag to guarantee linearity; it seems like that would violate the spirit of “abort instead of unwinding” as being “just an optimization”, which is how it has tended to be discussed, i.e. code could start doing Very Bad Things if unwinding were ever turned back on. Maybe an in-code marker would be better… but I’m not sure how that would work (it can’t “reach into” called functions to keep them from unwinding); would it just abort when unwinding reaches the scope of the marker? In that case it’s easier to just say “unwinding with a linear type in scope is a process abort” in general, without the extra markering.)


#5

I think such feature could be useful for IO.

People assume that buffered stream is flushed on drop. So, currently, if thread is unwinding on error, destructor may hang indefinitely trying to flush streams.

In my opinion, destructors should only release resources, not flush buffers for that reason.

But if currently destructors won’t flush, programs will have lots of bugs because of forgotten flush call.

Linerar types may solve this problem: BufferedWriter can be made linear (with operation like flush_and_drop()), and BufferedWriter destructor won’t flush.

Alternatively, destructor could query a reason for unwinding: is it called because of panic or normal return? And flush only on normal return.


#6

Well, you could turn the lint off for that one function. : )

Yeah, occurred to me, too… I know this was said tongue-in-cheek, but drop isn’t the only function where we’d want this, library writers will also want to define their own clean-up functions, and forcing an explicit drop within the library writer’s clean-up function may not be what’s desired…

For what it’s worth, I kind of went down a rabbit-hole that resulted in this RFC in thinking about how the language can help us make use of intrusive structures safe… (You’ll remember I mentioned the case in a comment on your intrusive structure RFC, where we proxy ownership of a container through ownership of the contained intrusive field.) Drops of the intrusive structure are likely to cause errors when the container has a destructor… The only way to avoid those errors is by preventing drops on the intrusive field. Hence, linear types.

The nounwind marker was just sort of tossed out as an example of how we might be able to ensure that these types can be used in a linear way… It’s not necessarily the way to go, but I didn’t want to think too deeply about the problem, yet. But being able to guarantee that unwind won’t occur will be a critical feature of the language for me when it becomes time to advocate to the higher-ups that we can get good results by building parts of our system in Rust.


#7

@eddyb and I were talking about how a future &out T might/could/should (?) be safe it if it were linear. Conveniently, if &out T is never Send/Share, it would also be unwind-safe despite unwinds breaking linearity. That is a bit of an annoying restriction though.


#8

Using a #[linear] attribute sounds good, but it probably makes more sense as a simple error, rather than a lint, although a lint would also obviously work.

Regarding the issue of the destructor function, I think there is a simple solution: allow using destructuring patterns on #[linear] types and use them in those functions to destroy the value without triggering the error.

Obviously if there are private fields destructuring patterns would only be allowed in the struct implementation, thus forcing to call one of the destructor functions.

BTW, regarding avoiding unwind, just make panic! call abort() and it’s done. Avoiding panics/aborts at all is much more problematic because you need to statically prevent recursive function calls to avoid stack overflow (and also not use anything from the standard library that allocated memory).


#9

This idea is very interesting to me though I’m not sure if we really need a new type for it.

I also thought about a command line option for rustc to print out program locations where Drop::drop() are inserted before.


#10

I appreciate the detailed proposal, but I can’t agree with it.

First off, it requires a keyword. Those are pricey and we have reserved a bunch of them already like JS did, very wasteful IMO (I fear we’ll be forever stuck with the likes of be and override). If we replace linear T with Linear<T> or #[linear] T (though we don’t have support for the latter), this becomes more like #[must_use] with stronger semantics.

Even then, I’d have to argue that the usefulness of linear types which can be consumed at will without any restriction imposable by a type, is quite limited. Or that they’re not even linear types!

The drop function is defined as fn drop<T>(_: T) {}, par excellence affine, not linear. If drop(x) works, then let _ = x; and (unless #[must_use]) {x;} also work. Kind of reminds of the “noisy drop” discussions.

I have sketched my own linear type design, it was simpler to implement than this and it worked better for my usecases (specialized consumer functions) - but it wasn’t very well received so I shelved it. I’ll embed it here for future reference:

// std::markers:
#[lang="linear"]
struct Linear;
impl Linear {
    fn consume(self) { unsafe { std::mem::forget(self) } }
}
// std::thread:
struct Thread<T> {
    // ...
    linear_marker: markers::Linear
}
impl<T> Thread<T> {
    fn detach(self) {
        // This can only be done in std::thread because linear_marker
        // is private, and partial moves are disallowed.
        let {/*...*/, linear_marker} = self;
        // Dispose of the only reason self is linear.
        linear_marker.consume();
        /* detach thread etc. */
    }
    fn join(self) -> T {
        let {/*...*/, linear_marker} = self;
        // Dispose of the only reason self is linear.
        linear_marker.consume();
        /* join thread etc. */
    }
}

Since the kinds and related markers are going away (for Copy, Sync and Send) it may make more sense to use a Linear trait here (necessary in some form if you want to allow generics to opt-in to being instantiated with linear types - another important point this proposal doesn’t cover), and impl<T> Linear for Thread<T> in a similar way to Drop. I would then guess that having at least one private field will be the only requirement to restrict consuming a linear type to the module where it is defined (which can then provide a restricted interface, as it is the case with the rest of Rust’s abstraction-building primitives).


[pre-RFC] linear types, take 2
#11

Could you elaborate? Is this the formulation where &out may only point into the stack?


#12

For what it’s worth, embedded developers often argue about whether it’s allowable to use dynamic memory allocation at all, precisely because of the likelihood of unexpected error. We live without access to large portions of the standard library… But we can’t work without provable bounds on resource usage.


#13

Thank you for the detailed feedback… I’m still working through it, and hope to address it more completely, later. It also occurred to me overnight that the way I’ve used drop in the proposal wouldn’t work for the reason you mention… In the spirit of the original proposal, I’d remove the implicit coercion from linear T to T, and add an explicit unlinearize transformation, so that you would need to drop(unlinearize(T)). (In an earlier draft, I did this with a DerefMove-type operation: you would need to drop(*foo). Probably that was the technically better choice.)


#14

That is an improvement, but it still doesn’t allow building abstractions like my Thread example above, File::close (this was given as an example on reddit a while ago, I believe) or &out pointers.


#15

Does this come closer to the spirit of what people would like to see?

#[linear]
#[deriving(Drop)]
pub struct Linear<T>(T);

impl<T> DerefMove<T> for Linear<T> {
    pub fn deref_move(self) -> T {
        let Linear(inner) = self;
        inner
    }
}

#16

I have grown to like the automatic drop of resources with out explicitly dropping them. I feel like it is really ergonomic. This proposal does not really bother me until you commonly used libraries start doing it and then it will become annoying.

One specific case would be an existing code base requiring major overhaul because the developer of a library dependency thinks it would be a good idea to make a type linear. So now I wake up and have to go through tons of code fixing it because someone else thought I did not know what I was doing. So unless there is a way to turn it off I really do not like it.

Also, I do not know of many real world situations where I had a problem with automatic dropping. I am usually in tune with my work enough to have all potential factors in mind while I write code. In regard to the mutex example above. I have never had a problem with dropping of a mutex guard! I mean if you let that mutex guard drop out of scope while you still need it then you are:

  1. Not paying good attention to what you are doing at all.

  2. Should have been protecting the T in Mutex<T> not something outside of it, because otherwise you would be unable to access it if the guard drops. You basically have weak protection using the mutex to protection something outside of it.

Like I said the linear type sounds great as another feature but to summarize:

  1. MutexGuard<T> does not need to be explicitly dropped.
  2. A linear type can get annoying very quickly even though the library author thinks it is a good idea.
  3. No proposed way to turn it off, or make it a warning, or something less devastating than an error.
  4. It complicates rustc which means it consumes more programmer fuel each time something is changed or fixed. That is one more part on an ever increasing complexity we call rustc. Is it worth it? Likely not.

#17

For what it’s worth, I’m working on a new version of this proposal that allows a Drop wrapper around a linear type. It’ll take a little more time before it’s ready to post, but it would allow one to write an affine wrapper around a linear type:

struct Foo;

#[linear]
struct LinearFoo(Foo);
fn explicit_cleanup_function(lf: LinearFoo) {
  ...
}

struct AffineOfLinear(LinearFoo);
impl Drop for AffineOfLinear {
  fn drop(&mut self) {
    let AffineOfLinear(inner) = self;
    explicit_cleanup_function(inner);
  }
}

In this case, even if your library author made a bad choice, it’d be possible for you to put a wrapper around his linear type allowing it to be treated as affine. Still, part of choosing a library is evaluating its ergonomics, and comparing the author’s development philosophy to yours… If they disagree too much, there will almost certainly be some pain in relying on that library. If they generally agree, that author is less likely to make a choice that hurts.

Importantly for me, I know of cases where implicit drop of a variable would absolutely be a program error (involving intrusive structures), and linear types feel like the solution in those cases. As a separate argument, I think “eager drop” is likely to prove difficult to use without a linear type facility…


#18

In Intutionistic Logic there are 3 rules referred to as the “structural rules” if you drop any of these rules you find your self in a substructural logic (i.e affine, linear, relevant, ordered). Which rules you choose to drop give you different logics and therefore different type systems.

You get relevant by dropping the weakening rule, a rule that allows you to have unneeded assumptions when performing a proof, so as a programmer this means we have to use every term (everything is “relevant”).

You get a affine type system by dropping contraction, the rule that allows you to duplicate an assumption an arbitrary number of times, this means every value can be used at most once.

You get linear by dropping both weakening and contraction meaning every value must be used exactly once.

Finally you can get an ordered type system by dropping the exchange property which allows the you to reorder assumptions arbitrarily. Removing this rule means as a programmer you must use terms in the order they are introduced, restricting programs even more.

Here is a high level overview from Wikipedia: http://en.wikipedia.org/wiki/Substructural_type_system

The metatheory can be a little complicated but the ideas are simple.


#19

Second pass at a linear types RFC is here.


#20

@glaebhoerl Thanks, I had forgotten about heap allocated &outs, but it in fact works out. The &out to heap does not own the box, just the contents of the box, so to speak. Unwinding will hit the &out T, and do nothing, and then hit the borrowed Box<T>. The lack of Send+Sync ensures the box and &out will never be unwound separately.