573       // The informal arguments above can be tightened into a formal
 574       // correctness proof and it behooves us to write up such a proof,
 575       // or to use model checking to prove that there are no lingering
 576       // concerns.
 577       //
 578       // Clearly because of Case 3b one cannot bound the time for
 579       // which a card will retain what we have called a "stale" value.
 580       // However, one can obtain a Loose upper bound on the redundant
 581       // work as a result of such stale values. Note first that any
 582       // time a stale card lies in the occupied part of the space at
 583       // the start of the collection, it is scanned by younger refs
 584       // code and we can define a rank function on card values that
 585       // declines when this is so. Note also that when a card does not
 586       // lie in the occupied part of the space at the beginning of a
 587       // young collection, its rank can either decline or stay unchanged.
 588       // In this case, no extra work is done in terms of redundant
 589       // younger refs scanning of that card.
 590       // Then, the case analysis above reveals that, in the worst case,
 591       // any such stale card will be scanned unnecessarily at most twice.
 592       //
 593       // It is nonethelss advisable to try and get rid of some of this
 594       // redundant work in a subsequent (low priority) re-design of
 595       // the card-scanning code, if only to simplify the underlying
 596       // state machine analysis/proof. ysr 1/28/2002. XXX
 597       cur_entry++;
 598     }
 599   }
 600 }
 601 
 602 void CardTableRS::verify() {
 603   // At present, we only know how to verify the card table RS for
 604   // generational heaps.
 605   VerifyCTGenClosure blk(this);
 606   CollectedHeap* ch = Universe::heap();
 607 
 608   if (ch->kind() == CollectedHeap::GenCollectedHeap) {
 609     GenCollectedHeap::heap()->generation_iterate(&blk, false);
 610     _ct_bs->verify();
 611     }
 612   }
 613 

 573       // The informal arguments above can be tightened into a formal
 574       // correctness proof and it behooves us to write up such a proof,
 575       // or to use model checking to prove that there are no lingering
 576       // concerns.
 577       //
 578       // Clearly because of Case 3b one cannot bound the time for
 579       // which a card will retain what we have called a "stale" value.
 580       // However, one can obtain a Loose upper bound on the redundant
 581       // work as a result of such stale values. Note first that any
 582       // time a stale card lies in the occupied part of the space at
 583       // the start of the collection, it is scanned by younger refs
 584       // code and we can define a rank function on card values that
 585       // declines when this is so. Note also that when a card does not
 586       // lie in the occupied part of the space at the beginning of a
 587       // young collection, its rank can either decline or stay unchanged.
 588       // In this case, no extra work is done in terms of redundant
 589       // younger refs scanning of that card.
 590       // Then, the case analysis above reveals that, in the worst case,
 591       // any such stale card will be scanned unnecessarily at most twice.
 592       //
 593       // It is nonetheless advisable to try and get rid of some of this
 594       // redundant work in a subsequent (low priority) re-design of
 595       // the card-scanning code, if only to simplify the underlying
 596       // state machine analysis/proof. ysr 1/28/2002. XXX
 597       cur_entry++;
 598     }
 599   }
 600 }
 601 
 602 void CardTableRS::verify() {
 603   // At present, we only know how to verify the card table RS for
 604   // generational heaps.
 605   VerifyCTGenClosure blk(this);
 606   CollectedHeap* ch = Universe::heap();
 607 
 608   if (ch->kind() == CollectedHeap::GenCollectedHeap) {
 609     GenCollectedHeap::heap()->generation_iterate(&blk, false);
 610     _ct_bs->verify();
 611     }
 612   }
 613