Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Parallel verification #21

Closed
wants to merge 10 commits into from
Prev Previous commit
Next Next commit
add more debug printing
  • Loading branch information
carolynzech committed Dec 16, 2024
commit eabaca149f8585d66e7ed39429a239ced2f39304
13 changes: 12 additions & 1 deletion scripts/run-kani.sh
Original file line number Diff line number Diff line change
Expand Up @@ -178,7 +178,8 @@ run_verification_subset() {
harness_args="$harness_args --harness $harness"
done

echo "Running verification for harnesses: ${harnesses[*]}"
echo "Running verification for harnesses:"
printf '%s\n' "${harnesses[@]}"
"$kani_path" verify-std -Z unstable-options ./library \
-Z function-contracts \
-Z mem-predicates \
Expand Down Expand Up @@ -245,12 +246,22 @@ main() {
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}")
Expand Down
Loading