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

Hi Nick,

First of all, I make one point clear: I believe it is *not* a good idea to write about
this "interference" in the main CDL specification. The spec itself is not going to
include any technical aspects of static/dynamic checking. Therefore I suspect its
inclusion would be technically irrelevant. As I noted, anyway the current CDL
assumes there is a single role to which each channel belongs to.

Second, maybe I was slightly misleading in my previous mails, but my discussion is
exclusively about description of logical behaviour, not of its implementation. For
example, it is often the case that hundreds of servers are communicated via a single
IP address, which does not prevent us from describing it as the behaviour of a single
entity, say as google.com (or other similar services).

In the example you posted, it can be implemented by two servers, it can be
implemented by a single server, or it may be implemented by 100 servers. If a
proper interactive behaviour is realised, each case would be OK. So your
observation and mine do not contradict with each other: rather  they coexist.
I hope this point is now made clear.

For the concrete wording of the shared mode, we may replace

   ...more than one participant...

with

   ...more than one participant at one time (even if they are in different
   components of parallel composition)...

Maybe this is too detailed. Anyway the point is to make it clear that two or more guys
can concurrently send messages to the same channel.

Best wishes,

kohei

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


>
> Hi Kohei,
>
> In (2), (3) below, you are suggesting that oper-name can be used for
> determining
> if there is interference or not. But this is not clear from the text in the
> proposal for
> issue 1003 as it stands now for the channel section, since the proposal
> states that in "shared" mode
> "more than one participant can share a reference to the client side of a
> channel instance".
> In the example that I presented below, there were 2 interactions performed
> in parallel, where
> two clients were sharing the same channel instance and two servers were
> sharing the same channel
> instance but still there was not interference.
>
>
> --
> Nick
>
> ----- Original Message -----
> From: "Kohei Honda" <kohei@dcs.qmul.ac.uk>
> To: "Nickolas Kavantzas" <nickolas.kavantzas@oracle.com>
> Cc: "Steve Ross-Talbot" <steve@pi4tech.com>; "'WS-Choreography List'"
> <public-ws-chor@w3.org>; "Nobuko Yoshida" <yoshida@doc.ic.ac.uk>; "Marco
> Carbone" <carbonem@dcs.qmul.ac.uk>; "Kohei Honda" <kohei@dcs.qmul.ac.uk>
> Sent: Wednesday, May 11, 2005 3:06 AM
> Subject: Re: CLARITY ON LINEAR TYPES IN WS-CDL (aka Proposal for issue 1003)
>
>
> > Hi Nick,
> >
> > I might not have been as clear as could be in my previous reply to you, so
> I summarise the
> > main points below.
> >
> > (1) In "once", "distinct", and "shared", only the last one allows the use
> of the same channel
> > in different threads of interactions.
> >
> > (2) So, in "shared", it is possible to have interference. This can be
> resolved by operation
> > names, identities, etc. My position is guaranteeing the lack of
> non-interference  is the role of
> > static checking.
> >
> > (3) For the example you listed, it is not hard to determine it induces no
> interference (I was
> > vague about this), because of distinct operations used in the two threads.
> There can be more
> > subtle cases. However I believein most practical cases static checking can
> be done economically.
> >
> > I hope this is clearer. Your further inquiries (and more examples) are
> warmly welcome.
> >
> > Best wishes,
> >
> > kohei
> >
> >
> >
> > Nickolas Kavantzas wrote:
> >
> > >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 Thursday, 12 May 2005 23:33:21 UTC