[cap-talk] Partial authority

[Toby Murray]

On Mon, 2007-05-07 at 17:35 +0100, David Hopwood wrote: 
> Pierre THIERRY wrote:
> > Scribit Toby Murray dies 29/04/2007 hora 14:07:
> > 
> >>ie. if we remove all of o's events from s (to produce some sequence
> >>s') and if e can't follow s', then we conclude that o causes this
> >>occurrence of e and hence, that o has the authority to cause e to
> >>occur.
> >
> > How would you characterize the following: Carol creates a wrapper object
> > that holds a send capability to Ted, and has two methods, shakeLeftHand
> > and shakeRightHand. Only if both methods are called is Ted sent a fixed
> > message. If Carol gives Alice a capability to a facet of the wrapper
> > with only the shakeLeftHand method and Bob one with only shakeRightHand,
> > has Alice or Bob authority to send the message to Ted?
> 
> The definition above says that both alice and bob [*] have (partial) authority
> to cause the message to be sent to ted. 

<snip>

> 
> However, while the definition does what we want (for most analysis purposes)
> in this case, I'm not sure that it does in all cases. Suppose that in addition,
> david has a capability to send both shakeLeftHand() and shakeRightHand() to
> carol, and that in a particular execution,
> 
> s = <david sends carol <- shakeLeftHand(), david sends carol <- shakeRightHand(),
>      alice sends carol <- shakeLeftHand(), bob sends carol <- shakeRightHand()>
> 
> e = "carol sends ted <- run()"
> 
> s'_a = <david sends carol <- shakeLeftHand(), david sends carol <- shakeRightHand(),
>         bob sends carol <- shakeRightHand()>
> s'_b = <david sends carol <- shakeLeftHand(), david sends carol <- shakeRightHand(),
>         alice sends carol <- shakeLeftHand()>
> s'_d = <alice sends carol <- shakeLeftHand(), bob sends carol <- shakeRightHand()>
> 
> Now e *can* follow s'_a, s'_b or s'_d. So we conclude, *incorrectly*, that none of
> alice, bob or david had authority to cause e.

If I understand your meaning then I disagree. I think your analysis
might be contradictory.

The above conclusion presumes that that s, s'_a, s'_b and s'_d are valid
traces of the system, if I follow you.

If we remove all "david" events from either s'_a or s'_b, then e
certainly can't follow. Hence, one cannot conclude from this example
that david does not have authority to cause e.

Similarly, if we remove all "alice" or "bob" events from s'_d, we see
that e cannot follow.

Hence, both david, alice and bob have authority to cause e.

Not that I'm saying that there aren't counter examples for which this
analysis might not work. There may well be and I'm very interested in
any discussion of the deficiencies of this sort of thing.

Cheers

Toby