Skip to content

ITMO-PTDC-Team/LTest

Repository files navigation

Ltest

LTest (Linearizability Test) is a framework for writing tests for concurrent data structures. It allows you to write complex tests in a declarative way.

LTest instruments your data structure’s methods with context switches, executes these methods in a single thread, and produces different interleavings due to the context switches. Later, the obtained execution is checked for linearizability.

Test examples can be found in the verifying directory.

Build

It is not recommended to try install all required dependencies locally in your system. Build docker image and run container:

./scripts/rund.sh

Run

  • Run for release:
cmake -G Ninja -B build -DCMAKE_BUILD_TYPE=Release
  • Run unit tests:
cmake --build build --target lin_check_test
  • Run verify:
cmake --build build --target verifying/targets/nonlinear_queue && ./build/verifying/targets/nonlinear_queue --tasks 10 --rounds 240 --strategy pct

Blocking

Verifying of blocking data structures uses syscall interception, so we need to build and install special hooks, that are required to be load through LD_PRELOAD:

cmake --build build --target verifying/blocking/nonlinear_mutex && LD_PRELOAD=build/syscall_intercept/libpreload.so ./build/verifying/blocking/nonlinear_mutex

Some blocking targets depends on boost and folly. For them you need to install boost and folly locally, and provide ./boost and ./folly symbolic links at the root of the project, then we can lincheck these targets.

About

LTest is a framework for verifying the linearizability of C++ data structures.

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Contributors 5

Languages