On the Termination of Borrow Checking in Featherweight Rust - Université de La Réunion Access content directly
Conference Papers Year : 2022

On the Termination of Borrow Checking in Featherweight Rust

David J Pearce
Fausto Spoto

Abstract

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
Origin Files produced by the author(s)

Dates and versions

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

Identifiers

Cite

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⟩
42 View
202 Download

Altmetric

Share

Gmail Mastodon Facebook X LinkedIn More