IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Stale Certificates
In Altering Certificates the notion of "stale" Certificate was introduced as a sort of database "inconsistency" induced by various operations and resolved by certificate "reconsideration" procedures. Here we elaborate on the methods for inducing and resolving staleness.
We do not consider the staleness of certificates in the current closed map to be part of the map, but rather part of the state of the Session to which the current closed map belongs. As will be explained, other data pertinent to reconsidering a stale certificate are also maintained along with the mark of staleness.
Some quick orientation:
At the level of interaction via a Session with the FDL process, current closed maps have no stale certificates; every operation on the current closed map at this level is automatically followed by reconsideration of all certificates marked stale. If an operation is attempted which induces staleness in any certificates, and those certificates are not recertified, rehabilitated or deleted, then the operation fails leaving the current closed map as it was.
There is a procedure stipulated as part of a certificate's kind for reconsidering a stale certificate of that kind, and it is the execution of this procedure that effects the recertification, rehabilitation, or deletion or the certificate.
The operations on the current closed map that can induce staleness in pertinent certificates are updating the content of an object, identifying two or more objects that were previously distinct (see Folding), stipulation of a set of objects to be "shunned" in anticipation of deletion, and direct stipulation that a certificate is to be considered stale. When one of these occurs, data which may help to rehabilitate the certificate is saved as well, such as the old content of an object that has been changed.
Not all certificates that may eventually become stale as the result of a change to the current closed map are necessarily marked stale at first; this makes it possible for some certificates to serve as buffers against various changes deemed "irrelevant" by other, more remote, certificates. When reconsidering a certificate object results in its alteration, pertinent certificates which depend on it will in turn be marked stale, thus a cascade of staleness marking is possible.
This presents the following issues:
* What are the "pertinent" certificates for reconsideration when an object is altered, multiple objects become identified, or a set of objects is to be shunned?
* When a staleness inducing operation occurs, what data are saved for pertinent certificates?
* How is a certificate's reconsideration procedure applied in order to reconsider the certificate?
See Pertinence, Extra State, and Resolving Staleness.
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html