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 Monday, 9 May 2005 21:40:48 UTC