[cap-talk] controversial article

[Mark Miller]

Carl, I'm cc'ing you especially regarding the question at the bottom.

On Sun, Jul 5, 2009 at 7:18 PM, Matej Kosik<kosik at fiit.stuba.sk> wrote:
>
> 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.

Ah. None of its *possible* 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.

Did you mean "defensively correct"?

By "cannot", do you mean "no matter what behavior it chooses among the
behaviors it is allowed"? Or "by inspection, we see that it won't
choose a behavior that would cause denial of service."? I mean the
first.


> You sa[y] 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>

If only clients of VGA server need be inspected in your proof, then,
by the terminology in my thesis, you have proved exactly "cooperative
correctness". If all subsystems within the overall program (universe
of discourse) need be inspected, then you have proved exactly
"conventional correctness".


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

What do you mean by "potential"?

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

In that case, I would say defensive correctness is impossible in Pict.
Pict, like most programming language, implicitly allocates for
unavoidable operations with no throttling, budgeting, or preemptive
deallocation of memory. For all such programming languages, even
cooperative correctness is impossible. Of my taxonomy, the most that
can be achieved in such languages is
1) conventional correctness
2) defensive correctness up to resource exhaustion
3) defensive consistency

None of these subsume the others.

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

Exactly.


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

Yes. See the discussion of "arbitrary behavior" that follows in section 5.5.


> 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

I think that's exactly right. I vaguely remember some early Actors
papers making a similar generalization, but I don't know where to
look. Carl?

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

    Cheers,
    --MarkM