8 ms·

Show HN: Cuq – Formal Verification of Rust GPU Kernels

94 points by nsomani 1y ago

nsomani 1y ago
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.
- gaogao 1y ago
  Do you think it might be easier to target cuTile instead of PTX? (Probably not, since it has a less formalized model?)
  - nsomani 1y ago
    That instinct is right. cuTile would be easier to parse but harder to reason about formally.
    - jroesch 1y ago
      We also have a formal memory model and the program semantics are simpler so if anything reasoning about it should be easier.
      - nsomani 1y ago
        Oh really? I can't find anything about the memory model online. I'm not sure what's the best way to do this, but if there's a way for us to get in contact, I'd be interested in adjusting the project so it's developed in the most ergonomic way possible. I'm chatting with a couple of universities and I might issue a research grant for this project to be further fleshed out, so would be keen to hear your insights prior to kicking this off. My email is neel[at]berkeley.edu.
      - gaogao 1y ago
        Oh also good talk at PTC yesterday! I had meant to ask you more about the formal memory model, but the other post talk questions ended up being really interesting too.
- YouAreWRONGtoo 1y ago
  [dead]
Hexigonz 1y ago
This is pretty cool! Are you sure about the name...
- NitpickLawyer 1y ago
  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.
  - bitwize 1y ago
    It's called Rocq now—for this reason.
    - sayrer 1y ago
      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. https://en.wikipedia.org/wiki/Le_Coq_Sportif https://en.wikipedia.org/wiki/Le_Coq_Sportif It's Nike now, but it still has a rooster on it.
      - OneDeuxTriSeiGo 1y ago
        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.
      - vlovich123 1y ago
        Coq is also named after the creator Coquand. It’s a shame that his work is being minimized because the English-speaking majority is sensitive and can’t hear a homonym for the slang for a male body part. I wish we sometimes lived in a world where people wouldn’t be afraid at work to discuss why they like or dislike Coq or whether it meets their needs or if it’s too much for them. A man can dream though, a man can dream.
- 1y ago
skrrtww 1y ago
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.
- 7bit 1y ago
  Yeah, coq is already bad, but cuq is the cherry on top of it. I don't like both.
  - tracker1 1y ago
    Like a similar thread... I always thought of "coq" as "co queue" in terms of as a word. "cuq" as "cook" with the cu as in "CUDA" etc.
- Dilettante_ 1y ago
  Maybe this surprises you, but some people have different sensibilities than you do.
- webdevver 1y ago
  not at all - its perfectly logical you are cucking the betabuxxed bugs in your kernels with your BFV (Big Formal Verifier)
- nsomani 1y ago
  Oh wow, honestly this caught me off guard - I've been pronouncing it "kook" in my head the whole time.
  - skrrtww 1y ago
    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.
    - 1y ago
thrownawaysz 1y ago
'Yer a cuq, Harry
ModernMech 1y ago
Two step guide to naming programming languages. 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.
orliesaurus 1y ago
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......
deleted 1y ago
[deleted]
the_real_cher 1y ago
I wished this name had been reserved for some sort of monitoring software.
kaffekaka 1y ago
As a swede I am reminded of the Honda Fitta.
- Rendello 1y ago
  Or Heinz's mayo-ketchup fusion, which had a funny translation in a local native language: "This new sandwich spread, whatever it is, they call it Mayochup, In Cree, it means shit-face. lol" https://www.cbc.ca/news/canada/sudbury/mayochup-cree-translation-1.5144737 https://www.cbc.ca/news/canada/sudbury/mayochup-cree-transla...
cboyardee 1y ago
[dead]
heromal 1y ago
Cuck?
dekerklas 1y ago
[flagged]

94 points by nsomani 1y ago

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.

gaogao 1y ago
Do you think it might be easier to target cuTile instead of PTX? (Probably not, since it has a less formalized model?)
- nsomani 1y ago
  That instinct is right. cuTile would be easier to parse but harder to reason about formally.
  - jroesch 1y ago
    We also have a formal memory model and the program semantics are simpler so if anything reasoning about it should be easier.
    - nsomani 1y ago
      Oh really? I can't find anything about the memory model online. I'm not sure what's the best way to do this, but if there's a way for us to get in contact, I'd be interested in adjusting the project so it's developed in the most ergonomic way possible. I'm chatting with a couple of universities and I might issue a research grant for this project to be further fleshed out, so would be keen to hear your insights prior to kicking this off. My email is neel[at]berkeley.edu.
    - gaogao 1y ago
      Oh also good talk at PTC yesterday! I had meant to ask you more about the formal memory model, but the other post talk questions ended up being really interesting too.
YouAreWRONGtoo 1y ago
[dead]

Hexigonz 1y ago

This is pretty cool! Are you sure about the name...

NitpickLawyer 1y ago
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.
- bitwize 1y ago
  It's called Rocq now—for this reason.
  - sayrer 1y ago
    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. https://en.wikipedia.org/wiki/Le_Coq_Sportif https://en.wikipedia.org/wiki/Le_Coq_Sportif It's Nike now, but it still has a rooster on it.
    - OneDeuxTriSeiGo 1y ago
      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.
    - vlovich123 1y ago
      Coq is also named after the creator Coquand. It’s a shame that his work is being minimized because the English-speaking majority is sensitive and can’t hear a homonym for the slang for a male body part. I wish we sometimes lived in a world where people wouldn’t be afraid at work to discuss why they like or dislike Coq or whether it meets their needs or if it’s too much for them. A man can dream though, a man can dream.
1y ago

skrrtww 1y ago

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.

7bit 1y ago
Yeah, coq is already bad, but cuq is the cherry on top of it. I don't like both.
- tracker1 1y ago
  Like a similar thread... I always thought of "coq" as "co queue" in terms of as a word. "cuq" as "cook" with the cu as in "CUDA" etc.
Dilettante_ 1y ago
Maybe this surprises you, but some people have different sensibilities than you do.
webdevver 1y ago
not at all - its perfectly logical you are cucking the betabuxxed bugs in your kernels with your BFV (Big Formal Verifier)
nsomani 1y ago
Oh wow, honestly this caught me off guard - I've been pronouncing it "kook" in my head the whole time.
- skrrtww 1y ago
  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.
  - 1y ago

thrownawaysz 1y ago

'Yer a cuq, Harry

ModernMech 1y ago

Two step guide to naming programming languages. 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.

orliesaurus 1y ago

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......

deleted 1y ago

[deleted]

the_real_cher 1y ago

I wished this name had been reserved for some sort of monitoring software.

kaffekaka 1y ago

As a swede I am reminded of the Honda Fitta.

Rendello 1y ago
Or Heinz's mayo-ketchup fusion, which had a funny translation in a local native language: "This new sandwich spread, whatever it is, they call it Mayochup, In Cree, it means shit-face. lol" https://www.cbc.ca/news/canada/sudbury/mayochup-cree-translation-1.5144737 https://www.cbc.ca/news/canada/sudbury/mayochup-cree-transla...

cboyardee 1y ago

[dead]

heromal 1y ago

Cuck?

dekerklas 1y ago

[flagged]