Properties

Properties

• Some correctness criteria:
  • Two caches cannot be simultaneously in EXCLUSIVE for the address 0.
• AG(((cc1.block_state = EXCLUSIVE) * (cc2.block_state = EXCLUSIVE))-> ((cc1.block_address =0)*(cc1.block_address=0)))
  • The cache state stored in the directory and the cache actual state must be consistent .

Previous slide

Next slide

Back to the first slide

View Graphic Version