summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Concurrency/OwickiGries.cs7
-rw-r--r--Test/og/civl-paper.bpl145
-rw-r--r--Test/og/civl-paper.bpl.expect2
-rw-r--r--Test/og/multiset.bpl178
-rw-r--r--Test/og/ticket.bpl83
-rw-r--r--Test/og/ticket.bpl.expect2
6 files changed, 201 insertions, 216 deletions
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index e5201809..23c8945b 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -945,13 +945,6 @@ namespace Microsoft.Boogie
ParCallCmd parCallCmd = cmd as ParCallCmd;
AddCallToYieldProc(parCallCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
DesugarParallelCallCmd(newCmds, parCallCmd);
- if (globalMods.Count > 0 && pc != null)
- {
- // assume pc || alpha(i, g);
- Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
- assumeExpr.Type = Type.Bool;
- newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
- }
HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(parCallCmd));
linearTypeChecker.AddAvailableVars(parCallCmd, availableLinearVars);
Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl
index eadf81e3..be519470 100644
--- a/Test/og/civl-paper.bpl
+++ b/Test/og/civl-paper.bpl
@@ -15,86 +15,123 @@ function map(lmap): [int]int;
function cons([int]bool, [int]int) : lmap;
axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && map(cons(x,y)) == y);
-var {:phase 2} {:linear "mem"} g: lmap;
+var {:phase 3} {:linear "mem"} g: lmap;
+var {:phase 3} lock: X;
+var {:phase 1} b: bool;
const p: int;
-procedure {:yields} {:phase 1,2} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap);
-ensures {:both} |{ A: assert tid != nil && lock == tid; g := l; return true; }|;
+procedure {:yields} {:phase 1} Yield1()
requires {:phase 1} InvLock(lock, b);
ensures {:phase 1} InvLock(lock, b);
+{
+ yield;
+ assert {:phase 1} InvLock(lock, b);
+}
-procedure {:yields} {:phase 1,2} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap);
-ensures {:both} |{ A: assert tid != nil && lock == tid; l := g; return true; }|;
-requires {:phase 1} InvLock(lock, b);
-ensures {:phase 1} InvLock(lock, b);
+function {:inline} InvLock(lock: X, b: bool) : bool
+{
+ lock != nil <==> b
+}
-procedure {:yields} {:phase 1} Load({:linear "mem"} l: lmap, a: int) returns (v: int);
-ensures {:both} |{ A: v := map(l)[a]; return true; }|;
-requires {:phase 1} InvLock(lock, b);
-ensures {:phase 1} InvLock(lock, b);
+procedure {:yields} {:phase 2} Yield2()
+{
+ yield;
+}
-procedure {:yields} {:phase 1} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);
-ensures {:both} |{ A: assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|;
-requires {:phase 1} InvLock(lock, b);
-ensures {:phase 1} InvLock(lock, b);
+procedure {:yields} {:phase 3} Yield3()
+requires {:phase 3} Inv(g);
+ensures {:phase 3} Inv(g);
+{
+ yield;
+ assert {:phase 3} Inv(g);
+}
-procedure {:yields} {:phase 2} P({:linear "tid"} tid: X)
-requires {:phase 1} InvLock(lock, b);
+function {:inline} Inv(g: lmap) : bool
+{
+ dom(g)[p] && dom(g)[p+4] && map(g)[p] == map(g)[p+4]
+}
+
+procedure {:yields} {:phase 3} P({:linear "tid"} tid: X)
+requires {:phase 1} tid != nil && InvLock(lock, b);
ensures {:phase 1} InvLock(lock, b);
-requires {:phase 2} tid != nil && Inv(g);
-ensures {:phase 2} Inv(g);
+requires {:phase 3} tid != nil && Inv(g);
+ensures {:phase 3} Inv(g);
{
var t: int;
var {:linear "mem"} l: lmap;
- par Yield() | YieldLock();
- call Acquire(tid);
- call l := TransferFromGlobal(tid);
+ par Yield3() | Yield1();
+ call AcquireProtected(tid);
+ call l := TransferFromGlobalProtected(tid);
call t := Load(l, p);
call l := Store(l, p, t+1);
call t := Load(l, p+4);
call l := Store(l, p+4, t+1);
- call TransferToGlobal(tid, l);
- call Release(tid);
- par Yield() | YieldLock();
+ call TransferToGlobalProtected(tid, l);
+ call ReleaseProtected(tid);
+ par Yield3() | Yield1();
}
-procedure {:yields} {:phase 2} Yield()
-requires {:phase 2} Inv(g);
-ensures {:phase 2} Inv(g);
+
+procedure {:yields} {:phase 2,3} TransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap)
+ensures {:both} |{ A: assert tid != nil && lock == tid; g := l; return true; }|;
+requires {:phase 1} InvLock(lock, b);
+ensures {:phase 1} InvLock(lock, b);
{
- yield;
- assert {:phase 2} Inv(g);
+ par Yield1() | Yield2();
+ call TransferToGlobal(tid, l);
+ par Yield1() | Yield2();
}
-function {:inline} Inv(g: lmap) : bool
+procedure {:yields} {:phase 2,3} TransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap)
+ensures {:both} |{ A: assert tid != nil && lock == tid; l := g; return true; }|;
+requires {:phase 1} InvLock(lock, b);
+ensures {:phase 1} InvLock(lock, b);
{
- dom(g)[p] && dom(g)[p+4] && map(g)[p] == map(g)[p+4]
+ par Yield1() | Yield2();
+ call l := TransferFromGlobal(tid);
+ par Yield1() | Yield2();
}
+procedure {:yields} {:phase 2,3} AcquireProtected({:linear "tid"} tid: X)
+ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;
+requires {:phase 1} tid != nil && InvLock(lock, b);
+ensures {:phase 1} InvLock(lock, b);
+{
+ par Yield1() | Yield2();
+ call Acquire(tid);
+ par Yield1() | Yield2();
+}
-var {:phase 1} b: bool;
-var {:phase 2} lock: X;
+procedure {:yields} {:phase 2,3} ReleaseProtected({:linear "tid"} tid: X)
+ensures {:left} |{ A: assert tid != nil && lock == tid; lock := nil; return true; }|;
+requires {:phase 1} InvLock(lock, b);
+ensures {:phase 1} InvLock(lock, b);
+{
+ par Yield1() | Yield2();
+ call Release(tid);
+ par Yield1() | Yield2();
+}
procedure {:yields} {:phase 1,2} Acquire({:linear "tid"} tid: X)
-requires {:phase 1} InvLock(lock, b);
+requires {:phase 1} tid != nil && InvLock(lock, b);
ensures {:phase 1} InvLock(lock, b);
-ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;
+ensures {:atomic} |{ A: assume lock == nil; lock := tid; return true; }|;
{
var status: bool;
var tmp: X;
- par YieldLock();
+ par Yield1();
L:
assert {:phase 1} InvLock(lock, b);
call status := CAS(tid, false, true);
- par YieldLock();
+ par Yield1();
goto A, B;
A:
assume status;
- par YieldLock();
+ par Yield1();
return;
B:
@@ -103,15 +140,27 @@ ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; retur
}
procedure {:yields} {:phase 1,2} Release({:linear "tid"} tid: X)
-ensures {:left} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|;
+ensures {:atomic} |{ A: lock := nil; return true; }|;
requires {:phase 1} InvLock(lock, b);
ensures {:phase 1} InvLock(lock, b);
{
- par YieldLock();
+ par Yield1();
call CLEAR(tid, false);
- par YieldLock();
+ par Yield1();
}
+procedure {:yields} {:phase 0,2} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap);
+ensures {:atomic} |{ A: g := l; return true; }|;
+
+procedure {:yields} {:phase 0,2} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap);
+ensures {:atomic} |{ A: l := g; return true; }|;
+
+procedure {:yields} {:phase 0,3} Load({:linear "mem"} l: lmap, a: int) returns (v: int);
+ensures {:both} |{ A: v := map(l)[a]; return true; }|;
+
+procedure {:yields} {:phase 0,3} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);
+ensures {:both} |{ A: assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|;
+
procedure {:yields} {:phase 0,1} CAS(tid: X, prev: bool, next: bool) returns (status: bool);
ensures {:atomic} |{
A: goto B, C;
@@ -124,15 +173,3 @@ ensures {:atomic} |{
A: b := next; lock := nil; return true;
}|;
-procedure {:yields} {:phase 1} YieldLock()
-requires {:phase 1} InvLock(lock, b);
-ensures {:phase 1} InvLock(lock, b);
-{
- yield;
- assert {:phase 1} InvLock(lock, b);
-}
-
-function {:inline} InvLock(lock: X, b: bool) : bool
-{
- lock != nil <==> b
-}
diff --git a/Test/og/civl-paper.bpl.expect b/Test/og/civl-paper.bpl.expect
index ac38b46e..4bcd03fb 100644
--- a/Test/og/civl-paper.bpl.expect
+++ b/Test/og/civl-paper.bpl.expect
@@ -1,2 +1,2 @@
-Boogie program verifier finished with 23 verified, 0 errors
+Boogie program verifier finished with 35 verified, 0 errors
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;
diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index 552a4007..9c1b7c9a 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -8,10 +8,10 @@ axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
type X;
function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
const nil: X;
-var {:phase 3} t: int;
-var {:phase 3} s: int;
-var {:phase 3} cs: X;
-var {:phase 3} T: [int]bool;
+var {:phase 2} t: int;
+var {:phase 2} s: int;
+var {:phase 2} cs: X;
+var {:phase 2} T: [int]bool;
function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
@@ -36,17 +36,18 @@ function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool)
procedure Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);
ensures {:phase 1} {:phase 2} xl != nil;
-procedure {:yields} {:phase 3} main({:linear_in "tid"} xls':[X]bool)
-requires {:phase 3} xls' == mapconstbool(true);
+procedure {:yields} {:phase 2} main({:linear_in "tid"} xls':[X]bool)
+requires {:phase 2} xls' == mapconstbool(true);
{
var {:linear "tid"} tid: X;
var {:linear "tid"} xls: [X]bool;
yield;
- call xls := Init(xls');
+ call Init(xls');
+ xls := xls';
- par Yield1() | Yield2() | Yield();
+ par Yield1() | Yield2();
while (*)
invariant {:phase 1} Inv1(T, t);
@@ -54,63 +55,59 @@ requires {:phase 3} xls' == mapconstbool(true);
{
call xls, tid := Allocate(xls);
async call Customer(tid);
- par Yield1() | Yield2() | Yield();
+ par Yield1() | Yield2();
}
- par Yield1() | Yield2() | Yield();
+ par Yield1() | Yield2();
}
-procedure {:yields} {:phase 3} Customer({:linear_in "tid"} tid': X)
+procedure {:yields} {:phase 2} Customer({:linear_in "tid"} tid: X)
requires {:phase 1} Inv1(T, t);
-requires {:phase 2} tid' != nil && Inv2(T, s, cs);
-requires {:phase 3} true;
+requires {:phase 2} tid != nil && Inv2(T, s, cs);
{
- var {:linear "tid"} tid: X;
- tid := tid';
-
- par Yield1() | Yield2() | Yield();
+ par Yield1() | Yield2();
while (*)
invariant {:phase 1} Inv1(T, t);
- invariant {:phase 2} tid != nil && Inv2(T, s, cs);
+ invariant {:phase 2} Inv2(T, s, cs);
{
- call tid := Enter(tid);
+ call Enter(tid);
+ par Yield1() | Yield2() | YieldSpec(tid);
+ call Leave(tid);
par Yield1() | Yield2();
- call tid := Leave(tid);
- par Yield1() | Yield2() | Yield();
}
- par Yield1() | Yield2() | Yield();
+ par Yield1() | Yield2();
}
-procedure {:yields} {:phase 2,3} Enter({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X)
+procedure {:yields} {:phase 2} Enter({:linear "tid"} tid: X)
requires {:phase 1} Inv1(T, t);
ensures {:phase 1} Inv1(T,t);
-requires {:phase 2} tid' != nil && Inv2(T, s, cs);
-ensures {:phase 2} tid != nil && Inv2(T, s, cs);
-ensures {:right} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil; cs := tid; return true; }|;
+requires {:phase 2} tid != nil && Inv2(T, s, cs);
+ensures {:phase 2} Inv2(T, s, cs) && cs == tid;
{
var m: int;
par Yield1() | Yield2();
- tid := tid';
- call tid, m := GetTicketAbstract(tid);
+ call m := GetTicketAbstract(tid);
par Yield1();
- call tid := WaitAndEnter(tid, m);
- par Yield1() | Yield2();
+ call WaitAndEnter(tid, m);
+ par Yield1() | Yield2() | YieldSpec(tid);
}
-procedure {:yields} {:phase 1,2} GetTicketAbstract({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int)
+procedure {:yields} {:phase 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int)
requires {:phase 1} Inv1(T, t);
ensures {:phase 1} Inv1(T, t);
-ensures {:right} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; return true; }|;
+ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|;
{
par Yield1();
- tid := tid';
- call tid, m := GetTicket(tid);
+ call m := GetTicket(tid);
par Yield1();
}
-procedure {:yields} {:phase 3} Yield()
+procedure {:yields} {:phase 2} YieldSpec({:linear "tid"} tid: X)
+requires {:phase 2} tid != nil && cs == tid;
+ensures {:phase 2} cs == tid;
{
yield;
+ assert {:phase 2} tid != nil && cs == tid;
}
procedure {:yields} {:phase 2} Yield2()
@@ -129,15 +126,15 @@ ensures {:phase 1} Inv1(T,t);
assert {:phase 1} Inv1(T,t);
}
-procedure {:yields} {:phase 0,3} Init({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool);
-ensures {:atomic} |{ A: assert xls' == mapconstbool(true); xls := xls'; cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
+procedure {:yields} {:phase 0,2} Init({:linear "tid"} xls:[X]bool);
+ensures {:atomic} |{ A: assert xls == mapconstbool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
-procedure {:yields} {:phase 0,1} GetTicket({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int);
-ensures {:atomic} |{ A: tid := tid'; m := t; t := t + 1; T[m] := true; return true; }|;
+procedure {:yields} {:phase 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);
+ensures {:atomic} |{ A: m := t; t := t + 1; T[m] := true; return true; }|;
-procedure {:yields} {:phase 0,2} WaitAndEnter({:linear_in "tid"} tid': X, m:int) returns ({:linear "tid"} tid: X);
-ensures {:atomic} |{ A: tid := tid'; assume m <= s; cs := tid; return true; }|;
+procedure {:yields} {:phase 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int);
+ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|;
-procedure {:yields} {:phase 0,3} Leave({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X);
-ensures {:atomic} |{ A: assert cs == tid'; assert tid' != nil; tid := tid'; s := s + 1; cs := nil; return true; }|;
+procedure {:yields} {:phase 0,2} Leave({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|;
diff --git a/Test/og/ticket.bpl.expect b/Test/og/ticket.bpl.expect
index bc10e4e3..f7c1129d 100644
--- a/Test/og/ticket.bpl.expect
+++ b/Test/og/ticket.bpl.expect
@@ -1,2 +1,2 @@
-Boogie program verifier finished with 21 verified, 0 errors
+Boogie program verifier finished with 14 verified, 0 errors
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 21:00:08 +0000