- From: Kohei Honda <kohei@dcs.qmul.ac.uk>
- Date: Fri, 13 May 2005 14:05:33 +0100
- 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>
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 Friday, 13 May 2005 13:05:49 UTC