diff options
| author |  Ally Donaldson <unknown> | 2014-01-17 10:36:33 +0000 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2014-01-17 10:36:33 +0000 |
| commit | b6e440731cf30f00b7b8840be8a1e048c8f21d60 (patch) | |
| tree | 7000e81ad029df274530352db584a1629a1fdd4f /Test | |
| parent | 16bc038b94f93c37ce5ecd1ba0cbeff1a3aa5ec7 (diff) | |
| parent | 4b265b8ef4428e6d583359650c07c652884112bb (diff) | |
Merge
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/og/Answer | 14 | ||||
| -rw-r--r-- | Test/og/multiset.bpl | 322 | ||||
| -rw-r--r-- | Test/og/treiber-stack.bpl | 86 |
3 files changed, 415 insertions, 7 deletions
diff --git a/Test/og/Answer b/Test/og/Answer index 73ec8537..067a6534 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -1,6 +1,6 @@ -------------------- foo.bpl --------------------
-foo.bpl(14,3): Error BP5001: This assertion might not hold.
+foo.bpl(14,3): Error: Non-interference check failed
Execution trace:
foo.bpl(6,5): anon0
(0,0): inline$Impl_YieldChecker_PC_2147483647$0$L0
@@ -8,11 +8,11 @@ Execution trace: Boogie program verifier finished with 4 verified, 1 error
-------------------- bar.bpl --------------------
-bar.bpl(13,3): Error BP5001: This assertion might not hold.
+bar.bpl(13,3): Error: Non-interference check failed
Execution trace:
bar.bpl(6,5): anon0
(0,0): inline$Impl_YieldChecker_PC_2147483647$0$L0
-bar.bpl(13,3): Error BP5001: This assertion might not hold.
+bar.bpl(13,3): Error: Non-interference check failed
Execution trace:
bar.bpl(23,5): anon0
(0,0): inline$Impl_YieldChecker_PC_2147483647$0$L0
@@ -24,11 +24,11 @@ Boogie program verifier finished with 3 verified, 2 errors Boogie program verifier finished with 2 verified, 0 errors
-------------------- parallel1.bpl --------------------
-parallel1.bpl(10,1): Error BP5001: This assertion might not hold.
+parallel1.bpl(10,1): Error: Non-interference check failed
Execution trace:
parallel1.bpl(6,5): anon0
(0,0): inline$Proc_YieldChecker_PC_2147483647$0$L0
-parallel1.bpl(14,3): Error BP5001: This assertion might not hold.
+parallel1.bpl(14,3): Error: Non-interference check failed
Execution trace:
parallel1.bpl(6,5): anon0
(0,0): inline$Impl_YieldChecker_PC_2147483647$0$L0
@@ -72,7 +72,7 @@ Boogie program verifier finished with 4 verified, 0 errors Boogie program verifier finished with 3 verified, 0 errors
-------------------- t1.bpl --------------------
-t1.bpl(35,5): Error BP5001: This assertion might not hold.
+t1.bpl(35,5): Error: Non-interference check failed
Execution trace:
(0,0): og_init
(0,0): inline$Impl_YieldChecker_A_2147483647$0$L1
@@ -88,7 +88,7 @@ Boogie program verifier finished with 2 verified, 0 errors Boogie program verifier finished with 2 verified, 0 errors
-------------------- async.bpl --------------------
-async.bpl(14,1): Error BP5001: This assertion might not hold.
+async.bpl(14,1): Error: Non-interference check failed
Execution trace:
async.bpl(7,3): anon0
async.bpl(7,3): anon0$1
diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl new file mode 100644 index 00000000..9da8c125 --- /dev/null +++ b/Test/og/multiset.bpl @@ -0,0 +1,322 @@ +type X;
+
+const unique null : int;
+const unique nil: X;
+const unique done: X;
+
+var {:qed} elt : [int]int;
+var {:qed} valid : [int]bool;
+var {:qed} lock : [int]X;
+var {:qed} owner : [int]X;
+const max : int;
+
+axiom (max > 0);
+
+procedure {:yields} acquire(i : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
+ensures {:right 0} |{ A:
+ assert 0 <= i && i < max;
+ assert tidIn != nil && tidIn != done;
+ assume lock[i] == nil;
+ tidOut := tidIn;
+ lock[i] := tidOut;
+ return true;
+ }|;
+
+
+procedure {:yields} release(i : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
+ensures {:left 0} |{ A:
+ assert 0 <= i && i < max;
+ assert lock[i] == tidIn;
+ assert tidIn != nil && tidIn != done;
+ tidOut := tidIn;
+ lock[i] := nil;
+ return true;
+ }|;
+
+
+procedure {:yields} getElt(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, elt_j:int);
+ensures {:both 0} |{ A:
+ assert 0 <= j && j < max;
+ assert lock[j] == tidIn;
+ assert tidIn != nil && tidIn != done;
+ tidOut := tidIn;
+ elt_j := elt[j];
+ return true;
+ }|;
+
+
+procedure {:yields} setElt(j : int, x : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
+ensures {:both 0} |{ A:
+ assert x != null;
+ assert owner[j] == nil;
+ assert 0 <= j && j < max;
+ assert lock[j] == tidIn;
+ assert tidIn != nil && tidIn != done;
+ tidOut := tidIn;
+ elt[j] := x;
+ owner[j] := tidIn;
+ return true;
+ }|;
+
+
+procedure {:yields} setEltToNull(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
+ensures {:left 0} |{ A:
+ assert owner[j] == tidIn;
+ assert 0 <= j && j < max;
+ assert lock[j] == tidIn;
+ assert !valid[j];
+ assert tidIn != nil && tidIn != done;
+ tidOut := tidIn;
+ elt[j] := null;
+ owner[j] := nil;
+ return true;
+ }|;
+
+
+
+
+procedure {:yields} getValid(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, valid_j:bool);
+ensures {:both 0} |{ A:
+ assert 0 <= j && j < max;
+ assert lock[j] == tidIn;
+ assert tidIn != nil && tidIn != done;
+ tidOut := tidIn;
+ valid_j := valid[j];
+ return true;
+ }|;
+
+
+procedure {:yields} setValid(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
+ensures {:both 0} |{ A:
+ assert 0 <= j && j < max;
+ assert lock[j] == tidIn;
+ assert tidIn != nil && tidIn != done;
+ assert owner[j] == tidIn;
+ tidOut := tidIn;
+ valid[j] := true;
+ owner[j] := done;
+ return true;
+ }|;
+
+
+procedure {:yields} FindSlot(x : int, {:linear "tid"} tidIn: X) returns (r : int, {:linear "tid"} tidOut: X)
+requires {:phase 1} Inv(valid, elt, owner);
+ensures {:phase 1} Inv(valid, elt, owner);
+ensures {:right 1} |{ A: assert tidIn != nil && tidIn != done;
+ assert x != null;
+ // assert (forall ii:int :: 0 <= ii && ii<max ==> lock[ii] != tidIn);
+ havoc r; assume (-1 <= r && r < max); goto B, C;
+ B: assume (r != -1);
+ assume elt[r] == null;
+ assume owner[r] == nil;
+ elt[r] := x;
+ owner[r] := tidIn;
+ tidOut := tidIn;
+ return true;
+ C: assume (r == -1); tidOut := tidIn; 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);
+ {
+ par Yield1();
+
+ call tidTmp := acquire(j, tidTmp);
+ call tidTmp, elt_j := getElt(j, tidTmp);
+ if(elt_j == null)
+ {
+ call tidTmp := setElt(j, x, tidTmp);
+ call tidTmp := release(j, tidTmp);
+ r := j;
+ tidOut := tidTmp;
+
+ par Yield1();
+
+ return;
+ }
+ call tidTmp := release(j,tidTmp);
+
+ par Yield1();
+
+ j := j + 1;
+ }
+ r := -1;
+ tidOut := tidTmp;
+ return;
+}
+
+procedure {:yields} Insert(x : int, {:linear "tid"} tidIn: X) returns (result : bool, i : int, {:linear "tid"} tidOut: X)
+requires {:phase 1} Inv(valid, elt, owner);
+requires {:phase 2} Inv(valid, elt, owner);
+ensures {:phase 1} Inv(valid, elt, owner);
+requires {:phase 2} Inv(valid, elt, owner);
+ensures {:atomic 2} |{ var r:int;
+ A: assert tidIn != nil && tidIn != done;
+ assert x != null;
+ havoc r; assume (-1 <= r && r < max); goto B, C;
+ B: assume (r != -1);
+ 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;
+ }|;
+ {
+
+ var {:linear "tid"} tidTmp: X;
+ par Yield12();
+ tidTmp := tidIn;
+ call i, tidTmp := FindSlot(x, tidTmp);
+
+ if(i == -1)
+ {
+ result := false;
+ tidOut := tidTmp;
+ par YieldInv();
+ return;
+ }
+ par Yield1();
+ assert {:phase 1} i != -1;
+ assert {:phase 2} i != -1;
+ call tidTmp := acquire(i, tidTmp);
+ assert {:phase 2} elt[i] == x;
+ assert {:phase 2} valid[i] == false;
+ call tidTmp := setValid(i, tidTmp);
+ call tidTmp := release(i, tidTmp);
+ result := true;
+ tidOut := tidTmp;
+ par YieldInv();
+ return;
+}
+
+procedure {:yields} InsertPair(x : int,
+ y : int,
+ {:linear "tid"} tidIn: X)
+ returns (result : bool,
+ i : int,
+ j : int,
+ {:linear "tid"} tidOut: X)
+requires {:phase 1} Inv(valid, elt, owner);
+ensures {:phase 1} Inv(valid, elt, owner);
+requires {:phase 2} Inv(valid, elt, owner);
+ensures {:phase 2} Inv(valid, elt, owner);
+ensures {:atomic 2} |{ var rx:int;
+ var ry:int;
+ A: assert tidIn != nil && tidIn != done;
+ assert x != null && y != null;
+ havoc rx; assume (-1 <= rx && rx < max);
+ havoc ry; assume (-1 <= ry && ry < max);
+ assume (rx == ry ==> rx == -1);
+ goto B, C;
+ B: assume (rx != -1 && ry != -1);
+ assume valid[rx] == false;
+ assume valid[ry] == false;
+ assume elt[rx] == null;
+ assume elt[rx] == null;
+ elt[rx] := x;
+ elt[ry] := y;
+ valid[rx] := true;
+ valid[ry] := true;
+ owner[rx] := done;
+ owner[ry] := done;
+ tidOut := tidIn;
+ result := true; return true;
+ C: tidOut := tidIn;
+ result := false; return true;
+ }|;
+ {
+
+ var {:linear "tid"} tidTmp: X;
+ par Yield12();
+
+ tidTmp := tidIn;
+
+ call i, tidTmp := FindSlot(x, tidTmp);
+
+ if (i == -1)
+ {
+ result := false;
+ tidOut := tidTmp;
+ par Yield12();
+ return;
+ }
+
+ par Yield1();
+ call j, tidTmp := FindSlot(y, tidTmp);
+
+ if(j == -1)
+ {
+ par Yield1();
+ call tidTmp := acquire(i,tidTmp);
+ call tidTmp := setEltToNull(i, tidTmp);
+ call tidTmp := release(i,tidTmp);
+ 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);
+ 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);
+ result := true;
+ tidOut := tidTmp;
+ par Yield12();
+ return;
+}
+
+procedure {:yields} {:stable} Yield1()
+requires {:phase 1} Inv(valid, elt, owner);
+ensures {:phase 1} Inv(valid, elt, owner);
+ensures {:both 1} |{ A: return true; }|;
+{
+}
+
+procedure {:yields} {:stable} YieldInv()
+requires {:phase 2} Inv(valid, elt, owner);
+ensures {:phase 2} Inv(valid, elt, owner);
+{
+ yield;
+ assert {:phase 2} Inv(valid, elt, owner);
+}
+
+procedure {:yields} {:stable} Yield12()
+requires {:phase 1} {:phase 2} Inv(valid, elt, owner);
+ensures {:phase 1} {:phase 2} Inv(valid, elt, owner);
+{
+ yield;
+ assert {:phase 1} {:phase 2} Inv(valid, elt, owner);
+}
+
+
+
+function {:inline} Inv(valid: [int]bool, elt: [int]int, owner: [int]X): (bool)
+{
+ ( forall i:int :: 0 <= i && i < max ==>
+ ( elt[i] == null <==>
+ !valid[i] && (owner[i] == nil)
+ )
+ )
+}
diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl new file mode 100644 index 00000000..707688a6 --- /dev/null +++ b/Test/og/treiber-stack.bpl @@ -0,0 +1,86 @@ +type Node;
+type lmap;
+function dom(lmap): [Node]bool;
+function map(lmap): [Node]Node;
+
+function {:builtin "MapConst"} MapConst(bool) : [Node]bool;
+function {:builtin "MapOr"} MapOr([Node]bool, [Node]bool) : [Node]bool;
+
+procedure Load(i:Node) returns(v:Node);
+ requires dom(stack)[i];
+ ensures v == map(stack)[i];
+
+procedure Store({:linear "Node"} l_in:lmap, i:Node, v:Node) returns({:linear "Node"} l_out:lmap);
+ requires dom(l_in)[i];
+ ensures dom(l_out) == dom(l_in);
+ ensures map(l_out) == map(l_in)[i := v];
+
+procedure TransferIn({:linear "Node"} l1_in:lmap, d:Node);
+ requires dom(l1_in)[d];
+ modifies stack;
+ ensures dom(stack) == dom(old(stack))[d := true];
+ ensures map(stack) == map(old(stack))[d := map(l1_in)[d]];
+
+procedure TransferOut(d:Node);
+ requires dom(stack)[d];
+ modifies stack;
+ ensures dom(stack) == dom(old(stack))[d := false];
+ ensures map(stack) == map(old(stack));
+
+procedure New() returns ({:linear "Node"} l: lmap, d: Node);
+ensures dom(l)[d];
+
+const unique null: Node;
+
+var TOP: Node;
+var {:linear "Node"} stack: lmap;
+
+procedure {:yields} CAS(oldVal: Node, newVal: Node)
+returns (r: bool)
+{
+ r := (TOP == oldVal);
+ if (r) {
+ TOP := newVal;
+ }
+}
+
+procedure {:yields} push()
+{
+ var t, x: Node;
+ var g: bool;
+ var {:linear "Node"} x_lmap: lmap;
+
+ call x_lmap, x := New();
+
+ while(true)
+ {
+ t := TOP;
+ call x_lmap := Store(x_lmap, x, t);
+ call g := CAS(t, x);
+ if (g) {
+ call TransferIn(x_lmap, x);
+ break;
+ }
+ }
+}
+
+procedure {:yields} pop()
+{
+ var t, x: Node;
+ var g: bool;
+
+ while(true)
+ {
+ t := TOP;
+ if (t == null)
+ {
+ return;
+ }
+ call x := Load(t);
+ call g := CAS(t, x);
+ if (g) {
+ call TransferOut(t);
+ break;
+ }
+ }
+}
\ No newline at end of file |