diff --git a/.github/workflows/README.md b/.github/workflows/README.md index 25f3f964a37..0651ec5b625 100644 --- a/.github/workflows/README.md +++ b/.github/workflows/README.md @@ -16,7 +16,7 @@ Triggered on every commit on `main`, but not on PR builds because the setup requ File: `bencher.yml` 3rd party dependencies: `bencherdev/bencher@main` -# CI Containers GHCR +# Continuous Integration Containers GHCR Produces the build images used by nearly all other actions, particularly CI and release from 5.0.0-rc0 onwards. Complete images are attested and published to GHCR. Triggered on label creation (`build/*`). @@ -28,7 +28,7 @@ File: `ci-containers-ghcr.yml` - `docker/metadata-action@v5` - `docker/build-push-action@v6` -# CI +# Continuous Integration Main continuous integration job. Builds CCF for all target platforms, runs unit, end to end and partition tests Virtual. Run on every commit, including PRs from forks, gates merging. Also runs once a week, regardless of commits. @@ -52,11 +52,21 @@ Builds CCF with CodeQL, and runs the security-extended checks. Triggered on PRs File: `codeql-analysis.yml` 3rd party dependencies: None -# Verification +# Continuous Verification -Runs all existing TLA+ jobs. Triggered on PRs that affect tla/ or src/consensus and weekly on main. +Runs quick verification jobs: trace validation, simulation and short model checking configurations. Triggered on PRs that affect tla/ or src/consensus and weekly on main. -File: tlaplus.yml +File: `ci-verification.yml` +3rd party dependencies: None + +# Long Verification + +Runs more expensive verification jobs, such as model checking with reconfiguration. + +- Runs weekly. +- Can be manually run on a PR by setting `run-long-verification` label. + +File: `long-verification.yml` 3rd party dependencies: None # Release diff --git a/.github/workflows/ci-containers-ghcr.yml b/.github/workflows/ci-containers-ghcr.yml index cd067f888d3..c52d69b6d31 100644 --- a/.github/workflows/ci-containers-ghcr.yml +++ b/.github/workflows/ci-containers-ghcr.yml @@ -1,4 +1,4 @@ -name: "CI Containers GHCR" +name: "Continuous Integration Containers GHCR" on: push: diff --git a/.github/workflows/tlaplus.yml b/.github/workflows/ci-verification.yml similarity index 83% rename from .github/workflows/tlaplus.yml rename to .github/workflows/ci-verification.yml index 7d3cfa8bdee..623889ad369 100644 --- a/.github/workflows/tlaplus.yml +++ b/.github/workflows/ci-verification.yml @@ -1,4 +1,4 @@ -name: "Verification" +name: "Continuous Verification" on: schedule: @@ -147,12 +147,6 @@ jobs: cd tla/ Configurations=1C3N MaxTermLimit=2 RequestLimit=3 ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft1C3N2T3R.trace.tla -dumpTrace json MCccfraft1C3N2T3R.json - - name: MCccfraft - Configurations=2C2N (atomic reconf) MaxTermLimit=4 RequestLimit=3 NoCheckQuorum - run: | - set -x - cd tla/ - Configurations=2C2N MaxTermLimit=4 RequestLimit=1 NoCheckQuorum= ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft2C2N4T1R.trace.tla -dumpTrace json MCccfraft2C2N4T1R.json - - name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox. uses: actions/upload-artifact@v4 if: ${{ failure() }} @@ -162,34 +156,6 @@ jobs: tla/consensus/*_TTrace_*.tla tla/*.json - model-checking-with-reconfig-consensus: - name: Model Checking With Reconfig - Consensus - runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub] - container: - image: ghcr.io/microsoft/ccf/ci/default:build-25-07-2024 - - steps: - - uses: actions/checkout@v4 - - run: | - sudo apt update - sudo apt install -y default-jre - python3 ./tla/install_deps.py - - - name: MCccfraft - Configurations=3C2N MaxTermLimit=4 RequestLimit=1 NoCheckQuorum - run: | - set -x - cd tla/ - Configurations=3C2N MaxTermLimit=4 RequestLimit=1 NoCheckQuorum= ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft3C2N4T1R.trace.tla -dumpTrace json MCccfraft3C2N4T1R.json - - - name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox. - uses: actions/upload-artifact@v4 - if: ${{ failure() }} - with: - name: tlc-model-checking-with-reconfig-consensus - path: | - tla/consensus/*_TTrace_*.tla - tla/*.json - simulation-consensus: name: Simulation - Consensus runs-on: ubuntu-latest @@ -207,7 +173,7 @@ jobs: cd tla/ ./tlc.sh -workers auto -simulate -depth 500 consensus/SIMccfraft.tla -dumpTrace tla SIMccfraft.trace.tla -dumpTrace json SIMccfraft.json env: - SIM_TIMEOUT: 3000 + SIM_TIMEOUT: 1200 - name: Upload artifacts. uses: actions/upload-artifact@v4 diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e5a28e8fd59..04599064e76 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,4 +1,4 @@ -name: CI +name: Continuous Integration on: schedule: diff --git a/.github/workflows/long-verification.yml b/.github/workflows/long-verification.yml new file mode 100644 index 00000000000..9507f362fd2 --- /dev/null +++ b/.github/workflows/long-verification.yml @@ -0,0 +1,104 @@ +name: "Long Verification" + +on: + pull_request: + types: + - labeled + - synchronize + - opened + - reopened + schedule: + - cron: "0 0 * * 0" + workflow_dispatch: + +permissions: + actions: read + contents: read + security-events: write + +jobs: + model-checking-with-atomic-reconfig-consensus: + name: Model Checking With Atomic Reconfig - Consensus + if: ${{ contains(github.event.pull_request.labels.*.name, 'run-long-verification') }} + runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub] + container: + image: ghcr.io/microsoft/ccf/ci/default:build-25-07-2024 + + steps: + - uses: actions/checkout@v4 + - run: | + sudo apt update + sudo apt install -y default-jre + python3 ./tla/install_deps.py + + - name: MCccfraft - Configurations=2C2N (atomic reconf) MaxTermLimit=4 RequestLimit=3 NoCheckQuorum + run: | + set -x + cd tla/ + Configurations=2C2N MaxTermLimit=4 RequestLimit=1 NoCheckQuorum= ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft2C2N4T1R.trace.tla -dumpTrace json MCccfraft2C2N4T1R.json + + - name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox. + uses: actions/upload-artifact@v4 + 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: ${{ contains(github.event.pull_request.labels.*.name, 'run-long-verification') }} + runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub] + container: + image: ghcr.io/microsoft/ccf/ci/default:build-25-07-2024 + + steps: + - uses: actions/checkout@v4 + - run: | + sudo apt update + sudo apt install -y default-jre + python3 ./tla/install_deps.py + + - name: MCccfraft - Configurations=3C2N MaxTermLimit=4 RequestLimit=1 NoCheckQuorum + run: | + set -x + cd tla/ + Configurations=3C2N MaxTermLimit=4 RequestLimit=1 NoCheckQuorum= ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft3C2N4T1R.trace.tla -dumpTrace json MCccfraft3C2N4T1R.json + + - name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox. + uses: actions/upload-artifact@v4 + if: ${{ failure() }} + with: + name: tlc-model-checking-with-reconfig-consensus + path: | + tla/consensus/*_TTrace_*.tla + tla/*.json + + simulation-consensus: + name: Simulation - Consensus + if: ${{ contains(github.event.pull_request.labels.*.name, 'run-long-verification') }} + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v4 + - run: | + sudo apt update + sudo apt install -y default-jre + python3 ./tla/install_deps.py + + - name: Simulation + run: | + set -x + cd tla/ + ./tlc.sh -workers auto -simulate -depth 500 consensus/SIMccfraft.tla -dumpTrace tla SIMccfraft.trace.tla -dumpTrace json SIMccfraft.json + env: + SIM_TIMEOUT: 3000 + + - name: Upload artifacts. + uses: actions/upload-artifact@v4 + if: ${{ failure() }} + with: + name: tlc-simulation-consensus + path: | + tla/*