Original benchmarks from ldv-commits-races

[vesalvojdani]

Since we can't lift the benchmarks directly (#3), we could try to extract the race commits from the original sources. Here are the relevant commits:

• [x] https://github.com/torvalds/linux/commit/0e2400e Seems to work, but takes more than 2 hours to complete. It did terminate over night; many warnings though.
• [x] https://github.com/torvalds/linux/commit/0f90c9c Runs quickly. No difference in race output, but with the sv-comp22 setup, goblint quite impressively finds that there is a single data race and it's precisely the relevant variable. The problem is a potential division by zero due to this race, and the fix does not eliminate the race, but instead adds a non-zeroness check when the variable is privatized. Might be an interesting use case for our privatization, but it's all very heap-based.
• [x] https://github.com/torvalds/linux/commit/10ef175. This already states that the fix avoids adding locks. I wanted to see if the mhp analysis does something interesting here, but seems to actually increase the number of "vulnerable" locations compare to the thread analysis. This is too messy; may look at it again at some point.
• [ ] https://github.com/torvalds/linux/commit/1a81087
• [ ] https://github.com/torvalds/linux/commit/1adc906
• [ ] https://github.com/torvalds/linux/commit/2d4cf3d
• [x] https://github.com/torvalds/linux/commit/34596a8
• [ ] https://github.com/torvalds/linux/commit/3627c07
• [ ] https://github.com/torvalds/linux/commit/3b91850
• [ ] https://github.com/torvalds/linux/commit/4036523
• [ ] https://github.com/torvalds/linux/commit/6b1246d
• [ ] https://github.com/torvalds/linux/commit/7357404
• [x] https://github.com/torvalds/linux/commit/8a2629a. Goblint says function definition missing for down_interruptible, but this is far too complicated anyway. Wait queues are replaced by semaphores and it's the kind of producer-consumer type semaphore where one function upon accepting a connection decreases and another function making the requests increases.
• [ ] https://github.com/torvalds/linux/commit/aea9dd5
• [x] https://github.com/torvalds/linux/commit/c99bd4f
• [x] https://github.com/torvalds/linux/commit/d5c55fa
• [x] https://github.com/torvalds/linux/commit/f0c626f
• [x] https://github.com/torvalds/linux/commit/f1a8a3f

(The following are not publicly available: https://github.com/torvalds/linux/commit/2e4ce49, https://github.com/torvalds/linux/commit/883f30e)

Preparing the include files

Most of the include files remain the same, but some are generated with the commands make defconfig && make prepare, and one has to make some tweaks for this to work with newer versions of gcc:

• disable -pie.
• Apply our usual hack of copying compiler-gcc4.h to whatever version is currently used.
• Disable use of asm goto keyword.
• All such tweaks (except the copying of the compiler header), i.e., the output of git diff w.r.t. the original kernel sources should be added to each benchmark (adaptations.patch)

At the moment, I have been using goblint -v to get the preprocessing command and then ran that with -M to get the list of included files and then copied all those files here. Maybe there is a better way than to just upload them all here. The only files different from the kernel repo are in the generated subdirectories.

[sim642]

At the moment, I have been using goblint -v to get the preprocessing command and then ran that with -M to get the list of included files and then copied all those files here.

The json-messages output should also contain a list of all the files involved. That might be easier to automate as well if desired.