refactor

boogie-org · Nov 22, 2024 · c9aa857 · c9aa857
1 parent ca6094e
commit c9aa857
Showing 1 changed file with 8 additions and 8 deletions.
diff --git a/Test/civl/large-samples/cache-coherence.bpl b/Test/civl/large-samples/cache-coherence.bpl
@@ -87,6 +87,14 @@ invariant (forall ma: MemAddr:: {dir[ma]} (var state := dir[ma]->state; state is
 invariant (forall ma: MemAddr:: {dir[ma]} dir[ma]->state is Sharers ==> mem[ma] == absMem[ma]);
 invariant (forall ma: MemAddr:: dir[ma]->currRequest == NoDirRequest() ==> Set_IsSubset(WholeDirPermission(ma), dirPermissions));
 
+yield invariant {:layer 2} YieldEvict(i: CacheId, ma: MemAddr, value: Value, {:linear} drp: Set CachePermission);
+invariant Set_Contains(drp, CachePermission(i, Hash(ma)));
+invariant value == cache[i][Hash(ma)]->value;
+
+yield invariant {:layer 2} YieldRead(i: CacheId, ma: MemAddr, {:linear} drp: Set CachePermission);
+invariant Set_Contains(drp, CachePermission(i, Hash(ma)));
+invariant (var line := cache[i][Hash(ma)]; (line->state == Invalid() || line->state == Shared()) && line->ma == ma);
+
 /// Cache
 yield procedure {:layer 2} cache_evict_req(i: CacheId, ca: CacheAddr) returns (result: Result)
 preserves call YieldInv#1();
@@ -506,10 +514,6 @@ action {:layer 1,2} primitive_cache_snoop_req_shd(i: CacheId, ma: MemAddr, s: St
 }
 
 /// Directory
-yield invariant {:layer 2} YieldEvict(i: CacheId, ma: MemAddr, value: Value, {:linear} drp: Set CachePermission);
-invariant Set_Contains(drp, CachePermission(i, Hash(ma)));
-invariant value == cache[i][Hash(ma)]->value;
-
 yield procedure {:layer 2} dir_evict_req(i: CacheId, ma: MemAddr, value: Value, {:layer 1,2} {:linear_in} drp: Set CachePermission)
 preserves call YieldInv#1();
 preserves call YieldInv#2();
@@ -535,10 +539,6 @@ requires call YieldEvict(i, ma, value, drp);
   par dir_req_end(ma, dirState, dp) | YieldInv#1();
 }
 
-yield invariant {:layer 2} YieldRead(i: CacheId, ma: MemAddr, {:linear} drp: Set CachePermission);
-invariant Set_Contains(drp, CachePermission(i, Hash(ma)));
-invariant (var line := cache[i][Hash(ma)]; (line->state == Invalid() || line->state == Shared()) && line->ma == ma);
-
 yield procedure {:layer 2} dir_read_shd_req(i: CacheId, ma: MemAddr, {:layer 1,2} {:linear_in} drp: Set CachePermission)
 preserves call YieldInv#1();
 preserves call YieldInv#2();