[E-Lang] New Page: Partially Ordered Message Delivery
Mark S. Miller
Tue, 13 Feb 2001 11:57:46 -0800
At 08:02 AM Tuesday 2/13/01, Tyler Close wrote:
>In E, a local reference is indistinguishable from a remote reference
>if you are only doing eventual sends, as Alice would be in this
>scenario. If Alice, Bob and Carol are all in the same Vat, then there
>is nothing preventing Bob from doing a synchronous invocation on the
>received Carol reference. If Bob receives the Carol reference before X
>gets to Carol, then Bob can do a synchronous invocation on pre-X
>Carol. Since Alice's references to Bob and Carol are, by definition,
>different references, there is no guarantee on the order in which the
>messages will arrive at their respective targets. The E language never
>guaranteed Alice that she was only giving Bob access to post-X Carol.
"Why build a Doomsday Machine if you're not going to tell anybody about it?"
-- Dr. Strangelove
Actually, E has guaranteed this for a long time, I just never documented
this fact, nor explained it clearly. Certainly we should still argue this
through, but the page above isn't documenting a change to the language, it's
belatedly documenting the semantics I've had in my head that I've been
implementing all these years. You question gives me the opportunity to get
more of it written down. Thanks!
Above, you ask the correct hard question: how do NEAR references, which
allow synchronous invocation, screw this up? It turns out, in only the way
documented on that page:
[after Alice eventually sends a message to Carol]
>If Alice and Carol are in the same Vat and Alice has a NEAR reference to
>Carol, Alice can still immediately call Carol, perhaps delivering a message
>before messages which were eventually sent earlier.
Although this is ugly, it doesn't violate the above guarantee.
But what about the case you ask about? Let's say that Bob and Carol are in
the same Vat, whether or not Alice is in this Vat as well. The guarantee
implies the following semantics: If message Y is delivered to Bob before
message X is delivered to Carol, then the the reference "to Carol" contained
in msg Y must be an promise for Carol, and therefore an eventual reference,
that only gets resolved after X is delivered to Carol.
There are two ways to implement an if-then specification. One of them is to
make sure the condition part never occurs. The E spec in my head doesn't
say how this if-then should be satisfied. The current E implementation
satisfies it by ensuring the condition never occurs: If Carol & Bob are in
the same Vat, then no matter where Alice is, X will be delivered to Carol
before Y is delivered to Bob. (Correct programs of course may only count on
properties of the E spec, not the stronger properties provided by the E
Further spec implied by the guarantee:
If a partition prevents X from being delivered to Carol, then if Y gets
delivered anyway, the contained reference to Carol must be or become broken.
No message sent on it (such as W) may ever be delivered.
If Bob & Carol are in the same Vat, the current implementation again
satisfies this spec the easy way. In order for a partition to prevent
delivery of X, Alice must be in a different Vat. A partition which prevents
delivery of X will also prevent delivery of Y, so we don't need to worry
about breaking the reference.
>The only way I can see to rescue this behaviour is to attach semantics
>to the Vat.
Do you agree that the above spec rescues the guarantee without attaching
extra semantics to the Vat?
>To date, you've been very careful to restrict semantics to
>the reference graph, allowing the Vat boundaries to be ignored. I
>think this approach might be more valuable than the behaviour that
>could be rescued.
Actually, there are *some* semantics related to the Vat, such as the
possibility of NEAR references only with a Vat, and the possibility of
partition only between Vats. But I'm glad you appreciate that I've kept it
down to a dull roar.
I agree that minimizing Vat semantics is the more important issue. Would
you agree that the above cake is both had and eaten?
>If this behaviour is not rescued, then it begs the question of whether
>there should be any order guarantees at all on sends. Are we sure that
>we need them? Does the chaining of the return value from one
>invocation into a parameter to a later invocation provide us with
>enough control over the order of execution? I think so. I'd be
>interested to hear from MarcS.
It's certainly worth re-examining, but first a bit of history. Actors,
Kernel Joule, and the early versions of Original-E both do as you suggest.
AFAIK, EC Habitats, the decentralized graphically based, secure social
virtual reality system remains the single biggest system ever built in the
Actors / Concurrent Logic / Joule concurrency paradigm, and therefore its
most extensive test. When we tried to build it without these ordering
guarantees, we had a hell of a time.
The ordering guarantees originated in syntactic sugar used in the Joule user
language (though I don't think they are in the on-line manual). When we
added these guarantees to Original-E and used them, suddenly a whole mess of
n-party (for n >= 3) concurrency problems went away. Unlike Joule,
Original-E and E provide the ordering guarantees primitively, rather than by
sugar, and this choice would also be worth arguing about.
In any case, I'm personally very happy with how the semantics here have
>Dropping order guarantees on sends
>creates a lot of implementation flexibility. It also blurs the line
>between what a sturdy ref is and what a "live" reference is. This
>suggests that the two could be merged, significantly reducing the
>application complexity of managing separate references to the same
I think I now understand what you've been trying to explain to me about
Droplets. Does the following E implement the semantics of a Droplets
message send? (Assume "srBob" is a SturdyRef to Bob.)
srBob liveRef <- foo(...)
It either succeeds or it doesn't, but either way, the next time someone
tries this, it also either succeeds or doesn't. No fail-stop implied.
UDP-like, rather than TCP-like.