- 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:
- If the developer intended that the lock possibly be held for the
(***)code, he could wrap the guard in anOption. This solution is well understood, I don’t feel I need to spend more time on it here. - If the developer intended that the lock not be held, he should enforce that each branch of the
matchabove 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:
- Failure to free.
- Use after free.
This proposal continues to prevent both issues in rust:
- The obligation that data be moved out of a
lineartype means that it is impossible to fail to free resources (compilation will fail if thelinearpointer is not explicitly moved from); AND - 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.