Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Reports, Documentation, and Standards
  4. Capabilities for Uniqueness and Borrowing
 
report

Capabilities for Uniqueness and Borrowing

Haller, Philipp  
•
Odersky, Martin  
2009

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

  • Files
  • Details
  • Metrics
Type
report
Author(s)
Haller, Philipp  
Odersky, Martin  
Date Issued

2009

Total of pages

51

Subjects

Aliasing

•

Linear Types

•

Capabilities

•

Uniqueness

•

Borrowing

•

Concurrency

•

Scala

•

Actors

URL

URL

http://lamp.epfl.ch/~phaller/capabilities.html
Written at

EPFL

EPFL units
LAMP1  
Available on Infoscience
December 14, 2009
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/44842
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés