7 ms·

Show HN: Cuq – Formal Verification of Rust GPU Kernels

94 points by nsomani 11mo ago

Hexigonz 11mo ago
This is pretty cool! Are you sure about the name...
- NitpickLawyer 11mo 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 11mo ago
    It's called Rocq now—for this reason.
    - sayrer 11mo 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 11mo 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 11mo 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.
- CaptainOfCoit 11mo ago
  I'm getting a ԃҽʝα ʋυ
- hnuser123456 11mo ago
  Bonus points if it runs on UNIX
- VoodooJuJu 11mo ago
  [dead]
- ahallock 11mo ago
  Aren't we more mature than this? Granted, it's the first thing I thought of as well
  - 7bit 11mo ago
    Can we instead please be mature about choosing a adequate sounding name?
nsomani 11mo 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 11mo ago
  Do you think it might be easier to target cuTile instead of PTX? (Probably not, since it has a less formalized model?)
  - nsomani 11mo ago
    That instinct is right. cuTile would be easier to parse but harder to reason about formally.
    - jroesch 11mo ago
      We also have a formal memory model and the program semantics are simpler so if anything reasoning about it should be easier.
      - nsomani 11mo 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.
skrrtww 11mo 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.
- Dilettante_ 11mo ago
  Maybe this surprises you, but some people have different sensibilities than you do.
- webdevver 11mo ago
  not at all - its perfectly logical you are cucking the betabuxxed bugs in your kernels with your BFV (Big Formal Verifier)
- nsomani 11mo ago
  Oh wow, honestly this caught me off guard - I've been pronouncing it "kook" in my head the whole time.
  - skrrtww 11mo 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.
    - nsomani 11mo ago
      I think I've just spent too much time reading the word "CUDA" that I read "cu" as "koo", lol.
  - skavi 11mo ago
    It's your project, but with the current name I'd expect this thread to be duplicated any time the project is discussed.
- OneDeuxTriSeiGo 11mo ago
thrownawaysz 11mo ago
'Yer a cuq, Harry
ModernMech 11mo 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 11mo 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 11mo ago
[deleted]
the_real_cher 11mo ago
I wished this name had been reserved for some sort of monitoring software.
kaffekaka 11mo ago
As a swede I am reminded of the Honda Fitta.
- Rendello 11mo 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 11mo ago
[dead]
heromal 11mo ago
Cuck?
dekerklas 11mo ago
[flagged]

94 points by nsomani 11mo ago

Hexigonz 11mo ago

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

NitpickLawyer 11mo 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 11mo ago
  It's called Rocq now—for this reason.
  - sayrer 11mo 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 11mo 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 11mo 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.
CaptainOfCoit 11mo ago
I'm getting a ԃҽʝα ʋυ
hnuser123456 11mo ago
Bonus points if it runs on UNIX
VoodooJuJu 11mo ago
[dead]
ahallock 11mo ago
Aren't we more mature than this? Granted, it's the first thing I thought of as well
- 7bit 11mo ago
  Can we instead please be mature about choosing a adequate sounding name?

nsomani 11mo 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 11mo ago
Do you think it might be easier to target cuTile instead of PTX? (Probably not, since it has a less formalized model?)
- nsomani 11mo ago
  That instinct is right. cuTile would be easier to parse but harder to reason about formally.
  - jroesch 11mo ago
    We also have a formal memory model and the program semantics are simpler so if anything reasoning about it should be easier.
    - nsomani 11mo 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.

skrrtww 11mo 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.

Dilettante_ 11mo ago
Maybe this surprises you, but some people have different sensibilities than you do.
webdevver 11mo ago
not at all - its perfectly logical you are cucking the betabuxxed bugs in your kernels with your BFV (Big Formal Verifier)
nsomani 11mo ago
Oh wow, honestly this caught me off guard - I've been pronouncing it "kook" in my head the whole time.
- skrrtww 11mo 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.
  - nsomani 11mo ago
    I think I've just spent too much time reading the word "CUDA" that I read "cu" as "koo", lol.
- skavi 11mo ago
  It's your project, but with the current name I'd expect this thread to be duplicated any time the project is discussed.
OneDeuxTriSeiGo 11mo ago

thrownawaysz 11mo ago

'Yer a cuq, Harry

ModernMech 11mo 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 11mo 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 11mo ago

[deleted]

the_real_cher 11mo ago

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

kaffekaka 11mo ago

As a swede I am reminded of the Honda Fitta.

Rendello 11mo 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 11mo ago

[dead]

heromal 11mo ago

Cuck?

dekerklas 11mo ago

[flagged]