WS-CDL Issue 1003 and channel types

  Dear Kohei/Nobuko,

  In the last Choreo conf-call we discussed in the group Issue 1003, which
  is about RELINGUISHING CONTROL OF PASSED OUTPUT CHANNELS.

  In that call, I explained the current syntax/semantics of the channel type.

    From the latest WS-CDL WD, section 2.3.4 Channel Types
    http://www.w3.org/TR/2004/WD-ws-cdl-10-20041217/#collaboratingparties_choreographydescriptionlanguagemodel_channeltypes
  The syntax of the channelType construct is:

<channelType  name="ncname"
              usage="once"|"unlimited"?
              action="request-respond"|"request"|"respond"? >
   <passing  channel="qname"
             action="request-respond"|"request"|"respond"?
             new="true"|"false"? />*
   <role  type="qname"  behavior="ncname"? />
   <reference>
      <token name="qname"/>
   </reference>
   <identity>
      <token name="qname"/>+
   </identity>?
</channelType>
And there is a paragraph that discusses the semantics regarding the usage/passing of a channel
  of a given channel type:

    One or more Channel(s) MAY be passed around from one party to another in an information exchange. A Channel Type     MAY be used to:
  a.. Restrict the number of times a Channel of this Channel Type can be used

  b.. Restrict the type of information exchange that can be performed when using a Channel of this Channel Type

  c.. Restrict the Channel Type(s) that will be passed through a Channel of this Channel Type

  d.. Enforce that a passed Channel is always distinct


I designed the channelType this way, so that:
    a) The 'usage' attribute gives you linearity if desired. 
    b) The 'new' attribute could forbid free channels to be passed.

I think that these two attributes could accomplish what Gary/Steve desire.



Best Regards,

--
Nick


----- 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
>
>