From 445af7e80f0efd17c706173ab8651f086660aabe Mon Sep 17 00:00:00 2001 From: Will Binns Date: Sun, 11 Oct 2026 13:16:28 +0000 Subject: [PATCH 1/7] Prior art and qualification path pages; Degradation-first nav item points to its section Prior art lists only verified references (von Neumann, Lyons and Vanderkulk, STAR, Sklaroff, Meyer, Lamport et al., Spector and Gifford, Rasmussen) with how Mru relates to each. Qualification path maps what exists to NPR 7150.2, NASA-STD-8739.8, ECSS-E-ST-40C and ECSS-Q-ST-80C by topic and makes no compliance claim. Metadata for both, and descriptions updated for the shrinking quorum, quorum crate and Dusk pages. --- src/data/metadata.json | 22 ++- src/data/nav.ts | 27 +++- src/pages/concepts/prior-art.astro | 175 +++++++++++++++++++++ src/pages/concepts/qualification.astro | 203 +++++++++++++++++++++++++ 4 files changed, 421 insertions(+), 6 deletions(-) create mode 100644 src/pages/concepts/prior-art.astro create mode 100644 src/pages/concepts/qualification.astro diff --git a/src/data/metadata.json b/src/data/metadata.json index 6002109..9e2bb0f 100644 --- a/src/data/metadata.json +++ b/src/data/metadata.json @@ -10,7 +10,7 @@ { "url": "https://docs.mru.space/concepts/shrinking-quorum/", "title": "Shrinking quorum · Mru Docs", - "description": "Vote on three replicas, compare on two, self-check on one. The rule, its Kani-proved guarantees, its cost, and how replicas are diagnosed.", + "description": "Vote on three replicas, compare on two, self-check on one. What Kani proves per tick, what is tested per run, the cost and the command path.", "ogTitle": "Shrinking quorum", "cardLabel": "Docs · Concepts", "schema": ["TechArticle", "BreadcrumbList"] @@ -23,10 +23,26 @@ "cardLabel": "Docs · Concepts", "schema": ["TechArticle", "BreadcrumbList"] }, + { + "url": "https://docs.mru.space/concepts/prior-art/", + "title": "Prior art and related work · Mru Docs", + "description": "TMR, degradable systems, Byzantine agreement, Space Shuttle redundancy management and deep-space fault protection, and how Mru relates.", + "ogTitle": "Prior art and related work", + "cardLabel": "Docs · Concepts", + "schema": ["TechArticle", "BreadcrumbList"] + }, + { + "url": "https://docs.mru.space/concepts/qualification/", + "title": "Qualification path · Mru Docs", + "description": "What exists for Mru against NPR 7150.2, NASA-STD-8739.8, ECSS-E-ST-40C and ECSS-Q-ST-80C, and what has not started. No compliance claim.", + "ogTitle": "Qualification path", + "cardLabel": "Docs · Concepts", + "schema": ["TechArticle", "BreadcrumbList"] + }, { "url": "https://docs.mru.space/core/quorum-crate/", "title": "quorum crate API reference · Mru Docs", - "description": "API reference for the quorum crate: Policy, Mode, Reply, Outcome, Verdict, decide(), Health. no_std, no allocation, four Kani proofs.", + "description": "API reference for the quorum crate: Policy, Mode, Reply, Outcome, Verdict, decide(), Health. no_std, no allocation, nine Kani proofs.", "ogTitle": "The quorum crate", "cardLabel": "Docs · Core runtime", "schema": ["TechArticle", "SoftwareSourceCode", "BreadcrumbList"] @@ -58,7 +74,7 @@ { "url": "https://docs.mru.space/simulation/dusk/", "title": "Dusk simulator reference · Mru Docs", - "description": "Run Dusk, the Monte Carlo of redundancy policies: options and defaults, the fault model, default results, sweeps and what it does not claim.", + "description": "Run Dusk, the Monte Carlo of redundancy policies: options, the fault model, results and their definitions, sweeps, ground support and limits.", "ogTitle": "Dusk", "cardLabel": "Docs · Simulation", "schema": ["TechArticle", "SoftwareSourceCode", "BreadcrumbList"] diff --git a/src/data/nav.ts b/src/data/nav.ts index 0774146..3abb441 100644 --- a/src/data/nav.ts +++ b/src/data/nav.ts @@ -1,5 +1,10 @@ // Docs navigation, from the DocsNav artboard. The nav follows concepts and // layers, not repository names. Prev/next follow PAGES. +// +// A page marks one item active: the item for the page itself. Items that link +// to a section of a page (an href with #) are never active; the page item is. +// So on /concepts/shrinking-quorum/ "Shrinking quorum" is active, not +// "Degradation-first" or "Graceful Degradation Index". export type NavId = | 'home' @@ -8,6 +13,8 @@ export type NavId = | 'quorum' | 'gdi' | 'layers' + | 'prior' + | 'qual' | 'crate' | 'cli' | 'proofs' @@ -36,10 +43,12 @@ export const NAV: NavGroup[] = [ { title: 'Concepts', items: [ - { id: 'dfp', label: 'Degradation-first', href: '/concepts/shrinking-quorum/' }, + { id: 'dfp', label: 'Degradation-first', href: '/concepts/shrinking-quorum/#degradation-first' }, { id: 'quorum', label: 'Shrinking quorum', href: '/concepts/shrinking-quorum/' }, { id: 'gdi', label: 'Graceful Degradation Index', href: '/concepts/shrinking-quorum/#gdi' }, { id: 'layers', label: 'Layers 0 to 5', href: '/concepts/architecture/' }, + { id: 'prior', label: 'Prior art', href: '/concepts/prior-art/' }, + { id: 'qual', label: 'Qualification path', href: '/concepts/qualification/' }, ], }, { @@ -87,7 +96,7 @@ export const PAGES: DocPage[] = [ { path: '/concepts/shrinking-quorum/', short: 'Shrinking quorum', - updated: '7 Oct 2026', + updated: '11 Oct 2026', file: 'src/pages/concepts/shrinking-quorum.astro', }, { @@ -96,10 +105,22 @@ export const PAGES: DocPage[] = [ updated: '11 Oct 2026', file: 'src/pages/concepts/architecture.astro', }, + { + path: '/concepts/prior-art/', + short: 'Prior art', + updated: '11 Oct 2026', + file: 'src/pages/concepts/prior-art.astro', + }, + { + path: '/concepts/qualification/', + short: 'Qualification path', + updated: '11 Oct 2026', + file: 'src/pages/concepts/qualification.astro', + }, { path: '/core/quorum-crate/', short: 'The quorum crate', - updated: '7 Oct 2026', + updated: '11 Oct 2026', source: 'quorum/src/lib.rs', file: 'src/pages/core/quorum-crate.astro', }, diff --git a/src/pages/concepts/prior-art.astro b/src/pages/concepts/prior-art.astro new file mode 100644 index 0000000..23f9a34 --- /dev/null +++ b/src/pages/concepts/prior-art.astro @@ -0,0 +1,175 @@ +--- +import DocsLayout from '../../layouts/DocsLayout.astro'; +import DocsEnd from '../../components/DocsEnd.astro'; +import Breadcrumbs from '../../components/Breadcrumbs.astro'; + +const crumbs = [ + { label: 'Docs', href: '/' }, + { label: 'Concepts', href: '/concepts/shrinking-quorum/' }, + { label: 'Prior art' }, +]; +--- + + +
+ +

Prior art and related work

+

+ The shrinking quorum builds on decades of work in fault-tolerant computing. Stepping down from three replicas to + two to one is not new. This page lists the work Mru draws on and how Mru relates to each. +

+ +

TMR and its origins

+
    +
  • +

    + von Neumann, 1956. Shows that reliable computation can be built from unreliable components + through redundancy. Mru: the shrinking quorum is one use of that idea, with the redundancy shrinking as parts + fail. +

    +

    + J. von Neumann, "Probabilistic Logics and the Synthesis of Reliable Organisms from Unreliable + Components," in C. E. Shannon and J. McCarthy (eds.), Automata Studies, Princeton University Press, 1956, + pp. 43-98. +

    +
    • +
  • +

    + Lyons and Vanderkulk, 1962. Triple modular redundancy with a majority vote, applied to + reliability. Mru: fixed TMR in this form is the baseline on these pages. With three replicas, the shrinking + quorum votes the same way. +

    +

    + R. E. Lyons and W. Vanderkulk, "The Use of Triple-Modular Redundancy to Improve Computer + Reliability," IBM Journal of Research and Development, 6(2):200-209, 1962.{' '} + doi:10.1147/rd.62.0200 +

    +
    • +
+ +

Degradable systems and performability

+
    +
  • +

    + Meyer, 1980. Defines performability, a measure that combines performance and reliability for + systems that degrade. Mru: Dusk's figure of merit, useful work summed over the whole decline, is a measure + of this kind. The whitepaper cites Meyer for it. +

    +

    + J. F. Meyer, "On Evaluating the Performability of Degradable Computing Systems," IEEE Transactions + on Computers, C-29(8):720-731, 1980.{' '} + doi:10.1109/TC.1980.1675654 +

    +
    • +
+ +

Byzantine agreement

+
    +
  • +

    + Lamport, Shostak and Pease, 1982. Sets the limits of agreement when faulty components can + give conflicting information to different parts of a system. Mru: the shrinking quorum assumes replicas that + are damaged, not malicious. It does not solve input agreement: all replicas must already have the same input. + See Open questions. +

    +

    + L. Lamport, R. Shostak and M. Pease, "The Byzantine Generals Problem," ACM Transactions on + Programming Languages and Systems, 4(3):382-401, 1982.{' '} + doi:10.1145/357172.357176 +

    +
    • +
+ +

Redundancy management on the Space Shuttle

+
    +
  • +

    + Sklaroff, 1976. The Shuttle's general-purpose computers ran as a redundant set. Voting + detected and identified two failures. The remaining two used comparison and self-test to tolerate a third. + Mru: degradation from voting to comparison to self-test is not new. Mru does it with no ground team. +

    +

    + J. R. Sklaroff, "Redundancy Management Technique for Space Shuttle Computers," IBM Journal of + Research and Development, 20(1):20-28, 1976.{' '} + doi:10.1147/rd.201.0020 +

    +
    • +
  • +

    + Spector and Gifford, 1984. A case study of the Shuttle's primary computer system. Mru: a + reference for how a flown redundant system was designed and managed. +

    +

    + A. Spector and D. Gifford, "The Space Shuttle Primary Computer System," Communications of the ACM, + 27(9):872-900, 1984. doi:10.1145/358234.358246 +

    +
    • +
+ +

Autonomous fault protection on deep-space missions

+
    +
  • +

    + Avizienis et al., 1971 (STAR). JPL's self-testing and repairing computer, designed for + outer-planet spacecraft. Standby spares replaced failed units by automatic recovery. Mru: autonomous recovery + in deep space is decades old. The shrinking quorum steps down instead of relying on spares. The F´{' '} + RedundancyManager can admit a spare after a known-answer test. +

    +

    + A. Avizienis, G. C. Gilley, F. P. Mathur, D. A. Rennels, J. A. Rohr and D. K. Rubin, "The STAR + (Self-Testing And Repairing) Computer: An Investigation of the Theory and Practice of Fault-Tolerant Computer + Design," IEEE Transactions on Computers, C-20(11):1312-1321, 1971.{' '} + doi:10.1109/T-C.1971.223133 +

    +
    • +
  • +

    + Rasmussen, 2008. Fundamentals of fault-tolerant design for spacecraft guidance, navigation + and control, from JPL. Mru: the shrinking quorum is one autonomous response to processor loss. It is not a + full fault-protection system and does not replace one. +

    +

    + R. D. Rasmussen, "GN&C Fault Protection Fundamentals," 31st Annual AAS Guidance and Control + Conference, Breckenridge, CO, 2008. Jet Propulsion Laboratory. Companion presentation:{' '} + NASA NTRS 20100020171. +

    +
    • +
+ + + + + + + +

What Mru adds

+
    +
  • + Autonomy with no ground team. The step-down from three replicas to one runs on board, with no + command from the ground. +
    • +
  • + A small decision core with proofs. The quorum crate is{' '} + no_std with no allocation. Kani proves four properties of decide() for every set of + three replies. See Kani proofs for the scope of each. +
    • +
  • + Published trade data. Dusk and the{' '} + bench publish what the step-down buys in useful work and what it costs in wrong + results, with the code to reproduce them. +
    • +
+ +
+ diff --git a/src/pages/concepts/qualification.astro b/src/pages/concepts/qualification.astro new file mode 100644 index 0000000..b5fc681 --- /dev/null +++ b/src/pages/concepts/qualification.astro @@ -0,0 +1,203 @@ +--- +import DocsLayout from '../../layouts/DocsLayout.astro'; +import DocsEnd from '../../components/DocsEnd.astro'; +import Breadcrumbs from '../../components/Breadcrumbs.astro'; + +const crumbs = [ + { label: 'Docs', href: '/' }, + { label: 'Concepts', href: '/concepts/shrinking-quorum/' }, + { label: 'Qualification path' }, +]; +--- + + +
+ +

Qualification path

+

+ What exists today, and the NASA and ECSS software standards it relates to. No qualification evidence exists yet. + Mru makes no compliance claim. +

+ +

Standards

+

This page maps Mru to four software standards, two from NASA and two from ECSS:

+
+ + + + + + + + + + + + + + + + + + + + + + + + + +
NumberTitle
NPR 7150.2NASA Software Engineering Requirements
NASA-STD-8739.8Software Assurance and Software Safety Standard
ECSS-E-ST-40CSpace engineering: Software
ECSS-Q-ST-80CSpace product assurance: Software product assurance
+
+

+ The tables below map by topic, not by clause. No clause of any standard has been checked against Mru. +

+ +

What exists

+

+ These activities run today. They are engineering evidence, not qualification evidence: none was planned, reviewed + or recorded under a standard. +

+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
ActivityWhat existsRelated standards
Unit tests + Unit tests of the core and the C interface, run in CI on every change. See{' '} + the quorum crate. + NPR 7150.2, ECSS-E-ST-40C
Formal proofs + Nine Kani proofs, four on the core and five on the C interface, run in CI on every change. Each has a + stated scope. See Kani proofs. + NPR 7150.2, NASA-STD-8739.8, ECSS-E-ST-40C, ECSS-Q-ST-80C
Continuous integration + Build and test on Linux x86_64, Linux ARM64 and macOS, plus static ARM Linux binaries tested under + emulation and a bare-metal ARM Cortex-M build. + NPR 7150.2, ECSS-E-ST-40C
Scenario tests + scripts/scenarios.sh runs the demo program and checks its output: faults, limits, resets and + the comparison with fixed TMR. + NPR 7150.2, ECSS-E-ST-40C
Bench + 300 runs per host with injected faults on three general-purpose processors. Not radiation testing, not + target hardware. See Bench. + NPR 7150.2, ECSS-E-ST-40C
F´ unit tests and system test + 37 unit tests of the F´ components, and a 60-case system test against the demo's counts. Not run + on flight hardware. See F´ components. + NPR 7150.2, ECSS-E-ST-40C
+
+ +

Not started

+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
ActivityStatusRelated standards
Software classification and criticalityNot startedNPR 7150.2, NASA-STD-8739.8, ECSS-Q-ST-80C
Requirements traceabilityNot startedNPR 7150.2, ECSS-E-ST-40C
Independent verification and validationNot startedNPR 7150.2, NASA-STD-8739.8, ECSS-E-ST-40C
Tool qualification (compiler, Kani, test tools)Not startedNPR 7150.2, ECSS-Q-ST-80C
Rust toolchain qualification plan: TODONot startedNPR 7150.2, ECSS-Q-ST-80C
Coding standard complianceNot startedNPR 7150.2, ECSS-Q-ST-80C
MC/DC structural coverageNot startedNPR 7150.2, ECSS-E-ST-40C
Software development and assurance plansNot startedNPR 7150.2, NASA-STD-8739.8, ECSS-E-ST-40C, ECSS-Q-ST-80C
+
+

+ Status as of 11 Oct 2026, flight v0.2.0. The F´ components and the C interface have numbered requirements, + each with a verification method, but no trace to mission or standard requirements. +

+ + + + +
+ From 8942c505f09dcc310a0e84214a972cdd0ae3b941 Mon Sep 17 00:00:00 2001 From: Will Binns Date: Sun, 11 Oct 2026 13:16:28 +0000 Subject: [PATCH 2/7] Shrinking quorum: proved per tick vs tested per run, two replicas, command path, open questions New lede without 'decides exactly as fixed TMR'. Each Kani harness is linked with its scope. Fixed TMR is framed as the baseline, not as what spacecraft fly; the Shuttle and degradable systems are cited as prior art. Adds the Degradation-First Principle and corollary (whitepaper section 5), the KAT outcomes at two replicas with their gaps, the command path, and open questions. The 1.34x states its no-ground-support assumption. A RISK-METRIC marker holds the place for Dusk's per-mission risk. --- src/pages/concepts/shrinking-quorum.astro | 196 ++++++++++++++++++++-- 1 file changed, 178 insertions(+), 18 deletions(-) diff --git a/src/pages/concepts/shrinking-quorum.astro b/src/pages/concepts/shrinking-quorum.astro index 5c15dc7..595422d 100644 --- a/src/pages/concepts/shrinking-quorum.astro +++ b/src/pages/concepts/shrinking-quorum.astro @@ -8,6 +8,7 @@ const crumbs = [ { label: 'Concepts', href: '/concepts/shrinking-quorum/' }, { label: 'Shrinking quorum' }, ]; +const proofs = 'https://github.com/mruspace/flight/blob/v0.2.0/quorum/src/lib.rs'; --- @@ -27,8 +32,14 @@ const crumbs = [

Shrinking quorum

- A redundancy policy: vote on three replicas, compare on two, self-check on one. It decides exactly as fixed TMR - while TMR can run, and continues after TMR stops. + A redundancy policy for unattended missions with no repair path: vote on three replicas, compare on two, + self-check on one. It keeps running on the last replica, where fixed TMR stops. +

+

+ Kani proves that, with two or more replicas alive, decide() gives the same outcome under both + policies, for every set of three replies. The shrinking quorum also sets diagnose at two replicas, so + it can retire a stuck replica and continue where fixed TMR stays in disagreement. Over a whole run, never less + than fixed TMR is tested, not proved.

The trouble with a fixed threshold

@@ -37,8 +48,20 @@ const crumbs = [ still detect a disagreement. One cannot outvote anything, so the system stops.

- With a repair crew in reach, stopping is safe: someone swaps the board. With no one in reach, stopping throws away - the last processor's whole remaining life. + Most fault tolerance assumes someone can step in eventually. With a ground team in reach, stopping is safe: the + team finds the fault and commands a fallback. With no one in reach, stopping throws away the last processor's + whole remaining life. +

+

+ Fixed TMR is the baseline on these pages because both policies give the same outcome while two or more replicas + live. It is not what most spacecraft fly. Most fly dual-string radiation-hardened processors with EDAC, watchdogs + and autonomous fault protection. Stepping down from three to two to one is not new either: the Space Shuttle's + redundant set of general-purpose computers did it, and Meyer gave degradable systems a measure, performability, in + 1980. See Prior art. +

+

+ What Mru adds: the step-down runs with no ground team, the decision core is small and checked with Kani, and the + trade data is published (Dusk, bench).

Three modes

@@ -92,24 +115,117 @@ const crumbs = [ {'}'} {'}'} -

What it guarantees

+

Degradation-first

+

The shrinking quorum applies the whitepaper's design principle:

+
+ Principle + + "A system intended to operate for millennia without intervention must treat its own physical decay, of + power, computation, memory, and thermal capacity, not as an exceptional fault to be handled, but as the + constant, governing condition around which every architectural decision is made." + +
+
+ Corollary + + "Capability is a depleting resource to be spent, not a fixed budget to be defended. The objective is not to + preserve function but to maximize the cumulative useful work extracted across the entire descent from full + capability to silence." + +
+

+ W. Binns, Mru whitepaper, section 5, + doi:10.5281/zenodo.20579438. Dashes in the original are shown as commas. +

+

+ For the shrinking quorum, the figure of merit is useful work over the whole decline, not correct operation at full + strength. Dusk measures it, along with the wrong results it costs. +

+ +

What is proved and what is tested

+

Proved (per tick)

+

+ Four Kani proofs on decide(). Each reply is any of Absent, Single or{' '} + Pair, with any u64 values, so each proof covers every set of three replies to{' '} + decide(). +

  • - Never less than fixed TMR. While TMR can still run, both policies make exactly the same - decision. They differ only after TMR has stopped. + + identical_while_tmr_can_run + + : with two or more replies present, both policies give the same outcome. It compares the outcome only, not the + mode or diagnose.
  • - It halts only with nothing left. Fixed TMR stops below two replicas. The shrinking quorum stops - at zero. + + tmr_stops_below_two + + : with fewer than two replies present, the fixed TMR outcome is Halted.
  • - Only agreed results go out. A delivered value came from at least two replicas, or from both - runs of the last replica's self-check. + + shrink_halts_only_with_nothing_left + + : the shrinking quorum's outcome is Halted if and only if no reply is present. +
    • +
  • + + delivers_only_agreed_values + + : if either policy delivers a value, at least two replies agree on it, or exactly one replica is alive and it + returned Pair(v, v).

- Each property is a Kani proof over every possible input, run in CI on every change. See{' '} - Kani proofs. + CI runs cargo kani -p quorum -p quorum-ffi on every change. Five more proofs show that the C + interface gives the core's answer. The proofs do not cover the health record, the diagnosis, the known-answer + test, timing, or the system over a run. See Kani proofs. +

+ +

Tested (per run)

+

Never less useful work than fixed TMR over a whole run is a test result, with these scopes:

+
    +
  • + Scenario tests. scripts/scenarios.sh in CI: ten seeds, two kill faults per run, + 20,000 ticks. Kill faults only. +
    • +
  • + Bench. 150 pairs of runs per host, five fault schedules, on three hosts with general-purpose + processors. The three replicas are processes on one host, not separate processors. No pair below fixed TMR. See{' '} + Bench. +
    • +
  • + Dusk. 10,000 simulated missions. The two policies are identical until fixed TMR stops, by + construction of the model, and a unit test checks it over 200 seeds. See Dusk. +
    • +
+ +

Two replicas

+

+ With two replicas left, decide() compares them. Equal values are delivered. Unequal values give{' '} + Detected, and nothing goes out that tick. Under the shrinking quorum it also sets{' '} + diagnose. Fixed TMR does not. +

+

+ The demo then runs a known-answer test (KAT) on both replicas: a fixed input whose result is known. There are + three cases. +

+
    +
  • + Both pass. Nothing is retired. The tick is lost, and nothing escalates. A persistent fault that + the KAT cannot see keeps every tick Detected. +
    • +
  • + Both fail or time out. Both are retired, and the run halts. Fixed TMR would keep comparing. +
    • +
  • + One fails. It is retired. The survivor goes on in self-check. +
    • +
+

+ This is the current behavior. The first two cases are gaps: no escalation for a fault the KAT cannot see, and a + halt where fixed TMR would go on.

What it costs

@@ -121,15 +237,30 @@ const crumbs = [ Trade In Dusk's default run, fixed TMR comes out ahead only if one wrong result costs more than 136 years of - useful work (95% CI 131 to 142). + useful work (95% CI 131 to 142). The run assumes no ground support after launch. Planned: a per-mission risk + metric from Dusk, the probability of at least one wrong result. + +

Command path

+

+ Self-check on one replica can deliver a few wrong results before the KAT catches a stuck fault. The KAT runs every{' '} + --kat-period ticks, 64 by default. An upset that hits both self-check runs alike can also get + through. +

+

+ This mode is for data products, not spacecraft commands, unless the mission adds its own command safety layer. + Integrators can gate commands on Verdict.mode: issue a command only when the mode is{' '} + Vote or Compare and the outcome is Deliver. See the{' '} + example. +

+

Health and diagnosis

A replica outvoted STRIKES = 3 times within STRIKE_WINDOW = 200 ticks is diagnosed with - a known-answer test: a fixed input whose result is known. Pass, and its strikes are cleared, because the upsets - were transient. Fail, and it is retired. + a known-answer test. Pass, and its strikes are cleared, on the assumption that the upsets were transient. Fail, + and it is retired. The strike record has unit tests, not proofs.

Graceful Degradation Index

@@ -139,6 +270,29 @@ const crumbs = [ decline.

+

Open questions

+
    +
  • + Common-mode faults, such as shared power, clock or thermal. Dusk models correlated deaths with{' '} + --p-corr. The demo models an upset that hits both self-check runs alike with{' '} + --common-mode. Neither models shared power, clock or thermal faults. +
    • +
  • + Input agreement between replicas. In the demo, all replicas get the same input because it is a + function of the tick. Real sensor inputs need an agreement step. Mru does not provide one yet. +
    • +
  • + Replica determinism under interrupts and scheduling. The replicas must compute the same bits. + In the demo this holds only because the task is a pure function of the tick. Neither Dusk nor the bench tests + it. +
    • +
  • + KAT coverage on real hardware. Dusk sets self-check coverage as a parameter,{' '} + --coverage. The bench's stuck fault returns the same wrong value for every input, so the KAT + always sees it. Neither measures the share of real hardware faults a KAT catches. +
    • +
+

Default results

- 
policy              useful      p10      p50      p90      service   wrong days
-                    mean y                                  mean y   mean / run
-fixed TMR             99.0     37.6     92.7    168.9         99.0        0.000
-standby simplex       83.1     38.4     78.3    134.0        166.4        0.603
-shrinking quorum     132.6     64.3    126.6    208.3        166.4        0.246
+ 
policy                     useful      p10      p50      p90      service   wrong days     risk
+                           mean y                                  mean y   mean / run   P(>=1)
+fixed TMR                    99.0     37.6     92.7    168.9         99.0        0.000     0.0%
+standby simplex              83.1     38.4     78.3    134.0        166.4        0.603    43.2%
+shrinking quorum            132.6     64.3    126.6    208.3        166.4        0.246    20.1%
+TMR + unchecked simplex     166.2     76.9    156.7    267.9        166.4       24.715    87.2%
+cold standby, aging 0.1     144.7     69.7    139.3    226.7        289.8        1.043    61.3%
+cold standby, aging 1.0      83.1     38.4     78.3    134.0        166.4        0.603    43.2%

- 1.34× the useful work of fixed TMR in total (95% CI 1.33× to 1.35×). This assumes no ground support after launch. - The gain falls to 1.00× when support never ends. See Ground support. Never less on any - single mission, by construction: the two policies are identical until fixed TMR stops. + {t('dusk.work_vs_tmr')} the useful work of fixed TMR in total (95% CI {ci('dusk.work_vs_tmr')}). This assumes no + ground support after launch. The gain falls to {t('dusk.ground.never')} when support never ends. See{' '} + Ground support. Never less on any single mission, by construction: the two policies are + identical until fixed TMR stops. Fixed TMR comes out ahead only if one wrong result costs more than{' '} + {t('dusk.break_even_years')} years of useful work (95% CI {ci('dusk.break_even_years')}), next to a risk of{' '} + {t('dusk.risk.shrink')} against {t('dusk.risk.tmr')}.

- Standby simplex is the nearest model here of dual-string with autonomous switchover. It runs one self-checking - processor at a time and swaps in the next when it dies. + Cold standby is the nearest model here of dual-string with autonomous switchover. Standby simplex is the same + design with spares that age as fast as a powered processor, so it equals cold standby at aging 1.0. See{' '} + Baselines.

What the columns mean

@@ -176,8 +196,8 @@ shrinking quorum 132.6 64.3 126.6 208.3
  • Useful. The sum over days of throughput credit for a correct delivered result: 1.0 for a vote day with at most one upset, 1.0 for a pair day with no upset, 0.5 (--selfcheck-throughput) for a - single self-check day with no upset, and 0 for lost, wrong and idle days. Shown as the mean in years, with the - 10th, 50th and 90th percentiles. + single self-check day with no upset, 1.0 for an unchecked day with no upset, and 0 for lost, wrong and idle + days. Shown as the mean in years, with the 10th, 50th and 90th percentiles.
  • Service. The first day the policy can never produce output again, or the horizon. For fixed @@ -187,7 +207,10 @@ shrinking quorum 132.6 64.3 126.6 208.3
  • Wrong days. Days whose delivered result was corrupted by an upset that nothing caught. One day is one result. Only a lone processor can make one: its self-check misses an upset with probability 1 minus{' '} - --coverage. Shown as the mean per mission. + --coverage, and an unchecked processor delivers every upset. Shown as the mean per mission. +
    • +
  • + Risk. The share of missions with at least one wrong day, with a paired bootstrap 95% CI.

    • @@ -195,12 +218,38 @@ shrinking quorum 132.6 64.3 126.6 208.3 delivers nothing.

    - +

    Baselines

    +

    + Fixed TMR is one baseline, not what most spacecraft fly. Two more act with no ground team, on the same fault + histories. +

    +
      +
    • + TMR + unchecked simplex steps down on its own, but its last processor does not check itself. It + isolates the value of self-check. The shrinking quorum does {t('dusk.work_vs_unchecked')} of its useful work and + makes {t('dusk.wrong_vs_unchecked')} of its wrong results (95% CI {ci('dusk.wrong_vs_unchecked')}). Risk:{' '} + {t('dusk.risk.unchecked')} against {t('dusk.risk.shrink')}. +
      • +
    • + Cold standby keeps one processor powered and switches on the next, in order, when it dies. The + active one self-checks. Here it has three strings, on the same hardware as TMR. Correlated deaths follow the + powered fault history, which slightly under-counts them for an unpowered spare. +
      • +
    +

    + How fast an unpowered spare ages is not known, so --sweep varies it from 0.1 to 1.0 of the powered + rate. Against cold standby, the shrinking quorum does {t('dusk.work_vs_cold.01')} the useful work at 0.1 (95% CI{' '} + {ci('dusk.work_vs_cold.01')}) and {t('dusk.work_vs_cold.10')} at 1.0 (95% CI {ci('dusk.work_vs_cold.10')}). Cold + standby does more useful work below an aging rate of about {t('dusk.cold.crossing')}. At every rate it has more + missions with a wrong result: {t('dusk.risk.cold_10')} to {t('dusk.risk.cold_01')}, against{' '} + {t('dusk.risk.shrink')}. With two strings (--nodes 2), the shrinking quorum does{' '} + {t('dusk.nodes2.work_vs_cold.01')} to {t('dusk.nodes2.work_vs_cold.10')} the useful work of cold standby. +

    Sweeps

    - --sweep varies each parameter the model cannot pin down. Across every row, the gain over fixed TMR - stays between 1.11× and 1.68×. Every row assumes no ground support after launch. + --sweep varies each parameter the model cannot pin down. Across every row, the gain over fixed TMR is{' '} + {t('dusk.sweep.range')}. Every row assumes no ground support after launch.

    Ground support

    diff --git a/src/styles/shared/site.css b/src/styles/shared/site.css index cba5bd5..9a3e64a 100644 --- a/src/styles/shared/site.css +++ b/src/styles/shared/site.css @@ -167,10 +167,25 @@ html.js .quorum-fallback { .log a.entry[hidden] { display: none; } -/* First section of a research entry: its heading sits on the top rule. */ -.entry-body > .article:first-child .body > h2:first-child { +/* Research entry sections: the space between sections sits above the section, + not on its heading, so a margin note starts level with its own heading + (the first heading sits on the top rule). */ +.entry-body > .article .body > h2:first-child { margin-top: 0; } +.entry-body > .article + .article { + margin-top: 56px; +} +/* A number cell that may wrap at its space on a narrow screen, e.g. a ratio + with the lowest seed in brackets: "1.50 (1.50)". */ +.tbl td.m.wrap { + white-space: normal; +} +/* A margin note is running text: the label on its own line, then links and + code inline. .note is a flex column for cards, which split it at each link. */ +.article .note { + display: block; +} /* Tablets (no canvas artboard): from 641 to 920 px the seven nav links and the button do not fit, so the header uses the phone menu, as below 640 px. */ From 02cf618c56349a1009b0e6a07ac71923303c54df Mon Sep 17 00:00:00 2001 From: Will Binns Date: Sun, 11 Oct 2026 13:44:50 +0000 Subject: [PATCH 7/7] Architecture page: Dusk numbers from claims.json --- src/pages/concepts/architecture.astro | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/pages/concepts/architecture.astro b/src/pages/concepts/architecture.astro index dcf739b..a2108c7 100644 --- a/src/pages/concepts/architecture.astro +++ b/src/pages/concepts/architecture.astro @@ -2,6 +2,7 @@ import DocsLayout from '../../layouts/DocsLayout.astro'; import DocsEnd from '../../components/DocsEnd.astro'; import Breadcrumbs from '../../components/Breadcrumbs.astro'; +import { t } from '../../data/claims'; const crumbs = [ { label: 'Docs', href: '/' }, @@ -309,9 +310,9 @@ const crumbs = [ standards
  • - Dusk: 10,000 missions, 1.34× the useful work of fixed TMR. This assumes no - ground support after launch. The gain falls to 1.00× when support never ends. See{' '} - Ground support. + Dusk: {t('dusk.runs')} missions, {t('dusk.work_vs_tmr')} the useful work of + fixed TMR. This assumes no ground support after launch. The gain falls to {t('dusk.ground.never')} when support + never ends. See Ground support.