Ante: Ein neuer Ansatz, der Borrow Checking und Referenzzählung kombiniert

 (verdagon.dev)
1 Punkte von GN⁺ 4 시간 전 | 1 Kommentare | Auf WhatsApp teilen
  • Ante ist der Entwurf einer Systemsprache, die die Flexibilität von Referenzzählung mit der Sicherheit von Borrow Checking verbinden will, ohne Rust-artige Runtime-Panics oder den Overhead von Swifts Laufzeitprüfung auf exklusiven Zugriff
  • Der Kernmechanismus besteht aus shape-stability und temporary uniq conversion: Für Felder referenzgezählter Werte lassen sich sicher mutable Borrows erzeugen, während Werte innerhalb von Unions nur in begrenztem Umfang als uniq behandelt werden
  • Rusts Rc<RefCell<T>> kann bei falscher Nutzung zur Laufzeit panicken, und Swifts Borrowing-System enthält Laufzeitprüfungen auf exklusiven Zugriff; Ante versucht dagegen, einige Fälle über Compile-Time-Regeln abzudecken
  • Es handelt sich noch um ein nur teilweise implementiertes Work-in-progress-Design; da Typen rekursiv analysiert werden müssen, um zu bestimmen, ob ein bestimmtes Objekt erreichbar ist, kann das Hinzufügen eines Feldes zu einem Breaking API Change werden
  • Dieser Ansatz schwächt die Annahme ab, dass shared mutable borrowing grundsätzlich unmöglich sei, und erweitert zusammen mit Techniken wie Vale, group borrowing und Rust GhostCell den Ausnahmebereich im Design von Speichersicherheit

Die Kombination, auf die Ante abzielt

  • Ante ist eine Systemprogrammiersprache, die eine einfachere Variante von Rust mit Speichersicherheit und Thread-Sicherheit anstrebt
  • Das Grundmodell sind Single Ownership und Borrow Checking; Werte liegen inline auf dem Stack oder innerhalb der enthaltenden Structs bzw. Arrays
  • Wenn Einfachheit Vorrang haben soll, kann man durch das Schlüsselwort shared an einem Typ Referenzzählung wählen
  • Eine balance-Funktion für einen Red-Black-Tree mit shared type Color und shared type RbTree t ist etwa so kurz wie das Python-Beispiel und kleiner als die C++- und Rust-Beispiele
  • Die zentrale Frage ist, wie sich referenzgezählte Daten mutable borrowen lassen, ohne Rusts Risiko eines borrow_mut()-Panics oder Swifts Laufzeitprüfung auf exklusiven Zugriff
  • Ante befindet sich noch im Work-in-progress-Status: Einiges ist implementiert, einiges theoretisch, und auch das Design verändert sich noch

shape-stability und mehrere mutable Referenzen

  • Antes shape-stability bezeichnet die Idee, dass „eine Referenz auf ein Ziel mit stable shape immer gültig bleibt, egal welche Änderungen anderswo passieren“
  • Dieses Konzept macht es möglich, gleichzeitig mehrere mutable Borrow-Referenzen auf dasselbe Struct zu haben
  • Im Beispiel heal (healer: mut Entity) (target: mut Entity) ist ein self_heal-Aufruf möglich, bei dem dieselbe Entity als beide Argumente übergeben wird
    • Selbst wenn healer und target auf dieselbe Entity zeigen, kann dieser Code die Entity nicht zerstören, sodass beide Referenzen weiterhin gültig bleiben
  • Auch mutable Referenzen auf ein Struct selbst, auf seine Felder und auf Felder dieser Felder können gleichzeitig erlaubt sein
    • Selbst wenn ship: mut Spaceship und engine_alias: mut Engine = ship.engine gleichzeitig verwendet werden, wird angenommen, dass während der Funktionsausführung weder ship noch die darin enthaltene engine zerstört werden
  • Rust und Swift erlauben keine Form, bei der mehrere &mut-Referenzen gleichzeitig auf dieselben Daten zeigen

Mutable Borrows von Feldern referenzgezählter Werte

  • Wenn in Ante einer Typdefinition shared vorangestellt wird, wird dieser Typ automatisch referenzgezählt
  • Im Beispiel shared mut type Spaceship hält launch ein Spaceship, das einem Rc entspricht, und übergibt mut ship.engine an set_fuel
  • Da launch das enthaltende Objekt Spaceship am Leben hält, kann auch dessen Feld engine als lebendig betrachtet werden
  • Die allgemeine Regel lautet: Für Felder eines shared mut-Typs kann immer eine mut-Borrow-Referenz erzeugt werden
    • Allerdings lässt sich nicht für jedes Objekt innerhalb dieses Feldes immer ein mutable Borrow erzeugen; dafür braucht es zusätzliche Regeln
  • Die folgenden Beispiele verwenden statt des Syntax-Zuckers shared mut type Spaceship die explizitere Schreibweise Rc Spaceship
    • shared mut type Spaceship wird zu type Spaceship, und var ship: Spaceship wird zu var ship: Rc Spaceship

Wo Unions Sicherheitsprobleme erzeugen

  • Unions können Inhalte inline speichern und dadurch Pointer-Chasing und Cache-Misses reduzieren, was der Geschwindigkeit zugutekommt
    • Wenn Cs union Engine in einem struct Spaceship liegt, befinden sich StringTheoryEngine und ImpulseEngine im Speicher des Spaceship
    • Das steht im Gegensatz zu einem Ansatz wie in Java mit Interfaces und Pointern
  • Das Problem ist, dass sichere Unterstützung für Unions in speichersicheren Sprachen schwierig ist
  • In einem Beispiel, in dem Engine entweder StringTheoryEngine(str: String) oder ImpulseEngine(fuel: I32) ist, kann es zu einem Segfault kommen, wenn ship und other_ship auf dasselbe Spaceship zeigen
    • Nach match uniq ship.engine wird eine Referenz auf das Innere des Strings gehalten
    • Dann wird mit other_ship.engine := ImpulseEngine 0x42 dieselbe Engine in eine andere Variante geändert
    • Wenn anschließend das alte str verändert wird, wird Inneres verwendet, nachdem der Container zerstört wurde
  • Daher muss Ante verhindern, dass aus einer mutable Borrow-Referenz, die auf eine Union zeigt, eine mutable Borrow-Referenz auf eine ihrer Varianten erzeugt wird
  • Das ist das Gegenteil der Struct-Regel
    • Hat man eine mut-Referenz auf ein Struct, kann man eine mut-Referenz auf ein Feld erzeugen
    • Hat man eine mut-Referenz auf eine Union, kann man keine mut-Referenz auf das Innere einer Variante erzeugen

uniq und temporary uniq conversion

  • uniq steht für exclusive mutable reference, also eine exklusiv mutable Referenz
  • Wenn eine Variable ein uniq Spaceship enthält, ist sie die einzige nutzbare Referenz auf dieses Spaceship
    • Das ist ein ähnliches Konzept wie Rusts &mut Spaceship
  • Um das Innere von Unions sicher zu behandeln, verwendet Ante temporary uniq conversion
  • Die Kernregel lautet: Wenn in einem bestimmten Scope keine anderen potenziell aliasenden Referenzen verwendet werden, kann temporär eine uniq-Referenz erhalten werden
    • Im Bereich match uniq ship.engine wird auf ship.engine wie über uniq zugegriffen
    • Während dieses Bereichs verhindert der Compiler die Nutzung anderer bereits existierender Variablen, die indirekt ein Spaceship enthalten könnten
  • Während Rust die Existenz von uniq schon deshalb verhindert, weil „andere Referenzen irgendwo vorhanden sein könnten“, erlaubt Ante uniq unter der Bedingung, dass diese Referenzen in diesem Scope nicht verwendet werden
  • Dabei ist uniq Spaceship tatsächlich nicht global die einzige Referenz, sondern die einzige in diesem Scope nutzbare Referenz
    • Die Nuance ähnelt Cs restrict-Pointer

Erlaubte und abgelehnte Zugriffe

  • Wenn innerhalb des Bereichs match uniq ship.engine auf other_ship: Rc Spaceship zugegriffen wird, sollte ein Compile-Fehler entstehen
    • other_ship.engine könnte ein Alias von ship.engine sein
    • Und eine Änderung von other_ship.engine könnte während der Nutzung von ship.engine einen Drop auslösen
  • Andere Structs, die wie HasAShip ein Rc Spaceship als Feld enthalten, werden aus demselben Grund abgelehnt
    • Auch other.ship.engine kann indirekt dasselbe Spaceship erreichen
  • Umgekehrt kann ein Integer wie new_fuel: I32 verwendet werden
    • Denn I32 kann keine Referenz auf ein Spaceship enthalten
  • Wenn Spaceship selbst ein Feld wie follow_ship: Rc Spaceship enthält, wird es abgelehnt
    • In diesem Fall wäre auch uniq Spaceship über einen Pfad im eigenen Inneren wieder erreichbar; daher kann man rekursive Typen im Allgemeinen nicht von mut nach uniq konvertieren

Einschränkungen bei Funktionsaufrufen und Rückgaben

  • Auch bei Funktionsaufrufen kann eine mut -> uniq-Konvertierung stattfinden
  • Wenn foo (var ship: Rc Spaceship) (new_res: Resonator) maybe_use_resonator ship new_res aufruft, wird ship an der Aufrufstelle in uniq Spaceship konvertiert
    • Der Compiler muss nur prüfen, ob andere Argumente eine Spaceship-Referenz enthalten können
    • Der Resonator im Beispiel enthält keine solche Referenz, daher ist es erlaubt
  • Bei Rückgaben kann die konvertierte uniq-Referenz nicht als normale uniq zurückgegeben werden
    • Nach der Rückgabe greift die Compilerprüfung „im Scope werden keine aliasfähigen Variablen verwendet“ nicht mehr
  • Stattdessen kann der Rückgabetyp als local uniq Foo angegeben werden
    • Intern entsteht beim Konvertieren von mut ref zu uniq ref tatsächlich immer eine local uniq
    • In den meisten Fällen kann sie wie eine normale uniq verwendet werden, bei Rückgaben ist aber eine explizite Angabe nötig

Designkosten und Alternativen

  • Ante kann eine referenzgezählte Referenz wie Rc Spaceship ohne Runtime-Fehler temporär in uniq Spaceship umwandeln
  • Der Nachteil ist, dass der Compiler Typen rekursiv untersuchen muss, um Fragen wie „Kann man von Engine aus ein Spaceship erreichen?“ zu beantworten
  • Eine solche Analyse kann fragil sein
    • Das Hinzufügen eines Feldes zu einem Struct kann zu einem Breaking API Change werden
  • Jake, der Entwickler von Ante, sucht nach besseren Wegen, diese Garantie aufrechtzuerhalten
    • Einen Ansatz wie group borrowing und Flix references, bei dem jedem shared mutable Typ ein anonymer eindeutiger Brand-Typ zugeordnet wird
    • Einen Ansatz, bei dem beim Ändern eines shared Typs ein Effect wie Mutates 'a hinzugefügt wird, um die Typanalyse zu eliminieren
    • Einen Ansatz, bei dem Nutzer zur Laufzeit prüfen, ob zwei Referenzen auf unterschiedliche Objekte zeigen, oder bei dem eine safe API eine unsafe Prüfung kapselt
    • Einen Ansatz, bei dem der Compiler Werte verfolgt, die nicht indirekt in einem Rc gespeichert sind und daher nicht aliasen können
  • Auch eine Idee ähnlich Ponys iso permission oder eine temporäre Berechtigung, die zwar ins Innere eines Structs schaut, aber keine nach außen zeigenden Referenzen verwenden lässt, bleibt möglich
  • Schwierig ist, diese Flexibilität zu erhalten und zugleich Antes Ziele Benutzbarkeit, Lesbarkeit und Einfachheit zu wahren

Der breitere Trend bei Speichersicherheit

  • Shared mutable borrowing galt früher als unmöglich; zugrunde liegt die Sichtweise, dass auch Rust auf dieser Annahme entworfen wurde
  • Mehrere Ausnahmen häufen sich an
    • Ante kann durch Regeln für local uniqueness uniq-Borrow-Referenzen aus shared-mutable Daten gewinnen
    • Vale kann über pure functions unveränderliche Borrow-Referenzen aus shared-mutable Daten gewinnen
    • group borrowing kann shared-mutable Borrow-Referenzen erzeugen, auch wenn etwas nicht shape-stable ist
    • Rusts GhostCell erlaubt Objektgraphen, die frei aufeinander zeigen können, aber zu einem bestimmten Zeitpunkt nur eine mutable Referenz auf eines dieser Objekte haben
  • Dieser Trend deutet darauf hin, dass es im Design von Speichersicherheit allgemeinere Prinzipien für den Umgang mit shared mutable borrowing geben könnte

Vergleich mit Rusts Cell

  • Rust-Nutzer könnten nach dem Unterschied zwischen dem Einfügen von Cell in Struct-Felder und Antes Ansatz fragen
  • Im Ante-Beispiel kann man aus Rc Spaceship eine mut String-Referenz auf status: String erhalten und " (refueling)" direkt anhängen
  • Mit Rusts Cell<String>-Ansatz kann man aus Rc<Spaceship> kein &mut String erhalten
    • Stattdessen muss man mit status_ref.replace(String::new()) einen temporären Standardwert einsetzen
    • Den herausgenommenen String verändern
    • Und ihn am Ende mit replace(status) wieder zurücksetzen
  • Dieser Ansatz hat einige Nachteile
    • Es muss eine Standardinstanz wie "" erzeugt werden
    • Man kann den letzten replace-Aufruf vergessen
    • Jemand könnte status lesen, während der Wert ersetzt ist
  • Ante lässt temporär eine Referenz auf den status-String zu und erzwingt währenddessen per Compiler, dass kein anderer Code darauf zugreift

Verwandte Beiträge

1 Kommentare

 
GN⁺ 4 시간 전
Lobste.rs-Kommentare

  • Dass man „geteiltes veränderliches Borrowing“ für unmöglich hielt, war nicht einfach nur ein Opfer, das Rust zur Erreichung seiner Ziele in Kauf nahm, sondern liegt eher am Kern von Rusts eigentlichen Zielen
    Denn geteilter veränderlicher Zustand erschwert das lokale Schließen über Code
    "References are like jumps" von withoutboats behandelt diesen Punkt gut. Zu verhindern, dass Zustand mit Aliasen versehentlich verändert wird, ist zentral dafür, leichter Systeme zu bauen, die korrekt funktionieren, und Rusts Lifetime-Regeln sind nicht bloß ein Mittel, um Garbage Collection zu vermeiden, sondern laut dieser Sicht eine tiefere Struktur, die Inferenzfähigkeit in einer Sprache sicherstellt, die veränderlichen Zustand und aliasierten Zustand zugleich erlaubt

    • Als der Autor früher den Mojo Borrow Checker behandelte, hatte ich denselben Gedanken. Rusts Borrow Checker bewahrt auch in Single-Thread-Programmen Wertsemantik

  • Sieht ziemlich gut aus
    Wenn ich es richtig verstanden habe, ist die Magie beim Übergang von einer geteilten Referenz zu einer veränderlichen Referenz möglich, weil sie auf Typen beschränkt ist, die nicht zwischen Threads geteilt werden, und die Eindeutigkeit von Rc scheint dadurch garantiert zu werden, dass alle Objekte desselben Typs so behandelt werden, als würden sie mit derselben Lifetime geborgt
    Ob explizite oder natürlichere Syntax besser ist, ist vielleicht Geschmackssache, aber es zeigt, dass der Compiler, wenn er mehr über Cell weiß, veränderliche Referenzen darauf flexibler zulassen kann
    Und man vermeidet auch die verwirrende Terminologie in Rust, bei der mut nicht Veränderlichkeit, sondern Exklusivität/Eindeutigkeit zu bedeuten scheint

    • Ich habe mich gefragt, wie das zwischen Threads funktionieren würde. So etwas wie: „Bedeutet uniq-Promotion das Erwerben eines Locks?“ Aber ich verstehe es so, dass der Vergleich nicht mit Arc, sondern mit Rc gemeint ist
    • Könntest du den Teil näher erläutern, dass mut Exklusivität/Eindeutigkeit bedeutet?

  • Ich frage mich, ob jemand eine Vermutung hat, welches vereinheitlichende Prinzip am Ende angedeutet wurde

  • Auch die früheren Diskussionen zu Blogposts auf antelang.org sind lesenswert

  • Ich verstehe nicht wirklich, wie das funktionieren soll. Es klingt so, als hieße es: „Wenn man einen veränderlichen Pointer auf ein Objekt hat, kann man eine veränderliche Referenz auf einen Slice dieses Objekts erhalten“
    Wenn das so ist, scheint zum Beispiel so etwas möglich zu sein wie mutref someobjext = …, mutref subfield = someobjext.a.b, someobjext.a = somethingelse, und dann könnte subfield ungültig werden oder kaputtgehen, weil sich der Wert ändert
    Der Artikel hatte viele Erklärungen, Vergleiche mit anderen Sprachen und Codebeispiele, aber ich konnte kaum eine Stelle finden, die die Schritt-für-Schritt-Semantik dieses Verhaltens grundlegend erklärt