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

Add regenerated Klever Linux 5.5 concurrency safety benchmarks #27

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Apr 14, 2022

This was an attempt to regenerate the benchmarks from #3 using a newer version of Klever etc. Seems that the Frama-C issue has been fixed: #3 (comment). Moreover, the generated benchmarks use a Linux 5.5 build base instead of 4.2.6 or 4.18.

Requires goblint/analyzer#688 to analyze with Goblint.

TODO

  • Is Goblint sound on them?
  • Is the amount of dead code expected from the unused model?
  • Are there even threads, races and locks to analyze?

@sim642 sim642 added the new benchmark New benchmark to analyze label Apr 14, 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

Successfully merging this pull request may close these issues.

CPALockator's Linux device driver data race detection benchmarks
1 participant