VMCAI '26 Artifact Description¶

Data Race Detection by Digest-Driven Abstract Interpretation¶

This is the artifact description for our VMCAI '26 paper "Data Race Detection by Digest-Driven Abstract Interpretation". The artifact is available on Zenodo.

The description here is provided for convenience and not maintained. The artifact contains Goblint at vmcai26 git tag.

Overview¶

This artifact contains the following components:

Evaluation Results  ::  The evaluation results, and overview tables (HTML)
                        generated from the raw data.
Source Code         ::  Source code for Goblint.
Verifier Binary     ::  Binary for Goblint.
Benchmark Programs  ::  Benchmarks used for evaluation (SV-COMP 2025).
BenchExec Tool      ::  The BenchExec benchmarking tool can be used
                        to replicate our results on these benchmarks.

The next section gives instructions on how to setup and quickly get an overview of the artifact. The subsequent sections then describe each of these components in detail. The final section gives information on how to reuse this artifact.

Remark on license:

• ~/analyzer/LICENSE: Is the MIT license governing the Goblint system as well as ancillary files such as this README
• The benchmarks from SV-COMP come with their individual licenses (all allowing for redistribution), where a LICENSE file is located in each folder of tasks or the license is otherwise directly recorded in the file header.

Getting Started¶

1. Setup¶

The artifact is a virtual machine (VM), as the BenchExec system used for reliable benchmarking cannot be installed in docker images. The machine is intended for an x86 machine, behavior on M1 chips is untested. Follow these steps to set it up:

• If you have not done so already, install VirtualBox. (https://www.virtualbox.org/wiki/Downloads)
• Download the artifact.
• Import the artifact via the VirtualBox UI (File > Import Appliance).

You can then start the VM from the VirtualBox UI. Login with user goblint and password goblint.

The machine is configured for QWERTY keyboards by default. If you use a different layout, you can click the small en button on the top right of the screen to select your keyboard layout.

2. Quick Test of the Benchmark Setup¶

To check Goblint is properly installed, run

cd ~/analyzer
make sanitytest

on a console in the VM. The run should take no longer than 2-4 minutes, the expected output is

Excellent: ignored check on tests/regression/03-practical/21-pfscan_combine_minimal.c:21 is now passing!
Excellent: ignored check on tests/regression/03-practical/21-pfscan_combine_minimal.c:29 is now passing!
No errors :)

You can also run the analysis for a subset of tasks and configurations by executing from the analyzer directory:

benchexec ../benchexec/minimal.xml -o minimal_results

• This runs three configurations on 62 tasks and should run for anywhere between 2 and 7 minutes (depending on your hardware).
• Then, run the command output at the end (will look like table-generator minimal_results/....).
• Navigate to minimal_results/results.*.table.html (where * will be the timestamp when the command was run) and open the HTML file.
• The table will show none succeeding (correct true) for 1 task, mutex-only for 14, and full for 41.

3. Running the Full Experiments¶

The full run of the experiments takes somewhere between 5 and 10 hours. If desired, this can be reduced by not evaluating all of the configurations, but only some of them (runtime is proportional to number of configurations). To disable configurations, you can remove them from ~/benchexec/races.xml, ideally after making a backup copy in case you decide to run some configuration after all.

To run the experiments, from ~/analyzer run

benchexec ../benchexec/races.xml

• Then, run the command output at the end (will look like table-generator results/....).

Evaluation Results¶

This evaluation supports all experimental claims made in Section 7. Please note that Table 1 is not based on our experiments, but cited from the report on SV-COMP 2025.

• All claims can be verified by opening the tables generated by the steps outlined in (3. Running the Full Experiments) which are located in ~/analyzer/results/results.*.table.html.
• If results were only generated for some configs in that step, the remaining results can be verified using the tables located in ~/analyzer/results-our-artifact-run/results.*.table.html where * is replaced with the date from our run inside the artifact.

These are HTML overviews as generated by the BenchExec benchmarking tool, and can be opened by a browser.

The table contains one configuration for every column of the table in Fig. 8 which are named by the activated digests.

• The row correct true indicates tasks where race-freedom was correctly established.
• The row correct false indicates tasks that were correctly identified as racy. (Goblint can't do this, always 0)
• The row incorrect true indicates false negatives, i.e., cases where race-freedom was claimed, even though the program is racy.
• The row incorrect false indicates false positives, i.e., cases where the definite presence of a race was claimed, but there is none. (Goblint never claims that a program must be racy, always 0)

How the claims are supported by this table:¶

Fig. 8

The numbers in Fig. 8 can be directly read off from this table.

None of the approaches produced any false negatives for the other 235 tasks in the benchmark set, which are racy.

Can be verified by checking that the incorrect true number for all configurations is zero.

Discussion on the success of (combinations of) digests

All numbers are from Fig. 8.

With these settings, the system ran out of memory for 4 tasks, 3 tasks timed out, and the analyzer crashed for 7 tasks.

The numbers in the VM are essentially the same as those on the server as Goblint is inherently single-threaded, and each of the cores of the server is not too powerful. Our run inside the VM matched exactly these numbers, however, some wiggle between machines is to be expected.

The numbers can be inspected by clicking on the Table tab on top of the document. Then, change the dropdown for one of the configs from Show all to:

• Select OUT OF MEMORY to see how often Goblint ran out of memory
• Select TIMEOUT to see how often Goblint ran into a timeout
• Select EXCEPTION(*) to see the cases where Goblint crashed.

Where execution terminated, it did so within at most 20s, where for all but 6 tasks the runtime was below 10s.

The same caveat as above applies here too. The numbers can be inspected by clicking on the Table tab on top of the document. Then, sort the runtime in a column by wall time by clicking on walltime twice. In our run inside the artifact, there in fact were no tasks which ran more than 9s, as each core in our machine for the VM is a bit more powerful than the cores in the server. Your run likely will not yield identical numbers, but they will be in the same ballpark.

The Table tab also gives access to detailed evaluation results for each file. For this to work, first unpack the *.logfiles.zip folder located in the results folder. Clicking on a status then shows the complete log for the benchmark run.

Note: If you are trying to view logs for individual runs through the HTML table (by clicking on the evaluation result true or false), you may encounter a warning because browsers block access to local files. Follow the instructions in the message to enable log viewing.

Source Code¶

The Goblint analyzer (https://goblint.in.tum.de) is developed by Technical University of Munich and University of Tartu with one of the authors recently having moved from TUM to National University of Singapore. The source code for Goblint at the time of evaluation can be found in this artifact in the ~/analyzer directory.

For an explanation of the general structure of the system, please refer to the online documentation of the system: https://goblint.readthedocs.io/en/latest/

The type of code particularly relevant for this paper is best illustrated along an example:

• A digest (lightweight thread ids in Fig. 4)
  • Consider the file ~/analyzer/src/analyses/threadFlag.ml which implements a slightly more powerful version of the lightweight thread ids in Fig. 4
  • A is defined in ~/analyzer/src/cdomains/threadFlagDomain.ml (Simple)
  • The functions threadenter and threadspawn take care of computing appropriate successors
  • ||^? is implemented in the function may_race
  • The b components concern interaction with other analysis and can be ignored for now
  • After checking whether the digest should be used to exclude races GobConfig.get_bool "ana.race.digests.threadflag", the predicate returns T (mapped to true here) if both accesses happen in multi-threaded mode, and at least one of the threads is not the unique main thread.

  let may_race (m1,b1) (m2,b2) =
    let use_threadflag = GobConfig.get_bool "ana.race.digests.threadflag" in
    let both_mt = Flag.is_multi m1 && Flag.is_multi m2 in
    let one_not_main = Flag.is_not_main m1 || Flag.is_not_main m2 in
    ((not use_threadflag) || (both_mt && one_not_main)) && b1 && b2

• The code in all the other digests is conceptually similar to the code provided here.
• Product of ||^?
• Consider ~/analyzer/src/analyses/mCPAccess.ml, here the product construction happens

  let may_race x y = binop_for_all (fun n (module S: Analyses.MCPA) x y ->
      S.may_race (Obj.obj x) (Obj.obj y)
    ) x y

• Here a fold over two lists of digests (each corresponding to one activated digest) is performed to get the effect of the definition in Section 5.3)

More recent versions of Goblint can be found at https://github.com/goblint.

Verifier Binaries¶

A pre-built binary of Goblint is available as ~/analyzer/goblint. See ~/analyzer/GOBLINT_README.md for information on how to run Goblint. To build Goblint from scratch, run make release.

Benchmark Programs¶

This artifact includes the benchmark programs on which we evaluated the verifiers. These benchmarks are taken from the publicly available sv-benchmarks set (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks) and correspond to the NoData-Race category of SV-COMP'25 (https://sv-comp.sosy-lab.org/2025/). The benchmarks are written in C and use POSIX threads (pthreads) to model concurrency.

Extending & Reusing This Artifact¶

• Adding benchmarks: You can easily add your own benchmarks programs written in C by following the SV-COMP format and adding a task and corresponding *.yml file, e.g., to the folder ~/sv-benchmarks/c/pthread. The easiest way to go about this is to copy the files bigshot_p.* and rename them to yourtest.*.
• The *.c file is provided for convenience only and contains the unpreprocessed program
• The *.i file contains the preprocessed (by GCC) program
• the *.yml file specifies:
  • The input file (change to yourtest.i)
  • The properties (of relevance here is only the no-data-race.prp property, change expected verdict according to your program)
  • The memory model (change if you preprocessed for a 64bit machine)

The framework automatically picks up new tasks placed in an existing directory.

• Adding your own analysis: The easiest way to do this is to start with a simple analysis such as the thread-flag analysis described above and then gradually modifying it to obtain the desired analysis.

Acknowledgment¶

This description is based, in part, on earlier artifact descriptions involving the Goblint system, in particular of our VMCAI'24, VMCAI'25 and ESOP'23 papers.