[cap-talk] 'Destroy' vs 'Sever'

[Jonathan S. Shapiro]

On Mon, 2007-11-26 at 21:11 -0800, Charles Landau wrote:

> I repeat, Sever is not an operation on the object.

But aside from implementation convenience, it is not clear why this
should be so. If I allocated an object, I can accomplish the effect of
sever via:

  new alloc
  shallow copy
  destroy old

Given which, it does not seem that there is any semantic or security
motivation that would *preclude* making sever a per-object operation
[except, of course, that we would then need to implement non-several
page caps in the same way that we have non-writable page caps].

I think this question is worth exploring briefly, because it sheds light
on the semantic distinction between severing storage and destroying the
object that resides in that storage. The confusion is exacerbated
(unavoidably) in KeyKOS/EROS/Coyotos because certain data structure
(e.g. Node, Page, GPT, Process) have simultaneous roles as constituent
storage of an aggregate object and as objects in their own right.

Part of the disconnect that I think you and David Hopwood are having
stems from the fact that in a language-based system the duality of
storage and (language) object is never exposed in the operations. Indeed
it *cannot* be, as the hiding of this duality is one of the root sources
of language safety. This explains in part why malloc cannot be
implemented within a conventional safe language. Doing so would require
a combination of monadic style and dynamic cast that has not been
explored in the safe language realm. Realizing free() in a safe system
[even in the underlying version called by GC] is even MORE complex --
probably beyond what type systems are able, in principle, to capture.


shap