Show HN: Cuq – Formal Verification of Rust GPU Kernels
1–10 of 70 posts
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#2Hi 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.
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#3This is pretty cool! Are you sure about the name...
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#4This is pretty cool! Are you sure about the name...
It's a system where a 3rd party library (aptly named Coq) gets to throughly verify your kernel, and you get to watch it do its thing? I think the name is fitting.
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#5This is pretty cool! Are you sure about the name...
I'm getting a ԃҽʝα ʋυ
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#6This is pretty cool! Are you sure about the name...
Bonus points if it runs on UNIX
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#7This is pretty cool! Are you sure about the name...
[dead]
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#8This 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.
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#9Hi 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) *…
Do you think it might be easier to target cuTile instead of PTX? (Probably not, since it has a less formalized model?)
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#10This 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.
Maybe this surprises you, but some people have different sensibilities than you do.