Violation Witnesses for Concurrent C Programs (accompanying artifact)

Concurrency Violation Witnesses - reproduction artifact This repository reproduces the evaluation of the paper "Concurrency Violation Witnesses" (ICSE 2027). It contains the raw BenchExec results the paper's numbers are drawn from (results/), the scripts that turn them into LaTeX macros/tables/plots (data-analysis/), and everything needed to re-run the underlying verification/validation experiments from scratch. There are three things you can do here, roughly in order of effort: Inspect: regenerate the paper's tables and plots from the already-included results/ - no tools, benchmarks, or BenchExec run required. See §1. Re-check: re-run validation (or verification) yourself against the included witnesses/tasks to confirm the results, at a scale you choose (smoke test / meaningful subset / full paper run). See §2. Extend: add a new tool to the pipeline - see doc/developing.md. This can be used to easily test your tool against the new format specification. 1. Inspect: regenerate tables & plots from results/ make analyze-results This reads the per-tool and per-property latest results/*.xml.bz2 file already in this repository and produces PDFs and LaTeX macros in the latex directory. The violin plot for speedup is generated under latex/plots/speedup-distribution.pdf. To get a full picture of the data: cd latex && latexmk -pdf preview.tex Alternatively, a full verifier × validator cross-product HTML table can be generated: make generate-tables # -> results/tables/index.html 2. Reproduce: re-run the experiments Re-running produces new witnesses/results from scratch - either to smoke-test the pipeline, to re-check a representative subset, or to reproduce the full paper run. Requirements first: §3. 2.1 Clean slate Re-running writes into results/ and witnesses/; if you want a run that isn't mixed with the included data (recommended), clear them first: rm -rf results witnesses data-analysis/cache 2.2 One-time setup This step has already been done before packaging, but can be re-run: make download-all # benchexec + sv-benchmarks (SV-COMP26) + all tools (tools/) Builds CPAchecker (ant) and Theta (Gradle) from source, so it needs network access and takes a while (mostly Java compilation). 2.3 Pick a scale and a backend Every run needs one scale (which tasks, which limits) and one backend (where BenchExec executes them): Scale make command Tasks Limits (mem / timelimit / hardtimelimit) Smoke test make setup-test 6 hand-picked tasks (tasks/test.xml) 4 GB / 60 s / 90 s Meaningful subset make setup-subset ~2 CPU-hours, budgeted evenly across the 3 properties (tasks/subset.xml, from §1) 15 GB / 900 s / 960 s Full paper run make setup-benchmark full SV-COMP26 Concurrency.set (tasks/all.xml) - what produced results/ 15 GB / 900 s / 960 s Backend source command Use when Local, containerized source benchmark-utils/config.sh Default; one core group (-N 1) BenchCloud source benchmark-utils/vcloud_config.sh You have BenchCloud access; sets VCLOUD=1 Then, for any (scale, backend) pair: source benchmark-utils/config.sh # pick one of the three backends above make setup-test # pick one of the three scales above make verification-all # runs cpachecker, theta-hb, theta-interleaving make validation-all # runs every validator against every verifier's witnesses make analyze-results # regenerate latex/ as in §1 make generate-tables # regenerate results/tables as in §1 3. Requirements Ubuntu packages Tested on Ubuntu 24.04. Recommended install: sudo apt-get update sudo apt-get install -y \ git make unzip zip \ ant openjdk-21-jdk \ gcc gcc-multilib libc6-dev \ libgomp1 libmpfr6 \ python3 python3-pip python3-venv Rationale (from each tool's declared fm-tools entry, plus what building them from source additionally needs): Package(s) Needed by git, unzip, zip, make cloning/building/packaging every tool (make download-all, make package) ant building CPAchecker (tools/cpachecker) openjdk-21-jdk building and running CPAchecker and Theta (fm-tools lists openjdk-21-jre-headless for running; the JDK is additionally needed to build with ant/./gradlew) gcc, gcc-multilib, libc6-dev CPAchecker's gcc-multilib/libc6-dev requirement; gcc for ConcurrentWitness2Test's generated test harnesses libgomp1, libmpfr6 running Theta python3, python3-pip, python3-venv ConcurrentWitness2Test, the witnesslint validator, data-analysis/, and BenchExec itself BenchExec and cgroups BenchExec (cloned by make benchexec) needs access to Linux cgroups to enforce CPU/memory/time limits reliably; this is a one-time system setup, independent of using the cloned checkout directly (as this artifact's Makefile does) rather than the apt package. Easiest path on Ubuntu - installs the SoSy-Lab benchexec package, which also configures cgroup permissions: sudo add-apt-repository ppa:sosy-lab/benchmarking sudo apt-get update sudo apt-get install -y benchexec sudo adduser "$USER" benchexec # then log out/in again For other distributions, cgroups v1/v2, or systemd-less setups, follow BenchExec's own guide: Setting up Cgroups (part of doc/INSTALL.md). Python packages python3 -m venv .venv && source .venv/bin/activate pip install -r requirements.txt requirements.txt covers BenchExec, data-analysis/ (pandas/matplotlib/seaborn/scipy), and the witnesslint validator (jsonschema/lxml/pycparser/libclang); it's a superset of data-analysis/requirements.txt, which alone suffices for §1.