diff --git a/.github/workflows/bench.yml b/.github/workflows/bench.yml index ad0bbf81f2c2..f7aa9313a186 100644 --- a/.github/workflows/bench.yml +++ b/.github/workflows/bench.yml @@ -10,7 +10,7 @@ name: Kani Performance Benchmarks on: push: branches: - - 'main' + - '*' workflow_call: jobs: diff --git a/tools/benchcomp/benchcomp/visualizers/__init__.py b/tools/benchcomp/benchcomp/visualizers/__init__.py index 8de4a9f130b6..fa33d9e724d0 100644 --- a/tools/benchcomp/benchcomp/visualizers/__init__.py +++ b/tools/benchcomp/benchcomp/visualizers/__init__.py @@ -155,7 +155,9 @@ class dump_markdown_results_table: returns a string that is rendered in the benchmark's row in the new column. This allows you to emit arbitrary text or markdown formatting in response to particular combinations of values for different variants, such as - regressions or performance improvements. + regressions or performance improvements. If `delete_row_if_empty` is set to + `true` on the extra column, then benchmarks for which the extra row text + evaluates to an empty string will not be displayed in the table at all. 'scatterplot' takes the values 'off' (default), 'linear' (linearly scaled axes), or 'log' (logarithmically scaled axes). @@ -176,13 +178,16 @@ class dump_markdown_results_table: else "**" + str(b["variant_2"]/b["variant_1"]) + "**" success: - column_name: change + delete_row_if_empty: true text: > lambda b: "" if b["variant_2"] == b["variant_1"] else "newly passing" if b["variant_2"] else "regressed" ``` - Example output: + Example output. Note that `bench_1` does not appear in the second table + because it neither regressed or is newly passing, so the text in the extra + column is empty, and `delete_row_if_empty` is set to `true`. ``` ## runtime @@ -196,7 +201,6 @@ class dump_markdown_results_table: | Benchmark | variant_1 | variant_2 | change | | --- | --- | --- | --- | - | bench_1 | True | True | | | bench_2 | True | False | regressed | | bench_3 | False | True | newly passing | ``` @@ -355,10 +359,18 @@ def _add_extra_columns(self, metrics): columns = self.extra_columns[metric] except KeyError: continue + to_delete = set() for bench, variants in benches.items(): tmp_variants = dict(variants) for column in columns: variants[column["column_name"]] = column["text"](tmp_variants) + if all(( + column.get("delete_row_if_empty"), + not variants[column["column_name"]])): + to_delete.add(bench) + break + for bench in to_delete: + benches.pop(bench) @staticmethod diff --git a/tools/benchcomp/configs/perf-regression.yaml b/tools/benchcomp/configs/perf-regression.yaml index c938b3dd861f..63f8396e75f5 100644 --- a/tools/benchcomp/configs/perf-regression.yaml +++ b/tools/benchcomp/configs/perf-regression.yaml @@ -40,6 +40,7 @@ visualize: # embolden if the absolute difference is more than 10% of the old value number_vccs: - column_name: diff old → new + delete_row_if_empty: true text: > lambda b: "" if b["kani_new"] == b["kani_old"] else ("**" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) > 0.1 else "") @@ -48,6 +49,7 @@ visualize: + ("**" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) > 0.1 else "") number_program_steps: - column_name: diff old → new + delete_row_if_empty: true text: > lambda b: "" if b["kani_new"] == b["kani_old"] else ("**" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) > 0.1 else "") @@ -59,24 +61,27 @@ visualize: # cells whose absolute change is >50% solver_runtime: - column_name: "% change old → new" + delete_row_if_empty: true text: > - lambda b: "" if b["kani_new"] == b["kani_old"] + lambda b: "" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) < 0.1 else ("**" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) > 0.5 else "") + ("+" if b["kani_new"] > b["kani_old"] else "") + "%.3f%%" % ((b["kani_new"] - b["kani_old"]) * 100 / b["kani_old"]) + ("**" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) > 0.5 else "") verification_time: - column_name: "% change old → new" + delete_row_if_empty: true text: > - lambda b: "" if b["kani_new"] == b["kani_old"] + lambda b: "" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) < 0.1 else ("**" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) > 0.5 else "") + ("+" if b["kani_new"] > b["kani_old"] else "") + "%.3f%%" % ((b["kani_new"] - b["kani_old"]) * 100 / b["kani_old"]) + ("**" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) > 0.5 else "") symex_runtime: - column_name: "% change old → new" + delete_row_if_empty: true text: > - lambda b: "" if b["kani_new"] == b["kani_old"] + lambda b: "" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) < 0.1 else ("**" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) > 0.5 else "") + ("+" if b["kani_new"] > b["kani_old"] else "") + "%.3f%%" % ((b["kani_new"] - b["kani_old"]) * 100 / b["kani_old"]) @@ -85,6 +90,7 @@ visualize: # For success metric, display some text if success has changed success: - column_name: change + delete_row_if_empty: true text: > lambda b: "" if b["kani_new"] == b["kani_old"] else "❌ newly failing" if b["kani_old"]