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

Hi Kohei,

I am sorry to insist on this but we need to get a clear answer from you so
that is properly written within the CDL spec,
since this enables implementors to deal with the issue in a standard way.

So the semantics of the usage attribute (for the various values) need to be
totally clear and unabigous.

It needs to be a yes or no on the legality for the example I presented
below, when
usage="shared".


Thanks much,

--
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: Friday, May 13, 2005 6:05 AM
Subject: Re: CLARITY ON LINEAR TYPES IN WS-CDL (aka Proposal for issue 1003)


> Hi Nick,
>
> On that point (the same op-name) what I wrote in my first reply applies:
>
> > (...) However, in this case we may consider there is interference. Or,
we may also consider there is none.
> > (...) This decision depends on (1) what we regard as interference, and
(2) how much
> > static checking you wish to do. This is a design decision, but we can
have a good behavioural basis for such decision.
>
> A question is if we feel like regarding, without any exception, having
> outputs with the same op-name
> and the same channel in two threads, as inconsistent behaviour. I feel
> this pattern may not occur too
> often: nevertheless we can think of such usecases. And we do not have to
> collectively preclude them.
>
> As in many typed programming languages, the syntax of CDL allows (apart
> from basic  consistency)
> diverse kinds of behaviours some of which you may rather wish to be
> warned whether it is meaningful/
> safe/well-behaving/... or not.   For developing good criteria for that
> and associated tools, I believe it is
> most practical if we only impose bare minimal constraints on syntax,
> incorporate as many "hooks" as
> possible, which will plausibly become useful when we develop various
> forms of static/dynamic checking.
> The latter possiblity I hope we can explore together with you and other
> WG members in coming days.
>
> Best wishes,
>
> kohei
>
> Nickolas Kavantzas wrote:
>
> >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 Tuesday, 24 May 2005 20:35:34 UTC