Typbasierte Speichersicherheit ohne manuelle Speicherverwaltung oder Garbage Collection zur Laufzeit?

Nehmen wir an, wir wollten eine typvolle, rein funktionale Programmiersprache wie Haskell oder Idris, die auf die Systemprogrammierung ohne Garbage Collection abzielt und keine Laufzeit hat (oder zumindest nicht mehr als die C- und Rust-Laufzeit). Etwas, das mehr oder weniger auf blankem Metall laufen kann.

Welche Optionen für die statische Speichersicherheit erfordern keine manuelle Speicherverwaltung oder Speicherbereinigung zur Laufzeit, und wie könnte das Problem mithilfe des Typsystems einer reinen Funktion gelöst werden, die Haskell oder Idris ähnelt?

Grob gesagt gibt es zwei Hauptstrategien für die sichere manuelle Speicherverwaltung.

1. Der erste Ansatz besteht in der Verwendung einer Substrukturlogik wie der linearen Logik zur Steuerung der Ressourcennutzung. Diese Idee hat sich seit Beginn der linearen Logik herumgesprochen und basiert im Wesentlichen auf der Beobachtung, dass durch das Verbieten der strukturellen Kontraktionsregel jede Variable höchstens einmal verwendet wird und es daher kein Aliasing gibt. Infolgedessen ist der Unterschied zwischen der direkten Aktualisierung und der Neuzuweisung für das Programm nicht sichtbar, sodass Sie Ihre Sprache mit der manuellen Speicherverwaltung implementieren können.

   Dies ist, was Rust macht (es benutzt ein affines Typensystem). Wenn Sie sich für die Theorie der Sprachen im Rust-Stil interessieren, ist Ahmed et al .s L3: A Linear Language with Locations eine der besten Veröffentlichungen . Im Übrigen ist auch der erwähnte LFPL-Kalkül Damiano Mazza linear, von dem eine vollständige Sprache in der RAML-Sprache abgeleitet ist .

   Wenn Sie sich für die Verifizierung im Idris-Stil interessieren, sollten Sie sich die ATS-Sprache von Xi et al ansehen , eine Sprache im Rust / L3-Stil mit Unterstützung für die Verifizierung basierend auf indizierten Typen im Haskell-Stil Kontrolle über die Leistung.

   Ein noch aggressiverer Ansatz ist die von Microsoft Research entwickelte F-Star-Sprache , bei der es sich um eine vollständige Theorie des abhängigen Typs handelt. Diese Sprache hat eine monadische Schnittstelle mit Vor- und Nachbedingungen im Sinne der Hoare-Typentheorie von Nanevski et al. (Oder sogar meiner eigenen integrierenden linearen und abhängigen Typen ) und verfügt über eine definierte Teilmenge, die zu C-Code auf niedriger Ebene kompiliert werden kann - Tatsächlich werden sie bereits als Teil von Firefox mit verifiziertem Krypto-Code ausgeliefert!

   Es ist klar, dass weder F-Stern noch HTT linear typisierte Sprachen sind, aber die Indexsprache für ihre Monaden basiert normalerweise auf der Trennungslogik von Reynold und O'Hearn , einer mit der linearen Logik verwandten Substrukturlogik, die sich als äußerst erfolgreich erwiesen hat die Assertionssprache für Hoare-Logik für Zeigerprogramme.

2. Der zweite Ansatz besteht darin, einfach anzugeben, welche Assemblierung (oder welche niedrige IR-Ebene Sie möchten) ausgeführt wird, und dann eine Art lineare Logik oder Trennungslogik zu verwenden, um direkt über das Verhalten in einem Proof-Assistenten zu urteilen. Grundsätzlich können Sie den Proof-Assistenten oder eine abhängig eingegebene Sprache als ausgefallenen Makro-Assembler verwenden, der nur korrekte Programme generiert.

   Die High-Level-Trennungslogik von Jensen et al. Für Low-Level-Code ist ein besonders reines Beispiel dafür - sie erstellt eine Trennungslogik für die x86-Assembly! Es gibt jedoch viele Projekte in diesem Bereich, wie die Verified Software Toolchain bei Princeton und das CertiKOS- Projekt bei Yale.

Alle diese Ansätze werden sich wie Rust "anfühlen", da die Verfolgung des Eigentums durch Einschränkung der Verwendung von Variablen der Schlüssel zu allen ist.

Lineare Typen und Trennungslogik sind beide großartig, können jedoch einen erheblichen Programmieraufwand erfordern. Das Schreiben einer sicheren verknüpften Liste in Rust könnte zum Beispiel ziemlich schwierig sein.

Es gibt jedoch eine Alternative, die viel weniger Programmieraufwand erfordert, wenn auch mit weniger strengen Garantien. Ein (ziemlich alter) Arbeitsstrom besteht darin, die Speichersicherheit durch die Verwendung (normalerweise eines Stapels von) Regionen zu gewährleisten. Mithilfe der Regionsinferenz kann ein Compiler statisch entscheiden, in welche Region ein Teil der zugewiesenen Daten verschoben werden soll, und die Zuordnung der Region aufheben, wenn diese außerhalb des Gültigkeitsbereichs liegt.

Regionsinferenz ist nachweislich sicher (kann erreichbaren Speicher nicht freigeben) und erfordert nur minimale Programmiererinterferenzen, ist aber nicht "total" (dh es kann immer noch Speicher verlieren, obwohl definitiv viel besser als "nichts tun"), weshalb es normalerweise mit kombiniert wird GC in der Praxis. DasMLtonDer ML Kit-Compiler verwendet Regionen, um die meisten GC-Aufrufe zu eliminieren. Er verfügt jedoch weiterhin über einen GC, da sonst immer noch ein Speicherverlust auftritt. Nach Ansicht einiger der frühen Pioniere in Bezug auf Regionen wurde die Regionsinferenz nicht für diesen Zweck erfunden (ich glaube, für die automatische Parallelisierung). Es stellte sich jedoch heraus, dass es auch für die Speicherverwaltung verwendet werden kann.

Als Ausgangspunkt würde ich für das Papier "Implementierung des typisierten Call-by-Value-λ-Kalküls unter Verwendung eines Stapels von Regionen" von Mads Tofte und Jean-Pierre Talpin sagen. Weitere Artikel zu regionalen Schlussfolgerungen finden Sie in anderen Artikeln von M. Tofte und J.-P. Talpin, einige Arbeiten von Pierre Jouvelot sowie Greg Morrisett, Mike Hicks und Dan Grossmans Reihe von Artikeln über Cyclone.

Ein triviales Schema für die "Bare-Metal" -Systeme besteht darin, einfach alle Laufzeitspeicherzuordnungen zu sperren. Denken Sie daran, dass auch das C- malloc/freePaar eine Laufzeitbibliothek benötigt. Aber auch wenn alle Objekte zur Kompilierungszeit definiert sind, können sie typensicher definiert werden.

Das Hauptproblem dabei ist die Fiktion unveränderlicher Werte in reinen Funktionssprachen, die während des Programmablaufs erstellt werden. Echte Hardware (und sicherlich auch Bare-Metal-Systeme) setzen auf veränderlichen Arbeitsspeicher, der nur in begrenztem Umfang zur Verfügung steht. Die Laufzeit einer Implementierung einer funktionalen Sprache in der Praxis ordnet RAM dynamisch zu, wenn neue "unveränderliche" Werte erstellt werden, und Garbage sammelt sie, wenn der "unveränderliche" Wert nicht mehr benötigt wird.

Bei den interessantesten Problemen hängt die Lebensdauer von mindestens einigen Werten von der Laufzeit- (Benutzer-) Eingabe ab, sodass die Lebensdauer nicht statisch bestimmt werden kann. Aber selbst wenn die Lebensdauer nicht von der Eingabe abhängt, kann sie höchst unwesentlich sein. Nehmen Sie das einfache Programm, das wiederholt Primzahlen findet, indem Sie einfach jede Zahl der Reihe nach prüfen und gegen alle Primzahlen bis zu prüfen sqrt(N). Offensichtlich muss dies die Primzahlen behalten und kann den für die Nicht-Primzahlen verwendeten Speicher recyceln.