20,000 ticks per run. Results for all three upset rates are in the JSON files.
In all 150 pairs of runs, the shrinking quorum delivered at least as many correct results as fixed TMR on the same
- seed and faults. While two or more replicas live, both policies make the same decision, as the{' '}
- Kani proofs show. The gain comes after TMR stops: TMR halts at the second
- loss, or, in the stuck schedule, keeps comparing a good replica with a stuck one and rejects every result.
+ seed and faults. This is a test result over these runs, not a proof. On the same replies, both policies give the
+ same outcome each tick, as the Kani proofs show. The runs differ because
+ the shrinking quorum keeps going and retires bad replicas: TMR halts at the second loss, or, in the stuck
+ schedule, keeps comparing a good replica with a stuck one and rejects every result.
Wrong results
@@ -345,6 +375,116 @@ const results = 'https://github.com/mruspace/flight/tree/main/bench/results';
--kat-period gives fewer wrong results and less throughput.
+ Known-answer test coverage
+
+ On the last replica, self-check cannot see a fault that gives the same wrong answer twice. Only the periodic
+ known-answer test can catch it, and only if the fault changes the test's answer.{' '}
+ scripts/kat-coverage.sh measures this: it kills two replicas, injects one fault into the last one,
+ and records whether the voter caught it, how fast, and how many wrong results got out first. Results:{' '}
+
+ {CLAIM_SOURCES.flight.kat}
+
+ .
+
+
+ Scope. These figures come from the demo task on a general-purpose processor: three replica processes on one host,
+ each hashing a 4 KiB block with FNV-1a, with faults the voter injects by command. The test sends one input (tick
+ 0) and compares one 64-bit result. The fractions are properties of that task, that input and this fault model.
+ They are not properties of flight hardware or of any flight software. A stuck-at bit is one bit of the input, the
+ working block, the hash accumulator or the result, forced to 0 or 1 from a chosen tick. A bit flip changes one bit
+ of the working block during one computation. The campaign does not cover faults in the voter, the operating system
+ or the links between processes. It is not a radiation test, and the F´ components do not model stuck-at bits.
+
+
+
+
+
+ | Fault on the last replica |
+ Faults |
+ Detected |
+ Ticks to detect, mean (max) |
+ Wrong before detection, mean (max) |
+ Missed, wrong results |
+ Missed, no effect |
+
+
+
+ {KAT.map((r) => (
+
+ | {r.label} |
+ {r.d.runs} |
+ {r.pct} |
+
+ {n1(r.d.latency_mean)} ({n1(r.d.latency_max)})
+ |
+
+ {n1(r.d.wrong_before_detection_mean)} ({n1(r.d.wrong_before_detection_max)})
+ |
+ {r.d.missed_with_wrong} |
+ {r.d.missed_no_effect} |
+
+ ))}
+
+
+
+ Test every 64 ticks. Missed, wrong results: the test never caught the fault and wrong results were delivered.
+ Missed, no effect: the fault changed nothing in the run. Bit flips are caught by self-check, not by the
+ known-answer test; the share is the chance that both runs get the same flip.
+
+
+ -
+ One test input sees about half of the stuck-at bits. A stuck bit shows only when it changes the
+ answer to the one test input. A stuck-at-0 bit on the input never does, because the input is 0. The input faults
+ marked "no effect" changed nothing only because these short runs never set those bits.
+
+ -
+ A missed stuck-at bit keeps delivering wrong results. For a stuck bit in the result, about half
+ of all later results are wrong, and nothing flags them.
+
+ -
+ Fix, planned: a second test input would make most of these visible. It is not built.
+
+
+
+ Test period
+
+
+
+
+ | Period, ticks |
+ Stuck results detected |
+ Ticks to detect, mean (max) |
+ Wrong before detection, mean (max) |
+ Tests per delivered result |
+ Extra CPU, measured (median) |
+
+
+
+ {PERIODS.map((r) => (
+
+ | {r.p} |
+ {r.pct} |
+
+ {n1(r.d.latency_mean)} ({n1(r.d.latency_max)})
+ |
+
+ {n1(r.d.wrong_before_detection_mean)} ({n1(r.d.wrong_before_detection_max)})
+ |
+ {r.tests} |
+ {r.cpu ? r.cpu.text : 'not measured'} |
+
+ ))}
+
+
+
+ Stuck results: 256 per period, one for every phase of the test. The test count is exact. The CPU column is the
+ median of 10 runs of 100,000 ticks against the same runs with no test, on one host. It includes the request round
+ trip, so it is above the share of extra computations. From period 32 up, it is smaller than the run-to-run spread
+ (about 6% of the median): read it as a few percent at most, not a precise value.
+
+
Cost of the core
The bench crate times quorum::decide() and Health::strike() with{' '}
@@ -453,8 +593,8 @@ const results = 'https://github.com/mruspace/flight/tree/main/bench/results';
Run it
# in a clone of mruspace/flight
-./scripts/bench.sh # 300 runs, about 2 minutes on an Apple M4
-./scripts/bench.sh --quick # 2 seeds, 5,000 ticks
+./scripts/bench.sh # 300 runs, about 3 minutes on an Apple M4
+./scripts/bench.sh --quick # 2 seeds, 5,000 ticks, about 15 s
cargo run --release -p bench # the cost of the core only
The script writes bench/results/<date>-<host>.json and .csv, with the host,
diff --git a/src/pages/core/fprime.astro b/src/pages/core/fprime.astro
index aab51a4..dbf6918 100644
--- a/src/pages/core/fprime.astro
+++ b/src/pages/core/fprime.astro
@@ -238,8 +238,10 @@ void quorum_health_clear(quorum_health *health, uint32_t replica);
Only plain values cross. The health record lives in the caller's memory. Out-of-range input gets the safe
answer: a policy that is not 0 or 1 halts, an unknown reply kind counts as absent, a replica above 2 changes
- nothing, and a null pointer does the same. Five Kani proofs show that each function gives the core's answer
- for every valid input and the safe answer for every other.
+ nothing, and a null pointer does the same. Five Kani proofs show that quorum_mode,{' '}
+ quorum_decide, quorum_health_strike and quorum_health_clear give the
+ core's answer for every valid input, and the safe answer for a bad policy, an unknown reply kind or a replica
+ above 2. Unit tests check the null pointers. See Kani proofs.
Verification
diff --git a/src/pages/core/quorum-cli.astro b/src/pages/core/quorum-cli.astro
index b59256d..91815b2 100644
--- a/src/pages/core/quorum-cli.astro
+++ b/src/pages/core/quorum-cli.astro
@@ -37,7 +37,7 @@ const crumbs = [
Synopsis
quorum [--policy shrink|tmr] [--ticks N] [--seed S]
[--upset-rate R] [--common-mode C] [--kat-period P]
- [--fault kill|corrupt|stuck|hang|sensor:I@T] ... [--faults-file F]
+ [--fault kill|corrupt|stuck|hang|sensor:I@T | stuckbit:I@T/LOC.BIT.V] ... [--faults-file F]
[--max-memory-mb M] [--max-cpu-seconds S] [--cpu-percent P]
[--max-seconds S] [--reply-timeout-ms T]
[--sensor-mb M] [--sensor-every N]
@@ -120,7 +120,20 @@ const crumbs = [
| corrupt |
- One bit flips in the replica's working memory during a computation. |
+
+ One bit flips in the replica's working memory during its next computation. (In v0.2.0, a corrupt fault
+ on an odd tick in self-check mode was lost. Fixed after v0.2.0.)
+ |
+
+
+ | stuckbit |
+
+ stuckbit:I@T/LOC.BIT.V: from tick T, bit BIT of LOC is forced to V (0 or 1), in both
+ self-check runs and in the known-answer test. LOC is in (the input, bits 0 to 63),{' '}
+ block (the 4 KiB working block, bits 0 to 32767), acc (the hash accumulator, 0
+ to 63) or out (the result, 0 to 63). Added after v0.2.0. See{' '}
+ known-answer test coverage.
+ |
| sensor |
@@ -190,15 +203,23 @@ const crumbs = [
stopped, halted and sensor flips. --progress-every N adds running totals.{' '}
--summary file.txt writes the final report for downlink.
- quorum --policy shrink ... useful=14989 detected=11 wrong=0 halted_at=never
+
+ The run from the Quickstart,{' '}
+ --policy shrink --ticks 20000 --seed 1 --upset-rate 0.001 --fault kill:0@5000 --fault kill:1@10000,
+ prints:
+
+ policy=shrink ticks=20000 seed=1 upset_rate=0.001
+useful=14989 detected=11 wrong=0 halted_at=never alive_at_end=1 stopped=completed last_useful=20000
+footprint: voter_max_rss=1920KiB replica_max_rss=1808KiB cpu=0.48s wall=0.46s
+limits: memory=128MB/process cpu_time=none cpu_share=none max_run=none reply_timeout=2000ms
+
+ flight v0.2.0 on an Apple M4. The footprint line varies by host.
+
- The summary also gives last_useful, the tick of the last correct result. With a scheduled stuck, hang
- or corrupt fault, it adds a detection: line: the faults injected, how many the voter caught, and the
- mean and longest ticks from fault to first reaction. The bench runs this program over a
- matrix of faults.
+ last_useful is the tick of the last correct result. With a scheduled stuck, hang or corrupt fault,
+ the output adds a detection: line (also for stuckbit, after v0.2.0): the faults
+ injected, how many the voter caught, and the mean and longest ticks from fault to first reaction. The{' '}
+ bench runs this program over a matrix of faults.
Resets and power cuts
@@ -221,8 +242,9 @@ const crumbs = [
On OPS-SAT
- opssat/run.sh starts, checks and stops a run with all limits set. Tagged releases ship each static
- Linux binary (three ARM, one x86_64) with the launcher, a sample fault schedule and the operations note.
+ For a proposed experiment on ESA's OPS-SAT. The experiment has not been accepted. opssat/run.sh{' '}
+ starts, checks and stops a run with all limits set. Tagged releases ship each static Linux binary (three ARM, one
+ x86_64) with the launcher, a sample fault schedule and the operations note.
diff --git a/src/pages/core/quorum-crate.astro b/src/pages/core/quorum-crate.astro
index 03fe810..51296cf 100644
--- a/src/pages/core/quorum-crate.astro
+++ b/src/pages/core/quorum-crate.astro
@@ -17,6 +17,7 @@ const crumbs = [
toc={[
{ href: '#install', label: 'Install' },
{ href: '#example', label: 'Example' },
+ { href: '#gate', label: 'Gate commands' },
{ href: '#api', label: 'API' },
{ href: '#proofs', label: 'Kani proofs' },
{ href: '#targets', label: 'Targets and builds' },
@@ -36,7 +37,7 @@ const crumbs = [
no allocation
no dependencies
- 4 Kani proofs
+ 9 Kani proofs
v0.2.0
@@ -65,6 +66,66 @@ quorum = {'{'} git = "https://github.com/mruspace/flight"
{'}'}
{'}'}
+ Gate commands on the mode
+
+ On one replica, self-check can deliver a few wrong results before the periodic known-answer test catches a stuck
+ fault. Use that mode for data products, not spacecraft commands, unless the mission adds its own command safety
+ layer. This example issues a command only when the mode is Vote or Compare and the
+ outcome is Deliver. See Command path.
+
+ //! Gate commands on the mode. Only a result that two or more replicas agree
+//! on (vote or compare) may command the spacecraft. A result from the last
+//! replica's self-check goes out as a data product only.
+use quorum::{'{'}decide, Mode, Outcome, Policy, Reply, REPLICAS{'}'};
+
+/// What to do with one tick's result.
+enum Action {'{'}
+ /// Agreed by two or more replicas: may be used as a command.
+ Command(u64),
+ /// Self-check on the last replica: data product only.
+ Data(u64),
+ /// Nothing to send this tick.
+ Hold,
+{'}'}
+
+fn gate(replies: &[Reply; REPLICAS]) -> Action {'{'}
+ let verdict = decide(Policy::Shrink, replies);
+ match (verdict.mode, verdict.outcome) {'{'}
+ (Mode::Vote | Mode::Compare, Outcome::Deliver(x)) => Action::Command(x),
+ (Mode::SelfCheck, Outcome::Deliver(x)) => Action::Data(x),
+ _ => Action::Hold,
+ {'}'}
+{'}'}
+
+fn main() {'{'}
+ use Reply::{'{'}Absent, Pair, Single{'}'};
+ let ticks = [
+ [Single(7), Single(7), Single(9)], // vote: two agree on 7
+ [Absent, Single(7), Single(7)], // compare: both say 7
+ [Absent, Single(7), Single(9)], // compare: mismatch
+ [Absent, Absent, Pair(7, 7)], // self-check on the last replica
+ [Absent, Absent, Absent], // nothing left
+ ];
+ for replies in &ticks {'{'}
+ match gate(replies) {'{'}
+ Action::Command(x) => println!("{'{'}replies:?{'}'}: command {'{'}x{'}'}"),
+ Action::Data(x) => println!("{'{'}replies:?{'}'}: data product {'{'}x{'}'}"),
+ Action::Hold => println!("{'{'}replies:?{'}'}: hold"),
+ {'}'}
+ {'}'}
+{'}'}
+
+ Its output, from cargo run against v0.2.0:
+
+ [Single(7), Single(7), Single(9)]: command 7
+[Absent, Single(7), Single(7)]: command 7
+[Absent, Single(7), Single(9)]: hold
+[Absent, Absent, Pair(7, 7)]: data product 7
+[Absent, Absent, Absent]: hold
+
API
const REPLICAS: usize = 3
Number of replicas.
@@ -190,13 +251,16 @@ quorum = {'{'} git = "https://github.com/mruspace/flight"
reset or hand it to C.
- From C or C++, use the C interface, quorum.h. Kani proves that each of
- its functions gives this crate's answer.
+ From C or C++, use the C interface, quorum.h. Kani proves that{' '}
+ quorum_mode, quorum_decide, quorum_health_strike and{' '}
+ quorum_health_clear give this crate's answer.
Kani proofs
- Run with cargo kani -p quorum. Each holds for every possible input.
+ Nine proofs: four on the core in quorum, five on the C interface in quorum-ffi. CI runs
+ cargo kani -p quorum -p quorum-ffi on every change. In the core proofs, each reply is any of
+ Absent, Single or Pair, with any u64 values.
@@ -204,28 +268,129 @@ quorum = {'{'} git = "https://github.com/mruspace/flight"
| Proof |
Property |
+ Scope |
- | identical_while_tmr_can_run |
- With two or more replicas alive, both policies decide the same. |
+
+
+ identical_while_tmr_can_run
+
+ |
+ With two or more replies present, both policies give the same outcome. |
+
+ Every set of three replies with two or more present. Outcome only, not mode or diagnose.
+ |
+
+
+ |
+ tmr_stops_below_two
+ |
+
+ With fewer than two replies present, fixed TMR's outcome is Halted.
+ |
+ Every set of three replies with fewer than two present. |
+
+
+ |
+
+ shrink_halts_only_with_nothing_left
+
+ |
+
+ The shrinking quorum's outcome is Halted if and only if no reply is present.
+ |
+ Every set of three replies. |
+
+
+ |
+
+ delivers_only_agreed_values
+
+ |
+
+ A delivered value has two agreeing replies, or exactly one replica alive that returned{' '}
+ Pair(v, v).
+ |
+ Every set of three replies, under both policies. |
+
+
+ |
+ decide_is_the_core
+ |
+
+ quorum_decide gives the core's verdict. An unknown reply kind counts as absent.
+ |
+ C interface: policy 0 or 1, any reply kind and values. |
- | tmr_stops_below_two |
- Fixed TMR halts below two replicas. |
+
+ bad_policy_halts
+ |
+
+ Any other policy code halts quorum_decide and quorum_mode.
+ |
+ C interface: any policy code above 1. |
- | shrink_halts_only_with_nothing_left |
- The shrinking quorum halts only at zero. |
+
+ mode_is_the_core
+ |
+
+ quorum_mode gives the core's mode.
+ |
+
+ C interface: policy 0 or 1, any u32 count.
+ |
- | delivers_only_agreed_values |
- A delivered value had two votes, or a clean self-check. |
+
+ strike_is_the_core
+ |
+
+ quorum_health_strike gives the core's answer and record. A replica above 2 changes
+ nothing.
+ |
+
+ C interface: any record with counts in the u32 range, any replica and cycle.
+ |
+
+
+ |
+ clear_is_the_core
+ |
+
+ quorum_health_clear gives the core's record. A replica above 2 changes nothing.
+ |
+
+ C interface: any record with counts in the u32 range, any replica.
+ |
+ Each proof name links to its source at v0.2.0.
+ Not covered
+
+ -
+
+
Health in the core.
+ {' '}
+ Unit tests only.
+
+ -
+ Diagnosis and the known-answer test. They run in the demo and in F´, not in the core.
+
+ -
+ Timing. The proofs say what
decide() returns, not how long it takes. The
+ bench measures that.
+
+ -
+ The system over a run. Never less than fixed TMR over a whole run is tested, not proved. See
+ Tested (per run).
+
+
Targets and builds
CI builds and tests on every change:
diff --git a/src/pages/index.astro b/src/pages/index.astro
index b8ca37b..c697730 100644
--- a/src/pages/index.astro
+++ b/src/pages/index.astro
@@ -7,16 +7,18 @@ import DocsLayout from '../layouts/DocsLayout.astro';
Overview
Mru documentation
- Reference for Mru's open core: the shrinking-quorum runtime, the Dusk simulator, and the tools around them.
+ Reference for Mru's open core, for unattended missions with no repair path: the shrinking-quorum runtime, the
+ Dusk simulator, and the tools around them.
Where to start
-
+
Concepts
Degradation-first design
- The Degradation-First Principle, the shrinking quorum, and how we score a system that is always losing parts.
+ The Degradation-First Principle and the shrinking quorum that applies it: what is proved, what is tested, and
+ what it costs.
@@ -39,8 +41,8 @@ import DocsLayout from '../layouts/DocsLayout.astro';
Integrations
F´ and OPS-SAT
- F´ components around the Rust core, a C interface for other frameworks, and the operations note for
- running on OPS-SAT.
+ F´ components around the Rust core, a C interface for other frameworks, and the operations note for a
+ proposed OPS-SAT experiment.
@@ -58,16 +60,19 @@ import DocsLayout from '../layouts/DocsLayout.astro';
git clone https://github.com/mruspace/flight
cd flight
cargo test --workspace
-cargo run --release -- --policy shrink --ticks 20000 --seed 1 \
+cargo run --release --bin quorum -- --policy shrink --ticks 20000 --seed 1 \
--upset-rate 0.001 --fault kill:0@5000 --fault kill:1@10000
- Run the same seed with --policy tmr to compare:
+ Run the same seed with --policy tmr to compare. The first two lines of each run:
+
+ policy=shrink ticks=20000 seed=1 upset_rate=0.001
+useful=14989 detected=11 wrong=0 halted_at=never alive_at_end=1 stopped=completed last_useful=20000
+
+policy=tmr ticks=20000 seed=1 upset_rate=0.001
+useful=9990 detected=9 wrong=0 halted_at=10000 alive_at_end=1 stopped=halted last_useful=9999
+
+ flight v0.2.0 on an Apple M4. The counts depend only on the seed.
- quorum --policy tmr ... useful=9990 detected=9 wrong=0 halted_at=10000
-quorum --policy shrink ... useful=14989 detected=11 wrong=0 halted_at=never
Fixed TMR halts at tick 10000, when the second replica dies. The shrinking quorum keeps running on the last
replica, which checks its own work.
@@ -75,8 +80,11 @@ quorum --policy shrink ... useful=14989 detected=11 wron
Then the simulator, which needs no dependencies:
git clone https://github.com/mruspace/dusk
cd dusk
-cargo run --release # 10,000 missions, about 2 s
-cargo run --release -- --sweep # sensitivity, about 30 s
+cargo run --release --bin dusk # 10,000 missions, about 2 s
+cargo run --release --bin dusk -- --sweep # sensitivity, about 1 minute
+
+ Times on an Apple M4 with 10 cores.
+
Where the code lives
diff --git a/src/pages/simulation/dusk.astro b/src/pages/simulation/dusk.astro
index 5c36e2f..dfecfa9 100644
--- a/src/pages/simulation/dusk.astro
+++ b/src/pages/simulation/dusk.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, ci } from '../../data/claims';
const crumbs = [{ label: 'Docs', href: '/' }, { label: 'Simulation', href: '/simulation/dusk/' }, { label: 'Dusk' }];
---
@@ -15,7 +16,10 @@ const crumbs = [{ label: 'Docs', href: '/' }, { label: 'Simulation', href: '/sim
{ href: '#options', label: 'Options' },
{ href: '#model', label: 'The fault model' },
{ href: '#results', label: 'Default results' },
- { href: '#sweep', label: 'Sweeps and ground' },
+ { href: '#definitions', label: 'What the columns mean' },
+ { href: '#baselines', label: 'Baselines' },
+ { href: '#sweep', label: 'Sweeps' },
+ { href: '#ground', label: 'Ground support' },
{ href: '#bench', label: 'Checked against the bench' },
{ href: '#claims', label: 'What this does not claim' },
]}
@@ -40,13 +44,14 @@ const crumbs = [{ label: 'Docs', href: '/' }, { label: 'Simulation', href: '/sim
cargo run --release # the default scenario, about 2 s
-cargo run --release -- --spares 2 # add salvaged processors
-cargo run --release -- --sweep # sensitivity, about 30 s
-cargo run --release -- --ground # against TMR with a ground team, about 10 s
-cargo run --release --bin charts # redraw the charts and data.json
+ >cargo run --release --bin dusk
# the default scenario, about 2 s
+cargo run --release --bin dusk -- --spares 2
# add salvaged processors
+cargo run --release --bin dusk -- --sweep
# sensitivity and cold standby, about 2 minutes
+cargo run --release --bin dusk -- --ground
# against TMR with a ground team, about 12 s
+cargo run --release --bin charts
# redraw the charts and data.json, about 2 minutes
- Times are for an 8-core laptop. Results depend only on the seed, never on the thread count.
+ The package has two programs. dusk is the default, and --bin charts redraws the charts.
+ Times are for an Apple M4 with 10 cores. Results depend only on the seed, never on the thread count.
Options
@@ -120,6 +125,14 @@ cargo run --release --bin charts
# redraw the charts and data
0.5 |
Lone output vs a vote |
+
+ | --cold-aging |
+ 0.1 and 1.0 |
+
+ How fast an unpowered spare ages, relative to a powered one. The report shows both ends; give a value to
+ show one.
+ |
+