Fw: Linearity and Channel Passing.

Forwarding to the public group the email thread regarding CDL and linearity
(or absense of it) that happened
between me, Kohei, et al.

--
Nick

----- Original Message ----- 
From: "Nickolas Kavantzas" <nickolas.kavantzas@oracle.com>
To: "Gary Brown" <gary@enigmatec.net>; "Kohei Honda" <kohei@dcs.qmul.ac.uk>;
"Steve Ross-Talbot" <steve@enigmatec.net>
Cc: "Nobuko Yoshida" <yoshida@doc.ic.ac.uk>; <kohei@dcs.qmul.ac.uk>; "Marco
Carbone" <carbonem@dcs.qmul.ac.uk>
Sent: Tuesday, April 12, 2005 11:17 AM
Subject: Re: Linearity and Channel Passing.


> Hi all,
>
> For CDL as I've designed it:
>
> 1) usage="unlimited" means no linearity constraints at all. This is like
> normal pi.
>
> 2) In the case of usage="once", i had it open so one could mean different
> types of
> linearity as Kohei described below.
>
> Since, there is another CDL issue that asks for making usage an XML
element
> instead of
> an XML attribute and i have designed the CDL language/schema to allow
> extensibility one
> could add other things as well, for example usage-output=2, usage-input=1,
> etc.
>
>
> Regards,
>
> --
> Nick
>
> ----- Original Message ----- 
> From: "Gary Brown" <gary@enigmatec.net>
> To: "Kohei Honda" <kohei@dcs.qmul.ac.uk>; "Nickolas Kavantzas"
> <nickolas.kavantzas@oracle.com>; "Steve Ross-Talbot" <steve@enigmatec.net>
> Cc: "Nobuko Yoshida" <yoshida@doc.ic.ac.uk>; <kohei@dcs.qmul.ac.uk>;
"Marco
> Carbone" <carbonem@dcs.qmul.ac.uk>
> Sent: Monday, April 11, 2005 12:52 AM
> Subject: Re: Linearity and Channel Passing.
>
>
> > Hi Kohei,
> >
> > Possibly the strongly linear pattern could be employed  in the concise
CDL
> > calculus, as a way to represent the request response interaction in CDL.
> > This way it does not need to be explicit in CDL, and therefore it would
> not
> > be obvious to users- but at the same time it would still be useful for
the
> > model checking.
> >
> > Does this mean that a way to model a CDL channel, that is used
> continuously
> > to send multiple request/response interactions, would be to use a
> > persistently linear pattern to model the request channel, and strongly
> > linear pattern to model the response channels? Therefore it would mean
> that
> > the request direction of a channel would be used multiple times, while
the
> > response direction of a channel would only be used once to respond to a
> > particular request. However, even if this is the case, I think we should
> be
> > able to hide the two types of linearity in the tranformation from CDL to
> the
> > calculus representation.
> >
> > Regards
> > Gary
> >
> > ----- Original Message ----- 
> > From: "Kohei Honda" <kohei_honda@ntlworld.com>
> > To: "Gary Brown" <gary@enigmatec.net>; "Kohei Honda"
> <kohei@dcs.qmul.ac.uk>;
> > "Nickolas Kavantzas" <nickolas.kavantzas@oracle.com>; "Steve
Ross-Talbot"
> > <steve@enigmatec.net>
> > Cc: "Nobuko Yoshida" <yoshida@doc.ic.ac.uk>; <kohei@dcs.qmul.ac.uk>;
> "Marco
> > Carbone" <carbonem@dcs.qmul.ac.uk>
> > Sent: Monday, April 11, 2005 2:28 AM
> > Subject: Re: Linearity and Channel Passing.
> >
> >
> > > Hi Gary,
> > >
> > > Many thanks for your observations. I will reflect some of these points
> > > in my post. Also what you implied about replies to multi-cast is quite
> > > interesting --- Steve did mention about it, and hearing it twice makes
> > > it very clear. Typing such usage (both behaviourally and
syntactically)
> > > would be fascinating.
> > >
> > > There are many aspects in types, but one of them is they give us
> > > "hooks" using which we can do various static analysis, assuming that
> > > a given type is honest --- that a program do obey the constraint via
> > > its syntactic structure. As you wrote, the strong linearity is
something
> > > which has attracted attention among us, but other kinds of channel
> > > usage also offer such hooks.
> > >
> > > One use of strong linearity in pi-processes is when we wish to
represent
> > > request-reply using only one-way message passing --- the reply channel
> > > is usually used as a strongly linear channel (in combination with
"new"
> > > name generation). I do not know this can be potentially useful in CDL.
> > > One possible way to use this would be, for example in compilation into
> > > a terser form where we have only request, which may be easier to
> > > implement: however CDL may not be used for such purposes.
> > >
> > > Anyway, I hope we can make CDL 1.0 as robust and well-digested as
> > > possible during the remaining period (this is also a preparation for
the
> > > next stage, I believe). In particular, given its importance, I am
happy
> > > to participate in further dialogue on channel usage --- how it appears
> in
> > > real (and perhaps potential) business protocols, and how we can best
> > > articulate it.
> > >
> > > Best wishes,
> > >
> > > kohei
> > >
> > > ----- Original Message -----
> > > From: "Gary Brown" <gary@enigmatec.net>
> > > To: "Kohei Honda" <kohei@dcs.qmul.ac.uk>; "Nickolas Kavantzas"
> > > <nickolas.kavantzas@oracle.com>; "Steve Ross-Talbot"
> > > <steve@enigmatec.net>
> > > Cc: "Nobuko Yoshida" <yoshida@doc.ic.ac.uk>; <kohei@dcs.qmul.ac.uk>;
> > > "Marco Carbone" <carbonem@dcs.qmul.ac.uk>
> > > Sent: Sunday, April 10, 2005 11:38 AM
> > > Subject: Re: Linearity and Channel Passing.
> > >
> > >
> > >> Hi Kohei
> > >>
> > >> I found your description of the issues very easy to understand, and I
> do
> > >> think that LTC is and should be the primary usage pattern for CDL at
> the
> > >> current time.
> > >>
> > >> I don't believe that strong linearity, although academically
> > >> interesting/useful, adds any value to CDL as I don't believe users
will
> > >> understand it when defining business protocols. It may be possible
that
> > >> higher level tools can hide this level of detail, but then they will
> > >> probably be presenting the persistently linear style pattern to the
> user,
> > >> so
> > >> makes me wonder whether it is useful.
> > >>
> > >> The third (server linearity) pattern sounds useful in multi-cast
> > >> scenarios.
> > >> However, from my understanding of your note, this would have to be a
> > >> uni-directional channel - i.e. the exchanges on those channels would
> only
> > >> consist of requests, with no responses.
> > >>
> > >> Therefore, in the current version of CDL (where broadcast/multicast
is
> > >> not
> > >> supported/discussed), I think pattern (2) is the only one that is
> > >> relevant.
> > >> When we tackle (3), it will need to include a description of the
> > >> restrictions on the usage of that type of channel.
> > >>
> > >> Regards
> > >> Gary
> > >>
> > >> ----- Original Message -----
> > >> From: "Kohei Honda" <kohei_honda@ntlworld.com>
> > >> To: "Nickolas Kavantzas" <nickolas.kavantzas@oracle.com>; "Steve
> > >> Ross-Talbot" <steve@enigmatec.net>; "Gary Brown" <gary@enigmatec.net>
> > >> Cc: "Nobuko Yoshida" <yoshida@doc.ic.ac.uk>; <kohei@dcs.qmul.ac.uk>;
> > >> "Marco
> > >> Carbone" <carbonem@dcs.qmul.ac.uk>
> > >> Sent: Thursday, April 07, 2005 12:01 AM
> > >> Subject: Linearity and Channel Passing.
> > >>
> > >>
> > >> > Dear Nick, Steve and Gary,
> > >> >
> > >> > Here is my tentative analysis on linearity. I thank you three to
give
> > >> > me
> > >> > a chance to analyse this point, which would touche many other
aspects
> > >> > of CDL.
> > >> >
> > >> > I will be very  happy to receive your views on this. I do not post
> this
> > >> > to
> > >> > the list directly since I fear it can be a bit too technical for
all
> > >> > others  ---
> > >> > though I try to give as simple illustration as possible. At least I
> may
> > >> > have
> > >> > to add some illustration on process notation I used.
> > >> >
> > >> > Reflecting your ideas, it may be posted to the public list, since
> this
> > >> > is
> > >> > an
> > >> > interesting technical point which may deserve recording as well as
> > >> > asking
> > >> > for others' opinions.
> > >> >
> > >> > As I wrote, your views on this analysis are warmly welcome. In
> > >> > particular,
> > >> > I wonder if what I called LTC is correct or not...
> > >> >
> > >> > Best wishes,
> > >> >
> > >> > kohei
> > >> >
> > >> >
> > >>
> > >>
> > >
> >
> >
> >
>

Received on Tuesday, 3 May 2005 20:34:05 UTC