From a032ae0f50094ff158695df0f7bc2e0f01d58ca3 Mon Sep 17 00:00:00 2001 From: Amaury Chamayou Date: Mon, 30 Sep 2024 12:34:23 +0100 Subject: [PATCH] Split Verification Jobs (#6512) --- .github/workflows/README.md | 20 +++- .github/workflows/ci-containers-ghcr.yml | 2 +- .../{tlaplus.yml => ci-verification.yml} | 38 +------ .github/workflows/ci.yml | 2 +- .github/workflows/long-verification.yml | 104 ++++++++++++++++++ 5 files changed, 123 insertions(+), 43 deletions(-) rename .github/workflows/{tlaplus.yml => ci-verification.yml} (83%) create mode 100644 .github/workflows/long-verification.yml diff --git a/.github/workflows/README.md b/.github/workflows/README.md index 25f3f964a37d..0651ec5b625f 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 cd067f888d39..c52d69b6d317 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 7d3cfa8bdeed..623889ad3694 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 e5a28e8fd59c..04599064e769 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 000000000000..9507f362fd2c --- /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/*