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 13 days ago | parent | next [-]

Do you think it might be easier to target cuTile instead of PTX? (Probably not, since it has a less formalized model?)

▲

nsomani 13 days ago | parent [-]

That instinct is right. cuTile would be easier to parse but harder to reason about formally.

▲

jroesch 12 days ago | parent [-]

We also have a formal memory model and the program semantics are simpler so if anything reasoning about it should be easier.

	▲	gaogao 12 days ago \| parent \| next [-]
		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.
	▲	nsomani 12 days ago \| parent \| prev [-]
		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.

▲

YouAreWRONGtoo 9 days ago | parent | prev [-]

[dead]