Benchmark z3 and cvc5

[jprider63]

This updates the benchmarking CI to display results for z3 and cvc5. An example of what this looks like is available here.

Note: #596 must be merged first.

[jprider63]

I found one edge case. I'm fixing it now.

[jprider63]

This is now fixed!

[PeterSewell]

Looks good. I wouldn't want to suggest anyone tinkers endlessly with the visualisation - but on the other hand it'd be lovely to be able to see the comparisons in a slightly more granular way. Perhaps it'd be easy to fix an order of the tests, eg order by increasing Z3 runtime in the current version, and then draw bargraphs with the tests on the x axis and four thin bars (z3 previous, z3 current, cvc5 previous, cvs current) for each test? Is buddy in the CI? p

…

On Wed, 25 Sept 2024 at 21:30, JP ***@***.***> wrote: This updates the benchmarking CI to display results for z3 and cvc5. An example of what this looks like is available here <https://galoisinc.github.io/cerberus/dev/bench/>. *Note*: #596 <#596> must be merged first. ------------------------------ You can view, comment on, or merge this pull request online at: #597 Commit Summary - 114870c <114870c> Benchmark z3 and cvc5 File Changes (2 files <https://github.com/rems-project/cerberus/pull/597/files>) - *M* .github/workflows/ci-bench.yml <https://github.com/rems-project/cerberus/pull/597/files#diff-c0d8bb86d6a1aa2b01fbd72483d2b2380bd3344a56b386cff7a751410e340f41> (12) - *M* tests/run-ci-benchmarks.sh <https://github.com/rems-project/cerberus/pull/597/files#diff-17a833c88e1426ea9b69871f285b9e438af77bbf2741323e91492668e8f45086> (18) Patch Links: - https://github.com/rems-project/cerberus/pull/597.patch - https://github.com/rems-project/cerberus/pull/597.diff — Reply to this email directly, view it on GitHub <#597>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFMZZQRYWGCPMIJPRJ3W3DZYMMNRAVCNFSM6AAAAABO3KTEJ6VHI2DSMVQWIX3LMV43ASLTON2WKOZSGU2DQOJUGE2DANY> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[cp526]

Is buddy in the CI?

Not currently. Last we checked the performance was bad enough we couldn't tell whether it's even in a working state, so we can't include it in CI at the moment.

[jprider63]

Perhaps it'd be easy to fix an order of the tests, eg order by increasing Z3 runtime in the current version

The current CI visualization tool does not support ordering. I can extend it, but it would take some time.

draw bargraphs with the tests on the x axis and four thin bars (z3 previous, z3 current, cvc5 previous, cvs current) for each test

These graphs currently show how the performance changes over time. They display runtimes with z3 and cvc5 for every update to master, where the x-axis is the update's commit. Would you prefer a single bar graph that only displays the last two updates instead? This would lose the history over time information that would help us identify future regressions.

I've also implemented this PR which runs regression benchmarks on every pull request that is opened. It posts a comment on the PR that compares the previous performance with the PR's performance and highlights any regressions. An example on Galois' fork is here. Unfortunately, it is currently not working on this repository due to Github permission errors that we haven't successfully debugged yet.