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 _______________________________________________ L4-hurd mailing list [email protected] http://lists.gnu.org/mailman/listinfo/l4-hurd
