[cap-talk] controversial article

[Mark Miller]

On Thu, Jul 2, 2009 at 5:03 AM, Matej Kosik <kosik at fiit.stuba.sk> wrote:

>
> I hope that it is correct to say that all object-capability programming
> languages can be used for creating software systems that are defensively
> consistent but none of these languages (or platforms) can be used for
> creating defensively correct software systems. (?)
>

AFAIK, that is true. I am not aware of any ocap *languages* that attempt to
address this.

>
> What about defensive correctness?
> Are there platforms that can be used for building defensively correct
> software systems? (distributed or at least non-distributed).
>

Non-distributed platforms, yes. All the members of the KeyKOS family
(KeyKOS, EROS, GuardOS, CapROS, Coyotos) do/did a brilliant job at this.

Inherent in their approach, the kernel does no implicit allocation. All are
based on rendezvous rather than asynchronous messages, and so no kernel
buffering of messages is implied.

Distributed defensive correctness over unreliable networks is, almost by
definition of "unreliable", impossible.

This suggests defining some possible approximations to defensive
correctness:

* Distributed defensive correctness in the absence of spontaneous partitions
or crashes, where "spontaneous" means, not caused by the actions of the
programs we are concerned with.

* Defensive correctness up to resource exhaustion, which corresponds to the
traditional concept of "liveness". Since this concept is well known in the
literature, you may at least want to mention it, even if only to dismiss it.

* Budgeted and preemptively reclaimable resource allocation, in order to
isolate the effects of resource exhaustion. For example, if we run a
KeyKOS-like system but run only dynamically allocating languages -- or
languages with no contract regarding resource use -- within each KeyKOS-like
process, then an individual KeyKOS like process can still not be defensively
correct, because we can't reason about if it will run out of storage while
serving a valid request from a valid client. However, if it does, it only
exhausts its own storage and thereby fails to service only its own clients.
And it can't prevent the reclamation of its storage by an adequately
authorized subject.

Hope this helps. Good luck!

-- 
Text by me above is hereby placed in the public domain

   Cheers,
   --MarkM
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.eros-os.org/pipermail/cap-talk/attachments/20090702/880767fe/attachment.html