add readme and post-processing scripts

tools/verifyio/README.md

@@ -1,36 +1,66 @@
+# VerifyIO
+VerifyIO collects execution traces, detects data conflicts, and verifies proper synchronization against specified consistency models. 
+The workflow for VerifyIO can generally be divided into three independent steps (Step 1 - Step 3). This process requires [Recorder](https://github.com/uiuc-hpc/Recorder/tree/dev), [VerifyIO](https://github.com/uiuc-hpc/Recorder/tree/dev/tools/verifyio), and the corresponding traces.
 
-### Verify if I/O operations are properly synchronized uder specific semantics
-------------------------------
+Make sure `$RECORDER_INSTALL_PATH` is the install location of Recorder. 
 
+Additional [scripts](https://github.com/uiuc-hpc/Recorder/blob/dev/tools/verifyio/scripts/) are available for exporting results as CSV files and visualizing them (Step 4 and Step 5). The verification can be performed in a batched manner for multiple traces. For this, alternative steps can be followed to handle multiple traces more efficiently.
 
+## Step 1:  Run the application with Recorder to generate traces.
 
-Make sure `$RECORDER_INSTALL_PATH` is the install location of Recorder.
+```bash
+mpirun -np N -env LD_PRELOAD $RECORDER_INSTALL_PATH/lib/librecorder.so ./test_mpi
 
-Dependencies: `recorder-viz` and `networkx`. Both can be installed using pip.
+# On HPC systems, you may need to use srun or
+# other job schedulers to replace mpirun, e.g.,
+srun -n4 -N1 --overlap --export=ALL,LD_PRELOAD=$RECORDER_INSTALL_PATH/lib/librecorder.so ./test_mpi
+```
+For detailed information on the Recorder and guidance on its usage, please refer to: https://recorder.readthedocs.io/latest/overview.html
 
-Steps:
-1. Run program with Recorder to generate traces.
-2. Run the conflict detector to report **potential** conflicting I/O accesses.
-   Those acesses are only potentially conflicting as here we do not take happens-before order into consideration yet.
+## Step 2: Conflict Detection
+Run the conflict detector to report **potential** conflicting I/O accesses. Those acesses are only potentially conflicting as here we do not take happens-before order into consideration yet.
+To detect conflicts, use the `conflict-detector` tool from Recorder:
 
-   `$RECORDER_INSTALL_PATH/bin/conflict_detector /path/to/traces`
-
-   This command will write all potential conflicts found to the file `/path/to/traces/conflicts.txt`
-
-3. Finally run the verification code, which checks if those potential conflicting operations are properly synchronzied.
+```bash
+$RECORDER_INSTALL_PATH/bin/conflict-detector /path/to/trace
+```
+This command will write all potential conflicts found to the file `/path/to/traces/conflicts.txt`
 
-   The `semantics` option needs to match the one provided by the underlying file system. For example, if the traces were collected on UnifyFS, set it to "commit".
-
-   ```python
-   python ./verifyio.py -h  # print out usage
-
-   #Example:
-   python ./verifyio.py /path/to/traces --semantics=mpi
-   ```
-
-
-
-#### Note on the third step:
+Alternatively, the [`auto_detect.sh`](https://github.com/uiuc-hpc/Recorder/blob/dev/tools/verifyio/scripts/auto_detect.sh)  script can be used to process multiple traces and detect conflicts. The script requires the path to the directory containing the traces as an argument. Please adjust the configuartion for resource manager accordingly. 
+
+```bash
+./auto_detect.sh /path/to/target/traces
+```
+
+## Step 3: Semantic Verification
+The next step is to run the semantic verification using [`verifyio.py`](https://github.com/uiuc-hpc/Recorder/tree/dev/tools/verifyio). It checks if those potential conflicting operations are properly synchronzied. By default, MPI-IO semantics and the vector clock algorithm are used for verification.
+
+### Dependencies for step 3:
+
+Ensure the following dependencies are installed:
+
+#### Python Libraries
+- **recorder-viz**:  For visualizing recorder traces. `pip install recorder-viz`
+- **networkx**: For creating, analyzing, and manipulating complex networks and graphs. Install using `pip install networkx`.
+
+```bash
+python /path/to/verifyio.py /path/to/trace
+```
+Available arguments:
+* --semantics: Specifies the I/O semantics to verify. Choices are: POSIX, MPI-IO (default), Commit, Session, Custom
+* --algorithm: Specifies the algorithm for verification. Choices are: 1: Graph reachability 2: Transitive closure 3: Vector clock (default) 4: On-the-fly MPI check
+* --semantic_string: A custom semantic string for verification. Default is: "c1:+1[MPI_File_close, MPI_File_sync] & c2:-1[MPI_File_open, MPI_File_sync]""
+* --show_details: Displays details of the conflicts.
+* --show_summary: Displays a summary of the conflicts.
+* --show_full_chain: Displays the full call chain of the conflicts.
+
+Alternatively, the [`auto_verify.sh`](https://github.com/uiuc-hpc/Recorder/blob/dev/tools/verifyio/scripts/auto_verify.sh) script can be used for verification. This script requires the path to the directory containing the traces, and the path to verifyio as arguments. By default, it verifies all supported semantics, i.e., POSIX, MPI-IO, Commit, Session with Vector clock algorithm.
+
+```bash
+./auto_verify.sh /path/to/target/traces /path/to/verifyio.py
+```
+
+#### Note on step 3:
 
  The code first matches all MPI calls to build a graph representing the happens-before order. Each node in the graph represents a MPI call, if there is a path from node A to node B, then A must happens-before B. 
 
@@ -48,3 +78,40 @@ However, things are a little different with default MPI user-imposed semantics (
 With user-imposed semantics, the **"sync-barrier-sync"** construct is required to guarnatee sequencial consistency. Barrier can be replaced by a send-recv or the collectives listed above. Sync is one of MPI_File_open, MPI_File_close or MPI_File_sync.
 
 Now, given two potential conflicting accesses op1 an op2, our job is to find out if there is a **sync-barrier-sync** in between.
+
+
+## Step 4: Export Results to CSV
+
+### Dependencies for step 4 & 5:
+
+Ensure the following dependencies are installed:
+
+#### Python Libraries
+- **argparse**: For parsing command-line arguments.
+- **pandas**: For data manipulation and analysis. Install using `pip install pandas`.
+- **seaborn**: For advanced data visualization. Install using `pip install seaborn`.
+- **matplotlib**: For creating static, animated, and interactive plots. Install using `pip install matplotlib`.
+- **numpy**: For numerical computations. Install using `pip install numpy`.
+
+VerifyIO results can be exported to a CSV format for further analysis by using [`verifyio_to_csv.py `](https://github.com/uiuc-hpc/Recorder/blob/dev/tools/verifyio/scripts/verifyio_to_csv.py). Use the following command, providing the output file (usually stdout from VerifyIO execution) as an argument:
+
+```bash
+python verifyio_to_csv.py /path/to/verifyio/output /path/to/output.csv
+```
+Optional arguments:
+* --dir_prefix="/prefix/to/remove": Removes a specified prefix from the paths in the output.
+* --group_by_api: Groups the output by API calls.
+
+## Step 5: Heatmap Visualization
+
+To visualize the results from VerifyIO, use the [`verifyio_plot_heatmap.py`](https://github.com/uiuc-hpc/Recorder/blob/dev/tools/verifyio/scripts/verifyio_plot_violation_heatmap.py) script:
+
+```bash
+python verifyio_plot_heatmap.py --file=/path/to/output.csv
+```
+Alternatively, for visualizing up to three CSV files in a single heatmap, use the following argument:
+
+```bash
+python verifyio_plot_heatmap.py --files="/path/to/output1.csv" "/path/to/output2.csv" "/path/to/output3.csv"
+```
+

tools/verifyio/scripts/auto_detect.sh

@@ -0,0 +1,25 @@
+#!/bin/bash
+
+if [ -z "$1" ]; then
+    echo "Usage: $0 <base_directory>"
+    exit 1
+fi
+
+BASE_DIR="$1"
+PROGRAM="$RECORDER_INSTALL_PATH/bin/conflict-detector"
+
+if [[ ! -x "$PROGRAM" ]]; then
+    echo "Program $PROGRAM not found or is not executable."
+    exit 1
+fi
+
+for dir in "$BASE_DIR"/*/; do
+    if [ -d "$dir" ]; then
+        echo "Entering directory: $dir"
+        cd "$dir"
+        $PROGRAM "$dir"
+        echo "command: $PROGRAM $dir"
+        echo "finished"
+        cd ..
+    fi
+done

tools/verifyio/scripts/auto_verify.sh

@@ -0,0 +1,31 @@
+#!/bin/bash
+
+
+#SBATCH -N 1
+#SBATCH -J jobname
+#SBATCH -t 01:00:00
+#SBATCH -p partition
+#SBATCH -o /path/to/out.out
+
+
+if [ -z "$1" ]; then
+    echo "Usage: $0 <base_directory>"
+    exit 1
+fi
+
+BASE_DIR="$1"
+PROGRAM="/path/to/verifyio.py"
+SEMANTICS=("POSIX" "MPI-IO" "Commit" "Session")
+
+for semantic in "${SEMANTICS[@]}"; do
+    for dir in "$BASE_DIR"/*/; do
+        if [ -d "$dir" ]; then
+            echo "Entering directory: $dir"
+            (
+                cd "$dir" || exit
+                python "$PROGRAM" "$dir" "--semantics=$semantic"
+            )
+            echo "Finished --semantic=$semantic"
+        fi
+    done
+done