Valen's Memory Safety: A New Kind of Borrow Checking

116 pointsposted 8 hours ago
by verdagon
(verdagon.dev)

42 Comments

EliasLittle

12 minutes ago

This is super exciting!

Having mutability not be a property of the data, but of the function arguments reminds me a lot of modes from Jane Street’s OxCaml ^1 which is really interesting to me, as OxCaml’s focus is not really about memory management (they still use garbage collection for everything not on the stack). Feels like we might be converging towards a new standard! I can see the morning sun on the horizon :)

[1]: https://oxcaml.org/documentation/modes/intro/

aaron_m04

4 minutes ago

> Having mutability not be a property of the data, but of the function arguments [...]

I don't know if you were aware of this, but Rust has that too. (Actually it's a property of any binding, not just function parameters)

zamalek

3 hours ago

> Borrow checking has the "shared-xor-mutable" restriction: if you hold a reference to an object, nobody else can change the object.

The article makes this sound like a problem. It isn't. This restriction frees you from thinking about certain classes of bugs in concurrent code; it's where the "fearless concurrency" comes from. R^w isn't about lifetimes - you could, in spirit (not sure about practice), remove it from Rust without affecting use-after-free at all.

Of course, it means you can't write many completely valid programs, and so we'd hope there's a better solution, but removing it is not one.

If you want to have to think about that (and potentially introduce bugs), that's perfectly fine. The flexibility of not requiring r^w is extremely useful. I'm just clearing up this mis-attribution.

verdagon

2 hours ago

Just to clarify, Valen's borrow checker can express shared-xor-mutable, its value proposition is that it can _also_ express mutable aliasing (with `in`).

* When a function has a mutable effect into a group, and the function doesn't declare any other groups to alias it (with `in`), it is effectively a unique reference.

* When a function has references into a group, and it declares no `mut` effects into any of them, they are effectively shared/immutable references.

This helps with Valen's structured concurrency in particular, but also helps guard against the single-threaded race conditions in the same way that Rust's borrow checker does. It also helps with Rust interop!

So, TL;DR: Valen lets you choose between shared-xor-mutable and mutable aliasing.

Also note how mutable aliasing is opt-in (via `in`), so there's a subtle influence pushing people towards shared-xor-mutable, so that they only reach for mutable aliasing when it will benefit them.

uhhuak

an hour ago

> "fearless concurrency"

That saying does more harm than good, and it counts against the Rust community that it keeps repeating it. Deadlocks are not something that Rust prevents. On the contrary, many beginners to Rust often run into deadlocks, some even spurred on by trying to satisfy the borrow checker. An infamous example is https://fasterthanli.me/articles/a-rust-match-made-in-hell . Instead of making blatantly false claims and causing newcomers to Rust frustration, pain and bugs, the Rust community should warn about concurrency and direct beginners to learn about concurrency, both generally as well as specifically in Rust.

kvark

5 hours ago

It sounds more like "path" borrowing than "group" borrowing to me, but the idea is great! Quite eye opening!

One minor thing is that I'm not sure why they had to have "in" keyword for sub-borrows. Wouldn't it be more consistent to see "entity &world.entities[?]" instead of "entity in world.entities[]"? We'd consistently get the borrow "&" symbol and open the door for some contracts on what index (range) is affected.

cmrx64

3 hours ago

(hi kvark, long time!) it’s a clever algorithm, if you’re curious about other factorizations of referentiality frames I’ve been tinkering with analyzer across interpretation boundary like the gpu command queue :) I need to get some writing together. the techniques like from this post are a little “cute” compared to what real systems need.

verdagon

8 hours ago

Also, as I was writing this, a couple things occurred to me:

* We _could_ use the function parameter syntax `entities: &world.entities[]` instead of `entities in world.entities[]`.

* "Groups" aren't really central to understanding the idea, so Path Borrowing might be a better name than Group Borrowing.

Opinions welcome =)

falserum

9 minutes ago

A bit more fuel for the bikesheding aspect of this:

Subtree borrowing.

(Single ownership stemming from main is a tree of owners; each path specifies some subtree)

(Btw. I enjoyed reading it)

munchler

6 hours ago

FWIW `foo in bar` implies iteration to me, not a path. In the .NET world, for example, `bar` would be a collection that we’re iterating through, assigning each element to `foo` in turn.

_old_dude_

3 hours ago

Assuming “groups” are mainly about grouped invalidation, I agree, Path Borrowing is the better name, since it describes the core idea rather than the implementation mechanism.

giovannibonetti

6 hours ago

I wonder if nowadays we should be focusing less on scalar data structures and more on languages that facilitate vectorized/SIMD instructions. Languages like Vx lang, Mojo, and Futhark that work both in the CPU or the GPU, although each one works in a different level of abstraction and control.

verdagon

6 hours ago

GPU compilation is definitely something I intend Valen to support. I wrote about it back in 2022, [0] and I learned a lot of lessons on how to do it (and how not to do it!) from working on the Mojo compiler.

The biggest decision for Valen is what to lower to:

* Rust MIR, since rustc has CUDA now, [1] (perhaps other cards soon?)

* SPIR-V, like Zig does for its GPU compilation [2]

* MLIR

Rust MIR is looking pretty nice. Valen already has Rust interop by doing some rustc sorcery, [3] and it would be somewhat straightforward to switch from emitting LLVM to emitting Rust MIR. I just need to figure out if Rust MIR can support the optimizations I have planned for Valen.

In a perfect world, Rust would be able to lower its MIR to MLIR, since MLIR has so many backends. I recall there were some efforts to do that, unsure where that ended up.

[0] https://verdagon.dev/blog/next-gen-languages-gpu

[1] https://developer.nvidia.com/blog/introducing-cuda-rust-two-...

[2] https://ziglang.org/devlog/2026/#2026-06-26

[3] https://verdagon.dev/blog/golden-spike-reviving-vale-valen

peesem

6 hours ago

nit: you need a better way of laying out asides/footnotes. when they get bunched up like at the start of this article you start having to scroll full screens back and forth. at least make the numbers on the asides link back to their position in the main text

Cpoll

5 hours ago

They're fragment links, so you can use your browser's back button to go back to where you were.

verdagon

6 hours ago

Yes, absolutely, lol. This article is really pushing my notes system past its limits. And it loops between six note colors, which normally isn't a problem, but is here. During the holidays, I want to see if I can implement Tufte notes like in https://edwardtufte.github.io/tufte-css/

Hunpeter

4 hours ago

Off-topic (as I don't have the knowledge to intelligently comment on the concept): all I can think when I hear the name "Valen" is Babylon 5. I wonder if it's a coincidence or a deliberate reference?

variaga

3 hours ago

The about page says Valen is a successor to the Vale programming language, so I doubt it.

melodyogonna

3 hours ago

Mojo's origin can represent a lot of these semantics. I think a lot was learned from Nick's proposal, even if it wasn't directly implemented. Here is an example of how you could represent the first snippet, where two references can update the same list: https://godbolt.org/z/78bhzWjYM

verdagon

3 hours ago

Unfortunately, Mojo kind of limits itself by forcing all parameters to be unique references or shared references. So the first example works in Mojo, but not the `step` example nor the `attack` example from the original group borrowing explanation. [0]

I hope they one day upgrade to full group borrowing, it would be a nice fit for them.

[0] https://verdagon.dev/blog/group-borrowing

amluto

4 hours ago

Neat!

I have a question about immutability. In Rust, if I have a shared reference to T (an &T a variable or a parameter), then I have a restriction that I can't modify T or anything in it (which Valen thinks is annoyingly restrictive, and I tend to agree), but I also have a promise that no one else will modify it. The latter is quite nice: it makes the optimizer happier (improves aliasing analysis), makes threading happier (nothing descended from the reference can have data races while the reference is alive), and makes me happier (I don't need to think about descendent values being mutated).

Valen can call into Rust, and I think I can see how, at the site of any particular call, Valen can tell that no one is mutating the referent or its descendents: in a single-threaded world, the only thing executing is the current line of code or a maybe a few consecutive lines of code, and the compiler can see the function's signature and any mutable references therein, and if there is no permission to modify a descendent, then it doesn't get modified.

But in a multithreaded world, especially if calling into Rust in a thread, doesn't there need to be a way to guarantee the immutability of an object across an entire region of code? How does that work in Valen?

And for making immutability more comprehensible to people and to local analysis in general, would a special type of reference meaning "yes, this one really is fully frozen and there are no mutable paths into it for the entire lifetime of this reference" be a nice feature?

(Aside: I've occasionally contemplated whether Rust would benefit from another flavor of reference: no-access. A no-access reference would guarantee the referent's existence but could coexist with shared and with mutable references. Safe code would be unable to read or write through such a reference. Other than making some cell-like types mildly less mind-bending, I'm not convinced I have an actual justification for this thing. This would give Rust three flavors of references.

But I can imagine a Valen-like language having three flavors of references: frozen references (cannot use them to mutate and there's a promise that no one else can either), exclusive references (fully mutable, etc, just like Rust's &mut) and flexible references (the kind of reference in the blog post).)

verdagon

2 hours ago

Awesome question, you're getting at the good stuff.

Short answer: Valen would have something similar to Fn and FnMut (but phrased in terms of effects rather than Fn vs FnMut). In other words, we would be able to express "a closure that does not modify anything it captures", or rather, "a closure that has no mut effects".

That closure, because it doesn't modify anything it captures, would be safe to share among multiple threads in a structured-concurrency-like / std::thread::scope-ish way.

The key here is that one _can_ express immutable references in Valen; an immutable reference is a reference that the containing function doesn't express a `mut` effect for. And once we have immutable references, we get all of the nice concurrency benefits that Rust trailblazed.

I'd also like to make a way to do the above without a function call, perhaps using something like the `parallel` keyword I described in [0].

A no-access reference is an interesting idea. That could be a more powerful way to express may_dangle. In Valen, I hope to have an "opaque" group to express something like that.

I don't know whether it's a good idea, but in Valen I'm trying to decouple access capabilities away from the reference types as much as possible. We'll see if that bet pays off.

[0] https://verdagon.dev/blog/seamless-fearless-structured-concu...

AlotOfReading

2 hours ago

    I've occasionally contemplated whether Rust would benefit from another flavor of reference: no-access.
Most of the uses for this I can think of are best solved by opaque pointers for FFI. Having a rust-native reference just seems incongruous. Like, does it have size and alignment info? How would it interact with NLL? The only way I can imagine it working is if it extended referent lifetime throughout the lexical lifetime of the reference, but that defeats the purpose of NLL.

Rust solves a similar problem in closures with unique immutable references, but they're not quite the same.

SleepyMyroslav

2 hours ago

This looks cool for code-driven systems where code has static knowledge of every path in the system. It might be strictly better for things like rendering where types of rendering are code-driven. Like your world can have skybox and such. The examples assuming gamedev 'world' and 'entity' are completely misleading though. Because I think everyone has moved on to data-driven worlds. Think of entity 'advance' from the code examples as an 'entity blueprint execute'.

maufl

6 hours ago

How likely is it that such a borrow checker could be "backported" to Rust? Maybe in a new edition?

verdagon

6 hours ago

You know, it's not crazy. Niko wrote about lifetimes based on places back in 2024, [0] though it was in the context of shared-xor-mutable, which is consistent with Rust's spirit.

And Rust already supports forms of mutable aliasing already, such as with Cell, and GhostCell which is halfway towards Valen's approach. I would love to see someone augment GhostCell to have the sort of "invalidation" logic that group borrowing does. In fact, Plecra is working on something like that with their (WIP) "Exclusion Typing". [1]

On top of that, Polonius already thinks in terms of "paths", just like Valen does. So it's not so much a question of compiler design, but of language design, and how Rust would expose it to the user.

[0] https://smallcultfollowing.com/babysteps/blog/2024/06/02/the...

[1] https://dilated.me/blog/posts/introduction-to-exclusion-typi...

zozbot234

4 hours ago

It would have to take &Cell<T> references or the like in order to preserve the existing uniqueness properties for &mut T references. Not so different ultimately from what GhostCell, QCell, LCell etc. do already, except possibly simpler in some ways.

sebastianmestre

7 hours ago

IIRC this Verdagon guy had a language called Vale... is Valen a rename or a new project?

Edit: tfa makes it clear it's a separate project

verdagon

7 hours ago

Hi! Kind of both. Even though Valen reuses 90% of the Vale compiler, its approach (Rust interop, borrow checking with mutable aliasing, etc.) is so different that it really needed a new name.

Also, I really like where Vale ended up, Vale's generational references + region borrowing was a truly weird and unusual memory safety blend. I didn't want that combination to be lost to time, so I wanted "Vale" to keep referring to that.

user142

6 hours ago

I noticed that there is no control flow in the examples.

verdagon

6 hours ago

Next article =) How the borrow checker handles ifs and loops is a pretty fun topic. If-statements work like you'd expect (invalidations from both branches are merged). Loops is where it gets weird: we have to scout all the invalidations that happen inside the loop and then "replay" them _before_ the body of the loop. I can explain it more if you'd like.

JackSlateur

3 hours ago

Checking the following code, could you confirm that is does not work concurrently ? The "world" var is read-only, does it mean that all other entities are also readonly (cannot be modified by another thread, for instance) ?

  struct World {
    entities Vec<Entity>;
  }
  func step(world &World, entity in world.entities[] mut) {
    entity.advance();
    let collision = world.get_collision_for_entity(entity);
    entity.resolve(collision);
  }

verdagon

2 hours ago

Yep, that works today. The neat thing here is that `world` is immutable _except_ for its `.entities[]` elements.

That wouldn't be shareable with another thread, because part of it is `mut`. _Theoretically_ we could make this shareable with other threads if we had another kind of effect, let me know if you're curious about that.

The `entity in world.entities[] mut` gives `step` blanket permission to mutate any element inside world.entities. We wouldn't be able to say "all other entities are readonly".

Though, it's worth mentioning that `advance` and `resolve` both receive the entity as a unique reference (since it's the only reference into a group which has a mut effect).

octoberfranklin

an hour ago

A function signature describes the paths it modifies.

The problem with this is that it imposes a cost on abstraction. Zero-cost abstraction is one of the most fundamental design principles behind both C++ and Rust.

A field-path into a struct/enum fundamentally depends on its concrete implementation. If you hide the fields of a struct and use getters/setters, you break the ability to talk about the "paths modified" by a function which uses getters/setters.

Aside: it really annoyed me that I had to read halfway through this article to find the first attempt at defining "group borrowing". The whole first half of the article is basically fluff.

swiftcoder

an hour ago

> The whole first half of the article is basically fluff

There are multiple links in the article that suggest the reader skip to the good stuff if they are already familiar with how borrow checking works

fithisux

6 hours ago

Is it possible to retrofit it to Freepascal, D, Freebasic or even Java?

verdagon

6 hours ago

Maybe! I think about D a lot when designing Valen, since they attempted to blend borrowing with garbage collection. Swift is facing some of the same challenges, and I expect Java could soon too now that Valhalla has landed.

If Valen solves those challenges as well as I think it can, it could be a good direction for them to explore.

falconBrisk47

7 hours ago

Path Borrowing reads clearer to me, "group" made me look for a group type.