Parallelize & Partition Verification

.github/workflows/kani.yml

@@ -17,25 +17,37 @@ defaults:
 
 jobs:
   check-kani-on-std:
-    name: Verify std library
+    name: Verify std library (partition ${{ matrix.partition }})
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
         os: [ubuntu-latest, macos-latest]
+        partition: [1, 2, 3, 4]
         include:
           - os: ubuntu-latest
             base: ubuntu
           - os: macos-latest
             base: macos
+      fail-fast: false
+
+    env:
+      PARALLEL_INDEX: ${{ matrix.partition }}
+      PARALLEL_TOTAL: 4
+
     steps:
       # Step 1: Check out the repository
       - name: Checkout Repository
         uses: actions/checkout@v4
         with:
           path: head
           submodules: true
-
-      # Step 2: Run Kani on the std library (default configuration)
+
+      # Step 2: Install jq
+      - name: Install jq
+        if: matrix.os == 'ubuntu-latest'
+        run: sudo apt-get install -y jq
+
+      # Step 3: Run Kani on the std library (default configuration)
       - name: Run Kani Verification
         run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
 

scripts/run-kani.sh

@@ -77,6 +77,10 @@ TOML_FILE=${KANI_TOML_FILE:-$DEFAULT_TOML_FILE}
 REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL}
 BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME}
 
+# Kani list related variables, set in get_harnesses(); these are only used to parallelize harness verification
+declare -a ALL_HARNESSES
+declare -i HARNESS_COUNT
+
 # Function to read commit ID from TOML file
 read_commit_from_toml() {
     local file="$1"
@@ -151,10 +155,43 @@ get_kani_path() {
     echo "$(realpath "$build_dir/scripts/kani")"
 }
 
-run_kani_command() {
+# Run kani list with JSON format and process with jq to extract harness names and total number of harnesses.
+# Note: The code to extract ALL_HARNESSES is dependent on `kani list --format json` FILE_VERSION 0.1.
+# If FILE_VERSION changes, this logic may need to change as well.
+get_harnesses() {
+    local kani_path="$1"
+    "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi ./library --std --format json
+    ALL_HARNESSES=($(jq -r '
+        ([.["standard-harnesses"] | to_entries | .[] | .value[]] + 
+            [.["contract-harnesses"] | to_entries | .[] | .value[]]) | 
+        .[]
+    ' $WORK_DIR/kani-list.json))
+    HARNESS_COUNT=${#ALL_HARNESSES[@]}
+}
+
+# Given an array of harness names, run verification for those harnesses
+run_verification_subset() {
     local kani_path="$1"
-    shift
-    "$kani_path" "$@"
+    local harnesses=("${@:2}")  # All arguments after kani_path are harness names
+
+    # Build the --harness arguments
+    local harness_args=""
+    for harness in "${harnesses[@]}"; do
+        harness_args="$harness_args --harness $harness"
+    done
+
+    echo "Running verification for harnesses:"
+    printf '%s\n' "${harnesses[@]}"
+    "$kani_path" verify-std -Z unstable-options ./library \
+        -Z function-contracts \
+        -Z mem-predicates \
+        -Z loop-contracts \
+        -Z float-lib \
+        -Z c-ffi \
+        $harness_args --exact \
+        $command_args \
+        --enable-unstable \
+        --cbmc-args --object-bits 12
 }
 
 # Check if binary exists and is up to date
@@ -176,7 +213,6 @@ check_binary_exists() {
     return 1
 }
 
-
 main() {
     local build_dir="$WORK_DIR/kani_build"
 
@@ -209,16 +245,44 @@ main() {
     "$kani_path" --version
 
     if [[ "$run_command" == "verify-std" ]]; then
-        echo "Running Kani verify-std command..."
-        "$kani_path" verify-std -Z unstable-options ./library \
-            -Z function-contracts \
-            -Z mem-predicates \
-            -Z loop-contracts \
-            -Z float-lib \
-            -Z c-ffi \
-            $command_args \
-            --enable-unstable \
-            --cbmc-args --object-bits 12
+        if [[ -n "$PARALLEL_INDEX" && -n "$PARALLEL_TOTAL" ]]; then
+            echo "Running as parallel worker $PARALLEL_INDEX of $PARALLEL_TOTAL"
+            get_harnesses "$kani_path"
+
+            echo "All harnesses:"
+            printf '%s\n' "${ALL_HARNESSES[@]}"
+            echo "Total number of harnesses: $HARNESS_COUNT"
+
+            # Calculate this worker's portion
+            chunk_size=$(( (HARNESS_COUNT + PARALLEL_TOTAL - 1) / PARALLEL_TOTAL ))
+            echo "Number of harnesses this worker will run: $chunk_size"
+
+            start_idx=$(( (PARALLEL_INDEX - 1) * chunk_size ))
+            end_idx=$(( start_idx + chunk_size ))
+            # If end_idx > HARNESS_COUNT, truncate it to $HARNESS_COUNT
+            [[ $end_idx -gt $HARNESS_COUNT ]] && end_idx=$HARNESS_COUNT
+
+            echo "Start index into ALL_HARNESSES is $start_idx"
+            echo "End index into ALL_HARNESSES is $end_idx"
+
+            # Extract this worker's harnesses
+            worker_harnesses=("${ALL_HARNESSES[@]:$start_idx:$chunk_size}")
+
+            # Run verification for this subset
+            run_verification_subset "$kani_path" "${worker_harnesses[@]}"
+        else
+            # Run verification for all harnesses (not in parallel)
+            echo "Running Kani verify-std command..."
+            "$kani_path" verify-std -Z unstable-options ./library \
+                -Z function-contracts \
+                -Z mem-predicates \
+                -Z loop-contracts \
+                -Z float-lib \
+                -Z c-ffi \
+                $command_args \
+                --enable-unstable \
+                --cbmc-args --object-bits 12
+        fi
     elif [[ "$run_command" == "list" ]]; then
         echo "Running Kani list command..."
         "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi ./library --std --format markdown