[cap-talk] controversial article

[Toby Murray]

On Fri, 2009-07-03 at 15:29 +0200, Matej Kosik wrote:
> 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.

I think Lamport [1] is responsible for the terms "safety" and
"liveness". Roughly, a safety property asserts that something (bad) can
never happen. A liveness property asserts that something (good) must
happen.

So defensive consistency asserts that no misbehaving client can cause a
server to give incorrect service to a well behaved client. It is like a
safety property because it asserts the absence of something bad ("a
server giving incorrect service to a well behaved client as the result
of misbehaviour from some other client") ever happening.

Defensive correctness asserts that no misbehaving client can prevent a
server from giving incorrect service to a well behaved client. It is
like a liveness property because it asserts that something ("correct
service being rendered to all well behaved clients, regardless of the
actions of misbehaving clients") must happen.

However, I would conjecture that neither of these properties are
'traditional' safety or liveness properties. Each is more akin to
different information flow properties, which have long been known not to
be safety nor liveness properties. (I plan to formalise and prove all of
this in my thesis but, for now, let me just conjecture away.) 

Defensive consistency says clients can cause bad service to be rendered
to well-behaved clients. It is akin to an information flow property that
says when a Well-behaved ("Low") user of a service can detect only the
occurrence of events from the server, a Misbehaving user ("High") cannot
interfere with the Low user's view of the service. Preventing events
from occurring does not interfere with the Low user's view because it
cannot detect that this prevention has occurred. 

On the other hand, defensive correctness asserts not only defensive
consistency but that the High user cannot prevents events that would
have occurred for Low had the HIgh user not been misbehaving.

These kind of information flow properties are probably 'hypersafety'
properties though. (see
http://www.cs.cornell.edu/fbs/publications/1813-9480.pdf).

Cheers

Toby