diff --git a/README.md b/README.md index e19baadc..67a492cb 100644 --- a/README.md +++ b/README.md @@ -108,6 +108,7 @@ Here is a list of specs included in this repository which are validated by the C | [DAG-based Consensus](specifications/dag-consensus) | Giuliano Losa | | | ✔ | ✔ | | | [German Cache-Coherence Protocol](specifications/GermanProtocol) | Markus Kuppe | | | | ✔ | ✔ | | [FLASH Cache-Coherence Protocol](specifications/FlashProtocol) | Markus Kuppe | | | | ✔ | ✔ | +| [Stale-View Shrink (Mutual Inclusion)](specifications/StaleViewShrink) | Ceri John, Claude AI (Anthropic) | | | | ✔ | | ## Other Examples diff --git a/specifications/StaleViewShrink/README.md b/specifications/StaleViewShrink/README.md new file mode 100644 index 00000000..01a4b990 --- /dev/null +++ b/specifications/StaleViewShrink/README.md @@ -0,0 +1,83 @@ +# StaleViewShrink: safe contraction on stale views + +N nodes each hold a shared resource (here, one sector of a distributed hash +table). Any of them may decide to stop holding it, but at least R must always +remain. That is *R-mutual inclusion* (called *l-mutual inclusion* in the literature below), the mirror image of k-exclusion. There is +no coordinator. A node announces that it intends to leave, waits `D` ticks, +then re-checks against its own view of the world, which is up to `L` ticks old. + +The spec compares two re-check rules (`Rule` in the `.cfg`): + +- **`"tb"`, lowest-ID tie-break:** count lower-ID announcers as already gone; + leave if R would remain. +- **`"patient"`, "patient lowest":** count *every* other announcer as already + gone; leave if R would remain. If not, and only higher-ID announcers are + racing, keep the announcement and re-check next tick instead of withdrawing. + +## Structure and timing model + +Each node acts alone, in its own steps: `Announce(n)` and `Recheck(n)`. A step +reads only that node's own variables and a *view*: a snapshot of the system +published between 1 and `L` ticks earlier, chosen afresh at every re-check, so +a node's information can be a different age at each decision. + +Time is an explicit clock, `now`, advanced by its own action (`AdvanceTime`), +in the style of Abadi and Lamport's "old-fashioned recipe" for real time. +Nodes never read the clock. It stands for two assumptions: whatever a node acts +on is at most `L` ticks old (gossip delivers within a known bound, a synchronous +timing assumption rather than an asynchronous model), and a node's timer fires +after `D` ticks. `AdvanceTime` waits until every re-check that is due has +happened, and publishes the state at the end of each tick; `snapshots` stands +for what gossip has delivered. + +The rule needs the bound: a node deciding alone can only rule out that a holder +it still sees has already left if it knows how old its information can be. + +## References + +- Origin: dynamic storage-arc sizing in Holochain's kitsune2 DHT + ([holochain/kitsune2#160](https://github.com/holochain/kitsune2/issues/160)). + The rules, and the Python checker and Rust implementation this spec mirrors, + are in [ValiChord/polite-shrink](https://github.com/ValiChord/polite-shrink). + As far as we know, the rules are not published elsewhere. +- The problem: H. Kakugawa, "Mutual inclusion in asynchronous message-passing + distributed systems", JPDC 77 (2015); S. Kamei and H. Kakugawa, "An + asynchronous message-passing distributed algorithm for the global critical + section problem", [arXiv:1807.05674](https://arxiv.org/abs/1807.05674). + Their solutions use quorums and permission messages; this one uses neither. +- Announce, wait, then decide: the doorway of Lamport's bakery algorithm + (CACM 17(8), 1974). +- Timing: M. Abadi and L. Lamport, "An old-fashioned recipe for real time", + TOPLAS 16(5), 1994; L. Lamport, "Real-time model checking is really simple", + CHARME 2005. + +## Why it is instructive + +An earlier model of the same protocol let each node read the *current* holder +set atomically at re-check. Under that assumption both rules pass, and so does a +bare re-check with no tie-break at all. Giving nodes stale views changes the +verdict: + +| model | rule | wait | result | +|---|---|---|---| +| `StaleShrink.cfg` | patient | 1× the max lag | no error (`Safety` and `Progress`) | +| `StaleShrinkV6Wait2x.cfg` | patient | 2× | no error | +| `StaleShrinkV3Cascade.cfg` | tb | 2× | **`Safety` violated** | +| `StaleShrinkV6TooShort.cfg` | patient | 0.5× | **`Safety` violated** (control) | + +The tie-break fails to a **staggered cascade**: nodes 4, 3, 2 and 1 announce a +tick apart, in descending ID order, all two ticks stale. Each counts a higher-ID +announcer as staying, and that announcer has already left inside its blind +window. The last copy goes at tick 7. The patient rule never relies on a node +that might itself be leaving. It is safe whenever the wait is at least the +maximum lag, and it always lets someone leave. No rule is safe when the wait is +shorter than the lag, which is what the control shows. + +There are no crashes in this spec. The source repository, +, has an exhaustive Python checker +that agrees with every verdict here and adds a crash at any tick. It also has a +Rust implementation, including a forced run of the cascade on a real (in-memory) +network. + +Written by Ceri John with AI assistance (Claude, Anthropic). Apache-2.0, as in +the source repository. diff --git a/specifications/StaleViewShrink/StaleShrink.cfg b/specifications/StaleViewShrink/StaleShrink.cfg new file mode 100644 index 00000000..edffe880 --- /dev/null +++ b/specifications/StaleViewShrink/StaleShrink.cfg @@ -0,0 +1,12 @@ +\* V6, wait = 1x the max lag: expect no error. +SPECIFICATION Spec +CONSTANTS + Nodes = {1, 2, 3, 4} + R = 1 + L = 2 + D = 2 + Rule = "patient" +INVARIANTS + TypeOK + Safety + Progress diff --git a/specifications/StaleViewShrink/StaleShrink.tla b/specifications/StaleViewShrink/StaleShrink.tla new file mode 100644 index 00000000..c17dfaa5 --- /dev/null +++ b/specifications/StaleViewShrink/StaleShrink.tla @@ -0,0 +1,180 @@ +------------------------------- MODULE StaleShrink ------------------------------- +(***************************************************************************) +(* Safe contraction on stale views ("polite shrink"), for one sector that *) +(* every node initially holds. *) +(* *) +(* N nodes each hold a shared resource. Any of them may decide to stop *) +(* holding it, but at least R must always remain: R-mutual inclusion. No *) +(* node asks permission. A node announces that it intends to leave, waits *) +(* D ticks on its own timer, then re-checks against its own view of the *) +(* system, which is up to L ticks out of date, and either leaves, waits *) +(* a tick, or withdraws. *) +(* *) +(* The two re-check rules compared: *) +(* - "tb" (V3): count LOWER-id announcers as gone; leave if R remain. *) +(* - "patient" (V6): count EVERY other announcer as gone; leave if R *) +(* remain. If not, and some higher-id announcer is racing and no lower *) +(* one is, keep the announcement and re-check next tick instead of *) +(* withdrawing. *) +(* *) +(* STRUCTURE. Each node acts alone, in its own steps: Announce(n) and *) +(* Recheck(n). A step reads only that node's own variables (whether it *) +(* holds the sector, its timer intent[n], whether it has announced) and a *) +(* view: a snapshot of the system published between 1 and L ticks ago, *) +(* chosen afresh at every re-check, so a node's information can be a *) +(* different age at each decision. Time is modelled with an explicit *) +(* clock, now, advanced by its own action, in the style of Abadi and *) +(* Lamport's "old-fashioned recipe" for real time. Nodes never read now: *) +(* it stands for two timing assumptions, (1) whatever a node acts on is at *) +(* most L ticks old (gossip delivers within a known bound: a synchronous *) +(* timing assumption, not an asynchronous model), and (2) a node's timer *) +(* fires after D ticks. AdvanceTime is enabled only when no re-check is *) +(* due, so timers fire on time. When time advances, the current state is *) +(* published: snapshots stands for what gossip has delivered. *) +(* *) +(* The rule depends on the bound L: a node deciding alone can only rule out *) +(* that a holder it still sees has already left if it knows how old its *) +(* information can be. Announcements are unconstrained (any holder may *) +(* announce at any tick), so safety does not lean on the trigger. *) +(* *) +(* Expected results: *) +(* - tb, N=4, R=1, L=2, D=4: Safety is VIOLATED by a staggered cascade: *) +(* nodes announce in descending id order a tick apart, each counts a *) +(* higher-id announcer as staying, and that announcer has left inside *) +(* its blind window. *) +(* - patient, with D >= L: no error; and whenever anyone announced and a *) +(* copy could be spared, someone left (Progress). *) +(* - patient with D < L: Safety is violated: no rule is safe when the *) +(* wait is shorter than the staleness. *) +(* There are no deaths: every departure is a shrink, so Safety is "never *) +(* fewer than R holders". *) +(* *) +(* REFERENCES *) +(* - Origin: dynamic storage-arc sizing in Holochain's kitsune2 DHT *) +(* (github.com/holochain/kitsune2/issues/160). The rules, and the *) +(* Python checker and Rust implementation this spec mirrors, are in *) +(* github.com/ValiChord/polite-shrink (REPORT_stale_views.md). As far *) +(* as we know, the rules are not published elsewhere. *) +(* - The problem: H. Kakugawa, "Mutual inclusion in asynchronous message- *) +(* passing distributed systems", JPDC 77, 2015; S. Kamei and *) +(* H. Kakugawa, "An asynchronous message-passing distributed algorithm *) +(* for the global critical section problem", arXiv:1807.05674. There *) +(* the problem is called l-mutual inclusion; their solutions use quorums *) +(* and permission messages, this one uses neither. *) +(* - Announce, wait, then decide: the doorway of Lamport's bakery *) +(* algorithm (CACM 17(8), 1974). *) +(* - Timing: M. Abadi and L. Lamport, "An old-fashioned recipe for real *) +(* time", TOPLAS 16(5), 1994; L. Lamport, "Real-time model checking is *) +(* really simple", CHARME 2005. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets, Sequences + +CONSTANTS Nodes, \* node ids, ordered naturals, e.g. 1..4 + R, \* minimum number of holders + L, \* maximum age of a view, in ticks + D, \* wait between announcing and re-checking, in ticks + Rule \* "tb" (V3) or "patient" (V6) + +ASSUME /\ Nodes \subseteq Nat /\ Nodes # {} + /\ R \in Nat /\ L \in Nat \ {0} /\ D \in Nat \ {0} + /\ Rule \in {"tb", "patient"} + +\* Announcements may happen in ticks 0..Span-1: enough to cover every +\* relative offset between announcements, waits and view ages that matters. +Span == D + 2 * L + 1 +\* Room for every intent to resolve, including V6's waiting. +Horizon == Span + D + 2 + + (IF Rule = "patient" THEN Cardinality(Nodes) * (D + 2 * L + 2) ELSE 0) + +VARIABLES now, \* the clock (nodes never read it; see STRUCTURE) + holds, \* nodes holding the sector + intent, \* intent[n]: tick at which n re-checks; 0 = none + announced, \* nodes that have announced (each announces once) + snapshots \* the last (up to) L published <>, + \* oldest first; the last entry is tick now-1 + +vars == <> + +TypeOK == /\ now \in 0..Horizon + /\ holds \in SUBSET Nodes + /\ intent \in [Nodes -> 0..(Horizon + D)] + /\ announced \in SUBSET Nodes + /\ snapshots \in Seq((SUBSET Nodes) \X (SUBSET Nodes)) + /\ Len(snapshots) <= L + +Announcers == { n \in Nodes : intent[n] # 0 } + +Init == /\ now = 0 + /\ holds = Nodes + /\ intent = [n \in Nodes |-> 0] + /\ announced = {} + /\ snapshots = << >> + +\* A view of age a (1 <= a <= L): the state published at tick now - a. +\* snapshots holds ticks max(0, now-L)..now-1, so when now >= a the index +\* Len(snapshots) - a + 1 is valid. Before tick a nothing older exists yet, +\* and the initial state is seen. +View(a) == IF now >= a + THEN snapshots[Len(snapshots) - a + 1] + ELSE <> + +\* n's decision on a view: "go", "wait" or "withdraw". +Decide(n, view) == + LET hs == view[1] + its == view[2] + lower == { m \in its : m < n } + higher == { m \in its : m > n } + IN IF Rule = "tb" + THEN IF Cardinality((hs \ {n}) \ lower) >= R THEN "go" ELSE "withdraw" + \* eff: the holders n sees other than itself, counting every other + \* announcer as already gone. It is what n can rely on staying. + ELSE LET eff == Cardinality((hs \ {n}) \ (its \ {n})) + IN IF eff >= R THEN "go" + ELSE IF higher # {} /\ lower = {} THEN "wait" + ELSE "withdraw" + +\* n announces that it intends to leave, and sets its timer. +Announce(n) == + /\ now < Span + /\ n \in holds + /\ n \notin announced + /\ intent' = [intent EXCEPT ![n] = now + D] + /\ announced' = announced \cup {n} + /\ UNCHANGED <> + +\* n's timer fires: it re-checks on a view of some age a in 1..L. +Recheck(n) == + /\ n \in holds + /\ intent[n] = now + /\ intent[n] # 0 + /\ \E a \in 1..L : + LET d == Decide(n, View(a)) + IN /\ holds' = IF d = "go" THEN holds \ {n} ELSE holds + /\ intent' = [intent EXCEPT ![n] = IF d = "wait" THEN now + 1 ELSE 0] + /\ UNCHANGED <> + +\* Time advances once every re-check due now has happened; the state at the +\* end of the tick is published. +AdvanceTime == + /\ now < Horizon + /\ \A n \in holds : intent[n] # now \/ intent[n] = 0 + /\ now' = now + 1 + /\ snapshots' = LET s == Append(snapshots, <>) + IN IF Len(s) > L THEN Tail(s) ELSE s + /\ UNCHANGED <> + +Done == now = Horizon /\ UNCHANGED vars + +Next == \/ \E n \in Nodes : Announce(n) \/ Recheck(n) + \/ AdvanceTime + \/ Done + +Spec == Init /\ [][Next]_vars + +\* Never fewer than R holders (no deaths here, so any loss is a shrink's). +Safety == Cardinality(holds) >= R + +\* At the end, if anyone announced and a copy could be spared, someone left. +Progress == (now = Horizon /\ announced # {} /\ Cardinality(Nodes) > R) + => holds # Nodes +============================================================================= diff --git a/specifications/StaleViewShrink/StaleShrinkV3Cascade.cfg b/specifications/StaleViewShrink/StaleShrinkV3Cascade.cfg new file mode 100644 index 00000000..b1a9f016 --- /dev/null +++ b/specifications/StaleViewShrink/StaleShrinkV3Cascade.cfg @@ -0,0 +1,12 @@ +\* V3, wait = 2x the max lag: expect Safety violated by the staggered cascade (nodes 4,3,2,1 announce a tick apart). +SPECIFICATION Spec +CONSTANTS + Nodes = {1, 2, 3, 4} + R = 1 + L = 2 + D = 4 + Rule = "tb" +INVARIANTS + TypeOK + Safety + Progress diff --git a/specifications/StaleViewShrink/StaleShrinkV6TooShort.cfg b/specifications/StaleViewShrink/StaleShrinkV6TooShort.cfg new file mode 100644 index 00000000..e2c2a87f --- /dev/null +++ b/specifications/StaleViewShrink/StaleShrinkV6TooShort.cfg @@ -0,0 +1,12 @@ +\* Control: V6 with a wait SHORTER than the max lag: expect Safety violated (no rule is safe there). +SPECIFICATION Spec +CONSTANTS + Nodes = {1, 2, 3, 4} + R = 1 + L = 2 + D = 1 + Rule = "patient" +INVARIANTS + TypeOK + Safety + Progress diff --git a/specifications/StaleViewShrink/StaleShrinkV6Wait2x.cfg b/specifications/StaleViewShrink/StaleShrinkV6Wait2x.cfg new file mode 100644 index 00000000..90a246ad --- /dev/null +++ b/specifications/StaleViewShrink/StaleShrinkV6Wait2x.cfg @@ -0,0 +1,12 @@ +\* V6, wait = 2x the max lag: expect no error. +SPECIFICATION Spec +CONSTANTS + Nodes = {1, 2, 3, 4} + R = 1 + L = 2 + D = 4 + Rule = "patient" +INVARIANTS + TypeOK + Safety + Progress diff --git a/specifications/StaleViewShrink/manifest.json b/specifications/StaleViewShrink/manifest.json new file mode 100644 index 00000000..ce0f938a --- /dev/null +++ b/specifications/StaleViewShrink/manifest.json @@ -0,0 +1,48 @@ +{ + "sources": [ + "https://github.com/ValiChord/polite-shrink" + ], + "authors": [ + "Ceri John", + "Claude AI (Anthropic)" + ], + "tags": [], + "modules": [ + { + "path": "specifications/StaleViewShrink/StaleShrink.tla", + "features": [], + "models": [ + { + "path": "specifications/StaleViewShrink/StaleShrink.cfg", + "runtime": "00:00:02", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 16848, + "totalStates": 48663, + "stateDepth": 52 + }, + { + "path": "specifications/StaleViewShrink/StaleShrinkV6Wait2x.cfg", + "runtime": "00:00:03", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 43348, + "totalStates": 111445, + "stateDepth": 64 + }, + { + "path": "specifications/StaleViewShrink/StaleShrinkV3Cascade.cfg", + "runtime": "00:00:03", + "mode": "exhaustive search", + "result": "safety failure" + }, + { + "path": "specifications/StaleViewShrink/StaleShrinkV6TooShort.cfg", + "runtime": "00:00:02", + "mode": "exhaustive search", + "result": "safety failure" + } + ] + } + ] +}