---
title: "F´ components"
url: https://docs.mru.space/core/fprime/
description: "RedundancyManager, HealthRegistry, ReplicaHost and FaultInjector for F´ v4.4.1, the C interface to the core, and how they were verified."
---

[Docs](https://docs.mru.space/) / [Core runtime](https://docs.mru.space/core/quorum-crate/) / F´ components

# F´ components

Layer 1 as components for NASA JPL's F´ framework, version 4.4.1. Every decision comes from the [`quorum` crate](https://docs.mru.space/core/quorum-crate/), through a C interface that Kani proves equal to it.

F´ v4.4.1 C++14 37 unit tests v0.2.0

The source is in [fprime/](https://github.com/mruspace/flight/blob/v0.2.0/fprime) of mruspace/flight. The requirements and the design were written and approved in F´'s own order, requirements first, then the model, then the code: [requirements](https://github.com/mruspace/flight/blob/v0.2.0/docs/fprime-requirements.md), [design and results](https://github.com/mruspace/flight/blob/v0.2.0/docs/fprime-design-fpp.md).

## Components

| Component | Kind | What it does |
| --- | --- | --- |
| `RedundancyManager` | active | Asks the replicas for a result each cycle, decides with the core, delivers or rejects, steps the mode down as replicas are lost, and runs known-answer tests. |
| `HealthRegistry` | passive | Holds the strike record per replica: three outvotes within 200 cycles start a diagnosis. |
| `ReplicaHost` | active, one per replica | Runs the payload and answers requests and known-answer tests. A disabled host does not answer. |
| `FaultInjector` | passive, test builds only | Sits between the manager and the replicas in a test topology: silence (kill, hang), a stuck value, and bit flips in a replica's working memory, with the same random upsets as the demo for a seed. |

In a flight topology the manager connects to the replicas directly, so no test code is in the flight path.

The replicas run as three threads of one deployment. Three processes, and then separate processors, use the same components.

## RedundancyManager

| Element | Name |
| --- | --- |
| Input ports | `schedIn` (rate group, once per cycle), `replyIn[3]`, `pingIn` |
| Output ports | `requestOut[3]`, `enableOut[3]`, `resultOut`, `healthStrike`, `healthClear`, `pingOut` |
| Commands | `SET_POLICY`, `STANDBY_REPLICA`, `ADMIT_REPLICA` |
| Parameters | `KatPeriod` (64 cycles), `StateSavePeriod` (1,000 cycles; 0 saves on change only) |
| Telemetry | `CurrentPolicy`, `CurrentMode`, `LiveReplicas`, `Retired`, `Slots` on change; `Delivered`, `Caught` each cycle |
| Events | Mode changes, caught disagreements (throttled), diagnoses, retirements with their reason, standby and admission, the state file, and the halt |

The full model: RedundancyManager.fpp in fprime/Mru/Components/RedundancyManager.

A replica is retired when its known-answer result is wrong or missing, or after three missed cycles in a row. The event gives the reason: a diagnosis that failed or was not answered, a periodic test on the last replica that failed or was not answered, or lost.

F´ returns 0 for a parameter that was never loaded. The manager then uses the model's defaults, so a topology that skips `loadParameters()` does not run the known-answer test every cycle.

## Spares and standby

Each of the three slots is ACTIVE, STANDBY or RETIRED. Only ACTIVE slots get requests. These follow section 8 of the [whitepaper](https://mru.space/mru-whitepaper.pdf), where salvaged processors join as spares and declining nodes are set aside.

-   **STANDBY\_REPLICA** disables an ACTIVE slot to save power. It is refused if the policy could not run on the slots left. A power accountant will use it; that accountant is not built.
-   **ADMIT\_REPLICA** enables a STANDBY slot, or new hardware in a RETIRED slot, and asks for its known answer. The slot becomes ACTIVE only if the right answer arrives by the end of the next cycle.

## Resets

The manager saves the policy, the slot states and the cycle counter when one of them changes, and every `StateSavePeriod` cycles. The record is 21 bytes with a CRC-32. It writes a new file, flushes it and renames it over the old one, so a power cut leaves the old state or the new one. At start it restores a valid file and reports it, or starts with all slots ACTIVE and warns. Strikes are not saved: after a reset each replica starts a fresh window.

## One cycle

The order follows a tick of the demo, so the same seed gives the same counts:

-   **Close the last cycle.** Decide it if it is not yet decided, with a missing reply as absent. Count missed replies, and fail tests that had a full cycle to answer.
-   **Start the next.** Ask every ACTIVE slot. On the last replica, ask for two results on even cycles only, and add the known-answer test every `KatPeriod` cycles.
-   **Decide as soon as every answer is in.** Strikes, the test of two disagreeing replicas, and the periodic test follow at once.

A replica that dies stops answering, so the manager finds the death by silence. When a death leaves one replica, the cycles until it is marked lost end as caught disagreements. The demo kills its replicas itself and knows at once; this is the one place the counts differ.

## C interface

`quorum-ffi` builds the core as a `no_std` static library with a C header, [quorum.h](https://github.com/mruspace/flight/blob/v0.2.0/quorum-ffi/include/quorum.h). It is not tied to F´: any C or C++ framework can use it.

```
uint8_t quorum_mode(uint8_t policy, uint32_t alive);
quorum_verdict quorum_decide(uint8_t policy, const quorum_reply *replies);
void quorum_health_init(quorum_health *health);
bool quorum_health_strike(quorum_health *health, uint32_t replica, uint64_t cycle);
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.

## Verification

| Check | Result |
| --- | --- |
| Kani, core and C interface | 9 of 9 proofs |
| C test of quorum.h | Sizes, layout and known cases pass |
| F´ unit tests | 37, by requirement: HealthRegistry 5, ReplicaHost 5, FaultInjector 8, RedundancyManager 19. Built with address and undefined-behavior sanitizers. |
| System test against the demo | 60 cases: the five [bench](https://docs.mru.space/core/bench/) schedules, both policies, three upset rates, two seeds, 4,000 cycles. 36 identical to the demo. In the other 24, a kill that leaves one replica costs 2 correct results and adds 3 caught disagreements. Wrong results are identical in all 60. |

All of these run in CI on every change. The expected counts are written by the demo itself, and CI checks they are current.

## Build and test

```
# in a clone of mruspace/flight
git submodule update --init --recursive
cd fprime
python3 -m venv fprime-venv && . fprime-venv/bin/activate
pip install -r requirements.txt
fprime-util generate && fprime-util build
fprime-util generate --ut && fprime-util check --all
```

The build calls `cargo` to compile the core, so it needs a Rust toolchain. On macOS 27, the CMake that F´ v4.4.1 pins fails; CMake 4.4 works. Linux works with the pinned version.

## Limits

-   **Not on flight hardware.** The components run in tests on general-purpose processors. The [architecture status](https://docs.mru.space/concepts/architecture/) keeps Layer 1 at Prototype.
-   **No reference deployment yet.** The system test wires the four components itself; a full F´ deployment with ground data is planned.
-   **Not built:** the retry of a cycle after a disagreement on two replicas (the whitepaper's "dual with checkpointing"), the health score by error rate and response time, the power accountant, and memory scrubbing.

Updated 11 Oct 2026 · Source: fprime/Mru/Components · [Edit on GitHub](https://github.com/mruspace/docs/edit/main/src/pages/core/fprime.astro) · [Questions? Get in touch](https://mru.space/contact/)