Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Civl] rename procedures in cache coherence and add more comments #991

Merged
merged 1 commit into from
Nov 28, 2024
Merged

[Civl] rename procedures in cache coherence and add more comments #991

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 38 additions & 18 deletions Test/civl/large-samples/cache-coherence.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ At layer 1, cachePermissions and dirPermissions are introduced allowing dirBusy
to be hidden. At this layer, absMem is also introduced. The main purpose of this layer is to
create atomic actions with suitable mover types. Specifically, we want the following:
- Memory operations (read and write) to be both movers.
- Shared snoop request at cache to be left mover.
- Shared invalidate request at cache to be left mover.
- Response to read request at cache to be left mover.
- Initiation and conclusion of cache and directory operations to be right and left movers, respectively.

Expand Down Expand Up @@ -115,6 +115,24 @@ 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
/*
There are 5 top-level operations on the cache.
cache_read and cache_write read and write a cache entry, respectively;
they may nondeterministically choose not to do the operation.
cache_evict_req initiates eviction of a cache line.
cache_read_shd_req and cache_read_exc_req initiate bringing a memory address into the cache
in Shared and Exclusive mode, respectively.
The last three operations make asynchronous calls to corresponding operations on the directory
to achieve their goals.

To specify the protocol, we introduce absMem, a global variable capturing the logical view of
memory at layer 1.
The verification demonstrates that cache_read and cache_read do the appropriate operation
on absMem.
At layer 3, all operations other than cache_read and cache_write disappear by becoming "skip"
since all the concrete state is hidden by layer 2.
*/

yield procedure {:layer 2} cache_read(i: CacheId, ma: MemAddr) returns (result: Option Value)
preserves call YieldInv#2();
refines atomic action {:layer 3} _ {
Expand Down Expand Up @@ -188,6 +206,7 @@ refines atomic action {:layer 2} _ {
var line: CacheLine;

if (*) {
// this relaxation allows cache_invalidate_shd#1 to commute to the left of cache_read#1
result := Some(absMem[ma]);
} else if (*) {
result := None();
Expand Down Expand Up @@ -335,7 +354,7 @@ refines atomic action {:layer 2} _ {
}

/*
The left mover types of the actions cache_read_resp#1 and cache_snoop_req_shd#1 are critical
The left mover types of the actions cache_read_resp#1 and cache_invalidate_shd#1 are critical
to achieve the correct atomicity for the directory operations.
If the two invocations are hitting different caches, the argument is straightforward.
Otherwise, they are hitting the same cache and their i arguments are the same.
Expand Down Expand Up @@ -373,29 +392,30 @@ refines left action {:layer 2} _ {
call {:layer 1} Set_Put(cachePermissions, drp);
}

yield procedure {:layer 1} cache_snoop_req_shd#1(i: CacheId, ma: MemAddr, s: State, {:linear} {:layer 1} dp: Set DirPermission)
yield procedure {:layer 1} cache_invalidate_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()));
// this assertion accompanies the relaxation in cache_read#1 to allow cache_invalidate_shd#1 to commute to the left of cache_read#1
assert cache[i][ca]->value == absMem[ma];
call primitive_cache_snoop_req_shd(i, ma, s);
call primitive_cache_invalidate_shd(i, ma, s);
}
{
call cache_snoop_req_shd#0(i, ma, s);
call cache_invalidate_shd#0(i, ma, s);
}

yield procedure {:layer 1} cache_snoop_req_exc#1(i: CacheId, ma: MemAddr, s: State, {:linear} {:layer 1} dp: Set DirPermission) returns (value: Value)
yield procedure {:layer 1} cache_invalidate_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 := primitive_cache_invalidate_exc(i, ma, s);
}
{
call value := cache_snoop_req_exc#0(i, ma, s);
call value := cache_invalidate_exc#0(i, ma, s);
}

// Cache primitives
Expand Down Expand Up @@ -512,12 +532,12 @@ refines atomic action {:layer 1} _ {
cacheBusy[i][ca] := false;
}

yield procedure {:layer 0} cache_snoop_req_shd#0(i: CacheId, ma: MemAddr, s: State);
yield procedure {:layer 0} cache_invalidate_shd#0(i: CacheId, ma: MemAddr, s: State);
refines atomic action {:layer 1} _ {
call primitive_cache_snoop_req_shd(i, ma, s);
call primitive_cache_invalidate_shd(i, ma, s);
}

action {:layer 1,2} primitive_cache_snoop_req_shd(i: CacheId, ma: MemAddr, s: State)
action {:layer 1,2} primitive_cache_invalidate_shd(i: CacheId, ma: MemAddr, s: State)
{
var ca: CacheAddr;
var line: CacheLine;
Expand All @@ -530,12 +550,12 @@ action {:layer 1,2} primitive_cache_snoop_req_shd(i: CacheId, ma: MemAddr, s: St
cache[i][ca]->state := s;
}

yield procedure {:layer 0} cache_snoop_req_exc#0(i: CacheId, ma: MemAddr, s: State) returns (value: Value);
yield procedure {:layer 0} cache_invalidate_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);
call value := primitive_cache_invalidate_exc(i, ma, s);
}

action {:layer 1,2} primitive_cache_snoop_req_exc(i: CacheId, ma: MemAddr, s: State) returns (value: Value)
action {:layer 1,2} primitive_cache_invalidate_exc(i: CacheId, ma: MemAddr, s: State) returns (value: Value)
{
var ca: CacheAddr;
var line: CacheLine;
Expand All @@ -559,7 +579,7 @@ requires call YieldEvict(i, ma, value, drp);
var {:linear} {:layer 1,2} dp: Set DirPermission;

par dirState, dp := dir_req_begin(ma) | YieldInv#1();
// do not change dirState in case this is a stale evict request due to a race condition with a snoop
// do not change dirState in case this is a stale evict request due to a race condition with an invalidate
if (dirState == Owner(i)) {
par write_mem(ma, value, dp) | YieldInv#1();
dirState := Sharers(Set_Empty());
Expand All @@ -584,7 +604,7 @@ requires call YieldRead(i, ma, drp);

par dirState, dp := dir_req_begin(ma) | YieldInv#1();
if (dirState is Owner) {
par value := cache_snoop_req_exc#1(dirState->i, ma, Shared(), dp) | YieldInv#1();
par value := cache_invalidate_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();
Expand All @@ -610,7 +630,7 @@ requires call YieldRead(i, ma, drp);

par dirState, dp := dir_req_begin(ma) | YieldInv#1();
if (dirState is Owner) {
par value := cache_snoop_req_exc#1(dirState->i, ma, Invalid(), dp) | YieldInv#1();
par value := cache_invalidate_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);
Expand All @@ -629,7 +649,7 @@ requires call YieldRead(i, ma, drp);
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 cache_invalidate_shd#1(victim, ma, Invalid(), dpOne) | YieldInv#1();
par dp := put_victim(dpOne, dp) | YieldInv#1();
}
par value := read_mem(ma, dp) | YieldInv#1();
Expand Down
Loading