Continuous Verification #123
This file contains 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: "Continuous Verification" | |
| on: | |
| schedule: | |
| - cron: "0 0 * * 0" | |
| pull_request: | |
| paths: | |
| - "tla/**" | |
| - "src/consensus/**" | |
| - ".github/workflows/ci-verification.yml" | |
| workflow_dispatch: | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| permissions: | |
| actions: read | |
| contents: read | |
| security-events: write | |
| jobs: | |
| model-checking-consistency: | |
| name: Model Checking - Consistency | |
| runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub] | |
| container: | |
| image: mcr.microsoft.com/azurelinux/base/core:3.0 | |
| options: --user root --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE | |
| steps: | |
| - name: "Checkout dependencies" | |
| shell: bash | |
| run: | | |
| gpg --import /etc/pki/rpm-gpg/MICROSOFT-RPM-GPG-KEY | |
| tdnf -y update | |
| tdnf -y install ca-certificates git | |
| - uses: actions/checkout@v4 | |
| - name: Install TLC dependencies | |
| run: | | |
| tdnf install -y jre wget | |
| python3 tla/install_deps.py --skip-apt-packages | |
| - run: cd tla && ./tlc.py mc consistency/MCSingleNode.tla | |
| - run: cd tla && ./tlc.py mc consistency/MCSingleNodeReads.tla | |
| - run: cd tla && ./tlc.py mc consistency/MCMultiNode.tla | |
| - run: cd tla && ./tlc.py mc consistency/MCMultiNodeReads.tla | |
| - run: cd tla && ./tlc.py mc consistency/MCMultiNodeReadsAlt.tla | |
| - name: Upload TLC traces | |
| uses: actions/upload-artifact@v4 | |
| if: ${{ failure() }} | |
| with: | |
| name: tlc-model-checking-consistency | |
| path: | | |
| tla/consistency/*_TTrace_*.tla | |
| tla/*.json | |
| counterexamples-consistency: | |
| name: Counterexamples - Consistency | |
| runs-on: ubuntu-latest | |
| defaults: | |
| run: | |
| working-directory: tla | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install TLC dependencies | |
| run: | | |
| sudo apt update | |
| sudo apt install -y default-jre | |
| python3 install_deps.py | |
| - run: ./tlc_debug.sh --config consistency/MCSingleNodeCommitReachability.cfg mc consistency/MCSingleNodeReads.tla | |
| - run: ./tlc_debug.sh --config consistency/MCMultiNodeCommitReachability.cfg mc consistency/MCMultiNodeReads.tla | |
| - run: ./tlc_debug.sh --config consistency/MCMultiNodeInvalidReachability.cfg mc consistency/MCMultiNodeReads.tla | |
| - run: ./tlc_debug.sh --config consistency/MCMultiNodeReadsNotLinearizable.cfg mc consistency/MCMultiNodeReads.tla | |
| simulation-consistency: | |
| name: Simulation - Consistency | |
| runs-on: ubuntu-latest | |
| defaults: | |
| run: | |
| working-directory: tla | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install TLC dependencies | |
| run: | | |
| sudo apt update | |
| sudo apt install -y default-jre | |
| python3 install_deps.py | |
| - run: ./tlc.py sim --num 500 --depth 50 consistency/MultiNodeReads.tla | |
| - name: Upload TLC traces | |
| uses: actions/upload-artifact@v4 | |
| if: ${{ failure() }} | |
| with: | |
| name: tlc-simulation-consistency | |
| path: | | |
| tla/consistency/*_TTrace_*.tla | |
| tla/*.json | |
| model-checking-consensus: | |
| name: Model Checking - Consensus | |
| runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub] | |
| container: | |
| image: mcr.microsoft.com/azurelinux/base/core:3.0 | |
| options: --user root --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE | |
| steps: | |
| - name: "Checkout dependencies" | |
| shell: bash | |
| run: | | |
| gpg --import /etc/pki/rpm-gpg/MICROSOFT-RPM-GPG-KEY | |
| tdnf -y update | |
| tdnf -y install ca-certificates git | |
| - uses: actions/checkout@v4 | |
| - name: Install TLC dependencies | |
| run: | | |
| tdnf install -y jre wget | |
| python3 tla/install_deps.py --skip-apt-packages | |
| - run: cd tla && ./tlc.py mc consensus/MCabs.tla | |
| - run: cd tla && ./tlc.py --trace-name 1C2N mc --term-count 2 --request-count 2 --raft-configs 1C2N consensus/MCccfraft.tla | |
| - run: cd tla && ./tlc.py --trace-name 1C3N mc --term-count 0 --request-count 3 --raft-configs 1C3N consensus/MCccfraft.tla | |
| - name: Upload TLC traces | |
| uses: actions/upload-artifact@v4 | |
| if: ${{ failure() }} | |
| with: | |
| name: tlc-model-checking-consensus | |
| path: | | |
| tla/consensus/*_TTrace_*.tla | |
| tla/*.json | |
| simulation-consensus: | |
| name: Simulation - Consensus | |
| runs-on: ubuntu-latest | |
| defaults: | |
| run: | |
| working-directory: tla | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install TLC dependencies | |
| run: | | |
| sudo apt update | |
| sudo apt install -y default-jre | |
| python3 install_deps.py | |
| - run: ./tlc.py sim consensus/SIMccfraft.tla | |
| - name: Upload TLC traces | |
| uses: actions/upload-artifact@v4 | |
| if: ${{ failure() }} | |
| with: | |
| name: tlc-simulation-consensus | |
| path: | | |
| tla/consensus/*_TTrace_*.tla | |
| tla/*.json | |
| trace-validation-consensus: | |
| name: Trace Validation - Consensus | |
| runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub] | |
| container: | |
| image: mcr.microsoft.com/azurelinux/base/core:3.0 | |
| options: --user root --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE | |
| steps: | |
| - name: "Checkout dependencies" | |
| shell: bash | |
| run: | | |
| gpg --import /etc/pki/rpm-gpg/MICROSOFT-RPM-GPG-KEY | |
| tdnf -y update | |
| tdnf -y install ca-certificates git | |
| - uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: Install TLC dependencies | |
| run: | | |
| tdnf install -y jre wget | |
| python3 tla/install_deps.py --skip-apt-packages | |
| - name: "Install dependencies" | |
| shell: bash | |
| run: | | |
| set -ex | |
| ./scripts/setup-ci.sh | |
| # Parallel | |
| wget https://ftp.gnu.org/gnu/parallel/parallel-latest.tar.bz2 | |
| tar -xjf parallel-latest.tar.bz2 | |
| cd $(ls | grep 'parallel' | grep -v 'tar' | grep -v 'rpm') | |
| ./configure && make && make install | |
| - name: "Build" | |
| run: | | |
| set -ex | |
| git config --global --add safe.directory /__w/CCF/CCF | |
| mkdir build | |
| cd build | |
| cmake -L -GNinja .. -DCMAKE_BUILD_TYPE=Debug -DVERBOSE_LOGGING=ON -DCOMPILE_TARGET=virtual -DCCF_RAFT_TRACING=ON | |
| ninja raft_driver | |
| shell: bash | |
| - name: "Test" | |
| run: | | |
| set -x | |
| cd build | |
| rm -rf /github/home/.cache | |
| mkdir -p /github/home/.cache | |
| ./tests.sh -VV --timeout --no-compress-output -T Test -L raft_scenario | |
| shell: bash | |
| - name: Run trace validation | |
| run: | | |
| set -x | |
| cd tla/ | |
| mkdir -p traces/consensus | |
| mv ../build/consensus traces/ | |
| parallel './tlc.py --workers 1 --dot --trace-name {} tv --ccf-raft-trace {} consensus/Traceccfraft.tla' ::: $(ls traces/consensus/*.ndjson) | |
| shell: bash | |
| - name: Upload artifacts. | |
| uses: actions/upload-artifact@v4 | |
| if: always() | |
| with: | |
| name: tlc-trace-validation-consensus | |
| path: | | |
| tla/traces/* |