An invariant for Dragon memory system

February 5, 1982

I am writing down the invariant that is true over the entire memory system after each memory bus operation, in order to clarify the model of cache operations.  

Notation:

  Memory is a real memory represented as an array of quadwords.  
  RealAddress is an index to this array.
  VM is a virtual memory.
  VAddress converts from RealAddress to the index of VM.

Invariants:

--i) In one cache, no two cells contain the same block.
(A x: Cache)(A i,j: CacheIndex) 
  (x[i].Status#empty & x[j].Status#empty & i#j => 
    x[i].RealAddress#x[j].RealAddress)

--ii) RPDirty flags for the real memory block and all the cache cells 
--containing the same block are the same. 
(A r: RealAddress)(A x: Cache)(A i: CacheIndex)
  {x[i].Status#empty & r=x[i].RealAddress => 
    Memory[r].RPDirty=x[i].RPDirty}

--iii) If all the CEDirty flags for the cells containing the same block 
--are false, then the data must be the same as in real memory.
(A r: RealAddress)(A x: Cache)(A i: CacheIndex)
  {x[i].Status#empty & r=x[i].RealAddress & 
   (A y: Cache)(A j: CacheIndex)(r=y[j].RealAddress => ~y[j].CEDirty) => 
    Memory[r].Data=x[i].Data]}

--iv) If two caches have the same block, the Shared flags of the cache 
--cells must be the same, and they contain the same data.
(A x,y: Cache)(A i,j: CacheIndex)
  (x[i].Status#empty & y[j].Status#empty & x#y & 
   x[i].RealAddress=y[j].RealAddress =>
    x[i].Shared & y[j].Shared & 
    x[i].Data=y[j].Data)

--v) Cache, not the main memory, always contains the truth. 
(A x: Cache)(A i: CacheIndex)
  (x[i].Status#empty => VM[VAddress[x[i].RealAddress]].Data=x[i].Data)

--vi) Cache entry can be dirty only if the page is not write protected. 
(A x: Cache)(A i: CacheIndex)
  (x[i].Status#empty & x[i].CEDirty => 
    ~Memory[x[i].RealAddress].WriteProtect)(635)\f8