forked from model-checking/kani
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add a script to measure build performance
In order to avoid redundancy and make it more maintainable, I refactored the performance script. - I moved the logic into a common script file (kani-perf-setup.sh) - I also changed the performance to run in a temporary file - To avoid messing up with repository files - I changed benchcomp to work with the new location
- Loading branch information
Showing
4 changed files
with
116 additions
and
36 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,23 @@ | ||
#!/usr/bin/env bash | ||
# Copyright Kani Contributors | ||
# SPDX-License-Identifier: Apache-2.0 OR MIT | ||
# Run compiler benchmarks (only build time) | ||
|
||
set -o pipefail | ||
set -o nounset | ||
|
||
SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" | ||
source ${SCRIPT_DIR}/kani-perf-setup.sh | ||
prep_build_perf | ||
run_benchmarks | ||
exit_code=$? | ||
cleanup_perf | ||
|
||
echo | ||
if [ $exit_code -eq 0 ]; then | ||
echo "All Kani perf tests completed successfully." | ||
else | ||
echo "***Kani perf tests failed." | ||
fi | ||
echo | ||
exit $exit_code |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,83 @@ | ||
#!/usr/bin/env bash | ||
# Copyright Kani Contributors | ||
# SPDX-License-Identifier: Apache-2.0 OR MIT | ||
# This is just the setup stage of all performance benchmarks | ||
# Other scripts should source this and invoke which setup they want to run | ||
|
||
set -o pipefail | ||
set -o nounset | ||
|
||
SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" | ||
KANI_DIR=$SCRIPT_DIR/.. | ||
PERF_DIR="${KANI_DIR}/tests/perf" | ||
|
||
SUITE="kani_perf_run_$(date +%s)" | ||
RUN_DIR="/tmp/${SUITE}" | ||
|
||
build_kani() { | ||
# Build Kani using release mode. | ||
cargo build-dev -- --release | ||
} | ||
|
||
prep_perf_files() { | ||
mkdir ${RUN_DIR} # We want to error out if the folder exists | ||
ln -s ${RUN_DIR} ${KANI_DIR}/tests/${SUITE} | ||
cp -r ${PERF_DIR} ${RUN_DIR}/perf | ||
for overlay_dir in ${PERF_DIR}/overlays/*/; do | ||
orig_dir=$(basename ${overlay_dir}) | ||
echo "Copying overlays for $orig_dir" | ||
cp -r -v ${overlay_dir}* ${RUN_DIR}/perf/${orig_dir}/ | ||
done | ||
} | ||
|
||
cleanup_perf() { | ||
echo "Cleaning up..." | ||
rm -r ${RUN_DIR} | ||
rm ${KANI_DIR}/tests/${SUITE} | ||
} | ||
|
||
run_benchmarks() { | ||
suite="${SUITE}" | ||
mode="cargo-kani-test" | ||
echo "Check compiletest suite=$suite mode=$mode" | ||
cargo run -p compiletest -- --suite $suite --mode $mode --no-fail-fast --report-time "$@" | ||
} | ||
|
||
print_result() { | ||
exit_code=$1 | ||
echo | ||
if [ $exit_code -eq 0 ]; then | ||
echo "All Kani perf tests completed successfully." | ||
else | ||
echo "***Kani perf tests failed." | ||
fi | ||
echo | ||
exit $exit_code | ||
} | ||
|
||
prep_build_perf() { | ||
build_kani | ||
# Prepare for a verification first | ||
prep_perf_files | ||
|
||
# Now override expected files to just expect a successful build | ||
expected_files=$(find ${RUN_DIR} -name "*expected") | ||
for expected_file in ${expected_files}; do | ||
echo "Compiling" > ${expected_file} | ||
echo "Finished" >> ${expected_file} | ||
done | ||
|
||
run_benchmarks --kani-flag="--only-codegen" | ||
exit_code=$? | ||
cleanup_perf | ||
print_result ${exit_code} | ||
} | ||
|
||
benchmark_verification() { | ||
build_kani | ||
prep_perf_files | ||
run_benchmarks | ||
exit_code=$? | ||
cleanup_perf | ||
print_result ${exit_code} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters