[cap-talk] controversial article

[Mark Miller]

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


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


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

    Cheers,
    --MarkM