New paper on unique references and Scala compiler plug-in

Would it be an over-simplification that with the "equivalences"
expose - dosyncunique - reftransient - deref
the contract of a STM like Clojure's is statically enforced and therefore the notion of transaction made obsolete?
-Carsten

On Thu, Apr 9, 2009 at 6:04 PM, Philipp Haller <philipp.haller@epfl.ch> wrote:

Hi all,

I'd like to announce a new paper on unique references by Martin and myself.

 Title:   Capabilities for External Uniqueness

 Authors: Philipp Haller and Martin Odersky

 Abstract:
 Unique object references have many important applications in
 object-oriented programming. For instance, with sufficient
 encapsulation properties they enable safe and efficient transfer
 of message objects between concurrent processes. However, it is
 a long-standing challenge to integrate unique references into
 practical object-oriented programming languages.

 This paper introduces a new approach to external uniqueness.
 The idea is to use capabilities for enforcing both aliasing
 constraints that guarantee external uniqueness, and linear
 consumption of unique references. We formalize our approach as a
 type system, and prove a type preservation theorem. Type safety
 rests on an alias invariant that builds on a novel formalization
 of external uniqueness.

 We show how a capability-based type system can be used to
 integrate external uniqueness into widely available
 object-oriented programming languages. Practical experience
 suggests that our system allows adding uniqueness information to
 common collection classes in a simple and concise way.

The technical report is available as PDF from:
http://lamp.epfl.ch/~phaller/uniquerefs/

An abbreviated version has been submitted to OOPSLA'09. The main difference to the submitted version is that the technical report contains a complete proof of the type preservation theorem.

A prototype implementation of the type system as a Scala compiler plug-in is available in the Scala SVN repository:
http://lampsvn.epfl.ch/trac/scala/browser/compiler-plugins/uniquerefs/trunk

We are planning a more formal release of the plug-in together with one of the next major Scala releases.

Feedback on both the paper and the plug-in is very welcome, of course!

Best regards,
Philipp

This is different from STM.  With STM multiple threads can share reference to mutable objects but they must manipulate the state inside transactions.

With this system the compiler can prove statically that a message passed from one actor to another cannot be referenced by the original actor and therefor can be manipulated by the second without racing the first. 

So while STM is about concurrently sharing things safely, this is about proving that things are not shared.

On Thu, Apr 9, 2009 at 9:43 AM, Carsten Saager <csaager@gmail.com> wrote:

Would it be an over-simplification that with the "equivalences"
expose - dosyncunique - reftransient - deref
the contract of a STM like Clojure's is statically enforced and therefore the notion of transaction made obsolete?
-Carsten

Снова конфуз Не угадал