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: TMR · Memory Scrubbing · DO-178C Hauptseite · Attribute & Pragmas

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
}

Parse error: @integrity: `interval` gilt nur fuer `mode: scrubbed` — `software_lockstep` prueft vor jedem `return`

Parse error: @integrity(mode: software_lockstep) gilt nur an einer FUNKTION, nicht an der Unit

Für eine Funktion mit software_lockstep erzeugt der Compiler folgenden Ablauf. Verdoppelt wird der Rückgabeausdruck, nicht der gesamte Funktionsrumpf:

@integrity(mode: software_lockstep)
fn ComputeSpan(current: int64, target: int64): int64 {
    return target - current;
}

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.

Zwei Regeln setzt der Compiler selbst durch — er weist ab, statt stillschweigend nichts zu tun:

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:

// 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
}

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

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.

Das Programm bricht ab, Code 133. Es gibt keinen Handler und keine Rückkehr in den normalen Ablauf.

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.

Letzte Aktualisierung: 2026-09-05 — Seite auf den gemessenen Compilerstand gezogen (#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).