summaryrefslogtreecommitdiff
path: root/Test/og/multiset.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/og/multiset.bpl')
-rw-r--r--Test/og/multiset.bpl178
1 files changed, 68 insertions, 110 deletions
diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 8ee661c6..a522f304 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -20,92 +20,85 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
axiom (max > 0);
-procedure {:yields} {:phase 0} acquire(i : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
+procedure {:yields} {:phase 0} acquire(i : int, {:linear "tid"} tid: X);
ensures {:right} |{ A:
assert 0 <= i && i < max;
- assert tidIn != nil && tidIn != done;
+ assert tid != nil && tid != done;
assume lock[i] == nil;
- tidOut := tidIn;
- lock[i] := tidOut;
+ lock[i] := tid;
return true;
}|;
-procedure {:yields} {:phase 0} release(i : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
+procedure {:yields} {:phase 0} release(i : int, {:linear "tid"} tid: X);
ensures {:left} |{ A:
assert 0 <= i && i < max;
- assert lock[i] == tidIn;
- assert tidIn != nil && tidIn != done;
- tidOut := tidIn;
+ assert lock[i] == tid;
+ assert tid != nil && tid != done;
lock[i] := nil;
return true;
}|;
-procedure {:yields} {:phase 0,1} getElt(j : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, elt_j:int);
+procedure {:yields} {:phase 0,1} getElt(j : int, {:linear "tid"} tid: X) returns (elt_j:int);
ensures {:both} |{ A:
assert 0 <= j && j < max;
- assert lock[j] == tidIn;
- assert tidIn != nil && tidIn != done;
- tidOut := tidIn;
+ assert lock[j] == tid;
+ assert tid != nil && tid != done;
elt_j := elt[j];
return true;
}|;
-procedure {:yields} {:phase 0,1} setElt(j : int, x : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
+procedure {:yields} {:phase 0,1} setElt(j : int, x : int, {:linear "tid"} tid: X);
ensures {:both} |{ A:
assert x != null;
assert owner[j] == nil;
assert 0 <= j && j < max;
- assert lock[j] == tidIn;
- assert tidIn != nil && tidIn != done;
- tidOut := tidIn;
+ assert lock[j] == tid;
+ assert tid != nil && tid != done;
elt[j] := x;
- owner[j] := tidIn;
+ owner[j] := tid;
return true;
}|;
-procedure {:yields} {:phase 0} setEltToNull(j : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
+procedure {:yields} {:phase 0} setEltToNull(j : int, {:linear "tid"} tid: X);
ensures {:left} |{ A:
- assert owner[j] == tidIn;
+ assert owner[j] == tid;
assert 0 <= j && j < max;
- assert lock[j] == tidIn;
+ assert lock[j] == tid;
assert !valid[j];
- assert tidIn != nil && tidIn != done;
- tidOut := tidIn;
+ assert tid != nil && tid != done;
elt[j] := null;
owner[j] := nil;
return true;
}|;
-procedure {:yields} {:phase 0} setValid(j : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
+procedure {:yields} {:phase 0} setValid(j : int, {:linear "tid"} tid: X);
ensures {:both} |{ A:
assert 0 <= j && j < max;
- assert lock[j] == tidIn;
- assert tidIn != nil && tidIn != done;
- assert owner[j] == tidIn;
- tidOut := tidIn;
+ assert lock[j] == tid;
+ assert tid != nil && tid != done;
+ assert owner[j] == tid;
valid[j] := true;
owner[j] := done;
return true;
}|;
-procedure {:yields} {:phase 0} isEltThereAndValid(j : int, x : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, fnd:bool);
+procedure {:yields} {:phase 0} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool);
ensures {:both} |{ A:
assert 0 <= j && j < max;
- assert lock[j] == tidIn;
- assert tidIn != nil && tidIn != done;
- tidOut := tidIn;
+ assert lock[j] == tid;
+ assert tid != nil && tid != done;
fnd := (elt[j] == x) && valid[j];
return true;
}|;
-procedure {:yields} {:phase 1} FindSlot(x : int, {:linear_in "tid"} tidIn: X) returns (r : int, {:linear "tid"} tidOut: X)
-requires {:phase 1} Inv(valid, elt, owner);
+procedure {:yields} {:phase 1} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int)
+requires {:phase 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done;
ensures {:phase 1} Inv(valid, elt, owner);
-ensures {:right} |{ A: assert tidIn != nil && tidIn != done;
+ensures {:right} |{ A: assert tid != nil && tid != done;
assert x != null;
goto B, C;
B: assume (0 <= r && r < max);
@@ -113,112 +106,91 @@ ensures {:right} |{ A: assert tidIn != nil && tidIn != done;
assume owner[r] == nil;
assume !valid[r];
elt[r] := x;
- owner[r] := tidIn;
- tidOut := tidIn;
+ owner[r] := tid;
return true;
- C: assume (r == -1); tidOut := tidIn; return true;
+ C: assume (r == -1); return true;
}|;
{
var j : int;
var elt_j : int;
- var {:linear "tid"} tidTmp: X;
par Yield1();
j := 0;
- tidTmp := tidIn;
-
-
while(j < max)
- invariant {:phase 1} tidTmp != nil && tidTmp != done;
- invariant {:phase 1} tidTmp == tidIn;
invariant {:phase 1} Inv(valid, elt, owner);
invariant {:phase 1} 0 <= j;
{
- call tidTmp := acquire(j, tidTmp);
- call tidTmp, elt_j := getElt(j, tidTmp);
+ call acquire(j, tid);
+ call elt_j := getElt(j, tid);
if(elt_j == null)
{
- call tidTmp := setElt(j, x, tidTmp);
- call tidTmp := release(j, tidTmp);
+ call setElt(j, x, tid);
+ call release(j, tid);
r := j;
- tidOut := tidTmp;
par Yield1();
return;
}
- call tidTmp := release(j,tidTmp);
+ call release(j,tid);
par Yield1();
j := j + 1;
}
r := -1;
- tidOut := tidTmp;
par Yield1();
return;
}
-procedure {:yields} {:phase 2} Insert(x : int, {:linear_in "tid"} tidIn: X) returns (result : bool, {:linear "tid"} tidOut: X)
-requires {:phase 1} Inv(valid, elt, owner);
-requires {:phase 2} Inv(valid, elt, owner);
+procedure {:yields} {:phase 2} Insert(x : int, {:linear "tid"} tid: X) returns (result : bool)
+requires {:phase 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done;
ensures {:phase 1} Inv(valid, elt, owner);
-requires {:phase 2} Inv(valid, elt, owner);
+requires {:phase 2} Inv(valid, elt, owner) && x != null && tid != nil && tid != done;
+ensures {:phase 2} Inv(valid, elt, owner);
ensures {:atomic} |{ var r:int;
- A: assert tidIn != nil && tidIn != done;
- assert x != null;
- goto B, C;
+ A: goto B, C;
B: assume (0 <= r && r < max);
assume valid[r] == false;
assume elt[r] == null;
assume owner[r] == nil;
elt[r] := x; valid[r] := true; owner[r] := done;
- tidOut := tidIn; result := true; return true;
- C: tidOut := tidIn; result := false; return true;
+ result := true; return true;
+ C: result := false; return true;
}|;
{
var i: int;
- var {:linear "tid"} tidTmp: X;
par Yield12();
- tidTmp := tidIn;
- call i, tidTmp := FindSlot(x, tidTmp);
+ call i := FindSlot(x, tid);
if(i == -1)
{
result := false;
- tidOut := tidTmp;
par Yield12();
return;
}
par Yield1();
assert {:phase 1} i != -1;
assert {:phase 2} i != -1;
- call tidTmp := acquire(i, tidTmp);
+ call acquire(i, tid);
assert {:phase 2} elt[i] == x;
assert {:phase 2} valid[i] == false;
- call tidTmp := setValid(i, tidTmp);
- call tidTmp := release(i, tidTmp);
+ call setValid(i, tid);
+ call release(i, tid);
result := true;
- tidOut := tidTmp;
par Yield12();
return;
}
-procedure {:yields} {:phase 2} InsertPair(x : int,
- y : int,
- {:linear_in "tid"} tidIn: X)
- returns (result : bool,
- {:linear "tid"} tidOut: X)
-requires {:phase 1} Inv(valid, elt, owner);
+procedure {:yields} {:phase 2} InsertPair(x : int, y : int, {:linear "tid"} tid: X) returns (result : bool)
+requires {:phase 1} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done;
ensures {:phase 1} Inv(valid, elt, owner);
-requires {:phase 2} Inv(valid, elt, owner);
+requires {:phase 2} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done;
ensures {:phase 2} Inv(valid, elt, owner);
ensures {:atomic} |{ var rx:int;
var ry:int;
- A: assert tidIn != nil && tidIn != done;
- assert x != null && y != null;
- goto B, C;
+ A: goto B, C;
B: assume (0 <= rx && rx < max && 0 <= ry && ry < max && rx != ry);
assume valid[rx] == false;
assume valid[ry] == false;
@@ -230,68 +202,60 @@ ensures {:atomic} |{ var rx:int;
valid[ry] := true;
owner[rx] := done;
owner[ry] := done;
- tidOut := tidIn;
result := true; return true;
- C: tidOut := tidIn;
- result := false; return true;
+ C: result := false; return true;
}|;
{
var i : int;
var j : int;
- var {:linear "tid"} tidTmp: X;
par Yield12();
- tidTmp := tidIn;
-
- call i, tidTmp := FindSlot(x, tidTmp);
+ call i := FindSlot(x, tid);
if (i == -1)
{
result := false;
- tidOut := tidTmp;
par Yield12();
return;
}
par Yield1();
- call j, tidTmp := FindSlot(y, tidTmp);
+ call j := FindSlot(y, tid);
if(j == -1)
{
par Yield1();
- call tidTmp := acquire(i,tidTmp);
- call tidTmp := setEltToNull(i, tidTmp);
- call tidTmp := release(i,tidTmp);
+ call acquire(i,tid);
+ call setEltToNull(i, tid);
+ call release(i,tid);
result := false;
- tidOut := tidTmp;
par Yield12();
return;
}
par Yield1();
assert {:phase 2} i != -1 && j != -1;
- call tidTmp := acquire(i, tidTmp);
- call tidTmp := acquire(j, tidTmp);
+ call acquire(i, tid);
+ call acquire(j, tid);
assert {:phase 2} elt[i] == x;
assert {:phase 2} elt[j] == y;
assert {:phase 2} valid[i] == false;
assert {:phase 2} valid[j] == false;
- call tidTmp := setValid(i, tidTmp);
- call tidTmp := setValid(j, tidTmp);
- call tidTmp := release(j, tidTmp);
- call tidTmp := release(i, tidTmp);
+ call setValid(i, tid);
+ call setValid(j, tid);
+ call release(j, tid);
+ call release(i, tid);
result := true;
- tidOut := tidTmp;
par Yield12();
return;
}
-procedure {:yields} {:phase 2} LookUp(x : int, {:linear_in "tid"} tidIn: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool, {:linear "tid"} tidOut: X)
+procedure {:yields} {:phase 2} LookUp(x : int, {:linear "tid"} tid: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool)
requires {:phase 1} {:phase 2} old_valid == valid && old_elt == elt;
requires {:phase 1} {:phase 2} Inv(valid, elt, owner);
-requires {:phase 1} {:phase 2} (tidIn != nil && tidIn != done);
+requires {:phase 1} {:phase 2} (tid != nil && tid != done);
ensures {:phase 1} {:phase 2} Inv(valid, elt, owner);
-ensures {:atomic} |{ A: assert tidIn != nil && tidIn != done;
+ensures {:atomic} |{ A: assert tid != nil && tid != done;
assert x != null;
assume found ==> (exists ii:int :: 0 <= ii && ii < max && valid[ii] && elt[ii] == x);
assume !found ==> (forall ii:int :: 0 <= ii && ii < max ==> !(old_valid[ii] && old_elt[ii] == x));
@@ -300,37 +264,31 @@ ensures {:atomic} |{ A: assert tidIn != nil && tidIn != done;
{
var j : int;
var isThere : bool;
- var {:linear "tid"} tidTmp: X;
par Yield12() | YieldLookUp(old_valid, old_elt);
j := 0;
- tidTmp := tidIn;
while(j < max)
- invariant {:phase 1} {:phase 2} tidTmp != nil && tidTmp != done;
- invariant {:phase 1} {:phase 2} tidTmp == tidIn;
invariant {:phase 1} {:phase 2} Inv(valid, elt, owner);
invariant {:phase 1} {:phase 2} (forall ii:int :: 0 <= ii && ii < j ==> !(old_valid[ii] && old_elt[ii] == x));
invariant {:phase 1} {:phase 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);
invariant {:phase 1} {:phase 2} 0 <= j;
{
- call tidTmp := acquire(j, tidTmp);
- call tidTmp, isThere := isEltThereAndValid(j, x, tidTmp);
+ call acquire(j, tid);
+ call isThere := isEltThereAndValid(j, x, tid);
if(isThere)
{
- call tidTmp := release(j, tidTmp);
+ call release(j, tid);
found := true;
- tidOut := tidTmp;
par Yield12() | YieldLookUp(old_valid, old_elt);
return;
}
- call tidTmp := release(j,tidTmp);
+ call release(j,tid);
par Yield12() | YieldLookUp(old_valid, old_elt);
j := j + 1;
}
found := false;
- tidOut := tidTmp;
par Yield12() | YieldLookUp(old_valid, old_elt);
return;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 02:28:38 +0000