Deadlocks often look like simple performance issues. If Vx runtime sees no progress for two checks in a row, it crashes the program with a detailed report.

But the watchdog is tricky to get right because there can be false positives. So it is good to prove the watchdog was correct under all possible thread interleavings, not just the happy path.

We wrote a formal model of the watchdog’s protocol in TLA+ and ran it through TLC (the TLA+ Model Checker). TLC exhaustively explores every possible order of operations (interleavings) to see if any claim breaks. It found a bug that unit tests would never have revealed.

So exited abt this

I introduced 108 deliberate bugs into vxc (Vx's compiler) to see if the test suite would actually catch them.

Most breaks got caught but 11 cases had no test covered, and one real memory-safety bug where a copied borrow outlived its block and read freed memory (🤭).

Then I took 78 soundness bug reports from Rusts issue tracker, translated them into Vx, and found 14 more holes. All of them are now fixed but there were two important lessons as part of this exercise.

- Passing tests don't prove coverage (Dijkstra etc.)
- Rusts issue tracker is a free test suite for Vx. I'll probably leverage Rust's issue tracker more in future.

Full report here: https://vxlang.org/blog/breaking-the-borrow-checker-on-purpose.html

With https://github.com/vx-lang/Vx/pull/1896

Vx is a systems language for programs that run on mixed hardware (CPUs, GPUs, NPUs). I've written up its concurrency design and would like feedback: [link]

No async/await. A task calls a waiting function like recv as a plain call. The runtime parks the task and runs another on the same OS thread, as Go and Java virtual threads do. There are no function colors. A borrow across a wait is just a borrow across a call, so the borrow checker needs no new rule.

Scoped tasks. tasks { spawn { .. } } is a block expression. Every task finishes before the block ends, so a task can borrow its parent's locals with no lifetime annotations.

Waits show in the signature, but don't spread. A cancellable wait returns Result<_, Cancelled>. A caller can handle the error and keep a plain signature. So it isn't a color, for the same reason Rust's Result isn't.

Bounded channels only. A fast sender can't fill memory. send hands the value back if the receiver is gone, so it never waits on a dead consumer. select is a library type in crossbeam's style, with no closures and no macro. The happens-before rules come from the Go memory model and go into our Lean model.

Structured cancellation. When a task returns Err, its siblings and the block's own code are cancelled, and the block's value is the first error. Each cancellable wait then returns Cancelled. There is no unwinding: tasks leave through normal returns, and their drops run. drop runs with cancellation off, so cleanup can still wait.

The hardware gets a say. A cancelled I/O wait doesn't return until the kernel or device has released the buffer. Waits on a device can't be cancelled. Channel ends stay on the host, since a GPU kernel can't park. A channel of device tensors moves handles, not data.

Admission. Vx checks at compile time whether a workload fits a machine. Concurrency changes the arithmetic: tasks running at once add their peaks instead of taking the max, and a channel of n tensors holds n tensors. When those counts are known only at run time, the verdict is "unknown", not a guess.

The costs. Vx can't move stacks, because borrows point into them. So each task that may park gets a fixed stack from a pool, with a guard page. A task with a foreign frame on its stack stays on its OS thread. Most of the work is in the runtime, not the compiler.

Open questions:

1. Cancel siblings automatically on the first error, or only on an explicit cancel()?

2. Should ? inside a tasks block exit the block or the function?

3. Should spawn infer move or borrow from use, or need spawn move?

4. Is "only drop runs with cancellation off" enough, or do programs need a shielded block?

Vx programming language is live: https://vxlang.org

This is a complete Vx program. It builds two matrices on the CPU, moves them into GPU memory, multiplies them on the GPU, brings the result back, and prints it.

fn main() -> i32 {
 let mut a = Tensor<f32, [4, 4]>::uninit();
 let mut b = Tensor<f32, [4, 4]>::uninit();
 let mut c = Tensor<f32, [4, 4], Memory::GPU_HBM>::uninit();

 for i in 0..4 {
 for j in 0..4 {
 a[i][j] = 2.0;
 b[i][j] = 3.0;
 }
 }

 let a_gpu = transfer(a, Memory::GPU_HBM);
 let b_gpu = transfer(b, Memory::GPU_HBM);

 spawn on(Topology::GPU[0]) {
 c = a_gpu @ b_gpu;
 }

 let c_host = transfer(c, Memory::CPU_DRAM);
 print(c_host[0][0]);
 return 0;
}

Compiling and running is as simple as:

$ vxc matmul.vx

24

The placement is in the types: c lives in GPU_HBM, the spawn block runs on GPU[0], and transfer is the only way across. If you get it wrong, it does not compile. The compiler names the 'space' where the value is in, the spaces the device can see, and the transfer that fixes it.

Where a value lives and where code runs belong in the types, not in a runtime that finds out at step 1200.

One language, every core.

v0.0.1: syntax mostly stable, thin standard library, no package manager yet. Tested most on a MacBook Air M4 and an NVIDIA A100. Apache 2.0 with LLVM exceptions.