[cap-talk] controversial article

[Matej Kosik]

Mark Miller wrote:
> 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"?

Yes. Sorry.

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

Ok. The first meaning is more useful than the second.

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

OK.

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

In that case I meant those two clients:
- ClockMorph
- GameOfLifeMorph
that in a given situation can access VGA server.

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

So this refactored variant of the definition of defensive correctness
(expressed in terms of defensive consistency and "responsiveness") may be:

  We say that a given subsystem is defensively correct if:
  - it is defensively consistent (safety property)
  - it is responsive (liveness property)

`Subsystem' may be either a server in a client-server system o a peer in
a peer-to-peer system.

  We say that a given subsystem is responsive if it is not possible
  to write a client that can force given subsystem
  to stop providing services for any well-behaving clients.

What is a "well-behaving client" is undefined but in my case (Sahara) it
may be a client that does not exceed its memory quota.

So now it is quite simple. Section 3 in
http://altair.fiit.stuba.sk/mediawiki/upload/2/2d/Sofsem2010.pdf
now contains this updated definition. This is a usable context where I
can describe what I have tried to make possible (the ability to achieve
responsiveness).