Glonce

Valen's borrow checker walks functions backwards to catch use-after-free

toolsThe Glonce editorsHacker News🔥44Glonce rating44Impact25Novelty45Relevance70Surprise45Players5Credibility60

A blog post on verdagon.dev describes an unusual design in the borrow checker of Valen, a language whose checker makes shared-xor-mutable optional and can call into Rust functions with memory safety across the boundary. The author says it is similar to Rust's borrow checker but also allows memory-safe mutable aliasing. The twist is direction: the use-after-free check walks each function backwards, from the last statement to the top. As far as the author knows, it is the only borrow checker whose safety check goes backwards.

Valen compiles a function in four phases. Phase 2 is static typing, an ordinary forward pass that assigns types to variables (for example, turning let fuel = 5; into let fuel i64 = 5;). Phase 3 is static grouping, another forward pass that works out where each reference points. In print_first_fuel_cell, it determines that first_ref is a &int pointing somewhere in the s.fuel_cells[] array, and that information becomes part of the variable's type. Phase 4 is the use-after-free check, and it is the one that runs in reverse. The author mentions a secret fifth phase that computes attributes to send to LLVM, which is out of scope for the post. In Valen's first version (V1), static grouping also recorded the line where a reference was made; V2 does not need that because of the backwards scan. The author also says the term "group" will probably give way to "path" soon, and invites opinions.

The backward scan looks for three kinds of events: DECLARE, USE and MUTATE. It keeps a pending list of everything used further down that the scan hopes to see declared above. A USE adds a variable to pending, a DECLARE removes it, and a MUTATE triggers a check that nothing in pending points at anything under the mutated group.

The first example is a function foo(e &Entity mut) that takes let buff = &e.buffs[0];, then calls e.add_buff(), then calls print_int(buff). Scanning upward, the checker meets print_int(buff) first and adds buff (group g.buffs[]) to pending. It then reaches e.add_buff(), which is a USE of e and a MUTATE of group g. Because buff points into g.buffs[], which starts with the mutated g, buff is invalidated above the line where it is used. That is a use-after-free, and the compiler reports an error.

In the corrected version, e.add_buff() is moved to the first line. The scan adds buff to pending at print_int(buff), removes it at the let buff declaration, leaving pending empty, and then reaches the MUTATE with nothing to check. It adds e to pending at the USE and finishes the function without a MUTATE hitting any pending variable, so the program is memory-safe. The author adds that the first person to break the algorithm gets a prize.

The author gives three reasons for going backwards: convenience, loops and speed.

Convenience: a backward scan makes it easy to find the last use of a variable. In an attack function with seven statements, bookkeeping at a variable's last use (such as decrementing a reference count, inserting a destructor call or checking for use-after-free) needs an extra fetch-and-navigate step in a forward scan, because the last use cannot be recognised when it is met. The backward scan is simpler.

Loops: two examples show why. In a correct program, a loop calls observe(e), then add_element(&arr), then set e = &arr[0]. The e in observe can come from two places, so a forward scan would have to look ahead to the set e to conclude the use is valid. Remove the set e and the e in the loop is invalidated by a previous iteration, so a forward scan would have to look ahead to confirm nothing revives it. The author sets out options for tackling this; the last was tempting, but its data structures looked very complex and had the same fetch-and-navigate problem. Going straight to the reverse walk was simpler. Loops still need adjustments: MUTATE and DECLARE are handled differently, and the checker reacts to a LOOP START event. In the worked loop example, a DECLARE puts e into a revived_after_this set, a MUTATE of arr puts it into mutations_after_this, and a USE puts e into pending. At the loop start, the checker tests each pending item against the loop's mutations; the text available here cuts off in that sentence.

Speed: the author is fairly certain that V2's approach is faster, because each node is processed once in the phase 3 forward pass and once in the phase 4 backward pass. The post does not yet claim O(n): MUTATE still has to check everything in the pending list, though the author thinks that check can be sped up a lot. There is no benchmark for loops, because V1 never had full loop support. A side note says the examples use the name ArrayList, but the real compiler calls it Array, and that will change soon. The post also states that 0% of it was written by AI.

Key facts

  • Valen's V2 borrow checker runs its use-after-free check in reverse, from the last statement of a function up to the top; the author believes it is the only borrow checker to do so.
  • Valen compiles a function in four phases: phase 2 static typing and phase 3 static grouping are forward passes, and phase 4 is the backward safety check.
  • The scan tracks DECLARE, USE and MUTATE events with a pending list: a MUTATE that invalidates anything in pending is a use-after-free and produces a compiler error.
  • The author gives three reasons for going backwards: convenience (finding last use), loops, and speed.
  • The speed advantage is the author's belief, not a measurement: each node is processed once forward and once backward, but the algorithm is not yet O(n) because MUTATE checks the whole pending list.

Why it matters

Borrow checkers are usually described as forward analyses, and the author says no other borrow checker is known to check memory safety backwards. Reverse passes are common in optimisation work, and the post argues they also fit safety checking. The claimed gains are simpler last-use detection, simpler loop handling and a lighter pass structure. In V1, references carried the line where they were made inside their types; V2 drops that bookkeeping.

Who it affects

Mainly people who design or implement compilers, borrow checkers and memory-safety systems, and people following Valen, whose checker makes shared-xor-mutable optional and can call Rust functions with memory safety across the boundary. It is a language design essay, not a product announcement.

How to use it

The post is an explanation, not a download. A reader can follow the two worked examples to see the pending list in action: a MUTATE that hits a pending variable is an error, and a DECLARE removes a variable from pending. The author invites readers to try to break the algorithm, with a prize for the first person who does, and welcomes opinions on renaming "group" to "path".

How solid is it

It is one author's account of the author's own compiler. The core mechanism is shown through two small worked examples. The speed claim is hedged in the post itself ("fairly certain"), and no benchmark is given; the algorithm is not yet O(n). The loop section is only partly covered here, and the final result of the LOOP START check is not visible in the available text. No formal soundness proof is given.

Risks and caveats

Loops need extra machinery (adjusted MUTATE and DECLARE handling plus a LOOP START check), so the reverse walk is not free there. There is nothing to benchmark loops against, because V1 never had full loop support. The MUTATE check against the whole pending list is a known cost, and the proposed speed-up is only a hope. Details such as the group-to-path rename and the ArrayList-to-Array naming are still in flux. The claim of uniqueness is hedged with "as far as I know".

“as far as I know, it's the only borrow checker whose safety check goes backwards.”

— The author of the verdagon.dev post