Table of Contents
- Apalache Benchtests
- Installation and development
- Adding benchmarks
- Running the benchmarks
The benchmarking framework is not currently packaged separately from this repository so installing the framework locally currently means cloning this repo:
git clone [email protected]:informalsystems/apalache-bench.gitThe Apalache benchmarking framework is written as two sbt plugins.
sbt-benchexecis defined inproject/sbt-benchexecand provides an eDSL for generating benchexec definitions and sbt tasks for running benchexec and generating reports from the results.sbt-apalacheis defined inproject/sbt-apalacheand provides tasks for fetching and installing released apalche, either from its releases or by building from source.
The benchmarks can be organized into sbt sub-projects. Each project consists of
a directory holding a build.sbt file and the source code used to define the
specs to be run in the benchmarks. For an example of a working project, see the
performance directory.
Report data are stored in src/site/. The assets in this directory
are then served from github pages.
The top-level configuration for the benchmarks run from this repo is the build.sbt file.
This configures
- the sbt projects that define subsets of thematically related projects (e.g.,
the
performancebenchmarks) - some data necessary for publishing the reports to github pages
- the list of
benchmarksLongitudinalVersions, which are the versions of Apalche to include in the "Longitudinal Comparison of Experiments" reports.
Each project also has a build.sbt file in its directory. This is where the
definition of the tasks to run for the benchmarks are defined. For an example,
see [performance/build.sbt]. For documentation on how to add a new benchmark,
see adding benchmarks.
Benchmarks are added to a projects by adding a benchmark
suite to the sequence of benchmarks defined in the project's build.sbt
configuration. Here is an annotated example:
// The eDSL for defining benchmark executions
import BenchExecDsl._
// The sbt-benchexec plugin
enablePlugins(BenchExec)
// The set of benchmark suites that are part of this project
benchmarks ++= Seq(
Bench.Suite(
name = "suite-name",
// The sub tasks that are collected as part of this suite
runs = Seq(
// A collection of commands that all run on the same specification files
Bench.Runs(
// The name for the collection of commands
"APAEWD840",
timelimit = "3h",
// The commands to run (all called with apalache)
cmds = Seq(
Cmd(
// a name for the command configuration
"no init",
// The options to pass to apalache-mc
Opt("check"),
Opt("--inv", "InvAndTypeOK"), // passed as --inv=InvAndTypeOk
Opt("--length", 0),
Opt("--cinit", "ConstInit10"),
),
Cmd(
"--init=InvAndTypeOK",
Opt("check"),
Opt("--init", "InvAndTypeOK"),
Opt("--inv", "InvAndTypeOK"),
Opt("--length", 1),
Opt("--cinit", "ConstInit10"),
),
),
// The set of files to run each command on
tasks = Seq(Tasks("APAEWD840", Seq("ewd840/APAEWD840.tla"))),
// Optional group ID used to group results into disjoint sets
// in reports. Most benchmarks can simply ommit the group id.
group = Some("group-id")
),
)For a complete working example, see performance/build.sbt.
The benchmarks run against the latest main branch every weekend, and the
results are published. The following instructions are for if you want to
manually run the benchmarks.
NOTE: The Apalache benchmarking framework is only compatible with Apalache
>= v0.22.0.
-
Navigate to https://github.com/informalsystems/apalache-bench/actions/workflows/main.yml
-
Select
Run workflowand fill in the fields:
- To benchmark a released version, prefix the version tag with
@. E.g., to benchmark version0.24.0, supply@v0.24.0. - To benchmark a branch or commit, prefix the identifier with
#. E.g., to benchmark branchmy-feature, supply#my-feature. - You can run a specific set of suites, by supply a comma separated list of
suite names. E.g.,
001indinv-apalache,010encoding-SetAdd.
- To benchmark a released version, prefix the version tag with
sbt benchmarksReportPrefix the tag corresponding to the version with @. E.g.:
sbt 'set apalacheVersion := "@v0.22.0"; benchmarksReport'Prefix the branch name or commit ref with #. E.g.:
# For a branch
sbt 'set apalacheVersion := "#main"; benchmarksReport'
# For a specific commit
sbt 'set apalacheVersion := "#c1ed9ef1596bb6e8df6b4f77a8335448eebfa80f"; benchmarksReport'apalache-bench will try not to rebuild and relink Apalache if nothing has
changed. You can ensure that the build and linking of the configured Apalache is
performed via
sbt apalacheEnableVersionThis will ensure the configured Apalche version is downloaded, built, and that the executable is available for subsequent benchmarks in that shell session.
The general recipe for running benchmarks and generating reports for a specific project is:
sbt {project}/benchmarksReportE.g., To run the benchmarks and produce reports for the performance project, run:
sbt performance/benchmarksReportYou can limit the benchmarks run to specific bench suites by setting
ThisBuild/benchmarksFilterExperiments to a set with the names of the
experiments to run. E.g., to only run benchmark suites named "foo" and "bar",
you can run:
sbt 'set ThisBuild/benchmarksFilterExperiments := Set("foo", "bar")' performance/benchmarksReportTo generate the site that gather and presents the report data, run
sbt site/benchmarksLongitudinalUpdate site/benchmarksIndexUpdate makeSiteThis will update the files in ./src/site. Open ./src/site/index.html in your browser to preview the site locally.
This is done via our GitHub workflow. See .github/workflows/main.yml.
The files generated by Apalache for each run, including the detailed.log, are
saved into site/reports/${verion}/${experiment}/${name}.files, where
versionis the version of Apalache that was benchmarkedexperimentis the name of the experiment runnameis the name and timestamp of the particular set of tasks executed
Enable debug logging in benchexec by setting the environment variable
BENCH_DEBUG=true