From 4d3cc517a5d2b9898ac1ad7d2a9e72f8aa8cd586 Mon Sep 17 00:00:00 2001 From: Ceri John Date: Wed, 21 Oct 2026 12:24:50 +0100 Subject: [PATCH 1/2] StaleViewShrink: safe contraction (mutual inclusion) on stale views 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 Signed-off-by: Ceri John --- README.md | 1 + specifications/StaleViewShrink/README.md | 46 ++++++ .../StaleViewShrink/StaleShrink.cfg | 12 ++ .../StaleViewShrink/StaleShrink.tla | 140 ++++++++++++++++++ .../StaleViewShrink/StaleShrinkV3Cascade.cfg | 12 ++ .../StaleViewShrink/StaleShrinkV6TooShort.cfg | 12 ++ .../StaleViewShrink/StaleShrinkV6Wait2x.cfg | 12 ++ specifications/StaleViewShrink/manifest.json | 48 ++++++ 8 files changed, 283 insertions(+) create mode 100644 specifications/StaleViewShrink/README.md create mode 100644 specifications/StaleViewShrink/StaleShrink.cfg create mode 100644 specifications/StaleViewShrink/StaleShrink.tla create mode 100644 specifications/StaleViewShrink/StaleShrinkV3Cascade.cfg create mode 100644 specifications/StaleViewShrink/StaleShrinkV6TooShort.cfg create mode 100644 specifications/StaleViewShrink/StaleShrinkV6Wait2x.cfg create mode 100644 specifications/StaleViewShrink/manifest.json 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..dea81322 --- /dev/null +++ b/specifications/StaleViewShrink/README.md @@ -0,0 +1,46 @@ +# 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 *l-mutual inclusion*, 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. + +## 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..2de683bf --- /dev/null +++ b/specifications/StaleViewShrink/StaleShrink.cfg @@ -0,0 +1,12 @@ +\* V6, wait = 1x the max lag: expect no error (65,001 distinct states). +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..e4d0f2f9 --- /dev/null +++ b/specifications/StaleViewShrink/StaleShrink.tla @@ -0,0 +1,140 @@ +------------------------------- MODULE StaleShrink ------------------------------- +(***************************************************************************) +(* Polite shrink with STALE views, for one sector held by every node. *) +(* *) +(* PoliteShrink.tla lets a node execute against the CURRENT holder set, *) +(* read atomically. Under that assumption even a bare re-check is safe, so *) +(* it cannot tell the shrink rules apart. This spec gives each node a view *) +(* of the world as it was Lag[n] ticks ago, which is what the rules exist *) +(* to survive. It is the TLA+ form of spec/timed_check.py and follows its *) +(* semantics tick for tick: *) +(* *) +(* - Time advances in ticks. Each tick: (1) every intent due this tick *) +(* is re-checked, all against views from earlier ticks, so same-tick *) +(* decisions cannot see each other; (2) any holder that has not yet *) +(* announced may announce, executing D ticks later; (3) the tick's *) +(* holders and intenders are published to History. *) +(* - A node's view at tick t is the state published at tick t - Lag[n] *) +(* (the initial state if that is before tick 0). Lag is per node, *) +(* chosen nondeterministically from 1..L, so heterogeneous staleness is *) +(* covered. Only the last L published states can ever be read, so only *) +(* those are kept. *) +(* - Announcement is unconstrained (any tick, any subset), as in *) +(* PoliteShrink.tla: safety must not lean on the trigger being right. *) +(* *) +(* The two re-check rules: *) +(* - "tb" (V3): count LOWER-id intenders as gone; vacate if R remain. *) +(* - "patient" (V6): count EVERY other intender as gone; vacate if R *) +(* remain. If not, and some higher-id intender is racing and no lower *) +(* one is, keep the intent and re-check next tick instead of standing *) +(* down. *) +(* *) +(* Expected results (the same as timed_check.py): *) +(* - 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, same constants (and any D >= L): no error; and whenever *) +(* anyone announced, someone vacated (Progress). *) +(* *) +(* No deaths in this spec: every departure is a shrink, so Safety is *) +(* "never fewer than R holders". *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets, Sequences + +CONSTANTS Nodes, \* node ids, ordered naturals, e.g. 1..4 + R, \* redundancy target + L, \* maximum view lag, 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 that matters (as in timed_check.py). +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 t, \* current tick + lag, \* lag[n]: node n's view lag (fixed per behaviour) + holds, \* nodes holding the sector + intent, \* intent[n]: tick at which n re-checks; 0 = none + announced, \* nodes that have announced (each announces once) + recent \* the last (up to) L published <>, + \* oldest first; the last entry is tick t-1 + +vars == <> + +Intenders(f) == { n \in Nodes : f[n] # 0 } + +Init == /\ t = 0 + /\ lag \in [Nodes -> 1..L] + /\ holds = Nodes + /\ intent = [n \in Nodes |-> 0] + /\ announced = {} + /\ recent = << >> + +\* Node n's view at tick t: the state published at tick t - lag[n]. +View(n) == IF t >= lag[n] + THEN recent[Len(recent) - lag[n] + 1] + ELSE <> + +\* The decision for a due intent: "go", "wait" or "cancel". +Decide(n) == + LET hs == View(n)[1] + its == View(n)[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 "cancel" + ELSE LET eff == Cardinality((hs \ {n}) \ (its \ {n})) + IN IF eff >= R THEN "go" + ELSE IF higher # {} /\ lower = {} THEN "wait" + ELSE "cancel" + +Tick == + /\ t < Horizon + /\ LET due == { n \in holds : intent[n] # 0 /\ intent[n] = t } + go == { n \in due : Decide(n) = "go" } + wait == { n \in due : Decide(n) = "wait" } + holds1 == holds \ go + intent1 == [n \in Nodes |-> + IF n \in wait THEN t + 1 + ELSE IF n \in due THEN 0 + ELSE intent[n]] + eligible == IF t < Span + THEN { n \in holds1 : n \notin announced /\ intent1[n] = 0 } + ELSE {} + IN \E ann \in SUBSET eligible : + LET intent2 == [n \in Nodes |-> + IF n \in ann THEN t + D ELSE intent1[n]] + IN /\ holds' = holds1 + /\ intent' = intent2 + /\ announced' = announced \cup ann + /\ recent' = LET r == Append(recent, <>) + IN IF Len(r) > L THEN Tail(r) ELSE r + /\ t' = t + 1 + /\ UNCHANGED lag + +Done == t = Horizon /\ UNCHANGED vars + +Next == Tick \/ Done + +Spec == Init /\ [][Next]_vars + +TypeOK == /\ t \in 0..Horizon + /\ holds \subseteq Nodes + /\ announced \subseteq Nodes + /\ intent \in [Nodes -> 0..(Horizon + D)] + +\* 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 == (t = 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..755c39cb --- /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:08", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 65001, + "totalStates": 107209, + "stateDepth": 44 + }, + { + "path": "specifications/StaleViewShrink/StaleShrinkV6Wait2x.cfg", + "runtime": "00:00:23", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 245146, + "totalStates": 364922, + "stateDepth": 56 + }, + { + "path": "specifications/StaleViewShrink/StaleShrinkV3Cascade.cfg", + "runtime": "00:00:14", + "mode": "exhaustive search", + "result": "safety failure" + }, + { + "path": "specifications/StaleViewShrink/StaleShrinkV6TooShort.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "safety failure" + } + ] + } + ] +} From ddc724009d6e9968c4b5ef24b0888aeb174b7ff2 Mon Sep 17 00:00:00 2001 From: Ceri John Date: Wed, 21 Oct 2026 12:24:51 +0100 Subject: [PATCH 2/2] StaleViewShrink: per-node actions, explicit clock, references Addresses review: each node acts in its own steps, Announce(n) and Recheck(n), reading only its own variables and a view published 1..L ticks earlier, chosen afresh at every re-check. Time is an explicit clock advanced by AdvanceTime once every due re-check has happened (Abadi-Lamport style); nodes never read it. This also removes the per-node fixed lag. TypeOK follows the variables and covers all of them; comments on the snapshots index and on eff; renamed to R-mutual inclusion; references to the origin and to the literature. Results unchanged: both V6 models pass (16,848 and 43,348 distinct states), the V3 cascade and the short-wait control violate Safety. Co-Authored-By: Claude Opus 5.5 Signed-off-by: Ceri John --- specifications/StaleViewShrink/README.md | 39 +++- .../StaleViewShrink/StaleShrink.tla | 213 +++++++++++------- specifications/StaleViewShrink/manifest.json | 20 +- 3 files changed, 175 insertions(+), 97 deletions(-) diff --git a/specifications/StaleViewShrink/README.md b/specifications/StaleViewShrink/README.md index dea81322..01a4b990 100644 --- a/specifications/StaleViewShrink/README.md +++ b/specifications/StaleViewShrink/README.md @@ -2,7 +2,7 @@ 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 *l-mutual inclusion*, the mirror image of k-exclusion. There is +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. @@ -14,6 +14,43 @@ The spec compares two re-check rules (`Rule` in the `.cfg`): 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 diff --git a/specifications/StaleViewShrink/StaleShrink.tla b/specifications/StaleViewShrink/StaleShrink.tla index e4d0f2f9..8ecc9348 100644 --- a/specifications/StaleViewShrink/StaleShrink.tla +++ b/specifications/StaleViewShrink/StaleShrink.tla @@ -1,50 +1,77 @@ ------------------------------- MODULE StaleShrink ------------------------------- (***************************************************************************) -(* Polite shrink with STALE views, for one sector held by every node. *) +(* Safe contraction on stale views ("polite shrink"), for one sector that *) +(* every node initially holds. *) (* *) -(* PoliteShrink.tla lets a node execute against the CURRENT holder set, *) -(* read atomically. Under that assumption even a bare re-check is safe, so *) -(* it cannot tell the shrink rules apart. This spec gives each node a view *) -(* of the world as it was Lag[n] ticks ago, which is what the rules exist *) -(* to survive. It is the TLA+ form of spec/timed_check.py and follows its *) -(* semantics tick for tick: *) +(* 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. *) (* *) -(* - Time advances in ticks. Each tick: (1) every intent due this tick *) -(* is re-checked, all against views from earlier ticks, so same-tick *) -(* decisions cannot see each other; (2) any holder that has not yet *) -(* announced may announce, executing D ticks later; (3) the tick's *) -(* holders and intenders are published to History. *) -(* - A node's view at tick t is the state published at tick t - Lag[n] *) -(* (the initial state if that is before tick 0). Lag is per node, *) -(* chosen nondeterministically from 1..L, so heterogeneous staleness is *) -(* covered. Only the last L published states can ever be read, so only *) -(* those are kept. *) -(* - Announcement is unconstrained (any tick, any subset), as in *) -(* PoliteShrink.tla: safety must not lean on the trigger being right. *) +(* 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. *) (* *) -(* The two re-check rules: *) -(* - "tb" (V3): count LOWER-id intenders as gone; vacate if R remain. *) -(* - "patient" (V6): count EVERY other intender as gone; vacate if R *) -(* remain. If not, and some higher-id intender is racing and no lower *) -(* one is, keep the intent and re-check next tick instead of standing *) -(* down. *) +(* 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. *) (* *) -(* Expected results (the same as timed_check.py): *) +(* 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, same constants (and any D >= L): no error; and whenever *) -(* anyone announced, someone vacated (Progress). *) +(* - 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". *) (* *) -(* No deaths in this spec: 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, \* redundancy target - L, \* maximum view lag, in ticks + 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) @@ -53,88 +80,102 @@ ASSUME /\ Nodes \subseteq Nat /\ Nodes # {} /\ Rule \in {"tb", "patient"} \* Announcements may happen in ticks 0..Span-1: enough to cover every -\* relative offset that matters (as in timed_check.py). +\* 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 t, \* current tick - lag, \* lag[n]: node n's view lag (fixed per behaviour) +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) - recent \* the last (up to) L published <>, - \* oldest first; the last entry is tick t-1 + snapshots \* the last (up to) L published <>, + \* oldest first; the last entry is tick now-1 + +vars == <> -vars == <> +TypeOK == /\ now \in 0..Horizon + /\ holds \subseteq Nodes + /\ intent \in [Nodes -> 0..(Horizon + D)] + /\ announced \subseteq Nodes + /\ Len(snapshots) <= L + /\ \A i \in 1..Len(snapshots) : + snapshots[i] \in (SUBSET Nodes) \X (SUBSET Nodes) -Intenders(f) == { n \in Nodes : f[n] # 0 } +Announcers == { n \in Nodes : intent[n] # 0 } -Init == /\ t = 0 - /\ lag \in [Nodes -> 1..L] +Init == /\ now = 0 /\ holds = Nodes /\ intent = [n \in Nodes |-> 0] /\ announced = {} - /\ recent = << >> - -\* Node n's view at tick t: the state published at tick t - lag[n]. -View(n) == IF t >= lag[n] - THEN recent[Len(recent) - lag[n] + 1] + /\ 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 <> -\* The decision for a due intent: "go", "wait" or "cancel". -Decide(n) == - LET hs == View(n)[1] - its == View(n)[2] +\* 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 "cancel" + 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 "cancel" - -Tick == - /\ t < Horizon - /\ LET due == { n \in holds : intent[n] # 0 /\ intent[n] = t } - go == { n \in due : Decide(n) = "go" } - wait == { n \in due : Decide(n) = "wait" } - holds1 == holds \ go - intent1 == [n \in Nodes |-> - IF n \in wait THEN t + 1 - ELSE IF n \in due THEN 0 - ELSE intent[n]] - eligible == IF t < Span - THEN { n \in holds1 : n \notin announced /\ intent1[n] = 0 } - ELSE {} - IN \E ann \in SUBSET eligible : - LET intent2 == [n \in Nodes |-> - IF n \in ann THEN t + D ELSE intent1[n]] - IN /\ holds' = holds1 - /\ intent' = intent2 - /\ announced' = announced \cup ann - /\ recent' = LET r == Append(recent, <>) - IN IF Len(r) > L THEN Tail(r) ELSE r - /\ t' = t + 1 - /\ UNCHANGED lag - -Done == t = Horizon /\ UNCHANGED vars - -Next == Tick \/ Done + 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 -TypeOK == /\ t \in 0..Horizon - /\ holds \subseteq Nodes - /\ announced \subseteq Nodes - /\ intent \in [Nodes -> 0..(Horizon + D)] - \* 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 == (t = Horizon /\ announced # {} /\ Cardinality(Nodes) > R) +Progress == (now = Horizon /\ announced # {} /\ Cardinality(Nodes) > R) => holds # Nodes ============================================================================= diff --git a/specifications/StaleViewShrink/manifest.json b/specifications/StaleViewShrink/manifest.json index 755c39cb..ce0f938a 100644 --- a/specifications/StaleViewShrink/manifest.json +++ b/specifications/StaleViewShrink/manifest.json @@ -14,31 +14,31 @@ "models": [ { "path": "specifications/StaleViewShrink/StaleShrink.cfg", - "runtime": "00:00:08", + "runtime": "00:00:02", "mode": "exhaustive search", "result": "success", - "distinctStates": 65001, - "totalStates": 107209, - "stateDepth": 44 + "distinctStates": 16848, + "totalStates": 48663, + "stateDepth": 52 }, { "path": "specifications/StaleViewShrink/StaleShrinkV6Wait2x.cfg", - "runtime": "00:00:23", + "runtime": "00:00:03", "mode": "exhaustive search", "result": "success", - "distinctStates": 245146, - "totalStates": 364922, - "stateDepth": 56 + "distinctStates": 43348, + "totalStates": 111445, + "stateDepth": 64 }, { "path": "specifications/StaleViewShrink/StaleShrinkV3Cascade.cfg", - "runtime": "00:00:14", + "runtime": "00:00:03", "mode": "exhaustive search", "result": "safety failure" }, { "path": "specifications/StaleViewShrink/StaleShrinkV6TooShort.cfg", - "runtime": "00:00:01", + "runtime": "00:00:02", "mode": "exhaustive search", "result": "safety failure" }