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 00:31:06 UTC