Automate build and test for the various benchmarked versions about apalache-tests HOT 6 CLOSED

Cool. Then we can totally rely on docker images for running the tests. We can even build an unstable image every time a build runs in travis.

from apalache-tests.

Towards apalache-mc/apalache#182 and this issue, I've roughed out the following plan:

Instead of building each version from source, we'll can use the published docker images. We can use one script as a function from a docker image to benchmark data. A second script to take that data into a human-friendly report, and a third to take a set data and produce a summarizing report.

In types:

type exec = Docker_image
type data = CSV
type report = Markdown_file

val benchmark : exec     -> data
val report    : data     -> report
val summary   : data set -> report
val run_tests : exec set -> (reports * report)

We can then parallelize the execution by running a build matrix in our CI for each version we want to benchmark.

The implementation steps are roughly:

• Redesign the current workflows to run a single benchmark in the docker image containing the built apalache instance
• Tweak scripts to save the results to a database (which is just the current dir of CSVs)
• Tweak scripts to take a version number and extract reports from the CSV data.
• Set up CI to run the benchmarks.

from apalache-tests.

Instead of building each version from source, we'll use the published docker images

I like that. Do you know how big is the performance penalty when running images in docker?

from apalache-tests.

I like that. Do you know how big is the performance penalty when running images in docker?

It seems like, in principle, the performance penalty should be negligible, at least according to this nice SO answer. This follows from containerization just being an abstraction over the kernel services, rather than incurring the costs associated with virtualization. However, in practice it looks like it might cause a measure reduction on the order of single percentage points.

I can run some empirical tests tomorrow to see how Apalache performs on my machine in and out of containers.

One of my working assumptions here is that the important thing in the benchmarks is the relative change in a known context. Since we don't seem to mention hardware specs (or VPS specs) anywhere obvious here, I assumed the underlying system running the benchmarks isn't relevant to what we're testing. However, if we're really aiming benchmarking on the specs of some hardware or optimal system, then the containerization approach probably shouldn't be pursued!

Thoughts?

from apalache-tests.

Sweet. I'll move forward with this, then see if I can leverage any learnings to bring back into the apalache CI pipeline.

from apalache-tests.

Closed by #22

from apalache-tests.