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

Jump to bottom

[Civl] eliminated one layer in reserve example #804

Merged
merged 1 commit into from
Oct 30, 2023
Merged

[Civl] eliminated one layer in reserve example #804

Show file tree
Hide file tree
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
104 changes: 29 additions & 75 deletions Test/civl/samples/reserve.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,9 @@ go below zero. If the decrement succeeds, then a scan of isFree is performed to
free cell. The goal of the verification is to prove that this scan will succeed. The
main challenge in the proof is to reason about cardinality of constructed sets.

The layer transformations are as follows:
1 -> 2: transform isFree array into the finite set isFreeSet enabling cardinality reasoning
2 -> 3: use cardinality reasoning to transform freeSpace into the bijection allocMap

The verification goal is discharged at layer 3.
At layer 1, isFree array is transformed into the finite set isFreeSet and the bijection
allocMap is introduced. The verification goal is discharged at layer 2 using cardinality
reasoning.
*/

datatype Bijection {
Expand All @@ -38,29 +36,27 @@ axiom 0 < memLo && memLo <= memHi;
function {:inline} memAddr(i: int) returns (bool) { memLo <= i && i < memHi }

var {:layer 0,1} isFree: [int]bool;
var {:layer 1,3} isFreeSet: Set int;
var {:layer 1,2} isFreeSet: Set int;
var {:layer 0,2} freeSpace: int;
var {:layer 2,3} allocMap: Bijection;
var {:layer 1,2} allocMap: Bijection;

yield procedure {:layer 3} Malloc({:linear "tid"} tid: Tid)
yield procedure {:layer 2} Malloc({:linear "tid"} tid: Tid)
preserves call YieldInvariant#1();
preserves call YieldInvariant#2(tid, false);
preserves call YieldInvariant#3(tid, false, memLo);
preserves call YieldInvariant#2(tid, false, memLo);
{
var i: int;
var spaceFound: bool;

call DecrementFreeSpace#2(tid);
call DecrementFreeSpace#1(tid);
i := memLo;
while (i < memHi)
invariant {:yields} true;
invariant {:layer 1, 2} memLo <= i && i <= memHi;
invariant {:layer 3} memAddr(i);
invariant {:layer 1} memLo <= i && i <= memHi;
invariant {:layer 2} memAddr(i);
invariant call YieldInvariant#1();
invariant call YieldInvariant#2(tid, true);
invariant call YieldInvariant#3(tid, true, i);
invariant call YieldInvariant#2(tid, true, i);
{
call spaceFound := AllocIfPtrFree#2(tid, i);
call spaceFound := AllocIfPtrFree#1(tid, i);
if (spaceFound)
{
return;
Expand All @@ -70,7 +66,7 @@ preserves call YieldInvariant#3(tid, false, memLo);
call Unreachable(); // verification goal
}

yield procedure {:layer 3} Collect()
yield procedure {:layer 2} Collect()
preserves call YieldInvariant#1();
{
var ptr: int;
Expand All @@ -79,11 +75,11 @@ preserves call YieldInvariant#1();
invariant {:yields} true;
invariant call YieldInvariant#1();
{
call ptr := Reclaim#2();
call ptr := Reclaim#1();
}
}

action {:layer 2,3} Alloc(tid: Tid, ptr: int)
action {:layer 1,2} Alloc(tid: Tid, ptr: int)
modifies allocMap;
{
var tid': Tid;
Expand All @@ -100,7 +96,7 @@ modifies allocMap;
allocMap := Bijection(Map_Remove(allocMap->tidToPtr, tid), Map_Remove(allocMap->ptrToTid, ptr'));
}

action {:layer 2,3} PreAlloc({:linear "tid"} tid: Tid, set: Set int)
action {:layer 1,2} PreAlloc({:linear "tid"} tid: Tid, set: Set int)
modifies allocMap;
{
var ptr: int;
Expand All @@ -109,21 +105,17 @@ modifies allocMap;
allocMap := Bijection(Map_Update(allocMap->tidToPtr, tid, ptr), Map_Update(allocMap->ptrToTid, ptr, tid));
}

atomic action {:layer 3} AtomicDecrementFreeSpace#2({:linear "tid"} tid: Tid)
modifies allocMap;
atomic action {:layer 2} AtomicDecrementFreeSpace#1({:linear "tid"} tid: Tid)
modifies freeSpace, allocMap;
{
var set: Set int;
set := Set_Difference(isFreeSet, allocMap->ptrToTid->dom);
assume set != Set_Empty();
call PreAlloc(tid, set);
assert !Map_Contains(allocMap->tidToPtr, tid);
call AtomicDecrementFreeSpace#0(tid);
call PreAlloc(tid, Set_Difference(isFreeSet, allocMap->ptrToTid->dom));
}
yield procedure {:layer 2} DecrementFreeSpace#2({:linear "tid"} tid: Tid)
refines AtomicDecrementFreeSpace#2;
yield procedure {:layer 1} DecrementFreeSpace#1({:linear "tid"} tid: Tid)
refines AtomicDecrementFreeSpace#1;
preserves call YieldInvariant#1();
requires call YieldInvariant#2(tid, false);
ensures call YieldInvariant#2(tid, true);
{
var set: Set int;
call DecrementFreeSpace#0(tid);
call PreAlloc(tid, Set_Difference(isFreeSet, allocMap->ptrToTid->dom));
}
Expand All @@ -137,44 +129,25 @@ modifies freeSpace;
yield procedure {:layer 0} DecrementFreeSpace#0({:linear "tid"} tid: Tid);
refines AtomicDecrementFreeSpace#0;

atomic action {:layer 3} AtomicAllocIfPtrFree#2({:linear "tid"} tid: Tid, ptr: int) returns (spaceFound:bool)
atomic action {:layer 2} AtomicAllocIfPtrFree#1({:linear "tid"} tid: Tid, ptr: int) returns (spaceFound:bool)
modifies isFreeSet, allocMap;
{
assert memAddr(ptr);
assert Map_Contains(allocMap->tidToPtr, tid) && ptr <= Map_At(allocMap->tidToPtr, tid);
spaceFound := Set_Contains(isFreeSet, ptr);
if (spaceFound) {
isFreeSet := Set_Remove(isFreeSet, ptr);
call Alloc(tid, ptr);
}
}
yield procedure {:layer 2} AllocIfPtrFree#2({:linear "tid"} tid: Tid, ptr: int) returns (spaceFound:bool)
refines AtomicAllocIfPtrFree#2;
preserves call YieldInvariant#1();
requires call YieldInvariant#2(tid, true);
ensures call YieldInvariant#2(tid, !spaceFound);
{
call spaceFound := AllocIfPtrFree#1(tid, ptr);
if (spaceFound) {
call Alloc(tid, ptr);
}
}

atomic action {:layer 2} AtomicAllocIfPtrFree#1({:linear "tid"} tid: Tid, ptr: int) returns (spaceFound:bool)
modifies isFreeSet;
{
assert memAddr(ptr);
spaceFound := Set_Contains(isFreeSet, ptr);
if (spaceFound) {
isFreeSet := Set_Remove(isFreeSet, ptr);
}
}
yield procedure {:layer 1} AllocIfPtrFree#1({:linear "tid"} tid: Tid, ptr: int) returns (spaceFound:bool)
refines AtomicAllocIfPtrFree#1;
preserves call YieldInvariant#1();
{
call spaceFound := AllocIfPtrFree#0(tid, ptr);
if (spaceFound) {
call IsFreeSetRemove(ptr);
call Alloc(tid, ptr);
}
}

Expand All @@ -190,19 +163,6 @@ modifies isFree;
yield procedure {:layer 0} AllocIfPtrFree#0({:linear "tid"} tid: Tid, ptr: int) returns (spaceFound:bool);
refines AtomicAllocIfPtrFree#0;

atomic action {:layer 3} AtomicReclaim#2() returns (ptr: int)
modifies isFreeSet;
{
assume memAddr(ptr) && !Set_Contains(isFreeSet, ptr);
isFreeSet := Set_Add(isFreeSet, ptr);
}
yield procedure {:layer 2} Reclaim#2() returns (ptr: int)
refines AtomicReclaim#2;
preserves call YieldInvariant#1();
{
call ptr := Reclaim#1();
}

action {:layer 1,2} IsFreeSetAdd(ptr: int)
modifies isFreeSet;
{
Expand Down Expand Up @@ -240,7 +200,7 @@ modifies freeSpace, isFree;
yield procedure {:layer 0} Reclaim#0() returns (ptr: int);
refines AtomicReclaim#0;

left action {:layer 1,3} AtomicUnreachable()
left action {:layer 1,2} AtomicUnreachable()
{
assert false;
}
Expand All @@ -250,16 +210,10 @@ refines AtomicUnreachable;
yield invariant {:layer 1} YieldInvariant#1();
invariant (forall y: int :: Set_Contains(isFreeSet, y) <==> memAddr(y) && isFree[y]);

yield invariant {:layer 2} YieldInvariant#2({:linear "tid"} tid: Tid, status: bool);
invariant Map_Contains(allocMap->tidToPtr, tid) == status;
invariant 0 <= freeSpace;
invariant freeSpace == Set_Size(Set_Difference(isFreeSet, allocMap->ptrToTid->dom));
invariant Set_IsSubset(allocMap->ptrToTid->dom, isFreeSet);
invariant BijectionInvariant(allocMap);

yield invariant {:layer 3} YieldInvariant#3({:linear "tid"} tid: Tid, status: bool, i: int);
yield invariant {:layer 2} YieldInvariant#2({:linear "tid"} tid: Tid, status: bool, i: int);
invariant Map_Contains(allocMap->tidToPtr, tid) == status;
invariant Set_IsSubset(allocMap->ptrToTid->dom, isFreeSet);
invariant freeSpace == Set_Size(Set_Difference(isFreeSet, allocMap->ptrToTid->dom));
invariant BijectionInvariant(allocMap);
invariant (forall y: int :: Set_Contains(isFreeSet, y) ==> memAddr(y));
invariant Map_Contains(allocMap->tidToPtr, tid) ==> i <= Map_At(allocMap->tidToPtr, tid);
2 changes: 1 addition & 1 deletion Test/civl/samples/reserve.bpl.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@

Boogie program verifier finished with 21 verified, 0 errors
Boogie program verifier finished with 13 verified, 0 errors
Loading