Towards Proving Liveness on Weak Memory (Extended Version)

1. Problemstellung

Die Verifikation von nebenläufigen Programmen ist aufgrund der feinkörnigen Verschachtelung von Programmschritten bereits unter der Annahme der sequentiellen Konsistenz (SC) komplex. Diese Komplexität steigt drastisch, wenn schwache Speichermodelle (Weak Memory Models) moderner Hardware-Architekturen oder Programmiersprachen berücksichtigt werden müssen.

• Aktueller Stand: Bisherige Beweiskalküle für schwache Speichermodelle konzentrieren sich fast ausschließlich auf Sicherheits Eigenschaften (Safety Properties), wie z. B. das Fehlen von Race Conditions oder Deadlocks.
• Die Lücke: Lebendigkeitseigenschaften (Liveness Properties), wie Terminierung oder Starvation Freedom (Freiheit von Verhungern), wurden in diesem Kontext kaum behandelt. Bestehende Ansätze für Fairness unter schwachen Speichermodellen (z. B. von Lahav et al. oder Abdulla et al.) bieten zwar semantische Konzepte, aber es fehlte ein deduktives Beweiskalkül, das direkt auf der Ebene von Programmen und Speichermodellen anwendbar ist.
• Herausforderung: In schwachen Speichermodellen sehen Threads nicht notwendigerweise dieselben Werte für geteilte Speicherstellen zur gleichen Zeit. Dies macht traditionelle Invarianten und Ranking-Funktionen (die oft auf dem aktuellen Zustand basieren) ungültig oder undefiniert.

2. Methodik

Die Autoren entwickeln einen Beweiskalkül für Lebendigkeitseigenschaften, der auf den Regeln von Manna und Pnueli für Antwortrelationen (Response Properties) unter schwacher Fairness basiert, jedoch um spezifische Erweiterungen für schwache Speichermodelle ergänzt wird.

Kernkomponenten der Methode:

1. Erweiterung von Manna-Pnueli (WELL-J):

   • Das Paper nutzt die Regel WELL-J (Well-founded Response under Justice), die auf wohlgeordneten Mengen (Well-Founded Domains) und Ranking-Funktionen basiert.
   • Erweiterung 1: Speicher-Fairness (Memory Fairness): Die Regel wird so erweitert, dass interne Speicher-Transitionsen (Memory Internal Steps, z. B. Propagation von Werten) als „hilfreiche Übergänge" (Helpful Transitions) in die Fairness-Menge $J$ aufgenommen werden können. Dies ist entscheidend, da in schwachen Modellen oft nur interne Speicher-Schritte (wie Flushes oder Propagation) einen Thread dazu bringen, neue Werte zu sehen.
   • Erweiterung 2: Ranking-Funktionen über schwachen Zustand: Die Ranking-Funktionen messen nicht nur den Fortschritt im Programmzähler, sondern auch den „Abstand" eines Threads zum Sehen des neuesten Werts einer Speicherstelle.

2. Logik Piccolo und Potentials:

   • Um Beweise zu führen, die für mehrere Speichermodelle gültig sind, verwenden die Autoren die Logik Piccolo (basierend auf dem Konzept der Potentials).
   • Potentials: Ein Potential ist eine Liste von Speicherzuständen (Stores), die die Sicht eines Threads auf die Vergangenheit und Zukunft repräsentiert. Ein Thread kann „veraltete" (stale) Werte sehen, aber das Potential enthält auch die zukünftigen, aktuellsten Werte.
   • Erweiterung von Piccolo: Die Autoren erweitern Piccolo um neue Konstrukte:
     • $\vec{x}$: Der aktuellste (letzte) Wert einer Speicherstelle.
     • dist(τ, x): Eine Funktion, die den Abstand (Anzahl der veralteten Werte) zwischen dem aktuellen Blick des Threads $\tau$ und dem neuesten Wert von $x$ misst.
     • C(x): Ein Prädikat für „Covered", wichtig für Read-Modify-Write-Operationen (RMW).
   • Diese Erweiterungen erlauben es, Aussagen über die Sichtbarkeit von Werten zu treffen und zu beweisen, dass interne Speicher-Schritte diesen Abstand verringern.

3. Generischer Ansatz:

   • Statt Regeln für ein spezifisches Modell zu definieren, werden die Regeln auf dem abstrakten Potential-Domain definiert.
   • Die Korrektheit (Soundness) wird durch eine Lifting-Funktion (mapM) sichergestellt, die konkrete Speicherzustände eines Modells $M$ (z. B. Release-Acquire) auf Potentials abbildet.
   • Ein Beweis ist gültig für alle Modelle, in denen die verwendeten Regeln sound sind.

3. Wichtige Beiträge

1. Erster Beweis-Kalkül für Liveness unter Weak Memory: Das Paper stellt den ersten deduktiven Kalkül vor, der speziell für Lebendigkeitseigenschaften (wie Terminierung und Starvation Freedom) in schwachen Speichermodellen entwickelt wurde.
2. Integration von Memory Fairness: Die Autoren formalisieren, wie interne Speicher-Transitionsen (die für das Fortschreiten in schwachen Modellen notwendig sind) als faire, hilfreiche Übergänge in Liveness-Beweise integriert werden können.
3. Erweiterung der Piccolo-Logik: Einführung von dist und view maximality ($\tau \uparrow x$), um den Fortschritt beim „Sehen" neuer Werte quantitativ zu erfassen und in Ranking-Funktionen zu nutzen.
4. Soundness für spezifische Modelle: Die Autoren definieren Lifting-Funktionen und beweisen die Soundness der Regeln für die Speichermodelle Release-Acquire (RA) und Strong Coherence (StrCOH).

4. Ergebnisse

Die Methode wurde auf zwei Algorithmen angewendet, um deren Starvation Freedom zu beweisen:

1. Das „Waiting"-Programm (Beispiel):

   • Ein einfaches Synchronisationsbeispiel, bei dem ein Thread auf ein Signal wartet.
   • Der Beweis zeigt, dass Thread T2 terminiert, sobald es das Signal sieht.
   • Erkenntnis: Unter schwachen Modellen ist es notwendig, einen zusätzlichen Zustand ($\phi_3$) einzuführen, der den Fall abdeckt, dass T2 das Signal noch nicht gesehen hat, aber T1 bereits geschrieben hat. Hier ist der hilfreiche Übergang ein interner Speicher-Schritt ($\iota$), der die Sicht von T2 aktualisiert. Das Ranking muss den dist-Wert enthalten.

2. Ticket Lock Algorithmus:

   • Ein klassischer Mutual-Exclusion-Algorithmus für $n$ Threads.
   • Die Autoren verwenden eine parametrisierte Version der Regel (WELL-JP), um die Starvation Freedom für eine beliebige Anzahl von Threads zu beweisen.
   • Ergebnis: Der Algorithmus garantiert Starvation Freedom unter den Modellen Release-Acquire (RA) und Strong Coherence (StrCOH).
   • Nuance: Der Beweis für StrCOH erfordert keine Regel St-Other (die besagt, dass das Sehen eines Schreibens auch das Sehen früherer Schreibungen impliziert). Da Ticket Lock ohne diese Regel bewiesen werden kann, ist er auch für StrCOH gültig. Das „Waiting"-Programm hingegen wäre unter StrCOH ohne zusätzliche Annahmen nicht liveness-garantiert, da dort die Reihenfolge der Sichtbarkeit kritisch ist.

5. Bedeutung und Ausblick

• Theoretischer Fortschritt: Das Paper schließt eine signifikante Lücke in der formalen Verifikation von Nebenläufigkeit. Es zeigt, dass Lebendigkeitseigenschaften auch unter komplexen, schwachen Speichermodellen mechanisierbar und deduktiv beweisbar sind.
• Praktische Relevanz: Die Fähigkeit, Starvation Freedom für Algorithmen wie Ticket Lock unter realistischen Hardware-Modellen (RA) zu beweisen, ist für die Zuverlässigkeit von Betriebssystemen und verteilten Systemen essenziell.
• Generizität: Der Ansatz ist nicht auf ein einzelnes Modell beschränkt. Durch die Trennung von abstrakten Regeln und konkreten Lifting-Funktionen können neue Speichermodelle leicht integriert werden, sofern die Soundness der Regeln nachgewiesen wird.
• Zukünftige Arbeit: Die Autoren planen, weitere Modelle (z. B. Partial Store Ordering) zu untersuchen und stärkere Fairness-Konzepte (Compassion) sowie automatische Werkzeuge zu integrieren.

Zusammenfassend bietet das Paper einen robusten Rahmen, um zu beweisen, dass nebenläufige Programme unter schwachen Speicherbedingungen nicht nur sicher, sondern auch fair und terminierend sind, indem es die Lücke zwischen semantischen Fairness-Konzepten und syntaktischen Beweiskalkülen schließt.