Reference Capabilities for Flexible Memory Management
Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, James Noble, Matthew J. Parkinson, Tobias Wrigstad
摘要
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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了每一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
引用它的顶会 Paper6
- When Concurrency Matters: Behaviour-Oriented ConcurrencyLuke Cheeseman, Matthew J. Parkinson, Sylvan Clebsch, Marios Kogias 等OOPSLA 2023 · 被引用 9 次
- Data Race Freedom à la ModeAïna Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White 等POPL 2025 · 被引用 6 次
- What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data StructuresYichen Xu, Oliver Bracevac, Cao Nguyen Pham, Martin OderskyOOPSLA 2025 · 被引用 4 次
- Dynamic Region Ownership for Concurrency SafetyFridtjof Peer Stoldt, Gary Brandt Bucher II, Sylvan Clebsch, Matthew A. Johnson 等PLDI 2025 · 被引用 4 次
- Complete the Cycle: Reachability Types with Expressive Cyclic ReferencesHaotian Deng, Siyuan He, Songlin Jia, Yuyan Bao 等OOPSLA 2025 · 被引用 3 次
它引用的顶会 Paper6
- Understanding memory and thread safety practices and issues in real-world Rust programsBoqin Qin, Yilun Chen, Zeming Yu, Linhai Song 等PLDI 2020 · 被引用 112 次
- Stacked borrows: an aliasing model for RustRalf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek DreyerPOPL 2020 · 被引用 67 次
- 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 次
- A flexible type system for fearless concurrencyMae Milano, Joshua Turcotti, Andrew C. MyersPLDI 2022 · 被引用 14 次
- When Concurrency Matters: Behaviour-Oriented ConcurrencyLuke Cheeseman, Matthew J. Parkinson, Sylvan Clebsch, Marios Kogias 等OOPSLA 2023 · 被引用 9 次
相关 Paper
- Veracity: declarative multicore programming with commutativityAdam Chen, Parisa Fathololumi, Eric Koskinen, Jared PincusOOPSLA 2022 · 被引用 2 次
- Verus: Verifying Rust Programs using Linear Ghost TypesAndrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun 等OOPSLA 2023 · 被引用 86 次
- Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent SystemsTravis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann 等OSDI 2023 · 被引用 18 次
- From Linearity to BorrowingAndrew Wagner, Olek Gierczak, Brianna Marshall, John M. Li 等OOPSLA 2025 · 被引用 1 次
- A Framework for the Interoperable Specification and Verification of Encapsulated Data StructuresWolfram Pfeifer, Werner Dietl, Mattias UlbrichFM 2026
