Glossary FDLnotes
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Certificates' Pertinence to Objects (stipulation)

Here is a key concept used in propagation of Stale Certificates. It is based on the reference relation between objects:

An object X refers "simply" to an object Y just when X refers (perhaps indirectly) to Y via a reference path with no interior certificate references. That is, either X refers directly to Y or X refers directly to a non-certificate object Z that refers "simply" to Y.

As will be seen in Staleness (extra state), the certificates pertinent to operations involving some change to a set of objects are those that simply refer to objects in that set. Certificates are intended normally to be directly "about" the content and identity of the objects to which they simply refer, and they get marked for reconsideration as a result of changes to such content or identity.

This strategy is adopted rather than one of two more obvious ones for the following reasons. A simpler strategy would be to force reconsideration for all certificates that refer at all to the affected objects because they are, after all, about those objects and so could go wrong. However, we expect many certificate kinds to be designed to be independent of various features of the objects they refer to, for example such as what "comments" may be adorning their contents. When the reconsideration procedure stipulated for that kind of certificate is executed, it may ascertain that the referenced objects have not changed in ways it considers relevant and simply resolve the certificate by leaving it intact; then our staging strategy avoids forcing reconsideration of other certificates on account of changes to this one.

This staging strategy enables the use of certificates as buffers against certain changes to their subjects. We shall use the term "buffering certificate" to mean certificates that remain intact when reconsidered due to certain changes to the objects they simply refer to. In order to make a certificate unaffected by certain changes to objects, rather than having it simply refer to those objects, one can have it refer to such "buffering" certificates that refer to those objects; then such changes will not even induce reconsideration beyond the buffering certificates.

That expensive strategy of reconsidering all (indirectly) referring certificates would at least have been useful, and indeed is equivalent to our staging strategy when buffering certificates are not employed, since if no certificates remain intact after reconsideration then all the (indirectly) referring certificates will eventually get reconsidered (unless there is a failure earlier).

Consider another extreme strategy we have not adopted. Suppose that rather than forcing reconsideration of all simply referring certificates, we were to force reconsideration of only directly referring certificates. Under such a regime, certificates must be designed to carefully restrict their attention to those objects they directly refer to, which would fail to exploit a major convenience of our closed map design, namely allowing free and easy access to all the content one can reach from a small collection of object identifiers, i.e. allowing small expressions to refer (indirectly) to large numbers of objects. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Glossary FDLnotes