Hi all, this is a small research prototype I built that connects Rust's MIR (Mid-level IR) to Coq, the proof assistant used for formal verification.
cuq takes the MIR dump of a Rust CUDA kernel and translates it into a minimal Coq semantics that emits memory events, which are then lined up with the PTX memory model formalized by Lustig et al., ASPLOS 2019.
Right now it supports:
* a simple saxpy kernel (no atomics)
* an atomic flag kernel using acquire/release semantics
* a "negative" kernel that fails type/order checking
The goal isn't a full verified compiler yet. It's a first step toward formally checking the safety of GPU kernels written in Rust (e.g. correct use of atomics, barriers, and memory scopes).
Happy to hear thoughts from folks working in Rust verification, GPU compilers, or Coq tooling.
This might be the worst named project of all time. Not funny and demonstrates an absolutely terrible impulse on the part of the author. Probably the worst way possible to advertise your project.
edit: According to the author in a reply, the double entendre was in fact not intentional.
Step 1: Make sure no other programming language has the name you want.
Step 2: Make sure the name you want isn't a slur or rude word in all the languages your audience will write in. Be sure to check misspellings and homophones.
Optional 3rd step is to make sure the name lends itself to a cute animal mascot. For this project, I dunno maybe a corner chair is the mascot.
Reading through this thread, it seems the naming debate is taking up most of the oxygen, but the underlying technical goal behind the project is worth highlighting. Formal verification for GPU kernels could make massively parallel Rust code safer and more reliable as more workloads move onto GPUs. Race conditions and undefined behaviors in GPU programming are notoriously tricky to reason about;
HOWEVER, I'm curious whether a proof‑driven approach like this can scale beyond toy examples or specific hardware assumptions. If so, it might set a precedent for bringing formal methods to other low‑level domains too......
13 comments
[ 4.5 ms ] story [ 37.1 ms ] threadcuq takes the MIR dump of a Rust CUDA kernel and translates it into a minimal Coq semantics that emits memory events, which are then lined up with the PTX memory model formalized by Lustig et al., ASPLOS 2019.
Right now it supports:
* a simple saxpy kernel (no atomics)
* an atomic flag kernel using acquire/release semantics
* a "negative" kernel that fails type/order checking
The goal isn't a full verified compiler yet. It's a first step toward formally checking the safety of GPU kernels written in Rust (e.g. correct use of atomics, barriers, and memory scopes).
Happy to hear thoughts from folks working in Rust verification, GPU compilers, or Coq tooling.
edit: According to the author in a reply, the double entendre was in fact not intentional.
Step 1: Make sure no other programming language has the name you want.
Step 2: Make sure the name you want isn't a slur or rude word in all the languages your audience will write in. Be sure to check misspellings and homophones.
Optional 3rd step is to make sure the name lends itself to a cute animal mascot. For this project, I dunno maybe a corner chair is the mascot.
HOWEVER, I'm curious whether a proof‑driven approach like this can scale beyond toy examples or specific hardware assumptions. If so, it might set a precedent for bringing formal methods to other low‑level domains too......