Skip to content

Commit 2d05ec4

Browse files
AlexanderPortlandAlexanderPortland
committed
reorganize bench labels & workflows
by separating EndToEnd and Compiler [only] benchmarks and ensuring they each get run on appropriate changes
1 parent 4f99b01 commit 2d05ec4

File tree

4 files changed

+109
-74
lines changed

4 files changed

+109
-74
lines changed

‎.github/labeler.yml‎

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,20 @@
55
#
66
# Note that we enable dot, so "**" matches all files in a folder
77

8-
Z-BenchCI:
8+
Z-EndToEndBenchCI:
99
- any:
1010
- changed-files:
11-
- any-glob-to-any-file: ['kani-compiler/**', 'kani-driver/src/call-*', 'cprover_bindings/**', 'library/**']
11+
- any-glob-to-any-file: ['kani-compiler/**', 'kani-driver/src/call_*', 'cprover_bindings/**', 'library/**']
1212
- any-glob-to-any-file: ['rust-toolchain.toml', 'Cargo.lock']
1313
- any-glob-to-any-file: ['kani-dependencies']
14+
15+
Z-CompilerBenchCI:
16+
- any:
17+
# we want to run compiler benchmarks if:
18+
- changed-files:
19+
# any parts of the compiler change
20+
- any-glob-to-any-file: ['kani-compiler/**', 'cprover_bindings/**', 'library/**']
21+
# the way we call the compiler through cargo changes
22+
- any-glob-to-any-file: ['kani-driver/src/call_cargo.rs']
23+
# or if our dependencies change
24+
- any-glob-to-any-file: ['rust-toolchain.toml', 'Cargo.lock', 'kani-dependencies']

‎.github/workflows/bench.yml‎ renamed to ‎.github/workflows/bench-compiler.yml‎

Lines changed: 2 additions & 68 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
# This workflow will run when:
77
# - Changes are pushed to 'main'.
88
# - Triggered by another workflow
9-
name: Kani Performance Benchmarks
9+
name: Kani Compiler Performance Benchmarks
1010
on:
1111
push:
1212
branches:
@@ -75,70 +75,4 @@ jobs:
7575
export PATH="${{ github.workspace }}/new/scripts:$PATH"
7676
cd new/tests/perf && ../../target/release/compile-timer --out-path compile-times-new.json --ignore kani-lib --ignore display_trait --ignore s2n-quic
7777
- name: Run analysis between the two
78-
run: ./new/target/release/compile-analyzer --path-pre old/tests/perf/compile-times-old.json --path-post new/tests/perf/compile-times-new.json --only-markdown >> "$GITHUB_STEP_SUMMARY"
79-
80-
81-
perf-benchcomp:
82-
runs-on: ubuntu-24.04
83-
steps:
84-
- name: Save push event HEAD and HEAD~ to environment variables
85-
if: ${{ github.event_name == 'push' }}
86-
run: |
87-
echo "NEW_REF=${{ github.event.after}}" | tee -a "$GITHUB_ENV"
88-
echo "OLD_REF=${{ github.event.before }}" | tee -a "$GITHUB_ENV"
89-
90-
- name: Save pull request HEAD and base to environment variables
91-
if: ${{ contains(fromJSON('["pull_request", "pull_request_target"]'), github.event_name) }}
92-
run: |
93-
echo "OLD_REF=${{ github.event.pull_request.base.sha }}" | tee -a "$GITHUB_ENV"
94-
echo "NEW_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV"
95-
96-
- name: Check out Kani (old variant)
97-
uses: actions/checkout@v4
98-
with:
99-
path: ./old
100-
ref: ${{ env.OLD_REF }}
101-
fetch-depth: 2
102-
103-
- name: Check out Kani (new variant)
104-
uses: actions/checkout@v4
105-
with:
106-
path: ./new
107-
ref: ${{ env.NEW_REF }}
108-
fetch-depth: 1
109-
110-
- name: Set up Kani Dependencies (old variant)
111-
uses: ./old/.github/actions/setup
112-
with:
113-
os: ubuntu-24.04
114-
kani_dir: old
115-
116-
- name: Set up Kani Dependencies (new variant)
117-
uses: ./new/.github/actions/setup
118-
with:
119-
os: ubuntu-24.04
120-
kani_dir: new
121-
122-
- name: Copy benchmarks from new to old
123-
run: rm -rf ./old/tests/perf ; cp -r ./new/tests/perf ./old/tests/
124-
125-
- name: Run benchcomp
126-
run: |
127-
new/tools/benchcomp/bin/benchcomp \
128-
--config new/tools/benchcomp/configs/perf-regression.yaml \
129-
run
130-
new/tools/benchcomp/bin/benchcomp \
131-
--config new/tools/benchcomp/configs/perf-regression.yaml \
132-
collate
133-
134-
- name: Perf Regression Results Table
135-
run: |
136-
new/tools/benchcomp/bin/benchcomp \
137-
--config new/tools/benchcomp/configs/perf-regression.yaml \
138-
visualize --only dump_markdown_results_table >> "$GITHUB_STEP_SUMMARY"
139-
140-
- name: Run other visualizations
141-
run: |
142-
new/tools/benchcomp/bin/benchcomp \
143-
--config new/tools/benchcomp/configs/perf-regression.yaml \
144-
visualize --except dump_markdown_results_table
78+
run: ./new/target/release/compile-analyzer --path-pre old/tests/perf/compile-times-old.json --path-post new/tests/perf/compile-times-new.json --only-markdown >> "$GITHUB_STEP_SUMMARY"

‎.github/workflows/bench-e2e.yml‎

Lines changed: 80 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,80 @@
1+
# Copyright Kani Contributors
2+
# SPDX-License-Identifier: Apache-2.0 OR MIT
3+
#
4+
# Run performance benchmarks comparing two different Kani versions.
5+
# This workflow takes much longer than other workflows, so we don't run it by default.
6+
# This workflow will run when:
7+
# - Changes are pushed to 'main'.
8+
# - Triggered by another workflow
9+
name: Kani End-To-End Performance Benchmarks
10+
on:
11+
push:
12+
branches:
13+
- 'main'
14+
workflow_call:
15+
16+
jobs:
17+
perf-benchcomp:
18+
runs-on: ubuntu-24.04
19+
steps:
20+
- name: Save push event HEAD and HEAD~ to environment variables
21+
if: ${{ github.event_name == 'push' }}
22+
run: |
23+
echo "NEW_REF=${{ github.event.after}}" | tee -a "$GITHUB_ENV"
24+
echo "OLD_REF=${{ github.event.before }}" | tee -a "$GITHUB_ENV"
25+
26+
- name: Save pull request HEAD and base to environment variables
27+
if: ${{ contains(fromJSON('["pull_request", "pull_request_target"]'), github.event_name) }}
28+
run: |
29+
echo "OLD_REF=${{ github.event.pull_request.base.sha }}" | tee -a "$GITHUB_ENV"
30+
echo "NEW_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV"
31+
32+
- name: Check out Kani (old variant)
33+
uses: actions/checkout@v4
34+
with:
35+
path: ./old
36+
ref: ${{ env.OLD_REF }}
37+
fetch-depth: 2
38+
39+
- name: Check out Kani (new variant)
40+
uses: actions/checkout@v4
41+
with:
42+
path: ./new
43+
ref: ${{ env.NEW_REF }}
44+
fetch-depth: 1
45+
46+
- name: Set up Kani Dependencies (old variant)
47+
uses: ./old/.github/actions/setup
48+
with:
49+
os: ubuntu-24.04
50+
kani_dir: old
51+
52+
- name: Set up Kani Dependencies (new variant)
53+
uses: ./new/.github/actions/setup
54+
with:
55+
os: ubuntu-24.04
56+
kani_dir: new
57+
58+
- name: Copy benchmarks from new to old
59+
run: rm -rf ./old/tests/perf ; cp -r ./new/tests/perf ./old/tests/
60+
61+
- name: Run benchcomp
62+
run: |
63+
new/tools/benchcomp/bin/benchcomp \
64+
--config new/tools/benchcomp/configs/perf-regression.yaml \
65+
run
66+
new/tools/benchcomp/bin/benchcomp \
67+
--config new/tools/benchcomp/configs/perf-regression.yaml \
68+
collate
69+
70+
- name: Perf Regression Results Table
71+
run: |
72+
new/tools/benchcomp/bin/benchcomp \
73+
--config new/tools/benchcomp/configs/perf-regression.yaml \
74+
visualize --only dump_markdown_results_table >> "$GITHUB_STEP_SUMMARY"
75+
76+
- name: Run other visualizations
77+
run: |
78+
new/tools/benchcomp/bin/benchcomp \
79+
--config new/tools/benchcomp/configs/perf-regression.yaml \
80+
visualize --except dump_markdown_results_table

‎.github/workflows/extra_jobs.yml‎

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,9 @@ name: Kani Extra
2121
on:
2222
pull_request_target:
2323
merge_group:
24+
push:
25+
branches:
26+
- 'main'
2427

2528
jobs:
2629
# Keep this job minimal since it requires extra permission
@@ -43,9 +46,16 @@ jobs:
4346
with:
4447
dot: true
4548

46-
verification-bench:
47-
name: Verification Benchmarks
49+
end-to-end-bench:
50+
name: End-to-End Benchmarks
4851
needs: auto-label
4952
permissions: {}
50-
if: ${{ contains(needs.auto-label.outputs.all-labels, 'Z-BenchCI') && github.event_name != 'merge_group' }}
51-
uses: ./.github/workflows/bench.yml
53+
if: ${{ contains(needs.auto-label.outputs.all-labels, 'Z-EndToEndBenchCI') && github.event_name != 'merge_group' }}
54+
uses: ./.github/workflows/bench-e2e.yml
55+
56+
compiler-bench:
57+
name: Compiler Benchmarks
58+
needs: auto-label
59+
permissions: {}
60+
if: ${{ contains(needs.auto-label.outputs.all-labels, 'Z-CompilerBenchCI') && github.event_name != 'merge_group' }}
61+
uses: ./.github/workflows/bench-compiler.yml

0 commit comments

Comments
 (0)