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

So, what you are saying is that the CDL example I wrote below, with
usage="shared" would be legal,
even though the proposed text is silent regarding concurrently receiving
participants.

But, if I had the same oper-name within parallel, this would be illegal.


Right?

--
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 5:43 PM
Subject: Re: CLARITY ON LINEAR TYPES IN WS-CDL (aka Proposal for issue 1003)


> Hi Nick,
>
> As I wrote, it is an implementation issue. As you know, we have a basic
law in pi-calculus:
>
>  (*)  !P = !P|!P
>
> Replication is also the standard idea in distributed systems. The
right-hand side guy would
> be receiving a series of messages concurrently: there would be a bit of
sequencing on the
> left-hand side guy. But the behaviour is the same.
>
> Usually a server may receive requests through some channel, then spawn a
thread. Further
> these requests will be buffered (assume we are using TCP). In such a case,
do you think
>
>       there are two or more guys conrurrently receiving messages
>
> or
>
>       there is only one guy who is receiving messages?
>
> My point is that, because of (*), it does not matter two messages are
concurrently received
> or not: it does however matter two messages are concurrently *processed*
or not, for the
> obvious reason.
>
> The latter bit is indeed described in your example.
>
> 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: Friday, May 13, 2005 1:13 AM
> Subject: 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
> > spect 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 01:07:59 UTC