initial fixes still required #1
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: run-tests | |
| on: | |
| push: | |
| pull_request: | |
| branches: [ "master" ] | |
| jobs: | |
| unit-tests: | |
| runs-on: ubuntu-latest | |
| defaults: | |
| run: | |
| shell: bash | |
| container: | |
| image: silkeh/clang:19 | |
| options: --user root | |
| steps: | |
| - name: Install deps | |
| run: apt update && apt install -y git ninja-build valgrind libboost-context-dev libgflags-dev libclang-19-dev | |
| - name: Check out repository code | |
| uses: actions/checkout@v4 | |
| - name: Build | |
| run: | | |
| cmake -G Ninja -B build -DCMAKE_BUILD_TYPE=Debug | |
| cmake --build build --target lin_check_test | |
| - name: Run lin check test | |
| run: ./build/test/runtime/lin_check_test | |
| verifying-test-debug: | |
| runs-on: ubuntu-latest | |
| defaults: | |
| run: | |
| shell: bash | |
| container: | |
| image: silkeh/clang:19 | |
| options: --user root | |
| steps: | |
| - name: Install deps | |
| run: | | |
| apt update && apt install -y git ninja-build valgrind libgoogle-glog-dev libsnappy-dev protobuf-compiler libboost-context-dev pkg-config libcapstone-dev libclang-19-dev && \ | |
| git clone https://github.com/Kirillog/syscall_intercept.git && \ | |
| cmake syscall_intercept -G Ninja -B syscall_intercept/build -DCMAKE_INSTALL_PREFIX=/usr -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=clang && \ | |
| cmake --build syscall_intercept/build --target install | |
| - name: Check out repository code | |
| uses: actions/checkout@v4 | |
| - name: Build | |
| run: | | |
| cmake -G Ninja -B build -DCMAKE_BUILD_TYPE=Debug | |
| cmake --build build --target verifying/targets/nonlinear_queue verifying/blocking/nonlinear_mutex verifying/blocking/simple_mutex | |
| # Does not work, see issue: https://github.com/ITMO-PTDC-Team/LTest/issues/13 | |
| # - name: Run nonlinear_mutex with random strategy | |
| # run: | | |
| # LD_PRELOAD=build/syscall_intercept/libpreload.so ./build/verifying/blocking/nonlinear_mutex --strategy random || error_code=$? | |
| # if [ "${error_code}" -ne 1 ]; then | |
| # exit 1 | |
| # fi | |
| # - name: Run nonlinear_mutex with pct strategy | |
| # run: | | |
| # LD_PRELOAD=build/syscall_intercept/libpreload.so ./build/verifying/blocking/nonlinear_mutex --strategy pct --tasks 10 --rounds 240 || error_code=$? | |
| # if [ "${error_code}" -ne 1 ]; then | |
| # exit 1 | |
| # fi | |
| - name: Run simple_mutex with random strategy | |
| run: | | |
| LD_PRELOAD=build/syscall_intercept/libpreload.so ./build/verifying/blocking/simple_mutex --strategy random || error_code=$? | |
| if [ "${error_code}" -ne 1 ]; then | |
| exit 1 | |
| fi | |
| # Does not work, see issue: https://github.com/ITMO-PTDC-Team/LTest/issues/12 | |
| # - name: Run simple_mutex with pct strategy | |
| # run: | | |
| # LD_PRELOAD=build/syscall_intercept/libpreload.so ./build/verifying/blocking/simple_mutex --strategy pct --tasks 10 --rounds 240 || error_code=$? | |
| # if [ "${error_code}" -ne 1 ]; then | |
| # exit 1 | |
| # fi | |
| - name: Run nonlinear_queue with random strategy | |
| run: | | |
| ./build/verifying/targets/nonlinear_queue --tasks 4 --rounds 100000 --strategy random --switches 1 || error_code=$? | |
| if [ "${error_code}" -ne 1 ]; then | |
| exit 1 | |
| fi | |
| - name: Run nonlinear_queue with pct strategy | |
| run: | | |
| ./build/verifying/targets/nonlinear_queue --strategy pct --tasks 10 --rounds 240 || error_code=$? | |
| if [ "${error_code}" -ne 1 ]; then | |
| exit 1 | |
| fi | |
| - name: Run nonlinear_queue with random strategy (minimization) | |
| run: | | |
| ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy random --minimize || error_code=$? | |
| if [ "${error_code}" -ne 1 ]; then | |
| exit 1 | |
| fi | |
| - name: Run nonlinear_queue with pct strategy (minimization) | |
| run: | | |
| ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy pct --minimize || error_code=$? | |
| if [ "${error_code}" -ne 1 ]; then | |
| exit 1 | |
| fi | |
| verifying-test-release: | |
| runs-on: ubuntu-latest | |
| defaults: | |
| run: | |
| shell: bash | |
| container: | |
| image: silkeh/clang:19 | |
| options: --user root | |
| steps: | |
| - name: Install deps | |
| run: | | |
| apt update && apt install -y git ninja-build valgrind libgoogle-glog-dev libsnappy-dev protobuf-compiler libboost-context-dev pkg-config libcapstone-dev libclang-19-dev && \ | |
| git clone https://github.com/Kirillog/syscall_intercept.git && \ | |
| cmake syscall_intercept -G Ninja -B syscall_intercept/build -DCMAKE_INSTALL_PREFIX=/usr -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=clang && \ | |
| cmake --build syscall_intercept/build --target install | |
| - name: Check out repository code | |
| uses: actions/checkout@v4 | |
| - name: Build | |
| run: | | |
| cmake -G Ninja -B build -DCMAKE_BUILD_TYPE=Release | |
| cmake --build build --target verifying/targets/nonlinear_queue verifying/targets/nonlinear_ms_queue verifying/targets/nonlinear_treiber_stack verifying/targets/nonlinear_set verifying/targets/nonlinear_queue_with_custom_rounds verifying/blocking/nonlinear_mutex verifying/blocking/simple_mutex | |
| - name: Run nonlinear_queue_with_custom_rounds with random strategy | |
| run: | | |
| ./build/verifying/targets/nonlinear_queue_with_custom_rounds --rounds 0 --exploration_runs 100000 --strategy random || error_code=$? | |
| if [ "${error_code}" -ne 1 ]; then | |
| exit 1 | |
| fi | |
| - name: Run nonlinear_queue_with_custom_rounds with pct strategy | |
| run: | | |
| ./build/verifying/targets/nonlinear_queue_with_custom_rounds --rounds 0 --exploration_runs 100000 --strategy pct || error_code=$? | |
| if [ "${error_code}" -ne 1 ]; then | |
| exit 1 | |
| fi | |
| - name: Run nonlinear_queue with random strategy (minimization) | |
| run: | | |
| ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy random --minimize || error_code=$? | |
| if [ "${error_code}" -ne 1 ]; then | |
| exit 1 | |
| fi | |
| - name: Run nonlinear_queue with pct strategy (minimization) | |
| run: | | |
| ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy pct --minimize || error_code=$? | |
| if [ "${error_code}" -ne 1 ]; then | |
| exit 1 | |
| fi | |
| - name: Run nonlinear_ms_queue with random strategy (minimization) | |
| run: | | |
| ./build/verifying/targets/nonlinear_ms_queue --tasks 40 --rounds 100000 --strategy random --minimize || error_code=$? | |
| if [ "${error_code}" -ne 1 ]; then | |
| exit 1 | |
| fi | |
| - name: Run nonlinear_ms_queue with pct strategy (minimization) | |
| run: | | |
| ./build/verifying/targets/nonlinear_ms_queue --tasks 40 --rounds 100000 --strategy pct --minimize || error_code=$? | |
| if [ "${error_code}" -ne 1 ]; then | |
| exit 1 | |
| fi | |
| - name: Run nonlinear_treiber_stack with random strategy (minimization) | |
| run: | | |
| ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy random --minimize || error_code=$? | |
| if [ "${error_code}" -ne 1 ]; then | |
| exit 1 | |
| fi | |
| - name: Run nonlinear_treiber_stack with pct strategy (minimization) | |
| run: | | |
| ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy pct --minimize || error_code=$? | |
| if [ "${error_code}" -ne 1 ]; then | |
| exit 1 | |
| fi | |
| - name: Run nonlinear_set with random strategy (minimization) | |
| run: | | |
| ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy random --minimize || error_code=$? | |
| if [ "${error_code}" -ne 1 ]; then | |
| exit 1 | |
| fi | |
| - name: Run nonlinear_set with pct strategy (minimization) | |
| run: | | |
| ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy pct --minimize || error_code=$? | |
| if [ "${error_code}" -ne 1 ]; then | |
| exit 1 | |
| fi |