[e-lang] Looser memoization and constant-folding: will this work?

[Kevin Reid]

On Jul 23, 2006, at 0:41, Mark S. Miller wrote:

> I suppose, since the E-to-CL compiler is part of the TCB and can be  
> in bed with the E-on-CL runtime in magic ways, it could run the  
> DeepFrozen-returning-DeepFrozen computation in the same vat but  
> with a budget. If the computation exceeds its budget, the E-to-CL  
> compiler could preemptively terminate it, in violation of the  
> general E model. This would be safe since a partially completed  
> DeepFrozen-returning-DeepFrozen computation cannot leave behind any  
> reachable residual side effects.
>
> Is this reasoning sound? Is it really safe to preemptively  
> terminate such
> computation?

No. Consider what happens if one of the previously-discussed  
DeepFrozen memoizers is in the process of updating its hash table,  
within the speculative execution, at the moment you interrupt it.

In general, this breaks E's plan-interference guarantees, by allowing  
another turn (or enclosing synchronous code) to execute 'within' the  
never-to-be-finished interrupted computation.

This could be made safe by requiring that all implementations of  
DeepFrozen objects (and the E compiler/interpreter implementing them,  
and so on) that use mutation of existing state must provide finite- 
time cleanup code; I think this is impractical.

Meta:

I'm not sure that the above argument is correct, but through the many  
revisions of it, I've come to the conclusion that even if it is  
possible to implement interruptible E computation, it isn't practical  
to tell whether the implementation is correct.

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