[cap-talk] Hybrid Cap Systems redux

[Sandro Magi]

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 
search:
http://www.memorymanagement.org/bib/printezis96.html

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 
invoked.

> 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 
now safe!

Sandro