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
@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
The C++ plug-in we have to maintain is pretty trivial, since it's one of the hello world examples of libtooling. I mostly keep it in sync whenever I want to do an API bump. The OCaml part becomes manageable because it was written to support only the application we're interested in --- it's a restriction of the the whole API surface of libclang.
C++ code:
https://gitlab.com/umb-svl/c-to-json/-/blob/master/src/JSONNodeDumper.cpp
@AssertionError Very cool! Here's the link to the writeup of the stuff I did for master's work ("Parameterizing Algorithmic Skeletons for Correct and Efficient Performance-Portable Parallel Computations"), in case it's of interest: https://drive.google.com/file/d/0Byxgs15FUp2QRHJRVFVBLTZZc1U/view?usp=sharing&resourcekey=0-9gEBpYhSIuADsPecjSZO7w
Really cool MS project! I like the succinctness of the last example.
@AssertionError thanks! I'm still pretty pleased with how it came out
@elfprince13 @shriramk
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