Triple Modular Redundancy (TMR)

Triple Modular Redundancy (TMR) ist ein Hardware-Fehlertoleranzprinzip, das Lyx auf Software-Ebene implementiert: Kritische Werte werden dreifach im RAM gespeichert. Jeder Lesezugriff führt einen Mehrheitsentscheid durch — zwei von drei Kopien müssen übereinstimmen. Eine abweichende Kopie wird automatisch repariert (Self-Healing).

Zweck: Schutz gegen Single Event Upsets (SEU) — Bit-Flips in SRAM durch kosmische Strahlung. Im Erdorbit tritt ein SEU typischerweise alle 10–100 Stunden pro MBit Speicher auf. In erdnahen Orbits und auf Reiseflughöhen ist die Rate messbar erhöht.

→ Verwandt: Software Lockstep · Memory Scrubbing · DO-178C Hauptseite

Das Pragma @redundant auf einer globalen Variable veranlasst den Compiler, drei physisch getrennte Speicherbereiche anzulegen:

@redundant
var thrust_setpoint: int64 := 0;

@redundant
var autopilot_engaged: bool := false;

@redundant
var nav_heading: f64 := 0.0;

Intern legt der Compiler an:

// Konzeptuelle Darstellung — tatsächlich vom Compiler erzeugt, nicht manuell schreiben
var _thrust_setpoint_copy1: int64 @ section(".tmr_a");
var _thrust_setpoint_copy2: int64 @ section(".tmr_b");
var _thrust_setpoint_copy3: int64 @ section(".tmr_c");

Die drei Sektionen (.tmr_a, .tmr_b, .tmr_c) werden im Linker-Script auf physisch weit entfernte Speicheradressen gelegt — das verhindert, dass ein lokaler Speicherdefekt alle drei Kopien gleichzeitig trifft.

// Schreibzugriff im Quellcode:
thrust_setpoint := 850;

// Compiler-generierter Code (konzeptuell):
//   _thrust_setpoint_copy1 := 850;
//   _thrust_setpoint_copy2 := 850;
//   _thrust_setpoint_copy3 := 850;

// Lesezugriff im Quellcode:
var t: int64 := thrust_setpoint;

// Compiler-generierter Code (konzeptuell):
//   if copy1 = copy2 { t := copy1; copy3 := copy1; }
//   else if copy1 = copy3 { t := copy1; copy2 := copy1; }
//   else if copy2 = copy3 { t := copy2; copy1 := copy2; }
//   else { panic("TMR triple-fault — no majority"); }

Solange maximal eine der drei Kopien korrumpiert ist, gibt der Mehrheitsentscheid immer den korrekten Wert zurück und repariert die defekte Kopie. Erst wenn zwei Kopien gleichzeitig korrumpiert sind (sehr unwahrscheinlich), schlägt der Mehrheitsentscheid fehl.

unit flight_tmr;
import std.io;

type Altitude = int64 range -1000..60000;
type Speed    = int64 range 0..1000;

// Kritische Zustandsvariablen — alle dreifach
@redundant var current_altitude:  Altitude := 0;
@redundant var target_altitude:   Altitude := 0;
@redundant var airspeed:          Speed    := 0;
@redundant var autopilot_active:  bool     := false;
@redundant var flight_phase:      int64    := 0;   // 0=ground, 1=climb, 2=cruise, 3=descent

// Schreiben: sicher — alle drei Kopien aktualisiert
fn UpdateAltitude(measured_m: int64): void {
    current_altitude := measured_m as Altitude;
}

// Lesen: Majority Vote transparent
@dal(A)
@flight_crit
@wcet(50)
fn GetAltitudeError(): int64 {
    return target_altitude - current_altitude;   // Beide reads sind Majority-Votes
}

fn main(): int64 {
    autopilot_active := true;
    target_altitude  := 10000 as Altitude;

    UpdateAltitude(8500);

    var err: int64 := GetAltitudeError();
    PrintStr("Höhenfehler: "); PrintInt(err); PrintStr(" m\n");
    // Ausgabe: Höhenfehler: 1500 m

    return 0;
}

@redundant kann auch auf statische Arrays angewendet werden:

// Waypoint-Liste dreifach im RAM
@redundant
var waypoints: [16]Waypoint := [];

@redundant
var waypoint_count: int64 := 0;

fn AddWaypoint(wp: Waypoint): bool {
    if (waypoint_count >= 16) { return false; }
    waypoints[waypoint_count] := wp;   // Schreibt alle drei Kopien
    waypoint_count := waypoint_count + 1;
    return true;
}

Hinweis: Bei Array-Elementen wird der Majority-Vote pro Element durchgeführt, nicht über das gesamte Array. Das erhöht die Resilienz: Ein SEU in Kopie 2 bei Index 5 wird beim Lesezugriff auf Index 5 repariert, ohne andere Elemente zu beeinflussen.

Der Flag –verify-tmr lässt den Compiler prüfen, ob alle @redundant-Variablen korrekt auf drei physisch getrennte Speicherbereiche abgebildet wurden:

// lyxc --target=arm64 --verify-tmr src/flight_tmr.lyx
//
// Ausgabe bei Erfolg:
//   [TMR] thrust_setpoint: copy1@0x40010000, copy2@0x40015000, copy3@0x4001A000 ✓
//   [TMR] autopilot_active: copy1@0x40010008, copy2@0x40015008, copy3@0x4001A008 ✓
//   [TMR] All 8 @redundant variables verified.
//
// Ausgabe bei Fehler (Kopien zu nahe beieinander):
//   [TMR] WARNING: nav_heading copies within same 4KB page — SEU risk elevated
//   → Linker-Script anpassen: .tmr_b und .tmr_c auf andere Pages verteilen

Für maximale DAL-A-Absicherung kombiniert man TMR für Daten (@redundant) mit Software Lockstep für Berechnungen (@integrity):

@redundant
var flight_state_hash: int64 := 0;   // Geprüfte Zustandssignatur

@dal(A)
@flight_crit
@integrity(mode: software_lockstep, interval: 50)
@stack_limit(2048)
@wcet(200)
fn VerifyAndUpdateState(new_state: ^FlightState): bool {
    // software_lockstep: Berechnung wird dupliziert und verglichen
    var computed_hash: int64 := HashState(new_state);

    // @redundant: Lesezugriff ist Majority-Vote
    if (computed_hash = flight_state_hash) {
        return true;
    }

    // Zustandsabweichung — Recovery
    return false;
}

TMR schützt gegen zufällige Hardware-Fehler (SEUs), nicht gegen systematische Software-Fehler. Für systematische Fehler ist MC/DC-Coverage der richtige Ansatz.

Letzte Aktualisierung: 2026-05-22