This may frequently block on benchmarks which take a small amount of time (e.g., less than 5s). Maybe we should define different scales, for example:

* Less than 1s: Block on >3s

* Less than 30s: Block on >1min

* Anything else: Block on >1.1x

Of course, I haven't experimented on these particular values, so more scales or tweaks might be needed.

I agree with the idea that we have different scales for different benchmarks. But I am not sure about the numbers. How about running this check in CI a couple times to collect the data of running, time and then use the data to decide the scale numbers.

Just a nit: This PR is adding a new workflow for PRs but it isn't blocking yet. AFAIK, this is a github configuration which I think we should activate only after we adjust the scale that ensures this job won't give too many false positives.

Thanks, I've changed the commit message. Agreed about leaving this to bake for a while before we make it blocking

@qinheping here are my thoughts on which numbers to use:

I've tried a few experiments with CI and locally. I get a lot less variance locally, often all benchmarks (or all but one) have a variance <10%. This is when comparing identical Kanis.

In CI, the numbers that @adpaco-aws seem to work well for now. I do think it would be a good idea to optimize these numbers, but I would prefer to see what the range is on realistic PRs---that is, PRs that actually change the implementation of Kani and so cause and actual performance difference.

What I propose:

• In a future PR, I'll save the results.yaml file as an artifact. This will allow me to download the results of several runs over the last 30 days.
• benchcomp visualize can be used locally on a results.yaml file, without re-running the benchmarks. So if we download a lot of results.yaml files, we can try lots of different numbers in the config file and see which ones are best suited for checking that wide range of result files.

I suggest that we merge this PR first, though. I would be inclined to merge quickly and start getting data as quickly as we can, rather than trying to get it right from now, especially since we don't have data for realistic runs.

@qinheping here are my thoughts on which numbers to use:

I've tried a few experiments with CI and locally. I get a lot less variance locally, often all benchmarks (or all but one) have a variance <10%. This is when comparing identical Kanis.

In CI, the numbers that @adpaco-aws seem to work well for now. I do think it would be a good idea to optimize these numbers, but I would prefer to see what the range is on realistic PRs---that is, PRs that actually change the implementation of Kani and so cause and actual performance difference.

What I propose:

* In a future PR, I'll save the results.yaml file as an artifact. This will allow me to download the results of several runs over the last 30 days.

* `benchcomp visualize` can be used locally on a results.yaml file, without re-running the benchmarks. So if we download a lot of results.yaml files, we can try lots of different numbers in the config file and see which ones are best suited for checking that wide range of result files.

I suggest that we merge this PR first, though. I would be inclined to merge quickly and start getting data as quickly as we can, rather than trying to get it right from now, especially since we don't have data for realistic runs.

Sounds great! Thank you @karkhaz.
Yes, we also want to save the results from realistic runs and review them periodically to detect accumulating performance regression.

Got convinced that this is a start, but I do maintain that we need to dig deeper to figure out what the sources of performance variability are.

I agree. I think we should merge the PR but only make it required once we figure that out.