CeylonMigrationBot
commented
11 years ago [@HenningB] Seems that noone dares to tackle this stuff. I have to admit, it isn't an easy read, and I didn't read it in whole, as my mind balks with all these formal expressions: theorem, lemma, proof (repeat). That's how my prof at uni did linear algebra, and my mind went blank back then. But I hoped some big brains, which are definitely around here, could cope with it.
Let's start with a short excerpt, defining the four basic qualifiers:
writable: An "ordinary" object reference, which allows mutation of its referent.
readable: A read-only reference, which allows no mutation of its referent. Furthermore, no heap traversal through a read-only reference produces a writable reference (writable references to the same objects may exist and be reachable elsewhere, just not through a readable reference). A readable reference may also refer to an immutable object.
immutable: A read-only reference which additionally notes that its referent can never be mutated through any reference. Immutable references may be aliased by read-only or immutable references, but no other kind of reference. All objects reachable from an immutable reference are also immutable.
isolated: An external reference to an externally-unique object cluster. External uniqueness naturally captures thread locality of data. An externally-unique aggregate is a cluster of objects that freely reference each other, but for which only one external reference into the aggregate exists. We define isolation slightly differently from most work on external uniqueness because we also have immutable objects: all paths to non-immutable objects reachable from the isolated reference pass through the isolated reference. We allow references out of the externally-unique aggregate to immutable data because it adds flexibility without compromising our uses for isolation: converting clusters to immutable, and supporting non-interference among threads (see Figure 1). This change in definition does limit some traditional uses of externally-unique references that are not our focus, such as resource management tasks.
So what I get from it, and translated to Ceylon-speak is somewhat of the following.
writeable: Ceylon's variable or value reference, with refernces within it also changeable.
readable: A value reference with containing references being also values and everything in them 'readable'. So completely accessible, but noone can change anything.
immutable: More or less, what it's description above says, or I'm missing the point here.
isolated: A group of objects referenced by each other, being 'writeable' and such, but only referenced externally by one single point of entry. And this single point does not expose anything behind it, but handles all requests. Some kind of Facade that doesn't expose it's contents.
It needs support by the compiler, to check all references within Type being values and of type Readablity<>, or it's subtype Isolation<>. Plus the obligatory type-decoration and type-erasure (that's what I've figured from reading some compiler discussions). Similar holds true for the other two qualifiers 'immutable' and 'isolated'. The qualifier 'writeable' is around only for completeness.
The paper's research team extended C# with additional type handling, but I think Ceylon already internally has an extended type system, that is sufficient to hold these definitions.
So let me try some pseudo-Ceylon code for 'readable', that doesn't compile. Probably doesn't help much, but that's the best I came up with by checking out ceylon.language.
interface Readability<Type>
given Type satisfies Anything {
}
class ReadabilityAutoImpl<Type>(Type type)
extends Type()
satisfies Readability<Type>
given Type satisfies Anything {
// auto-wrapper around Type
}
Readability<Type> readable(Type type)
given Type satisfies Anything {
return ReadabilityAutoImpl<Type>(type);
}
readable value readableReference = "Hi Folks";
[@HenningB] This proposal is based on a paper called "Uniqueness and Reference Immutability for Safe Parallelism" that has surfaced on Slashdot: "The key to operation is adding permissions to reference types allowing you to declare normal references, read-only references to mutable objects, references to globally immutable objects, and references to isolated clusters of objects. With that information, the compiler is able to prove that chunks of code can safely be run in parallel."
Besides of multithreading verification, the compiler could automatically generate safe multithreaded code blocks out of singlethreaded code. It also would eliminate the needs for functional programming to some extend.
This is definitevely too late for Ceylon 1.0, but maybe it can be introduced in part with Ceylon 1.1 (verification), and fully implemented with Ceylon 2.0 (automatic thread generation). This proposal requires additional qualifiers, and if it gets accepted, it would make sense to introduce these new annotations in the 1.0 SDK, even if they are only marked as reserved without further implementation.
[Migrated from ceylon/ceylon-spec#502]