informalsystems / apalache-tests Goto Github PK

Towards informalsystems/apalache#349

We want to run some benchmarks that will take upwards of 24 hours. We cannot do this on GitHub hosted runners, but it looks easy to connect self-hosted runners. For a start, we are considering digital ocean droplets, as per the walkthrough here: https://digitaloceancode.com/deploying-self-hosted-runners-for-github-actions/ and we might graduate to our hardware if it seems worth it.

This repo hasn't seen updates in a while, and we keep running into maintenance burden (dependabot alerts and other breakage).

As discussed on Slack, we should probably archive it, to mark it as unsupported.
I don't have the necessary privileges; @konnov @shonfeder, maybe one of you?

Towards informalsystems/apalache#349

Probably the easiest way to do this is to the run the benchmarks inside of the apalache/mc:unstable image.

See https://github.com/informalsystems/apalache-tests/pull/75/files#diff-cfcf6d8feddb8c1221c23eab56846338cf8ac2984ace1cd2eaf499e3be44ea4c

There seems to be a few issues with the Raft spec in this repo.

(1) The quorums in the APAraft.tla should be subsets of the servers but they are not.

(2) The invariant OneLeader should be violated at some point. It is possible for multiple servers to believe themselves to be leaders so long as they are in different terms.

(3) Apalache (version: 0.22.1) will not check this spec without modification due to the following issue:

Assignment error: APAraft.tla:545:15-545:51: Manual assignment is spurious, votedFor is already assigned!

Once approved, propagate informalsystems/apalache-bench#111 to this repo.

We can't really get accurate indication of the relative running time if we don't track info about the computer power given to the benchmark runs.

Currently, we have to manually position the source code for every tested version in a hard-coded location and manually add a new make target for each version that should be tested. It would be helpful to set up the build along these lines

• we configure the version numbers we want to test
• this is fed to a build and test matrix that will take care of
  • obtaining the executables (ideally from pre-built binaries or docker images, instead of having to rebuild from source -- since the build is already covered in apalache's CI)
  • running all the benchmarks
  • posting the benchmarks to the desired location

Towards informalsystems/apalache#349

• cron job will run the benchmarks against the latest snapshot every Saturday
• manual job will allow specifying the version number to run against, which will look for a matching Apalache version

The CI task should present the report as an opened PR that adds the new results to our past results

Requires #18

But we should figure out the benchmark licenses first

Extend these benchmarks with the Informal specifications.

Transferred form informalsystems/apalache#349

We have discussed moving the build system (but not the specs) to the main apalache repo.

Benefits:

• Possibility of integrating CI easier
• All code in one place
• Would make it slightly easier to build from source
• Essentially moves us towards a monorepo development practice

Draw backs:

• Introduces tech debt (if we don't do a re-write first)
• Could encourage tighter coupling between systems that don't really need to be tightly coupled
• Takes some labor

Requirements

• Would need to rework the build system to pull in the the specs from a remote repo.

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

Currently, all the tests are assumed to report NoError. Add configurations, where errors are expected.