Geheugenveiligheid in Valen: Een nieuw soort Borrow Checking

Deze post gaat over de nieuwe, flexibele borrow checker van Valen.

Ik hou ervan om nieuwe benaderingen van geheugenveiligheid te verkennen en deze op ongebruikelijke manieren te combineren. Het is onderdeel van mijn eeuwige zoektocht naar de 'heilige graal' van geheugenveiligheid: iets dat net zo krachtig is als de borrow checking van Rust, maar net zo eenvoudig en flexibel als reference counting of garbage collection [^0][^1].

Ik heb vermoed dat we drie uitdagingen op het gebied van geheugenveiligheid moeten oplossen om deze heilige graal te vinden:

  1. Kunnen we een meer ontspannen borrow checker maken? [^2]
  2. Kunnen we een borrow checker maken die complexere data kan lezen? [^3][^4]
  3. Kunnen we deze twee systemen gelijktijdig laten werken?

Ik zal verderop uitleggen wat dit precies betekent en hoe Valen mogelijk een oplossing heeft gevonden. Deze post richt zich voornamelijk op het eerste deel: de meer ontspannen borrow checker van Valen. Ik zal bespreken wat het is, wat het kan en hoe het werkt.

In dit artikel neem ik enkele vrijheden met syntactic sugar voor de duidelijkheid: auto-deref, het direct indexeren van een struct (my_vec[0]) en het afleiden van types uit groepen (entity in world.entities[]) worden in november geïmplementeerd. Afgezien van deze syntactische aanpassingen werkt de borrow checker voor alles wat we bespreken [^6].

Daarnaast zal ik enkele specifieke details toelichten, zoals:

  • Hoe de borrow checker van Valen is vormgegeven om Valen-code Rust-code te laten aanroepen.
  • Hoe een compiler kan onthouden waar een referentie naar wijst.
  • Waarom Valen slechts één soort borrow-referentie heeft, in tegenstelling tot de twee die andere borrow checkers hebben.

Group Borrowing: een bijna-misser met enorm potentieel

(Deze sectie bevat achtergrondinformatie; u kunt deze overslaan als u direct naar de techniek wilt gaan.)

De aanpak van Valen is gebouwd op het "Group Borrowing"-voorstel, ontworpen door mijn vriend Nick Smith. De kern van dit concept is dat de compiler onthoudt waar een referentie naar wijst (dit leg ik later uit) en deze informatie gebruikt om te controleren of programma's geheugenveilig zijn.

Het ontwerp had een moeizame start. Het was oorspronkelijk ontworpen met Mojo in gedachten, maar ondanks mijn bestе inspanningen kon ik de leiding niet overtuigen om het te gebruiken [^7]. Group borrowing leek dood voordat het de kans had om te slagen.

Maar ik wist dat het enorm potentieel had. We hebben maanden besteed aan het aanscherpen van de uitleg en het uitwerken van de voordelen, en we schreven er vorig jaar een post over [^8] in de hoop dat andere talen het zouden overnemen.

En dat gebeurde! Het verspreidde zich wijd en breed [^9]:

  • De taal Carbon van Google is volledig overgestapt op group borrowing (en vermeldde zelfs ons artikel).
  • Ante is begonnen het in hun taal te integreren (zie Shared Mutability and Stability).
  • Plecra's exclusion typing herontwerpt de Rust borrow checker met concepten uit group borrowing en GhostCell [^10].
  • Zeta combineerde group borrowing met disjointness [^11] om runtime-feiten om te zetten in compile-time geheugenveiligheid.
  • Fang werkt het in hun ontwerpen (zie Cyclic References in Fang).

En nu combineert mijn taal, Valen, group borrowing met de aanpak van Vale [^12] en maakt het interoperabel met Rust-code.

De meeste van deze talen worstelen met dezelfde uitdaging: hoe maak je een flexibelere borrow checker? Valen wil bijvoorbeeld een borrow checker die flexibel genoeg is om te werken met reference counting en generationele referenties, terwijl Carbon een borrow checker wil die compatibel is met C++ code.

Dit is moeilijk, omdat er een fundamenteel conflict is tussen borrow checking en andere benaderingen [^13]:

  • Borrow checking hanteert de "shared-xor-mutable" restrictie: als je een referentie naar een object hebt, mag niemand anders dat object wijzigen.
  • Andere benaderingen willen toelaten dat je een referentie naar een object vasthoudt terwijl anderen het object wel mogen wijzigen [^14][^15].

Group borrowing lost dit conflict op door "shared-xor-mutable" te versoepelen naar "geen use-after-free". Dit klinkt cryptisch, maar wordt duidelijk wanneer ik uitleg hoe het werkt.

Wat Group Borrowing kan doen

Group borrowing biedt geheugenveiligheid zonder runtime-kosten [^16]. Het detecteert use-after-free problemen tijdens het compileren, en doet dit met minder restricties dan eerdere benaderingen.

Hier is een voorbeeld waarbij een use-after-free fout wordt opgevangen tijdens het compileren:

struct Entity {
    hp int;
}
struct World {
    entities Vec<Entity>;
}
func main() int {
    let world = World(Vec<Entity>.new());
    world.entities.push(Entity(42));
    let first_ref = &world.entities[0];
    world.entities = Vec<Entity>.new();
    // Compile error: Used a borrow after invalidated
    return first_ref.hp;
}

Het is een ongewoon flexibele aanpak. Normaal gesproken hebben compilers moeite met het onderstaande programma, maar deze aanpak begrijpt dat het veilig is [^17]:

func main() int {
    let list = Vec<int>.new();
    // Maak twee refs naar de lijst
    let ref_a = &list;
    let ref_b = &list;
    // Mutteer de lijst via beide refs
    ref_a.push(42);
    ref_b.push(73);
    return 42;
}

Group borrowing accepteert veel patronen die normaal gesproken moeilijk zijn voor borrow checkers, zoals:

  • Meerdere lokale variabelen hebben die naar hetzelfde object wijzen en via elk van hen kunnen schrijven (zoals hierboven).
  • Een parameter hebben die naar een object wijst, en een andere parameter die ergens binnen dat object wijst, en alleen via die laatste schrijven (zie volgende sectie).
  • Meerdere functieparameters hebben die naar hetzelfde object wijzen, en via elk van hen kunnen schrijven [^18].
  • Een "rollback"-struct maken die een object wijzigt wanneer deze buiten scope gaat, zoals het ScopeGuard-patroon [^19][^20].
  • Meerdere structs hebben die mutable referenties hebben naar een gemeenschappelijk subsysteem [^21].

En nog veel meer [^22]. Dit zijn patronen die we waarderen in C++, maar geen enkele taal had tot nu toe uitgezocht hoe dit allemaal op een geheugenveilige manier tijdens het compileren kon worden gedaan.

Een interessanter voorbeeld

Hier is een step-functie die een referentie naar een World ontvangt, en een referentie naar een van de entiteiten daarin. Het belangrijke deel is entity in world.entities[] mut, wat ik hieronder uitleg.

struct World {
    entities Vec<Entity>;
}
func step(world &World, entity in world.entities[] mut) {
    entity.advance();
    let collision = world.get_collision_for_entity(entity);
    entity.resolve(collision);
}

Let op deze onderdelen:

  • in betekent "een referentie naar een van de".
  • world.entities[] betekent "de elementen van de entities van world".
  • mut betekent hier "we kunnen het wijzigen" [^23][^24].

Samengevat: entity is een referentie naar een van de elementen in de entities van world, en we kunnen deze wijzigen. De kern van deze aanpak is dat de compiler weet waar een referentie naar wijst [^25], omdat de gebruiker via in specificeert waar deze naar wijst.

Vergelijking met andere talen

Om te zien waarom dit zo handig is, kijken we naar equivalenten in andere talen.

C++

struct World {
    vector<Entity> entities;
};
void step(const World& world, Entity& entity) {
    entity.advance();
    auto collision = world.getCollisionForEntity(entity);
    entity.resolve(collision);
}

C++ is simpel [^28], maar niet geheugenveilig; er is geen controle tijdens het compileren.

Rust (Vanilla)

struct World {
    entities: Vec<Entity>,
}
fn step(world: &mut World, entity_id: usize) {
    let entity_mut = &mut world.entities[entity_id]; // bounds check, mogelijke panic
    entity_mut.advance();
    let entity_read = &world.entities[entity_id]; // bounds check, mogelijke panic
    let collision = world.get_collision_for_entity(entity_read);
    let entity_mut = &mut world.entities[entity_id]; // bounds check, mogelijke panic
    entity_mut.resolve(collision);
}

Rust is geheugenveilig, maar in dit geval iets complexer en potentieel langzamer [^26], omdat we de referentie telkens opnieuw moeten ophalen wanneer we een &mut nodig hebben voor iets anders in dezelfde hiërarchie. Men zou de architectuur "vlakker" kunnen maken, maar dat heeft eigen trade-offs [^27].

Rust (met GhostCell)

struct World<'brand> {
    entities: Vec<GhostCell<'brand, Entity>>,
}
fn step<'brand>(
    world: &World<'brand>,
    entity: &GhostCell<'brand, Entity>,
    token: &mut GhostToken<'brand>,
) {
    entity.borrow_mut(token).advance();
    let collision = world.get_collision_for_entity(entity, token);
    entity.borrow_mut(token).resolve(collision);
}

GhostCell biedt de snelheid van C++, maar blijft complex.

Valen

struct World {
    entities Vec<Entity>;
}
func step(world &World, entity in world.entities[] mut) {
    entity.advance();
    let collision = world.get_collision_for_entity(entity);
    entity.resolve(collision);
}

Met de aanpak van Valen krijgen we iets dat snel, veilig en simpel is.

Hoe de borrow checker van Valen werkt

Kort samengevat bestaat de aanpak uit vijf mechanismen:

  1. Elk object wordt beschreven door een pad, volgens het principe van single ownership.
  2. Elke referentie onthoudt het pad van het object waarnaar hij wijst [^30].
  3. Wanneer we een object vernietigen, zijn alle referenties die naar dat pad wijzen niet meer bruikbaar.
  4. Een functiesignatuur beschrijft de paden die deze modificeert.
  5. Wanneer we een functie aanroepen, zijn alle referenties die wijzen naar data binnen de gemodificeerde paden niet meer bruikbaar.

Single Ownership

De borrow checker van Valen is gebaseerd op single ownership, net als C++ en Rust. Elke waarde wordt "bezet" door een overkoepelend object, array, stack frame of globale variabele [^31].

In single ownership heeft elk stuk data één eigenaar. Bijvoorbeeld:

  • Het stack frame van main bezit vector<Ship> ships.
  • De vector bezit elke Ship.
  • Elke Ship bezit zijn Engine.
  • Elke Engine bezit zijn int fuel.

Single ownership is de basis voor veel talen. Als je hier onbeperkte pointers aan toevoegt, krijg je C++. Voeg je exclusiviteitscontroles toe, dan krijg je Rust. Voeg je group borrowing en enkele andere mechanismen toe, dan krijg je Valen.

Paden (Paths)

Elk object kan worden beschreven door een pad. In een programma met een World struct, zijn de paden bijvoorbeeld:

  • x
  • world
  • world.diameter
  • world.entities
  • world.entities[]
  • world.entities[].hp

Een pad begint altijd bij een lokale variabele, een functiesparameter of een "group parameter". Daarna volgen lidnamen (.diameter), collectie-elementen ([]) of varianten van een union (.SomeType) [^34]. Omdat elk object slechts één eigenaar heeft, heeft elk object één pad [^36].

Referenties onthouden waar ze naar wijzen

De compiler weet naar welk pad elke referentie wijst. In het voorbeeld: let entityref = &world.entities[0]; Het type van entityref is &Entity in world.entities[]. Dit betekent dat het een referentie is naar een van de elementen in de entities van world.

Paden gebruiken voor geheugenveiligheid

De compiler gebruikt paden om use-after-free te detecteren. Dit gebeurt via twee regels:

  1. Wanneer we een object wijzigen, markeren we elke referentie die binnen dat object wijst als "geïnvalideerd".
  2. Wanneer we een "geïnvalideerde" referentie proberen te gebruiken, geeft de compiler een foutmelding.

Voorbeeld:

let first_ref = &world.entities[0];
world.entities = Vec<Entity>.new();
// De compiler invalideert alle referenties binnen world.entities[] -> first_ref is nu ongeldig.
return first_ref.hp; // Foutmelding!

Belangrijk is dat we referenties die naar een object wijzen niet invalideren, maar referenties die binnen het object wijzen.

let vec_ref = &vec;
let elem_ref = &vec[0];
vec.push(Ship(73)); // Modificeert vec. Invalideert elem_ref, maar NIET vec_ref.
vec_ref.push(Ship(81)); // Nog steeds geldig.
return elem_ref.fuel; // Foutmelding!

Functiesignaturen communiceren invalidaties

Hoe weet de compiler dat push de vector wijzigt? De functie push geeft dit aan in zijn signatuur met het mut-trefwoord: func push<T>(self &Vec<T> mut) { ... }

Dit is syntactic sugar voor: func push<T>(self &Vec<T>) mut(self) { ... }

Wanneer main de functie vec.push(...) aanroept, ziet de compiler mut(self), weet dat self in dit geval vec is, en markeert dus alles wat binnen vec wijst als ongeldig.

Als we een functie hebben die alleen een specifiek onderdeel wijzigt: func step(world &World, entity in world.entities[] mut) Dan worden alleen referenties naar die specifieke entiteit beïnvloed, niet de referenties naar de rest van de wereld. Dit kan de optimizer helpen om code efficiënter te rangschikken [^39].

Een twist op Group Borrowing

Valen voegt enkele extra functies toe aanHet oorspronkelijke Group Borrowing ontwerp:

Mutable-in-Immutable

Valen staat toe dat we een referentie ontvangen die onveranderlijk is, behalve voor specifieke elementen daarin. Dit voorkomt dat we telkens de hele wereld als mut moeten meenemen. Dit leidt tot sterkere API's en betere optimalisatie door de compiler [^40][^41][^42].

Tijdelijke Uniekheid (Temporary Uniqueness)

Om naadloos Rust-code aan te kunnen roepen, moet Valen omgaan met het verschil tussen group borrowing (meerdere mensen mogen wijzigen) en Rust (alleen één unieke referentie &mut mag wijzigen).

De oplossing: wanneer Valen Rust aanroept, kan een Valen-referentie worden doorgegeven als een Rust &mut als het de enige referentie is die op dat moment bij die data kan komen. Zo niet, dan kan het alleen als een gedeelde Rust & referentie worden doorgegeven.

Wildcard Descendant Paths

Wanneer een Rust-functie een referentie teruggeeft (bijv. -> &Gem), weet Valen niet precies naar welk pad dit wijst. Valen introduceert daarom het concept "wijst ergens binnen": func gem(self &Chest) -> &Gem in self.gem... Dit wordt een wildcard descendant path genoemd. Het maakt library API's flexibeler en toekomstbestendiger [^43].

Hoe dit alles samenhangt

De "heilige graal" van geheugenveiligheid vereist het oplossen van drie uitdagingen:

  1. Een meer ontspannen borrow checker maken.
  2. Een borrow checker maken die complexere data kan lezen.
  3. Deze systemen combineren.

De borrow checker van Valen is de sleutel tot punt 1. Voor punt 2 en 3 is een volgende post nodig, maar hier is een voorproefje.

Ik wil dat gebruikers de optie hebben om reference counted klassen te gebruiken wanneer ze geen paden willen specificeren:

class World { entities Vec<Entity>; }
func step(world World, entity Entity) mut { ... }

Het combineren van reference counting en borrowing is berucht moeilijk [^45]. De oplossing ligt in een gedachte-experiment uit 2023 genaamd Arrrlang [^46], waarbij de heap wordt gerepresenteerd als $N$ globale arrays (waar $N$ het aantal types is).

Als we reference-counted klassen aan een borrow checker presenteren alsof het een reeks arrays is, kunnen we op een veilige manier borrow-referenties daarin gebruiken. Hiervoor moeten we twee dingen toevoegen aan group borrowing:

  • Een "multi-typed group" (vergelijkbaar met een Vale region) [^47][^48].
  • Een "run-time group", waarbij referenties niet worden geïnvalideerd.

Bijlage: De Type-Stability Exception

(Nog niet volledig geïmplementeerd in Valen)

Group borrowing kan slim genoeg zijn om te weten dat een operatie zoals myvec.push(42) weliswaar mut(self) is, maar geen pointers naar myvec.size invalideert. Dit komt omdat de grootte van een vector altijd een integer blijft; het is "type-stabiel".

In het algemeen zal group borrowing nooit type-stabiele data invalideren. Dit betekent dat pointers naar primitieven, structs of arrays met vaste grootte behouden blijven, terwijl alleen pointers naar "type-onstabiele" zaken (zoals de inhoud van enums of pointers) worden geïnvalideerd.

***

Noten

[^0]: Deze zoektocht leidde tot experimenten met constraint references, linear types en reference counting. [^1]: 0% van dit artikel is geschreven door AI. [^2]: Specifiek: "Kunnen we een borrow checker maken die meerdere read-write borrow-referenties naar een enkel object ondersteunt?" [^3]: Met "complexere data" bedoel ik volledige grafen van data, waarbij objecten vrij referenties naar elkaar kunnen hebben (zoals in C++ of Java), in tegenstelling tot Rust. [^4]: Dit wordt beantwoord door de combinatie van generationele referenties en region borrowing in Vale. [^5]: Valen lost dit op door Vale, een experiment uit 2023 en de Group Borrowing aanpak van Nick Smith te combineren. [^6]: In de huidige compiler is handmatige dereferencing en expliciete typering nog nodig. [^7]: De realiteit van het werken aan de taal van iemand anders! [^8]: Zie Group Borrowing: Zero-Cost Memory Safety with Fewer Restrictions. [^9]: Er komt binnenkort een artikel over hoe deze verschillende taalbenaderingen zich tot elkaar verhouden. [^10]: Plecra gebruikt first class permissions om lifetimes te mergen met de type checker. [^11]: Zeta's borrow checker kan bewijzen wanneer twee referenties naar verschillende delen van dezelfde data wijzen ("disjoint"). [^12]: Valen verschilt van Vale door group borrowing (i.p.v. region), normale generationele referenties (i.p.v. probabilistische) en Rust interop. [^13]: Ik noem dit conflict "de language killer" omdat het veel experimentele talen heeft vernietigd. [^14]: C++ en reference counting willen vaak dat men een referentie vasthoudt terwijl anderen het object wijzigen. [^15]: Dit is controversieel; sommigen vinden dat een referent nooit mag veranderen, anderen vinden dat te restrictief. [^16]: Het is discutabel of enige taal nul runtime-kosten kan hebben. [^17]: Normaal gesproken verbieden borrow checkers meerdere read-write referenties; group borrowing staat dit toe omdat het specifieker beschermt tegen use-after-free. [^18]: Zie de "fn attack" voorbeelden; dit is vaak lastig voor borrow checkers. [^19]: Normale borrow checkers hebben hier moeite mee omdat er twee read-write referenties ontstaan (schending van shared-xor-mutable). [^20]: Dit kan de basis vormen voor een door de gebruiker gedefinieerd defer statement. [^21]: Bijvoorbeeld: meerdere File objecten die elk een referentie hebben naar een gemeenschappelijk FileSystem object. [^22]: Hiermee kunnen we snellere programma's maken (betere optimizer info) en reference counting gebruiken zonder Cell of Mutex. [^23]: Dit is niet zoals Rust's unique references (&mut). Er kunnen andere referenties naar dezelfde entiteit zijn. [^24]: Deze functie modificeert niet de hele wereld, alleen de entiteiten daarin. [^25]: Specifiek: hij weet ongeveer waar hij naar wijst (een groep objecten in de entities array). [^26]: In Rust moet men de referentie telkens weggooien en opnieuw ophalen om de containing &World te kunnen gebruiken. [^27]: Een vlakkere architectuur (zoals ECS) helpt met de borrow checker, maar men verliest sommige RAII-voordelen. [^28]: Ironisch om "C++" en "simpel" in één zin te gebruiken! [^29]: Men kan Rust-code vaak herstructureren om dezelfde snelheid als group borrowing te halen. [^30]: Group borrowing is in zekere zin een compile-time variant van generationele referenties. [^31]: Dit wordt later versoepeld met reference counting. [^32]: Men zou kunnen zeggen dat het stack frame van main het stack frame van foo bezit. [^33]: Oftewel: wie is er verantwoordelijk voor het vrijgeven van het geheugen? [^34]: Bijvoorbeeld: my_engine.WarpEngine als het een union is. [^35]: Zoals geassocieerde groepen of sub-types van een multi-typed groep. [^36]: Strikt genomen kunnen objecten via meerdere paden bereikt worden via geassocieerde groepen. [^37]: Een lifetime is meer een tijdsspanne van instructies, terwijl een pad een locatie is. [^38]: mut is hier onderdeel van de functiesignatuur, niet van het type van de parameter. [^39]: Als de optimizer weet dat functies alleen overlappen in reads en niet in writes, kan hij ze herordenen. [^40]: Vraag me hierover op Mastodon of Bluesky! [^41]: Dit vereist mogelijk patches voor LLVM om "read-only" beter te begrijpen dan alleen noalias. [^42]: Dit betekent niet per se dat Valen sneller is dan C++, maar dat de ergonomie en flexibiliteit beter zijn. [^43]: Men zou een private group kunnen re-exporteren onder een publieke naam. [^44]: Reference counting ontgrendelt patronen zoals observers en intrusive linked lists. [^45]: De reden waarom Rust Rc<RefCell<T>> nodig heeft. [^46]: Een voorbeeld van een "zero-cost" taal die in werkelijkheid kosten had door ID-chasing. [^47]: Dit zal ook nuttig zijn voor enums. [^48]: Dit is hoe heaps worden gerepresenteerd in Iris, gebruikt voor de formele verificatie van Rust.