Re: WS-CDL Issue 1003 and channel types

Usage mode of channels is one of the very good design ideas in CDL, which will
serve as a basis for various useful features of this language, from well-
structured design to safety/liveness guarantee. Prompted by Nick's inquiry,
I have prepared a brief note illustrating what is linearity in channel usage
and how they can be relevant in the context of CDL.

Many researchers, starting from Robin Milner's discussion on unique handles in
his tutorial and reaching Nobuko and others' more recent work, have studied
this notion in the general setting of the pi-calculus. While the attached note
is based on a fraction of what has been accumulated in this field, I hope that
the note can be useful for considering design choices for CDL 1.0 during the
remaining brief period for spec finalisation, especially in the context of
enhancement of its potential for safety guarantee of business protocols.

kohei

Nickolas Kavantzas wrote:
> 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:
> 
>     *
> 
>       Restrict the number of times a Channel of this Channel Type can be
>       used
> 
>     *
> 
>       Restrict the type of information exchange that can be performed
>       when using a Channel of this Channel Type
> 
>     *
> 
>       Restrict the Channel Type(s) that will be passed through a Channel
>       of this Channel Type
> 
>     *
> 
>       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 
> <mailto:kohei_honda_etc@yahoo.co.uk?Subject=Fw:%20Question%20on%20channel%20passing&In-Reply-To=%3C009501c51eaf%2445e67b50%240200a8c0@LATTITUDEGary%3E&References=%3C009501c51eaf%2445e67b50%240200a8c0@LATTITUDEGary%3E>>
> To: "Gary Brown" <gary@enigmatec.net 
> <mailto:gary@enigmatec.net?Subject=Fw:%20Question%20on%20channel%20passing&In-Reply-To=%3C009501c51eaf%2445e67b50%240200a8c0@LATTITUDEGary%3E&References=%3C009501c51eaf%2445e67b50%240200a8c0@LATTITUDEGary%3E>>; 
> "Kohei Honda" <kohei@dcs.qmul.ac.uk 
> <mailto:kohei@dcs.qmul.ac.uk?Subject=Fw:%20Question%20on%20channel%20passing&In-Reply-To=%3C009501c51eaf%2445e67b50%240200a8c0@LATTITUDEGary%3E&References=%3C009501c51eaf%2445e67b50%240200a8c0@LATTITUDEGary%3E>>
> Cc: "Nobuko Yoshida" <yoshida@doc.ic.ac.uk 
> <mailto:yoshida@doc.ic.ac.uk?Subject=Fw:%20Question%20on%20channel%20passing&In-Reply-To=%3C009501c51eaf%2445e67b50%240200a8c0@LATTITUDEGary%3E&References=%3C009501c51eaf%2445e67b50%240200a8c0@LATTITUDEGary%3E>>; 
> <steve@enigmatec.net 
> <mailto:steve@enigmatec.net?Subject=Fw:%20Question%20on%20channel%20passing&In-Reply-To=%3C009501c51eaf%2445e67b50%240200a8c0@LATTITUDEGary%3E&References=%3C009501c51eaf%2445e67b50%240200a8c0@LATTITUDEGary%3E>>
> 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
>  >
>  >

   
     Linearity and Channel Passing: basic ideas.

                Kohei Honda 

          April 7/April 15, 2005

Executive Summary: after concisely reviewing the ideas of
linearity which have arisen in the study of types for the
pi-calculus, we argue for their relevance in business 
protocols and recommend their careful incorporation into
CDL.

[1] Preamble.

The following brief note illustrates the central ideas of
linearity in communication, and relate it to possible
specifications of CDL. We shall be slightly informal when we
do not wish to be too pedantic. I sincerely thank Gary Brown
and Nickolas Kavantzas for their very useful suggestions,
inputs and clarifications.


[2] Linearity without Name Passing.

We start from the situation where we have no name passing,
which is simpler. Either with name passing or without, the
significance of these different ideas of linearity is that
they arise quite often in practice and that they allow
effective ways to guarantee various kinds of safety.

(2-1) Linearity in its most strict sense means:

  We say a channel x is strongly linear when x is used 
  precisely once for input (by one party) and precisely 
  once for output (by a different party). 

(A variant replaces "precisely once" with "at most once":
hereafter we do not be strict about this point.) So if x 
is linear, there is precisely one interaction that
takes place at x. For example, if x is linear:

   x(y).P  |    ~x<3>.Q

where P and Q do not own x --- once it is used, this channel 
is thrown away. Quite instantaneous.

(2-2) Another linearity is of the following kind:

  We say a channel x is persistently linear when x is used,
  at any one time, by a unique input (by one party) and 
  a unique output (by a different party). 

For example x is persistently linear in:

   x(y).x(z).~c<y+z>  |     ~x<1>.~x<2>

Note if a channel is strongly linear then it is persistently 
linear but the converse does not hold.  Mutual and exclusive.

(2-3) We also have the following kind of linearity:

   We say a channel x is server linear when x is used,
   at any one time, by a unique input (by one party)
   and many outputs (by different parties).

This is a typical situation where there is one resource
which can be repeatedly usable and there are many users.
For example x is server-linear in:

    x(y).x(z).x(w).P | ~x<1>  | ~x<2> | ~x<3>

where we omit the part where a server offers a service.
As in many servers, we can consider the case where a 
server can be repeatedly invoked:

    !x(y).P | ~x<1>  | ~x<2> | ~x<3>

where ! indicates repetition of behaviours.

It is also possible there is, at one time, only one output 
and many inputs. Note that, in either case, there is a 
racing condition.


[3] Linearity with Name Passing.

When we have name passing, channels can be instantiated
dynamically. The core idea of linear typing is to keep
the constraint on channel usage as in (1--3) above in 
spite of this dynamism.

(3-1) Suppose you send a channel x which is designated to 
be strongly linear. The constraint for this name passing
should be:

   If a channel is to be used as a linear output, then 
   the sender should not use it as an output. Usually
   the sender does not use it as an input either since 
   there is another party who would input at it.

Similarly when a channel is to be used as a linear input.
For example, x is strongly linear in:

    a(y).~y<1>    |      ~a<x>.P       |    x(z).Q

assuming P and Q do not use x at all. A dynamic form of
love --- at a totally unexpected place and time --- but
it is still strictly linear.
 
(3-2) Similarly suppose you send a channel x which is 
persistently linear. Then the sender should not use it 
after sending it ---  the sender should relinquish it.
Below x is persistently linear in spite of dynamic 
channel passing.

    a(y).~y<3>  |  ~x<1>.~x<2>.~a<x>.P   |  x(u).x(v).x(w).P

In this case there is some change of interacting
parties during interaction --- the interaction 
continues as if nothing had happened.

(3-3) We can see (3-1) and (3-2) are quite similar. However, 
in the server-linear case, there is difference. Consider 
a situation where, at one time, there should be a unique 
input at x but there can be many outputs at x. Since we 
*are* allowing sharing of x for output, it should be such 
that:

   If somebody uses x as an input and passes it to another,
   the same constraint as (1) and (2) apply. But when 
   you send x to be used for output, you can still continue
   to use it, since there can after all be as many outputs
   as we like.

So for example x is server linear (with a unique input and
many outputs) in:

   x(y).~a<x>  |  ~x<1>.~b<x>.~x<2>  |  a(x).x(z).x(w).P  |
   b(u).~u<3>      

since, at one time, there is always one input. Unlike (3-1)
and (3-2), where sending a specific linear channel can only
be done once, in this case sending x can also be done many
times as you like. (There are many variants such as
bounding the number of times a channel can be used.)


[4] Linearity in CDL.

For CDL, we observe:

(a) If a role has a channel which does not belong to 
    itself, then it is always used for an output. 

(b) A CDL channel may be used with the following modes:

  --- strong linearity.
  --- persistent linearity.
  --- server linearity.

  It looks many CDL usecases do not consider the case when a 
  channel is not linear in any of the above senses, but this 
  should be checked for sure. "Once" may correspond to strong 
  linearity: "unlimited" may mean server linearity. At any 
  rate, it looks to me that:

      [linearity thesis in CDL]
      In many (existing and potential) use cases, CDL 
      channels are predominantly used with persistent 
      linearity.

  We call this thesis LTC. Note LTC may or may not be true. 
  Note also LTC does *not* say all channels in business
  protocols should obey persistent linearity: it just 
  claims there are many such instances.

(c) New channel passing can be an important mode if we wish to 
  establish a private communication inside a CDL, especially
  we allow a role to spawn a new process dynamically. Thus 
  it may be better to treat "new" attribute as a separate 
  concern than linearity.

There are several merits in recording explicit linearity on
channels. First, at an informal level, it makes designers
conscious about the usage of channels, leading to richer/
better structures in specifications. Second, we can
statically check whether some spec is validated against its
linearity specification, which helps debugging. Third, just
as validation by DTD and XML Schemas leads to uniform
document processing by imposing structures, a well-typed spec
can be used for various behavioural checking.

Fortunately CDL includes mode specification for each channel,
in the attribute called "usage". I find its inclusion quite 
significant --- which can be used directly or by augmenting 
it for clarifying the linearity mode of each channel, as we 
discuss below. 


[5] Future Directions and Further Comments.

Some possible future directions are:

(R1) It may be a good idea to make clear what "linearity 
     intentions" may fit well in real use cases, in the 
     light of above three categories. In particular, if 
     LTC is true, one may consider adding this mode as a 
     usage attribute value (with some fancy name, perhaps). 

     NOTE: There is a design option if we should use 
     the same attribute or an additional one. The main
     aspect is to make it as less confusing to users 
     as possible, and cover most of the cases. This 
     needs a good thought if we are to introduce new
     modes.

(R2) If a channel to be passed is strongly/persistently linear,
     then relinquishing its usage --- either for sending 
     through it or sending it again --- is required.

(R3) If a channel to be passed is server-linear or non-linear,
     then relinquishing its usage may not be required.

There are several issues (apart from design considerations)
that we should consider.

(1) Can we statically check linear usage including 
    relinquishment?

As discussed, one significance of having linearity usage
explicitly recorded in a channel is that we can use it for
checking whether a CDL spec conforms to that pattern. I
believe we can efficiently check both:

-- Strong/persistent/server linearity, and 
-- Proper relinquishment pattern.

using various techniques for type/model checking developed so far.
Intuitively, this allows us to be sure channel usages declared in
a given Choreography spec surely follows the declared pattern.

(2) Is LTC valid? Are there other patterns of linearity
    or its relaxation?

LTC claims many usecases/business protocols for which CDL may be 
used for specification, would be largely based on persistent 
linearity in their channel usage. We wish to know: (a) if this 
is indeed true; and (b) if it is true then in what precise sense 
(e.g. is a series of communications in some Relationship performed 
using persistent linearity alone, or mixed with other modes,
including those which are not listed above?). 

* * * 

In conclusion, we believe that having carefully chosen linearity
modes as channel usage, possibly by overloading/augmenting already
existing attributes, and clarifying their meaning in the CDL
document, will be useful for CDL as a specification language. We
leave the further examination of the concrete instantiation of 
these ideas in CDL to future discussions in WG.
    
[end]