Tree Borrows

 (plf.inf.ethz.ch)
1 Punkte von GN⁺ 2025-07-10 | 1 Kommentare | Auf WhatsApp teilen
  • Tree Borrows wird als neues Speichermodell vorgeschlagen, um die Grenzen bei der Optimierung von unsafe-Code in der Programmiersprache Rust zu überwinden
  • Das bisherige Verfahren Stacked Borrows konnte mehrere in praktischem Rust-Code häufig verwendete Muster nicht zulassen; Tree Borrows löst dieses Problem mit einer Baumstruktur und bietet realistischere und flexiblere Regeln
  • Tree Borrows besteht 54 % mehr Testfälle aus realem Code als Stacked Borrows
  • Zugleich bleiben die wesentlichen Aspekte von Rusts Speichersicherheit und Optimierbarkeit erhalten, insbesondere etwa read-read reordering, und auch fortgeschrittene Funktionen des aktuellen Rust-Borrow-Checkers werden berücksichtigt
  • Mit der Einführung eines baum­basierten Zustandsautomatenmodells setzt es einen wichtigen Meilenstein für die Forschung zu Rust-Optimierungen und zur Verifikation von Sicherheit

Rusts Ownership-System und die Grenzen von unsafe-Code

  • Rust bietet durch ein Ownership-basiertes Typsystem starke Garantien wie Speichersicherheit und die Vermeidung von Data Races
  • Allerdings besitzt Rust einen unsafe escape hatch; in diesem Fall liegt die Verantwortung für die Sicherheitsprüfung nicht mehr beim Compiler, sondern bei den Entwicklerinnen und Entwicklern
  • Der Compiler möchte Regeln für Pointer-Aliasing nutzen, um starke Optimierungen durchzuführen, doch fehlerhafter unsafe-Code kann solche Optimierungen unwirksam machen

Stacked Borrows und seine Grenzen

  • Bisher definierte das Modell Stacked Borrows das „fehlerhafte Verhalten“ von unsafe-Code und gab Kriterien für Optimierungen vor
  • Dieser Ansatz konnte jedoch mehrere in echtem Rust-Code verbreitete unsafe-Muster nicht zulassen und berücksichtigte auch neu eingeführte Funktionen des Rust-Borrow-Checkers nicht

Das Aufkommen von Tree Borrows

  • Tree Borrows ist ein neues Modell, das Speicherberechtigungen nicht mehr in einer Stack-, sondern in einer Baumstruktur verfolgt
  • Dadurch können mehr Muster aus praktischem Rust-Code sicher zugelassen werden, was die Flexibilität und Praxistauglichkeit der Borrow-Regeln deutlich erhöht
  • Bei der Auswertung von 30.000 populären Rust-Crates bestand es 54 % mehr Testfälle als Stacked Borrows

Merkmale und Vorteile von Tree Borrows

  • Die wesentlichen Optimierungen von Stacked Borrows, etwa read-read reorderings, bleiben weitgehend erhalten
  • Zudem lassen sich fortgeschrittene Funktionen des aktuellen Rust-Borrow-Checkers berücksichtigen, etwa untypische Borrow-Muster oder komplexe Pointer-Manipulationen
  • Durch die Einführung eines baum­basierten Zustandsautomatenmodells wird ein Gleichgewicht zwischen Sicherheit und Optimierbarkeit geschaffen

Fazit und Bedeutung

  • Tree Borrows setzt einen neuen Maßstab für den Umgang des Rust-Compilers mit unsafe-Code und für die Forschung zu Optimierungen
  • Es gilt als realistisches und robustes Speichermodell, das sowohl praktischen Rust-Code als auch die aktuelle Politik des Borrow-Checkers abdeckt
  • Die zugehörige Arbeit, Artefakte und der Source Code sind öffentlich verfügbar und dürften die Community rund um Rust-Compiler und Verifikationsforschung stark beeinflussen

Verwandte Beiträge

1 Kommentare

 
GN⁺ 2025-07-10
Hacker-News-Kommentare

  • Ralf Jungs jüngster Blogpost liefert mehr Kontext Link
    Bonus: Empfehlenswert ist auch ein jüngster Vortrag einer Forschungsgruppe, die versucht, die Ausführungssemantik von Rust klar in einem Rust-Dialekt zu spezifizieren YouTube

  • Es wird behauptet, dass Compiler dank starker Garantien des Typsystems in Bezug auf Pointer-Aliasing starke Optimierungen durchführen können, aber ich frage mich, wie wirksam das in der Praxis tatsächlich ist.
    Linus Torvalds vertritt seit Langem die Ansicht, dass die strict-aliasing-Regeln von C wenig Nutzen bringen und eher Probleme verursachen.
    Sein Beitrag mit Beispiel ist ebenfalls interessant.
    Ich frage mich, ob Rust im Kern wirklich grundlegend anders als C ist; meiner persönlichen Erfahrung nach fühlt es sich, besonders wenn unsafe beteiligt ist, nicht sehr anders an.

    • Ich halte die strict-aliasing-Regeln von C wirklich für ziemlich schlecht.
      Die für Rust vorgeschlagenen Regeln sind deutlich anders, aus Sicht des Compilers nützlicher und für Programmierer weniger belastend.
      Mit Raw Pointern gibt es ein Opt-out innerhalb der Sprache, und es gibt Tools, mit denen sich Code prüfen lässt.
      Letztlich ist es wie jedes Sprachdesign ein Kompromiss.
      Rust scheint in diesem Optimierungsbereich ein neues Gleichgewicht gefunden zu haben, und die Zeit wird zeigen, wie gut diese Entscheidung war.

    • Rusts Aliasing-Regeln unterscheiden sich stark von denen in C.
      In C hat das Schlüsselwort restrict fast nur bei Funktionsargumenten Bedeutung, und typbasiertes Aliasing wird in der Praxis kaum genutzt oder ist unbequem zu verwenden.
      In Rust lassen sich Lifetimes und Mutabilität präzise ausdrücken, und Speicher kann auf viele Arten sicher behandelt werden, unabhängig vom Typ selbst.
      Entscheidend ist auch, dass nur überlappende &mut-Referenzen verboten sind, während mehrere nicht überlappende &mut-Bereiche durch Aufteilen durchaus nutzbar sind.

    • Mich würde eine breitere Analyse interessieren, wie stark sich das tatsächlich auf die Performance auswirkt.
      Man könnte es direkt testen, indem man im Compiler einfach alle Teile entfernt, die Aliasing-Informationen an LLVM weitergeben, und dann die Performance vergleicht.
      Es gibt auch die Behauptung, dass die Annotation noalias die Laufzeitleistung um etwa 5 % verbessert; dazu gibt es einen Kommentar (auch wenn die Daten schon älter sind).

    • Was Linus über Compiler sagt, sollte man mit Vorsicht betrachten.
      Betriebssystemkernel und Compiler sind völlig unterschiedliche Bereiche.
      Heutzutage ist Alias-Analyse wirklich ein Schlüssel für starke Performance-Verbesserungen.
      Die größten Effekte kommen aus einfachen Heuristiken, während komplexe Alias-Abfragen für sich genommen weniger nützlich sind.
      Ich würde theoretisch gern testen, wie viel perfekte Alias-Analyse an Performance bringen würde, aber selbst bei allgemeinem Code vermute ich, dass etwa 20 % die Obergrenze wären.
      Natürlich gibt es bei sehr fortgeschrittenen Optimierungen, etwa Datenlayout-Transformationen, die Grenze, dass man sie ohne Alias-Analyse gar nicht erst versucht.

    • Strict Aliasing in C und Aliasing in Rust sind konzeptionell verschieden.
      In C steht typbasierte Analyse (TBAA) im Mittelpunkt, und Rust hat das absichtlich nicht übernommen.

  • Zu Stacked Borrows gab es frühere Threads aus 2020 und 2018.
    Thread von 2020
    Thread von 2018

  • Ich habe die Tree-Borrows-Spezifikation vor ein paar Jahren auf Nevins Website gelesen und war beeindruckt, wie elegant sie auch komplizierte Probleme löst.
    Aus tatsächlicher Erfahrung ermöglicht Tree Borrows vernünftigen Code, der unter Stacked Borrows nicht möglich wäre.
    Auch der Beispielcode in der Rust-Standardbibliothek ist sehenswert.

  • Ich frage mich, ob Rust oder eine nächste Generation von PLs sich so entwickeln könnte, dass man zwischen mehreren Implementierungen des Borrow Checkers wählen kann, je nach Eigenschaften und Zielsetzung wie Kompiliergeschwindigkeit, Laufzeitgeschwindigkeit oder algorithmische Flexibilität.

    • Rust unterstützt bereits den Wechsel der Borrow-Checker-Implementierung.
      Es wurde von einer scope-basierten Variante auf nicht-lexikalische Lifetimes umgestellt, und mit Polonius gibt es auch eine experimentelle Implementierung als Option.
      Wenn eine neue Implementierung bereit ist, lässt man die alte nicht unbedingt bestehen.
      Man kann außerdem flexibler arbeiten, etwa mit Rc oder RefCell, wo Laufzeitprüfungen nötig sind.

    • Es gibt bereits viele Ansätze wie affine types (wie in Rust verwendet), lineare Typen, Effektsysteme, abhängige Typen und formale Beweise.
      Jeder Ansatz hat andere Eigenschaften in Bezug auf Implementierungskosten, Performance und Entwicklererfahrung.
      Auch jenseits von Rust gibt es die Tendenz, produktive automatische Ressourcenverwaltung mit Typsystemen zu kombinieren.

    • Was man tatsächlich braucht, ist Separation Logic, mit der sich Vorbedingungen von Funktionen präzise angeben und sogar Zwischenbedingungen beweisen lassen.
      Rusts Ansatz besteht darin, die gewöhnlichen Invarianten, die Menschen tatsächlich wollen, zu systematisieren und dadurch starke Optimierungen zu garantieren.

    • Ich frage mich, ob es stimmt, dass die Ergebnisse des Borrow Checkers nur false negatives, aber keine false positives haben.
      Falls ja, wäre es dann vielleicht möglich, mehrere Implementierungen parallel in Threads laufen zu lassen und das Ergebnis des schnellsten Gewinners zu verwenden?

    • Mehrere Borrow-Checker-Implementierungen gleichzeitig zuzulassen wäre wohl nicht wünschenswert, weil das Ökosystem dadurch leicht fragmentieren könnte.

  • Ich habe den Rust-Code aus dem Paper tatsächlich getestet und bestätigt, dass er vom aktuellen stabilen Compiler nicht abgelehnt wird.
    Beispielcode:

    fn write(x: &mut i32) {*x = 10}

fn main() {
  let x = &mut 0;
  let y = x as *mut i32;
  //write(x); 
  *x = 10; 
  unsafe {*y = 15 };
}
    • Stacked Borrows ist das Laufzeitmodell von miri.
      Wenn man den obigen Code in miri ausführt, meldet es bei *x = 10; einen Fehler, aber bei write(x); tritt kein Fehler auf.
      rustc hat aus Sicht des Typsystems keinen Grund, eine der beiden Versionen abzulehnen, weil y ein *mut ist.

  • Das Paper führt das folgende Beispiel als Problem mit unsafe-Code an:

    fn main() {
  let mut x = 42;
  let ptr = &mut x as *mut i32;
  let val = unsafe { write_both(&mut *ptr, &mut *ptr) };
  println!("{val}");
}

    Ich frage mich, ob das in der Praxis wirklich möglich ist.
    Mehrere mutable Referenzen auf dieselbe Variable über Pointer zu verwenden ist doch eindeutig UB, daher frage ich mich, ob ich hier etwas missverstehe.

    • Der Kern dieser Forschung besteht darin, die Grenzen von UB (undefiniertem Verhalten) präzise festzulegen.
      Der obige Code wird vom Rust-Compiler vielleicht akzeptiert, verletzt aber die Regeln.
      Welche Regeln?

  • Code, der den Borrow Checker besteht, ist legal.

  • unsafe kann auch illegale Fälle bzw. UB ausdrücken.

  • Es gibt eine Regelmenge, die breiter ist als der Geltungsbereich des Borrow Checkers und dennoch legal bleibt.
    Ziel dieser Forschung ist es, diese Grenze streng zu spezifizieren.
    Das Stacked-Borrows-Paper ist einfacher, hatte aber Grenzen bei realem unsafe-Code, während Tree Borrows einen größeren sicheren Bereich anerkennt.

    • Es ist zwar klar, dass „mehrere mutable Referenz-Pointer nicht gleichzeitig existieren können“, aber nirgends wird ausdrücklich benannt, welche genaue Regel dabei verletzt wird.
      Genau so eine Definition schlägt Tree Borrows vor.
      Die Aussage „Code kann so etwas tun“ bedeutet, dass man den betreffenden Code tatsächlich erzeugen und ausführen kann, aber ohne eine Definition wie Tree Borrows nur schwer begründen kann, warum das falsch ist.
      Du scheinst die Notwendigkeit klarer Regeln wie Tree Borrows selbst bereits zu akzeptieren.

    • unsafe-Code dieser Art ist tatsächlich möglich, und genau das ist UB.
      Beispiel: Playground-Link

    • Wenn du den Kontext dazu verstehen willst, zeigt der Beginn des direkt folgenden Absatzes im Paper die Absicht ziemlich gut.

Wenn Rust-Compiler-Entwickler Alias-Optimierungen wollen, brauchen sie eine Möglichkeit, Gegenbeispiele wie den obigen Code auszuschließen.

  • Genau das ist der Punkt.
    Die Regel, mehrere mutable Referenzen zu verbieten, ist schwer einzuhalten, und unsafe spiegelt wider, dass deutlich mehr möglich ist als das, was Rusts Lifetimesystem garantiert.

  • Einer der Autoren, Neven Villani, ist der Sohn von Cédric Villani, dem Fields-Medaillen-Gewinner von 2010.
    Da denkt man an das Sprichwort, dass der Apfel nicht weit vom Stamm fällt.

    • Und man könnte auch witzeln, dass er sogar „qualities“ vom Baum geborgt hat.

    • Ich hatte auch einmal ein Büro in der Nähe seines Vaters, des Fields-Medaillen-Gewinners.
      Das war noch vor seinem Eintritt in die Politik.

  • Dieses Modell ist wirklich großartig.
    Ich werde es wahrscheinlich auch in der Sprache implementieren, an der ich arbeite.

  • Das kann kein Déjà-vu sein.
    Ich habe das Gefühl, diesen Post alle zwei bis drei Monate wieder zu sehen.

    • Das Paper wurde über mehrere Jahre vorbereitet und ist jetzt endlich offiziell veröffentlicht worden.