Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees
Rust's novel type system has proved an attractive target for verification and program analysis tools, due to the rich guarantees it provides for controlling aliasing and mutability. However, fully understanding, extracting and exploiting these guarantees is subtle and challenging: existing models...
Zapisane w:
| Główni autorzy: | , , , , , , |
|---|---|
| Format: | Artykuł |
| Wydane: |
2025
|
| Hasła przedmiotowe: | |
| Dostęp online: | https://arxiv.org/abs/2503.21691 http://arxiv.org/abs/2503.21691 |
| Etykiety: |
Nie ma etykietki, Dołącz pierwszą etykiete!
|
| _version_ | 1879179655028670464 |
|---|---|
| author | Grannan, Zachary Bílá, Aurea Fiala, Jonáš Geer, Jasper de Medeiros, Markus Müller, Peter Summers, Alexander J. |
| author_browse | Bílá, Aurea Fiala, Jonáš Geer, Jasper Grannan, Zachary Müller, Peter Summers, Alexander J. de Medeiros, Markus |
| author_facet | Grannan, Zachary Bílá, Aurea Fiala, Jonáš Geer, Jasper de Medeiros, Markus Müller, Peter Summers, Alexander J. |
| author_sort | Grannan, Zachary |
| building | arXiv |
| collection | Acceso abierto |
| description | Rust's novel type system has proved an attractive target for verification and program analysis tools, due to the rich guarantees it provides for controlling aliasing and mutability. However, fully understanding, extracting and exploiting these guarantees is subtle and challenging: existing models for Rust's type checking either support a smaller idealised language disconnected from real-world Rust code, or come with severe limitations in terms of precise modelling of Rust borrows, composite types storing them, function signatures and loops.
In this paper, we present a novel model of Rust's type-checking called Place Capability Graphs, which lifts these limitations, and which can be directly calculated from the Rust compiler's own programmatic representations and analyses. We demonstrate that our model supports over 97% of Rust functions in the most popular public crates, and show its suitability as a general-purpose basis for verification and program analysis tools by developing promising new prototype versions of the existing Flowistry and Prusti tools. |
| first_indexed | 2026-10-16T01:36:02Z |
| format | Article |
| fullrecord | <oai_dc:dc xmlns:oai_dc="http://www.openarchives.org/OAI/2.0/oai_dc/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.openarchives.org/OAI/2.0/oai_dc/ https://www.openarchives.org/OAI/2.0/oai_dc.xsd"><identifier>arxiv-2503.21691</identifier><datestamp>2026-07-13</datestamp>
<dc:title>Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees</dc:title>
<dc:creator>Grannan, Zachary</dc:creator>
<dc:creator>Bílá, Aurea</dc:creator>
<dc:creator>Fiala, Jonáš</dc:creator>
<dc:creator>Geer, Jasper</dc:creator>
<dc:creator>de Medeiros, Markus</dc:creator>
<dc:creator>Müller, Peter</dc:creator>
<dc:creator>Summers, Alexander J.</dc:creator>
<dc:subject>Programming Languages</dc:subject>
<dc:description> Rust's novel type system has proved an attractive target for verification and program analysis tools, due to the rich guarantees it provides for controlling aliasing and mutability. However, fully understanding, extracting and exploiting these guarantees is subtle and challenging: existing models for Rust's type checking either support a smaller idealised language disconnected from real-world Rust code, or come with severe limitations in terms of precise modelling of Rust borrows, composite types storing them, function signatures and loops.
In this paper, we present a novel model of Rust's type-checking called Place Capability Graphs, which lifts these limitations, and which can be directly calculated from the Rust compiler's own programmatic representations and analyses. We demonstrate that our model supports over 97% of Rust functions in the most popular public crates, and show its suitability as a general-purpose basis for verification and program analysis tools by developing promising new prototype versions of the existing Flowistry and Prusti tools. </dc:description>
<dc:date>2025-03-27</dc:date>
<dc:date>2025-08-25</dc:date>
<dc:type>text</dc:type>
<dc:identifier>https://arxiv.org/abs/2503.21691</dc:identifier>
<dc:identifier>http://arxiv.org/abs/2503.21691</dc:identifier>
</oai_dc:dc> |
| id | arxiv-2503.21691 |
| institution | arXiv |
| last_indexed | 2026-10-16T01:36:02Z |
| publishDate | 2025 |
| publishDateRange | 2025 |
| publishDateSort | 2025 |
| record_format | oai_dc |
| spelling | arxiv-2503.216912026-07-13 Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees Grannan, Zachary Bílá, Aurea Fiala, Jonáš Geer, Jasper de Medeiros, Markus Müller, Peter Summers, Alexander J. Programming Languages Rust's novel type system has proved an attractive target for verification and program analysis tools, due to the rich guarantees it provides for controlling aliasing and mutability. However, fully understanding, extracting and exploiting these guarantees is subtle and challenging: existing models for Rust's type checking either support a smaller idealised language disconnected from real-world Rust code, or come with severe limitations in terms of precise modelling of Rust borrows, composite types storing them, function signatures and loops. In this paper, we present a novel model of Rust's type-checking called Place Capability Graphs, which lifts these limitations, and which can be directly calculated from the Rust compiler's own programmatic representations and analyses. We demonstrate that our model supports over 97% of Rust functions in the most popular public crates, and show its suitability as a general-purpose basis for verification and program analysis tools by developing promising new prototype versions of the existing Flowistry and Prusti tools. 2025-03-27 2025-08-25 text https://arxiv.org/abs/2503.21691 http://arxiv.org/abs/2503.21691 |
| spellingShingle | Programming Languages Grannan, Zachary Bílá, Aurea Fiala, Jonáš Geer, Jasper de Medeiros, Markus Müller, Peter Summers, Alexander J. Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees |
| title | Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees |
| title_full | Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees |
| title_fullStr | Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees |
| title_full_unstemmed | Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees |
| title_short | Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees |
| title_sort | place capability graphs a general purpose model of rust s ownership and borrowing guarantees |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2503.21691 http://arxiv.org/abs/2503.21691 |
| work_keys_str_mv | AT grannanzachary placecapabilitygraphsageneralpurposemodelofrustsownershipandborrowingguarantees AT bilaaurea placecapabilitygraphsageneralpurposemodelofrustsownershipandborrowingguarantees AT fialajonas placecapabilitygraphsageneralpurposemodelofrustsownershipandborrowingguarantees AT geerjasper placecapabilitygraphsageneralpurposemodelofrustsownershipandborrowingguarantees AT demedeirosmarkus placecapabilitygraphsageneralpurposemodelofrustsownershipandborrowingguarantees AT mullerpeter placecapabilitygraphsageneralpurposemodelofrustsownershipandborrowingguarantees AT summersalexanderj placecapabilitygraphsageneralpurposemodelofrustsownershipandborrowingguarantees |