Thanks for the references. I'll dig into separation logic and bunched implications. Responses below..
On Sat, Aug 2, 2014 at 3:23 PM, Matt Oliveri <[email protected]> wrote: > 5. Any borrowed pointer appears on a stack frame (as in Rust) or (now) > in some ComplexStructure rooted right under a stack frame. So when we > deallocate something like ListA, we can easily find all the > ComplexStructures to call releaseObject on a lot. > I'm not very concerned with short-lived data-structures on stack frames as stack-based borrowing already works quite well for these scenarios. I'm concerned with long lived heap data-structures. ListA is a heap-global owning structure and ComplexStructureB is a heap-global borrowing structure. Objects can be created into ListA as an owner, afterwhich they can be borrowed into ComplexStructureB. When the user deletes an object from ListA, is it guaranteed to be removed from ComplexStructureB because of the releaseObject() runtime event. > I'm guessing you want to know which containers tend to have efficient > implementations of releaseObject. I don't know, but it seems like > there ought to be a lot, > *otherwise manual memory management would beinfeasible more often than it > actually is*. > YES, and this is exactly my inspiration for the thought experiment. (Or maybe the programmer writes releaseObject. But in that case, > automatically proving it correct is probably too hard.) > The programmer must write releaseObject, because the idea is for releaseObject to operate as efficiently as possible. For example, an object indexed in a sorted-structure should be efficiently found and then removed. HOWEVER, the language to write releaseObject can be severely constrained, possibly not even turing complete -- for the purpose of making it provable. 4. So for a borrows-pointers data type, the compiler will try to > generate and prove-correct a releaseObject operation, which takes a > pointer "foo" and mutates the structure in place so that it no longer > references foo. > Yes. If the container is an "owner" of it's contents, then it has no sources of incoming releaseObject() calls. Only the programmer would make those calls. (aka, it is a root owner). Any other container referencing that data becomes a borrower. It is also possible to borrow from borrowers. (How does it know how this should be done? Is it always just nulling > the places where the pointer occurs? That sounds kind of like weak > references.) > Keep in mind that we are only talking about singly-owned objects and borrowers to keep the discussion simple. There are other implications outside this scenario. I'll elaborate a bit on this below. These borrowed references are conceptually a bit like weak-references. The difference being that **no expensive tracing is required** to make them memory-safe. If the original object is deleted, any borrowers are notified and must also delete references to that object. Hopefully it is not just nulling the pointer, but is cleanly removing that object entry from the data-structure. For example, if a borrowed object was added to a linked list, the removal would remove that linked list node entirely, not just leave a null pointer behind. However, it would be acceptable to merely null the reference and defer the cleanup -- like a weak-reference. (Would you call releaseObject for each borrowed object, or just for > the whole data structure, with other objects it owns being implicitly > released too. Either way, it looks like in general, you're doing a > nested traversal over both data structures, which would be rather > slow.) > If an entire data-structure is released (such as releasing ListA), then any borrowers can get a "releaseAllFrom(ListA)". If they only hold references from ListA, then they can be fully released quickly. If they borrow references from other sources, then the ListA entries will need to be removed one by one. releaseObject() can be O(1) for indexed structures and O(borrower-size) for non-indexed structures. relaseAllFrom(ListA) can be O(1) for single-source borrowers, and O(min(borrowersize,lista)) for multi-source borrowers. When heapsize is large, all of these seem much better than a tracing collector to me, because a tracing collector can only collect these through work proportional to the entire live heap. > > A) IF we can *prove* that after the release-event is called, > > ComplexStructureB no longer holds any references to the object, then I > think > > we can have typesafe memorysafe non-tracing precise heap collection for > that > > container. > > Well, you have to wonder whether it should really count as > non-tracing, if it has to traverse ComplexStructureB completely. But I > do see that there would be cases where the programmer could point out > a smarter way. > The goal is to use a smarter way to remove references. However, even if we are tracing, we are only tracing the borrowing-container, not the entire live heap! ------ Moving beyond the simple "single owner borrowing", this can also be a method of handling cycles without tracing in a reference-counting collector. If it can be easy to write provable programs in a constrained language to manipulate (possibly cyclic) data-structures, then we can essentially ignore their references. ComplexStructureB, which contains internal cycles, can reference-count it's "ownership" of an object as a single reference, ignoring it's own internal cyclic references -- since they are manipulated by a provably correct container-manipulation sub-language. > > B) However, IF we can prove that it's *unprovable* whether or not a > > release-event removes all references to an object, then I think we've > proven > > it's not possible have typesafe memorysafe non-tracing precise heap > > collection for that container > > Proving something unprovable requires a couter-model. And you didn't > say which logic it should be unprovable in. Did you just mean "prove > that releaseObject is unimplementable"? > The halting-problems says every turing complete program can't be proven to finish, which means a touring-complete implementation of releaseObject can't necessarily be proven to even finish, let alone release the object. Therefore, if we can prove that some reasonably interesting data-structure (say a kd-tree), requires a turning complete language to insert into, then we have proven that it is impossible to have a provably correct releaseObject implementation. However, I suspect there is a non-turing complete subset language which could provably manipulate many many common data-structures.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
