Re: [friam] E-order can be optimized out of CapTP for DeepFrozen objects

"Mark S. Miller" <[email protected]> Wed, 2 Oct 2013 16:10:36 -0700
Newsgroups gmane.comp.capabilities.general,gmane.comp.lang.e.general
Message-ID <CABHxS9jNsSfcgSoM80Nt0ODgLAj6Ur1PLOGFAU29XpdS5MGzVg@mail.gmail.com>
On Wed, Oct 2, 2013 at 3:26 PM, Daira Hopwood <
davidsarah.hopwood-gM/[email protected]> wrote:

> On 02/10/13 19:35, Kevin Reid wrote:
> > A novel observation that was made at last Friam while reviewing Cap'n
> Proto. In E
> > terms:
> >
> > If an object is known to be DeepFrozen, and therefore stateless, then it
> is not
> > necessary to delay third-party messages to that object in the fashion
> required by
> > E-order, as that requirement is to prevent mis-orderings of stateful
> operations.
>
> This appears to be almost unobservable in the case where all the arguments
> to the message
> are also DeepFrozen. Only 'almost', because the target machine receives
> information
> before it could have done so in E-order, and nothing prevents the target
> machine's
> E (or similar language) implementation from retaining that information
> despite its *claim*
> that the object is DeepFrozen.
>

CapTP does not enforce that the target machine (as opposed to the target
object) not receive the message ahead of E-Order. In the <
http://erights.org/elib/distrib/captp/provideFor.html> scenario I use to
explain how CapTP implements E-Order, I illustrate exactly such a case of
early delivery, which has a pipelining advantage rarely seen in 3-machine
introduction protocols.



>
> When some arguments are not DeepFrozen, this is an observable
> specification change
> even when all machines respect their claims about DeepFrozenness: it's
> possible for
> messages to sent to other stateful objects in an order that would not be
> possible
> according to E-order.
>

Perhaps an example?


>
> I can't immediately think how this could cause harm contrary to the design
> intent
> of E-ordering, but I haven't thought very hard about it. In any case I
> think this
> ordering should be given a different name, since it's clearly
> distinguishable.
>
> It would be really nice to have a formal specification of E-order. I know
> only of
> informal descriptions.
>

If anyone here would like to take the lead on writing a paper formalizing
E-Order, I'd be happy to participate and co-author.



>
> --
> Daira Hopwood ⚥
>
>


-- 
    Cheers,
    --MarkM

_______________________________________________
cap-talk mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/cap-talk