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 .