====== Software Lockstep ====== **Software Lockstep** ist ein Mechanismus zur Erkennung von Berechnungsfehlern — verursacht durch kurzzeitige Prozessorstörungen (SEUs in der CPU, Latch-Fehler, Timing-Anomalien). Der Compiler **dupliziert kritische Rechenoperationen** und vergleicht die Ergebnisse beider Berechnungen vor jedem dauerhaften Speicherzugriff oder ''return''. Stimmen sie nicht überein, greift ein kontrollierter Recovery-Pfad. Im Unterschied zu Hardware-Lockstep (zwei physische Kerne, synchron getaktet, Hardware vergleicht Ausgaben) läuft Software Lockstep auf einem einzelnen Kern — der Compiler fügt Instruktions-Redundanz in den Maschinencode ein. → Verwandt: [[lyx_-_programmiersprache:guides:do-178c:triple_modular_redundancy|TMR]] · [[lyx_-_programmiersprache:guides:do-178c:memory-scrubbing|Memory Scrubbing]] · [[lyx_-_programmiersprache:guides:do-178c|DO-178C Hauptseite]] · [[lyx_-_programmiersprache:sprache:attributes-pragmas|Attribute & Pragmas]] > **Was der Compiler wirklich tut** (gemessen mit lyxc 1.1.18A, 2026-09-05, [[https://github.com/SEOLizer/LyX-Compiler/issues/1908|#1908]]): > > * Seit 1.1.15A wird ''software_lockstep'' nachgewiesen — aber schmaler als diese Seite es früher beschrieb: **der Rückgabeausdruck wird zweimal gerechnet und vor dem ''ret'' verglichen.** Nicht jede ALU-Operation der Funktion. > * Bei Abweichung: **Abbruch mit Code 133.** Es gibt **keinen** Recovery-Handler — ''recovery_ptr'' steht im Dateiformat, wird aber nie angesprungen. Ein Wiederherstellungspfad bräuchte eine zweite Codekopie, die es nicht gibt. > * **Nur x86-64.** Die IR-Backends (lyxos, arm64, riscv, arm-cm4, xtensa) kennen weder Lockstep noch Sweep; dort ist ''@integrity'' wirkungslos. ---- ===== 1. Aktivierung ===== Software Lockstep wird per ''@integrity''-Pragma **an einer Funktion** aktiviert: @dal(A) @flight_crit @integrity(mode: software_lockstep) @stack_limit(2048) @wcet(200) fn ComputeAltitudeError(current: int64, target: int64): int64 { var delta: int64 := target - current; var clamped: int64 := delta; if (clamped > 5000) { clamped := 5000; } if (clamped < -5000) { clamped := -5000; } return clamped; // dieser Ausdruck wird zweimal gerechnet und verglichen } **''software_lockstep'' kennt kein ''interval''.** Der Vergleich sitzt vor jedem ''return'' und findet immer statt; eine Frist gibt es dort nicht. ''@integrity(mode: software_lockstep, interval: 50)'' wird **abgewiesen**: Parse error: @integrity: `interval` gilt nur fuer `mode: scrubbed` — `software_lockstep` prueft vor jedem `return` ''interval'' ist ausschließlich für ''mode: scrubbed'' zulässig. **An einer ''unit'' geht es ebenfalls nicht:** Parse error: @integrity(mode: software_lockstep) gilt nur an einer FUNKTION, nicht an der Unit ---- ===== 2. Was der Compiler generiert ===== Für eine Funktion mit ''software_lockstep'' erzeugt der Compiler folgenden Ablauf. Verdoppelt wird der **Rückgabeausdruck**, nicht der gesamte Funktionsrumpf: ==== Quellcode ==== @integrity(mode: software_lockstep) fn ComputeSpan(current: int64, target: int64): int64 { return target - current; } ==== Was daraus entsteht (konzeptuell) ==== var p: int64 := target - current; // primäre Rechnung var r: int64 := target - current; // redundante Rechnung, andere Register if (p != r) { // kein Handler, kein Rücksprung: Abbruch mit Code 133 } return p; Primäre und redundante Rechnung laufen in **unterschiedlichen physischen Registern**, damit ein einzelner Latch-Fehler in einer Registerbank nicht beide gleichzeitig trifft. Umgesetzt in ''src/codegen_x86.lyx'' (''cg_lockstepPruefe'', ''cg_lockstepEmitFail''); geprüft durch ''tests/integrity_test.sh''. ---- ===== 3. Einschränkungen und Regeln ===== Zwei Regeln setzt der Compiler selbst durch — er weist ab, statt stillschweigend nichts zu tun: ^ Abgewiesen ^ Meldung ^ Warum ^ | Rückgabeausdruck **mit Wirkung** (Aufruf, ''new'', Zuweisung) | ''der Rueckgabeausdruck hat eine Wirkung […] und laesst sich nicht zweimal rechnen'' | Zweimal rechnen hieße zweimal wirken | | **Struct- oder Tupel-Rückgabe** | ''Struct-Rueckgabe wird nicht abgedeckt'' | Es gibt kein einzelnes Register zu vergleichen | Praktische Folge: ''%%return Clamp(x, 0, 1000);%%'' übersetzt **nicht**. Das Ergebnis erst in eine Variable legen und diese zurückgeben. Die übrigen Punkte sind Entwurfsregeln, keine Compilerprüfungen: ^ Regel ^ Begründung ^ | Kein ''@extern fn'' in lockstep-geschützten Funktionen | Compiler hat keinen Zugriff auf externen Binärcode — kann ihn nicht duplizieren | | ''@wcet'' muss etwa **2× den normalen Wert** annehmen | Jede Operation wird zweimal ausgeführt | | Kein ''software_lockstep'' auf Funktionen mit Seiteneffekten (I/O, HW-Register) | I/O-Operationen dürfen nicht doppelt ausgeführt werden | | Empfohlen: Kombination mit ''@redundant'' für Variablen | Schutz der Berechnung (Lockstep) + Schutz des Speichers (TMR) | | Kein ''software_lockstep'' auf ISR-Funktionen ohne ''@no_opt'' | ISR-Code muss deterministisch bleiben | // FALSCH — Aufruf im Rückgabeausdruck: wird abgewiesen @integrity(mode: software_lockstep) fn BadFunction(sensor: int64): int64 { return Clamp(sensor * 3 / 2, 0, 1000); } // RICHTIG — Ergebnis in eine Variable, dann zurückgeben @integrity(mode: software_lockstep) fn ComputeOutput(sensor: int64): int64 { var v: int64 := Clamp(sensor * 3 / 2, 0, 1000); return v; } fn SendOutput(val: int64): void { WriteHardwareRegister(UART_TX, val); // I/O außerhalb des Lockstep-Schutzes } ---- ===== 4. WCET-Interaktion ===== Der verdoppelte Rückgabeausdruck kostet Laufzeit. Wie viel, hängt davon ab, wie viel Rechnung im ''return'' steht — die pauschale Verdopplung der Funktionslaufzeit gilt **nicht**, weil nur der Rückgabeausdruck doppelt läuft. ''@wcet'' entsprechend anpassen: // Ohne Lockstep: geschätzte WCET 80 µs @wcet(80) fn NormalFunction(x: int64): int64 { return x * x + x / 2; } // Mit Lockstep: WCET erhöhen @integrity(mode: software_lockstep) @wcet(180) // 2× + Overhead für Vergleich und Recovery-Pfad fn ProtectedFunction(x: int64): int64 { return x * x + x / 2; } Der Compiler zeigt bei fehlerhaft gesetztem ''@wcet'' auf lockstep-Funktionen eine Warnung: warning[W0244]: @wcet(80) on software_lockstep function ComputeControlOutput Estimated protected WCET: 167 µs exceeds declared budget: 80 µs Consider: @wcet(180) or higher ---- ===== 5. Vergleich der Integritätsmodi ===== Es gibt **zwei** Modi. ''mode: hardware_ecc'' wird abgewiesen (''nicht umgesetzt — es gibt keinen Traeger dafuer''); die Grammatik nennt den Namen, der Compiler kennt ihn nicht. ^ Merkmal ^ software_lockstep ^ scrubbed ^ | Schützt | den Rückgabeausdruck einer Funktion | die geladenen Codeseiten | | Erkennt | Rechenfehler vor dem ''ret'' | Bit-Flips im Code zur Laufzeit | | ''interval'' | **unzulässig** | 1…3600000 ms, Vorgabe 1000 | | Abbruchcode | 133 | 135 (Codeseite), 136 (keine Mehrheit der drei Hashkopien) | | Anbringung | nur an einer Funktion | Funktion; an der ''unit'' derzeit ebenfalls angenommen | | Laufzeit | doppelter Rückgabeausdruck | Sweep im Hintergrund (SIGALRM) | | Komb. mit @redundant | Empfohlen | Nicht nötig | ---- ===== 6. Was bei einer Abweichung passiert ===== **Das Programm bricht ab, Code 133.** Es gibt keinen Handler und keine Rückkehr in den normalen Ablauf. ''SetLockstepRecoveryHandler'' und ''LockstepFault'' **existieren nicht** — beide melden ''undefined function''. Frühere Fassungen dieser Seite zeigten sie als Beispiel. Was es gibt, ist ''VerifyIntegrity()'' aus [[lyx_-_programmiersprache:units:meta_safe|std.meta_safe]]: eine Prüfung **auf Zuruf** über die eigene Datei, kein Lockstep-Handler. Im Dateiformat steht ein Feld ''recovery_ptr'' (Offset 48). Es ist belegt, wird aber **nicht angesprungen**: ein Wiederherstellungspfad bräuchte eine zweite Codekopie, die es nicht gibt. Der Mechanismus **erkennt**, er korrigiert nicht. Wer einen kontrollierten Notfallpfad braucht, baut ihn außerhalb: Watchdog auf Systemebene, Umschalten auf einen Backup-Rechner, Auswertung des Abbruchcodes durch den Aufrufer. Innerhalb des Prozesses gibt es dafür heute keinen Ansatzpunkt. ---- ===== 7. DAL-Empfehlung ===== ^ DAL ^ software_lockstep ^ Begründung ^ | A | **Zwingend** für Kernberechnungen | Katastrophaler Ausfall — maximaler Schutz | | B | Empfohlen | Gefährlicher Ausfall — Investition gerechtfertigt | | C | Optional | WCET-Impact meist nicht vertretbar | | D/E | Nicht sinnvoll | Overhead ohne Sicherheitsgewinn | ---- Letzte Aktualisierung: 2026-09-05 — Seite auf den gemessenen Compilerstand gezogen ([[https://github.com/SEOLizer/LyX-Compiler/issues/1908|#1908]], gemessen mit lyxc 1.1.18A, 2026-09-05): ''interval'' aus allen sechs Aufrufen entfernt (an ''software_lockstep'' abgewiesen), der erklärende Absatz zum ''interval''-Polling gestrichen (beschriebenes Verhalten gibt es nicht), das Unit-Ebene-Beispiel entfernt (wird abgewiesen), Spalte ''hardware_ecc'' aus der Modus-Tabelle genommen (Modus wird abgewiesen), Abschnitt 6 ersetzt: ''SetLockstepRecoveryHandler'' und ''LockstepFault'' existieren nicht, bei Abweichung bricht das Programm mit 133 ab. Zwei Compilerprüfungen ergänzt (Rückgabeausdruck mit Wirkung, Struct-Rückgabe) und die Beispiele danach berichtigt. Vorherige Aktualisierung: 2026-05-22 Codebeispiele geprüft: gegen **lyxc 1.2.5C** übersetzt (Prüflauf 2026-09-08 über die gesamte Doku: 574 Vollprogramme, 0 echte Fehler; zusätzlich 5159 Aufrufe gegen die ''pub fn''-Signaturen in ''aurum/std'' gehalten, 0 Abweichungen).