Fw: Question on channel passing

As discussed on Tuesday's conference call, I have clarified the situation 
regarding whether control of a passed 'output' channel should be 
relinguished, with Kohei (response attached).

Therefore I would propose that we add an additional statement to section 
2.3.4 (Channel Types) following the sentence that begins "The optional 
element passing describes the Channel Type(s) of the Channel(s) that are 
passed from one party to .....".

Something like:

"When a channel instance is passed, as an information exchange message, the 
sending party will be required to relinguish control over that channel 
instance, if it is not the participant implementing the target role 
associated with that passed channel instance. In such a situation, it will 
be invalid for the participant that has passed the channel to make use of 
that channel instance in subsequent interactions.

If the passed channel instance's target role is implemented by the 
participant that is passing the channel instance, then the participant will 
retain control over the channel, as the passed channel instance will be used 
as a callback channel to the participant that is passing the channel 
instance."


I would be happy for any suggestions on better wording for such a 
constraint. One of the problems is that CDL does not define the concepts of 
'input' and 'output' endpoints of a channel instance - and therefore the 
fact that they are dealt with differently when being passed along another 
channel instance, is not easy to describe.

Also as noted in Kohei's response, it may be interesting to make use of the 
ability to share a channel instance (in 'output' mode) between multiple 
participants - but this is not something that is immediately required in 
CDL1.

Regards
Gary


----- 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 Thursday, 2 December 2004 16:32:21 UTC