TLA CI on Azure Linux (#6884)

Co-authored-by: Amaury Chamayou <amchamay@microsoft.com>
microsoft · Mar 5, 2025 · d157b65 · d157b65
1 parent 6a79fcc
commit d157b65
Show file tree

Hide file tree

Showing 2 changed files with 83 additions and 44 deletions.
diff --git 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
@@ -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