Skip to content

Commit

Permalink
added top level API
Browse files Browse the repository at this point in the history
  • Loading branch information
@shazqadeer
shazqadeer committed Nov 22, 2024
1 parent c9aa857 commit 7c5ff7c
Show file tree
Hide file tree
Showing 2 changed files with 53 additions and 16 deletions.
67 changes: 52 additions & 15 deletions Test/civl/large-samples/cache-coherence.bpl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ 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;
var {:layer 1,3} absMem: [MemAddr]Value;

/// Yield invariants
yield invariant {:layer 1} YieldInv#1();
Expand All @@ -76,7 +76,9 @@ function {:inline} Owns(cache: [CacheId]Cache, i: CacheId, ca: CacheAddr): bool

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 i: CacheId, ca: CacheAddr::
(var line := cache[i][ca]; (var state := dir[line->ma]->state;
line->state == Invalid() || (line->value == absMem[line->ma] && if line->state == Shared() then state is Sharers else state is Owner))));
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())));
Expand All @@ -85,7 +87,7 @@ invariant (forall ma: MemAddr:: {dir[ma]} (var state := dir[ma]->state; state is
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));
invariant (forall ma: MemAddr:: {dir[ma]} 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)));
Expand All @@ -96,6 +98,34 @@ 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_read(i: CacheId, ma: MemAddr) returns (result: Option Value)
preserves call YieldInv#2();
refines atomic action {:layer 3} _ {
if (*) {
result := None();
} else {
result := Some(absMem[ma]);
}
}
{
call result := cache_read#1(i, ma);
}

yield procedure {:layer 2} cache_write(i: CacheId, ma: MemAddr, v: Value) returns (result: Result)
preserves call YieldInv#1();
preserves call YieldInv#2();
refines atomic action {:layer 3} _ {
if (*) {
result := Fail();
} else {
result := Ok();
absMem[ma] := v;
}
}
{
call result := cache_write#1(i, ma, v);
}

yield procedure {:layer 2} cache_evict_req(i: CacheId, ca: CacheAddr) returns (result: Result)
preserves call YieldInv#1();
preserves call YieldInv#2();
Expand Down Expand Up @@ -150,14 +180,21 @@ refines atomic action {:layer 2} _ {
}

yield procedure {:layer 1} cache_write#1(i: CacheId, ma: MemAddr, v: Value) returns (result: Result)
preserves call YieldInv#1();
refines atomic action {:layer 2} _ {
var ca: CacheAddr;
var line: CacheLine;

if (*) {
result := Fail();
} else {
call result := primitive_cache_write(i, ma, v);
if (result == Ok()) {
absMem[ma] := v;
}
result := Ok();
ca := Hash(ma);
line := cache[i][ca];
assume line->state != Invalid() && line->state != Shared() && line->ma == ma && Set_Contains(cachePermissions, CachePermission(i, ca));
cache[i][ca]->value := v;
cache[i][ca]->state := Modified();
absMem[ma] := v;
}
}
{
Expand Down Expand Up @@ -191,7 +228,7 @@ refines atomic action {:layer 2} _ {
}
}

yield procedure {:layer 1} cache_read_shd_req#1(i: CacheId, ma: MemAddr) returns (result: Result, {:linear} {:layer 1} drp: Set CachePermission)
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;
Expand All @@ -202,22 +239,22 @@ refines atomic action {:layer 2} _ {
line := cache[i][ca];
call drp := Set_MakeEmpty();
if (*) {
assume line->state == Invalid();
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)));
cache[i][ca]->ma := ma;
result := Ok();
}
}
{
call result := cache_read_shd_req#0(i, ma);
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_read_exc_req#1(i: CacheId, ma: MemAddr) returns (result: Result, {:linear} {:layer 1} drp: Set CachePermission)
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;
Expand All @@ -228,15 +265,15 @@ refines atomic action {:layer 2} _ {
line := cache[i][ca];
call drp := Set_MakeEmpty();
if (*) {
assume line->state == Invalid() || (line->ma == ma && line->state == Shared());
assume line->state == Invalid();
assume Set_Contains(cachePermissions, CachePermission(i, ca));
call drp := Set_Get(cachePermissions, MapOne(CachePermission(i, ca)));
cache[i][ca]->ma := ma;
result := Ok();
}
}
{
call result := cache_read_exc_req#0(i, ma);
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))));
Expand Down Expand Up @@ -349,7 +386,7 @@ 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)
action {:layer 1} primitive_cache_write(i: CacheId, ma: MemAddr, v: Value) returns (result: Result)
modifies cache;
{
var ca: CacheAddr;
Expand All @@ -358,7 +395,7 @@ modifies cache;
ca := Hash(ma);
line := cache[i][ca];
result := Fail();
if (line->state != Invalid() && line->state != Shared() && line->ma == ma) {
if (line->state != Invalid() && line->state != Shared() && line->ma == ma && !cacheBusy[i][ca]) {
cache[i][ca]->value := v;
cache[i][ca]->state := Modified();
result := Ok();
Expand Down
2 changes: 1 addition & 1 deletion Test/civl/large-samples/cache-coherence.bpl.expect
View file
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@

Boogie program verifier finished with 90 verified, 0 errors
Boogie program verifier finished with 94 verified, 0 errors

0 comments on commit 7c5ff7c

Please sign in to comment.