Reproduction Package for SEFM 2026 Submission `Revisiting Sequentialization of Concurrent C Programs'

Le résumé fourni par la source

Reproduction Package for the Paper “Revisiting Sequentialization of Concurrent C Programs” Abstract This artifact is a reproduction package for the paper “Revisiting Sequentialization of Concurrent C Programs” submitted for SEFM 2026 (https://sefm-conference.github.io/2026/). This paper presents CPAmpor, a highly configurable sequentialization tool for concurrent C programs implemented in the actively maintained tool CPAchecker. CPAmpor is compatible with many sequential backends and provides novel encodings of partial order reduction strategies directly within the sequentialized program. This artifact consists of all executables, input data and results required to reproduce the experiments. In particular, it also contains the original results of the paper and a way to generate the HTML and CSV files used for the papers tables and plots. A full reproduction of the experiments requires roughly 200 days of CPU time. However, the benchmarks are configurable and parallelizable to reduce the amount of elapsed time. The experiments for each RQ can be run in isolation, and we provide shorter configurations for each RQ that run a representative subset of the tasks in less than 1 hour each. To test that everything is working as intended, we provide a Smoketest that takes roughly 20 minutes. Claimed Badges We claim the following badges in this artifact: Available: The artifact is available on Zenodo Functional and Reusable: There are explanations in this README to run the experiments and add a new tool to the experimental setup. 0. Table of Contents This README contains the following sections to help users reproduce the experiments: TL;DR: A quick guide to reproduce the experiments and analyze the data. Directory Structure: An overview of directories (and their purpose) that are part of this artifact. Requirements: Describes the software + hardware requirements for the artifact to work properly. Running Experiments Describes how to execute, configure and parallelize the experiments, including a quick Smoketest. Interpreting Results: Describes where the experiment results can be found and how to analyze them. Information for Reuse: Documentation on how to use the artifact for purposes other than reproduction. Used Versions: An overview of all benchmark and tool versions in this artifact. Known Issues: Describes known issues when executing the artifact and how to mitigate them. 1. TL;DR Note: All commands in this README should be executed from the root directory, i.e., the directory that contains this README. Start up the CAV 2026 VM (available at https://zenodo.org/records/19184839) using, e.g., VirtualBox. Download and extract the artifacts ZIP file into the VM, ideally not in a shared folder but in a VM local folder. Run the following to setup the VM correctly. The script will ask once for the admin password which is cav for the CAV 2026 VM. The VM will reboot after everything is finished. bash setup_vm.sh # takes 3 minutes After rebooting, run one or more of the following commands to run the experiments and obtain the results. All times refer to CPU time. make run_artifact_smoketest # takes 20 minutes make run_artifact_rq1_short # takes 1 hour make run_artifact_rq2_short # takes 1 hour make run_artifact_rq3_short # takes 1 hour make run_artifact_rq4_short # takes 1 hour make run_artifact_full # takes 200 days make run_artifact_rq1 # takes 3 days make run_artifact_rq2 # takes 45 days make run_artifact_rq3 # takes 75 days make run_artifact_rq4 # takes 80 days The file doc/smoketest-output.txt contains the expected output on the terminal when running the Smoketest. The results of the experiments can be obtained in the results dir (or results-smoketest for the Smoketest or results-short for the short experiments). This directory will be generated when running the corresponding experiments and is not provided in the artifact. Each RQ has its own subdirectory results/rq{1, 2, 3, 4}/. The subdirectories results/rq{1, 2, 3, 4}/*.results.table/ contain summary statistics for the experiments in HTML files that were used for the tables in our paper. The numbers reported in these HTML files should match the numbers of the HTML files in results-paper/rq{1, 2, 3, 4}/. Note that this only holds for the full experiments, since the Smoketest and the short experiments execute a subset of the programs only. rq{1, 3, 4} contain subdirectories named plot with PDF plot files that should match the figures in our paper. 2. Directory Structure This artifact contains the following items: README.md: This file. benchmarks: Contains (i) BenchExec, (ii) the subset of SV-Benchmarks used in the evaluation, and (iii) the XML files define benchmarks (used tool, timelimit, used tasks, etc.) that can be given to BenchExec for execution. The .set files list the programs to sequentialize: sv-benchmarks/c/Concurrency.set for the full experiments, sv-benchmarks-short/Concurrency-rq{1, 2, 3, 4}-short.set for the short experiments, and sv-benchmarks-smoketest/Concurrency-smoketest.set for the Smoketest. doc: Contains documentation on expected output on the terminal. results (Will be generated when running the full experiments): After running the full experiments, the results dir appears and contains summary HTML tables and CSV files (both produced by BenchExec) and logfiles (produced by the respective tools). results-short (Will be generated when running the short experiments): Same as results, but when executing the short instead of the full experiments. results-smoketest (Will be generated when running the smoketest): Same as results, but when executing the Smoketest instead of the full experiments. results-paper: Contains the original result files (HTML, CSV, logfiles) from our evaluation. The numbers match exactly the ones reported in our paper and will not be changed by any of the commands presented in this README. scripts/python: Contains several Python scripts that automate the artifact, such as task extraction or wrapper scripts for CPAmpor and Lazy-CSeq. sequentializations: After running CPAmpor and Lazy-CSeq, this directory contains the sequentialized C programs and the YML task definitions with expected verdicts for properties (data races, reachability, memory safety, overflows). tools: Contains (i) CPAmpor and Lazy-CSeq that create the sequentialized programs and (ii) the backends 2ls, Bubaak, CBMC, CPAchecker, Mopsa, Symbiotic, and Ultimate Kojak that analyze the programs produced by CPAmpor and Lazy-CSeq. Note that there are several subdirectories suffixed with -modified; these contain small adjustments to files in some of the used tools. Each of these directories contains a separate README explaining what changes were made and why they were made. The changes are all necessary for the artifact to work properly. 3. Requirements All tools in this artifact were compiled for a x86 architecture, so it will in general not be possible to run them on an ARM chip. The unpacked artifact needs 2GB of disk space, and for the VM image we recommend at least 16 GB of additional disk space. The artifact requires a VM with at least 4 cores and 20 GB of memory to run it properly. The Smoketest can be executed with 2 cores and 8 GB of memory. We tested this artifact with the VM used for artifacts submitted to the CAV 2026 conference (https://zenodo.org/records/19184839). The artifact was tested with version VirtualBox VM 7.2.12 r174389 linux.amd64. Any other VM will likely also work with this artifact if set up correctly, but the CAV 2026 VM has several requirements pre-installed already. For all further requirements, please take a look at setup_vm.sh, which installs all required dependencies into the VM and sets up the environment correctly. 4. Experiments 4.1. Setup All data and tools are contained inside the artifacts ZIP file already. Only the CAV 2026 VM and some small dependencies and system changes are required for the artifact to run. From the root folder of the extracted files, run the followi

Ce résumé expose les affirmations des auteurs. BNTIC ne l’interprète pas comme une validation indépendante des résultats.