From 4c523b5d7586e3dd20338e57126d40542a124b70 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Fri, 29 Aug 2025 12:58:02 +0100
Subject: [PATCH] feat: use matrix strategy to distribute LLVM evaluation

---
 .github/workflows/docker.yml | 35 +++++++++++++++++++++++---
 bv-evaluation/compare.py     | 48 +++++++++++++++++++++++++-----------
 2 files changed, 66 insertions(+), 17 deletions(-)

diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
index f591d46249..f31bf140fc 100644
--- a/.github/workflows/docker.yml
+++ b/.github/workflows/docker.yml
@@ -146,8 +146,10 @@ jobs:
     defaults:
       run:
         working-directory: /code/lean-mlir/bv-evaluation
-    permissions:
-      pull-requests: write
+    strategy:
+      matrix:
+        offset: [0, 1, 2]
+        stride: [3]
     steps:     
       - name: Symlink .elan (to correct for GHA changing $HOME)
         run: '[ -e ~/.elan ] || ln -s /root/.elan ~/.elan'
@@ -155,8 +157,35 @@ jobs:
       - name: Run LLVM
         continue-on-error: true
         run: |
-          uv run ./compare.py instcombine -j48 \
+          uv run ./compare.py instcombine -j48 --stride=${{matrix.stride}} --offset=${{matrix.offset}} \
             || echo "LEANMLIR_STATUS=fail" >> $GITHUB_ENV
+      
+      - name: Upload logs
+        id: upload
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ github.run_id }}-instcombine-logs-${{matrix.offset}}
+          retention-days: 1
+          path: |
+            /code/lean-mlir/bv-evaluation/results/InstCombine/
+
+  report-LLVM:
+    name: Collect & report LLVM evaluation data   
+    runs-on: ubuntu-latest # Run on GH-provided runner
+    needs: evaluation-LLVM
+    container: "ghcr.io/opencompl/lean-mlir-instcombine:${{ github.sha }}"
+    defaults:
+      run:
+        working-directory: /code/lean-mlir/bv-evaluation
+    permissions:
+      pull-requests: write
+    steps:
+      - name: Download data
+        uses: actions/download-artifact@v5
+        with:
+          path: /code/lean-mlir/bv-evaluation/results/InstCombine/
+          pattern: ${{ github.run_id }}-instcombine-logs-*
+          merge-multiple: true
 
       - name: Collect data LLVM
         continue-on-error: true
diff --git a/bv-evaluation/compare.py b/bv-evaluation/compare.py
index c38e91c251..bde19dd696 100755
--- a/bv-evaluation/compare.py
+++ b/bv-evaluation/compare.py
@@ -175,6 +175,8 @@ def compare(
     memout: int,
     num_samples,
     seed,
+    stride: int,
+    offset: int
 ):
     """Processes benchmarks using a thread pool."""
     with concurrent.futures.ThreadPoolExecutor(max_workers=jobs) as executor:
@@ -237,20 +239,22 @@ def compare(
             clear_folder(RESULTS_DIR_INSTCOMBINE)
             os.makedirs(RESULTS_DIR_INSTCOMBINE, exist_ok=True)
 
-            for file in os.listdir(BENCHMARK_DIR_INSTCOMBINE):
-                if "_proof" in file and file.endswith(
-                    ".lean"
-                ):  # Ensure it's a Lean file
-                    for r in range(reps):
-                        file_path = os.path.join(BENCHMARK_DIR_INSTCOMBINE, file)
-                        file_title = os.path.splitext(file)[0]
-                        log_file_path = os.path.join(
-                            RESULTS_DIR_INSTCOMBINE, f"{file_title}_r{str(r)}.txt"
-                        )
-                        future = executor.submit(
-                            run_file, file_path, log_file_path
-                        )
-                        futures[future] = file_path
+            files = [ file for file in os.listdir(BENCHMARK_DIR_INSTCOMBINE)
+                        if "_proof" in file and file.endswith(".lean") ] # Ensure it's a Lean file
+            # Filter to just the files meant for this runner (if distributed)
+            files = files[offset::stride]
+
+            for file in files:
+                for r in range(reps):
+                    file_path = os.path.join(BENCHMARK_DIR_INSTCOMBINE, file)
+                    file_title = os.path.splitext(file)[0]
+                    log_file_path = os.path.join(
+                        RESULTS_DIR_INSTCOMBINE, f"{file_title}_r{str(r)}.txt"
+                    )
+                    future = executor.submit(
+                        run_file, file_path, log_file_path
+                    )
+                    futures[future] = file_path
 
         elif benchmark == "smtlib":
             clear_folder(RESULTS_DIR_SMTLIB)
@@ -331,6 +335,20 @@ def main():
         help="Solver for SMT-LIB benchmarks",
     )
 
+    parser.add_argument(
+        "--stride",
+        type=int,
+        default=1,
+        help="For distributed runs, the total number of jobs (instcombine benchmark only!)"
+    )
+
+    parser.add_argument(
+        "--offset",
+        type=int,
+        default=0,
+        help="For distributed runs, the index of the current runner (instcombine benchmark only!)"
+    )
+
     args = parser.parse_args()
     benchmarks_to_run = (
         ["hackersdelight", "instcombine", "smtlib"]
@@ -348,6 +366,8 @@ def main():
             args.memout,
             args.num_samples,
             args.seed,
+            args.stride,
+            args.offset
         )