- From: Nickolas Kavantzas <nickolas.kavantzas@oracle.com>
- Date: Tue, 24 May 2005 13:33:00 -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, 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