Η αρχιτεκτονική της ανάδρομης σάρωσης
Σε αντίθεση με τους παραδοσιακούς borrow checkers, όπως αυτός της Rust που βασίζεται σε forward-pass ανάλυση και constraint solving, ο borrow checker της Valen υιοθετεί μια ανάδρομη προσέγγιση. Κατά τη φάση του safety-checking, ο αλγόριθμος διατρέχει τον κώδικα από την τελευταία εντολή προς την πρώτη, διατηρώντας μια λίστα με τις εκκρεμείς χρήσεις (pending list).
Μηχανισμός ελέγχου ασφαλείας
Η λογική του αλγορίθμου βασίζεται σε τρία βασικά γεγονότα κατά την ανάδρομη πορεία:
- USE: Προσθήκη της μεταβλητής στη λίστα pending.
- MUTATE: Έλεγχος αν κάποια μεταβλητή στη λίστα pending επηρεάζεται από τη μετάλλαξη (αν ναι, προκύπτει σφάλμα use-after-free).
- DECLARE: Αφαίρεση της μεταβλητής από τη λίστα pending, καθώς η εμβέλειά της ορίζεται πλέον έγκυρα.
Αυτή η προσέγγιση καθιστά την ανίχνευση των use-after-free σφαλμάτων εξαιρετικά άμεση, καθώς η σύγκρουση εντοπίζεται τη στιγμή που η ανάδρομη σάρωση συναντά μια μετάλλαξη που ακυρώνει μια ήδη καταγεγραμμένη χρήση.
Διαχείριση βρόχων (loops) και πολυπλοκότητα
Η διαχείριση των loops αποτελεί την κύρια πρόκληση για την ανάδρομη σάρωση. Η Valen επιλύει αυτό το ζήτημα εισάγοντας λίστες mutations_after_this και revived_after_this ανά loop. Κατά την είσοδο στο loop (LOOP START), ο αλγόριθμος επαληθεύει ότι οποιαδήποτε μεταβλητή στη λίστα pending που υφίσταται μετάλλαξη εντός του loop, έχει υποστεί και την αντίστοιχη αναζωογόνηση (re-declaration), διασφαλίζοντας έτσι τη μνημονική ασφάλεια χωρίς την ανάγκη για πολλαπλά forward passes ή dataflow fixpoints.