Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

TLA CI on Azure Linux #6884

Merged
merged 10 commits into from
Mar 5, 2025
Merged

TLA CI on Azure Linux #6884

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
f1fdf7c
.
maxtropets Mar 4, 2025
7149dd8
.
maxtropets Mar 4, 2025
ae0182e
.
maxtropets Mar 4, 2025
5d9a89f
.
maxtropets Mar 4, 2025
fc80fd3
.
maxtropets Mar 4, 2025
a493277
Merge branch 'main' into f/tla-azure-linux
maxtropets Mar 4, 2025
e1433a2
Parallel
maxtropets Mar 4, 2025
3776227
Merge branch 'main' into f/tla-azure-linux
maxtropets Mar 4, 2025
e5341c3
https
maxtropets Mar 5, 2025
ef558ec
Merge branch 'main' into f/tla-azure-linux
achamayou Mar 5, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
81 changes: 55 additions & 26 deletions .github/workflows/ci-verification.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
46 changes: 28 additions & 18 deletions .github/workflows/long-verification.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down