Repository navigation
Add StaleViewShrink: safe contraction (mutual inclusion) on stale views - #243
Open
topeuph-ai wants to merge 1 commit into
Open
topeuph-ai wants to merge 1 commit into
topeuph-ai wants to merge 1 commit into
Conversation
N nodes share a resource and any may leave, but at least R must remain, with no coordinator and each node acting on a view up to L ticks old. Compares a lowest-ID tie-break with a "patient lowest" rule. Four models: two pass (Safety and Progress), one fails instructively (TLC finds a staggered cascade that breaks the tie-break), and one control fails because the wait is shorter than the staleness. An atomic-read model of the same protocol passes the broken rule; modelling staleness exposes it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds
specifications/StaleViewShrink: a coordinator-free "leave only if R remain" protocol (l-mutual inclusion, the mirror of k-exclusion) in which each node acts on a view of the world up toLticks old. It compares a lowest-ID tie-break with a "patient lowest" rule.StaleShrink.cfgSafetyandProgress)StaleShrinkV6Wait2x.cfgStaleShrinkV3Cascade.cfgSafetyviolated: TLC finds a staggered cascade that breaks the tie-breakStaleShrinkV6TooShort.cfgSafetyviolated: control, with the wait shorter than the stalenessWhy it may be instructive: an atomic-read model of the same protocol passes the broken rule, and even a bare re-check with no tie-break. Modelling staleness explicitly is what exposes the cascade.
All models run in under 30 s (1–23 s single-worker). Checked locally with
check_manifest_schema.py,check_manifest_files.py,check_markdown_table.pyandcheck_small_models.py(TLC 2.19).manifest.jsonwas written by hand:generate_manifest.pywould not run on Windows (tree_sitterLanguage()overflow). Licence: Apache-2.0, as in the source repository (https://github.com/ValiChord/polite-shrink), which also has a Python checker that agrees with every verdict here and a Rust implementation.Written by Ceri John with AI assistance (Claude, Anthropic).
🤖 Generated with Claude Code