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

Hi Kohei,

My question/example was/is about two or more guys concurrently receiving
messages
from the same channel. Is this allowed or not?

Regards,

--
Nick

----- Original Message ----- 
From: "Kohei Honda" <kohei_honda@ntlworld.com>
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: Thursday, May 12, 2005 4:46 PM
Subject: 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 Friday, 13 May 2005 00:13:44 UTC