Skip to content

Commit

Permalink
Split Verification Jobs (#6512)
Browse files Browse the repository at this point in the history
  • Loading branch information
achamayou authored Sep 30, 2024
1 parent 2069c68 commit a032ae0
Show file tree
Hide file tree
Showing 5 changed files with 123 additions and 43 deletions.
20 changes: 15 additions & 5 deletions .github/workflows/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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/*`).
Expand All @@ -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.

Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/ci-containers-ghcr.yml
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
name: "CI Containers GHCR"
name: "Continuous Integration Containers GHCR"

on:
push:
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
name: "Verification"
name: "Continuous Verification"

on:
schedule:
Expand Down Expand Up @@ -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() }}
Expand All @@ -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
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
name: CI
name: Continuous Integration

on:
schedule:
Expand Down
104 changes: 104 additions & 0 deletions .github/workflows/long-verification.yml
Original file line number Diff line number Diff line change
@@ -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/*

0 comments on commit a032ae0

Please sign in to comment.