Fw: Question on channel passing

----- Original Message ----- 
From: "Kohei Honda" <kohei_honda_etc@yahoo.co.uk>
To: "Gary Brown" <gary@enigmatec.net>; "Kohei Honda" <kohei@dcs.qmul.ac.uk>
Cc: "Nobuko Yoshida" <yoshida@doc.ic.ac.uk>; <steve@enigmatec.net>
Sent: Thursday, December 02, 2004 2:07 AM
Subject: Re: Question on channel passing


> Hi Garry,
>
> I had a chat with Nobuko just now, I can now answer to your question.
>
>> Hi Kohei,
>>
>> I raised an issue with Nick, on last nights conference call, which I 
>> believe requires input from you and Nobuko to resolve.
>
> It is our pleasure if we can be of any help.
>
>> The issue is that currently, the mechanism used for passing channels in 
>> CDL, does not define whether the sending party
> relinguishes
>> control over that channel once it has been sent. Not sure about the 
>> correct terminology, but we are specifically talking about the
>> client side of the channel (output channel?). The participant would not 
>> relinguish control over the server side of a channel
>> (input channel?) that it has created as a callback to itself.
>
> Your terminology follows the standard one. Let's call a channel is in the 
> *output mode* if a principal uses it for outputting a
> certain
> message through it. It is in the *input mode* if a principal uses it for 
> inputting a message through it. You are asking whether a
> process
> (Role) which owns a channel in the output mode should cease to own this 
> capability after sending it off by channel passing.
>
>> For example, if participant A has a channel whose target 'to' role is on 
>> participant B. Participant A then decides to pass that
>> channel to participant C, so that participant C can now talk to 
>> participant B.
>
> This is the standard scenario in "well-typed" processes.
>
>> My assumption is that participant A should no longer be able to 
>> communicate with participant B on that channel. This is based on
> my
>> understanding of how channel passing in Pi works - which may be wrong. I 
>> would also assume that if the 'one to one' nature of a
> channel
>> could not be guaranteed, then this may be an issue for model checking - 
>> which is why I think we need to clarify the semantics of
> channel
>> passing before the document goes to last call.
>
> First I show how this looks like  in pi. The pi-calculus, especially 
> untyped one, allows arbitrary behaviour. Let's see how various
> scenarios can be represented in pi.
>
> (1) Use it again. Below ~a<b> is an output of a channel b through a 
> channel b.
>         a(x).~x<1>     |     ~a<b>.~b<3>
>      This reduces to
>         ~b<1>   |  ~b<3>
>      giving rise to a race condition at b.
>
> (2) Use it again, and this time as an input.
>         a(x).~x<1>  |   ~a<b>.b(y).Q  |  b(z).R
>      note there are two inputs at b.
>
> (3) Relinquish. In P, b does not occur.
>        a(x).~x<1>       |     ~a<b>.P
>      This reduces to
>         ~b<1>  |  P
>       since P does not have b, there is only one output to b.
>
> (We can also write crazier behaviours but we omit them.)
>
> In many pi-calculus with types, especially those based on "locality", (2) 
> is not allowed. In those pi-calculi with linear typing,
> (1) and (2) are not allowed. Linearity is a very good idea, making 
> reaosning easier, as you noted.
>
> Our assessment/recommendation on this issue is as follows.
>
> * We agree with you that relinquishment of a channel after sending it out, 
> the scenario (3) above, is a good idea. This is because
>   channels in the present case bears a crucial information on interaction 
> flows --- in your words, one-to-one nature in each
>   relationship. In this case, a sending capability is transposed from one 
> relationship (session) to another relationship (session).
>
> * We however also note, for the sake of completeness, that the scenario 
> (1) is indeed useful for sharing resources (we do it
>   everyday when we send URLs in e-mails). Our assessment on this point in 
> the contest of CDL is this:
>
>    (I) Such usage inside a choreography will be rare, since we have 
> mechanisms such as web service discovery separately
>         from the standard "interactions".
>
>   (II) If we wish to be ready for such usage, one may as well have a 
> different category for a channel. We know there are
>         two categories for a channel, "at most once" and "repeated". 
> Perhaps this categorisation may not be so useful.
>         Rather we think it is good to have two kinds of channels, one 
> which is for a session, which is default; and another
>         which is for sharing. I am not sure what would be the status of 
> such channels in verification, but it can be useful.
>         Note: This categorisation can be added on the basis of what we 
> have.
>
> I hope this assessment is of some use to yo (there are several interesting 
> associated topics, but I will leave them to another
> occasion.
>
> Best wishes,
>
> kohei
>
>

Received on Tuesday, 1 March 2005 23:10:18 UTC