You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Although WHOOP itself analyzes Boogie code, it seems that the Chauffeur component of their pipeline does some ad hoc rewriting of C code itself.
Moreover, c/pthread-driver-races in sv-benchmarks originate from WHOOP, although data races are checked by a value assertion. Unfortunately, sv-benchmarks only contains 2 out of 16 drivers mentioned in the paper and they're the smallest ones.
Nevertheless, the sv-benchmarks show a relatively thin main function harness to instantiate and invoke the driver hooks. This isn't mentioned anywhere, but the sv-benchmarks versions seem to have been generated using this fork: https://github.com/MontyCarter/chauffeur. So it might be good to get the other 14 drivers into pure C programs as well.
I tried to compile that in a LLVM 3.5 Docker container but got linking errors for a number of LLVM/Clang functions, so I couldn't get it to run. Maybe someone more familiar with LLVM knows how to fix the issue (@michael-schwarz?).
The text was updated successfully, but these errors were encountered:
WHOOP is the tool presented by the article Fast and precise symbolic analysis of concurrency bugs in device drivers.
Although WHOOP itself analyzes Boogie code, it seems that the Chauffeur component of their pipeline does some ad hoc rewriting of C code itself.
Moreover,
c/pthread-driver-races
in sv-benchmarks originate from WHOOP, although data races are checked by a value assertion. Unfortunately, sv-benchmarks only contains 2 out of 16 drivers mentioned in the paper and they're the smallest ones.Nevertheless, the sv-benchmarks show a relatively thin
main
function harness to instantiate and invoke the driver hooks. This isn't mentioned anywhere, but the sv-benchmarks versions seem to have been generated using this fork: https://github.com/MontyCarter/chauffeur. So it might be good to get the other 14 drivers into pure C programs as well.I tried to compile that in a LLVM 3.5 Docker container but got linking errors for a number of LLVM/Clang functions, so I couldn't get it to run. Maybe someone more familiar with LLVM knows how to fix the issue (@michael-schwarz?).
The text was updated successfully, but these errors were encountered: