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

On Oct 2, 2013, at 19:52, Daira Hopwood <davidsarah.hopwood-gM/[email protected]> wrote:

>>> 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'm too tired right now to write code, but I can describe an example informally.
> 
> Suppose two messages X <- foo(Y, 0) and X <- foo(Y, 1) are sent in that order, where X and Y are in the same vat, X is DeepFrozen, and Y is not DeepFrozen. Also suppose that X.foo(obj, i) sends obj <- bar(i).
> 
> Then in strict E-order, X <- foo(Y, 0) and X <- foo(Y, 1) must be received in that order, and Y <- bar(0) and Y <- bar(1) must also be received in that order. But under the relaxed E-order, if I understand correctly, X <- foo(Y, 1) may be received before X <- foo(Y, 0), and so Y <- bar(1) may be received before Y <- bar(0).



[Reiterating: Please send further messages To: e-lang, not whichever list you happen to be looking at. This will help ensure the discussion does not get fragmented in case of the absence of reply-all.]


Thank you for pointing this out. This sort of compositionality property is something we I want to have been thought carefully about.

Even if we somehow treated "X <- foo(Y, 0)" like a message send to Y, that would not be sufficient due to the possible ordering of events:
  sender: X <- foo(Y, 0)
  sender: X <- foo(Y, 1)
  X: Y <- bar(1)     (this is delayed...)
  X: Y <- bar(0)     (but this is still put on Y's queue *after*)

There is no obvious narrow patch to fix this problem. So, my original claim shall be weakened, as follows:

If the receiver and arguments of a message send are known to be DeepFrozen, and therefore stateless, then it is not necessary to delay the message in the fashion required by E-order.

It is not any harder to implement: if far refs have DeepFrozen flags then we can equally well check them for the arguments too.

I observe that this is slightly weaker than the condition required to generically turn a DeepFrozen function into a memoized DeepFrozen function; the latter also requires that the return value be Data (i.e. deeply not selfish).

-- 
Kevin Reid                                  <http://switchb.org/kpreid/>