Mark manifests as pending during resolution #83

Workflow file for this run

.github/workflows/p-model-check.yaml at 687f9b4

	name: P Model Check

	on:
	push:
	branches:
	- main
	pull_request:
	paths:
	- 'p/**'
	- '.github/workflows/p-model-check.yaml'
	schedule:
	- cron: '0 6 * * 1' # Every Monday at 06:00 UTC

	permissions:
	contents: read

	env:
	# Enforce NuGet package signature verification on the install steps below.
	# On Linux/macOS this verification is opt-in (it defaults on only on Windows),
	# so without this the signatureValidationMode=require in NuGet.config is a
	# no-op on these runners.
	# https://learn.microsoft.com/en-us/nuget/reference/signed-package-verification-options
	DOTNET_NUGET_SIGNATURE_VERIFICATION: true

	jobs:
	changes:
	runs-on: ubuntu-latest
	outputs:
	gc_reset: ${{ steps.filter.outputs.gc_reset }}
	gc_reset_multinode: ${{ steps.filter.outputs.gc_reset_multinode }}
	gc_leading_group: ${{ steps.filter.outputs.gc_leading_group }}
	gc_reset_leading_group: ${{ steps.filter.outputs.gc_reset_leading_group }}
	gc_decision: ${{ steps.filter.outputs.gc_decision }}
	delete_stream_anchor: ${{ steps.filter.outputs.delete_stream_anchor }}
	read_resolution: ${{ steps.filter.outputs.read_resolution }}
	trimmed_segment: ${{ steps.filter.outputs.trimmed_segment }}
	orphan_leak: ${{ steps.filter.outputs.orphan_leak }}
	tier_routing: ${{ steps.filter.outputs.tier_routing }}
	writer_fencing: ${{ steps.filter.outputs.writer_fencing }}
	manifest_replica_lifecycle: ${{ steps.filter.outputs.manifest_replica_lifecycle }}
	steps:
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
	with:
	fetch-depth: 0
	- name: Detect changed paths
	id: filter
	run: \|
	if [ "${{ github.event_name }}" = "pull_request" ]; then
	BASE=${{ github.event.pull_request.base.sha }}
	else
	BASE=${{ github.event.before }}
	fi
	# github.event.before can be the zero SHA (first push to a branch) or
	# a commit unreachable from history (e.g. a squash/rebase merge
	# rewrote main), which makes `git diff` fail. Fall back to treating
	# every path as changed so the affected jobs run instead of erroring out.
	if [ -z "$BASE" ] \|\| [ "$BASE" = "0000000000000000000000000000000000000000" ] \|\| ! git cat-file -e "$BASE^{commit}" 2>/dev/null; then
	CHANGED=$(git ls-tree -r --name-only HEAD)
	else
	CHANGED=$(git diff --name-only "$BASE" HEAD)
	fi
	echo "gc_reset=false" >> "$GITHUB_OUTPUT"
	echo "gc_reset_multinode=false" >> "$GITHUB_OUTPUT"
	echo "gc_leading_group=false" >> "$GITHUB_OUTPUT"
	echo "gc_reset_leading_group=false" >> "$GITHUB_OUTPUT"
	echo "gc_decision=false" >> "$GITHUB_OUTPUT"
	echo "delete_stream_anchor=false" >> "$GITHUB_OUTPUT"
	echo "read_resolution=false" >> "$GITHUB_OUTPUT"
	echo "$CHANGED" \| grep -q '^p/gc-reset/' && echo "gc_reset=true" >> "$GITHUB_OUTPUT" \|\| true
	echo "$CHANGED" \| grep -q '^p/gc-reset-multinode/' && echo "gc_reset_multinode=true" >> "$GITHUB_OUTPUT" \|\| true
	echo "$CHANGED" \| grep -q '^p/gc-leading-group/' && echo "gc_leading_group=true" >> "$GITHUB_OUTPUT" \|\| true
	echo "$CHANGED" \| grep -q '^p/gc-reset-leading-group/' && echo "gc_reset_leading_group=true" >> "$GITHUB_OUTPUT" \|\| true
	echo "$CHANGED" \| grep -q '^p/gc-decision/' && echo "gc_decision=true" >> "$GITHUB_OUTPUT" \|\| true
	echo "$CHANGED" \| grep -q '^p/delete-stream-anchor/' && echo "delete_stream_anchor=true" >> "$GITHUB_OUTPUT" \|\| true
	echo "$CHANGED" \| grep -q '^p/read-resolution/' && echo "read_resolution=true" >> "$GITHUB_OUTPUT" \|\| true
	echo "trimmed_segment=false" >> "$GITHUB_OUTPUT"
	echo "$CHANGED" \| grep -q '^p/trimmed-segment/' && echo "trimmed_segment=true" >> "$GITHUB_OUTPUT" \|\| true
	echo "orphan_leak=false" >> "$GITHUB_OUTPUT"
	echo "$CHANGED" \| grep -q '^p/orphan-leak/' && echo "orphan_leak=true" >> "$GITHUB_OUTPUT" \|\| true
	echo "tier_routing=false" >> "$GITHUB_OUTPUT"
	echo "$CHANGED" \| grep -q '^p/tier-routing/' && echo "tier_routing=true" >> "$GITHUB_OUTPUT" \|\| true
	echo "writer_fencing=false" >> "$GITHUB_OUTPUT"
	echo "$CHANGED" \| grep -q '^p/writer-fencing/' && echo "writer_fencing=true" >> "$GITHUB_OUTPUT" \|\| true
	echo "manifest_replica_lifecycle=false" >> "$GITHUB_OUTPUT"
	echo "$CHANGED" \| grep -q '^p/manifest-replica-lifecycle/' && echo "manifest_replica_lifecycle=true" >> "$GITHUB_OUTPUT" \|\| true
	if echo "$CHANGED" \| grep -q '^\.github/workflows/p-model-check\.yaml'; then
	echo "gc_reset=true" >> "$GITHUB_OUTPUT"
	echo "gc_reset_multinode=true" >> "$GITHUB_OUTPUT"
	echo "gc_leading_group=true" >> "$GITHUB_OUTPUT"
	echo "gc_reset_leading_group=true" >> "$GITHUB_OUTPUT"
	echo "gc_decision=true" >> "$GITHUB_OUTPUT"
	echo "delete_stream_anchor=true" >> "$GITHUB_OUTPUT"
	echo "read_resolution=true" >> "$GITHUB_OUTPUT"
	echo "trimmed_segment=true" >> "$GITHUB_OUTPUT"
	echo "orphan_leak=true" >> "$GITHUB_OUTPUT"
	echo "tier_routing=true" >> "$GITHUB_OUTPUT"
	echo "writer_fencing=true" >> "$GITHUB_OUTPUT"
	echo "manifest_replica_lifecycle=true" >> "$GITHUB_OUTPUT"
	fi

	gc-reset:
	needs: changes
	if: needs.changes.outputs.gc_reset == 'true' \|\| github.event_name == 'schedule'
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
	- uses: actions/setup-dotnet@a98b56852c35b8e3190ac28c8c2271da59106c68 # v6.0.0
	with:
	dotnet-version: '8.0.x'
	- name: Install the P checker
	run: \|
	dotnet tool install --global P --version 3.1.0 --configfile "$GITHUB_WORKSPACE/p/NuGet.config"
	echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
	- name: Compile
	run: \|
	cd p/gc-reset
	p compile
	- name: Tests that must hold
	run: \|
	cd p/gc-reset
	for tc in tcGcResetGuarded tcGcResetExplore tcEpochAxisSafe; do
	echo "::group::$tc (expect hold)"
	p check -tc "$tc" -i 5000
	echo "::endgroup::"
	done
	# PCT surfaces rare interleavings the random strategy misses.
	echo "::group::tcGcResetExplore (PCT)"
	p check -tc tcGcResetExplore --sch-pct 10 -i 5000
	echo "::endgroup::"
	- name: Validation gate (the guard-removed model must reproduce GC x reset)
	run: \|
	cd p/gc-reset
	rm -rf PCheckerOutput/
	echo "::group::tcGcResetUnguarded (expect the GC x reset counterexample)"
	if p check -tc tcGcResetUnguarded -i 2000; then
	echo "ERROR: tcGcResetUnguarded passed; the model no longer reproduces GC x reset."
	echo "The guard-removed model must fail, otherwise the guarded result is not trustworthy."
	exit 1
	fi
	if ! grep -rqF 'INV#2 violated: GC deleted live object (offset=850, uid=2)' PCheckerOutput/BugFinding/; then
	echo "ERROR: the unguarded run failed, but not with the expected INV#2 (850, uid 2) counterexample."
	exit 1
	fi
	echo "Gate satisfied: guard-removed model fails with the expected dangling reference."
	echo "::endgroup::"
	- name: Validation gate (the reset atomic-prefix ordering is load-bearing)
	run: \|
	cd p/gc-reset
	rm -rf PCheckerOutput/
	# The floor-last ordering deletes a live object even with the guard on.
	# It is a rare interleaving that the random strategy misses, so use PCT.
	echo "::group::tcGcResetFloorLast (expect the GC x reset counterexample under PCT)"
	if p check -tc tcGcResetFloorLast --sch-pct 10 -i 5000; then
	echo "ERROR: tcGcResetFloorLast passed; lowering the floor after the re-tier no longer"
	echo "deletes a live object. The atomic-prefix ordering is supposed to be necessary."
	exit 1
	fi
	if ! grep -rqF 'INV#2 violated: GC deleted live object (offset=850, uid=2)' PCheckerOutput/BugFinding/; then
	echo "ERROR: the floor-last run failed, but not with the expected INV#2 (850, uid 2) counterexample."
	exit 1
	fi
	echo "Gate satisfied: floor-last ordering fails with the expected dangling reference."
	echo "::endgroup::"

	gc-reset-multinode:
	needs: changes
	if: needs.changes.outputs.gc_reset_multinode == 'true' \|\| github.event_name == 'schedule'
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
	- uses: actions/setup-dotnet@a98b56852c35b8e3190ac28c8c2271da59106c68 # v6.0.0
	with:
	dotnet-version: '8.0.x'
	- name: Install the P checker
	run: \|
	dotnet tool install --global P --version 3.1.0 --configfile "$GITHUB_WORKSPACE/p/NuGet.config"
	echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
	- name: Compile
	run: \|
	cd p/gc-reset-multinode
	p compile
	- name: Tests that must hold
	run: \|
	cd p/gc-reset-multinode
	for tc in tcMultiNodeStaleGuarded tcMultiNodeSyncedGuarded tcMultiNodeExplore; do
	echo "::group::$tc (expect hold)"
	p check -tc "$tc" -i 5000
	echo "::endgroup::"
	done
	# PCT surfaces rare interleavings the random strategy misses.
	echo "::group::tcMultiNodeExplore (PCT)"
	p check -tc tcMultiNodeExplore --sch-pct 10 -i 5000
	echo "::endgroup::"
	- name: Validation gate (a stale replica cache must defeat still_dangling)
	run: \|
	cd p/gc-reset-multinode
	rm -rf PCheckerOutput/
	echo "::group::tcMultiNodeStaleUnguarded (expect the cross-node GC x reset counterexample)"
	if p check -tc tcMultiNodeStaleUnguarded -i 2000; then
	echo "ERROR: tcMultiNodeStaleUnguarded passed; the model no longer reproduces the stale-cache delete."
	echo "With the epoch guard off and the reset sync dropped, the shipped still_dangling/1 guard"
	echo "must re-read the stale floor and delete a live object, otherwise the guarded result is not trustworthy."
	exit 1
	fi
	if ! grep -rqF 'INV#2 violated: GC deleted live object (offset=850, uid=2)' PCheckerOutput/BugFinding/; then
	echo "ERROR: the unguarded run failed, but not with the expected INV#2 (850, uid 2) counterexample."
	exit 1
	fi
	echo "Gate satisfied: a stale replica cache defeats still_dangling and deletes the re-tiered live object."
	echo "::endgroup::"

	gc-leading-group:
	needs: changes
	if: needs.changes.outputs.gc_leading_group == 'true' \|\| github.event_name == 'schedule'
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
	- uses: actions/setup-dotnet@a98b56852c35b8e3190ac28c8c2271da59106c68 # v6.0.0
	with:
	dotnet-version: '8.0.x'
	- name: Install the P checker
	run: \|
	dotnet tool install --global P --version 3.1.0 --configfile "$GITHUB_WORKSPACE/p/NuGet.config"
	echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
	- name: Compile
	run: \|
	cd p/gc-leading-group
	p compile
	- name: Tests that must hold
	run: \|
	cd p/gc-leading-group
	echo "::group::tcLeadingGroupGuarded (expect hold)"
	p check -tc tcLeadingGroupGuarded -i 5000
	echo "::endgroup::"
	- name: Validation gate (removing the carve-out must delete the leading group)
	run: \|
	cd p/gc-leading-group
	echo "::group::tcLeadingGroupUnguarded (expect the INV#2 dangling reference)"
	if p check -tc tcLeadingGroupUnguarded -i 2000; then
	echo "ERROR: tcLeadingGroupUnguarded passed; the model no longer deletes the leading group."
	echo "Removing the referenced_group_key carve-out must delete a live group."
	exit 1
	fi
	if ! grep -rqF 'INV#2 violated: GC deleted referenced object (offset=80, uid=2)' PCheckerOutput/BugFinding/; then
	echo "ERROR: the carve-out-removed run failed, but not with the expected INV#2 (80, uid 2) counterexample."
	exit 1
	fi
	echo "Gate satisfied: carve-out-removed model deletes the referenced leading group."
	echo "::endgroup::"

	gc-reset-leading-group:
	needs: changes
	if: needs.changes.outputs.gc_reset_leading_group == 'true' \|\| github.event_name == 'schedule'
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
	- uses: actions/setup-dotnet@a98b56852c35b8e3190ac28c8c2271da59106c68 # v6.0.0
	with:
	dotnet-version: '8.0.x'
	- name: Install the P checker
	run: \|
	dotnet tool install --global P --version 3.1.0 --configfile "$GITHUB_WORKSPACE/p/NuGet.config"
	echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
	- name: Compile
	run: \|
	cd p/gc-reset-leading-group
	p compile
	- name: Tests that must hold
	run: \|
	cd p/gc-reset-leading-group
	for tc in tcLeadingGroupResetFixed tcLeadingGroupResetExplore tcLeadingGroupRetentionOnly; do
	echo "::group::$tc (expect hold)"
	p check -tc "$tc" -i 5000
	echo "::endgroup::"
	done
	# PCT surfaces rare interleavings the random strategy misses.
	echo "::group::tcLeadingGroupResetExplore (PCT)"
	p check -tc tcLeadingGroupResetExplore --sch-pct 10 -i 5000
	echo "::endgroup::"
	- name: Validation gate (offset-only re-check must delete the live leading group)
	run: \|
	cd p/gc-reset-leading-group
	rm -rf PCheckerOutput/
	echo "::group::tcLeadingGroupResetBug (expect the GC x reset x leading-group counterexample)"
	if p check -tc tcLeadingGroupResetBug -i 2000; then
	echo "ERROR: tcLeadingGroupResetBug passed; the model no longer deletes the live leading group."
	echo "The offset-only still_dangling re-check must delete a reset-installed leading group,"
	echo "otherwise the carve-out re-validation result is not trustworthy."
	exit 1
	fi
	if ! grep -rqF 'INV#2 violated: GC deleted live object (offset=850, uid=2) still referenced by the manifest (live leading group)' PCheckerOutput/BugFinding/; then
	echo "ERROR: the offset-only run failed, but not with the expected INV#2 (850, uid 2) leading-group counterexample."
	exit 1
	fi
	echo "Gate satisfied: the offset-only re-check deletes the live leading group."
	echo "::endgroup::"

	gc-decision:
	needs: changes
	if: needs.changes.outputs.gc_decision == 'true' \|\| github.event_name == 'schedule'
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
	- uses: actions/setup-dotnet@a98b56852c35b8e3190ac28c8c2271da59106c68 # v6.0.0
	with:
	dotnet-version: '8.0.x'
	- name: Install the P checker
	run: \|
	dotnet tool install --global P --version 3.1.0 --configfile "$GITHUB_WORKSPACE/p/NuGet.config"
	echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
	- name: Compile
	run: \|
	cd p/gc-decision
	p compile
	- name: Tests that must hold
	run: \|
	cd p/gc-decision
	for tc in tcGcBasicReclaim tcGcCrossNodeStaleGuarded tcGcCrossNodeSynced \
	tcGcResetRereadHolds tcGcLeadingGroupHolds tcGcResetAfterSnapshotGuarded \
	tcGcExploreGuarded; do
	echo "::group::$tc (expect hold)"
	p check -tc "$tc" -i 5000
	echo "::endgroup::"
	done
	# PCT surfaces rare interleavings the random strategy misses.
	echo "::group::tcGcExploreGuarded (PCT)"
	p check -tc tcGcExploreGuarded --sch-pct 20 -i 6000
	echo "::endgroup::"
	- name: Validation gate (each shipped guard is load-bearing)
	run: \|
	cd p/gc-decision
	# Each gate removes one shipped guard and must reproduce a live deletion
	# with the specific counterexample object, otherwise the guarded result
	# is not trustworthy.
	check_gate() {
	tc="$1"; expected="$2"
	rm -rf PCheckerOutput/
	echo "::group::$tc (expect $expected)"
	if p check -tc "$tc" -i 2000; then
	echo "ERROR: $tc passed; the model no longer reaps live data with this guard removed."
	exit 1
	fi
	if ! grep -rqF "$expected" PCheckerOutput/BugFinding/; then
	echo "ERROR: $tc failed, but not with the expected counterexample: $expected"
	exit 1
	fi
	echo "Gate satisfied: $tc reaps live data as expected."
	echo "::endgroup::"
	}
	check_gate tcGcCrossNodeStaleUnguarded 'INV#2 violated: GC deleted live object (kind=0, offset=850, uid=2, epoch=0)'
	check_gate tcGcNoReread 'INV#2 violated: GC deleted live object (kind=0, offset=80, uid=3, epoch=0)'
	check_gate tcGcNoLeadingReread 'INV#2 violated: GC deleted live object (kind=1, offset=80, uid=820, epoch=0)'
	- name: Validation gate (the reset-after-snapshot gap, shipped guards only)
	run: \|
	cd p/gc-decision
	# With all three shipped guards on, a reset that commits after the sweep
	# snapshots still reaps the live re-tier: the epoch gate was already
	# sampled and still_dangling re-reads the same stale floor. The proposed
	# GUARD D (tcGcResetAfterSnapshotGuarded above) closes it; these must fail.
	rm -rf PCheckerOutput/
	echo "::group::tcGcResetAfterSnapshotStale (expect the reset-after-snapshot counterexample)"
	if p check -tc tcGcResetAfterSnapshotStale -i 2000; then
	echo "ERROR: tcGcResetAfterSnapshotStale passed; the shipped-guard gap is no longer reproduced."
	exit 1
	fi
	if ! grep -rqF 'INV#2 violated: GC deleted live object (kind=0, offset=80, uid=3, epoch=0)' PCheckerOutput/BugFinding/; then
	echo "ERROR: the run failed, but not with the expected (offset=80, uid=3) counterexample."
	exit 1
	fi
	echo "Gate satisfied: reset-after-snapshot reaps the live re-tier under shipped guards."
	echo "::endgroup::"
	rm -rf PCheckerOutput/
	echo "::group::tcGcExploreShipped (PCT, expect the same gap)"
	if p check -tc tcGcExploreShipped --sch-pct 20 -i 6000; then
	echo "ERROR: tcGcExploreShipped passed; PCT no longer reaches the reset-after-snapshot gap."
	exit 1
	fi
	if ! grep -rqF 'INV#2 violated: GC deleted live object' PCheckerOutput/BugFinding/; then
	echo "ERROR: tcGcExploreShipped failed, but not via the INV#2 dangling reference."
	exit 1
	fi
	echo "Gate satisfied: PCT reaches the reset-after-snapshot live deletion."
	echo "::endgroup::"

	manifest-replica-lifecycle:
	needs: changes
	if: needs.changes.outputs.manifest_replica_lifecycle == 'true' \|\| github.event_name == 'schedule'
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
	- uses: actions/setup-dotnet@a98b56852c35b8e3190ac28c8c2271da59106c68 # v6.0.0
	with:
	dotnet-version: '8.0.x'
	- name: Install the P checker
	run: \|
	dotnet tool install --global P --version 3.1.0 --configfile "$GITHUB_WORKSPACE/p/NuGet.config"
	echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
	- name: Compile
	run: \|
	cd p/manifest-replica-lifecycle
	p compile
	- name: Tests that must hold
	run: \|
	cd p/manifest-replica-lifecycle
	for tc in tcCleanupGuarded tcStaleSyncGuarded tcReregisterGuarded \
	tcConvergenceGuarded tcForgetReleasesWriterRow tcSyncAfterExitFixed \
	tcEditAfterExitFixed tcStartupRaceContextFirst tcReconcileRaceResync tcExplore; do
	echo "::group::$tc (expect hold)"
	p check -tc "$tc" -i 5000
	echo "::endgroup::"
	done
	# PCT surfaces rare interleavings the random strategy misses.
	echo "::group::tcExplore (PCT)"
	p check -tc tcExplore --sch-pct 10 -i 5000
	echo "::endgroup::"
	- name: Validation gate (each guard is load-bearing)
	run: \|
	cd p/manifest-replica-lifecycle
	# Each gate removes one guard and must reproduce its specific failure,
	# otherwise the guarded results above are not trustworthy. A gate that
	# passes means the guard is no longer load-bearing, or the model rotted.
	check_gate() {
	tc="$1"; expected="$2"
	rm -rf PCheckerOutput/
	echo "::group::$tc (expect failure: $expected)"
	if p check -tc "$tc" -i 2000; then
	echo "ERROR: $tc passed with the guard removed; the model no longer reproduces the failure."
	exit 1
	fi
	if ! grep -rqF "$expected" PCheckerOutput/BugFinding/; then
	echo "ERROR: $tc failed, but not with the expected counterexample: $expected"
	exit 1
	fi
	echo "Gate satisfied: $tc reproduces the failure as expected."
	echo "::endgroup::"
	}
	# The three shipped guards: member-DOWN cleanup, stale-sync ordering,
	# and the re-registration monitor repoint.
	check_gate tcCleanupUnguarded 'NOLEAK violated: replica holds per-node state for stream 0 with no live reader'
	check_gate tcStaleSyncUnguarded 'STALEFLOOR violated: cache for stream 0 regressed to (epoch=1, sn=1) below already-applied (epoch=2, sn=2)'
	check_gate tcReregisterUnguarded 'RETAIN violated: replica dropped per-node state for stream 0 that still has a live reader (a superseded member DOWN evicted the live context)'
	# The gap this model surfaces: a sync after a member DOWN re-strands the
	# row (the shipped-in-this-branch A2 guard closes it in tcSyncAfterExitFixed).
	check_gate tcSyncAfterExitStrands 'NOLEAK violated: replica holds per-node state for stream 0 with no live reader'
	# The same gap on the other write path: apply_edits needed the identical
	# A2 guard sync already had (tcEditAfterExitFixed closes it).
	check_gate tcEditAfterExitStrands 'NOLEAK violated: replica holds per-node state for stream 0 with no live reader'
	# Liveness: syncs dropped forever (tcConvergenceStuck), and the two
	# startup triggers that starve the cache without recovery - the
	# WriterFirst acceptor race (A1 fixes it) and the writer-driven reconcile
	# race (only A1' can, since the node's attach ordering cannot reach it).
	check_gate tcConvergenceStuck "ReplicaConverges detected liveness bug in hot state 'Lagging'"
	check_gate tcStartupRaceWriterFirst "ReplicaConverges detected liveness bug in hot state 'Lagging'"
	check_gate tcReconcileRaceNoResync "ReplicaConverges detected liveness bug in hot state 'Lagging'"

	delete-stream-anchor:
	needs: changes
	if: needs.changes.outputs.delete_stream_anchor == 'true' \|\| github.event_name == 'schedule'
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
	- uses: actions/setup-dotnet@a98b56852c35b8e3190ac28c8c2271da59106c68 # v6.0.0
	with:
	dotnet-version: '8.0.x'
	- name: Install the P checker
	run: \|
	dotnet tool install --global P --version 3.1.0 --configfile "$GITHUB_WORKSPACE/p/NuGet.config"
	echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
	- name: Compile
	run: \|
	cd p/delete-stream-anchor
	p compile
	- name: Tests that must hold
	run: \|
	cd p/delete-stream-anchor
	for tc in tcAnchorReclaimsAcrossCrash tcAnchorExplore; do
	echo "::group::$tc (expect hold)"
	p check -tc "$tc" -i 5000
	echo "::endgroup::"
	done
	# PCT surfaces rare interleavings the random strategy misses.
	echo "::group::tcAnchorExplore (PCT)"
	p check -tc tcAnchorExplore --sch-pct 10 -i 5000
	echo "::endgroup::"
	- name: Validation gate (a stale read or out-of-order anchor must reap live data)
	run: \|
	cd p/delete-stream-anchor
	# Both MUST fail with the NOREAPLIVE counterexample. A green here means
	# the model no longer reaches the live-data reap, i.e. the consistent-read
	# or anchor-before-fragment requirement is no longer load-bearing in the
	# model and the by-construction result is not trustworthy.
	for tc in tcAnchorStaleReadReapsLive tcAnchorOrderingViolated; do
	rm -rf PCheckerOutput/
	echo "::group::$tc (expect the live-reap counterexample)"
	if p check -tc "$tc" -i 2000; then
	echo "ERROR: $tc passed; the model no longer reaps live data."
	echo "A stale anchor read (or a fragment written before the anchor) must reap a live"
	echo "stream, otherwise the consistent-read / ordering requirement is not load-bearing."
	exit 1
	fi
	if ! grep -rqF 'INV NOREAPLIVE violated' PCheckerOutput/BugFinding/; then
	echo "ERROR: $tc failed, but not with the expected NOREAPLIVE counterexample."
	exit 1
	fi
	echo "Gate satisfied: $tc reaps live data as expected."
	echo "::endgroup::"
	done

	read-resolution:
	needs: changes
	if: needs.changes.outputs.read_resolution == 'true' \|\| github.event_name == 'schedule'
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
	- uses: actions/setup-dotnet@a98b56852c35b8e3190ac28c8c2271da59106c68 # v6.0.0
	with:
	dotnet-version: '8.0.x'
	- name: Install the P checker
	run: \|
	dotnet tool install --global P --version 3.1.0 --configfile "$GITHUB_WORKSPACE/p/NuGet.config"
	echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
	- name: Compile
	run: \|
	cd p/read-resolution
	p compile
	- name: Tests that must hold
	run: \|
	cd p/read-resolution
	for tc in tcReadResolveGuarded tcReadResolveExplore; do
	echo "::group::$tc (expect hold)"
	p check -tc "$tc" -i 5000
	echo "::endgroup::"
	done
	echo "::group::tcReadResolveExplore (PCT)"
	p check -tc tcReadResolveExplore --sch-pct 10 -i 5000
	echo "::endgroup::"
	- name: Validation gate (the catch-all model must reproduce the silent skip)
	run: \|
	cd p/read-resolution
	echo "::group::tcReadResolveBuggy (expect the INV#4 silent remote skip)"
	if p check -tc tcReadResolveBuggy -i 2000; then
	echo "ERROR: tcReadResolveBuggy passed; the model no longer reproduces the silent remote skip."
	echo "The catch-all model must fail, otherwise the guarded result is not trustworthy."
	exit 1
	fi
	if ! grep -rqF 'INV#4 violated: resolved' PCheckerOutput/BugFinding/; then
	echo "ERROR: the catch-all run failed, but not with the expected INV#4 silent-skip counterexample."
	exit 1
	fi
	echo "Gate satisfied: catch-all model fails with the expected silent remote skip."
	echo "::endgroup::"

	trimmed-segment:
	needs: changes
	if: needs.changes.outputs.trimmed_segment == 'true' \|\| github.event_name == 'schedule'
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
	- uses: actions/setup-dotnet@a98b56852c35b8e3190ac28c8c2271da59106c68 # v6.0.0
	with:
	dotnet-version: '8.0.x'
	- name: Install the P checker
	run: \|
	dotnet tool install --global P --version 3.1.0 --configfile "$GITHUB_WORKSPACE/p/NuGet.config"
	echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
	- name: Compile
	run: \|
	cd p/trimmed-segment
	p compile
	- name: Tests that must hold
	run: \|
	cd p/trimmed-segment
	for tc in tcTrimGuarded tcTrimExplore; do
	echo "::group::$tc (expect hold)"
	p check -tc "$tc" -i 5000
	echo "::endgroup::"
	done
	echo "::group::tcTrimExplore (PCT)"
	p check -tc tcTrimExplore --sch-pct 10 -i 5000
	echo "::endgroup::"
	- name: Validation gate (removing local_log_ahead must wedge the transfer)
	run: \|
	cd p/trimmed-segment
	echo "::group::tcTrimBuggy (expect the liveness obligation to fail)"
	if p check -tc tcTrimBuggy -i 2000; then
	echo "ERROR: tcTrimBuggy passed; the model no longer wedges on a trimmed segment."
	echo "Removing the local_log_ahead recovery must leave the transfer unresolved forever."
	exit 1
	fi
	if ! grep -rqF "hot state 'AwaitingResolution'" PCheckerOutput/BugFinding/; then
	echo "ERROR: the buggy run failed, but not via the TransferEventuallyResolves liveness obligation."
	exit 1
	fi
	echo "Gate satisfied: the check-removed model leaves the transfer permanently unresolved."
	echo "::endgroup::"

	orphan-leak:
	needs: changes
	if: needs.changes.outputs.orphan_leak == 'true' \|\| github.event_name == 'schedule'
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
	- uses: actions/setup-dotnet@a98b56852c35b8e3190ac28c8c2271da59106c68 # v6.0.0
	with:
	dotnet-version: '8.0.x'
	- name: Install the P checker
	run: \|
	dotnet tool install --global P --version 3.1.0 --configfile "$GITHUB_WORKSPACE/p/NuGet.config"
	echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
	- name: Compile
	run: \|
	cd p/orphan-leak
	p compile
	- name: Tests that must hold
	run: \|
	cd p/orphan-leak
	for tc in tcOrphanGuarded tcOrphanExplore; do
	echo "::group::$tc (expect hold)"
	p check -tc "$tc" -i 5000
	echo "::endgroup::"
	done
	echo "::group::tcOrphanExplore (PCT)"
	p check -tc tcOrphanExplore --sch-pct 10 -i 5000
	echo "::endgroup::"
	- name: Validation gate (removing the GC re-sweep must leak an orphan)
	run: \|
	cd p/orphan-leak
	echo "::group::tcOrphanBuggy (expect the liveness obligation to fail)"
	if p check -tc tcOrphanBuggy -i 2000; then
	echo "ERROR: tcOrphanBuggy passed; the model no longer leaks a transiently-failed delete."
	echo "Removing the GC re-sweep must leave an orphan permanently outstanding."
	exit 1
	fi
	if ! grep -rqF "hot state 'Dirty'" PCheckerOutput/BugFinding/; then
	echo "ERROR: the buggy run failed, but not via the OrphanEventuallyReclaimed liveness obligation."
	exit 1
	fi
	echo "Gate satisfied: the re-sweep-removed model leaks an orphan forever."
	echo "::endgroup::"

	tier-routing:
	needs: changes
	if: needs.changes.outputs.tier_routing == 'true' \|\| github.event_name == 'schedule'
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
	- uses: actions/setup-dotnet@a98b56852c35b8e3190ac28c8c2271da59106c68 # v6.0.0
	with:
	dotnet-version: '8.0.x'
	- name: Install the P checker
	run: \|
	dotnet tool install --global P --version 3.1.0 --configfile "$GITHUB_WORKSPACE/p/NuGet.config"
	echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
	- name: Compile
	run: \|
	cd p/tier-routing
	p compile
	- name: Tests that must hold
	run: \|
	cd p/tier-routing
	echo "::group::tcTierRoutingGuarded (expect hold)"
	p check -tc tcTierRoutingGuarded -i 5000
	echo "::endgroup::"
	- name: Validation gate (removing the first_chunk_id == -1 guard must misroute)
	run: \|
	cd p/tier-routing
	echo "::group::tcTierRoutingBuggy (expect the INV#4 silent remote skip)"
	if p check -tc tcTierRoutingBuggy -i 2000; then
	echo "ERROR: tcTierRoutingBuggy passed; the model no longer misroutes an empty-local read."
	echo "Removing the first_chunk_id =/= -1 guard must route a remote-only offset locally."
	exit 1
	fi
	if ! grep -rqF 'INV#4 violated: an offset held only by the remote tier' PCheckerOutput/BugFinding/; then
	echo "ERROR: the guard-removed run failed, but not with the expected INV#4 misrouting counterexample."
	exit 1
	fi
	echo "Gate satisfied: the guard-removed model routes a remote-only offset to the local tier."
	echo "::endgroup::"

	writer-fencing:
	needs: changes
	if: needs.changes.outputs.writer_fencing == 'true' \|\| github.event_name == 'schedule'
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
	- uses: actions/setup-dotnet@a98b56852c35b8e3190ac28c8c2271da59106c68 # v6.0.0
	with:
	dotnet-version: '8.0.x'
	- name: Install the P checker
	run: \|
	dotnet tool install --global P --version 3.1.0 --configfile "$GITHUB_WORKSPACE/p/NuGet.config"
	echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
	- name: Compile
	run: \|
	cd p/writer-fencing
	p compile
	- name: Tests that must hold
	run: \|
	cd p/writer-fencing
	for tc in tcFencingGuarded tcFencingExplore; do
	echo "::group::$tc (expect hold)"
	p check -tc "$tc" -i 5000
	echo "::endgroup::"
	done
	echo "::group::tcFencingExplore (PCT)"
	p check -tc tcFencingExplore --sch-pct 10 -i 5000
	echo "::endgroup::"
	- name: Validation gate (removing the epoch fence must allow split-brain)
	run: \|
	cd p/writer-fencing
	echo "::group::tcFencingUnguarded (expect the epoch regression)"
	if p check -tc tcFencingUnguarded -i 2000; then
	echo "ERROR: tcFencingUnguarded passed; the model no longer regresses the committed epoch."
	echo "Removing the epoch fence must let a deposed writer overwrite a newer one."
	exit 1
	fi
	if ! grep -rqF 'split-brain: committed epoch regressed' PCheckerOutput/BugFinding/; then
	echo "ERROR: the fence-removed run failed, but not with the expected split-brain regression."
	exit 1
	fi
	echo "Gate satisfied: the fence-removed model regresses the committed epoch."
	echo "::endgroup::"

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Mark manifests as pending during resolution #83

Workflow file

Mark manifests as pending during resolution #83

Uh oh!

Workflow file for this run