Re: Why COPY != SIMULATED COPY

[Jonathan S. Shapiro]

A correction is needed concerning what I wrote to Harvey. I wrote:
 
> > So I think I mis-wrote. I think we understand the semantics of
> > revocation pretty well. The problem is that the implications for
> > per-object operational semantics very easily spills over into a
> > non-local and generally undecidable computation. While it is decidable
> > in finite systems, that decision procedure requires either a "God's eye"
> > view of the system (we cannot reasonably grant such authority in
> > practice) or an inductively established constraint on future computation
> > similar to the one imposed by the EROS constructor in order to impose
> > confinement.

My statement that the set of holding processes is undecidable may be
wrong. The formal problem is structurally similar to the safety
verification proof offered by Jones, Lipton, and Snyder for the
TAKE/GRANT access model, so it *may* be decidable from a "God's eye"
perspective. It is definitely intractable in practice.

The real difficulty is that we do not have and cannot permit such a
"Gods's eye" perspective at run time, so even if it turns out that the
decision problem is decidable, it is not useful.

The practical consequences of this may be stated as follows:

  There exist a very small number of specialized REVOCABLE COPY
  idioms that (a) we understand, and (b) preserve the comprehensibility
  of computation.

  General use of REVOCABLE COPY leads directly to computation that
  we cannot reason about.

  As in the "Safety Problem", the step from comprehensible to
  incomprehensible is microscopically short, and explosively bad.

I do not suggest that in practice we will do much formal reasoning about
our systems. But we *must* be able to do informal reasoning, and the
fact that the loss of comprehensibility is explosively bad means that we
cannot do this when there is general use of REVOCABLE COPY.

shap