An invariant for Dragon memory systemFebruary 5, 1982I am writing down the invariant that is true over the entire memorysystem after each memory bus operation, in order to clarify the model ofcache 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)î ·ïbpô×ð%î ·ï_î ·ï\ðCî ·ïZŠðHî ·ïYî ·ïUýî ·ïRõð?î ·ïQqð(î ·ïOíî ·ïNið8î ·ïKa î ·ïHYð7î ·ïFÕî ·ïEQð1î ·ïCÍð&î ·ï@ÅðEî ·ï?Að)î ·ï=¼ð/î ·ï<8ð,î ·ï:´ð#î ·ï7¬ðGî ·ï6(ð>î ·ï4¤ð/î ·ï3 ð+î ·ï1œðHî ·ï0î ·ï-ðFî ·ï+Œð9î ·ï*ð!î ·ï(„ð0î ·ï'ð'î ·ï%|î ·ï#øî ·ï ïð;î ·ïkî ·ïçðFî ·ïßðGî ·ï[î ·ï×ð&î ·ïSð+ÿü · =NM,©GACHA Wÿÿj/˜‹%±ÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿdragoninvariant.bravoSuzukiFebruary 5, 1982 4:26 PM