diff options
Diffstat (limited to 'Test/civl/multiset.bpl')
| -rw-r--r-- | Test/civl/multiset.bpl | 324 |
1 files changed, 324 insertions, 0 deletions
diff --git a/Test/civl/multiset.bpl b/Test/civl/multiset.bpl new file mode 100644 index 00000000..ec391380 --- /dev/null +++ b/Test/civl/multiset.bpl @@ -0,0 +1,324 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; + +const unique null : int; +const unique nil: X; +const unique done: X; + +var {:layer 0} elt : [int]int; +var {:layer 0} valid : [int]bool; +var {:layer 0} lock : [int]X; +var {:layer 0} owner : [int]X; +const max : int; + +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool +{ + MapConstBool(false)[x := true] +} + +axiom (max > 0); + +procedure {:yields} {:layer 0} acquire(i : int, {:linear "tid"} tid: X); +ensures {:right} |{ A: + assert 0 <= i && i < max; + assert tid != nil && tid != done; + assume lock[i] == nil; + lock[i] := tid; + return true; + }|; + + +procedure {:yields} {:layer 0} release(i : int, {:linear "tid"} tid: X); +ensures {:left} |{ A: + assert 0 <= i && i < max; + assert lock[i] == tid; + assert tid != nil && tid != done; + lock[i] := nil; + return true; + }|; + + +procedure {:yields} {:layer 0,1} getElt(j : int, {:linear "tid"} tid: X) returns (elt_j:int); +ensures {:both} |{ A: + assert 0 <= j && j < max; + assert lock[j] == tid; + assert tid != nil && tid != done; + elt_j := elt[j]; + return true; + }|; + + +procedure {:yields} {:layer 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] == tid; + assert tid != nil && tid != done; + elt[j] := x; + owner[j] := tid; + return true; + }|; + + +procedure {:yields} {:layer 0,2} setEltToNull(j : int, {:linear "tid"} tid: X); +ensures {:left} |{ A: + assert owner[j] == tid; + assert 0 <= j && j < max; + assert lock[j] == tid; + assert !valid[j]; + assert tid != nil && tid != done; + elt[j] := null; + owner[j] := nil; + return true; + }|; + +procedure {:yields} {:layer 0,2} setValid(j : int, {:linear "tid"} tid: X); +ensures {:both} |{ A: + assert 0 <= j && j < max; + assert lock[j] == tid; + assert tid != nil && tid != done; + assert owner[j] == tid; + valid[j] := true; + owner[j] := done; + return true; + }|; + +procedure {:yields} {:layer 0,2} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool); +ensures {:both} |{ A: + assert 0 <= j && j < max; + assert lock[j] == tid; + assert tid != nil && tid != done; + fnd := (elt[j] == x) && valid[j]; + return true; + }|; + +procedure {:yields} {:layer 1,2} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int) +requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; +ensures {:layer 1} Inv(valid, elt, owner); +ensures {:right} |{ A: assert tid != nil && tid != done; + assert x != null; + goto B, C; + B: assume (0 <= r && r < max); + assume elt[r] == null; + assume owner[r] == nil; + assume !valid[r]; + elt[r] := x; + owner[r] := tid; + return true; + C: assume (r == -1); return true; + }|; +{ + var j : int; + var elt_j : int; + + par Yield1(); + + j := 0; + while(j < max) + invariant {:layer 1} Inv(valid, elt, owner); + invariant {:layer 1} 0 <= j; + { + call acquire(j, tid); + call elt_j := getElt(j, tid); + if(elt_j == null) + { + call setElt(j, x, tid); + call release(j, tid); + r := j; + + par Yield1(); + return; + } + call release(j,tid); + + par Yield1(); + + j := j + 1; + } + r := -1; + + par Yield1(); + return; +} + +procedure {:yields} {:layer 2} Insert(x : int, {:linear "tid"} tid: X) returns (result : bool) +requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; +ensures {:layer 1} Inv(valid, elt, owner); +requires {:layer 2} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; +ensures {:layer 2} Inv(valid, elt, owner); +ensures {:atomic} |{ var r:int; + 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; + result := true; return true; + C: result := false; return true; + }|; + { + var i: int; + par Yield12(); + call i := FindSlot(x, tid); + + if(i == -1) + { + result := false; + par Yield12(); + return; + } + par Yield1(); + assert {:layer 1} i != -1; + assert {:layer 2} i != -1; + call acquire(i, tid); + assert {:layer 2} elt[i] == x; + assert {:layer 2} valid[i] == false; + call setValid(i, tid); + call release(i, tid); + result := true; + par Yield12(); + return; +} + +procedure {:yields} {:layer 2} InsertPair(x : int, y : int, {:linear "tid"} tid: X) returns (result : bool) +requires {:layer 1} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; +ensures {:layer 1} Inv(valid, elt, owner); +requires {:layer 2} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; +ensures {:layer 2} Inv(valid, elt, owner); +ensures {:atomic} |{ var rx:int; + var ry:int; + A: goto B, C; + B: assume (0 <= rx && rx < max && 0 <= ry && ry < max && rx != ry); + 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; + result := true; return true; + C: result := false; return true; + }|; + { + var i : int; + var j : int; + par Yield12(); + + call i := FindSlot(x, tid); + + if (i == -1) + { + result := false; + par Yield12(); + return; + } + + par Yield1(); + call j := FindSlot(y, tid); + + if(j == -1) + { + par Yield1(); + call acquire(i,tid); + call setEltToNull(i, tid); + call release(i,tid); + result := false; + par Yield12(); + return; + } + + par Yield1(); + assert {:layer 2} i != -1 && j != -1; + call acquire(i, tid); + call acquire(j, tid); + assert {:layer 2} elt[i] == x; + assert {:layer 2} elt[j] == y; + assert {:layer 2} valid[i] == false; + assert {:layer 2} valid[j] == false; + call setValid(i, tid); + call setValid(j, tid); + call release(j, tid); + call release(i, tid); + result := true; + par Yield12(); + return; +} + +procedure {:yields} {:layer 2} LookUp(x : int, {:linear "tid"} tid: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool) +requires {:layer 1} {:layer 2} old_valid == valid && old_elt == elt; +requires {:layer 1} {:layer 2} Inv(valid, elt, owner); +requires {:layer 1} {:layer 2} (tid != nil && tid != done); +ensures {:layer 1} {:layer 2} Inv(valid, elt, owner); +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)); + return true; + }|; +{ + var j : int; + var isThere : bool; + + par Yield12() | YieldLookUp(old_valid, old_elt); + + j := 0; + + while(j < max) + invariant {:layer 1} {:layer 2} Inv(valid, elt, owner); + invariant {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < j ==> !(old_valid[ii] && old_elt[ii] == x)); + invariant {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]); + invariant {:layer 1} {:layer 2} 0 <= j; + { + call acquire(j, tid); + call isThere := isEltThereAndValid(j, x, tid); + if(isThere) + { + call release(j, tid); + found := true; + par Yield12() | YieldLookUp(old_valid, old_elt); + return; + } + call release(j,tid); + par Yield12() | YieldLookUp(old_valid, old_elt); + j := j + 1; + } + found := false; + + par Yield12() | YieldLookUp(old_valid, old_elt); + return; +} + +procedure {:yields} {:layer 1} Yield1() +requires {:layer 1} Inv(valid, elt, owner); +ensures {:layer 1} Inv(valid, elt, owner); +{ + yield; + assert {:layer 1} Inv(valid, elt, owner); +} + +procedure {:yields} {:layer 2} Yield12() +requires {:layer 1} {:layer 2} Inv(valid, elt, owner); +ensures {:layer 1} {:layer 2} Inv(valid, elt, owner); +{ + yield; + assert {:layer 1} {:layer 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))) +} + +procedure {:yields} {:layer 2} YieldLookUp(old_valid: [int]bool, old_elt: [int]int) +requires {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]); +ensures {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]); +{ + yield; + assert {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]); +} |