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