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 <strong>source version</strong> contains:</p>
<ul>
<li><code>README.md</code>/<code>README.pdf</code> — This file.</li>
<li><code>concrat-benchmarks/</code> — Concrat benchmarks (RQ 3) and execution scripts.
<ul>
<li><code>results-paper/</code> — Reference results used for Table 2.</li>
</ul>
</li>
<li><code>extracted-micro-benchmarks/</code> — Extracted micro-benchmarks (with their racy variations) and execution scripts (RQ 2).
<ul>
<li><code>results-paper/</code> — Reference results used for Table 4 (Finding 2).</li>
</ul>
</li>
<li><code>concrat-benchmarks-excluded/</code> — Excluded Concrat benchmarks (RQ 3).</li>
<li><code>sv-benchmarks/</code> — SV-COMP 2023 NoDataRace-Main category benchmarks.</li>
<li><code>joern/</code> — Joern scripts for Table 5 (RQ 3).
<ul>
<li><code>concrat-benchmarks-paper/</code> — Reference results for Concrat benchmarks used for Table 5 (Finding 3).</li>
<li><code>concrat-benchmarks-excluded-paper/</code> — Reference results for excluded Concrat benchmarks used for Table 5 (Finding 3).</li>
<li><code>sv-benchmarks-paper/</code> — Reference results for SV-COMP benchmarks used for Table 5 (Finding 3).</li>
<li><code>extracted-micro-benchmarks-paper/</code> — Reference results for extracted micro-benchmarks used for Table 14.</li>
</ul>
</li>
<li><code>sv-benchmarks.sh</code> — Script to download SV-COMP 2023 NoDataRace-Main category benchmarks.</li>
<li><code>tools/download.sh</code> — Script to download SV-COMP 2023 tools from their reproduction packages.</li>
<li><code>properties/no-data-race.prp</code> — Property file for executing SV-COMP tools.</li>
<li><code>tsan-races/</code> — Scripts to run ThreadSanitizer on Concrat benchmarks.
<ul>
<li><code>logs/</code> — Reference results used for Table 2 and Table 10.</li>
</ul>
</li>
</ul>
<p dir="auto">The <strong>virtual machine version</strong> contains all of the above in <code>/home/vagrant</code>, but also:</p>
<ul>
<li><code>concrat-benchmarks/</code>
<ul>
<li><code>results-test/</code> — Results from kick-the-tires (initially empty).</li>
<li><code>results/</code> — Full evaluation results (initially empty).</li>
<li><code>results-reduced/</code> — Reduced evaluation results (initially empty).</li>
</ul>
</li>
<li><code>extracted-micro-benchmarks/</code>
<ul>
<li><code>results-test/</code> — Results from kick-the-tires (initially empty).</li>
<li><code>results/</code> — Full evaluation results (initially empty) (Finding 2).</li>
<li><code>results-reduced/</code> — Reduced evaluation results (initially empty) (Finding 2).</li>
</ul>
</li>
<li><code>joern/</code>
<ul>
<li><code>concrat-benchmarks/</code> — Results for Concrat benchmarks (initially empty) (Finding 3).</li>
<li><code>concrat-benchmarks-excluded/</code> — Results for excluded Concrat benchmarks (initially empty) (Finding 3).</li>
<li><code>sv-benchmarks/</code> — Results for SV-COMP benchmarks (initially empty) (Finding 3).</li>
</ul>
</li>
<li><code>tools/</code> (subdirectories) — Downloaded SV-COMP 2023 tools from their reproduction packages.</li>
</ul>
<h1>Hardware Dependencies</h1>
<p dir="auto">The executable artifact is a <a href="https://www.virtualbox.org/">VirtualBox</a> virtual machine, because <a href="https://github.com/sosy-lab/benchexec">BenchExec</a> does not run in Docker. <strong>Full evaluation</strong> 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. <strong>Reduced evaluation</strong> requires:</p>
<ul>
<li>8 CPU cores,</li>
<li>16 GB RAM,</li>
<li>7 GB disk space,</li>
<li>~2 hours.</li>
</ul>
opencc-by-4.0Mar 2024View details →
