[e-lang] Should local promises respond to __whenMoreResolved on resolution?

[Kevin Reid]

On Sep 9, 2007, at 21:44, Mark Miller wrote:
> On 9/9/07, Kevin Reid <kpreid at mac.com> wrote:
>> Additionally, it violates the expectation I had formed that for  
>> all x, x <- __whenMoreResolved(fn y { ... }), it is always the  
>> case that !(sameYet(x, y)).
>
> Just to be precise, even within a single vat, this is only the case  
> under cooperative conditions, i.e., when x does not override WMR.

Yes.

> Between vats, under cooperative conditions (all the vats obey the  
> protocol), I believe this expectation is still upheld, because by  
> then x will have become y. Can you propose a counter-example?

I think you missed the ! in my text; the expectation is *not* upheld.  
As written, it's definitely wrong; it needs to be expressed in terms  
of traversal keys. Revision:

For all properly behaving x,
   def xk := makeTraversalKey(x)
   x <- __whenMoreResolved(def _(y) {
     shouldBeTrue(xk != makeTraversalKey(y))
   })

The point at which this seems to be violated is when Alice's proxy  
for Carol's promise gets __whenMoreResolved(proxy-for-Bob) and sends  
itself to the reactor proxy.

>> My understanding had been -- and I was working on this code when I  
>> noticed this problem -- that WMR is never sent over over the wire  
>> (except for delayed redirection purposes) for a remote promise;  
>> rather, reactors are buffered locally, and invoked when the  
>> redirector for the proxy is invoked.
>>
>> Am I wrong about this?
>
> Yes. The protocol you're thinking of would lose the flush property.

Not that I wish to defend it now, but I don't think so: delayed  
redirectors would take care of that.

But the protocol you describe which I think I now understand is  
better, because it doesn't need any oddball buffers.

> If we're in the three vat shortening case previously described, the  
> proxy responds directly to the reactor. In all other cases, the WMR  
> message is sent along without buffering. But this does remind me of  
> another way in which a redirector is more that just  
> (resolver.resolve). It's also a DeadManSwitch, i.e., it overrides  
> __reactToLostClient in order to smash the resolver. Since the  
> redirector is exported when the WMR message is sent, that's all the  
> buffering we need.

Okay. I had thought that the buffering was done and is necessary to  
smash the resolvers upon termination. Using __reactToLostClient makes  
sense, and is the part I had missed.

-- 
Kevin Reid                            <http://homepage.mac.com/kpreid/>