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

[Jed Donnelley]

On 11/21/2007 5:05 PM, David Hopwood wrote:
> From: Lex Spoon <lex at lexspoon.org>
>> On Wednesday 21 November 2007 17:57:03 David Hopwood wrote:
>>>  I don't know KeyKOS well enough to say whether there were compelling
>>>  uses in that context; in general 'Sever' doesn't seem all that useful
>>>  (no object language that I know of has a similar operation, although
>>>  most have a convention of providing 'clone' for almost all objects).
>> Just to state what might be obvious, 'sever' sounds to me like a
>> simplified 'revoke' revoke the revocation pattern.  After calling
>> sever/revoke, you know that anyone you passed the reference can no longer use
>> their old reference.  So the presence of 'sever' means you can always revoke
>> a reference, even if you did not set up a revoker ahead of time.

I followed this "'Destroy vs 'Sever'" thread until it seemed to
stop.  I'm choosing to reply to this particular message to
mention a few things:

1.  Our NLTSS system had what I believe are these
operations.  We called them 'Destroy' and 'NewCap'.
I believe from what I've read here and elsewhere
(e.g.:
> Yes; both 'Sever' and 'Destroy' only work when the requirement is to
> revoke *all* current references to an object.
) that our semantics were exactly the same.

2.  I agree that 'Sever' is similar to a 'revoke'.  It
is more efficient and requires less setup than supporting
revoke through a separate server - whether with the all
references semantics or if only for a specific capability
instance.  However, 'Sever' revokes all references to
an object, not just a single reference as with 'revoke'.

3.  Any extension mechanism worth it's salt can support such
a 'Sever' call on it's objects, so the issue of whether or not
to support 'Sever' seems to me object specific and out of
the realm of discussion for any TCB/kernel discussions (e.g.
vs. something like EQ).

> That's also true if 'Destroy' is available but 'Sever' is not.

4.  I think David Hopwood (was it?) was suggesting that with
Sever one can revoke a reference (all reverences actually
if I have it right and it is like with NLTSS) without
actually destroying the object itself.  I believe the
semantics of 'Sever' can be achieved by copying out
all the relevant object state into a new object and then
'Destroy'ing the old object (though of course there may
be timing issues).

> The issue raised by 'Sever' is that the new reference it returns
> will point to an object that may malfunction, as a result of not
> receiving messages directed to the old object.

5.  This of course depends on the nature of the object and its
state.  For example, a file/page/segment will not 'malfunction'
in this way with typical semantics.  I suppose you might consider
such things as locking semantics, but it would be wise for any
such 'Sever' operation to release any locks and reset such
state, in addition to returning "invalid" to any pending
calls on 'Sever'ed capabilities.

> This is especially problematic when the object is part of a (nontrivial)
> composite: the Sever operation will break "internal" links from other
> objects of the composite to the severed object, but it won't destroy
> or sever those other objects. The resulting behaviour will depend on
> implementation details of the composite; it won't in general have a simple
> explanation in terms of the composite's documented behaviour.
> 
> 'Destroy' also won't destroy other objects in the composite, but it
> will prevent the destroyed object from being invoked and from performing
> any invocations. At the point at which another object of the composite
> tries to invoke the destroyed object via an existing reference, it will
> receive an error (typically reported as an exception at the language level),
> which assuming it is not ignored, will abort the current "plan" of the
> other object.

I'm sorry, but I don't understand the issue above.  Perhaps an
example "composite" might help?  I don't see a significant difference
between 'Sever' and 'Destroy' with regard to any such composite
object.  In both cases any references in the 'composite' will
return "Invalid" when invoked.  As I noted above, equivalent
semantics to 'Sever' can be implemented in most cases by
copying object state and then doing a 'Destroy'.

>>> I have not delved into such systems enough to say whether you want this to
>>> always be available on every reference.  One issue is that it is a really
>>> simplified instance of the revocation pattern, so many users of the
>>> revocation pattern will not be able to use this primitive.
> 
> Yes; both 'Sever' and 'Destroy' only work when the requirement is to
> revoke *all* current references to an object.

6.  and I believe the above makes 'Sever' different from 'revoke'.
E.g. if I ask an object for a reduced permission instance
(e.g. a RO file from a RW file), 'revoke' on either capability
will leave the other intact (not referring to 'membrane'
semantics which are of course richer).  'Sever' will invalidate
all references to the underlying object.

> [...]
>>> An additional use would seem to be to help with an issue I've long wondered
>>> about with the programmer's shell.  If you are a programmer monkeying with
>>> your system, then you will sometimes write incorrect code.  I know, I know,
>>> none of the present company, but some programmers do write incorrect code
>>> sometimes.  In such a case, it would seem nice if the shell gave you some
>>> sort of revocation available on all of the objects "owned" by that
>>> programmer, so that they can get the system back into a sane state with no
>>> leaked references.
> 
> 'Destroy' seems to be sufficient for this.

7.  I believe 'Destroy' suffices in general.  As noted above
I believe 'Sever' (our 'NewCap') can be effected by copying
state and doing a 'Destroy'.  Of course there are issues of
fixing state, there may different sorts of state for different
types of objects, and there can be efficiency issues.  For
me 'Sever' makes sense exactly because if simplifies all
the above.

--Jed http://www.webstart.com/jed/