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.
If this was genuinely unintentional on your part, then bless your heart and I'm sorry for assuming the worst. You might be the least morally corrupted internet user alive today.
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.
Yeah, "coq" is a grade school joke in French class. It just means "rooster" or something in French, but it sounds ridiculous in English. This one has the same problem.
A company with that in the name made the French national team jersey for a while.
To be entirely fair cock (which surprisingly isn't actually derived from french but from english's germanic roots) also means rooster in english as well.
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.
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.
edit: According to the author in a reply, the double entendre was in fact not intentional.
Just go ahead and rename this project to "Rocuda", save everyone a lot of time arguing about what names are appropriate or not.
I'd expect cuke, if pronounced like cucumber would be queueck or cuck depending on which cu in cucumber you're using.
However I pronounce CUDA koo-da so cuq would be pronounced perhaps like kook.
you are cucking the betabuxxed bugs in your kernels with your BFV (Big Formal Verifier)
A company with that in the name made the French national team jersey for a while.
https://en.wikipedia.org/wiki/Le_Coq_Sportif
It's Nike now, but it still has a rooster on it.
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.