The Linear-Aliasing Model

Instead of the more traditional approaches like reference counting, garbage collection, or borrow checking, Vale achieves its memory safety through something we call the Linear-Aliasing Model.

The Linear-Aliasing Model is where every object's lifetime is determined by exactly one owner, yet we can also have as many mutable references to it as we want. In other words, each type is linear, yet freely aliasable (we'll explain these further below).

This model offers efficient memory safety, plus be able to use shared mutability wherever we want. 0

The rest of this page is an overview, but if you'd like to see it in action, these articles will be helpful:

• Single Ownership and Memory Safety without Borrow Checking, RC, or GC, which approaches it from a C foundation.
• What Vale Taught Me About Linear Types, Borrowing, and Memory Safety which talks about how linear types allow memory safety without cost.
• Vale's Higher RAII, the pattern that saved me a vital 5 hours in the 7DRL Challenge
• Generational References, which talks about blending single ownership and mutable aliasing.

There are four basic types:

struct Ship { fuel int; }
exported func main() {
  ship = Ship(42);
  ship_ref = &ship;
  println(ship_ref.fuel);
  destruct ship;
}

42

And lastly, copy types, such as (bool, float, etc.), which are copied freely, similar to most languages.

The Linear-Aliasing Model adheres to single ownership:

• An owned value inhabits exactly one variable, struct field, or array element.
• An owned value on the heap is pointed at by exactly one owning pointer.

We can transfer an owned value or owning pointer from one place to another via a move operation. 2 Specifically:

• When we move out of a variable, the compiler invalidates it and prevents us from using it again.
• Only if we destroy a struct can we move its members out. 3
• We can only move an element out of an array if we pop it from the end, or shift all subsequent elements.

These are a certain flavor of move semantics, which uphold single ownership for a language.

It uses linear typing in that the user is required to explicitly destroy an owned value or owning pointer, and the compiler throws an error if the user forgets. The compiler won't automatically destroy something for us. 4 5

Linear typing has a lot of benefits:

• It gives memory safety with no run-time overhead.
• Safety from data races, since only one thread owns an object at a time.
• Objects can live inside the stack and inside other objects or arrays, which makes accessing them faster.
• We can use higher RAII so the compiler can guarantee we don't forget to some arbitrary future operation.

However, linear typing alone has historically had some drawbacks:

• It often can't do fast approaches like intrusive data structures and graphs.
• It can be at odds with interfaces and traits, as we're often required to pass dependencies in via parameter, which breaks API stability.
• It can't use patterns that help us decouple our codebases and make them more flexible, like observers, back-references, dependency references, callbacks, delegates, etc.

These drawbacks are because linear typing doesn't allow mutable aliasing.

We address that by adding mutable aliasing via generational references, which can do a run-time check to see if the target object is still alive. These checks are elided for owned values and owning pointers. In Vale, these checks are also eliminated by static analysis and regions.

Generational references are particularly suited to this task because they can read and write to the target data without affecting its lifetime.

Suddenly, we have all the benefits of mutable aliasing:

• We can do intrusive data structures and graphs.
• Interfaces and traits become tractable again, because objects can modify things outside themselves.
• We can use observers, back-references, dependency references, callbacks, delegates, and any other pattern.

...while still having the benefits of linear typing.

This addition isn't free; every allocation (though not every object 6) needs an 8-byte random generation number at the top. This could soon be obviated with unique references or isolates.

We end up with a model that's fast, safe, and most importantly, flexible. We can decide to use references only where necessary, or perhaps we can decide to drop into a more linear style where profiling suggests we should optimize.

For an example of a program that uses both the Linear-Aliasing Model and regions, see this tiny roguelike game. 7

If you'd like to see more, check out these articles:

• Single Ownership and Memory Safety without Borrow Checking, RC, or GC, which approaches it from a C foundation.
• What Vale Taught Me About Linear Types, Borrowing, and Memory Safety which talks about how linear types allow memory safety without cost.
• Vale's Higher RAII, the pattern that saved me a vital 5 hours in the 7DRL Challenge
• Generational References, which talks about blending single ownership and mutable aliasing.

The Linear-Aliasing Model is one of many techniques that Vale is bringing into the mainstream, along with:

• Region borrowing to eliminate memory safety overhead.
• Perfect Replayability, to record all inputs and replay execution, and completely solve heisenbugs and track down race conditions.
• Higher RAII, where the language can enforce that we don't forget to do an arbitrary future operation.
• Fearless FFI that lets us more safely interface with C and other native languages.