Fwd: Co-relation on channels.

Begin forwarded message:

> From: "Kohei Honda" <kohei_honda@ntlworld.com>
> Date: 5 May 2005 01:08:51 BST
> To: "Nickolas Kavantzas" <nickolas.kavantzas@oracle.com>, "Gary Brown"  
> <gary@pi4tech.com>
> Cc: "Steve Ross-Talbot" <steve@enigmatec.net>, "Nobuko Yoshida"  
> <yoshida@doc.ic.ac.uk>, "Marco Carbone" <carbonem@dcs.qmul.ac.uk>,  
> "Kohei Honda" <kohei@dcs.qmul.ac.uk>
> Subject: Re: Co-relation on channels.
> Reply-To: "Kohei Honda" <kohei@dcs.qmul.ac.uk>
>
> Nobuko and I are happy that our note is found to be possibly useful for
> Choreo public in general. Sometimes it can be confusing when we refer
> to the pi-calculus etc., without enough elaboration.  However perhaps
> this is the time when we should accelerate our concerted efforts by
> increasing bandwidth.
>
> I note both Nobuko and I are very positive about Gary's proposal, even
> if this may not be so clear from our text. On this assumption the note  
> lists
> several points we considered may deserve discussions.  Among the five
> points given, we believe (a)(b)(e) can be easily clarified through  
> pertinent
> examples.  As to (d) we could not so far find a concrete proposal:  
> perhaps
> Nick can clarify this point. (c) may need a formal analysis.
>
> To WG members and others in this list: the co-relation is not only  
> useful for
> static/dynamic analysis, but also may be used as a basic element for
> structuring choreography description. Examples of using this notion  
> will
> serve as a precious basis upon which its design can be refined and made
> robust.
>
> kohei
>
> ----- Original Message -----
> From: "Nickolas Kavantzas" <nickolas.kavantzas@oracle.com>
> To: "Kohei Honda" <kohei@dcs.qmul.ac.uk>; "Gary Brown"  
> <gary@pi4tech.com>
> Cc: "Steve Ross-Talbot" <steve@enigmatec.net>; "Nobuko Yoshida"  
> <yoshida@doc.ic.ac.uk>; "Marco Carbone" <carbonem@dcs.qmul.ac.uk>;
> "Kohei Honda" <kohei@dcs.qmul.ac.uk>
> Sent: Wednesday, May 04, 2005 11:53 PM
> Subject: Re: Co-relation on channels.
>
>
>> Based on Steve's request that conversations with Kohei/Nobuko should  
>> be
>> visible also to the Choreo public
>> list, I think that this thread should be forwarded to the Choreo  
>> public list
>> as well and subsequently any more
>> discussions should be done there.
>>
>> --
>> Nick
>>
>> ----- Original Message -----
>> From: "Kohei Honda" <kohei@dcs.qmul.ac.uk>
>> To: "Gary Brown" <gary@pi4tech.com>
>> Cc: "Nickolas Kavantzas" <nickolas.kavantzas@oracle.com>; "Steve
>> Ross-Talbot" <steve@enigmatec.net>; "Nobuko Yoshida"  
>> <yoshida@doc.ic.ac.uk>;
>> "Marco Carbone" <carbonem@dcs.qmul.ac.uk>; "Kohei Honda"
>> <kohei@dcs.qmul.ac.uk>
>> Sent: Tuesday, May 03, 2005 6:37 AM
>> Subject: Co-relation on channels.
>>
>>
>>> Dear Gary, Nick and Steve,
>>>
>>> Nobuko and I have agreed on how we can view your co-relation
>>> proposal, on which I attach a note in this mail. I hope this
>>> note is useful for further discussions on this point.
>>>
>>> Best wishes,
>>>
>>> kohei
>>>
>>
>>
>> ---------------------------------------------------------------------- 
>> ------
>> ----
>>
>>
>>> Brief Comments on Outline Proposal for Issue 1001.
>>>
>>> Kohei Honda (Queen Mary)
>>> Nobuko Yoshida (Imperial College)
>>>
>>> (1) general.
>>>
>>> We consider it is a good idea to have an explicit declaration of
>>> a logical session. This will help static analyses of various
>>> properties including dead/livelock detections.
>>>
>>> In the pi-calculus, we only have channels, so we may use channels
>>> and their chaining to make the session explicit.
>>>
>>> This proposal identifies session information through "identity"
>>> token value associated with a channel instance.
>>>
>>> Identity can be primary/derived/association/alternate.
>>>
>>> It is considered that multiple threads of interactions using multiple
>>> instances of multiple channel types may possibly refer to the same
>>> session via these identity values.
>>>
>>> Overall we believe incorporating this notion will have positive
>>> interaction with "linearity" and other constraints.
>>>
>>> (2) concrete points.
>>>
>>> (a) We cannot see why identification of a session needs to  
>>> incorporate
>>> the ordering of tokens (the last line of the first para of "Possible
>>> Solution"). Unless necessary it may be better not to use ordering  
>>> info.
>>>
>>> (b) We cannot see the need of "alternate". This may complicate static
>>> checking unless very clearly declared that it is an alias of a  
>>> primary
>>> ID (aliases are in general troublesome). If not necessary, we hope
>>> this can be taken off.
>>>
>>> (c) We believe when a channel is passed, its associated usage value
>>> should also be passed. Channel instances are real interaction points
>>> (say URIs), while identity tokens offer corelations. As in type
>>> passing in lambda/pi-calculi, it is consistent to send this info
>>> together with a channel.  So this may be made mandatory.
>>>
>>> (d) We could not check in detail the differences between Gary's
>>> original proposal and Nick's one. This seems design issues rather
>>> than logical issues, so it would be good to decide if we need
>>> this functionality first. Then we can examine, through many
>>> examples, the best way to write them down.
>>>
>>> (e) In pi, we have new name generation to generate a session. Since
>>> the same binding mechanism does not exist in CDL, some counterpart
>>> (a notation for random ID generation as well as a way to read it
>>> from a role instance's state) may be incorporated.
>>>
>>> We are happy to have further discussions on this topic.
>>>
>>>
>>>
>>>
>>

Received on Thursday, 5 May 2005 07:24:09 UTC