isa-bench

Warning

isa-bench is at the moment under active development. Documentation and API stabilization is still not done.

NOTE: isa-bench initially contained isalink with isalink.IsaClient and the parsers being factored out for use in ISM.

isa-bench is a k6-based stress test for isabelle server compatible services. It is based on isalink and provides a k6 extension which wraps isalink.IsaClient.

The main use case will be stress testing ISM for profiling and debugging.

Usage

Info

You need nix and/ or xk6 installed to use isa-bench. You also need access to the isalink git repository.

The invocation is a bit cumbersome at the moment, I will address this asap.

Preparation

  • Build k6 with extensions (output in ./bin/): nix develop -c make build
  • Setup test theory: sh scripts/bootstrap-tmp.sh

Run Test

The test host needs to be specified via environment variables:

  • ISA_HOST: Server host IP, e.g., 10.20.77.1
  • ISA_PORT: Server host port, e.g., 8080
  • ISA_PASSWORD: Server host password, e.g., anything

Info

You can pass these variables via the -e option when calling k6. For example: ./bin/k6 run -e ISA_HOST=10.20.77.1 -e ISA_PORT=8080 -e ISA_PASSWORD=anything ...

With these ready you can call the k6 binary (e.g., with 5 virtual users and 20 iterations): ./bin/k6 run -u 5 -i 20 test-state-with-delay.js

The benchmarking script, test-state-with-delay.js, can be exchanges with another script. Please note that the number of virtual users (VUs) is only representative of the number of concurrent users. They may not be synchronized in, e.g., dispatching use_theories calls or starting/ stopping sessions.