Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

WHOOP data race benchmarks #25

Open
sim642 opened this issue Apr 11, 2022 · 0 comments
Open

WHOOP data race benchmarks #25

sim642 opened this issue Apr 11, 2022 · 0 comments
Labels
new benchmark New benchmark to analyze

Comments

@sim642
Copy link
Member

sim642 commented Apr 11, 2022

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?).

@sim642 sim642 added the new benchmark New benchmark to analyze label Apr 11, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
new benchmark New benchmark to analyze
Projects
None yet
Development

No branches or pull requests

1 participant