- From: Nickolas Kavantzas <nickolas.kavantzas@oracle.com>
- Date: Tue, 24 May 2005 20:06:40 -0700
- 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>
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