Tree Borrows

 (plf.inf.ethz.ch)
1 points par GN⁺ 2025-07-10 | 1 commentaires | Partager sur WhatsApp
  • Tree Borrows, un nouveau modèle mémoire visant à dépasser les limites d’optimisation du code unsafe en Rust, est proposé
  • Là où l’approche Stacked Borrows n’autorisait pas plusieurs motifs courants dans le code Rust en production, Tree Borrows résout le problème grâce à une structure en arbre, en offrant des règles plus réalistes et plus souples
  • Tree Borrows fait passer 54 % de cas de test de code réel en plus que Stacked Borrows
  • Il préserve l’essentiel des garanties de sûreté mémoire et des possibilités d’optimisation de Rust (notamment le read-read reordering), tout en intégrant les fonctionnalités avancées du borrow checker moderne de Rust
  • Il introduit un modèle de machine à états fondé sur un arbre, marquant une étape importante pour la recherche sur l’optimisation de Rust et la vérification de la sûreté

Le système de possession de Rust et les limites du code unsafe

  • Rust offre de fortes garanties, comme la sûreté mémoire et la prévention des data races, grâce à son système de types fondé sur la possession
  • Mais Rust comporte aussi une unsafe escape hatch, dans laquelle la vérification de la sûreté ne relève plus du compilateur mais du développeur
  • Le compilateur aimerait exploiter des règles d’aliasing de pointeurs pour appliquer des optimisations agressives, mais un code unsafe incorrect peut rendre ces optimisations impossibles

Stacked Borrows et ses limites

  • Jusqu’ici, le modèle Stacked Borrows définissait les « comportements incorrects » du code unsafe et servait de référence pour les optimisations
  • Mais cette approche n’autorise pas plusieurs motifs unsafe courants dans le code Rust réel, et ne reflète pas non plus les fonctionnalités récentes du borrow checker de Rust

L’arrivée de Tree Borrows

  • Tree Borrows est un nouveau modèle qui suit les permissions mémoire au moyen d’une structure en arbre plutôt qu’en pile
  • Il permet ainsi d’autoriser en toute sûreté davantage de motifs de code Rust utilisés en pratique, en améliorant nettement la souplesse des règles de borrow et leur applicabilité au monde réel
  • Lors d’une évaluation sur 30 000 crates Rust populaires, il fait passer 54 % de cas de test en plus que Stacked Borrows

Caractéristiques et avantages de Tree Borrows

  • Il conserve l’essentiel des optimisations majeures de Stacked Borrows (par ex. les read-read reorderings)
  • Il peut aussi prendre en compte les fonctionnalités avancées du borrow checker moderne de Rust (par ex. des motifs de borrow atypiques, des manipulations de pointeurs complexes, etc.)
  • Il introduit un modèle de machine à états fondé sur un arbre afin d’équilibrer sûreté et potentiel d’optimisation

Conclusion et portée

  • Tree Borrows établit une nouvelle référence pour le traitement du code unsafe et la recherche sur l’optimisation dans le compilateur Rust
  • Il est considéré comme un modèle mémoire réaliste et robuste, couvrant à la fois le code Rust en production et les politiques récentes du borrow checker
  • L’article scientifique, les artefacts et le code source associés sont publiés, et devraient avoir un impact important sur la communauté de recherche autour du compilateur Rust et de la vérification

À lire aussi

1 commentaires

 
GN⁺ 2025-07-10
Commentaires Hacker News

  • Le récent billet de blog de Ralf Jung apporte davantage de contexte lien
    Bonus : je recommande aussi la récente présentation du groupe de recherche qui tente de spécifier clairement la sémantique d’exécution de Rust dans un dialecte de Rust YouTube

  • On affirme que, du point de vue du compilateur, les fortes garanties du système de types sur l’aliasing de pointeurs permettent des optimisations puissantes, mais je me demande dans quelle mesure c’est réellement efficace
    Linus Torvalds soutient depuis longtemps que les règles de strict aliasing du C sont de peu d’utilité et causent surtout des problèmes
    Son billet avec un exemple est aussi intéressant
    Je me demande si Rust est fondamentalement différent de C sur ce point ; d’après mon expérience personnelle, surtout quand unsafe entre en jeu, la différence ne me paraît pas énorme

    • Je trouve vraiment que les règles de strict aliasing du C sont mauvaises
      Les règles proposées par Rust sont très différentes, plus utiles pour le compilateur, et moins contraignantes pour le programmeur
      On peut s’en abstraire dans le langage en utilisant des raw pointers, et il existe aussi des outils pour vérifier le code
      Au final, comme tout choix de conception de langage, c’est un compromis
      Rust semble avoir trouvé un nouvel équilibre dans cette zone d’optimisation, et le temps dira si ce jugement était le bon

    • Les règles d’aliasing de Rust sont très différentes de celles du C
      En C, le mot-clé restrict n’a pratiquement de sens que pour les arguments de fonction, et l’aliasing basé sur les types (type-based aliasing) est en pratique peu utilisé ou peu pratique à utiliser
      En Rust, on peut exprimer finement les durées de vie et la mutabilité, et manipuler la mémoire de manière sûre de nombreuses façons indépendamment du type lui-même
      Le fait qu’il suffise d’éviter des références &mut qui se chevauchent, tout en pouvant découper en plusieurs &mut non recouvrantes, est un point important

    • J’aimerais voir une analyse plus large de l’impact réel sur les performances
      On pourrait le savoir assez vite en supprimant simplement du compilateur toute la partie qui transmet les informations d’aliasing à LLVM, puis en comparant les performances
      Il y a aussi l’affirmation selon laquelle l’annotation noalias améliore les performances d’environ 5 % à l’exécution ; voir ce commentaire (même si les données sont anciennes)

    • Il faut prendre avec recul ce que dit Linus sur les compilateurs
      Un noyau OS et un compilateur, ce sont deux domaines complètement différents
      Aujourd’hui, l’analyse d’aliasing est vraiment au cœur de fortes améliorations de performances
      Les gains les plus importants viennent d’heuristiques simples, et les requêtes d’aliasing complexes ont en elles-mêmes une utilité plus limitée
      J’aimerais faire une expérience pour voir de combien une analyse d’aliasing théoriquement parfaite améliorerait les performances, mais j’ai l’impression qu’on atteindrait une limite d’environ 20 % même sur du code général
      Bien sûr, certaines optimisations très avancées (par ex. les transformations de layout de données) ont aussi la limite qu’on n’essaiera même pas de les faire sans analyse d’aliasing

    • Le strict aliasing du C et l’aliasing de Rust sont des concepts différents
      En C, le cœur du sujet est la TBAA (type-based analysis aliasing), et Rust a délibérément choisi de ne pas l’adopter

  • Il y a eu d’anciens fils sur Stacked Borrows en 2020 et 2018
    Fil 2020
    Fil 2018

  • J’ai lu la spécification de Tree Borrows sur le site de Nevin il y a quelques années, et j’avais été impressionné par la façon élégante dont elle résolvait des problèmes complexes
    En pratique, Tree Borrows permet du code raisonnable qui n’est pas possible avec Stacked Borrows
    Le code d’exemple de la bibliothèque standard de Rust vaut aussi le détour

  • Je me demande si Rust, ou un langage de programmation de nouvelle génération, pourrait évoluer pour permettre de choisir entre plusieurs implémentations de borrow checker aux caractéristiques et objectifs différents (vitesse de compilation, vitesse d’exécution, flexibilité algorithmique, etc.)

    • Rust prend déjà en charge le changement d’implémentation du borrow checker
      On est passé d’un modèle fondé sur la portée à un modèle non lexical, et Polonius est aussi disponible comme implémentation expérimentale
      Quand une nouvelle implémentation est prête, il n’y a pas vraiment de raison de conserver l’ancienne
      On peut aussi écrire de façon plus souple avec Rc, RefCell, etc., qui nécessitent des vérifications à l’exécution

    • Il existe déjà diverses approches : types affines (utilisés par Rust), types linéaires, systèmes d’effets, types dépendants, preuves formelles, etc.
      Chaque approche a ses propres caractéristiques en matière de coût d’implémentation, de performances, d’expérience développeur, etc.
      Au-delà de Rust, il y a aussi une tendance à rechercher la combinaison entre gestion automatique productive des ressources et système de types

    • Ce qu’il faut réellement, c’est une logique de séparation permettant de spécifier précisément les préconditions d’une fonction et même de prouver les conditions intermédiaires
      L’approche de Rust consiste à systématiser les invariants ordinaires que les gens veulent réellement, tout en garantissant de fortes optimisations

    • Je me demande si le résultat du borrow checker n’a que des faux négatifs et pas de faux positifs
      Si c’est le cas, est-ce qu’on pourrait faire tourner plusieurs implémentations en parallèle sur différents threads et utiliser le résultat du gagnant le plus rapide ?

    • Autoriser simultanément plusieurs implémentations de borrow checker risquerait de fragmenter l’écosystème, donc ce ne serait pas souhaitable

  • J’ai effectivement testé le code Rust présenté dans l’article, et j’ai confirmé qu’il n’est pas rejeté par le compilateur stable le plus récent
    Exemple de code :

    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 est le modèle d’exécution de miri
      Si on exécute le code ci-dessus dans miri, il signale une erreur sur *x = 10;, mais write(x); ne provoque pas d’erreur
      Du point de vue du système de types, rustc n’a aucune raison de rejeter l’une ou l’autre version, puisque y est de type *mut

  • L’article donne l’exemple suivant comme problème de code unsafe :

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

    Je me demande si cela est réellement possible
    Utiliser plusieurs références mutables vers la même variable via des pointeurs est clairement de l’UB, donc je me demande si je ne passe pas à côté de quelque chose

    • Le cœur de cette recherche est de spécifier précisément la frontière de l’UB (comportement indéfini)
      Le code ci-dessus enfreint les règles, même si le compilateur Rust l’accepte
      Quelles règles ?

  • Le code qui passe le borrow checker est légal

  • unsafe peut aussi exprimer des choses illégales / de l’UB

  • Il existe un ensemble de règles plus large que le périmètre du borrow checker, mais qui reste légal
    Le but de cette recherche est de définir rigoureusement cette frontière
    L’article sur Stacked Borrows était plus simple, mais il avait des limites avec le vrai code unsafe, et Tree Borrows reconnaît un périmètre de sûreté plus large

    • Il est clair que « plusieurs pointeurs de références mutables ne peuvent pas exister simultanément », mais je n’ai vu nulle part une mention explicite de la règle exacte que cela violerait
      Tree Borrows propose précisément ce genre de définition
      Quand on dit que « le code peut faire ce genre de chose », cela signifie qu’on peut réellement écrire et exécuter ce code, mais que sans une définition comme Tree Borrows il est difficile d’établir pourquoi c’est incorrect
      On dirait que tu reconnais déjà toi-même la nécessité de règles claires comme celles de Tree Borrows

    • Du code unsafe comme cela est bel et bien possible en pratique, et c’est justement pour cela que c’est de l’UB
      Exemple : lien playground

    • Si tu veux le contexte, le début du paragraphe suivant dans l’article exprime bien l’intention

Si les développeurs du compilateur Rust veulent des optimisations d’aliasing, ils ont besoin d’un moyen d’exclure des contre-exemples comme le code ci-dessus

  • Oui, c’est exactement le point
    Cela reflète à quel point il est difficile de respecter la règle interdisant plusieurs références mutables, et combien unsafe peut autoriser davantage de choses que ce que garantit le système de lifetimes de Rust

  • L’un des auteurs, Neven Villani, est le fils de Cédric Villani, médaille Fields 2010
    On pense à l’expression selon laquelle les chiens ne font pas des chats

    • Et j’avais aussi envie de faire le trait d’esprit selon lequel « les qualités aussi ont été empruntées à l’arbre »

    • J’ai même eu un bureau proche de celui du père (lauréat de la médaille Fields) à une époque
      C’était avant son entrée en politique

  • Ce modèle est vraiment excellent
    Je vais aussi l’implémenter dans le langage que je développe

  • Impossible que ce soit un déjà-vu
    J’ai l’impression de revoir ce post tous les 2 ou 3 mois

    • L’article a été préparé sur plusieurs années, et il est enfin publié officiellement maintenant