[cap-talk] controversial article

[Matej Kosik]

Mark Miller wrote:
> On Sun, Jul 5, 2009 at 8:35 AM, Matej Kosik<kosik at fiit.stuba.sk> wrote:
>>> "In order to prove that a given subsystem is defensively correct, it is
>>> in general not enough to review its own code but it may be necessary to review
>>> also client’s code."
>>>
>>> This contradicts the definition of defensive correctness, including
>>> the definition you give in the preceding paragraph.
>> I do not understand why you see a contradiction.
>>
>> In order to prove that a given subsystem is defensively correct, I would
>> (also) have to prove that none of its subsystems can disrupt services
>> (for other well-behaving clients) that this subsystem provides.
> 
> I'm confused about your use of "subsystems" in your clarification
> above,

I do not wonder. I am sorry. Let me try again:

  In order to prove that a given server is defensively correct,
  I would (also) have to prove that none of its clients can force
  it to stop providing services for other well-behaving clients.

According to the above definition, in case of this system:
http://altair.fiit.stuba.sk/mediawiki/upload/2/2f/Testclockandgameoflifemorph-kernel-structure.png
if I prove that:
- VGA is defensively consistent
- VGA has only two clients: ClockMorph and GameOfLifeMorph
  (and the set of clients does not change over time)
- ClockMorph cannot prevent VGA from serving GameOfLifeMorph
- GameOfLifeMorph cannot prevent VGA from serving ClockMorph
then according to the above definition I could conclude that VGA is
defensively consistent.

You sa that this is not defensive correctness. I have interpret previous
David Wagner's post ("To be pedantic...") that this may also be a proof
of defensive correctness of VGA server.
<QUESTION>
So I have not proved defensive correctness of VGA server? If not, what
property did I prove? (it also sounds useful even though it may be hard,
but not impossible, to prove)
</QUESTION>

I haven't proved required property for any possible client that it would
be possible to invent but I have proved it for all potential clients.

I ask because if what I have described is valid proof of defensive
correctness, then defensive correctness can be theoretically achieved
also if this system
http://altair.fiit.stuba.sk/mediawiki/upload/2/2f/Testclockandgameoflifemorph-kernel-structure.png
were implemented in Pict which does not make the proof:
- ClockMorph cannot prevent VGA from serving GameOfLifeMorph
- GameOfLifeMorph cannot prevent VGA from serving ClockMorph
particularly easy (the complexity of that proof depends on the the
number of VGA's clients and on the complexity of the code of those
clients. If the set of potential clients were infinite, given proof
would be impossible in case of Pict programming language.

> so I may have misunderstood your earlier statement.To be
> concrete:
> 
> Alice and Bob are both clients of Carol. Neither Alice nor Bob is a
> subsystem of Carol, though each may be considered a subsystem of some
> larger system.
> 
> For Carol to be defensively consistent, it must be the case that she
> will continue to provide good service to Alice, so long as Alice is
> well behaved, no matter what Bob might do. Since Carol's defensive
> correctness must be independent of what Bob might do, it must hold for
> all possible Bobs, so any analysis attempting to ascertain whether
> Carol is defensively correct need not examine Bob.

Ok. This means that defensive correctness is not provable in case of
systems written in Pict (inability to prove this useful property
provoked my attempt to reconsider and enhance the semantics of the
language to make that proof possible).

> 
> 
>> That is possible to prove, but in general (without special special help
>> of the underlying platform) I have to go through all the potential
>> clients and check (among other things) that:
>> - none of them behaves as a "cancer"
>> - none of them behaves as a "spammer"
>> In general, we are force to proceed this way.
>>
>> In a special case (if we choose the right mechanisms for interaction) we
>> can defend servers from those threats regardless of how clients behave.
> 
> If Bob acting as a spammer or cancer would prevent Carol from
> continuing to provide good service to Alice, then Carol isn't
> defensively correct. In a system where Carol cannot protect herself
> from such Bobs, i.e., all systems except for the "special case" you
> mention, defensive correctness is not possible.
> 
> 

Ok. These examples were helpful. The current definition can be
interpreted in a wrong way. In the thesis you say:

"A program P is defensively correct if it continues to provide correct
behavior to well behaved clients despite arbitrary behavior on the part
of its other clients."

I would like to define `defensive correctness' in terms of:
- defensive consistency (which is well defined in the previous text)
- responsiveness (which is not well defined but could be)
My motivation is that I see correlations:

 world of processes    <---- world of algorithms
 -----------------------------------------------
 defensive consistency <---- partial correctness
 responsiveness        <---- termination
 defensive correctness <---- total correctness

that is:
- world of processes is a generalization of world of algorithms
- defensive consistency is a generalized notion of partial correctness
- responsiveness (if we defined it properly) would be a generalized
notion of termination
- defensive correctness is a generalized notion of total correctness