Triple Modular Redundancy (TMR) & Integrity

Die Lyx-Sprachspezifikation (v0.9.0+) implementiert umfassende Mechanismen zur Triple Modular Redundancy (TMR), um die Anforderungen an die Fehlertoleranz in sicherheitskritischen Umgebungen (z. B. DO-178C DAL A) zu erfüllen. Ziel ist der Schutz gegen hardwarebedingte Bit-Flips (Single Event Upsets) durch Strahlung oder Speicherfehler.

1. Daten-Redundanz: @redundant

Globale Variablen können mit dem Attribut @redundant markiert werden. Dies veranlasst den Compiler, die Variable redundant im RAM zu verwalten.

Funktionsweise

Allokation: Es werden automatisch drei physisch getrennte Kopien der Variable im Arbeitsspeicher angelegt.
Schreibzugriff: Jede Zuweisung schreibt den Wert gleichzeitig in alle drei Speicherstellen.
Lesezugriff (Majority Vote): Beim Lesen wird ein Mehrheitsentscheid durchgeführt; der Wert gilt als korrekt, wenn mindestens 2 von 3 Kopien übereinstimmen.
Self-Healing: Erkennt das System eine abweichende Kopie, wird diese zur Laufzeit automatisch durch den Mehrheitswert repariert.

Beispiel

@redundant
var thrust_vector: int64;

2. Code-Integrität: .meta_safe

Für den Schutz des ausführbaren Codes generiert Lyx bei Verwendung des @integrity-Pragmas auf Unit-Ebene eine spezielle ELF-Sektion namens .meta_safe.

Spezifikation der .meta_safe Sektion

Die Sektion ist 8232 Bytes groß und enthält drei identische CRC32-Hashes des Code-Segments:

Offset	Feld	Typ	Beschreibung
0..15	code_va	uint64	Start- und End-Virtual Address des Codes
16..23	params	uint32	Modus (lockstep, scrubbed, ecc) und Intervall
32..35	hash_copy_1	uint32	CRC32 IEEE 802.3 des Codes
4128..4131	hash_copy_2	uint32	Identische Kopie 2 (nach 4096B Padding)
8224..8227	hash_copy_3	uint32	Identische Kopie 3 (nach weiteren 4096B Padding)

Das 4096-Byte-Padding stellt sicher, dass ein lokaler Hardwaredefekt (z.B. eine defekte Speicherzeile) nicht mehrere Hashes gleichzeitig korrumpieren kann.

3. Laufzeit-Prüfung: VerifyIntegrity()

Das Builtin VerifyIntegrity() dient der aktiven Überprüfung der Programm-Integrität zur Laufzeit.

Rückgabetyp: bool.
Logik: Die Funktion berechnet den aktuellen Hash des Codes und führt einen TMR-Mehrheitsvergleich gegen die drei in .meta_safe gespeicherten Referenz-Hashes durch.
Ergebnis: Liefert true, wenn die Integrität durch mindestens zwei übereinstimmende Hashes bestätigt wird, andernfalls false.

4. Zusammenfassung der Modi

Das Attribut @integrity unterstützt verschiedene Modi für das Integritäts-Management:

Modus	Beschreibung
—	—
`software_lockstep`	Redundante Ausführung mit Ergebnisvergleich.
`scrubbed`	Periodischer Hintergrund-CRC-Memory-Sweep (Intervall empfohlen).
`hardware_ecc`	Vertrauen auf Hardware-ECC-Speicherkorrektur.

Dokumentation basierend auf Lyx Sprachspezifikation v0.9.0 (Aerospace-Todo P0/P2)