Een nieuwe manier om na te denken over Borrow Checking (in omgekeerde volgorde)

Heb je ooit een vreemd idee gehad dat onverwacht werkte, maar dat je bijna niet kon geloven? Dat is precies hoe ik me nu voel over de borrow checker van Valen. Want deze reist namelijk achteruit door de tijd.

Om minder dramatisch te zijn: hij doorloopt functies in omgekeerde volgorde, wat nog steeds erg vreemd is. Jaren geleden, als je me had verteld dat het een goed idee zou zijn om een functie in omgekeerde volgorde te itereren, had ik je voor gek verklaard. Het blijkt echter dat er echt goede redenen voor zijn; het is vrij gebruikelijk bij bijvoorbeeld optimalisatie-passes [^0]. Maar ik geloof niet dat iemand dit tot nu toe heeft gedaan voor het controleren van geheugenveiligheid.

Als je een diepe duik wilt nemen in de wereld van borrow checking, lees dan verder! We gaan een paar vreemde dingen zien [^1].

(Let op: dit is een technische blik onder de motorkap van borrow checking-algoritmen.)

Een vreemd soort borrow checker

Dit is geen normale shared-xor-mutable borrow checker. Dit is de borrow checker van Valen, die shared-xor-mutable optioneel maakt en in staat is om Rust-functies aan te roepen met geheugenveiligheid over de grens heen.

Valen is nog zeer experimenteel. Veel zaken bevatten nog gaten en scherpe randjes, waarschijnlijk tot v0.1 ergens in februari verschijnt. De grote refactoring-ronde is al begonnen (vandaar deze nieuwe borrow checker!). Voel je vrij om de Valen-repo te bekijken, maar pas op: here be dragons! [^2]

Het lijkt een beetje op de borrow checker van Rust, maar het ondersteunt ook geheugenveilige mutable aliasing.

Een vreemde, omgekeerde implementatie

Valen compileert een functie in vier fasen [^3]:

1. Parsing: De functie wordt geparsed, waarbij de brontekst wordt omgezet in een AST (Abstract Syntax Tree).
2. Statische typering: Het bepalen van het type voor elke variabele, argument en expressie.
3. Statische groepering: Hierbij wordt vastgesteld naar welke variabele (of welk deel van een variabele) elke referentie wijst [^4].
4. Veiligheidscontrole: Er wordt gecontroleerd of een referentie niet wordt gebruikt nadat deze is ongeldig gemaakt.

Het vreemdste is dat fase 4 in omgekeerde volgorde gebeurt. De compiler kijkt naar de laatste statement in de functie en loopt vervolgens achteruit terug naar het begin van de functie.

Voor zover ik weet, is dit de enige borrow checker waarvan de veiligheidscontrole achteruit gaat [^5]. Hieronder leg ik uit waarom we dit doen (hint: gemak, lussen en snelheid), maar eerst kijken we hoe het precies werkt.

Fase 2: Statische typering

De pass voor statische typering is bekend bij velen: het wijst types toe aan variabelen. Bijvoorbeeld, het zet dit programma:

exported func main() {
    let fuel = 5;
    let force = fuel;
}

om in dit programma:

exported func main() {
    let fuel i64 = 5;
    let force i64 = fuel;
}

Dit is vrij normaal; veel compilers doen dit via een forward pass, van boven naar beneden door de functie. In fase 3 doen we iets soortgelijks, maar vreemders.

Fase 3: Statische groepering [^6]

Dit is eveneens een forward pass, die bepaalt waar elke referentie naar wijst. Neem bijvoorbeeld dit programma:

func print_first_fuel_cell(s &Ship) {
    let first_ref = &s.fuel_cells[0];
    print_int(first_ref);
}

Statische groepering stelt vast dat firstref wijst naar s.fuelcells[] [^7]:

func print_first_fuel_cell(s &Ship) {
    // Statische typering zegt:   first_ref &int
    // Statische groepering zegt: first_ref &int in s.fuel_cells[]
    let first_ref = &s.fuel_cells[0];
    print_int(first_ref);
}

In andere woorden: het wijst naar een int ergens in het s.fuel_cells[] array. Deze informatie wordt nu onderdeel van het type van de variabele. Deze informatie gebruiken we in de volgende fase om use-after-free fouten op te sporen.

Fase 4: Veiligheidscontrole

Dit is de fase die controleert op use-after-free. Dit gebeurt met een backwards scan. Laten we dit bekijken in een groter voorbeeld:

struct Entity { hp int; buffs []int; }
func add_buff(self &Entity mut) { ... }

func foo(e &Entity mut) {
    let buff = &e.buffs[0];
    e.add_buff();
    print_int(buff);
}

Dit programma veroorzaakt een use-after-free, en we willen dat de compiler hierover klaagt. Eerst desugaren we dit naar een explicietere syntaxis:

struct Entity { hp int; buffs []int; }
func add_buff<g'>(self &Entity in g) mut(g) { ... }
func foo<g'>(e &Entity in g) mut(g) {
    let buff = &e.buffs[0];
    e.add_buff();
    print_int(buff);
}

Nu voegen we commentaren toe, bepaald door de backwards scan:

struct Entity { hp int; buffs []int; }
func add_buff<g'>(self &Entity in g) mut(g) { ... }
func foo<g'>(
    e &Entity in g          // DECLARE e (groep g)
) mut(g) {
    let buff = &e.buffs[0]; // DECLARE buff (groep g.buffs[])
    e.add_buff();           // USE e (groep g)
                            // MUTATE groep g
    print_int(buff);        // USE buff (groep g.buffs[])
}

Het algoritme loopt in omgekeerde volgorde, van het einde van de functie naar het begin. Tijdens het scannen zoekt het naar deze gebeurtenissen:

• USE: Wanneer we een variabele gebruiken, voegen we deze toe aan de pending-lijst.
• MUTATE: Wanneer we iets muteren, controleren we of er geen variabelen in de pending-lijst staan die hierdoor ongeldig worden.
• DECLARE: Wanneer we een variabele declareren, verwijderen we deze uit de pending-lijst.

De pending-lijst bevat alle variabelen die lager in de functie worden gebruikt en daarom tot dat moment geldig moeten blijven. We willen nooit een MUTATE tegenkomen van iets dat op dat moment pending is.

Stapsgewijze analyse van het voorbeeld:

1. We beginnen bij de laatste regel: print_int(buff);. Dit is een USE, dus we voegen buff (groep g.buffs[]) toe aan de pending-lijst.
2. We gaan een regel omhoog: e.add_buff();. Hier zien we een MUTATE van groep g. We controleren of er iets in pending staat dat onder e valt.
3. buff (groep g.buffs[]) matcht! De compiler geeft een foutmelding.

Wat er is gebeurd: buff wees naar g.buffs[], wat begint met de g die we net muteerden met add_buff. Dit betekent dat buff ongeldig is geworden vóórdat deze werd gebruikt: een use-after-free.

Een correct voorbeeld

Laten we een correct programma bekijken om te zien hoe de backwards walk omgaat met een declaratie. We nemen hetzelfde programma, maar we verplaatsen e.add_buff(); naar de eerste regel.

struct Entity { hp int; buffs []int; }
func add_buff<g'>(self &Entity in g) mut(g) { ... }
func foo<g'>(
    e &Entity in g          // DECLARE e (groep g)
) mut(g) {
    e.add_buff();           // USE e (groep g)
                            // MUTATE groep g
    let buff = &e.buffs[0]; // DECLARE buff (groep g.buffs[])
    print_int(buff);        // USE buff (groep g.buffs[])
}

1. We starten aan het einde bij print_int(buff);. Dit is een USE, dus buff gaat in de pending-lijst.
2. Een regel omhoog: let buff = &e.buffs[0];. Dit is een DECLARE, dus we verwijderen buff uit de pending-lijst. De lijst is nu leeg.
3. Een regel omhoog: e.add_buff();. We zien een MUTATE. Omdat de pending-lijst leeg is, gebeurt er niets. Daarna zien we een USE van e, dus we voegen e (groep g) toe aan de pending-lijst.
4. We bereiken het einde van de functie zonder dat er een pending variabele is gemuteerd. Het programma is geheugenveilig.

Waarom achteruit?

Er zijn drie redenen: gemak, lussen en snelheid.

1. Gemak In het algemeen is achteruit lopen handig om te bepalen wanneer iets voor het laatst wordt gebruikt. Als we willen dat er iets gebeurt bij de declaratie (X) en iets anders wanneer een variabele niet meer nodig is (Y), biedt een backward scan een simpelere oplossing zonder dat we hoeven te navigeren naar de laatst geregistreerde locatie.

2. Lussen Achteruit lopen is beter voor lussen. Overweeg dit voorbeeld:

exported func main() {
    let arr = ArrayList<int>(3);
    let e = &arr[0];
    while ... {
        observe(e); // Geldige `e` use.
        add_element(&arr);
        set e = &arr[0];
    }
}

Hier kan e uit twee verschillende bronnen komen: de declaratie vóór de lus, of de set e aan het einde van de lus. Een forward scan zou vooruit moeten kijken naar de set e om te concluderen dat observe(e) geldig is. Met een backward scan is dit natuurlijker.

3. Snelheid Ik vermoed dat de V2-benadering sneller is, omdat elke node slechts één keer in de forward pass (fase 3) en één keer in de backward pass (fase 4) hoeft te worden verwerkt [^11].

Omgekeerd lopen met lussen [^13]

Om lussen correct af te handelen, heeft het algoritme wat extra's nodig. We reageren nu ook op LOOP START en gebruiken twee nieuwe lijsten: mutationsafterthis en revivedafterthis.

Het proces werkt als volgt:

• USE: Voeg toe aan pending.
• MUTATE: Controleer pending op invalidatie en voeg de mutatie toe aan de mutationsafterthis lijst van de huidige lus.
• DECLARE: Verwijder uit pending. Als het niet is geïnvalideerd door mutationsafterthis, voeg het dan toe aan de revivedafterthis lijst van de lus.
• LOOP START: Voor elk item in pending: als het is geïnvalideerd door iets in mutationsafterthis, controleer dan of het ook in revivedafterthis staat [^14].

Voorbeeld van een veilige lus:

exported func main() {
    let arr: ArrayList<int> = ...; // DECLARE arr (groep arr)
    let e = &arr[0];               // DECLARE e (groep arr[])
    while ... {                    // LOOP START
        observe(e);                // USE e (groep arr[])
        add_element(&arr);         // MUTATE arr (groep arr)
        set e = &arr[0];           // DECLARE e (groep g.arr[])
    }
}

1. We beginnen achteraan bij set e = &arr[0];. Dit is een DECLARE [^15]. We voegen e toe aan revivedafterthis.
2. Daarna addelement(&arr);. Dit is een MUTATE. We voegen arr toe aan mutationsafter_this.
3. Daarna observe(e);. Dit is een USE. e gaat in de pending-lijst.
4. We bereiken LOOP START. We controleren: e is in pending en wordt geïnvalideerd door arr in mutationsafterthis. Is e aanwezig in revivedafterthis? Ja. De check is geslaagd.

Richting de borrow checker van Rust?

Er is nog één grote wijziging die ik uiteindelijk wil doorvoeren. Rust kan feiten van overal in de functie gebruiken om de lifetime van een referentie te bepalen. Valen doet dit nog niet; fase 3 (statische groepering) gebruikt nog normale eenrichtingsinferentie.

Als we fase 3 veranderen in een volledige solver zoals rustc dat doet, kunnen we soortgelijke "superkrachten" krijgen, zonder dat we de backward pass van fase 4 hoeven aan te passen.

Slotwoord

De borrow checker van Valen is nog jong (slechts 3.600 regels) en verre van compleet. We moeten nog zaken toevoegen zoals onderbrekingen in de control flow (break, continue) [^16], geassocieerde groepen en closures [^17].

Bedankt voor het lezen!

***

Notities

[^0]: Of destructor-insertie, en nu, het controleren van geheugenveiligheid! [^1]: 0% van dit artikel is geschreven door AI. Mijn standpunt: als je wilt dat iemand de tijd neemt om iets te lezen, neem dan de tijd om het met de hand te schrijven. [^2]: Specifiek groene draken. [^3]: Er is ook een geheime vijfde fase waarin we berekenen welke attributen naar LLVM moeten worden gestuurd om te beschrijven welke operaties welke groepen kunnen wijzigen. [^4]: Het bepaalt ook alle groepen die ongeldig worden gemaakt door mut effects van instructies. [^5]: Bijvoorbeeld: Rust (NLL en Polonius) doet een constraint-solve voor region inference, gevolgd door een forward pass. rustc doet wel een backwards scan om te bepalen waar elke variabele wordt gebruikt, maar de eigenlijke veiligheidschecks gebeuren voorwaarts. Vale's typing-pass bepaalt regio's, en een latere forward pass doet de borrow checking. [^6]: Ik zal waarschijnlijk binnenkort overstappen van de term "groep" naar "pad". [^7]: In V1 bepaalde de statische groepering ook wanneer een referentie werd gemaakt (bijv. op regel 7.2). V2 heeft dit niet nodig vanwege de backwards scan. [^8]: De eerste persoon die dit algoritme breekt, krijgt een prijs! [^9]: Dit kan het decrementeren van een referentieteller zijn, het toevoegen van een destructor-call, of het controleren op use-after-frees. [^10]: In deze voorbeelden gebruik ik de naam ArrayList, maar in de echte Valen-compiler heten deze Array vanwege historische redenen. [^11]: Dit betekent niet dat het algoritme al O(n) is; de MUTATE moet nog steeds alles in de pending-lijst controleren. [^12]: V1 had nooit volledige ondersteuning voor lussen, dus is er niets om tegen te benchmarken. [^13]: Easter egg: Sergeant Stubby was de ster van het 102e Infanterieregiment in de Eerste Wereldoorlog. Hij diende 18 maanden, nam deel aan 17 gevechten en vier offensieven. Hij is de meest gedecoreerde oorlogshond van de Grote Oorlog. (Bron: Wikipedia). [^14]: We verwijderen hier niets uit pending, omdat die uses nog steeds verzadigd moeten worden door de code boven de lus. [^15]: Ik heb spijt dat ik het DECLARE noem, want eigenlijk is dit gewoon het opnieuw aanwijzen van een bestaande variabele. [^16]: Het huidige plan is om de borrow checker zo te refactoren dat deze naar een control-flow graph kijkt in plaats van een typed AST. [^17]: Ik ben erg enthousiast over closures; ik denk dat ik een elegante manier heb gevonden om ze te laten werken.