On the Termination of Borrow Checking in Featherweight Rust - Université de La Réunion Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

On the Termination of Borrow Checking in Featherweight Rust

David J Pearce
Fausto Spoto

Résumé

A distinguished feature of the Rust programming language is its ability to deallocate dynamically-allocated data structures as soon as they go out of scope, without relying on a garbage collector. At the same time, Rust lets programmers create references, called borrows, to data structures. A static borrow checker enforces that borrows can only be used in a controlled way, so that automatic deallocation does not introduce dangling references. Featherweight Rust provides a formalisation for a subset of Rust where borrow checking is encoded using flow typing [25]. However, we have identified a source of non-termination within the calculus which arises when typing environments contain cycles between variables. In fact, it turns out that well-typed programs cannot lead to such environments-but this was not immediately obvious from the presentation. This paper defines a simplification of Featherweight Rust, more amenable to formal proofs. Then it develops a sufficient condition that forbids cycles and, hence, guarantees termination. Furthermore, it proves that this condition is, in fact, maintained by Featherweight Rust for welltyped programs.
Fichier principal
Vignette du fichier
nfm22.pdf (536.81 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-04055346 , version 1 (02-04-2023)

Identifiants

Citer

Etienne Payet, David J Pearce, Fausto Spoto. On the Termination of Borrow Checking in Featherweight Rust. NASA Formal Methods (NFM 2022), Jyotirmoy V. Deshmukh; Klaus Havelund; Ivan Perez, May 2022, Pasadena (CA), United States. pp.411-430, ⟨10.1007/978-3-031-06773-0_22⟩. ⟨hal-04055346⟩
47 Consultations
216 Téléchargements

Altmetric

Partager

Gmail Mastodon Facebook X LinkedIn More