isa-bench
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
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
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.