Stream: Miscellaneous

Topic: Gpgpu application of coq


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: Aug 19 2022 at 21:02 UTC