diff --git a/.github/workflows/ci-bench.yml b/.github/workflows/ci-bench.yml new file mode 100644 index 000000000..88882ab7b --- /dev/null +++ b/.github/workflows/ci-bench.yml @@ -0,0 +1,113 @@ +name: CI Benchmarks + +on: + push: + branches: + - master + +env: + CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn:release + +permissions: + # deployments permission to deploy GitHub pages website + deployments: write + # contents permission to update benchmark contents in gh-pages branch + contents: write + +# cancel in-progress job when a new push is performed +concurrency: + group: ci-bench-${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +jobs: + benchmark: + name: Performance benchmarks + strategy: + matrix: + # version: [4.12.0, 4.14.1] + version: [4.14.1] + + + runs-on: ubuntu-22.04 + + steps: + - uses: actions/checkout@v3 + + - name: System dependencies (ubuntu) + run: | + sudo apt install build-essential libgmp-dev z3 opam cmake jq + + - name: Restore cached opam + id: cache-opam-restore + uses: actions/cache/restore@v4 + with: + path: ~/.opam + key: ${{ matrix.version }} + + - name: Setup opam + if: steps.cache-opam-restore.outputs.cache-hit != 'true' + run: | + opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }} + opam install --deps-only --yes ./cerberus-lib.opam + opam switch create with_coq ${{ matrix.version }} + eval $(opam env --switch=with_coq) + opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released + opam pin --yes -n coq-struct-tact https://github.com/uwplse/StructTact.git + opam repo add --yes --this-switch iris-dev https://gitlab.mpi-sws.org/iris/opam.git + opam pin --yes -n coq-sail-stdpp https://github.com/rems-project/coq-sail.git#f319aad + opam pin --yes -n coq-cheri-capabilities https://github.com/rems-project/coq-cheri-capabilities.git + opam install --deps-only --yes ./cerberus-lib.opam ./cerberus-cheri.opam + + - name: Save cached opam + if: steps.cache-opam-restore.outputs.cache-hit != 'true' + id: cache-opam-save + uses: actions/cache/save@v4 + with: + path: ~/.opam + key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }} + + - name: Install Cerberus + run: | + opam switch ${{ matrix.version }} + eval $(opam env --switch=${{ matrix.version }}) + opam pin --yes --no-action add cerberus-lib . + opam pin --yes --no-action add cerberus . + opam install --yes cerberus + + - name: Download cvc5 release + uses: robinraju/release-downloader@v1 + with: + repository: cvc5/cvc5 + tag: cvc5-1.1.2 + fileName: cvc5-Linux-static.zip + + - name: Unzip and install cvc5 + run: | + unzip cvc5-Linux-static.zip + chmod +x cvc5-Linux-static/bin/cvc5 + sudo cp cvc5-Linux-static/bin/cvc5 /usr/local/bin/ + + - name: Install CN + run: | + opam switch ${{ matrix.version }} + eval $(opam env --switch=${{ matrix.version }}) + opam pin --yes --no-action add cn . + opam install --yes cn ocamlformat.0.26.2 + + - name: Run benchmark + run: | + opam switch ${{ matrix.version }} + eval $(opam env --switch=${{ matrix.version }}) + cd tests; USE_OPAM='' ./run-ci-benchmarks.sh + cd .. + + - name: Store benchmark result + uses: benchmark-action/github-action-benchmark@v1 + with: + name: CN Benchmarks + tool: 'customSmallerIsBetter' + output-file-path: tests/benchmark-data.json + # Access token to deploy GitHub Pages branch + github-token: ${{ secrets.GITHUB_TOKEN }} + # Push and deploy GitHub pages branch automatically + auto-push: true diff --git a/tests/run-ci-benchmarks.sh b/tests/run-ci-benchmarks.sh new file mode 100755 index 000000000..f209dfd05 --- /dev/null +++ b/tests/run-ci-benchmarks.sh @@ -0,0 +1,50 @@ +#!/usr/bin/env bash +set -euo pipefail -o noclobber +# set -xv # uncomment to debug variables + +JSON_FILE="benchmark-data.json" + +echo "[" >> "${JSON_FILE}" + +DIRNAME=$(dirname "$0") + +TESTS=$(find "${DIRNAME}"/cn -name '*.c') + +COUNT=0 +for TEST in ${TESTS}; do + let COUNT=${COUNT}+1 +done + +INDEX=0 +for TEST in ${TESTS}; do + + # Record wall clock time in seconds + /usr/bin/time --quiet -f "%e" -o /tmp/time cn verify "${TEST}" || true + TIME=$(cat /tmp/time) + + # If we're last, don't print a trailing comma. + if [[ ${INDEX} -eq ${COUNT}-1 ]]; then + # Hack to output JSON. + cat << EOF >> ${JSON_FILE} + { + "name": "${TEST}", + "unit": "Seconds", + "value": ${TIME} + } +EOF + else + cat << EOF >> ${JSON_FILE} + { + "name": "${TEST}", + "unit": "Seconds", + "value": ${TIME} + }, +EOF + fi + + let INDEX=${INDEX}+1 +done + +echo "]" >> "${JSON_FILE}" + +jq . "${JSON_FILE}"