diff --git a/.github/workflows/ci-verification.yml b/.github/workflows/ci-verification.yml index 8511d46da24..0fe67bbc062 100644 --- a/.github/workflows/ci-verification.yml +++ b/.github/workflows/ci-verification.yml @@ -24,24 +24,28 @@ jobs: name: Model Checking - Consistency runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub] container: - image: ghcr.io/microsoft/ccf/ci/default:build-14-01-2025 - defaults: - run: - working-directory: tla + 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: | - sudo apt update - sudo apt install -y default-jre - python3 install_deps.py + tdnf install -y jre wget + python3 tla/install_deps.py --skip-apt-packages - - run: ./tlc.py mc consistency/MCSingleNode.tla - - run: ./tlc.py mc consistency/MCSingleNodeReads.tla - - run: ./tlc.py mc consistency/MCMultiNode.tla - - run: ./tlc.py mc consistency/MCMultiNodeReads.tla - - run: ./tlc.py mc consistency/MCMultiNodeReadsAlt.tla + - 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 @@ -102,22 +106,26 @@ jobs: name: Model Checking - Consensus runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub] container: - image: ghcr.io/microsoft/ccf/ci/default:build-14-01-2025 - defaults: - run: - working-directory: tla + 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: | - sudo apt update - sudo apt install -y default-jre - python3 install_deps.py + tdnf install -y jre wget + python3 tla/install_deps.py --skip-apt-packages - - run: ./tlc.py mc consensus/MCabs.tla - - run: ./tlc.py --trace-name 1C2N mc --term-count 2 --request-count 2 --raft-configs 1C2N consensus/MCccfraft.tla - - run: ./tlc.py --trace-name 1C3N mc --term-count 0 --request-count 3 --raft-configs 1C3N consensus/MCccfraft.tla + - 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 @@ -158,20 +166,41 @@ jobs: name: Trace Validation - Consensus runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub] container: - image: ghcr.io/microsoft/ccf/ci/default:build-14-01-2025 + 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: | - sudo apt update - sudo apt install -y default-jre parallel - python3 ./tla/install_deps.py + 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 diff --git a/.github/workflows/long-verification.yml b/.github/workflows/long-verification.yml index 81dda7b0c66..a3b6cfda133 100644 --- a/.github/workflows/long-verification.yml +++ b/.github/workflows/long-verification.yml @@ -22,19 +22,24 @@ jobs: if: ${{ 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-virtual-ccf-sub] container: - image: ghcr.io/microsoft/ccf/ci/default:build-14-01-2025 - defaults: - run: - working-directory: tla + 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 - - run: | - sudo apt update - sudo apt install -y default-jre - python3 install_deps.py + - name: Install TLC dependencies + run: | + tdnf install -y jre wget + python3 tla/install_deps.py --skip-apt-packages - - run: ./tlc.py --trace-name 2C2N mc --term-count 2 --request-count 0 --raft-configs 2C2N --disable-check-quorum consensus/MCccfraft.tla + - 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@v4 @@ -50,19 +55,24 @@ jobs: if: ${{ 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-virtual-ccf-sub] container: - image: ghcr.io/microsoft/ccf/ci/default:build-14-01-2025 - defaults: - run: - working-directory: tla + 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 - - run: | - sudo apt update - sudo apt install -y default-jre - python3 install_deps.py + - name: Install TLC dependencies + run: | + tdnf install -y jre wget + python3 tla/install_deps.py --skip-apt-packages - - run: ./tlc.py --trace-name 3C2N mc --term-count 2 --request-count 0 --raft-configs 3C2N --disable-check-quorum consensus/MCccfraft.tla + - 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@v4