Een alias-gebaseerde formulering van de borrow checker

De prestaties moeten echter nog aanzienlijk verbeteren (momenteel is het trager dan de bestaande analyse). Dat gezegd hebbende, ik ben nog niet eens begonnen met optimaliseren en ik weet dat ik enkele naïeve en inefficiënte dingen doe die zeker beter kunnen; ik ben dus nog optimistisch dat we daar grote stappen kunnen zetten.

Daarnaast werd me erop gewezen dat gisteren, 26 april, de zesde "verjaardag" van de borrow check was – het is leuk om terug te kijken naar mijn commit van die tijd, wat een goed beeld geeft van hoe Rust er toen uitzag.

Eindgebruikers hoeven zich geen zorgen te maken

Het eerste dat opgemerkt moet worden, is dat dit voorstel geen verschil maakt vanuit het perspectief van een eindgebruiker van Rust. Dat wil zeggen dat de borrow checker min of meer hetzelfde zou moeten werken als onder het NLL-voorstel.

Er zijn echter enkele subtiele verschuivingen in dit voorstel met betrekking tot hoe de compiler over je programma denkt, en dat zou potentieel toekomstige taalfuncties kunnen beïnvloeden.

Ons eerste voorbeeld

De analyse werkt op MIR, maar ik zal het uitleggen aan de hand van eenvoudige Rust-voorbeelden. Hier is het eerste voorbeeld, dat ik voorbeeld A zal noemen. Het voorbeeld zou niet moeten compileren:

fn main() {
    let mut x: i32 = 22;
    let mut v: Vec<&i32> = vec![];
    let r: &mut Vec<&i32> = &mut v;
    let p: &i32 = &x; // 1. `x` wordt hier geleend om `p` te maken
    r.push(p);        // 2. `p` wordt in `v` opgeslagen, maar via `r`
    x += 1;           // <-- Fout! kan `x` niet muteren terwijl deze is geleend
    take(v);          // 3. de referentie naar `x` wordt later hier gebruikt
}

fn take<T>(p: T) { .. }

Regio's zijn verzamelingen van leningen (loans)

De grootste verschuiving in deze nieuwe benadering is dat wanneer je een type hebt zoals &'a i32, de betekenis van 'a verandert.

In het systeem beschreven in de NLL RFC correspondeerde 'a – een lifetime genoemd – uiteindelijk met een bepaald deel van het bronprogramma of de control-flow grafiek. Onder dit voorstel correspondeert 'a – wat ik een regio zal noemen – in plaats daarvan met een verzameling leningen (loans) – dat wil zeggen, een verzameling borrow-expressies, zoals &x of &mut v in Voorbeeld A. Het idee is dat als een referentie r het type &'a i32 heeft, het ongeldig maken van de termen van een van de leningen in 'a ook r ongeldig maakt.

Het ongeldig maken van de termen van een lening betekent het uitvoeren van een illegale toegang tot het pad dat door de lening is geleend. Als je bijvoorbeeld een muteerbare lening hebt zoals r = &mut v, dan kun je de waarde v alleen benaderen via de referentie r. Het direct benaderen van v op enige wijze – lezen, schrijven of verplaatsen – zou de lening ongeldig maken. Voor een gedeelde lening zoals p = &x is lezen via x (of p) toegestaan, maar het schrijven naar of muteren van x zou de termen van de lening ongeldig maken (en schrijven via p is ook niet mogelijk).

De subtyping-regels voor referenties werken nu iets anders, aangezien een regio een verzameling leningen is en geen programmapunten. Waar je bij punten een referentie kunt benaderen door de lifetime te verkorten, kun je bij verzamelingen van leningen benaderen door de verzameling te vergroten. In andere woorden:

'a ⊆ 'b $\implies$ &'a u32 <: &'b u32

In Rust-syntaxis correspondeert 'a ⊆ 'b met de notatie 'a: 'b, en dat is wat ik voor de rest van het bericht zal gebruiken. We hebben dit traditioneel een outlives-relatie genoemd, maar ik ga het in plaats daarvan een subset-relatie noemen, passend bij de nieuwe betekenis van regio's.

Om een beter intuïtief begrip te krijgen van regio's als verzamelingen van leningen, beschouw dan dit programma:

let x = vec![1, 2];
let p: &'a i32 = if random() {
    &x[0] // Lening L0
} else {
    &x[1] // Lening L1
};

Hier zou de regio 'a corresponderen met de verzameling {L0, L1}, aangezien het kan verwijzen naar data geproduceerd door lening L0, maar ook naar data van lening L1.

Datalog

In dit bericht zal ik de analyse definiëren met behulp van Datalog-regels. Datalog is in zekere zin een subset van Prolog, ontworpen voor efficiënte uitvoering. Het komt in feite overeen met regels zoals deze (met de syntaxis van het Souffle-project):

.decl cfg_edge(P:point, Q:point)
.input cfg_edge

.decl reachable(P:point, Q:point)
reachable(P, Q) :- cfg_edge(P, Q).
reachable(P, R) :- reachable(P, Q), cfg_edge(Q, R).

Zoals je hier ziet, definiëren Datalog-programma's relaties tussen dingen; deze relaties worden gedeclareerd met .decl. Sommige relaties zijn inputs, gedeclareerd met .input, wat betekent dat hun waarden vooraf door de gebruiker worden gegeven (deze worden ook feiten genoemd). In dit programma is dat cfg_edge. Andere relaties, zoals reachable, worden gedefinieerd via regels die nieuwe zaken synthetiseren uit die feiten. Net als in Prolog zijn hoofdletter-identificatoren variabelen, en wanneer een variabele twee keer voorkomt, moet deze dezelfde waarde hebben.

Merk op dat Datalog, omdat het een subset is, veel van de meer "programmeertaal-achtige" eigenschappen van Prolog vermijdt. Bijvoorbeeld, Datalog-programma's stoppen altijd wanneer ze worden uitgevoerd op een eindige verzameling feiten (zelfs wanneer ze recursief zijn, zoals hierboven). Ook is het prima om negatieve redeneringen in een Datalog-programma te gebruiken, omdat het negatieve cycli verbiedt.

Om deze regels te implementeren, heb ik de differential-dataflow crate van Frank McSherry gebruikt. Dit is een geweldige ervaring geweest: zodra je het onder de knie hebt, kun je Datalog-regels op een zeer directe manier vertalen, wat betekent dat ik snel nieuwe ontwerpen kon prototypen in slechts een uur of twee. Bovendien is de resulterende uitvoering vrij snel.

Regio-variabelen

Nu we regio's hebben beschreven als verzamelingen van leningen, wil ik dat je dat voor nu vergeet. De analyse zoals ik die heb gedefinieerd, manipuleert die verzamelingen niet direct, althans niet in eerste instantie. In plaats daarvan gebruikt het "regio-variabelen" om alle regio's in het programma te representeren. Ik zal deze aanduiden als "genummerde" regio's zoals '0, '1, etc.

Als we ons programma herschrijven om deze abstracte regio's te gebruiken (basaal: een genummerde regio overal waar MIR er een zou hebben), ziet het er als volgt uit:

fn main() {
    let mut x: i32 = 22;
    let mut v: Vec<&'0 i32> = vec![];
    let r: &'1 mut Vec<&'2 i32> = &'3 mut v;
    let p: &'5 i32 = &'4 x;
    r.push(p);
    x += 1;
    take::<Vec<&'6 i32>>(v);
}

fn take<T>(p: T) { .. }

Deze abstracte regio's verschijnen via onze Datalog-regels; ik zal ze aanduiden met R voor "region".

Relaties tussen regio's

De abstracte regio's die we zojuist zagen, hebben nog geen betekenis. Wat vervolgens gebeurt, is dat we door het programma lopen en de regels van het typesysteem op de standaardmanier toepassen. Dit resulteert in "subset"-relaties tussen regio's. Overweeg bijvoorbeeld de volgende regel uit Voorbeeld A:

let p: &'5 i32 = &'4 x;

Hier produceert de expressie &'4 x een waarde van type &'4 i32. Dit type moet een subtype zijn van het type van p, &'5 i32, dus we krijgen:

&'4 i32 <: &'5 i32 $\implies$ '4: '5

Als we naar het programma kijken, zien we een aantal subtype-relaties ontstaan:

fn main() {
    let mut x: i32 = 22;
    let mut v: Vec<&'0 i32> = vec![];
    let r: &'1 mut Vec<&'2 i32> = &'3 mut v;
    // vereist: &'3 mut Vec<&'0 i32> <: &'1 mut Vec<&'2 i32>
    //        => '3: '1, '0: '2, '2: '0

    let p: &'5 i32 = &'4 x;
    // vereist: &'4 i32 <: &'5 i32
    //        => '4: '5

    r.push(p);
    // vereist: &'5 i32 <: &'2 i32
    //        => '5: '2

    x += 1;
    take::<Vec<&'6 i32>>(v);
    // vereist: Vec<&'0 i32> <: Vec<&'6 i32>
    //        => '0: '6
}

Uiteindelijk worden deze subset-relaties input-feiten in het systeem. Om redenen die later duidelijk worden, noem ik dit de "base subset" relaties:

.decl base_subset(R1:region, R2:region, P:point)
.input base_subset

Met andere woorden: base_subset(R1, R2, P) betekent dat R1: R2 waar moest zijn op punt P.

Deze base_subset input is slechts het startpunt; het vertelt je welke relaties direct vereist waren bij aanvang, maar niet de volledige set relaties op elk punt. Dit komt omdat subset-relaties "accumuleren" terwijl je itereert. We gaan een completere subset-relatie definiëren, maar daarvoor moeten we eerst kijken naar hoe we de control-flow grafiek definiëren.

Punten in de control-flow grafiek (CFG)

De control-flow grafiek die door deze analyse wordt gebruikt, is gedefinieerd op basis van MIR. We definiëren de punten in de flow-grafiek als volgt:

Point = Start(Statement) | Mid(Statement) Statement = BBi '/' j

Hier identificeert Statement een specifieke instructie (de $j$-de statement uit het $i$-de basic block). We maken vervolgens onderscheid tussen het startpunt van een statement en het middelpunt. Het startpunt is in feite "voordat er iets is gedaan", en het "middelpunt" is de plaats waar het statement wordt uitgevoerd. Als zodanig zijn alle base-subset relaties uit de vorige sectie gedefinieerd als plaatsvindend op het middelpunt van hun overeenkomstige statements.

We definiëren de flow in de grafiek met een cfg_edge input:

.decl cfg_edge(P:point, Q:point)
.input cfg_edge

Natuurlijk heeft elk startpunt een edge naar zijn corresponderende middelpunt. Middelpunten hebben een edge naar het begin van het volgende statement of, in het geval van een terminator, naar het begin van de basic blocks die volgen. (Voor het grootste deel kun je middelpunten voor nu negeren, maar ze worden later zeer belangrijk bij de integratie van liveness-concepten.)

Subset-relaties volgen over de grafiek

Nu komen we bij het interessantste deel van de analyse: het berekenen van de subset-relaties. Om de intuïtie op te bouwen, begin ik met een eenvoudigere vorm dan de uiteindelijke analyse.

Het kernidee is dat de analyse niet direct de waarden van elke regiovariabele berekent. In plaats daarvan berekent het de subset-relaties die tussen hen moeten gelden op elk punt in de control-flow grafiek. Deze relaties worden geïntroduceerd door de "base subset" relaties die voortkomen uit de type-check, maar ze worden vervolgens over de control-flow edges gepropageerd volgens de volgende regel:

Zodra een base subset-relatie wordt geïntroduceerd tussen twee regio's 'a: 'b, moet deze waar blijven.

We kunnen dit in Datalog als volgt definiëren. We beginnen met een relatie subset:

.decl subset(R1:region, R2:region, P:point)

// Regel subset1
subset(R1, R2, P) :- base_subset(R1, R2, P).

// Regel subset2 (Transitiviteit)
subset(R1, R3, P) :- subset(R1, R2, P), subset(R2, R3, P).

// Regel subset3 (versie 1: Propagatie)
subset(R1, R2, Q) :- subset(R1, R2, P), cfg_edge(P, Q).

Als we deze regels toepassen op ons Voorbeeld A, eindigen we met de volgende subset-relaties tussen elk statement (ik toon hier alleen de relaties op elk "start"-punt en niet de volledige transitieve afsluiting):

fn main() {
    let mut x: i32 = 22;
    // (geen)
    let mut v: Vec<&'0 i32> = vec![];
    // (geen)
    let r: &'1 mut Vec<&'2 i32> = &'3 mut v;
    // '3: '1, '0: '2, '2: '0
    let p: &'5 i32 = &'4 x;
    // '3: '1, '0: '2, '2: '0, '4: '5
    r.push(p);
    // '3: '1, '0: '2, '2: '0, '4: '5, '5: '2
    x += 1;
    // '3: '1, '0: '2, '2: '0, '4: '5, '5: '2
    take::<Vec<&'6 i32>>(v);
    // '3: '1, '0: '2, '2: '0, '4: '5, '5: '2, '0: '6
}

Kijk naar de uiteindelijke set relaties. We kunnen bijvoorbeeld een relatie zien tussen regio '4 (de regio van de borrow van x) en regio '0 (de regio voor de data in vector v):

'4: '5: '2: '0

Dit weerspiegelt in feite de datastroom in je programma. Als je elke regio ziet als een "set van leningen", dan zegt dit dat '0 (de vector) referenties kan bevatten die zijn afgeleid van dat &x statement. Dit leidt naar het volgende deel van de analyse.

Borrow-regio's

Tot nu toe hebben we de subset-relatie geïntroduceerd. Nu gaan we hetzelfde doen voor het volgen van welke regio's afhankelijk zijn van welke leningen.

Eerst introduceren we een nieuwe input, genaamd borrow_region:

.decl borrow_region(R:region, L:loan, P:point)
.input borrow_region

Deze input is gedefinieerd voor elke borrow-expressie (bijv. &x of &mut v) in het programma. Het relateert de regio van de borrow aan de abstracte lening die wordt gemaakt. Hier is Voorbeeld A, geannoteerd met de borrow-regio's:

fn main() {
    let mut x: i32 = 22;
    let mut v: Vec<&'0 i32> = vec![];
    let r: &'1 mut Vec<&'2 i32> = &'3 mut v; // borrow_region('3, L0)
    let p: &'5 i32 = &'4 x;                // borrow_region('4, L1)
    r.push(p);
    x += 1;
    take::<Vec<&'6 i32>>(v);
}

Net als de basesubset relaties worden borrowregion created op het middelpunt van het corresponderende borrow-statement.

Actieve (live) regio's en leningen

In normale compiler-terminologie is een variabele X live op een bepaald punt P in de control-flow grafiek als de huidige waarde later gebruikt kan worden.

We kunnen een analoge definitie maken voor regio's: een regio 'a is live op een punt P als een referentie met type &'a i32 later gedereferenceerd kan worden. Voor het grootste deel betekent dit simpelweg dat er een live variabele X is en dat 'a voorkomt in het type van X. Er zijn echter subtiliteiten rondom drops, omdat we proberen te begrijpen welke regio's een destructor zou gebruiken en welke niet (bijv. een waarde van type Vec<&'a u32> zal geen toegang hebben tot 'a wanneer deze wordt gedropt).

In Datalog kunnen we een input regionliveat definiëren:

.decl region_live_at(R:region, P:point)
.input region_live_at

De "requires"-relatie

Nu kunnen we de borrow_region relatie uitbreiden over de control-flow grafiek. We introduceren een nieuwe relatie, genaamd requires:

.decl requires(R:region, L:loan, P:point)

Dit kan worden gelezen als: Regio R vereist dat de termen van lening L worden gehandhaafd op punt P. Of anders gezegd: Als de termen van lening L worden geschonden op punt P, dan wordt regio R ongeldig.

De eerste regel stelt dat de regio voor een borrow altijd afhankelijk is van zijn corresponderende lening: // Regel requires1 requires(R, L, P) :- borrow_region(R, L, P).

De volgende regel stelt dat als R1: R2, dan R2 afhangt van alle leningen waar R1 van afhangt: // Regel requires2 requires(R2, L, P) :- requires(R1, L, P), subset(R1, R2, P).

Ten slotte propageren we deze vereisten over control-flow edges, maar met een twist: // Regel requires3 (versie 1) requires(R, L, Q) :- requires(R, L, P), !killed(L, P), cfg_edge(P, Q).

Deze regel zegt dat als regio R lening L vereist op P, het L ook vereist op de opvolger Q – zolang L niet is "gedood" (killed) op P. De killed input-relatie wordt als volgt gedefinieerd:

.decl killed(L:loan, P:point)
.input killed

killed(L, P) is gedefinieerd wanneer punt P een toewijzing is die een van de referenties overschrijft wiens referent werd geleend in lening L. Stel je dit voor:

let p = 22;
let q = 44;
let x: &mut i32 = &mut p; // `x` wijst naar `p`
let y = &mut *x;           // Lening L0, `y` wijst ook naar `p`
// ...
x = &mut q;               // `x` wijst nu naar `q`; doodt L0

Hier wees x aanvankelijk naar p, en dat is gekopieerd naar y. Op dit punt is het benaderen van x illegaal omdat y het heeft geleend. Maar dan wordt x opnieuw toegewezen om naar q te wijzen – nu aliast x niet meer met y. Dit wordt weerspiegeld door lening L0 te doden, wat aangeeft dat y niet langer ongeldig zou worden gemaakt door toegang tot x.

We kunnen Voorbeeld A nu annoteren met zowel de subset- als de requires-relaties:

fn main() {
    let mut x: i32 = 22;
    // (geen)
    let mut v: Vec<&'0 i32> = vec![];
    // (geen)
    // Lening L0
    let r: &'1 mut Vec<&'2 i32> = &'3 mut v;
    // '3: '1, '0: '2, '2: '0
    // requires('3, L0)

    // Lening L1
    let p: &'5 i32 = &'4 x;
    // '3: '1, '0: '2, '2: '0, '4: '5
    // requires('3, L0)
    // requires('4, L1)

    r.push(p);
    // '3: '1, '0: '2, '2: '0, '4: '5, '5: '2
    // requires('3, L0)
    // requires('4, L1)

    x += 1;
    // '3: '1, '0: '2, '2: '0, '4: '5, '5: '2
    // requires('3, L0)
    // requires('4, L1)

    take::<Vec<&'6 i32>>(v);
    // '3: '1, '0: '2, '2: '0, '4: '5, '5: '2, '0: '6
    // requires('3, L0)
    // requires('4, L1)
}

Beschouw specifiek de feiten bij aanvang van het x += 1 statement. Lening L1 is een gedeelde borrow van x, en '4 vereist L1. Bovendien bevat variabele v referenties van type &'0 i32, en we zien dat '4 een subset is van '0:

'4: '5: '2: '0

Dit impliceert dat de referenties in vector v ongeldig zouden worden gemaakt door x te muteren, omdat dat de termen van L1 ongeldig maakt. Aangezien v op de volgende regel wordt gebruikt, is dat een probleem.

Een "fout" definiëren

Nu kunnen we definiëren wat een borrow check fout is. We definiëren een input invalidates(P, L), die aangeeft dat een actie op punt P de termen van lening L ongeldig maakt:

.decl invalidates(P:point, L:loan)
.input invalidates

Vervolgens breiden we het begrip liveness uit van regio's naar leningen. Een lening L is live op punt P als een live regio R deze vereist:

.decl loan_live_at(L:loan, P:point)
// Regel loan_live_at1
loan_live_at(L, P) :- region_live_at(R, P), requires(R, L, P).

Ten slotte is het een fout als een punt P een lening L ongeldig maakt terwijl lening L live is:

.decl error(P:point)
// Regel error1
error(P) :- invalidates(P, L), loan_live_at(L, P).

Verfijning van constraint propagation met liveness

Dit is bijna de analyse die ik heb geïmplementeerd, behalve één punt. We kunnen de propagatie van constraints verfijnen door rekening te houden met liveness, wat ons in staat stelt veel meer programma's te accepteren. Overweeg dit voorbeeld:

let x = 22;
let y = 44;
let mut p: &'0 i32 = &'1 x; // Lening L0
// '1: '0, requires('1, L0)
p = &'3 y;                  // Lening L1
// '3: '0, requires('3, L1)
x += 1;                     // invalidates(L0)
print(*p);

Het zou mooi zijn als we dit programma accepteren: hoewel p aanvankelijk naar x verwijst, wordt het later opnieuw toegewezen om naar y te verwijzen. Tegen de tijd dat we x += 1 uitvoeren, zou de lening dus vrijgegeven kunnen zijn. Onder de huidige regels zouden we dit echter afwijzen omdat we informatie constant accumuleren.

Dit probleem ontstaat omdat we een bestaande variabele p hergebruiken in plaats van een nieuwe te declareren, waardoor dezelfde regio '0 wordt gebruikt. We kunnen dit oplossen door de regels voor propagatie van subset- en requires-relaties aan te passen. In plaats van onvoorwaardelijk te propageren, propageren we nu alleen relaties voor regio's die live zijn op het volgende punt:

// Regel subset3 (versie 2)
subset(R1, R2, Q) :-
    subset(R1, R2, P), cfg_edge(P, Q),
    region_live_at(R1, Q), region_live_at(R2, Q).

// Regel requires3 (versie 2)
requires(R, L, Q) :-
    requires(R, L, P), !killed(L, P), cfg_edge(P, Q),
    region_live_at(R, Q).

Met deze regels wordt ons oorspronkelijke programma geaccepteerd. Het cruciale punt is dat bij aanvang van de regel p = &y, variabele p dood is (zijn waarde wordt overschreven) en dus ook zijn regio '0. De constraints die dit beïnvloeden, propageren daarom niet verder.

Deze verbetering is ook cruciaal voor het accepteren van het voorbeeld uit #47680:

struct Thing;
impl Thing {
    fn maybe_next(&mut self) -> Option<&mut Self> { .. }
}

fn main() {
    let mut temp = &mut Thing;
    loop {
        match temp.maybe_next() {
            Some(v) => { temp = v; }
            None => { }
        }
    }
}

Het probleem hier is dat temp.maybe_next() *temp leent. Deze lening wordt soms via variabele v teruggegeven en vervolgens weer in temp opgeslagen. Onder de nieuwe regels zien we dat – langs het Some-pad – de lening wordt gedood omdat temp opnieuw wordt toegewezen. Ondertussen – langs het None-pad – wordt de requires-relatie gedropt omdat deze op dat punt alleen geassocieerd is met dode regio's. Hierdoor wordt het programma geaccepteerd.

Top-down versus bottom-up en causale berekening

In een echte compiler is weten of er fouten zijn niet genoeg; we moeten de fout ook netjes kunnen rapporteren. De NLL RFC stelde een techniek voor die ik de three-point form noemde: we proberen alle fouten uit te leggen aan de hand van drie punten:

1. Het punt waar de borrow plaatsvond (B).
2. Het punt waar de resulterende referentie wordt gebruikt (U).
3. Een tussenliggend punt dat de referentie ongeldig kan hebben gemaakt (A).

Een interessant bijproduct van het formuleren van de analyse als een reeks Datalog-regels is dat we deze drie punten kunnen extraheren door te kijken naar de manier waarop elke fout is afgeleid. Als we Prolog zouden gebruiken (dat "top-down" executeert), zouden we een bewijsboom tegenkomen die precies laat zien waarom een fout optreedt: error(P) $\implies$ invalidates(P, L1) en loanliveat(L1, P), enzovoort.

Traditioneel executeert Datalog echter "bottom-up" (het berekent alle basisfeiten, dan de afgeleide feiten, etc.). Hoewel dit efficiënter kan zijn, kan het verspillend zijn als niet alle feiten uiteindelijk nodig zijn. Er bestaan technieken om top-down en bottom-up propagatie te combineren (bijv. magic sets) of om "uitleggingen" uit Datalog te halen.

Ik heb hier nog niet veel aan gedaan – ik probeer eerst zeker te weten dat dit de analyse is die we willen – maar het lijkt duidelijk dat we op deze manier goede foutinformatie kunnen verkrijgen.

***

Voetnoten

1. We gebruikten toen nog de keywords alt en ret, en nog geen => voor match arms.
2. Macros waren destijds #foo[..] in plaats van foo!(..).
3. "Region" is de standaardterm uit de academische wereld, maar het roept hier niet noodzakelijkerwijs de juiste intuïtie op.
4. Dit betekent dat het type &'a u32 covariant is ten opzichte van 'a, terwijl het voorheen natuurlijker gedefinieerd was als contravariant.
5. Deze .foo directieven zijn specifiek voor Souffle.
6. Negatie wordt in deze regels alleen op een triviale manier gebruikt (genegateerde inputs).
7. Deze subset-propagatieregel is de regel die we later verfijnen.