[cap-talk] Authority vs. Information Flow
daw at cs.berkeley.edu
Sat Feb 16 16:12:24 EST 2008
Toby Murray writes:
>I think that this is too coarse grained. In my work so far, I consider
>single traces of execution rather than entire behaviour of the system.
>Now, Alice has authority to cause Bob to see the light turn on iff:
>1. There is a sequence of events in which Alice acts and Bob sees the
>light turn on (i.e. the sequence ends with the evnt "Bob sees the light
>turn on" and contains some event(s) that Alice performed.)
> \exists s . s ^ <bobSeesLight> \in traces(System)
>( ^ is contatenation, <x> is the sequence of events containing the
>single event x, traces(System) is the (prefix-closed) set containing all
>sequences of events that System can perform )
>2. When we remove Alice's actions from that sequence of events, "Bob
>sees the light turn on" does not directly follow. (i.e. without Alice
>acting -- but with NO other changes to the sequence -- Bob can't see the
>light turn on).
> s \ AliceEvents ^ <bobSeesLight> \nin traces(System)
>( s \ X is the sequence s with all events from the set X removed )
How do we know whether this is the appropriate definition of causality?
Perhaps the apparent paradox arises because the definition you are using
isn't a great one, rather than due to any inherent contradiction.
This definition of causality seems somewhat fragile, because the result
of the analysis will depend heavily upon how you define the set of events.
Suppose the trace is
(Alice tries to press the button, Dave tries to press the button,
the light turns on, Bob sees the light turn on)
Then when we delete Alice's action (the first event), Bob still sees
the light turn on. If this was how we modelled the system, we'd
conclude Alice did not cause Bob to see the light go on.
It also seems odd to remove only Alice's actions. What if some
subsequent part of the trace depended upon the presence or absence of
Alice's actions? Seems like you may need to fix up the rest of the
trace as well.
>I think it is dangerous to argue that Alice has no authority to cause
>Bob to see the light turn on here.
I guess I don't see the danger yet. Can you spell it out? What
harmful consequence might this have?
>Surely, you would agree that both of the Alice and Dave objects have the
>authority to invoke Bob's "observeLight()" method?
Why? What's wrong with saying that, if the behavior of Dave truly
is known and immutable and fixed, then (subject to that constraint)
Alice does not have authority to invoke observeLight()? It seems like
a viable position to take. Does that create some kind of absurdity?
I'd say that that your observeLight() example is not representative of
how we usually reason about systems, because it assumes that we know
somehow that Dave's behavior is fixed and immutable. In practice we will
often review the code of Alice in isolation, without looking at the code
of Dave. In that case we will conclude conservatively that Alice might
have authority to invoke observeLight(). (When looking at only part of
the system, it's typical that we can only make conservative upper bounds
on the authority that particular components might have. We might often
say "Alice has authority to invoke observeLight()" but that is really
shorthand for "Alice might have authority to invoke observeLight(),
so we'd better be prepared for the possibility that she does".)
More information about the cap-talk