vlj (Aug 05 2020 at 20:34): vlj (Aug 05 2020 at 20:34):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.
Karl Palmskog (Aug 05 2020 at 20:54):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
Paolo Giarrusso (Aug 06 2020 at 20:26):As elegant abstractions go, it's nice that at least one of those uses concurrent separation logic :-)
Last updated: Dec 06 2023 at 15:01 UTC