Is there some lib or even research paper on using coq to prove correctness of gpgpu program ? I suspect it's possible to use monad to model non pure computation as usual but gpu kernels are usually very low level code (manual management of cache and cache sync), I wonder if there was some work on building an élégant abstraction on top of this in order to make proof tractable.
there's quite a few different threads of work in the last 3-4 years on Coq-based verification of GPU-related languages, e.g., https://personal.utdallas.edu/~hamlen/ferrell19date.pdf https://dl.acm.org/doi/10.1145/3299771.3299798 https://www.jstage.jst.go.jp/article/ipsjjip/24/1/24_132/_pdf/-char/en
As elegant abstractions go, it's nice that at least one of those uses concurrent separation logic :-)
Last updated: Aug 19 2022 at 21:02 UTC