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...

• Type: Journal
• Year: 2012
• Where: POPL
• Authors: Karl Naden, Robert Bocchino, Jonathan Aldrich, Kevin Bierhoff
• Keywords: Correctness Properties, Dynamic Semantics, Memory Updates, POPL 2012, Programming Languages