(As seen posted on an Obj Cap list today)
Uniqueness and Reference Immutability for Safe Parallelism. 2012.
We provide a novel combination of im- mutable and unique (isolated) types that ensures safe paral- lelism (race freedom and deterministic execution). The type system includes support for polymorphism over type quali- fiers, and can easily create cycles of immutable objects. Key to the systemâ€™s flexibility is the ability to recover immutable or externally unique references after violating uniqueness without any explicit alias tracking. Our type system models a prototype extension to C# that is in active use by a Mi- crosoft team. We describe their experiences building large systems with this extension. We prove the soundness of the type system by an embedding into a program logic.