Apalache Benchtests

Table of Contents

• Apalache Benchtests
• Installation and development
  • Prerequisites
  • Installation
  • Organization
    • Apalache benchmarking framework
    • Benchmark Projects
    • Reports
    • Configuration
• Adding benchmarks
• Running the benchmarks
  • Via GitHub actions
  • Via command-line
    • For all projects
    • For a specific build of apalache
      • For a released version
      • For a branch or commit
    • For a specific project
    • For a particular subset of bench suites
    • Generating reports and the website
      • Updating the reports and site content
      • Publishing the site to gh-pages
    • Debugging
      • Debugging tasks
      • Debugging benchexec

Installation and development

Prerequisites

• sbt
• benchexec
• direnv or run source ./.envrc

Installation

The benchmarking framework is not currently packaged separately from this repository so installing the framework locally currently means cloning this repo:

git clone git@github.com:informalsystems/apalache-bench.git

Organization

Apalache benchmarking framework

The Apalache benchmarking framework is written as two sbt plugins.

• sbt-benchexec is defined in project/sbt-benchexec and provides an eDSL for generating benchexec definitions and sbt tasks for running benchexec and generating reports from the results.
• sbt-apalache is defined in project/sbt-apalache and provides tasks for fetching and installing released apalche, either from its releases or by building from source.

Benchmark Projects

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.

Reports

Report data are stored in src/site/. The assets in this directory are then served from github pages.

Configuration

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 performance benchmarks)
• 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.

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.

Running the benchmarks

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.

Via GitHub actions

• Navigate to https://github.com/informalsystems/apalache-bench/actions/workflows/main.yml

• Select Run workflow and fill in the fields:

  

  • To benchmark a released version, prefix the version tag with @. E.g., to benchmark version 0.24.0, supply @v0.24.0.
  • To benchmark a branch or commit, prefix the identifier with #. E.g., to benchmark branch my-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.

Via command-line

For all projects

sbt benchmarksReport

For a specific build of apalache

For a released version

Prefix the tag corresponding to the version with @. E.g.:

sbt 'set apalacheVersion := "@v0.22.0"; benchmarksReport'

For a branch or commit

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'

Build and link a version of Apalache

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 apalacheEnableVersion

This will ensure the configured Apalche version is downloaded, built, and that the executable is available for subsequent benchmarks in that shell session.

For a specific project

The general recipe for running benchmarks and generating reports for a specific project is:

sbt {project}/benchmarksReport

E.g., To run the benchmarks and produce reports for the performance project, run:

sbt performance/benchmarksReport

For a particular subset of bench suites

You 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/benchmarksReport

Generating reports and the website

Updating the reports and site content

To generate the site that gather and presents the report data, run

sbt site/benchmarksLongitudinalUpdate site/benchmarksIndexUpdate makeSite

This will update the files in ./src/site. Open ./src/site/index.html in your browser to preview the site locally.

Publishing the site to gh-pages

This is done via our GitHub workflow. See .github/workflows/main.yml.

Debugging

Debugging tasks

The files generated by Apalache for each run, including the detailed.log, are saved into site/reports/${verion}/${experiment}/${name}.files, where

• version is the version of Apalache that was benchmarked
• experiment is the name of the experiment run
• name is the name and timestamp of the particular set of tasks executed

Debugging benchexec

Enable debug logging in benchexec by setting the environment variable

BENCH_DEBUG=true