From b949025e0a207c9b8187aa8c0d0d9a98be006f5d Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Thu, 21 Nov 2024 19:21:00 -0800 Subject: [PATCH] first commit --- Source/Core/BoogiePL.atg | 18 +- Source/Core/Parser.cs | 4 +- Test/civl/large-samples/coherence.bpl | 701 ++++++++++++++++++++++++++ 3 files changed, 715 insertions(+), 8 deletions(-) create mode 100644 Test/civl/large-samples/coherence.bpl diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 27f1444d5..681e0d7b7 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -1133,15 +1133,19 @@ WhileCmd "invariant" { Attribute } ( - Expression (. if (isFree) { - invariants.Add(new AssumeCmd(z, e, kv)); - } else { - invariants.Add(new AssertCmd(z, e, kv)); - } - kv = null; + Expression (. + if (isFree) { + invariants.Add(new AssumeCmd(z, e, kv)); + } else { + invariants.Add(new AssertCmd(z, e, kv)); + } + kv = null; .) | - CallCmd (. yields.Add((CallCmd)cmd); .) + CallCmd (. + yields.Add((CallCmd)cmd); + kv = null; + .) ) ";" } diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index ccb2d44ab..b06d6cc77 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -1667,7 +1667,9 @@ void WhileCmd(out WhileCmd wcmd) { } else if (la.kind == 38 || la.kind == 53 || la.kind == 71) { CallCmd(out cmd); - yields.Add((CallCmd)cmd); + yields.Add((CallCmd)cmd); + kv = null; + } else SynErr(151); Expect(10); } diff --git a/Test/civl/large-samples/coherence.bpl b/Test/civl/large-samples/coherence.bpl new file mode 100644 index 000000000..5628aebe7 --- /dev/null +++ b/Test/civl/large-samples/coherence.bpl @@ -0,0 +1,701 @@ +type MemAddr; + +type Value; + +datatype State { + Modified(), + Exclusive(), + Shared(), + Invalid() +} + +type CacheAddr; + +datatype Result { + Ok(), + Fail() +} + +datatype CacheLine { + CacheLine(ma: MemAddr, value: Value, state: State) +} + +type Cache = [CacheAddr]CacheLine; + +type CacheId; +const i0: CacheId; + +function Hash(MemAddr): CacheAddr; + +datatype DirState { + Owner(i: CacheId), + Sharers(iset: Set CacheId) +} + +datatype DirRequest { + EvictAtDir(i: CacheId), + ReadShdAtDir(i: CacheId), + ReadExcAtDir(i: CacheId), + NoDirRequest() +} + +datatype DirInfo { + DirInfo(state: DirState, currRequest: DirRequest) +} + +datatype CachePermission { + CachePermission(i: CacheId, ca: CacheAddr) +} + +datatype DirPermission { + DirPermission(i: CacheId, ma: MemAddr) +} + +function {:inline} WholeDirPermission(ma: MemAddr): Set DirPermission { + Set((lambda {:pool "DirPermission"} x: DirPermission :: x->ma == ma)) +} + +var {:layer 0,2} mem: [MemAddr]Value; +var {:layer 0,2} dir: [MemAddr]DirInfo; +var {:layer 0,2} cache: [CacheId]Cache; +var {:layer 0,1} cacheBusy: [CacheId][CacheAddr]bool; +var {:linear} {:layer 1,2} cachePermissions: Set CachePermission; +var {:linear} {:layer 1,2} dirPermissions: Set DirPermission; +var {:layer 1, 3} absMem: [MemAddr]Value; + +/// Yield invariants +yield invariant {:layer 1} YieldInv#1(); +invariant (forall i: CacheId, ca: CacheAddr:: Set_Contains(cachePermissions, CachePermission(i, ca)) || cacheBusy[i][ca]); + +function {:inline} Owns(cache: [CacheId]Cache, i: CacheId, ca: CacheAddr): bool { + cache[i][ca]->state == Exclusive() || cache[i][ca]->state == Modified() +} + +yield invariant {:layer 2} YieldInv#2(); +invariant (forall i: CacheId, ca: CacheAddr:: Hash(cache[i][ca]->ma) == ca); +invariant (forall i: CacheId, ca: CacheAddr:: (var line := cache[i][ca]; line->state == Invalid() || line->value == absMem[line->ma])); +invariant (forall ma: MemAddr:: {dir[ma]} (var state := dir[ma]->state; state is Owner ==> Owns(cache, state->i, Hash(ma)) && cache[state->i][Hash(ma)]->ma == ma)); +invariant (forall ma: MemAddr:: {dir[ma]} (var state := dir[ma]->state; state is Owner ==> + (forall i: CacheId:: cache[i][Hash(ma)]->ma == ma ==> state->i == i || cache[i][Hash(ma)]->state == Invalid()))); +invariant (forall ma: MemAddr:: {dir[ma]} (var state := dir[ma]->state; state is Sharers ==> + (forall i: CacheId:: Set_Contains(state->iset, i) ==> cache[i][Hash(ma)]->state == Shared() && cache[i][Hash(ma)]->ma == ma))); +invariant (forall ma: MemAddr:: {dir[ma]} (var state := dir[ma]->state; state is Sharers ==> + (forall i: CacheId:: cache[i][Hash(ma)]->ma == ma ==> Set_Contains(state->iset, i) || cache[i][Hash(ma)]->state == Invalid()))); +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)); + +/// Cache +yield procedure {:layer 2} cache_evict_req(i: CacheId, ca: CacheAddr) returns (result: Result) +preserves call YieldInv#1(); +preserves call YieldInv#2(); +{ + var ma: MemAddr; + var value: Value; + var {:linear} {:layer 1,2} drp: Set CachePermission; + + call result, ma, value, drp := cache_evict_req#1(i, ca); + if (result == Ok()) { + async call dir_evict_req(i, ma, value, drp); + } +} + +yield procedure {:layer 2} cache_read_exc_req(i: CacheId, ma: MemAddr) returns (result: Result) +preserves call YieldInv#1(); +preserves call YieldInv#2(); +{ + var {:linear} {:layer 1,2} drp: Set CachePermission; + + call result, drp := cache_read_exc_req#1(i, ma); + if (result == Ok()) { + async call dir_read_exc_req(i, ma, drp); + } +} + +yield procedure {:layer 2} cache_read_shd_req(i: CacheId, ma: MemAddr) returns (result: Result) +preserves call YieldInv#1(); +preserves call YieldInv#2(); +{ + var line: CacheLine; + var {:linear} {:layer 1,2} drp: Set CachePermission; + + call result, drp := cache_read_shd_req#1(i, ma); + if (result == Ok()) { + async call dir_read_shd_req(i, ma, drp); + } +} + +yield procedure {:layer 1} cache_read#1(i: CacheId, ma: MemAddr) returns (result: Option Value) +refines atomic action {:layer 2} _ { + if (*) { + result := None(); + } else if (*) { + result := Some(absMem[ma]); + } else { + call result := primitive_cache_read(i, ma); + } +} +{ + call result := cache_read#0(i, ma); +} + +yield procedure {:layer 1} cache_write#1(i: CacheId, ma: MemAddr, v: Value) returns (result: Result) +refines atomic action {:layer 2} _ { + if (*) { + result := Fail(); + } else { + call result := primitive_cache_write(i, ma, v); + if (result == Ok()) { + absMem[ma] := v; + } + } +} +{ + call result := cache_write#0(i, ma, v); + if (result == Ok()) { + call {:layer 1} absMem := Copy(absMem[ma := v]); + } +} + +yield procedure {:layer 1} cache_evict_req#1(i: CacheId, ca: CacheAddr) returns (result: Result, ma: MemAddr, value: Value, {:linear} {:layer 1} drp: Set CachePermission) +preserves call YieldInv#1(); +refines atomic action {:layer 2} _ { + var line: CacheLine; + + result := Fail(); + call drp := Set_MakeEmpty(); + if (*) { + assume Set_Contains(cachePermissions, CachePermission(i, ca)); + call drp := Set_Get(cachePermissions, MapOne(CachePermission(i, ca))); + line := cache[i][ca]; + ma := line->ma; + value := line->value; + result := Ok(); + } +} +{ + call result, ma, value := cache_evict_req#0(i, ca); + call {:layer 1} drp := Set_MakeEmpty(); + if (result == Ok()) { + call {:layer 1} drp := Set_Get(cachePermissions, MapOne(CachePermission(i, ca))); + } +} + +yield procedure {:layer 1} cache_read_shd_req#1(i: CacheId, ma: MemAddr) returns (result: Result, {:linear} {:layer 1} drp: Set CachePermission) +preserves call YieldInv#1(); +refines atomic action {:layer 2} _ { + var ca: CacheAddr; + var line: CacheLine; + + result := Fail(); + ca := Hash(ma); + line := cache[i][ca]; + call drp := Set_MakeEmpty(); + if (*) { + assume line->state == Invalid(); + assume Set_Contains(cachePermissions, CachePermission(i, ca)); + call drp := Set_Get(cachePermissions, MapOne(CachePermission(i, ca))); + result := Ok(); + } +} +{ + call result := cache_read_shd_req#0(i, ma); + call {:layer 1} drp := Set_MakeEmpty(); + if (result == Ok()) { + call {:layer 1} drp := Set_Get(cachePermissions, MapOne(CachePermission(i, Hash(ma)))); + } +} + +yield procedure {:layer 1} cache_read_exc_req#1(i: CacheId, ma: MemAddr) returns (result: Result, {:linear} {:layer 1} drp: Set CachePermission) +preserves call YieldInv#1(); +refines atomic action {:layer 2} _ { + var ca: CacheAddr; + var line: CacheLine; + + result := Fail(); + ca := Hash(ma); + line := cache[i][ca]; + call drp := Set_MakeEmpty(); + if (*) { + assume line->state == Invalid() || (line->ma == ma && line->state == Shared()); + assume Set_Contains(cachePermissions, CachePermission(i, ca)); + call drp := Set_Get(cachePermissions, MapOne(CachePermission(i, ca))); + result := Ok(); + } +} +{ + call result := cache_read_exc_req#0(i, ma); + call {:layer 1} drp := Set_MakeEmpty(); + if (result == Ok()) { + call {:layer 1} drp := Set_Get(cachePermissions, MapOne(CachePermission(i, Hash(ma)))); + } +} + +yield procedure {:layer 1} cache_nop_resp#1(i: CacheId, ma: MemAddr, {:linear_in} {:layer 1} drp: Set CachePermission, {:linear} {:layer 1} dp: Set DirPermission) +preserves call YieldInv#1(); +refines atomic action {:layer 2} _ { + assert Set_Contains(drp, CachePermission(i, Hash(ma))); + assert dp == WholeDirPermission(ma); + call Set_Put(cachePermissions, drp); +} +{ + call {:layer 1} Set_Put(cachePermissions, drp); +} + +yield procedure {:layer 1} cache_evict_resp#1(i: CacheId, ma: MemAddr, {:linear_in} {:layer 1} drp: Set CachePermission, {:linear} {:layer 1} dp: Set DirPermission) +preserves call YieldInv#1(); +refines atomic action {:layer 2} _ { + var ca: CacheAddr; + var line: CacheLine; + + ca := Hash(ma); + line := cache[i][ca]; + assert Set_Contains(drp, CachePermission(i, ca)); + assert dp == WholeDirPermission(ma); + assert line->ma == ma; + assume {:add_to_pool "DirPermission", DirPermission(i0, ma)} true; + cache[i][ca]->state := Invalid(); + call Set_Put(cachePermissions, drp); +} +{ + call cache_evict_resp#0(i, ma); + call {:layer 1} Set_Put(cachePermissions, drp); +} + +yield procedure {:layer 1} cache_read_resp#1(i: CacheId, ma: MemAddr, v: Value, s: State, {:linear_in} {:layer 1} drp: Set CachePermission, {:linear} {:layer 1} dp: Set DirPermission) +preserves call YieldInv#1(); +refines left action {:layer 2} _ { + var ca: CacheAddr; + var line: CacheLine; + + assert dp == WholeDirPermission(ma); + assert s == Shared() || s == Exclusive(); + ca := Hash(ma); + assert Set_Contains(drp, CachePermission(i, ca)); + line := cache[i][ca]; + assert line->state == Invalid() || (line->state == Shared() && line->ma == ma); + assume {:add_to_pool "DirPermission", DirPermission(i0, ma)} true; + if (line->state == Invalid()) { + cache[i][ca] := CacheLine(ma, v, s); + } else { + cache[i][ca]->state := s; + } + call Set_Put(cachePermissions, drp); +} +{ + call cache_read_resp#0(i, ma, v, s); + call {:layer 1} Set_Put(cachePermissions, drp); +} + +yield procedure {:layer 1} cache_snoop_req_exc#1(i: CacheId, ma: MemAddr, s: State, {:linear} {:layer 1} dp: Set DirPermission) returns (value: Value) +refines atomic action {:layer 2} _ { + assert dp == WholeDirPermission(ma); + assume {:add_to_pool "DirPermission", DirPermission(i0, ma)} true; + call value := primitive_cache_snoop_req_exc(i, ma, s); +} +{ + call value := cache_snoop_req_exc#0(i, ma, s); +} + +yield procedure {:layer 1} cache_snoop_req_shd#1(i: CacheId, ma: MemAddr, s: State, {:linear} {:layer 1} dp: Set DirPermission) +refines left action {:layer 2} _ { + var ca: CacheAddr; + + assert Set_Contains(dp, DirPermission(i, ma)); + assume {:add_to_pool "DirPermission", DirPermission(i, ma)} true; + ca := Hash(ma); + assert (forall j: CacheId :: (var line := cache[j][ca]; line->ma == ma ==> line->state == Invalid() || line->state == Shared())); + assert cache[i][ca]->value == absMem[ma]; + call primitive_cache_snoop_req_shd(i, ma, s); +} +{ + call cache_snoop_req_shd#0(i, ma, s); +} + +// Cache primitives +yield procedure {:layer 0} cache_read#0(i: CacheId, ma: MemAddr) returns (result: Option Value); +refines atomic action {:layer 1} _ { + call result := primitive_cache_read(i, ma); +} + +action {:layer 1, 2} primitive_cache_read(i: CacheId, ma: MemAddr) returns (result: Option Value) +{ + var ca: CacheAddr; + var line: CacheLine; + + ca := Hash(ma); + line := cache[i][ca]; + result := None(); + if (line->state != Invalid() && line->ma == ma) { + result := Some(line->value); + } +} + +yield procedure {:layer 0} cache_write#0(i: CacheId, ma: MemAddr, v: Value) returns (result: Result); +refines atomic action {:layer 1} _ { + call result := primitive_cache_write(i, ma, v); +} + +action {:layer 1,2} primitive_cache_write(i: CacheId, ma: MemAddr, v: Value) returns (result: Result) +modifies cache; +{ + var ca: CacheAddr; + var line: CacheLine; + + ca := Hash(ma); + line := cache[i][ca]; + result := Fail(); + if (line->state != Invalid() && line->state != Shared() && line->ma == ma) { + cache[i][ca]->value := v; + cache[i][ca]->state := Modified(); + result := Ok(); + } +} + +yield procedure {:layer 0} cache_evict_req#0(i: CacheId, ca: CacheAddr) returns (result: Result, ma: MemAddr, value: Value); +refines atomic action {:layer 1} _ { + call result, ma, value := primitive_cache_evict_req(i, ca); +} + +action {:layer 1} primitive_cache_evict_req(i: CacheId, ca: CacheAddr) returns (result: Result, ma: MemAddr, value: Value) +modifies cache; +{ + var line: CacheLine; + + line := cache[i][ca]; + ma := line->ma; + value := line->value; + if (line->state != Invalid()) { + call result := acquire_cache_lock(i, ca); + } else { + result := Fail(); + } +} + +yield procedure {:layer 0} cache_read_shd_req#0(i: CacheId, ma: MemAddr) returns (result: Result); +refines atomic action {:layer 1} _ { + call result := primitive_cache_read_shd_req(i, ma); +} + +action {:layer 1} primitive_cache_read_shd_req(i: CacheId, ma: MemAddr) returns (result: Result) +modifies cache; +{ + var ca: CacheAddr; + var line: CacheLine; + + ca := Hash(ma); + line := cache[i][ca]; + if (line->state == Invalid()) { + call result := acquire_cache_lock(i, ca); + } else { + result := Fail(); + } +} + +yield procedure {:layer 0} cache_read_exc_req#0(i: CacheId, ma: MemAddr) returns (result: Result); +refines atomic action {:layer 1} _ { + call result := primitive_cache_read_exc_req(i, ma); +} + +action {:layer 1} primitive_cache_read_exc_req(i: CacheId, ma: MemAddr) returns (result: Result) +{ + var ca: CacheAddr; + var line: CacheLine; + + ca := Hash(ma); + line := cache[i][ca]; + if (line->state == Invalid() || (line->ma == ma && line->state == Shared())) { + call result := acquire_cache_lock(i, ca); + } else { + result := Fail(); + } +} + +action {:layer 1} acquire_cache_lock(i: CacheId, ca: CacheAddr) returns (result: Result) +modifies cache; +{ + if (!cacheBusy[i][ca]) { + cacheBusy[i][ca] := true; + result := Ok(); + } else { + result := Fail(); + } +} + +yield procedure {:layer 0} cache_evict_resp#0(i: CacheId, ma: MemAddr); +refines atomic action {:layer 1} _ { + call primitive_cache_evict_resp(i, ma); +} + +action {:layer 1} primitive_cache_evict_resp(i: CacheId, ma: MemAddr) +{ + var ca: CacheAddr; + var line: CacheLine; + + ca := Hash(ma); + line := cache[i][ca]; + assert line->ma == ma; + cache[i][ca]->state := Invalid(); + cacheBusy[i][ca] := false; +} + +yield procedure {:layer 0} cache_read_resp#0(i: CacheId, ma: MemAddr, v: Value, s: State); +refines atomic action {:layer 1} _ { + call primitive_cache_read_resp(i, ma, v, s); +} + +action {:layer 1} primitive_cache_read_resp(i: CacheId, ma: MemAddr, v: Value, s: State) +{ + var ca: CacheAddr; + var line: CacheLine; + + assert s == Shared() || s == Exclusive(); + ca := Hash(ma); + line := cache[i][ca]; + assert line->state == Invalid() || (line->state == Shared() && line->ma == ma); + cache[i][ca] := CacheLine(ma, if line->state == Invalid() then v else line->value, s); + cacheBusy[i][ca] := false; +} + +yield procedure {:layer 0} cache_snoop_req_exc#0(i: CacheId, ma: MemAddr, s: State) returns (value: Value); +refines atomic action {:layer 1} _ { + call value := primitive_cache_snoop_req_exc(i, ma, s); +} + +action {:layer 1,2} primitive_cache_snoop_req_exc(i: CacheId, ma: MemAddr, s: State) returns (value: Value) +{ + var ca: CacheAddr; + var line: CacheLine; + + assert s == Invalid() || s == Shared(); + ca := Hash(ma); + line := cache[i][ca]; + assert line->state == Exclusive() || line->state == Modified(); + assert line->ma == ma; + value := line->value; + cache[i][ca]->state := s; +} + +yield procedure {:layer 0} cache_snoop_req_shd#0(i: CacheId, ma: MemAddr, s: State); +refines atomic action {:layer 1} _ { + call primitive_cache_snoop_req_shd(i, ma, s); +} + +action {:layer 1,2} primitive_cache_snoop_req_shd(i: CacheId, ma: MemAddr, s: State) +{ + var ca: CacheAddr; + var line: CacheLine; + + assert s == Invalid(); + ca := Hash(ma); + line := cache[i][ca]; + assert line->state == Shared(); + assert line->ma == ma; + cache[i][ca]->state := s; +} + +/// 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(); +requires call YieldEvict(i, ma, value, drp); +{ + var dirInfo: DirInfo; + var dirState: DirState; + var {:linear} {:layer 1,2} dp: Set DirPermission; + + par dirInfo, dp := dir_req_begin(ma, EvictAtDir(i)) | YieldInv#1(); + dirState := dirInfo->state; + // do not change dirState in case this is a stale evict request due to a race condition with a snoop + if (dirState == Owner(i)) { + par write_mem(ma, value, dp) | YieldInv#1(); + dirState := Sharers(Set_Empty()); + call cache_evict_resp#1(i, ma, drp, dp); + } else if (dirState is Sharers && Set_Contains(dirState->iset, i)) { + dirState := Sharers(Set_Remove(dirState->iset, i)); + call cache_evict_resp#1(i, ma, drp, dp); + } else { + call cache_nop_resp#1(i, ma, drp, dp); + } + 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(); +requires call YieldRead(i, ma, drp); +{ + var dirInfo: DirInfo; + var dirState: DirState; + var {:linear} {:layer 1,2} dp: Set DirPermission; + var value: Value; + + par dirInfo, dp := dir_req_begin(ma, ReadShdAtDir(i)) | YieldInv#1(); + dirState := dirInfo->state; + if (dirState is Owner) { + par value := cache_snoop_req_exc#1(dirState->i, ma, Shared(), dp) | YieldInv#1(); + par write_mem(ma, value, dp) | YieldInv#1(); + call cache_read_resp#1(i, ma, value, Shared(), drp, dp); + par dir_req_end(ma, Sharers(Set_Add(Set_Add(Set_Empty(), dirState->i), i)), dp) | YieldInv#1(); + } else { + par value := read_mem(ma, dp) | YieldInv#1(); + call cache_read_resp#1(i, ma, value, if dirState->iset == Set_Empty() then Exclusive() else Shared(), drp, dp); + par dir_req_end(ma, if dirState->iset == Set_Empty() then Owner(i) else Sharers(Set_Add(dirState->iset, i)), dp) | YieldInv#1(); + } +} + +yield procedure {:layer 2} dir_read_exc_req(i: CacheId, ma: MemAddr, {:layer 1,2} {:linear_in} drp: Set CachePermission) +preserves call YieldInv#1(); +preserves call YieldInv#2(); +requires call YieldRead(i, ma, drp); +{ + var dirInfo: DirInfo; + var dirState: DirState; + var value: Value; + var {:linear} {:layer 1,2} dp: Set DirPermission; + var {:linear} {:layer 1,2} dpOne: Set DirPermission; + var victims: Set CacheId; + var victim: CacheId; + var {:layer 2} cache_s: [CacheId]Cache; + + par dirInfo, dp := dir_req_begin(ma, ReadExcAtDir(i)) | YieldInv#1(); + dirState := dirInfo->state; + if (dirState is Owner) { + par value := cache_snoop_req_exc#1(dirState->i, ma, Invalid(), dp) | YieldInv#1(); + par write_mem(ma, value, dp) | YieldInv#1(); + } else { + call {:layer 2} cache_s := Copy(cache); + victims := dirState->iset; + while (victims != Set_Empty()) + invariant {:yields} {:layer 1} true; + invariant {:layer 1} call YieldInv#1(); + invariant {:layer 2} dp == WholeDirPermission(ma); + invariant {:layer 2} Set_IsSubset(victims, dirState->iset); + invariant {:layer 2} (forall i: CacheId:: Set_Contains(dirState->iset, i) || cache[i] == cache_s[i]); + invariant {:layer 2} (forall i: CacheId:: Set_Contains(dirState->iset, i) ==> + if Set_Contains(victims, i) + then cache[i] == cache_s[i] + else cache[i] == cache_s[i][Hash(ma) := CacheLine(ma, cache_s[i][Hash(ma)]->value, Invalid())]); + { + victim := Choice(victims->val); + victims := Set_Remove(victims, victim); + par dpOne, dp := get_victim(victim, ma, dp) | YieldInv#1(); + par cache_snoop_req_shd#1(victim, ma, Invalid(), dpOne) | YieldInv#1(); + par dp := put_victim(dpOne, dp) | YieldInv#1(); + } + par value := read_mem(ma, dp) | YieldInv#1(); + } + call cache_read_resp#1(i, ma, value, Exclusive(), drp, dp); + par dir_req_end(ma, Owner(i), dp) | YieldInv#1(); +} + +yield procedure {:layer 1} get_victim(victim: CacheId, ma: MemAddr, {:layer 1} {:linear_in} dp: Set DirPermission) +returns ({:linear} {:layer 1} dpOne: Set DirPermission, {:linear} {:layer 1} dp': Set DirPermission) +refines both action {:layer 2} _ { + dp' := dp; + call dpOne := Set_Get(dp', MapOne(DirPermission(victim, ma))); +} +{ + dp' := dp; + call {:layer 1} dpOne := Set_Get(dp', MapOne(DirPermission(victim, ma))); +} + +yield procedure {:layer 1} put_victim({:linear_in} {:layer 1} dpOne: Set DirPermission, {:layer 1} {:linear_in} dp: Set DirPermission) +returns ({:linear} {:layer 1} dp': Set DirPermission) +refines both action {:layer 2} _ { + dp' := dp; + call Set_Put(dp', dpOne); +} +{ + dp' := dp; + call {:layer 1} Set_Put(dp', dpOne); +} + +yield procedure {:layer 1} dir_req_begin(ma: MemAddr, dirRequest: DirRequest) returns (dirInfo: DirInfo, {:linear} {:layer 1} dp: Set DirPermission) +refines right action {:layer 2} _ { + assume {:add_to_pool "DirPermission", DirPermission(i0, ma)} true; + call dirInfo := primitive_dir_req_begin(ma, dirRequest); + call dp := Set_Get(dirPermissions, WholeDirPermission(ma)->val); +} +{ + call dirInfo := dir_req_begin#0(ma, dirRequest); + call {:layer 1} dp := Set_Get(dirPermissions, WholeDirPermission(ma)->val); +} + +yield procedure {:layer 0} dir_req_begin#0(ma: MemAddr, dirRequest: DirRequest) returns (dirInfo: DirInfo); +refines atomic action {:layer 1} _ { + call dirInfo := primitive_dir_req_begin(ma, dirRequest); +} + +action {:layer 1,2} primitive_dir_req_begin(ma: MemAddr, dirRequest: DirRequest) returns (dirInfo: DirInfo) +modifies dir; +{ + assert !(dirRequest is NoDirRequest); + assume dir[ma]->currRequest == NoDirRequest(); + dir[ma]->currRequest := dirRequest; + dirInfo := dir[ma]; +} + +yield procedure {:layer 1} dir_req_end(ma: MemAddr, dirState: DirState, {:layer 1} {:linear_in} dp: Set DirPermission) +refines left action {:layer 2} _ { + assert dp == WholeDirPermission(ma); + assume {:add_to_pool "DirPermission", DirPermission(i0, ma)} true; + call primitive_dir_req_end(ma, dirState); + call Set_Put(dirPermissions, dp); +} +{ + call dir_req_end#0(ma, dirState); + call {:layer 1} Set_Put(dirPermissions, dp); +} + +yield procedure {:layer 0} dir_req_end#0(ma: MemAddr, dirState: DirState); +refines atomic action {:layer 1} _ { + call primitive_dir_req_end(ma, dirState); +} + +action {:layer 1,2} primitive_dir_req_end(ma: MemAddr, dirState: DirState) +modifies dir; +{ + assert !(dir[ma]->currRequest is NoDirRequest); + dir[ma]->state := dirState; + dir[ma]->currRequest := NoDirRequest(); +} + +/// Memory +yield procedure {:layer 1} read_mem(ma: MemAddr, {:linear} {:layer 1} dp: Set DirPermission) returns (value: Value) +refines both action {:layer 2} _ { + assert dp == WholeDirPermission(ma); + assume {:add_to_pool "DirPermission", DirPermission(i0, ma)} true; + value := mem[ma]; +} +{ + call value := read_mem#0(ma); +} + +yield procedure {:layer 0} read_mem#0(ma: MemAddr) returns (value: Value); +refines atomic action {:layer 1} _ { + value := mem[ma]; +} + +yield procedure {:layer 1} write_mem(ma: MemAddr, value: Value, {:linear} {:layer 1} dp: Set DirPermission) +refines both action {:layer 2} _ { + assert dp == WholeDirPermission(ma); + assume {:add_to_pool "DirPermission", DirPermission(i0, ma)} true; + mem[ma] := value; +} +{ + call write_mem#0(ma, value); +} + +yield procedure {:layer 0} write_mem#0(ma: MemAddr, value: Value); +refines atomic action {:layer 1} _ { + mem[ma] := value; +} +