CLARITY ON LINEAR TYPES IN WS-CDL (aka Proposal for issue 1003)

Kohei/Nobuko/Marco,

We discussed the proposal below at the last conference call and Nick, 
in particular, raised a number of concerns. These were all related to 
clarity in the use of the "once", "distinct" and "shared" attributes 
and how they relate to linearity. So the questions are as follows:

1. With respect to "once" what form of linearity does this align itself 
to (i.e. is it "strong")? 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?

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?

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")? 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.

What we need to aim for is to provide the greatest benefit from formal 
verification (i.e. model checking) which is a stated critical success 
factor for the working group. We need to do this in such a way as to 
reduce the  impact on WS-CDL. And so in order to proceed on this next 
week (Tuesday) we need to get clarification of these points. If you 
could provide the necessary clarity  (on the public email list) this 
would be very much appreciated.

Both Gary and I would be happy to talk about this in person, to 
facilitate, tomorrow when we meet. But the clarity really does need to 
come from you and/or Nobuko and/or Robin as invited experts.

Best Regards

Steve Ross-talbot



On 3 May 2005, at 16:00, Gary Brown wrote:

> Hi
>  
> This proposal slightly changes the values associated with the 
> ChannelType 'usage' attribute to enable it to support the three modes 
> of linearity previously discussed by Kohei, which also implicitly 
> defines whether channel types are relinquished when passed, and 
> therefore addresses this issue (1003).
>  
> 1) Change syntax in 2.3.4
>  
> from:
> <channelType  name="ncname"
>               usage="once"|"unlimited"?
>               action="request-respond"|"request"|"respond"? >
> to: 
>
> <channelType  name="ncname"
>               usage="once"|"distinct"|"shared"?
>               action="request-respond"|"request"|"respond"? >
>
>  
> 2) Change: 
>
>
> The OPTIONAL attribute usage is used to restrict the number of times a 
> Channel of this Channel Type can be used.
>
>  to:
>
> The OPTIONAL attribute usage is used to constrain the way in which an 
> instance of this Channel Type can be used. The values that can be used 
> for this attribute are:
>
> (1) "once"
>
> This usage pattern indicates that a choreography can make use of a 
> channel instance only once. This may be used in situations where 
> single acknowledgement or callback interaction is required.
>
> (2) "distinct" (NOTE TO GROUP: not sure of the best term for this)
>  
> 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. Therefore, if a 
> participant passes the channel instance to another participant, then 
> this constraint dictates that the original participant can no longer 
> use the channel instance, as they have relinguished control over the 
> client side of the channel instance.
>
> (3) "shared" (NOTE TO GROUP: equivalent to the current "unlimited" 
> value)
>
> 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. Therefore, if the original participant passes the channel 
> instance to another participant, both the sending and receiving 
> participants have access to the channel instance.
>  
>
>  
> NOTE: Reason for change is:
>  
> 1) To enable a choreography to indicate when a passed channel should 
> be relinquished (i.e. solves issue 1003)
>  
> 2) To provide the basis for model checking based on linearity, without 
> having to provide a detailed technical explanation within the CDL 
> specification. This more indepth discussion, with explanation of 
> linearity and the associated model checking approach, will be part of 
> a separate "supplement". The text above has been approved by Kohei and 
> Nobuko.
>  
>  
> Regards
> Gary
>  

Received on Wednesday, 4 May 2005 10:51:17 UTC