[cap-talk] controversial article

[Matej Kosik]

Mark Miller wrote:
> On Thu, Jul 2, 2009 at 5:03 AM, Matej Kosik <kosik at fiit.stuba.sk
> <mailto: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.

I have added this paragraph:

<text>
All members of the KeyKOS family of operating systems
(KeyKOS, EROS, CapROS, Coyotos) achieved defensive correctness.
All are based on rendezvous rather than asynchronous messages,
and so no kernel buffering of messages is necessary.
We are interested how to enable asynchronous message passing
without disrupting the possibility to build defensively correct
software systems.
</text>

All the reasons for preferring asynchronous message passing as a basic
communication mechanism over synchronous rendezvous are not listed directly.

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

I was confused for a while but now I think I see the connection.

Defensive consistency:
  (if some server provides some service, the service will be always
   appropriate)
is a "safety property". There are various safety properties and
defensive consistency is one of them.

Defensive correctness:
  (it is guaranteed that server provides appropriate service for
   all well behaving clients)
is a "liveness property". There are various liveness properties and
defensive correctness is one of them.

Right?

Other kinds of safety and liveness properties are discussed for example
here:
http://www.amazon.com/Concurrent-Programming-Principles-Greg-Andrews/dp/0805300864/ref=sr_1_1?ie=UTF8&s=books&qid=1246624767&sr=8-1

If there are many liveness properties, can you choose one particular
(e.g. as you suggest `Defensive correctness up to resource exhaustion'
and equate it with `liveness' ? That is why I was (I am) confused.