1 points par GN⁺ 2025-07-10 | 1 commentaires | Partager sur WhatsApp
  • Pour que le compilateur Rust puisse exploiter les garanties d’aliasing des pointeurs dans ses optimisations, il faut définir clairement où le code unsafe enfreint les règles
  • Le modèle existant Stacked Borrows proposait ce critère, mais il ne prend pas suffisamment en charge les motifs courants du code Rust unsafe réel ni les fonctionnalités récentes du borrow checker
  • Tree Borrows remplace la structure centrale de Stacked Borrows, une pile, par un arbre, afin de pouvoir exprimer davantage de motifs valides
  • Dans une évaluation portant sur les 30 000 crates Rust les plus utilisées, il rejette 54 % de cas de test en moins que Stacked Borrows
  • Une preuve Rocq confirme qu’il permet de conserver la plupart des optimisations existantes tout en autorisant aussi de nouvelles optimisations comme le réordonnancement read-read

Les règles d’aliasing nécessaires en Rust 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 propriété
  • Toutefois, dans les zones de code unsafe, la sûreté n’est pas automatiquement garantie, et des règles distinctes doivent être respectées par les programmeurs
  • Le compilateur cherche à renforcer les optimisations à l’intérieur des fonctions en exploitant les garanties du système de types, en particulier les informations liées à l’aliasing des pointeurs
  • Un code unsafe mal écrit peut invalider ces optimisations ; il est donc important de disposer d’un critère clair pour déterminer quel code doit être considéré comme « badly behaved »
  • Les travaux existants, Stacked Borrows, ont défini ce critère, mais présentent des limites
    • Ils rejettent plusieurs motifs courants dans le code Rust unsafe réel
    • Ils ne reflètent pas les fonctionnalités avancées récemment introduites dans le borrow checker de Rust

L’approche de Tree Borrows et les résultats d’évaluation

  • Tree Borrows est défini en remplaçant la pile, structure centrale de Stacked Borrows, par un arbre
  • Ce changement de structure assouplit les restrictions du modèle existant
    • Dans une évaluation portant sur les 30 000 crates Rust les plus utilisées, le nombre de cas de test rejetés baisse de 54 % par rapport à Stacked Borrows
  • Les propriétés liées aux optimisations ont également été vérifiées par une preuve Rocq
    • Il conserve la plupart des optimisations autorisées par Stacked Borrows
    • Il permet aussi une nouvelle optimisation importante : les read-read reorderings
  • Tree Borrows a reçu le PLDI'25 Distinguished Paper Award
  • Ressources associées

1 commentaires

 
GN⁺ 2025-07-10
Avis sur Hacker News
  • Un article récent de Ralf Jung apporte un contexte supplémentaire : https://www.ralfj.de/blog/2025/07/07/tree-borrows-paper.html
    En bonus, il y a aussi une présentation récente du groupe de Ralf Jung qui vise à spécifier précisément, sous forme exécutable, la sémantique d’exécution de Rust dans un dialecte de Rust : https://youtube.com/watch?v=yoeuW_dSe0o
  • Je me demande dans quelle mesure il est réellement exact de dire que « le compilateur veut exploiter les garanties du système de types liées à l’aliasing des pointeurs pour ouvrir la voie à de puissantes optimisations intra-fonction »
    Torvalds soutient depuis longtemps que les règles strictes d’aliasing du C font plus de mal que de bien, et ça paraît convaincant. Exemple ici : https://lore.kernel.org/all/CAHk-=wgq1DvgNVoodk7JKc6BuU1m9Un... ; si ce sujet vous intéresse, tout le fil vaut aussi la lecture
    D’après mon expérience limitée, Rust ne semble pas fondamentalement différent. Du moins, encore moins dès que unsafe entre en jeu
    • Je suis d’accord pour dire que les règles strictes d’aliasing du C sont mauvaises, mais les règles proposées pour Rust sont très différentes
      Je pense qu’elles sont plus utiles au compilateur et moins pénibles pour les programmeurs. Il existe aussi réellement une échappatoire dans le langage : utiliser des pointeurs bruts. Et il y a des outils pour vérifier le code
      Au final, comme pour tout en conception de langage, c’est un compromis, et je pense que Rust a peut-être trouvé un nouveau sweet spot pour ce type d’optimisation. Le temps dira si c’est le cas
    • Les règles d’aliasing de Rust sont assez différentes de celles du C
      En C, il existe l’arme nucléaire qu’est restrict, mais d’expérience, avec clang et gcc, cela n’a eu d’effet que lorsqu’il était appliqué aux paramètres de fonction. L’analyse d’aliasing fondée sur les types est généralement difficile à utiliser, et on ne peut pas créer une infinité de copies du type int64_t, ni d’ailleurs en avoir envie. Le fait d’imposer memcpy pour réinterpréter avec un autre type est aussi pénible
      À l’inverse, les références Rust sont délimitées finement par leur durée de vie, portée et mutabilité, et se soucient assez peu du type « physique » lui-même. Il est donc possible de réinterpréter la même mémoire en passant entre &mut i32/&i32 et &mut i64/&i64. Tant qu’une abstraction unsafe ne fournit pas simultanément des références &mut qui se chevauchent, ou qu’elle découpe un &mut en plusieurs &mut qui ne se chevauchent pas, on peut lire et écrire des demi-valeurs ou plusieurs valeurs avec de simples lectures/écritures Rust sûres
    • Il faut prendre avec un certain recul ce que Linus dit des compilateurs. Il écrit un noyau de système d’exploitation, pas des compilateurs, et ce sont des domaines assez différents
      L’analyse d’aliasing est aujourd’hui très importante pour obtenir de bonnes performances. Il faut toutefois garder à l’esprit que les plus gros gains viennent des heuristiques les plus simples. Par exemple, deux chargements utilisant la même valeur SSA comme pointeur aliasent forcément entre eux
      Du point de vue de LLVM, c’est le rôle de BasicAA. C’est un ensemble d’heuristiques simples qui se résument à peu près à : « si l’on peut suivre le point d’allocation de l’objet, on peut résoudre de manière certaine la requête d’aliasing ; sinon, on ne sait pas »
      La vraie question est la valeur de l’analyse d’aliasing au-delà des vérifications basiques et évidentes. Dès qu’une requête d’aliasing n’est plus triviale à résoudre, ce qu’on peut faire avec le résultat se réduit généralement beaucoup, et cela sert surtout à détecter des risques de déplacement de code. Le bénéfice est bien plus faible
      Une expérience que j’aimerais faire serait de mesurer l’accélération totale qu’apporterait, en théorie, une analyse d’aliasing parfaite. À vue de nez, même sur du code non HPC comme le noyau Linux, ce serait de l’ordre de 20 %
      [1] Cela n’inclut pas des optimisations héroïques comme des transformations de disposition des données qu’on ne tenterait pas sans une analyse d’aliasing de haute qualité. Comme on sait déjà qu’une telle analyse n’existe pas en pratique, on ne tenterait pas ces optimisations, et je ne pense pas qu’il vaille la peine de les inclure dans l’accélération attendue
    • L’aliasing strict du C et l’aliasing de Rust traitent tous deux des alias, mais ce ne sont pas les mêmes choses. Rust n’a assez explicitement pas adopté l’approche du C
      L’aliasing en C repose uniquement sur les types, d’où son autre nom : analyse d’aliasing fondée sur les types, ou TBAA
    • J’aimerais voir une analyse plus approfondie, mais une règle empirique simple consiste à retirer du compilateur toutes les parties qui transmettent les informations d’aliasing à LLVM, puis à observer les performances
      J’ai trouvé une affirmation selon laquelle noalias contribue à environ 5 % d’amélioration des performances en temps d’exécution, mais il est clair que la source est très ancienne
      https://github.com/rust-lang/rust/issues/54878#issuecomment-...
  • Les Stacked Borrows mentionnés avaient déjà fait l’objet de fils en 2020 et 2018
    https://news.ycombinator.com/item?id=22281205
    https://news.ycombinator.com/item?id=17715399
  • La présentation PLDI est également disponible : https://www.youtube.com/watch?v=CJi_Fcs4bak
  • J’ai testé moi-même l’affirmation de l’exemple 4 de l’article selon laquelle un certain code Rust serait rejeté, mais cela ne semble pas être le cas avec la version stable du compilateur
    D’après l’explication, si l’on crée un *mut i32 à partir d’un &mut puis que l’on fait *x = 10 au lieu de write(x), on n’utilise pas l’emprunt implicite en deux phases, donc le compilateur devrait le rejeter ; en pratique, cela passe
    • Stacked Borrows est le modèle d’exécution de Miri. Si on l’exécute dans Miri, la version *x = 10; signale une erreur, contrairement à la version write(x);
      L’erreur est de la forme « Undefined Behavior: attempting a write access using [...] but that tag does not exist in the borrow stack for this location »

rustc lui-même n’a aucune raison de rejeter l’un ou l’autre. y est un *mut et, du point de vue du système de types à la compilation, il n’a pas de relation d’emprunt ou de durée de vie avec x, qui est un &mut

  • L’article décrit le comportement dans le modèle Tree Borrows proposé, et non l’implémentation actuelle du vérificateur d’emprunts
    Le vérificateur d’emprunts actuel utilise une analyse plus restrictive et ne détecte pas ce conflit précis entre pointeur brut et référence mutable
  • Excellent travail. Je me souviens avoir lu la spécification Tree Borrows sur le site de Nevin il y a quelques années, et avoir été très impressionné par la manière élégante dont elle résolvait un problème assez délicat
    Dans mon expérience concrète [1] [2], elle autorisait aussi du code raisonnable qui était illégal avec Stacked Borrows
    [1] https://github.com/Voultapher/sort-research-rs/blob/main/wri... colonne Miri
    [2] https://github.com/rust-lang/rust/blob/6b3ae3f6e45a33c2d95fa...
  • Pour ceux que cela intéresse, l’implémentation Miri est ici : https://github.com/rust-lang/miri/tree/master/src/borrow_tra...
  • Je me demande si Rust, ou les futurs langages de programmation, évolueront vers la possibilité d’autoriser plusieurs implémentations du vérificateur d’emprunts avec des caractéristiques différentes — vitesse de compilation, vitesse d’exécution, flexibilité algorithmique — et de laisser les projets choisir
    • Rust prend déjà en charge le changement d’implémentation du vérificateur d’emprunts
      Il est passé d’un vérificateur d’emprunts fondé sur les portées au vérificateur d’emprunts à durées de vie non lexicales, et la prochaine implémentation expérimentale, Polonius, existe aussi en option. Cela dit, lorsqu’une nouvelle implémentation est prête pour la production, l’ancienne est abandonnée. Il n’y a aucune raison de choisir
      La vérification des emprunts est rapide, et la nouvelle implémentation accepte strictement davantage de programmes corrects
      Il existe aussi les types Rc et RefCell, qui permettent d’obtenir davantage de flexibilité en payant le coût de vérifications à l’exécution
    • Il existe déjà plusieurs approches. Les types affines utilisés par Rust, les types linéaires, les effets, les types dépendants, les preuves formelles, etc.
      Tous ont des coûts et des capacités différents en matière d’implémentation, de performances et d’expérience développeur
      Et ce que la plupart des langages hors Rust visent réellement, c’est la productivité de la gestion automatique des ressources. Quelle que soit l’approche, ils utilisent une gestion automatique des ressources et ne combinent l’un de ces systèmes de types que pour les chemins critiques en performance
    • Ce que l’on veut vraiment, en pratique, c’est probablement une logique de séparation sous-jacente. Une structure où l’on spécifie précisément les préconditions des fonctions, où l’on prouve les conditions intermédiaires des fonctions, puis où l’optimiseur reçoit ces « lemmes » et optimise librement jusqu’aux limites permises par les invariants explicitement énoncés
      Dans ce contexte, « Rust » peut être vu comme rien de plus que « les invariants que les gens veulent généralement » et « un ensemble d’optimisations qui supposent ces invariants usuels, ni plus ni moins »
    • Le vérificateur d’emprunts de Rust a un coût de compilation assez faible et n’a absolument aucun impact sur la génération de code
      La majeure partie du temps de compilation est consacrée à la résolution des traits, à la monomorphisation, aux passes d’optimisation LLVM et à l’édition de liens
    • Si je comprends bien, le vérificateur d’emprunts ne produit que des faux négatifs, et pas de faux positifs, non ?
      C’est peut-être une question stupide, mais je me demande pourquoi on ne pourrait pas lancer plusieurs implémentations dans des threads parallèles et laisser gagner celle qui donne d’abord un résultat positif
  • L’article dit que du code unsafe peut faire coexister plusieurs références mutables vers la même variable via des pointeurs, mais n’est-ce pas un comportement indéfini ?
    Utiliser des pointeurs pour faire exister simultanément plusieurs références mutables vers la même variable est un comportement indéfini. À moins que je n’aie mal compris l’intention de l’article, c’est ce qu’il me semble
    • Le cœur de ce travail est de fixer les frontières exactes du comportement indéfini
      Le code ci-dessus est accepté par le compilateur Rust, mais il enfreint les règles. La question est de savoir quelles règles il enfreint
      En substance, ce que le vérificateur d’emprunts accepte est légal, unsafe peut exprimer des choses illégales ou relevant d’un comportement indéfini, et il existe un ensemble de règles plus large que ce que le vérificateur d’emprunts peut vérifier, mais qui reste légal et à comportement défini
      L’objectif de cette recherche est de spécifier précisément cet ensemble de règles. Dans les grandes lignes, cela ressemble à « les pointeurs inscriptibles ne doivent pas avoir d’alias », mais les détails — pointeurs internes, invalidation d’itérateurs, savoir si le problème est de créer un mauvais pointeur ou de l’utiliser — sont très difficiles
      L’article précédent sur Stacked Borrows était plus simple, mais aussi plus restrictif, si bien que le code unsafe réel échouait souvent à respecter ses règles. Tree Borrows est plus large et autorise davantage de code, tout en restant prouvablement sûr
    • C’est vrai, mais la question est de savoir quelles règles exactement sont violées. Quelle est la définition précise qui nous dit qu’il s’agit d’un comportement indéfini ?
      Tree Borrows propose précisément ce genre de définition
      Ici, « le code peut faire cela » signifie « on peut écrire ce code, le compiler et l’exécuter, et sans quelque chose comme Tree Borrows, on n’a pas de fondement pour affirmer que ce code pose problème »
      On accepte déjà l’idée qu’il faut dire qu’un tel code relève d’un comportement indéfini, c’est-à-dire qu’il faut quelque chose comme Tree Borrows. Cette partie de l’article explique pourquoi une telle chose est nécessaire
    • Il me semble que vous avez mal compris le sens de « peut faire » ici. Dans du code unsafe, on peut effectivement faire cela. Et, comme vous le dites, c’est un comportement indéfini
      https://play.rust-lang.org/?version=stable&mode=debug&editio...
    • L’intention est la plus claire au début du paragraphe suivant
      Il y est dit que, comme les développeurs du compilateur Rust veulent clairement prendre en charge les optimisations fondées sur l’aliasing, il leur faut un moyen d’« exclure » de tels contre-exemples du champ considéré
    • C’est exactement le point essentiel, à mon avis. Il est trop facile de violer des contraintes comme celle qui interdit plusieurs références mutables

unsafe est destiné aux cas où il est difficile de prouver la validité du code avec l’analyse des durées de vie de Rust, mais il peut être détourné pour faire bien plus que cela

  • Je viens d’apprendre que l’un des auteurs, Neven Villani, est le fils de Cédric Villani, lauréat de la médaille Fields en 2010. L’expression « les chiens ne font pas des chats » convient parfaitement