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)