logoalt Hacker News

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

123 points • by verdagon • today at 12:06 PM • 74 comments • view on HN

Comments

Animats • today at 9:49 PM

> But group borrowing actually resolves the conflict, by relaxing "shared-xor-mutable" to "no use-after-free".

That's the one line that defines what's going on here.

If all you want is "no use after free", either reference counts or garbage collection will do the job. That's how most GC-oriented languages work.

Rust enforces stricter rules - single ownership, one writer or N readers. The question is whether that's worth the trouble. In threaded programs, it definitely is, because it prevents race conditions. Whether it's a win for single-thread programs is a good question.

Vale seems to be a way to move much of the overhead of a reference-counted system at compile time. Nothing wrong with that. The main motivation seems to be better interoperability with less restrictive languages. Am I reading that correctly?

➕ show 1 reply
zamalek • today at 5:33 PM

> 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.

➕ show 1 reply
kvark • today at 3:11 PM

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.

➕ show 1 reply
verdagon • today at 12:20 PM

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 =)

➕ show 3 replies
giovannibonetti • today at 1:46 PM

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.

➕ show 2 replies
amluto • today at 3:53 PM

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).)

➕ show 2 replies
EliasLittle • today at 8:04 PM

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/

➕ show 1 reply
peesem • today at 2:13 PM

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

➕ show 2 replies
Hunpeter • today at 4:42 PM

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?

➕ show 1 reply
melodyogonna • today at 5:26 PM

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

➕ show 1 reply
SleepyMyroslav • today at 5:50 PM

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 • today at 1:53 PM

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

➕ show 2 replies
sebastianmestre • today at 12:46 PM

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

➕ show 1 reply
c-fe • today at 4:37 PM

the link under recent posts here https://verdagon.dev/home 404s, as it links to https://verdagon.dev/blog/valen-memory-safety instead of https://verdagon.dev/blog/valen-group-borrowing . Interstingly this shows the page is hosted on Firebase, which is a bit unexpected for a static blog

➕ show 1 reply
user142 • today at 2:10 PM

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

➕ show 1 reply
JackSlateur • today at 5:31 PM

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);
  }
➕ show 1 reply
fithisux • today at 2:14 PM

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

➕ show 1 reply
octoberfranklin • today at 6:51 PM

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.

➕ show 1 reply
falconBrisk47 • today at 12:53 PM

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