On recovery, set UVM descriptor SVN to minimum of existing KV value and startup endorsements #5437
Workflow file for this run
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: "Long Verification" | |
| on: | |
| pull_request: | |
| types: | |
| - labeled | |
| - synchronize | |
| - opened | |
| - reopened | |
| schedule: | |
| - cron: "0 0 * * 0" | |
| workflow_dispatch: | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} | |
| permissions: read-all | |
| jobs: | |
| model-checking-with-atomic-reconfig-consensus: | |
| name: Model Checking With Atomic Reconfig - Consensus | |
| if: &check_trigger_conditions ${{ (github.event.action == 'labeled' && github.event.label.name == 'run-long-verification') || (github.event.action != 'labeled' && contains(github.event.pull_request.labels.*.name, 'run-long-verification')) || github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }} | |
| runs-on: | |
| [ | |
| self-hosted, | |
| 1ES.Pool=gha-vmss-d16av5-ci, | |
| "JobId=long_mc_atomic_reconfig-${{ github.run_id }}-${{ github.run_number }}-${{ github.run_attempt }}", | |
| ] | |
| 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@v6 | |
| - name: Install TLC dependencies | |
| run: | | |
| tdnf install -y jre wget | |
| python3 tla/install_deps.py | |
| - run: cd tla && ./tlc.py --trace-name 2C2N mc --term-count 2 --request-count 0 --raft-configs 2C2N --disable-check-quorum consensus/MCccfraft.tla | |
| - name: Upload TLC traces | |
| uses: actions/upload-artifact@v7 | |
| if: ${{ failure() }} | |
| with: | |
| name: tlc-model-checking-with-atomic-reconfig-consensus | |
| path: | | |
| tla/consensus/*_TTrace_*.tla | |
| tla/*.json | |
| model-checking-with-reconfig-consensus: | |
| name: Model Checking With Reconfig - Consensus | |
| if: *check_trigger_conditions | |
| runs-on: | |
| [ | |
| self-hosted, | |
| 1ES.Pool=gha-vmss-d16av5-ci, | |
| "JobId=long_mc_reconfig-${{ github.run_id }}-${{ github.run_number }}-${{ github.run_attempt }}", | |
| ] | |
| 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@v6 | |
| - name: Install TLC dependencies | |
| run: | | |
| tdnf install -y jre wget | |
| python3 tla/install_deps.py | |
| - run: cd tla && ./tlc.py --trace-name 3C2N mc --term-count 2 --request-count 0 --raft-configs 3C2N --disable-check-quorum consensus/MCccfraft.tla | |
| - name: Upload TLC traces | |
| uses: actions/upload-artifact@v7 | |
| if: ${{ failure() }} | |
| with: | |
| name: tlc-model-checking-with-reconfig-consensus | |
| path: | | |
| tla/consensus/*_TTrace_*.tla | |
| tla/*.json | |
| simulation-consensus: | |
| name: Simulation - Consensus | |
| if: *check_trigger_conditions | |
| runs-on: ubuntu-latest | |
| defaults: | |
| run: | |
| working-directory: tla | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - run: | | |
| sudo apt update | |
| sudo apt install -y default-jre wget | |
| python3 install_deps.py | |
| - run: ./tlc.py sim --max-seconds 3000 --depth 500 consensus/SIMccfraft.tla | |
| - name: Upload TLC traces | |
| uses: actions/upload-artifact@v7 | |
| if: ${{ failure() }} | |
| with: | |
| name: tlc-simulation-consensus | |
| path: | | |
| tla/consensus/*_TTrace_*.tla | |
| tla/*.json |