Skip to content
mruspacePublic

About

Onboard software that keeps a spacecraft working as its computers fail: a Kani-verified no_std Rust core, a fault-injection demo, and static ARM builds. F´ components next.

Topics

Resources

Stars

1 star

Watchers

0 watching

Forks

Repository files navigation

Mru

Mru Flight

ci

Onboard software that keeps a spacecraft doing useful work as its computers fail. Part of Mru.

Classic triple modular redundancy votes on three computers and stops when it can no longer form a majority. Mru's shrinking quorum keeps going: vote on three, compare on two, self-check on one. In 10,000 simulated missions it delivered 1.34× the useful work of fixed triple redundancy on the same hardware, and never less on any single mission (dusk).

This repository is where that policy becomes flight software: a small, verified Rust core, to be wrapped as components for NASA JPL's open-source F´ framework.

Status (October 2026): early prototype. The decision core and a demo on real processes, with faults injected, work today. The F´ components come next (design).

Correct results over 20,000 ticks with the same upsets and faults. Both lines are the same until tick 9,000. Then fixed TMR, left comparing a good replica with a stuck one, stops at 8,993 correct results. The shrinking quorum, which retired the stuck replica at tick 4,002, self-checks on the last replica and reaches 14,490.

What is here

Crate What it is
quorum The decision core: vote, compare, self-check, and the health record that decides when a replica must be diagnosed. no_std, no allocation, no dependencies. Unit-tested, checked with Kani, and built in CI for a bare-metal ARM Cortex-M target.
demo The quorum program: three replica processes, a voter built on the core, fault injection, enforced resource limits, and a report of what was delivered and what it cost. Runs on Linux and macOS; release builds are fully static binaries for 64-bit and 32-bit ARM Linux. Its only dependency is libc, for the system calls behind the limits.

What the core guarantees

Checked by unit tests over every combination of a small value domain, and by Kani over every possible input (4 proofs, verified in CI on every change):

  • Never less than fixed TMR. While fixed TMR can still run (two or more replicas), both policies make exactly the same decision. The shrinking quorum only differs after fixed TMR has stopped.
  • Fixed TMR stops below two replicas. The shrinking quorum halts only when no replica is left.
  • Only agreed results are delivered. A delivered value was produced by at least two replicas, or by both runs of the last replica's self-check.

How the demo works

  • Three replica processes run the same deterministic task (a hash over a 4 KiB block derived from the tick).
  • The voter asks the core for a verdict each tick and steps down as replicas fail. Self-check on one replica runs at half rate, because that replica computes everything twice.
  • Health scoring: a replica outvoted three times within 200 ticks is diagnosed with a known-answer test (a fixed input whose result is known). Passing means the upsets were transient, so its strikes are cleared. Failing retires it.
  • Known-answer tests also tell which side is wrong when two replicas disagree, and run periodically on the last replica to catch a stuck fault.
  • Fault injection by schedule or at random: kill a replica, make it hang, make it stuck, or flip a bit in its working memory during a computation, as radiation would, so the fault travels through the real calculation. On one replica, a share of upsets (--common-mode) hits both self-check runs at the same place, which is how a wrong result can slip through.
  • Safe on shared hardware: each process enforces a memory limit (128 MB by default) and an optional CPU-time limit on itself; the voter can cap its CPU share (--cpu-percent), stops cleanly on SIGTERM or after a maximum run time, and drops a replica that stops answering. See the operations note for OPS-SAT.
  • Radiation sensor (--sensor-mb): a block of memory with a known pattern, checked at a fixed interval; every flipped bit is logged with its location and repaired, to measure the real upset rate on flight hardware.
  • Ready to run: a fault schedule can come from a file (--faults-file), the summary can be written to a file for downlink (--summary), and opssat/run.sh starts, checks and stops a run with all the limits set.
  • Every run is reproducible from its seed.

Run it

cargo test --workspace         # unit tests
./scripts/scenarios.sh         # scenario tests against the real program
cargo run --release -- --policy shrink --ticks 20000 --seed 1 --upset-rate 0.001 \
  --fault stuck:1@4000 --fault kill:0@9000

--log file.csv writes every event (stuck, hang, lost, retired, cleared, killed, detected, wrong, stopped, sensor bit flips), and --progress-every N adds the running totals every N ticks. quorum with an unknown option prints all options. python3 scripts/chart.py --png redraws the chart above from two such runs. To run the proofs, install Kani and run cargo kani -p quorum.

Results

The same seed and faults for both policies: random upsets throughout, replica 1 stuck from tick 4,000, replica 0 dead at tick 9,000.

quorum --policy tmr    ...  useful=8993  detected=11007 wrong=0 halted_at=never
quorum --policy shrink ...  useful=14490 detected=10    wrong=0 halted_at=never

Fixed TMR masks the stuck replica while it has three, but once another replica dies it is left comparing a good replica with a stuck one, and every result is rejected. The shrinking quorum retired the stuck replica two ticks after it failed, then carried on with self-check on the last good one.

20,000 ticks, upset rate 0.001, seed 1:

Scenario Fixed TMR Shrinking quorum
Random upsets only 20,000 correct 20,000 correct
Replicas die at 5,000 and 10,000 9,990 correct, halts at 10,000 14,989 correct, still running
One dies at 5,000, one stuck at 10,000 9,990 correct, then stuck in disagreement 14,988 correct; the known-answer test finds the stuck replica

These are illustrative scenarios, not a reliability estimate. For statistics over thousands of simulated missions, see dusk.

The honest cost

On one replica, a stuck fault is only caught by the periodic known-answer test (every 64 ticks, --kat-period). With replicas lost at 5,000 and 8,000 and the last one stuck at 10,000, the demo delivered 24 wrong results before the test caught it and the system stopped. Fixed TMR would have stopped long before, at the second loss, and delivered none. A shorter test period trades throughput for a smaller window. This is the trade the whitepaper and dusk quantify: more useful work, at the cost of a small number of unchecked results late in life.

The scenario tests also caught a real flaw during development: health scoring first retired a replica as soon as it was outvoted three times, so random upsets could retire a healthy one, leaving the shrinking quorum with less hardware than fixed TMR. Diagnosing with a known-answer test before retiring fixed it, and scripts/scenarios.sh now checks over ten seeds that the shrinking quorum never delivers fewer correct results than fixed TMR.

Footprint and limits

Measured in CI on every change, 20,000 results (the shrinking-quorum demo run):

Platform Voter memory Each replica Binary
Linux ARM64 (aarch64) about 1.5 MB about 1.5 MB about 0.5 MB
Linux x86_64 about 2.0 MB about 2.0 MB about 0.5 MB
macOS (Apple silicon) about 1.5 MB about 1.4 MB about 0.5 MB

The scenario tests also check the safety limits: a hung replica is dropped after the reply timeout, SIGTERM ends the run cleanly with no replica left, the maximum run time is enforced, --cpu-percent 5 keeps CPU time near 5% of wall time, and on Linux the 128 MB memory limit is read back from the kernel for the voter and every replica. They also check the radiation sensor, the fault schedule file and the launcher script. In CI the whole suite also runs on the static 64-bit and 32-bit (hard and soft float) ARM binaries under emulation. Tagged releases package each binary with the launcher, a sample fault schedule and the operations note.

Roadmap

  1. F´ components: RedundancyManager, HealthRegistry, ReplicaHost and a test-only FaultInjector, as thin C++ shells around the Rust core (design). PowerAccountant and ScrubScheduler follow.
  2. Measurements on representative processors: static ARM Linux binaries are built and tested today; next, real boards.
  3. Hardware-in-the-loop bench: real boards with injected faults (bit flips, resets, power cuts).
  4. In orbit: an experiment proposed for ESA's OPS-SAT Space Lab (OPS-SAT PRETTY), logging real radiation upsets next to the satellite's own dosimetry.
  5. On Earth: the same software on an unattended ocean node, proposed for an EMSO ERIC observatory test.

Related

To cite this work, see CITATION.cff.

Questions or contributions

Email contact@mru.space.

Licence

Code under Apache License 2.0. The Mru name and mark are trademarks; see TRADEMARK.md.

About

Onboard software that keeps a spacecraft working as its computers fail: a Kani-verified no_std Rust core, a fault-injection demo, and static ARM builds. F´ components next.

Topics

Resources

Stars

1 star

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages