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. Conferences, Workshops, Symposiums, and Seminars
  4. Capabilities for Uniqueness and Borrowing
 
conference paper

Capabilities for Uniqueness and Borrowing

Haller, Philipp  
•
Odersky, Martin  
2010
ECOOP 2010 – Object-Oriented Programming
24th European Conference on Object-Oriented Programming

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
conference paper
DOI
10.1007/978-3-642-14107-2_17
Web of Science ID

WOS:000284803700016

Author(s)
Haller, Philipp  
Odersky, Martin  
Date Issued

2010

Publisher

Springer

Published in
ECOOP 2010 – Object-Oriented Programming
Series title/Series vol.

Lecture Notes in Computer Science; 6183

Start page

354

End page

378

Subjects

Aliasing

•

Linear Types

•

Capabilities

•

Uniqueness

•

Borrowing

•

Concurrency

•

Scala

•

Actors

URL

URL

http://lamp.epfl.ch/~phaller/capabilities.html
Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
LAMP1  
Event nameEvent placeEvent date
24th European Conference on Object-Oriented Programming

Maribor, Slovenia, EU

June 21-25, 2010

Available on Infoscience
April 9, 2010
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/49286
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