[cap-talk] Partial authority

[David Hopwood]

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. Let's work through it:

If s is the sequence
<alice sends carol <- shakeLeftHand(), bob sends carol <- shakeRightHand()>
and e is "carol sends ted <- run()",

then removing "alice sends carol <- shakeLeftHand()" from s to give
s'_a = <bob sends carol <- shakeRightHand()>, we see that e cannot follow s'_a

and removing "alice sends carol <- shakeLeftHand()" from s to give
s'_b = <bob sends carol <- shakeRightHand()>, we see that e cannot follow s'_b.

I.e. the definition says that both alice and bob are involved in the causal
chain that leads to run() being sent to ted.


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.

The problem here also occurs in simpler examples, e.g. if we get rid of
shakeRightHand() and bob, and program carol to send ted <- run() if it receives
just shakeLeftHand(), then we conclude incorrectly that neither alice nor david
have authority to cause e.


[*] I prefer lowercase for process names.

-- 
David Hopwood <david.hopwood at industrial-designers.co.uk> (note new address)