My side conversation with Raoul generated a not-obviously-terrible random though in the space of GC, borrowing, and static collection strategies. I'm curious if anyone knows of similar research, or has thoughts on it.
Tracing GC knows an object is no longer referenced because it uses a tracing prover to prove it at runtime. My idea here is to instead build runtime inductive reachability enforcement through API conformance and small provable data-structure programs. For now, lets consider only singly-owned objects. A container which wishes to hold borrowed pointers must implement a runtime releaseObject(foo) API, which the compiler must prove will remove all references to the object. Here is an example: ListA owns the objects. ComplexStructureB indexes borrowed pointers to the objects. The compiler would REQUIRE ComplexStructureB to implement the runtime releaseObject(foo) Event API, which the compiler has proven will remove all borrowed pointers to foo in the data-structure. Essentially, what this is doing is narrowing the scope of static analysis to only a single container. ComplexStructureB may have any pointers or data-elements it likes, as long as locally within that structure we can prove coherent "add/remove" semantics for an object. This is much like what happens ad-hoc in manual memory management. A C++ programmer believes it is safe to delete an object because he trusts that the code is written to not have any outstanding references. Is this making sense? This can be thought of as a mechanism to extend the lifetime semantics of borrowed pointers. Rust borrowed pointers are only allowed while in a nested-stack-frame. We can extend the lifetime of this borrowing if the container which wishes to borrow them agrees to honor a "release on request" event api releaseObject(foo) -- and that we can prove that releaseObject() code is implemented correctly. Rather than attempt to make this work for *any* code, we instead supply a domain-specific subset language for writing provable container operations. [1] 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. 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 --- "A" is certainly possible for some container data-structures. Therefore, this becomes an experiment in finding the limits of provable container manipulations. Can a language be written which allows operations on any container structure to be proven, or are there certain data-structures which can't be proven? As an interesting base-case, if we can prove a program can fully traverse a data-structure, we can prove it can release any reference in the data-structure (though it will require a full-traverse to do so) Obviously a prover like this would require some kind of invariant "indexing data" along with an identity test, such as a string used to sort something into a sorted-list and the actual object pointer. The indexing-data seems relatively easy, either via full-non-mutability, STM, or merely evaluating removal-and-insertion anytime indexing data changed. (though it requires other code never allows direct field-modification outside the reachability prover's view) The identity-test can be the pointer, as long as we don't compact or we have a means of fixing up relocated pointers. Before I deep end any more on this.... Is there any related research I should read? Does this sound interesting? totally bunk? Been tried before? Original? Any feedback is appreciated. [1] For related reading, check out this MIT Exokernel paper <http://pdos.csail.mit.edu/~engler/sosp-97.ps> on safety sharing a file partition through induction provers.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
