Fix support for running tlc benchmarks

[shonfeder]

At some point we lost support for running TLC. We should restore it by fixing the TODO in the tool_cmd function in https://github.com/informalsystems/apalache-tests/tree/master/scripts/mk-run.py

[lemmy]

@shonfeder Is TLC support still of interest? Also, how reliable are the results obtained by running the benchmarks on shared Github action instances?

[shonfeder]

Hi!

Is TLC support still of interest

Afaik, we have no pressing need for this, but we want to track it for the long term. IMO, I'd not consider integrating it into the current framework, but would instead subordinate this functionality to the longerterm plan to rewrite the benchmarking framework.

how reliable are the results obtained by running the benchmarks on shared Github action instances?

Probably not very. I don't think we'd use these results for scientific publication, but they are useful as a sanity check lest we introduced a change that caused a huge regression in performance.

[lemmy]

FWIW: The now-defunct performance/scalability test infrastructure for TLC used sponsored, bare-metal instances from https://metal.equinix.com
An integration into Github actions of Equinix (or another bare-metal provider) could be done through self-hosted runners.

[shonfeder]

Thanks!

[lemmy]

FYI: TLC now has this with https://github.com/tlaplus/tlaplus/actions/workflows/perf.yml, which runs a number of benchmarks upon request on a bare-metal instance hooked into Github actions via a self-hosted runner.