A glimpse of some research we’ve done recently just appeared at OOPSLA last week:
Uniqueness and Reference Immutability for Safe Parallelism
A key challenge for concurrent programming is that side-effects (memory operations) in one thread can affect the behavior of another thread. In this paper, we present a type system to restrict the updates to memory to prevent these unintended side-effects. We provide a novel combination of immutable and unique (isolated) types that ensures safe parallelism (race freedom and deterministic execution). The type system includes support for polymorphism over type qualifiers, 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 Microsoft 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.
The official ACM page is here, and a tech report version is available on MSR’s website.
As I said, this is just a glimpse. Its focus was mainly on the type soundness work we’ve done jointly with MSR, and less about the language, syntax, and uses. You’ll have to use your imagination to fill in the rest ;-)