[cap-talk] Hybrid Cap Systems redux
naasking at higherlogics.com
Tue Feb 19 09:36:56 EST 2008
Jonathan S. Shapiro wrote:
> Sandro: you have my concern backwards. My concern is that real-world
> capability systems need to scale to terabytes of data. This exceeds
> 32-bit spaces by a very large margin, and it exceeds available core
> working set even on 64-bit system.
> While I agree that GC "works", I believe that many of the GC-based
> approaches will be pragmatic failures when they are forced to switch
> from memory-GC to disk-GC.
I haven't read much on disk-based GC, but I found this after a cursory
There are a number of ways I can see to address more than 32-bits on
32-bit machines. Assuming a domain is the unit of persistence, all
cross-domain pointers are made "fat", like the capability descriptors in
EROS, and a simple pre-deref check can ensure that the target object is
in-memory first. If it's not, the runtime's object faulting logic is
> This is complete nonsense. Proof carrying code does not alter the safety
> of the code. You still have the problem of generating the proofs, and
> you simply aren't going to do that for C.
Proofs are a separable concern. Analyses already exist for inferring
safety properties of C subsets, and while I doubt an analysis will ever
encompass all of C, we may get to a point where a safety can be ensured
for a sufficiently broad C subset of C to compile many programs. For the
unknown accesses, there are runtime checks or user-provided proofs. All
you really need for capability systems is memory safety in a domain.
While proof techniques are still very onerous, they are getting
significant attention and I expect they may be usable more mere mortals
within 10 years.
> Two problems here:
> 1. C is unsafe, therefore these safety checks violate C semantics (and
> do so in practice, not just on paper).
They don't prevent the ability to write allocators, do pointer
arithmetic, etc. They use static analysis combined with runtime checks
to ensure that memory errors are prevented. An erroneous memory access
does not have a defined semantics.
> 2. It is a continuing source of wonder to me that people think it is
> good to induce failure in working C programs by adding checks that
> cause perfectly good programs to fail.
I'm not sure what failures you're referring to. LLVM's SAFECode project
does not induce C programs to fail. Quote the opposite, previously
failing programs no longer fail since out of bound memory accesses are
More information about the cap-talk