💻 computer science

Building Extensible Program Logics through Effect Handlers

Dieses Paper schlägt einen Ansatz zum Aufbau erweiterbarer Programmlogiken vor, indem Effekt-Handler innerhalb einer Basislogik implementiert werden, um komplexe Verhaltensweisen wie Nebenläufigkeit und Absturzwiederherstellung zu modellieren, wodurch die Ableitung expressiver Schlussfolgerungsregeln und relationaler Verfeinerungen in einer modularen und wiederverwendbaren Weise ermöglicht wird.

Ursprüngliche Autoren: Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti

Veröffentlicht 2026-07-15

📖 6 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie versuchen, eine supersichere Festung zu bauen, um ein digitales Schloss zu schützen. In der Welt der Informatik werden diese Festungen als Programmlogiken bezeichnet. Es sind Sätze strenger Regeln, die Mathematiker und Programmierer verwenden, um zu beweisen, dass eine Software niemals abstürzt, Geheimnisse verrät oder etwas Seltsames tut.

Lange Zeit war der Bau dieser Festungen so, als würde man jeden einzelnen Ziegelstein von Hand schnitzen. Wenn man eine neue Funktion hinzufügen wollte – wie etwa eine Möglichkeit, wie die Software mit einem Stromausfall (Crash-Wiederherstellung) umgeht oder mit anderen Computern über den Ozean hinweg kommuniziert (verteilte Systeme) – musste man bei Null anfangen. Man benötigte eine spezielle Art von „Ziegelsetzer“-Fertigkeit, die sich völlig von der Fertigkeit unterschied, die man brauchte, um die Festung einfach nur zu nutzen. Es war schwer, langsam, und man konnte die Ziegel einer alten Festung nicht einfach wiederverwenden, um eine neue zu bauen.

Die große Idee: Das „Effect Handler“-Toolkit

Dieses Paper, geschrieben von Zichen Zhang, Simon Oddershede Gregersen und Joseph Tassarotti, schlägt einen neuen Weg vor, diese Festungen zu bauen. Anstatt Ziegel von Hand zu schnitzen, verwenden sie ein magisches Werkzeug namens Effect Handler (Effekt-Handler).

Stellen Sie sich einen Effekt-Handler wie ein anpassbares Regelbuch für ein Spiel vor. In einem Standard-Videospiel sind die Regeln für das Springen oder Schießen fest in die Engine programmiert. Aber mit Effekt-Handlern sagt die Game-Engine: „Ich weiß noch nicht, was ‚Springen‘ bedeutet; ich warte erst einmal darauf, dass mir jemand sagt, was zu tun ist.“ Dann kann ein Programmierer ein kleines Skript (einen Handler) schreiben, das sagt: „Okay, wenn der Spieler versucht zu springen, lasse ich ihn für eine Sekunde schweben.“

Die Autoren bauten eine winzige, leere Sprache namens FicusLang, die gar keine Regeln hat, außer dieser „Warten auf Anweisungen“-Funktion. Dann schrieben sie Handler, um die Regeln für Dinge wie Folgendes zu erschaffen:

Speicher (Memory): Wie das Programm Dinge behält (wie eine Haftnotiz).
Nebenläufige Threads (Concurrent Threads): Wie das Programm viele Dinge gleichzeitig erledigt (wie ein Koch, der mehrere Pfannen jongliert).
Abstürze (Crashes): Was passiert, wenn der Strom ausfällt und wiederkommt.
Verteilte Systeme (Distributed Systems): Wie Computer über ein wackeliges Netzwerk miteinander sprechen.

Der magische Trick: Das Aufbauen

Das Coolste daran ist, dass sie diese Regeln nicht nur erstellt, sondern auch bewiesen haben. Sie begannen mit der leeren Sprache, schrieben einen Handler für „Speicher“ und nutzten ein Logiksystem namens Ficus, um zu beweisen, dass ihr Speicher-Handler korrekt funktioniert. Soblich dieser bewiesen war, konnten sie diesen „Speicher“-Handler nutzen, um einen „Nebenläufigkeit“-Handler zu bauen.

Es ist wie beim Bau eines Hauses. Zuerst beweisen Sie, dass Ihr Fundament solide ist. Dann nutzen Sie dieses solide Fundament, um das erste Stockwerk zu bauen. Sobald das erste Stockwerk als sicher bewiesen wurde, nutzen Sie es, um das zweite Stockwerk zu bauen. Weil sie es auf diese Weise aufgebaut haben, konnten sie Funktionen einfach kombinieren und austauschen. Wenn Sie ein Haus mit sowohl einem Pool als auch einer Garage wollten, konnten Sie einfach den „Pool-Handler“ und den „Garagen-Handler“ kombinieren, ohne das gesamte Fundament neu bauen zu müssen.

Stärkere Regeln und neue Tricks

Da sie diese Regeln von Grund auf unter Verwendung von Handlern aufgebaut haben, konnten sie stärkere Regeln als bisherige Methoden erzielen.

Der „Pause“-Trick: In der Standard-Nebenläufigkeit kann der Computer eine Aufgabe in jedem winzigen Moment stoppen, um zu einer anderen Aufgabe zu wechseln. Dies erzeugt ein riesiges Chaos an Möglichkeiten, das schwer zu erfassen ist. Der Handler der Autoren wechselt die Aufgaben nur dann, wenn ein spezifischer „Effekt“ auftritt (wie eine Anfrage, eine Datei zu lesen). Dies reduziert das Chaos. Die Autoren bewiesen, dass diese „Pause nur auf Anfrage“-Methode genauso sicher ist wie die „Pause jederzeit“-Methode, aber viel einfacher zu begründen ist.
Die Kristallkugel (Prophecy Variables): Manchmal müssen Sie, um zu beweisen, dass ein Programm sicher ist, wissen, was ein zufälliges Ereignis tun wird, bevor es passiert. Die Autoren erschufen einen „Kristallkugel“-Effekt-Handler. Er erlaubt dem Beweis zu sagen: „Ich sage voraus, dass diese Zufallszahl 5 sein wird“, und prüft später, ob dies korrekt war. Sie zeigten, dass man lokale Kristallkellen (für eine spezifische Variable) aus einer riesigen globalen Kristallkugel bauen kann und sie sogar automatisch für Speicheroperationen erscheinen lassen kann, ohne dass der Programmierer zusätzlichen Code schreiben muss.

Die „relationale“ Logik: Der Zwillingstest

Das Paper führt auch ein neues Werkzeug namens RelFicus ein. Stellen Sie sich vor, Sie haben zwei identische Zwillinge, Programm A und Programm B. Sie wollen beweisen, dass sie sich immer gleich verhalten, wenn man ihnen dieselbe Eingabe gibt, selbst wenn das eine eine leicht andere Version des anderen ist.

RelFicus ist eine Logik, die es Ihnen ermöglicht, diese beiden Programme nebeneinander in Ihrem Kopf laufen zu lassen (unter Verwendung von „Ghost State“ oder imaginären Ressourcen), um zu beweisen, dass sie Zwillinge sind. Dies ist entscheidend, um zu beweisen, dass ihr neuer „Pause-nur-auf-Anfrage“-Nebenläufigkeits-Handler tatsächlich sicher ist. Sie nutzten diesen Zwillingstest, um zu beweisen, dass das Hinzufügen extra „Pause-Punkte“ (Präemption) das Ergebnis des Programms nicht verändert, was ihr einfacheres, leichter zu verwendendes Modell rechtfertigt.

Was sie nicht getan haben (und was sie abgelehnt haben)

Es ist wichtig zu wissen, was dieses Paper nicht ist.

Sie sagen nicht, dass die alte Art, Logiken zu bauen (die „Ziegel-von-Hand-schnitzen“-Methode), nutzlos ist. Sie sagen nur, dass sie schwer zu reuse (wiederzuverwenden) und schwer darauf aufzubauen ist.
Sie lehnen die Idee ab, dass man komplexe, abstrakte mathematische Strukturen verstehen muss (wie die in früheren Arbeiten erwähnten „ITrees“), um diese Logiken zu bauen. Sie argumentieren, dass ihr Ansatz zugänglicher ist, da er Standard-Programmierkonzepte (Handler) verwendet, die Entwicklern bereits vertraut sind.
Sie behaupten nicht, jedes Problem der Computersicherheit gelöst zu haben. Sie haben gezielt Handler für Speicher, Nebenläufigkeit, Abstürze und verteilte Systeme gebaut, räumen aber ein, dass andere Funktionen neue Handler benötigen könnten.

Wie sicher sind sie sich?

Die Autoren sind sehr zuversichtlich, aber präzise dabei. Sie haben nicht nur „vorgeschlagen“, dass dies funktionieren könnte; sie haben es bewiesen.

Sie haben das gesamte Logiksystem in einem Tool namens Rocq Prover geschrieben (einem Computerprogramm, das mathematische Beweise prüft).
Sie haben ein Theorem namens Adequacy bewiesen, das garantiert, dass wenn ihre Logik sagt, ein Programm sei sicher, das Programm tatsächlich ohne hängen zu bleiben läuft.
Sie haben bewiesen, dass ihr neues Nebenläufigkeitsmodell äquivalent zu den Standard-, komplexeren Modellen ist.
Sie haben gezeigt, dass ihre „Kristallkugel“-Funktionen (Prophecy) funktionieren, indem sie diese aus einer globalen Version herleiten und damit beweisen, dass die Mathematik Bestand hat.

Das Fazit

Dieses Paper ist so, als würde man den Informatikern einen Satz Lego-Steine statt eines Haufens nasser Ton geben. Früher mussten Sie, wenn Sie eine neue Art von Schloss bauen wollten, den Ton selbst mischen. Jetzt haben Sie vorgefertigte, vorgetestete Steine für „Speicher“, „Abstürze“ und „Netzwerke“. Sie können sie zusammenstecken, und die Mathematik garantiert, dass das Schloss nicht einstürzt. Es macht den Bau komplexer, sicherer Software weniger zu einem Solo-Kunstprojekt und mehr zu einem kollaborativen Baustellengeschehen, bei dem jeder die besten Teile wiederverwenden kann.

Technisches Resümee: Aufbau erweiterbarer Programmlogiken durch Effekt-Handler

Problemstellung

Programmlogiken sind leistungsstarke Werkzeuge zur Verifizierung komplexer Programmfunktionen wie Nebenläufigkeit, schwache Speichermodelle, verteilte Ausführung und Crash-Recovery. Der traditionelle Ansatz zur Entwicklung dieser Logiken steht jedoch vor erheblichen Barrieren:

Zugänglichkeit: Die Entwicklung einer neuen Programmlogik erfordert spezialisierte Fähigkeiten, die sich von denen unterscheiden, die für das Anwenden einer Logik benötigt werden, was die Erstellung neuer Logiken erschüssig macht.
Wiederverwendbarkeit und Komposition: Es ist schwierig, Komponenten aus bestehenden Logiken wiederzuverwenden oder die Unterstützung für verschiedene Effekte zu kombinieren (z. B. die Kombination von Nebenläufigkeit mit Crash-Recovery).
Operationale Semantik: Neuere alternative Ansätze (z. B. die Verwendung von ITrees) adressieren die Wiederverwendbarkeit, stützen sich jedoch auf denotative Semantiken, die nicht unmittelbar ein operationales Verständnis des Programmverhaltens liefern, was Fragen hinsichtlich der Ausführbarkeit auf realen Maschinen aufwirft.

Bestehende Logiken für Effekt-Handler setzen oft eine Basissprache voraus, in der primitive Effekte (wie veränderlicher Zustand oder Nebenläufigkeit) bereits eingebaut sind. Dies erschwert die Beweise der Korrektheit, da die Komplexität primitiver Effekte mit der Handler-Logik vermischt wird, anstatt Handler als den primären Mechanismus zum Bootstrapping von Effekten zu nutzen.

Methodik

Die Autoren schlagen einen Ansatz vor, um erweiterbare Programmlogiken operational aufzubauen, indem sie Effekt-Handler verwenden, um alle Programmeffekte zu modellieren, ausgehend von einer minimalen, zustandslosen Kernsprache namens FicusLang.

Kernkomponenten

FicusLang: Eine minimale, ML-ähnliche Lambda-Kalkül mit Effekt-Handlern. Sie enthält zwei primitive Effekte: pick (nicht-deterministisches Boolean) und observe (gelabelte Übergänge für Ghost-Code). Die Autoren merken an, dass selbst diese Primitiven schließlich mittels Handlern kodiert werden können.
Ficus (Unäre Logik): Eine erweiterbare Separation Logic, die auf dem Iris-Framework basiert und von der Hazel-Logik adaptiert wurde.
- Protokolle: Ficus verwendet Protokolle ( $\Psi$ ), um das Verhalten von Effekt-Handlern zu spezifizieren. Eine Weakest-Precondition-Assertion ewp e <Ψ> {Φ} besagt, dass, wenn e unter Handlern ausgeführt wird, die $\Psi$ erfüllen, das Programm nicht stecken bleibt und die Postbedingung $\Phi$ erfüllt.
- Erweiterbare Welten: Um Nebenläufigkeit und Koordination zu unterstützen, führt Ficus „erweiterbare Welten“ ein. Im Gegensatz zu Standard-Iris, wo Invarianten fixiert sind, parametrisiert Ficus die ewp und die speziellen Update-Modalitäten durch anpassbare Welten ( $W$ ). Dies ermöglicht es den Implementierern von Handlern, ihre eigenen Vorstellungen von Invarianten und Atomarität zu definieren, die für den spezifischen zu modellierenden Effekt geeignet sind.
- Handler-Implementierung: Die Autoren implementieren Handler für veränderlichen Zustand, Shared-Memory-Nebenläufigkeit, verteilte Ausführung und Crash-Recovery innerhalb von FicusLang. Durch die Verifizierung dieser Handler mittels Ficus leiten sie Beweisregeln ab, die analogen spezialisierten Logiken für diese Merkmale entsprechen.
RelFicus (Relationale Logik): Eine relationale Logik zum Beweisen kontextueller Verfeinerungen zwischen Programmen unter Verwendung von Effekten.
- Sie bettet relationales Schließen in die unäre Logik ein, indem sie ein zweites „Spezifikationsprogramm“ als Ghost-Zustand kodiert.
- Sie nutzt dieselben erweiterbaren Welten und Protokolle wie Ficus, was ein kompositionales Schließen über relationale Eigenschaften von effektiven Programmen ermöglicht.

Zentrale Beiträge

Das Paper leistet die folgenden spezifischen Beiträge:

Ficus: Die Entwicklung einer erweiterbaren unären Programmlogik basierend auf Effekt-Handlern. Es verwendet Protokolle, um das Schließen über Handler und Client-Code zu zerlegen, und führt erweiterbare Welten ein, um Ressourcen zwischen Client-Code zu teilen.
RelFicus: Eine relationale Logik zum Beweisen kontextueller Verfeinerungen in Gegenwart von Effekt-Handlern, die Ficus-Protokolle in den relationalen Kontext adaptiert, um Wiederverwendbarkeit und Erweiterbarkeit zu ermöglichen.
Fallstudien: Die Autoren demonstrieren den Ansatz durch die Rekonstruktion und Erweiterung von Merkmalen bestehender Logiken:
- Prophecy-Variablen: Ableitung lokaler Prophecy-Variablen aus globalen Prophecies und Implementierung eines „prophetic heap“, der Prophecy-Variablen implizit mit Heap-Lokationen assoziiert, wodurch eine explizite Instrumentierung des Client-Codes entfällt.
- Crash-Recovery: Eine Logik für Crash-Recovery mit asynchronem, dauerhaftem Speicher, die die Merkmale der Perennial-Logik rekonstruiert, aber mit einem einfacheren Modell und neuartiger Unterstützung für Crash-bewusste Prophecy-Variablen.
- Verteilte Systeme: Eine Logik für verteilte Systeme mit IronFleet-artigen atomaren Blöcken.
Stärkere Beweisregeln: Der Handler-basierte Ansatz liefert stärkere Schlussregeln als bisherige Arbeiten in zwei Punkten:
1. Hierarchische Effekte: Spätere Effekte können unter Verwendung früherer Effekte aufgebaut werden (z. B. die Ableitung lokaler Prophecies aus globalen), was die Wiederverwendung von Beweisregeln ermöglicht.
2. Nicht-standardisierte Semantik: Handler können nicht-standardisierte Versionen von Effekten implementieren, die leichter zu schließen sind (z. B. ein Nebenläufigkeits-Handler, der weniger Interleavings erzeugt als die Standard-Preemptive-Semantik). Die Autoren rechtfertigen dies über RelFicus, indem sie die kontextuelle Äquivalenz zu Standard-Semantiken beweisen.
Ergonomie: Ficus enthält ein flexibles Taktik-System, das es erlaubt, Spezifikationen auch bei unterschiedlichen Protokollen anzuwenden, was eine Beweiserfahrung bietet, die der von Standard-Iris-basierten Logiken ähnelt.

Ergebnisse und Validierung

Mechanisierung: Die gesamte Arbeit ist im Iris-Separation-Logic-Framework und im Rocq-Theorembeweiser mechanisiert.
Adäquanz-Theoreme: Die Autoren beweisen Adäquanz-Theoreme für sowohl Ficus als auch RelFicus, um sicherzustellen, dass die logischen Ableitungen den operationalen Semantiken der Sprache entsprechen.
Kontextuelle Äquivalenz: Unter Verwendung von RelFicus beweisen die Autoren, dass ihr Nebenläufigkeits-Handler, der Präemption nur dann auslöst, wenn ein Effekt ausgelöst wird, kontextuell äquivalent zu einer Standard-Preemptive-Semantik ist, bei der Präemption an jedem Schritt auftreten kann. Dies rechtfertigt die Verwendung ihres „schwächeren“ Interleaving-Modells für stärkere Invarianten-Öffnungsregeln.
Implizite Prophecies: Die Fallstudie des „prophetic heap“ zeigt, dass Heap-Operationen automatisch mit Prophecy-Fähigkeiten erweitert werden können, ohne dass das Client-Programm manuell mit Prophecy-Operationen annotiert werden muss.

Bedeutung

Das Paper behauptet, dass dieser Ansatz die Entwicklung von Programmlogiken zugänglicher und modularer macht. Indem Effekt-Handler als primärer Mechanismus zum Bootstrapping von Logiken genutzt werden, können Entwickler:

Logiken komponieren: Unterstützung für verschiedene Effekte (z. B. Nebenläufigkeit + Crash-Recovery) durch Verschachtelung von Handlern kombinieren, anstatt monolithische Logiken von Grund auf neu zu bauen.
Stärkere Regeln ableiten: Die Fähigkeit nutzen, nicht-standardisierte, handler-spezifische Semantiken zu definieren, die leichter zu schließen sind, sofern diese via relationaler Logik als äquivalent zu Standard-Semantiken bewiesen werden.
Operationale Klarheit: Ein operationales Verständnis des Programmverhaltens beibehalten, um sicherzustellen, dass die resultierenden Logiken in ausführbaren Semantiken verwurzelt sind.

Die Arbeit schließt die Lücke zwischen der Zugänglichkeit der Anwendung von Programmlogiken und der Komplexität ihrer Entwicklung, indem sie einen Rahmen bietet, in dem neue Logiken für komplexe Systeme inkrementell und kompositional aufgebaut werden können.