Reference Capabilities for Flexible Memory Management
Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, James Noble, Matthew J. Parkinson, Tobias Wrigstad
Abstract
Verona is a concurrent object-oriented programming language that organises all the objects in a program into a forest of isolated regions. Memory is managed locally for each region, so programmers can control a program's memory use by adjusting objects' partition into regions, and by setting each region's memory management strategy. A thread can only mutate (allocate, deallocate) objects within one active region---its "window of mutability". Memory management costs are localised to the active region, ensuring overheads can be predicted and controlled. Moving the mutability window between regions is explicit, so code can be executed wherever it is required, yet programs remain in control of memory use. An ownership type system based on reference capabilities enforces region isolation, controlling aliasing within and between regions, yet supporting objects moving between regions and threads. Data accesses never need expensive atomic operations, and are always thread-safe.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext d28622a3-bf2b-4461-b937-579738ad626bCited by top-tier papers6
- When Concurrency Matters: Behaviour-Oriented ConcurrencyLuke Cheeseman, Matthew J. Parkinson, Sylvan Clebsch, Marios Kogias et al.OOPSLA 2023 · 9 citations
- Data Race Freedom à la ModeAïna Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White et al.POPL 2025 · 6 citations
- What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data StructuresYichen Xu, Oliver Bracevac, Cao Nguyen Pham, Martin OderskyOOPSLA 2025 · 4 citations
- Dynamic Region Ownership for Concurrency SafetyFridtjof Peer Stoldt, Gary Brandt Bucher II, Sylvan Clebsch, Matthew A. Johnson et al.PLDI 2025 · 4 citations
- Complete the Cycle: Reachability Types with Expressive Cyclic ReferencesHaotian Deng, Siyuan He, Songlin Jia, Yuyan Bao et al.OOPSLA 2025 · 3 citations
Builds on6
- Understanding memory and thread safety practices and issues in real-world Rust programsBoqin Qin, Yilun Chen, Zeming Yu, Linhai Song et al.PLDI 2020 · 112 citations
- Stacked borrows: an aliasing model for RustRalf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek DreyerPOPL 2020 · 67 citations
- Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and backJonathan Immanuel Brachthäuser, Philipp Schuster, Edward Lee, Aleksander Boruch-GruszeckiOOPSLA 2022 · 24 citations
- A flexible type system for fearless concurrencyMae Milano, Joshua Turcotti, Andrew C. MyersPLDI 2022 · 14 citations
- When Concurrency Matters: Behaviour-Oriented ConcurrencyLuke Cheeseman, Matthew J. Parkinson, Sylvan Clebsch, Marios Kogias et al.OOPSLA 2023 · 9 citations
Related papers
- Veracity: declarative multicore programming with commutativityAdam Chen, Parisa Fathololumi, Eric Koskinen, Jared PincusOOPSLA 2022 · 2 citations
- Verus: Verifying Rust Programs using Linear Ghost TypesAndrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun et al.OOPSLA 2023 · 86 citations
- Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent SystemsTravis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann et al.OSDI 2023 · 18 citations
- From Linearity to BorrowingAndrew Wagner, Olek Gierczak, Brianna Marshall, John M. Li et al.OOPSLA 2025 · 1 citation
- A Framework for the Interoperable Specification and Verification of Encapsulated Data StructuresWolfram Pfeifer, Werner Dietl, Mattias UlbrichFM 2026
