The artifacts and data for the paper "DD4AV: Detecting Atomicity Violations in Interrupt-Driven Programs with Guided Concolic Execution and Filtering" (OOPSLA 2025)
<p dir="ltr">DD4AV is a dynamically controlled scheduling testing tool that explores possible interleavings of interrupt-driven programs to detect atomicity violations. This repository provides the tool and evaluation subjects for the paper "DD4AV: Detecting Atomicity Violations...
Saved in:
| Main Author: | |
|---|---|
| Published: |
2025
|
| Subjects: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | <p dir="ltr">DD4AV is a dynamically controlled scheduling testing tool that explores possible interleavings of interrupt-driven programs to detect atomicity violations. This repository provides the tool and evaluation subjects for the paper "DD4AV: Detecting Atomicity Violations in Interrupt-Driven Programs with Guided Concolic Execution and Filtering<br>."</p><h2><b>Directory Structure</b></h2><p dir="ltr">The repository mainly contains three folders: <code><strong>tool</strong></code>, <code><strong>test</strong></code>, and <code><strong>realworld_AV</strong></code><b>.</b></p><ul><li><code><strong>tool</strong></code>: The root directory containing DD4AV's tools and scripts.</li><li><ul><li><code><strong>DBDS</strong></code>: The code implements our proposed dynamic scheduling execution method, which systematically explores task interleaving for atomicity violation detection, enhanced by an effective prefix-directed strategy.</li><li><code><strong>staticAnalysis</strong></code>: The scripts for static analysis are designed to identify key operations to be scheduled during testing.</li><li><code><strong>SVF</strong></code>: The third-party library project SVF provides interprocedural dependence analysis for LLVM-based languages.</li><li><code><strong>wllvm</strong></code>: The third-party library project WLLVM provides tools for building whole-program LLVM bitcode files from unmodified C or C++ source packages.</li></ul></li><li><code><strong>test</strong></code>: A few simple examples that are easy to understand and can be used to verify the installation.</li><li><code><strong>realworld_AV</strong></code>: 18 real-world embedded interrupt-driven programs, all written in C, including control software, firmware, and device drivers.</li></ul><h2><b>Tool</b></h2><h3><b>Requirements</b></h3><p dir="ltr">To install the tool from source code on your host system, please ensure that your environment meets the following requirements:</p><p dir="ltr"><b>Operating System:</b> Ubuntu 18.04 LTS or higher (requires kernel version 4.x or above due to the scheduling policy).</p><h3><b>Installation</b></h3><h4><b>install Dependencies</b></h4><p dir="ltr">Our artifact depends on several packages, please run the following command to install all necessary dependencies.</p><pre><pre>sudo apt-get install -y wget git build-essential python3 python python-pip python3-pip tmux cmake libtool libtool-bin automake autoconf autotools-dev m4 autopoint libboost-dev help2man gnulib bison flex texinfo zlib1g-dev libexpat1-dev libfreetype6 libfreetype6-dev libbz2-dev liblzo2-dev libtinfo-dev libssl-dev pkg-config libswscale-dev libarchive-dev liblzma-dev liblz4-dev doxygen libncurses5 vim intltool gcc-multilib sudo --fix-missing<br></pre></pre><pre><pre>pip install numpy && pip3 install numpy && pip3 install sysv_ipc<br></pre></pre><h4><b>Download the Code</b></h4><p dir="ltr">Download <b>DD4AV</b> from the Figshare website to your local machine and navigate to the project directory:</p><pre><pre>cd DD4AV<br></pre></pre><h4><b>Configure Environment and Install the Tool</b></h4><p dir="ltr">For convenience, we provide shell scripts to automate the installation process. Run the following commands to configure the environment and install the necessary tools:</p><pre><p dir="ltr"><i># Install LLVM and clang</i><br>tool/install_llvm.sh<br><br><i># Set up the environment</i><br>source tool/init_env.sh<br><br><i># Install SVF</i><br>$ROOT_DIR/tool/install_SVF.sh<br><br><i># Install the static analysis tool</i><br>$ROOT_DIR/tool/install_staticAnalysis.sh<br><br><i># Install wllvm</i><br>sudo pip install -e $ROOT_DIR/tool/wllvm/<br></p></pre><h4><b>Note</b></h4><p dir="ltr">Each time you open a new terminal, you will need to set the environment variables to ensure proper execution of the tool:</p><pre><pre><i># set up environment</i><br>source tool/init_env.sh</pre></pre><h2><b>Quick Start for Simple Test</b></h2><p dir="ltr">Before using DD4AV, we recommend starting with the simple examples provided to ensure that the tool functions correctly. Below, we use the <code><strong>simple_test</strong></code> example in the <code><strong>test</strong></code> folder to demonstrate how to use DD4AV.</p><h3><b>Steps:</b></h3><h4><b>1) Navigate to the working directory:</b><br><code>cd $ROOT_DIR/test/simple_test</code></h4><p><br></p><p dir="ltr"><b>2) Build the program using the provided scripts:</b><br><code>./clean.sh && ./build.sh</code><br><br><b>3) Perform systematic controlled testing with periodical scheduling:</b><br><code>$ROOT_DIR/tool/DBDS/run.py -y -d 4 ./simple_test</code><br></p><p><br></p><p dir="ltr">When the number of tasks is <b></b>, the maximum preemption count is set to <b>2−2 </b>(specified by the <b>-d</b> parameter), with the default period length set to 5 times the execution time of the current task.<br></p><p><br></p><p dir="ltr"><b>4) Expected output:</b></p><p dir="ltr">If <b>DD4AV </b>is functioning correctly, you should see an output similar to the following, indicating that DD4AV detected 1 atomicity violation in the program:</p><pre><pre> Start Testing!<br> There is no schedule to satisfy under the constraint: [2, 1, 1] , 2<br> Targeting bugs that bug depth = 1 . Iterate for 2 periods<br> Targeting bugs that bug depth = 2 . Iterate for 3 periods<br> test 0001: [[0, 0], [1], [2]]<br> test 0002: [[0, 0], [2], [1]]<br> test 0003: [[1], [0, 0], [2]]<br> test 0004: [[1], [2], [0, 0]]<br> test 0005: [[2], [0, 0], [1]]<br> test 0006: [[2], [1], [0, 0]]<br> Targeting bugs that bug depth = 3 . Iterate for 4 periods<br> test 0007: [[0], [1], [0], [2]]<br> test 0008: [[0], [1], [2], [0]]<br> test 0009: [[0], [2], [0], [1]]<br> test 0010: [[0], [2], [1], [0]]<br> test 0011: [[1], [0], [2], [0]]<br> test 0012: [[2], [0], [1], [0]]<br> There is no schedule to satisfy under the constraint in stage 2: [2, 1, 1] , 4<br> There is no schedule to satisfy under the constraint in stage 2: [2, 1, 1] , 4<br> There is no schedule to satisfy under the constraint: [2, 1, 1] , 5<br> Targeting bugs that bug depth = 4 . Iterate for 5 periods<br> test 0013 for prefix [[0], [1]]: [[0], [1], [2, 2], [1], [0]]<br> There is no schedule to satisfy under the constraint in stage 2: [2, 1, 1] , 5<br> End Testing!<br> <br> <br> --------------------------------------------------<br> (1) (('W', 13), ('R', 22), ('W', 16))<br> Total Round: 13<br> First_buggy_round:7 Total_buggy_rounds:4 Total_rounds:13<br> bugDepth: 4<br> DynamicExecTime:00.18557<br><br></pre></pre><p dir="ltr">If the above steps are executed successfully, your installation is complete. You can proceed by trying other examples in the <code><strong>test</strong></code> folder. To reproduce our experimental results, please refer to the detailed documentation in <code><strong>README.md</strong></code></p><p><br></p> |
|---|