Zero-Cost Borrowing with Vale Regions, Part 3: One-Way Isolation (Preview, Draft)

Watch how we split our memory into regions, for more performance!

Preview, Draft — Evan Ovadia — Sponsor us on GitHub!

Note: Regions are still a work-in-progress. Part 1 has been successfully prototyped, but parts 2-5 are only a preview describing how we expect them to work in practice, to show where we're headed and what we're aiming for. They could surpass our wildest expectations, or they could shatter and implode into a glorious fireball, who knows! Follow along as we implement all this, and reach out if anything isn't clear! 0 1

Vale has an ambitious goal: to be fast, memory safe, and most importantly, easy. There are a lot of stellar languages that have two, and we suspect it's possible to really maximize all three.

To do this, we're harnessing a new concept called regions.

In Part 1 we saw how we can use pure functions to easily immutably borrow data to make it faster to access.

Part 2 showed us how we could more precisely create regions via isolates, and immutably borrow them too.

The isolates we've seen so far have had complete isolation: no outside data can point to any inside data, and vice versa. This is useful for a lot of things, but there are times when we want inside data to point out.

Luckily, with one-way isolation, we can make data inside the region point to data outside the region.

An Example

Here's something similar to the example we saw in Part 2.

This snippet doesn't yet use isolation, we'll show that further below.

There are a couple differences from what we saw in part 2:

Cannon now points to an EnergySource.
We subtract from the EnergySource whenever we fire on a ship.

In Part 2, we were able to optimize this by making cannon isolated, because it didn't point to anything outside itself, and nothing outside pointed in.

However, Cannon now points to an EnergySource outside itself, so we can't use the isolation we saw in Part 2.

struct Cannon { source &EnergySource; strength int; ... } struct EnergySource { energy int; } struct Ship { hp int; } exported func main() { source = EnergySource(200); cannon = Cannon(&source, 12); ship = Ship(100); fire(&cannon, &ship); println("Ship's new hp: {ship.hp}"); } func fire( cannon &Cannon, ship &Ship) void { // Calculate damage using a very // complex algorithm. damage = cannon.strength * 2; // Use up that much energy. set cannon.source.energy -= damage; // Now hit the ship! set ship.hp -= damage; }

Ship's new hp: 88

The answer is to use one-way isolation. Here's how!

Using One-Way Isolation

Even though something inside the Cannon points outside itself, there's still nothing outside that points in.

In this case, we can still make cannon isolated, as long as we tell the compiler which parts of Cannon might point to outside itself.

We still make the changes from Part 2:

By putting the ' in front of the Cannon call, cannon is now of type 'Cannon which means it's isolated.
&cannon became cannon.imm, which immutably borrows the iso's contents.
We added <c'> after func fire so that the function can receive things in a read-only region, referred to as c.
We added a c' to the &Cannon to show that it's in that read-only region.

But there are a couple extra changes now, in Cannon and fire:

cannon is now of type 'Cannon<main'> which means it's isolated, but it can point to things inside main's region.
We made fire's parameter into a &c'Cannon<fire'>, so that it can point to things inside fire's own region.

struct Cannon<e'> { source &e'EnergySource; strength int; ... } struct EnergySource { energy int; } struct Ship { hp int; } exported func main() { source = EnergySource(200); cannon = Cannon(&source, 12); ship = Ship(100); fire(cannon.imm, &ship); println("Ship's new hp: {ship.hp}"); } func fire<c'>( cannon &c'Cannon<fire'>, ship &Ship) void { // Very fast, no generation checks! damage = cannon.strength; // Take energy from energy source. set cannon.source.energy -= damage; // Now hit the ship! set ship.hp -= damage; }

As you can see, we're still able to isolate Cannon and open it immutably, even though it points to something outside its own isolated region.

A lot of real-world code can fit easily with one-way isolation. Most languages have a notion of "private" data, that's not exposed via an object's API. Those objects can be in the object's isolate, yet they can still point outside.

With one-way isolation, we can immutably borrow much more of our programs data a lot more often.

Architectural Benefits

The best thing about one-way isolation is that it's opt-in:

A programmer can write a complete Vale program without ever learning about regions.
A programmer can ignore any region markers and still understand the code; regions don't affect a program's semantics.

This is consistent with Vale's philosophy of avoiding forced complexity.

This has two extra benefits to the programmer:

They can get started with Vale right away without learning these more advanced concepts.
They can focus on the problem at hand while still iterating and building out the program, and add regions later once their profiling identifies where optimization is needed.

In a way, regions and isolation allow us to get the optimization power of borrow checking, with less restrictions and constraints.

Conclusion

As we saw, one-way isolation can allow us to use isolation even for data that points to things outside itself.

Part 4 shows how one object can contain another region's data inline, and Part 5 shows how that combined with one-way isolation can make certain patterns (iterating collections, calculating determinants, etc.) and entire architectures (like entity-component-system) zero-cost. 2

That's all for now! We hope you enjoyed this article. Stay tuned for the next article, which shows how one-way isolation works.

If you're impressed with our track record and believe in the direction we're heading, please consider sponsoring us on GitHub!

Sponsor us on GitHub!

With your support, we can bring regions to programmers worldwide.

See you next time!

- Evan Ovadia

Side Notes

(interesting tangential thoughts)

Notes [–] Notes [+] 0 1 2 3

If anything isn't clear, feel free to reach out via discord, twitter, or the subreddit! We love answering questions, and it helps us know how to improve our explanations.

We're aiming to complete regions by early 2024, check out the roadmap for more details.

Together, isolates, pure functions, and one-way isolation combine to form something that looks suspiciously like an entire new programming paradigm... whether that's true remains to be seen!

This is still a draft! TODOs:

Talk about how this lets us truly have an opt-in borrow checker thats much more usable, flexible, and intuitive. It seems to fit the natural structure of our programs much better. Isolates are what truly makes it an opt-in borrow checker.
Mention somewhere that with channels, we can send isolated messages that point outside to mutable data.
What happens when we have MyStruct<T> impl MyInterface, but then try to upcast MyStruct<a'Bork>? Does it become a a'MyInterface? but it itself isn't in region a'. Perhaps we need something like MyInterface + a'? Maybe we can get around it with a &''Something?
Seamless concurrency threads use this under the hood. I think even regular threads might be able to as well.

Vale's Vision

Vale aims to bring a new way of programming into the world that offers speed, safety, and ease of use.

The world needs something like this! Currently, most programming language work is in:

High-overhead languages involving reference counting and tracing garbage collection.
Complex languages (Ada/Spark, Coq, Rust, Haskell, etc.) which impose higher complexity burden and mental overhead on the programmer.

These are useful, but there is a vast field of possibilities in between, waiting to be explored!

Our aim is to explore that space, discover what it has to offer, and make speed and safety easier than ever before.

In this quest, we've discovered and implemented a lot of new techniques:

Generational Memory, for a language to ensure an object still exists at the time of dereferencing.
Higher RAII, a form of linear typing that enables destructors with parameters and returns.
Fearless FFI, which allows us to call into C without risk of accidentally corrupting Vale objects.
Perfect Replayability, to record all inputs and replay execution, and completely solve heisenbugs and race bugs.

These techniques have also opened up some new emergent possibilities, which we hope to implement:

Region Borrow Checking, which adds mutable aliasing support to a Rust-like borrow checker.
Hybrid-Generational Memory, which ensures that nobody destroys an object too early, for better optimizations.
Seamless concurrency, the ability to launch multiple threads that can access any pre-existing data without data races, without the need for refactoring the code or the data.
Object pools and bump-allocators that are memory-safe and decoupled, so no refactoring needed.

We also gain a lot of inspiration from other languages, and are finding new ways to combine their techniques:

We can mix an unsafe block with Fearless FFI to make a much safer systems programming language!
We can mix Erlang's isolation benefits with functional reactive programming to make much more resilient programs!
We can mix region borrow checking with Pony's iso to support shared mutability.

...plus a lot more interesting ideas to explore!

The Vale programming language is a novel combination of ideas from the research world and original innovations. Our goal is to publish our techniques, even the ones that couldn't fit in Vale, so that the world as a whole can benefit from our work here, not just those who use Vale.

Our medium-term goals:

Finish the Region Borrow Checker, to show the world that shared mutability can work with borrow checking!
Prototype Hybrid-Generational Memory in Vale, to see how fast and easy we can make single ownership.
Publish the Language Simplicity Manifesto, a collection of principles to keep programming languages' learning curves down.
Publish the Memory Safety Grimoire, a collection of "memory safety building blocks" that languages can potentially use to make new memory models, just like Vale combined generational references and scope tethering.

We aim to publish articles biweekly on all of these topics, and create and inspire the next generation of fast, safe, and easy programming languages.

If you want to support our work, please consider sponsoring us on GitHub!

With enough sponsorship, we can:

Work on this full-time.
Turn the Vale Language Project into a 501(c)(3) non-profit organization.
Make Vale into a production-ready language, and push it into the mainstream!

Sponsor us on GitHub!