On Thu, Nov 4, 2010 at 2:26 PM, Jonathan S. Shapiro <[email protected]>wrote:
> On Wed, Nov 3, 2010 at 8:15 PM, Ben Karel <[email protected]> wrote: > >> >> From what I've read of the literature so far, the most well-known >> approaches are regions, ownership, and separation logic. >> > > Of these, I think only regions provide a complete solution. I'll return to > this momentarily. > Before I disappear for that hour, let me unpack this slightly. Imagine, as an example, that we choose a non-contiguous implementation of VectorPayload. Concretely: imagine we implement our VectorPayload as some sort of collection whose individual pieces are contiguous sequences of bounded length. Pragmatically, one might credibly choose to do this to bound delay in concurrent GC. But in this case, we have VectorPayload, an aggregate "object", that has a number of component runtime objects. And we have a contract that these objects have related mutability (all are mutable or none are mutable), and we further have that mutability contract needing to be expressed separately from the mutability of things further down the graph structure (for example, if it's an array of references to mutable things). What's just happened here is that we've introduced a need to coherently describe relations between commingled storage. That's precisely what regions do. At their core, regions are simply a tagging mechanism. Region-based memory analysis then builds a dominance relationship over the tags, but the regions themselves are just tags, and we then need a way to state which regions are mutable and which are not. My concern about regions remains that their expressiveness can lead rapidly to high complexity, but their are still the right conceptual tool for this problem. More in a bit.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
