Faial checks for absence of #dataraces in #CUDA kernels. New since our #CAV21 version is:
- a new frontend all written in OCaml (no more Python+Rust) we also have a new UI (sshot below)
- a new backend (invoke #Z3 as a library, as a process)
- support for partial inputs (eg, missing includes)
My intent to have a bit of a codebase written in Python was to attract students. Turns out interested students are excited to learn #OCaml.
@AssertionError how much of C++ does this support? I had a miserable time doing CUDA tooling for an academic project (@shriramk likely remembers 😅) because of having to deal with parsing all the bizarre C++ corner cases.
We use libclang to parse. Luckily most kernels we've seen use a small number of C++ features. We do support things like templated kernels and we have limited support for classes --- insofar as we only support arrays of opaque data.
@AssertionError @shriramk I did a clang plugin but there are an absurd number of weird corner cases even in the AST representation. Ignoring classes probably helps with a lot
Ah, exactly. Libclang/C++ overwhelmed me very quickly. Instead we just serialize the ast into JSON and then handle everything in OCaml here:
https://gitlab.com/umb-svl/faial/-/blob/main/inference/lib/c_lang.ml
@shriramk @AssertionError yeah I serialized to S-Expressions and used Racket macros for everything and the two biggest lifts were making the AST serialization comprehensive (using Clang’s existing facilities for doing so!!) and then writing my transformed Racket syntax objects back out as C++ code on the other side
@shriramk @AssertionError all the actually interesting PL stuff in the middle was trivial by comparison
