Ante : une nouvelle approche combinant vérification des emprunts et comptage de références

 (verdagon.dev)
1 points par GN⁺ 4 시간 전 | 1 commentaires | Partager sur WhatsApp
  • Ante est une conception de langage système qui cherche à combiner la flexibilité du comptage de références et la sûreté de la vérification des emprunts, tout en évitant les paniques à l’exécution à la Rust ou le surcoût des vérifications d’accès exclusif à la Swift
  • Le mécanisme central repose sur la shape-stability et la temporary uniq conversion : il permet de créer en sûreté des emprunts mutables sur les champs de valeurs à comptage de références, et de traiter les valeurs internes des unions comme uniq seulement dans une portée limitée
  • En Rust, Rc<RefCell<T>> peut provoquer une panique à l’exécution en cas de mauvaise utilisation, et le système de borrowing de Swift inclut des vérifications d’accès exclusif à l’exécution ; Ante tente de traiter certains de ces cas par des règles à la compilation
  • Il s’agit encore d’une conception work-in-progress, partiellement implémentée ; comme elle doit analyser récursivement les types pour déterminer si un objet donné est atteignable, l’ajout d’un champ peut devenir un breaking API change
  • Cette approche affaiblit l’hypothèse selon laquelle le shared mutable borrowing serait toujours impossible et, avec des techniques comme Vale, group borrowing et Rust GhostCell, élargit le champ des exceptions dans la conception de la sûreté mémoire

La combinaison visée par Ante

  • Ante est un langage de programmation système qui vise à être un Rust plus simple, avec sûreté mémoire et sûreté des threads
  • Son modèle de base repose sur la propriété unique et la vérification des emprunts ; les valeurs sont placées inline sur la pile ou dans la structure ou le tableau qui les contient
  • Quand on veut privilégier la simplicité, on peut choisir le comptage de références en ajoutant le mot-clé shared au type
  • Avec shared type Color et shared type RbTree t, la fonction balance d’un arbre red-black est aussi courte que l’exemple Python, et plus petite que les exemples C++ et Rust
  • La question centrale est de savoir comment emprunter de façon mutable des données à comptage de références sans risque de panique de borrow_mut() comme en Rust, ni vérification d’accès exclusif à l’exécution comme en Swift
  • Ante est encore dans un état work-in-progress : une partie est implémentée, une autre est théorique, et la conception évolue encore

Shape-stability et références mutables multiples

  • La shape-stability d’Ante est l’idée selon laquelle « une référence vers une cible ayant une shape stable reste toujours valide, quels que soient les changements effectués ailleurs »
  • Grâce à ce concept, il est possible d’avoir simultanément plusieurs références d’emprunt mutable vers la même structure
  • Dans l’exemple heal (healer: mut Entity) (target: mut Entity), il est possible d’appeler self_heal en passant la même Entity aux deux arguments pour qu’elle se soigne elle-même
    • Même si healer et target pointent vers la même Entity, ce code ne peut pas détruire l’Entity, donc les deux références restent valides
  • Les références mutables vers la structure elle-même, ses champs et les champs de ses champs peuvent aussi être autorisées simultanément
    • Même en utilisant simultanément ship: mut Spaceship et engine_alias: mut Engine = ship.engine, Ante considère que ship et son engine ne seront pas détruits pendant l’exécution de la fonction
  • Rust et Swift n’autorisent pas une forme où plusieurs références &mut pointent simultanément vers les mêmes données

Emprunt mutable des champs d’une valeur à comptage de références

  • Dans Ante, ajouter shared devant une définition de type rend automatiquement ce type à comptage de références
  • Dans l’exemple shared mut type Spaceship, launch possède un Spaceship correspondant à un Rc et passe mut ship.engine à set_fuel
  • Comme launch conserve l’objet conteneur Spaceship, on peut considérer que son champ engine reste lui aussi vivant
  • La règle générale est qu’il est toujours possible de créer une référence d’emprunt mut vers les champs d’un type shared mut
    • En revanche, cela ne signifie pas que l’on puisse toujours créer un emprunt mutable vers tous les objets situés à l’intérieur de ce champ ; des règles séparées sont nécessaires
  • Les exemples suivants utilisent la notation plus explicite Rc Spaceship au lieu du sucre syntaxique shared mut type Spaceship
    • shared mut type Spaceship devient type Spaceship, et var ship: Spaceship devient var ship: Rc Spaceship

Là où les unions posent un problème de sûreté

  • Les unions peuvent être avantageuses pour la vitesse, car elles stockent leur contenu inline et réduisent les suivis de pointeurs ainsi que les défauts de cache
    • Si l’union Engine de C est incluse dans une struct Spaceship, StringTheoryEngine et ImpulseEngine se trouvent dans la mémoire de Spaceship
    • Cela contraste avec une approche à la Java utilisant interfaces et pointeurs
  • Le problème est qu’il est difficile de prendre en charge les unions de façon sûre dans un langage memory-safe
  • Dans l’exemple où Engine est soit StringTheoryEngine(str: String), soit ImpulseEngine(fuel: I32), un segfault peut se produire lorsque ship et other_ship pointent vers le même Spaceship
    • Après avoir capturé une référence interne à la chaîne avec match uniq ship.engine
    • Puis remplacé le même moteur par une autre variante via other_ship.engine := ImpulseEngine 0x42
    • Modifier ensuite l’ancien str revient à utiliser l’intérieur d’un conteneur après sa destruction
  • Ante doit donc empêcher la création d’une référence d’emprunt mutable vers l’une des variantes lorsqu’une référence d’emprunt mutable pointe vers une union
  • C’est l’inverse de la règle des structures
    • Avec une référence mut vers une structure, on peut créer une référence mut vers un champ
    • Avec une référence mut vers une union, on ne peut pas créer de référence mut vers l’intérieur d’une variante

uniq et temporary uniq conversion

  • uniq désigne une exclusive mutable reference, c’est-à-dire une référence mutable exclusive
  • Si une variable contient uniq Spaceship, il s’agit de la seule référence utilisable vers ce Spaceship
    • C’est un concept similaire à &mut Spaceship en Rust
  • Pour manipuler en sûreté l’intérieur des unions, Ante utilise la temporary uniq conversion
  • La règle centrale est que l’on peut obtenir temporairement une référence uniq dans une certaine portée si l’on n’utilise pas d’autres références susceptibles d’être des alias
    • Dans la section match uniq ship.engine, ship.engine est accessible comme un uniq
    • Pendant cette section, le compilateur empêche l’utilisation d’autres variables existantes pouvant contenir indirectement un Spaceship
  • Rust empêche l’existence même d’un uniq au motif que « d’autres références peuvent exister quelque part », tandis qu’Ante autorise uniq à condition de ne pas utiliser ces références dans la portée concernée
  • Ici, uniq Spaceship n’est pas réellement une référence globalement unique, mais la seule référence utilisable dans cette portée
    • La nuance est proche de celle des pointeurs restrict en C

Accès autorisés et accès rejetés

  • Accéder à other_ship: Rc Spaceship dans la portée de match uniq ship.engine doit provoquer une erreur de compilation
    • other_ship.engine peut être un alias de ship.engine
    • et modifier other_ship.engine pendant l’utilisation de ship.engine peut entraîner un drop
  • Une autre structure possédant un champ Rc Spaceship, comme HasAShip, est rejetée pour la même raison
    • other.ship.engine peut lui aussi atteindre indirectement le même Spaceship
  • À l’inverse, un entier comme new_fuel: I32 peut être utilisé
    • car I32 ne peut pas contenir de référence vers Spaceship
  • Si Spaceship contient lui-même un champ comme follow_ship: Rc Spaceship, c’est rejeté
    • Dans ce cas, uniq Spaceship redevient atteignable via un chemin interne, donc, en général, une conversion mut -> uniq n’est pas possible pour les types récursifs

Contraintes sur les appels de fonctions et les retours

  • La conversion mut -> uniq peut aussi se produire lors d’un appel de fonction
  • Lorsque foo (var ship: Rc Spaceship) (new_res: Resonator) appelle maybe_use_resonator ship new_res, ship est converti en uniq Spaceship au point d’appel
    • Le compilateur doit seulement vérifier si les autres arguments peuvent contenir une référence à Spaceship
    • Dans l’exemple, Resonator ne contient pas une telle référence, donc l’appel est autorisé
  • Au retour, une référence uniq convertie ne peut pas être renvoyée comme un uniq normal
    • Après le retour, le compilateur ne peut plus appliquer la vérification « ne pas utiliser de variables pouvant être des alias dans la portée »
  • À la place, on peut définir le type de retour comme local uniq Foo
    • En interne, lorsqu’une mut ref est convertie en uniq ref, c’est en réalité toujours un local uniq qui est créé
    • Dans la plupart des cas, il peut être utilisé comme un uniq normal, mais au retour, il faut l’indiquer explicitement

Coûts de conception et alternatives

  • Ante peut transformer une référence à comptage de références comme Rc Spaceship en uniq Spaceship temporaire sans erreur à l’exécution
  • L’inconvénient est que le compilateur doit examiner récursivement les types pour répondre à des questions comme « peut-on atteindre Spaceship depuis Engine ? »
  • Ce type d’analyse peut être fragile
    • Ajouter un champ à une structure peut devenir un breaking API change
  • Jake, le créateur d’Ante, cherche une meilleure façon de conserver cette garantie
    • Une approche consistant à associer à chaque type mutable partagé un type de marque anonyme unique, comme dans group borrowing et Flix references
    • Une approche consistant à ajouter un effet comme Mutates 'a lors de la modification d’un type partagé, afin de supprimer l’analyse des types
    • Une approche où l’utilisateur vérifie à l’exécution que deux références pointent vers des objets différents, ou où un contrôle unsafe est encapsulé dans une API safe
    • Une approche où le compilateur suit les valeurs qui ne sont pas stockées indirectement dans un Rc et ne peuvent donc pas être aliasées
  • Des idées proches de l’iso permission de Pony, ou des permissions temporaires permettant de regarder à l’intérieur d’une structure tout en empêchant l’utilisation de références vers l’extérieur, restent aussi possibles
  • La difficulté consiste à conserver cette flexibilité tout en préservant les objectifs d’Ante : utilisabilité, lisibilité et simplicité

Un mouvement plus large dans la sûreté mémoire

  • Le shared mutable borrowing était autrefois considéré comme impossible, et le point de vue sous-jacent est que Rust a aussi été conçu sur cette croyance
  • Plusieurs exceptions s’accumulent
    • Ante peut obtenir des références d’emprunt uniq à partir de données shared-mutable grâce à des règles de local uniqueness
    • Vale peut obtenir des références d’emprunt immuables à partir de données shared-mutable via des pure functions
    • group borrowing peut créer des références d’emprunt shared-mutable même sans shape-stability
    • Le GhostCell de Rust permet à un graphe d’objets de se référencer librement, mais à un instant donné il ne peut y avoir qu’une seule référence mutable vers l’un d’eux
  • Ce mouvement suggère qu’il pourrait exister des principes plus généraux pour traiter le shared mutable borrowing dans la conception de la sûreté mémoire

Comparaison avec Cell en Rust

  • Les utilisateurs de Rust peuvent se demander quelle est la différence entre l’approche d’Ante et le fait de placer un Cell dans un champ de structure
  • Dans l’exemple d’Ante, on peut obtenir une référence mut String vers status: String depuis Rc Spaceship et y ajouter directement " (refueling)"
  • Avec l’approche Cell<String> de Rust, on ne peut pas obtenir de &mut String depuis Rc<Spaceship>
    • À la place, il faut insérer temporairement une valeur par défaut avec status_ref.replace(String::new())
    • modifier le String extrait
    • puis le remettre à la fin avec replace(status)
  • Cette méthode présente plusieurs inconvénients
    • Il faut créer une instance par défaut, comme ""
    • Il existe un risque d’oublier l’appel final à replace
    • Quelqu’un peut lire status pendant que la valeur a été remplacée
  • Ante permet d’obtenir temporairement une référence vers la chaîne status, et le compilateur garantit que les autres codes ne peuvent pas y accéder pendant ce temps

À lire aussi

1 commentaires

 
GN⁺ 4 시간 전
Avis sur Lobste.rs

  • Le fait de considérer les « emprunts mutables partagés » comme impossibles n’était pas simplement un sacrifice consenti par Rust pour atteindre son objectif, mais quelque chose de proche de l’objectif central de Rust lui-même.
    En effet, l’état mutable partagé rend difficile le raisonnement local sur le code.
    « References are like jumps » par withoutboats traite bien ce point. L’idée est qu’empêcher la modification accidentelle d’un état avec alias est essentiel pour faciliter la création de systèmes qui fonctionnent correctement, et que les règles de durée de vie de Rust ne sont pas seulement un mécanisme destiné à éviter le ramasse-miettes, mais une structure plus profonde qui garantit la possibilité de raisonner dans un langage autorisant à la fois état mutable et état avec alias.

    • J’avais eu la même impression lorsque l’auteur avait abordé le borrow checker de Mojo. Le vérificateur d’emprunts de Rust maintient la sémantique par valeur même dans les programmes monothread.

  • Ça a l’air plutôt pas mal.
    Si j’ai bien compris, la magie qui permet de passer d’une référence partagée à une référence mutable est possible parce qu’elle se limite aux types qui ne sont pas partagés entre threads, et l’unicité de Rc semble garantie en traitant tous les objets du même type comme s’ils étaient empruntés avec la même durée de vie.
    Que l’on préfère une syntaxe explicite ou une syntaxe plus naturelle est peut-être affaire de goût, mais cela montre que si le compilateur en sait davantage sur Cell, il peut autoriser plus souplement les références mutables vers celle-ci.
    Et cela évite aussi la terminologie déroutante de Rust, où mut est utilisé comme s’il signifiait non pas mutable, mais exclusif/unique.

    • Je me demandais comment cela se passait entre threads. Je me posais des questions du genre : « la promotion en uniq implique-t-elle l’acquisition d’un verrou ? », mais je comprends que le point de comparaison est Rc et non Arc.
    • Peux-tu expliquer un peu plus en quoi mut signifie exclusif/unique ?

  • Je me demande si quelqu’un devine ce que pourrait être le principe unificateur suggéré à la fin.

  • Les discussions précédentes sur les billets du blog antelang.org méritent aussi d’être consultées.

  • Je ne comprends pas bien comment cela fonctionne. On dirait que cela signifie : « si l’on a un pointeur mutable vers un objet, on peut obtenir une référence mutable vers une tranche de cet objet ».
    Mais dans ce cas, par exemple, il semble possible d’écrire quelque chose comme mutref someobjext = …, mutref subfield = someobjext.a.b, someobjext.a = somethingelse, ce qui pourrait invalider subfield ou le casser en modifiant sa valeur.
    L’article contenait beaucoup d’explications, de comparaisons avec d’autres langages et d’exemples de code, mais j’ai eu du mal à trouver une présentation de base de la sémantique étape par étape de ce comportement.