A type system for borrowing permissions

11 years 1 months ago
A type system for borrowing permissions
In object-oriented programming, unique permissions to object references are useful for checking correctness properties such as consistency of typestate and noninterference of concurrency. To be usable, unique permissions must be borrowed — for example, one must be able to read a unique reference out of a field, use it for something, and put it back. While one can null out the field and later reassign it, this paradigm is ungainly and requires unnecessary writes, potentially hurting cache performance. Therefore, in practice borrowing must occur in the type system, without requiring memory updates. Previous systems support borrowing with external alias analysis and/or explicit programmer management of fractional permissions. While these approaches are powerful, they are also awkward and difficult for programmers to understand. We present an integrated language and type system with unique, immutable, and shared permissions, together with new local permissions that say that a referen...
Karl Naden, Robert Bocchino, Jonathan Aldrich, Kev
Added 25 Apr 2012
Updated 25 Apr 2012
Type Journal
Year 2012
Where POPL
Authors Karl Naden, Robert Bocchino, Jonathan Aldrich, Kevin Bierhoff
Comments (0)