Sound Static Data Race Verification for C: Is the Race Lost?

<p>This artifact contains the benchmarks, tools and scripts for reproduction, along with our reference results used for the paper.</p> <h1>Contents</h1> <p dir="auto">The reproduction package contains materials for reproducing Tables 2, 4, 5, 10, and 14 from the paper. These tables provide the data supporting research questions 2 and 3, as well as additional evaluation results.</p> <p dir="auto">We provide two versions of the artifact:</p> <ol> <li>The source version includes benchmarks, scripts and reference results such that they can easily be accessed and reused outside of the virtual machine.</li> <li>The virtual machine version additionally includes tools and their dependencies such that the results can be reproduced by execution.</li> </ol> <p dir="auto">The&nbsp;<strong>source version</strong>&nbsp;contains:</p> <ul> <li><code>README.md</code>/<code>README.pdf</code>&nbsp;&mdash; This file.</li> <li><code>concrat-benchmarks/</code>&nbsp;&mdash; Concrat benchmarks (RQ 3) and execution scripts. <ul> <li><code>results-paper/</code>&nbsp;&mdash; Reference results used for Table 2.</li> </ul> </li> <li><code>extracted-micro-benchmarks/</code>&nbsp;&mdash; Extracted micro-benchmarks (with their racy variations) and execution scripts (RQ 2). <ul> <li><code>results-paper/</code>&nbsp;&mdash; Reference results used for Table 4 (Finding 2).</li> </ul> </li> <li><code>concrat-benchmarks-excluded/</code>&nbsp;&mdash; Excluded Concrat benchmarks (RQ 3).</li> <li><code>sv-benchmarks/</code>&nbsp;&mdash; SV-COMP 2023 NoDataRace-Main category benchmarks.</li> <li><code>joern/</code>&nbsp;&mdash; Joern scripts for Table 5 (RQ 3). <ul> <li><code>concrat-benchmarks-paper/</code>&nbsp;&mdash; Reference results for Concrat benchmarks used for Table 5 (Finding 3).</li> <li><code>concrat-benchmarks-excluded-paper/</code>&nbsp;&mdash; Reference results for excluded Concrat benchmarks used for Table 5 (Finding 3).</li> <li><code>sv-benchmarks-paper/</code>&nbsp;&mdash; Reference results for SV-COMP benchmarks used for Table 5 (Finding 3).</li> <li><code>extracted-micro-benchmarks-paper/</code>&nbsp;&mdash; Reference results for extracted micro-benchmarks used for Table 14.</li> </ul> </li> <li><code>sv-benchmarks.sh</code>&nbsp;&mdash; Script to download SV-COMP 2023 NoDataRace-Main category benchmarks.</li> <li><code>tools/download.sh</code>&nbsp;&mdash; Script to download SV-COMP 2023 tools from their reproduction packages.</li> <li><code>properties/no-data-race.prp</code>&nbsp;&mdash; Property file for executing SV-COMP tools.</li> <li><code>tsan-races/</code>&nbsp;&mdash; Scripts to run ThreadSanitizer on Concrat benchmarks. <ul> <li><code>logs/</code>&nbsp;&mdash; Reference results used for Table 2 and Table 10.</li> </ul> </li> </ul> <p dir="auto">The&nbsp;<strong>virtual machine version</strong>&nbsp;contains all of the above in&nbsp;<code>/home/vagrant</code>, but also:</p> <ul> <li><code>concrat-benchmarks/</code> <ul> <li><code>results-test/</code>&nbsp;&mdash; Results from kick-the-tires (initially empty).</li> <li><code>results/</code>&nbsp;&mdash; Full evaluation results (initially empty).</li> <li><code>results-reduced/</code>&nbsp;&mdash; Reduced evaluation results (initially empty).</li> </ul> </li> <li><code>extracted-micro-benchmarks/</code> <ul> <li><code>results-test/</code>&nbsp;&mdash; Results from kick-the-tires (initially empty).</li> <li><code>results/</code>&nbsp;&mdash; Full evaluation results (initially empty) (Finding 2).</li> <li><code>results-reduced/</code>&nbsp;&mdash; Reduced evaluation results (initially empty) (Finding 2).</li> </ul> </li> <li><code>joern/</code> <ul> <li><code>concrat-benchmarks/</code>&nbsp;&mdash; Results for Concrat benchmarks (initially empty) (Finding 3).</li> <li><code>concrat-benchmarks-excluded/</code>&nbsp;&mdash; Results for excluded Concrat benchmarks (initially empty) (Finding 3).</li> <li><code>sv-benchmarks/</code>&nbsp;&mdash; Results for SV-COMP benchmarks (initially empty) (Finding 3).</li> </ul> </li> <li><code>tools/</code>&nbsp;(subdirectories) &mdash; Downloaded SV-COMP 2023 tools from their reproduction packages.</li> </ul> <h1>Hardware Dependencies</h1> <p dir="auto">The executable artifact is a&nbsp;<a href="https://www.virtualbox.org/">VirtualBox</a>&nbsp;virtual machine, because&nbsp;<a href="https://github.com/sosy-lab/benchexec">BenchExec</a>&nbsp;does not run in Docker.&nbsp;<strong>Full evaluation</strong>&nbsp;requires:</p> <ul> <li>8 CPU cores,</li> <li>26 GB RAM,</li> <li>7 GB disk space,</li> <li>~2 days and 15 hours.</li> </ul> <p dir="auto">Considering the significant runtime, we also provide a reduced evaluation.&nbsp;<strong>Reduced evaluation</strong>&nbsp;requires:</p> <ul> <li>8 CPU cores,</li> <li>16 GB RAM,</li> <li>7 GB disk space,</li> <li>~2 hours.</li> </ul>