- From: Kohei Honda <kohei@dcs.qmul.ac.uk>
- Date: Wed, 11 May 2005 11:06:52 +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, 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, 11 May 2005 10:07:01 UTC