From 50481e2b476c1cb35d07d76cfb1a7cdef93107bd Mon Sep 17 00:00:00 2001 From: James Parker Date: Mon, 26 Aug 2024 10:47:29 -0400 Subject: [PATCH 1/8] Benchmarking for PRs --- .github/workflows/ci-pr-bench.yml | 158 ++++++++++++++++++++++++++++++ tests/compare-benchmarks.py | 73 ++++++++++++++ 2 files changed, 231 insertions(+) create mode 100644 .github/workflows/ci-pr-bench.yml create mode 100755 tests/compare-benchmarks.py diff --git a/.github/workflows/ci-pr-bench.yml b/.github/workflows/ci-pr-bench.yml new file mode 100644 index 000000000..fe563ccec --- /dev/null +++ b/.github/workflows/ci-pr-bench.yml @@ -0,0 +1,158 @@ +name: CI Benchmarks + +on: + pull_request: + branches: + - master + +env: + CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn:release + +permissions: + # Allow commenting on the PR + pull-requests: write + +# cancel in-progress job when a new push is performed +concurrency: + group: ci-pr-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 + with: + fetch-depth: 100 # this is to make sure we obtain the target base commit + + - name: System dependencies (ubuntu) + run: | + sudo apt install build-essential libgmp-dev z3 opam cmake + + - 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 python dependencies + run: pip install tabulate + + - 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: Set environment variables + run: | + echo "BASE_DATA=$(mktemp)" >> $GITHUB_ENV + echo "PR_DATA=$(mktemp)" >> $GITHUB_ENV + echo "COMMENT=$(mktemp)" >> $GITHUB_ENV + echo "BASE_SHA=$(echo ${{ github.event.pull_request.base.sha }} | cut -c1-8)" >> $GITHUB_ENV + echo "HEAD_SHA=$(echo ${{ github.event.pull_request.head.sha }} | cut -c1-8)" >> $GITHUB_ENV + + - name: Run benchmark on PR + run: | + opam switch ${{ matrix.version }} + eval $(opam env --switch=${{ matrix.version }}) + cd tests; USE_OPAM='' ./run-ci-benchmarks.sh + mv benchmark-data.json ${{ env.PR_DATA }} + cd .. + + - name: Switch to target branch + run: | + git checkout ${{ github.event.pull_request.base.sha }} + + - 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: 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 on baseline + run: | + opam switch ${{ matrix.version }} + eval $(opam env --switch=${{ matrix.version }}) + cd tests; USE_OPAM='' ./run-ci-benchmarks.sh; mv benchmark-data.json ${{ env.BASE_DATA }} + cd .. + + - name: Compare results + run: | + echo 'Benchmark comparison for [`${{ env.HEAD_SHA }}`](${{ github.event.repository.html_url }}/commit/${{ github.event.pull_request.head.sha }}) (PR) vs [`${{ env.BASE_SHA }}`](${{ github.event.repository.html_url }}/commit/${{ github.event.pull_request.base.sha }}) (baseline).' >> ${{ env.COMMENT }} + git checkout ${{ github.event.pull_request.head.sha }} + tests/compare-benchmarks.py ${{ env.BASE_DATA }} ${{ env.PR_DATA }} >> ${{ env.COMMENT }} + + - name: 'Comment PR' + uses: actions/github-script@v4.0.2 + with: + github-token: ${{ secrets.GITHUB_TOKEN }} + script: | + github.issues.createComment({ + issue_number: context.issue.number, + owner: context.repo.owner, + repo: context.repo.repo, + body: require('fs').readFileSync('${{ env.COMMENT }}').toString() + }); diff --git a/tests/compare-benchmarks.py b/tests/compare-benchmarks.py new file mode 100755 index 000000000..7f6f9d8ec --- /dev/null +++ b/tests/compare-benchmarks.py @@ -0,0 +1,73 @@ +#!/usr/bin/env python3 + +import json +import sys +import tabulate + +# Warn if the new code exceeds this percentage threshold of slowdown. +THRESHOLD = 150 # 2.5x slowdown + +def to_diff(new_value, baseline_value): + diff = new_value - baseline_value + + percent = (new_value / baseline_value - 1) * 100 + output = "{diff:+.2f} ({percent:+.2f}%)".format(diff=diff, percent=percent) + + return (output, percent) + +def main(): + if len(sys.argv) != 3: + print("usage: compare-benchmarks.py ", file=sys.stderr) + exit(-1) + + + with open(sys.argv[2], 'r') as f: + new_data = json.load(f) + + new_numbers = {} + for benchmark in new_data: + new_numbers[benchmark['name']] = benchmark['value'] + + with open(sys.argv[1], 'r') as f: + baseline = json.load(f) + + missing = set() + degradation = set() + + output = [] + for benchmark in baseline: + name = benchmark['name'] + baseline_value = benchmark['value'] + + new_value_m = new_numbers.get(name) + if new_value_m: + (diff, percentage) = to_diff(new_value_m, baseline_value) + + if percentage > THRESHOLD: + disp_name = "**" + name + "***" + degradation.add(name) + else: + disp_name = name + + output.append([disp_name, baseline_value, new_value_m, diff]) + + del new_numbers[name] + else: + missing.add(name) + + print("") + if len(degradation) != 0: + print("**Warning**: Performance degradations: " + ', '.join(degradation)) + if len(missing) != 0: + print("**Warning**: Removed benchmarks: " + ', '.join(missing)) + added = new_numbers.keys() + if len(added) != 0: + print("Added benchmarks: " + ', '.join(added)) + + print("\n# Benchmark comparison\n") + + # Benchmark name | Old time (s) | New time (s) | Difference (s) + print(tabulate.tabulate(output, headers=['Benchmark name', 'Baseline time (s)', 'New time (s)', 'Difference (s)'], tablefmt='pipe')) + +if __name__ == "__main__": + main() From 6d1dbc37b9dcb5e76e4390a79a4b5b9614572614 Mon Sep 17 00:00:00 2001 From: James Parker Date: Thu, 29 Aug 2024 11:47:35 -0400 Subject: [PATCH 2/8] Give permission for commenting on PRs --- .github/workflows/ci-pr-bench.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ci-pr-bench.yml b/.github/workflows/ci-pr-bench.yml index fe563ccec..6ab34b27d 100644 --- a/.github/workflows/ci-pr-bench.yml +++ b/.github/workflows/ci-pr-bench.yml @@ -11,6 +11,7 @@ env: permissions: # Allow commenting on the PR pull-requests: write + issues: write # cancel in-progress job when a new push is performed concurrency: From fde20655064d00b40faa33c5fcc3e9406374021c Mon Sep 17 00:00:00 2001 From: James Parker Date: Thu, 29 Aug 2024 13:08:49 -0400 Subject: [PATCH 3/8] Try giving all permissions for commenting --- .github/workflows/ci-pr-bench.yml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/.github/workflows/ci-pr-bench.yml b/.github/workflows/ci-pr-bench.yml index 6ab34b27d..c52f82492 100644 --- a/.github/workflows/ci-pr-bench.yml +++ b/.github/workflows/ci-pr-bench.yml @@ -8,10 +8,7 @@ on: env: CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn:release -permissions: - # Allow commenting on the PR - pull-requests: write - issues: write +permissions: write-all # cancel in-progress job when a new push is performed concurrency: From 90c146861e19b50e1e090606f0dc70e9cd0a7696 Mon Sep 17 00:00:00 2001 From: James Parker Date: Thu, 29 Aug 2024 13:26:23 -0400 Subject: [PATCH 4/8] Try removing permission field --- .github/workflows/ci-pr-bench.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/ci-pr-bench.yml b/.github/workflows/ci-pr-bench.yml index c52f82492..6a7298fb0 100644 --- a/.github/workflows/ci-pr-bench.yml +++ b/.github/workflows/ci-pr-bench.yml @@ -8,8 +8,6 @@ on: env: CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn:release -permissions: write-all - # cancel in-progress job when a new push is performed concurrency: group: ci-pr-bench-${{ github.workflow }}-${{ github.ref }} From ecd29063907324875b28ef4cd2a512238448c844 Mon Sep 17 00:00:00 2001 From: James Parker Date: Mon, 9 Sep 2024 15:46:34 -0400 Subject: [PATCH 5/8] Report total runtime in PR benchmark comments --- tests/compare-benchmarks.py | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/tests/compare-benchmarks.py b/tests/compare-benchmarks.py index 7f6f9d8ec..3fef5c86a 100755 --- a/tests/compare-benchmarks.py +++ b/tests/compare-benchmarks.py @@ -33,14 +33,18 @@ def main(): missing = set() degradation = set() + baseline_total = 0 + new_total = 0 output = [] for benchmark in baseline: name = benchmark['name'] baseline_value = benchmark['value'] + baseline_total += baseline_value new_value_m = new_numbers.get(name) if new_value_m: + new_total += new_value_m (diff, percentage) = to_diff(new_value_m, baseline_value) if percentage > THRESHOLD: @@ -55,6 +59,15 @@ def main(): else: missing.add(name) + for name in new_numbers: + new_value = new_numbers[name] + output.append([name, "-", new_value, "-"]) + + new_total += new_value + + (total_diff, _) = to_diff(new_total, baseline_total) + output.append(["**Total runtime**", baseline_total, new_total, total_diff]) + print("") if len(degradation) != 0: print("**Warning**: Performance degradations: " + ', '.join(degradation)) From 489e79fa657ed7470aa190994f04948ba7ffb4df Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Wed, 25 Sep 2024 15:22:22 +0100 Subject: [PATCH 6/8] add newline to trigger CI re-run --- .github/workflows/ci-pr-bench.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ci-pr-bench.yml b/.github/workflows/ci-pr-bench.yml index 6a7298fb0..6e9caefa4 100644 --- a/.github/workflows/ci-pr-bench.yml +++ b/.github/workflows/ci-pr-bench.yml @@ -152,3 +152,4 @@ jobs: repo: context.repo.repo, body: require('fs').readFileSync('${{ env.COMMENT }}').toString() }); + From 07e4c2d888629086427eb8eaa87bc3bf6538627b Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Wed, 25 Sep 2024 15:36:31 +0100 Subject: [PATCH 7/8] add James's permission in --- .github/workflows/ci-pr-bench.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/ci-pr-bench.yml b/.github/workflows/ci-pr-bench.yml index 6e9caefa4..299938d4d 100644 --- a/.github/workflows/ci-pr-bench.yml +++ b/.github/workflows/ci-pr-bench.yml @@ -5,6 +5,10 @@ on: branches: - master +permissions: + pull-requests: write + issues: write + env: CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn:release From 1280d99086bae1a9c10c9d86fb1d675aecaa842a Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Wed, 25 Sep 2024 15:48:10 +0100 Subject: [PATCH 8/8] another attempt, from https://github.com/actions/github-script#comment-on-an-issue --- .github/workflows/ci-pr-bench.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci-pr-bench.yml b/.github/workflows/ci-pr-bench.yml index 299938d4d..3fde1eb22 100644 --- a/.github/workflows/ci-pr-bench.yml +++ b/.github/workflows/ci-pr-bench.yml @@ -146,11 +146,11 @@ jobs: tests/compare-benchmarks.py ${{ env.BASE_DATA }} ${{ env.PR_DATA }} >> ${{ env.COMMENT }} - name: 'Comment PR' - uses: actions/github-script@v4.0.2 + uses: actions/github-script@v7 with: github-token: ${{ secrets.GITHUB_TOKEN }} script: | - github.issues.createComment({ + github.rest.issues.createComment({ issue_number: context.issue.number, owner: context.repo.owner, repo: context.repo.repo,