WIP: Weak memory support #2036

Workflow file for this run

	name: Format and Verify VOSTD (Main)

	on:
	push:
	branches:
	- main
	pull_request:
	branches:
	- main
	workflow_dispatch:
	inputs:
	branch:
	description: "Branch to run the workflow on"
	required: true
	default: "main"

	jobs:
	format-and-verify:
	runs-on: ubuntu-24.04
	env:
	CARGO_TERM_COLOR: always
	VERUS_REPOSITORY: https://github.com/asterinas/verus.git
	VERUS_BASE_COMMIT: bb61343fc97e4b3a97b1029f385ffb6bbb291da2
	VERUS_IRC11_PATCH: tools/patches/verus-irc11.patch
	VERUS_PATCH: tools/patches/verus-irc11-vstd.patch

	steps:
	- name: Checkout repository
	uses: actions/checkout@v7
	with:
	submodules: recursive

	- name: Install dependencies
	run: \|
	sudo apt update -qq
	sudo apt install -y build-essential unzip pkg-config libssl-dev llvm

	- name: Get Rust toolchain version
	id: rust-toolchain
	run: \|
	RUST_VERSION=$(grep 'channel' rust-toolchain.toml \| sed -E 's/.= "(.*)"/\1/')
	if [ -z "$RUST_VERSION" ]; then
	echo "Failed to extract Rust version from rust-toolchain.toml"
	exit 1
	fi
	echo "RUST_VERSION=$RUST_VERSION" >> "$GITHUB_ENV"
	echo "Rust version: $RUST_VERSION"

	- name: Cache Rust toolchain
	uses: actions/cache@v6
	with:
	path: \|
	~/.rustup/toolchains
	~/.rustup/update-hashes
	~/.rustup/tmp
	key: ${{ runner.os }}-rust-toolchain-${{ env.RUST_VERSION }}

	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-

	- name: Record toolchain revisions
	id: verus
	run: \|
	echo "Using pinned Asterinas Verus base: $VERUS_BASE_COMMIT"
	DV_COMMIT=$(git rev-parse HEAD:dv)
	echo "DV_COMMIT=$DV_COMMIT" >> "$GITHUB_ENV"
	echo "Using dv commit: $DV_COMMIT"

	- name: Cache dv build artifacts
	uses: actions/cache@v6
	with:
	path: dv/target
	key: ${{ runner.os }}-dv-${{ env.DV_COMMIT }}

	- name: Cache Verus
	id: cache-verus
	uses: actions/cache@v6
	with:
	path: tools/verus
	key: ${{ runner.os }}-verus-irc11-weak-memory-${{ env.VERUS_BASE_COMMIT }}-${{ hashFiles('tools/bootstrap-verus-irc11.sh', 'tools/patches/verus-irc11.patch', 'tools/patches/verus-irc11-vstd.patch') }}

	- name: Cache verusfmt
	id: cache-verusfmt
	uses: actions/cache@v6
	with:
	path: ~/.cargo/bin/verusfmt
	key: ${{ runner.os }}-verusfmt-${{ env.VERUS_BASE_COMMIT }}

	- name: Bootstrap Verus (if needed)
	run: \|
	if [ "${{ steps.cache-verus.outputs.cache-hit }}" = "true" ]; then
	echo "Using cached Verus"
	else
	echo "Cache miss, bootstrapping rebased Verus IRC11..."
	rm -rf tools/verus
	git init tools/verus
	git -C tools/verus remote add origin "$VERUS_REPOSITORY"
	git -C tools/verus fetch --depth=1 origin "$VERUS_BASE_COMMIT"
	git -C tools/verus checkout --detach FETCH_HEAD
	git -C tools/verus apply "$GITHUB_WORKSPACE/$VERUS_IRC11_PATCH"
	git -C tools/verus apply --reverse --check "$GITHUB_WORKSPACE/$VERUS_IRC11_PATCH"
	bash tools/bootstrap-verus-irc11.sh
	fi

	if ! command -v verusfmt >/dev/null 2>&1; then
	echo "verusfmt not found, installing..."
	curl --proto '=https' --tlsv1.2 -LsSf https://github.com/verus-lang/verusfmt/releases/latest/download/verusfmt-installer.sh \| sh
	fi
	test "$(git -C tools/verus rev-parse HEAD)" = "$VERUS_BASE_COMMIT"
	test -f tools/verus/source/vstd/atomic_weak.rs
	test -f tools/verus/source/vstd/thread_view.rs
	verusfmt --version

	- name: Enable IRC11 alongside existing SC atomics
	run: \|
	if git -C tools/verus apply --reverse --check "$GITHUB_WORKSPACE/$VERUS_PATCH"; then
	echo "IRC11 compatibility patch is already applied"
	else
	git -C tools/verus apply "$GITHUB_WORKSPACE/$VERUS_PATCH"
	fi

	- name: Run verification
	run: \|
	set -o pipefail
	if ! make 2>&1 \| tee verify_output.txt; then
	echo "❌ Verification failed"
	echo "VERIFY_FAILED=1" >> "$GITHUB_ENV"
	exit 1
	else
	echo "✅ Verification passed!"
	fi

	- name: Check for verification warnings
	if: always()
	run: \|
	WARNINGS=(
	"note: automatically chose triggers for this expression:\|auto-trigger notes"
	"warning: use of deprecated method \`vstd::set::Set::<A>::finite\`\|deprecated Set::finite()"
	"warning: use of deprecated associated function \`vstd::set::Set::<A>::new_assuming_finite\`\|deprecated Set::new_assuming_finite()"
	)

	FAILED=0
	for ITEM in "${WARNINGS[@]}"; do
	PATTERN="${ITEM%%\|*}"
	LABEL="${ITEM##*\|}"
	if grep -q "$PATTERN" verify_output.txt 2>/dev/null; then
	echo "❌ Found $LABEL"
	grep -n "$PATTERN" verify_output.txt
	FAILED=1
	else
	echo "✅ No $LABEL found"
	fi
	done

	if [[ "$FAILED" == "1" ]]; then
	echo "VERIFY_WARNINGS_FOUND=1" >> "$GITHUB_ENV"
	exit 1
	fi

	- name: Run format
	if: always()
	run: make fmt

	- name: Check for formatting changes
	if: always()
	run: \|
	if [[ -n $(git status --porcelain) ]]; then
	echo "Code is not properly formatted. Run 'make fmt'."
	git diff
	echo "FMT_FAILED=1" >> "$GITHUB_ENV"
	exit 1
	fi

	- name: Publish summary
	if: always()
	run: \|
	{
	echo "# CI Summary"
	if [[ "${FMT_FAILED:-0}" == "1" ]]; then
	echo "- Formatting: ❌ failed"
	else
	echo "- Formatting: ✅ passed"
	fi
	if [[ "${VERIFY_FAILED:-0}" == "1" ]]; then
	echo "- Verification: ❌ failed"
	else
	echo "- Verification: ✅ passed"
	fi
	if [[ "${VERIFY_WARNINGS_FOUND:-0}" == "1" ]]; then
	echo "- Verification warnings: ❌ found"
	else
	echo "- Verification warnings: ✅ none"
	fi
	} >> "$GITHUB_STEP_SUMMARY"

Navigation Menu

Uh oh!

WIP: Weak memory support #2036

Workflow file

WIP: Weak memory support #2036

Uh oh!

Workflow file for this run