Re: CLARITY ON LINEAR TYPES IN WS-CDL (aka Proposal for issue 1003)

Hi Kohei/all,

I have a question:

In the CDL script below, which codes a very typical 'order management'
business txn, what would
be the value of the 'usage' attribute (based on your notes below)?

CDL script for 'order management' choreography:

<channelType  name="SellerChannelType"
              usage="..."
              action="request" >
   <role  type="Seller" />

   <reference>
      <token name="qname"/>
   </reference>
   <identity>
      <token name="qname"/>
   </identity>
</channelType>


<choreography>

<variableDefinitions>
   <variable   name="chSeller"
       channelType="SellerChannelType" />
</variableDefinitions>


<sequence>
  <ixn channelVar="chSeller"
       oper="CreateOrder" fromRoleType="Buyer" toRoleType="Seller"...>

  ...

  <parallel>
     <ixn channelVar="chSeller"
          oper="ChangeOrder" fromRoleType="Buyer" toRoleType="Seller" ...>

     <ixn channelVar="chSeller"
          oper="CancelOrder" fromRoleType="Buyer" toRoleType="Seller" ...>
  </parallel>

</sequence>

</choreography>



Thanks,

--
Nick

----- Original Message ----- 
From: "Kohei Honda" <kohei_honda@ntlworld.com>
To: "Steve Ross-Talbot" <steve@pi4tech.com>; "'WS-Choreography List'"
<public-ws-chor@w3.org>
Cc: "Nobuko Yoshida" <yoshida@doc.ic.ac.uk>; "Marco Carbone"
<carbonem@dcs.qmul.ac.uk>; <kohei@dcs.qmul.ac.uk>
Sent: Monday, May 09, 2005 2:53 PM
Subject: Re: CLARITY ON LINEAR TYPES IN WS-CDL (aka Proposal for issue 1003)


>
> Dear Steve,
>
> My apolopgies my replies got late. In the following we answer to the
> questions you posted.
>
> > 1. With respect to "once" what form of linearity does this align itself
> > to (i.e. is it "strong")?
>
> According to Gary's description, yes.
>
> > If it is "strong" how does this apply to an
> > interaction on a channel that is a request/response? Or can only one
> > message be sent (i.e. a request or a response but not both)? Or is it
> > irrelevant and if so why?
>
> In the current CDL, a pair of request and reply use the same channel
> (we understrand this comes from the underlying web protocol: as Gary
> and I noted several times on differnet occasions, logically speaking we
> do not have to have request/reply as such). Given this, it would be
> natural to allow a "once" channel to be used once for a request and
> once for its paired response, and no more.
>
> It is not inconsistent to restrict a "once" channel to one-way channel,
> but it is not necessary.
>
> For analysis, we can represent this in a basic version of the pi-calculus,
> such as in its asynchronous core. Then a channel x in CDL for request-
> reply would be splitted into x_req and x_rep: first a requesting party
> would ask via x_req, very probably sending x_rep as a new cahannel
> along the way. Then the replying party would reply via x_rep.
>
> So if we are to have a "once" request-reply channel in CDL, this means
> we have strongly linear x_req and x_rep, which may correspond to the
> designer's intuition.
>
> So we think allowing request-reply channels to be "once" is natural.
> A static checking of conformance to this constraint will be done using
> techniques from typed pi-calculi.
>
> > 2. With respect to "distinct" what from of linearity does this align
> > itself to (i.e. is it "persistent")?  And if so why is this so?
>
> According to Gary's description, yes. As one small clafication, of its
> initial part:
>
> > This is the default usage pattern, which allows a channel instance to
> > be used multiple times, but that only one participant is permitted to
> > act as the client role for the channel instance.
>
> The final phrase, "as the client role for the channel instance", may be
> elaborated by adding:
>
>     as an output side of the interactions for the channel instance,
similarly
>     for an input side, at each moment during interactions.
>
> I know this is implied by Gary's text, but just to be doubly sure. Note
> it is intended that there are no two concurrent threads of interactions at
> the same linear channel.
>
> Next, if your question "why" means why we consider this is good,  our
> answer is: (1) as far as we know, this is a most basic and widely used
pattern in
> various usecases; and (2) having it as an explicit mode substantially
faciliates
> static (and dynamic) CDL verification, as have been found in various typed
> pi-calculi.  It is the same as having an interface specification for an
object:
> if you try to invoke an object with a wrong method, your compiler
complains,
>
> > 3. With respect to "shared" what form of linearity does this align
> > itself to (i.e. is it "non-linear" or is it "server linearity")?
>
> We understand that, in the current CDL, it is only the output capability
of
> a channel (the capability to send along the channel) which can be passed.
> This is a very sound choice, given a channel can belong to only one role.
>
> Thus Gary's description belongs to a general class of server linearity,
where
> there is only one inputting party through a channel and there can be many
> outputting parties, as written below:
>
> > This usage pattern is the least constrained, as it enables more than
> > one participant to share a reference to the client side of a channel
> > instance.
>
> This means we can have several concurrent threads connected by "parallel",
> each with an outputting party through a single channel, belonging to a
specific
> client. In such a situation, the designer's intention would naturally be
that
> distinct threads of interactions should go as prescribed: in particular,
s/he may
> not like interactions at the same "shared" channel to interfere with each
other
> (this point may be mentioned in the spec as appropriate). Prevention of
such
> interference is one of the roles of static checking for CDL
>
> Your next question:
>
> > If it
> > is "server-linearity" this would mean that we would no longer have
> > "non-linear" channel usage. If this is the case what do we loose in
> > terms of expressibility by not being able to support "non-linear"
> > models of channels/interaction.
>
> asks if using this mode sacrifices any expressive power. As noted already,
> CDL as it is g iven considers the input capability of a channel belons to
> a unique role. This means "shared" offers a most unconstrained form of
> channel usage as far as we stick to the basic idea of CDL interactions
> (with the constraint as above noted), so its adoption results in no loss
of
> expressiveness.
>
> For completeness we note that having a completely unconstrainted form of
> channel usage (as found in the untyped pi-calculus, where many inputs and
> many outputs coincide with possible interference) is of course a possible
> design choice. Our current assessment is however this may not be a very
> good idea from both execution and static checking viewpoint, unless there
> is a clear business need for such situations.
>
> As to terminology, we find "shared" is a good term to be used for
describing
> this idea, since that is what precisely takes place --- one input channel
is
> shared by multiple output parties.
>
> * * *
>
> We hope this gives basic clarification of this issue. Nobuko and I will be
very
> happy to receive further questions on these points, given linearity will
serve as
> one of the basic elements for a wide range of static/dynamic verification
of
> CDL descriptions.
>
> Best wishes,
>
> kohei
>
>
>
>

Received on Monday, 9 May 2005 22:58:06 UTC