000142817 001__ 142817
000142817 005__ 20190316234645.0
000142817 037__ $$aREP_WORK
000142817 245__ $$aCapabilities for Uniqueness and Borrowing
000142817 269__ $$a2009
000142817 260__ $$c2009
000142817 300__ $$a51
000142817 336__ $$aReports
000142817 520__ $$aAn important application of unique object references is safe and efficient message passing in concurrent object-oriented programming. However, to prevent the ill effects of aliasing, practical systems often severely restrict the shape of messages passed by reference. Moreover, the problematic interplay between destructive reads--often used to implement unique references--and temporary aliasing through "borrowed" references is exacerbated in a concurrent setting, increasing the potential for unpredictable run-time errors. This paper introduces a new approach to uniqueness. The idea is to use capabilities for enforcing both at-most-once consumption of unique references, and a flexible notion of uniqueness. The main novelty of our approach is a model of uniqueness and borrowing based on simple, unstructured capabilities. The advantages are: first, it provides simple foundations for uniqueness and borrowing. Second, it can be formalized using a relatively simple type system, for which we provide a complete soundness proof. Third, it avoids common problems involving borrowing and destructive reads, since unique references subsume borrowed references. We have implemented our type system as an extension to Scala. Practical experience suggests that our system allows type checking real-world actor-based concurrent programs with only a small number of additional type annotations.
000142817 6531_ $$aAliasing
000142817 6531_ $$aLinear Types
000142817 6531_ $$aCapabilities
000142817 6531_ $$aUniqueness
000142817 6531_ $$aBorrowing
000142817 6531_ $$aConcurrency
000142817 6531_ $$aScala
000142817 6531_ $$aActors
000142817 700__ $$0240993$$g172057$$aHaller, Philipp
000142817 700__ $$0241835$$g126003$$aOdersky, Martin
000142817 8564_ $$uhttp://lamp.epfl.ch/~phaller/capabilities.html$$zURL
000142817 8564_ $$uhttps://infoscience.epfl.ch/record/142817/files/haller-odersky09-Capabilities_for_uniqueness_and_borrowing_TR.pdf$$zn/a$$s345457
000142817 909C0 $$xU10409$$0252187$$pLAMP
000142817 909CO $$ooai:infoscience.tind.io:142817$$qGLOBAL_SET$$pIC$$preport
000142817 937__ $$aLAMP-REPORT-2009-004
000142817 973__ $$sPUBLISHED$$aEPFL
000142817 980__ $$aREPORT