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

Hi Kohei,

Thanks for the quick answer.

One more related question: what would be your answer if the oper names
where the same in the example below?


Best 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: Tuesday, May 24, 2005 5:26 PM
Subject: Re: CLARITY ON LINEAR TYPES IN WS-CDL (aka Proposal for issue 1003)


> Hi Nick,
>
> In your example, you used different operation names, "ChangeOrder" and
> "CancelOrder", in two parallel interactions. This can be easily
syntactically
> checked to see there is no interference. Hence the answer is yes --- I
find
> no problem to have this as an instance of "shared".
>
> One note on terminology: practically "shared" is close to "unlimited" as
> you put it. One basic question is if one wishes to have a channel being
used
> for input by multiple participants. Since the current CDL says there
should
> be only one inputting party through a given channel (the case of a reply
is
> associated with its paired request), the term "shared" seems appropriate,
> since one inputting channel is indeed shared by multiple outputting
parties.
>
> Syntactically we may not be able to say more in the CDL spec. As to static
> checking, note my intention is to have constraints such that all
well-structured
> business protocols (as they are put in CDL) can eventually be covered. On
> some potentially relevant theories and their usage, I hope we can have a
> discussion in the coming F2F meeting in London.
>
> 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: Tuesday, May 24, 2005 9:33 PM
> Subject: 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 Wednesday, 25 May 2005 03:07:41 UTC