diff options
| -rw-r--r-- | Source/Concurrency/MoverCheck.cs | 48 | ||||
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 19 | ||||
| -rw-r--r-- | Source/Concurrency/TypeCheck.cs | 159 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 19 | ||||
| -rw-r--r-- | Test/og/Answer | 2 | ||||
| -rw-r--r-- | Test/og/civl-paper.bpl | 2 | ||||
| -rw-r--r-- | Test/og/multiset.bpl | 18 | ||||
| -rw-r--r-- | Test/og/ticket.bpl | 6 |
8 files changed, 152 insertions, 121 deletions
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index adfcc5c9..db2bfb23 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -9,23 +9,39 @@ namespace Microsoft.Boogie {
public class MoverCheck
{
- public static MoverType GetMoverType(Ensures e, out int phaseNum)
+ public static MoverType GetMoverType(Ensures e, out int phaseNum, out int availableUptoPhaseNum)
{
- phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "atomic", int.MaxValue);
- if (phaseNum != int.MaxValue)
+ if (FindAtomicAction(e.Attributes, "atomic", out phaseNum, out availableUptoPhaseNum))
return MoverType.Atomic;
- phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "right", int.MaxValue);
- if (phaseNum != int.MaxValue)
+ if (FindAtomicAction(e.Attributes, "right", out phaseNum, out availableUptoPhaseNum))
return MoverType.Right;
- phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "left", int.MaxValue);
- if (phaseNum != int.MaxValue)
+ if (FindAtomicAction(e.Attributes, "left", out phaseNum, out availableUptoPhaseNum))
return MoverType.Left;
- phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "both", int.MaxValue);
- if (phaseNum != int.MaxValue)
+ if (FindAtomicAction(e.Attributes, "both", out phaseNum, out availableUptoPhaseNum))
return MoverType.Both;
return MoverType.Top;
}
+ private static bool FindAtomicAction(QKeyValue kv, string name, out int phaseNum, out int availableUptoPhaseNum)
+ {
+ phaseNum = int.MaxValue;
+ availableUptoPhaseNum = int.MaxValue;
+ for (; kv != null; kv = kv.Next)
+ {
+ if (kv.Key != name) continue;
+ if (!(kv.Params.Count == 1 || kv.Params.Count == 2)) continue;
+ LiteralExpr l0 = kv.Params[0] as LiteralExpr;
+ if (l0 == null || !l0.isBigNum) continue;
+ phaseNum = l0.asBigNum.ToIntSafe;
+ if (kv.Params.Count == 1) return true;
+ LiteralExpr l1 = kv.Params[1] as LiteralExpr;
+ if (l1 == null || !l1.isBigNum) continue;
+ availableUptoPhaseNum = l1.asBigNum.ToIntSafe;
+ return true;
+ }
+ return false;
+ }
+
LinearTypeChecker linearTypeChecker;
MoverTypeChecker moverTypeChecker;
List<Declaration> decls;
@@ -50,13 +66,16 @@ namespace Microsoft.Boogie Dictionary<int, HashSet<ActionInfo>> pools = new Dictionary<int, HashSet<ActionInfo>>();
foreach (ActionInfo action in moverTypeChecker.procToActionInfo.Values)
{
- foreach (int phaseNum in action.callerPhaseNums)
+ foreach (int phaseNum in moverTypeChecker.allPhaseNums)
{
- if (!pools.ContainsKey(phaseNum))
+ if (action.phaseNum < phaseNum && phaseNum <= action.availableUptoPhaseNum)
{
- pools[phaseNum] = new HashSet<ActionInfo>();
+ if (!pools.ContainsKey(phaseNum))
+ {
+ pools[phaseNum] = new HashSet<ActionInfo>();
+ }
+ pools[phaseNum].Add(action);
}
- pools[phaseNum].Add(action);
}
}
@@ -457,6 +476,8 @@ namespace Microsoft.Boogie {
domainNameToScope[domainName] = new HashSet<Variable>();
}
+ /*
+ // Commenting this out to avoid the danger of making an assumption about a hidden variable
foreach (Variable v in program.GlobalVariables())
{
var domainName = linearTypeChecker.FindDomainName(v);
@@ -464,6 +485,7 @@ namespace Microsoft.Boogie if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
domainNameToScope[domainName].Add(v);
}
+ */
if (first != null)
{
foreach (Variable v in first.thatInParams)
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index b5d41b21..9de83635 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -14,7 +14,7 @@ namespace Microsoft.Boogie {
MoverTypeChecker moverTypeChecker;
public int phaseNum;
- int enclosingProcPhaseNum;
+ Procedure enclosingProc;
public Dictionary<Procedure, Procedure> procMap; /* Original -> Duplicate */
public Dictionary<Absy, Absy> absyMap; /* Duplicate -> Original */
public Dictionary<Block, Block> blockMap; /* Original -> Duplicate */
@@ -22,7 +22,7 @@ namespace Microsoft.Boogie {
this.moverTypeChecker = moverTypeChecker;
this.phaseNum = phaseNum;
- this.enclosingProcPhaseNum = int.MaxValue;
+ this.enclosingProc = null;
this.procMap = new Dictionary<Procedure, Procedure>();
this.absyMap = new Dictionary<Absy, Absy>();
this.blockMap = new Dictionary<Block, Block>();
@@ -30,6 +30,11 @@ namespace Microsoft.Boogie private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List<Cmd> newCmds)
{
+ int enclosingProcPhaseNum = moverTypeChecker.FindPhaseNumber(enclosingProc);
+ if (enclosingProcPhaseNum == int.MaxValue)
+ {
+ enclosingProcPhaseNum = moverTypeChecker.allPhaseNums.Max();
+ }
Procedure originalProc = originalCallCmd.Proc;
if (phaseNum == enclosingProcPhaseNum && moverTypeChecker.procToActionInfo.ContainsKey(originalProc))
{
@@ -137,6 +142,7 @@ namespace Microsoft.Boogie public override Procedure VisitProcedure(Procedure node)
{
+ enclosingProc = node;
if (!QKeyValue.FindBoolAttribute(node.Attributes, "yields"))
return node;
if (!procMap.ContainsKey(node))
@@ -164,11 +170,7 @@ namespace Microsoft.Boogie private Variable dummyLocalVar;
public override Implementation VisitImplementation(Implementation node)
{
- enclosingProcPhaseNum = moverTypeChecker.FindPhaseNumber(node.Proc);
- if (enclosingProcPhaseNum == int.MaxValue)
- {
- enclosingProcPhaseNum = moverTypeChecker.allPhaseNums.Max();
- }
+ enclosingProc = node.Proc;
dummyLocalVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_dummy", Type.Bool));
Implementation impl = base.VisitImplementation(node);
impl.LocVars.Add(dummyLocalVar);
@@ -206,7 +208,8 @@ namespace Microsoft.Boogie Ensures ensures = base.VisitEnsures(node);
if (node.Free)
return ensures;
- if (ensures.IsAtomicSpecification || !OwickiGries.FindPhaseNums(ensures.Attributes).Contains(phaseNum))
+ bool isAtomicSpecification = moverTypeChecker.procToActionInfo.ContainsKey(enclosingProc) && moverTypeChecker.procToActionInfo[enclosingProc].ensures == ensures;
+ if (isAtomicSpecification || !OwickiGries.FindPhaseNums(ensures.Attributes).Contains(phaseNum))
{
ensures.Condition = Expr.True;
ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes);
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 27a4e6a5..a8266e79 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -20,9 +20,10 @@ namespace Microsoft.Boogie public class ActionInfo
{
public Procedure proc;
+ public Ensures ensures;
public MoverType moverType;
public int phaseNum;
- public HashSet<int> callerPhaseNums;
+ public int availableUptoPhaseNum;
public List<AssertCmd> thisGate;
public CodeExpr thisAction;
public List<Variable> thisInParams;
@@ -55,12 +56,14 @@ namespace Microsoft.Boogie get { return moverType == MoverType.Left || moverType == MoverType.Both; }
}
- public ActionInfo(Procedure proc, CodeExpr codeExpr, MoverType moverType, int phaseNum)
+ public ActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int phaseNum, int availableUptoPhaseNum)
{
+ CodeExpr codeExpr = ensures.Condition as CodeExpr;
this.proc = proc;
+ this.ensures = ensures;
this.moverType = moverType;
this.phaseNum = phaseNum;
- this.callerPhaseNums = new HashSet<int>();
+ this.availableUptoPhaseNum = availableUptoPhaseNum;
this.thisGate = new List<AssertCmd>();
this.thisAction = codeExpr;
this.thisInParams = new List<Variable>();
@@ -186,19 +189,17 @@ namespace Microsoft.Boogie else
return int.MaxValue;
}
- public HashSet<Variable> QedGlobalVariables()
- {
- return qedGlobalVariables;
- }
CheckingContext checkingContext;
public int errorCount;
- HashSet<Variable> qedGlobalVariables;
- int enclosingProcPhaseNum;
+ Dictionary<Variable, int> qedGlobalVariables;
+ Procedure enclosingProc;
public Dictionary<Procedure, ActionInfo> procToActionInfo;
public Program program;
public HashSet<int> allPhaseNums;
bool inAtomicSpecification;
+ bool inSpecification;
+ int minPhaseNum;
public void TypeCheck()
{
@@ -208,8 +209,8 @@ namespace Microsoft.Boogie if (proc == null) continue;
foreach (Ensures e in proc.Ensures)
{
- int phaseNum;
- MoverType moverType = MoverCheck.GetMoverType(e, out phaseNum);
+ int phaseNum, availableUptoPhaseNum;
+ MoverType moverType = MoverCheck.GetMoverType(e, out phaseNum, out availableUptoPhaseNum);
if (moverType == MoverType.Top) continue;
CodeExpr codeExpr = e.Condition as CodeExpr;
if (codeExpr == null)
@@ -222,16 +223,16 @@ namespace Microsoft.Boogie Error(proc, "A procedure can have at most one atomic action");
continue;
}
- ActionInfo actionInfo = new ActionInfo(proc, codeExpr, moverType, phaseNum);
- /*
- * Removing this restriction based on the new failure preservation check
- if (actionInfo.IsLeftMover && !actionInfo.isNonBlocking)
+ if (phaseNum >= availableUptoPhaseNum)
{
- Error(e, "A left mover must be non blocking");
+ Error(proc, "Available at phase number should be less than available up to phase number");
continue;
}
- */
- procToActionInfo[proc] = actionInfo;
+ if (phaseNum != int.MaxValue)
+ {
+ allPhaseNums.Add(phaseNum);
+ }
+ procToActionInfo[proc] = new ActionInfo(proc, e, moverType, phaseNum, availableUptoPhaseNum);
}
}
this.VisitProgram(program);
@@ -242,12 +243,19 @@ namespace Microsoft.Boogie public MoverTypeChecker(Program program)
{
- this.qedGlobalVariables = new HashSet<Variable>();
+ this.qedGlobalVariables = new Dictionary<Variable, int>();
foreach (var g in program.GlobalVariables())
{
if (QKeyValue.FindBoolAttribute(g.Attributes, "qed"))
{
- this.qedGlobalVariables.Add(g);
+ this.qedGlobalVariables.Add(g, int.MaxValue);
+ g.Attributes = OwickiGries.RemoveQedAttribute(g.Attributes);
+ }
+ else
+ {
+ int phaseNum = QKeyValue.FindIntAttribute(g.Attributes, "qed", int.MaxValue);
+ if (phaseNum == int.MaxValue) continue;
+ this.qedGlobalVariables.Add(g, phaseNum);
g.Attributes = OwickiGries.RemoveQedAttribute(g.Attributes);
}
}
@@ -256,36 +264,43 @@ namespace Microsoft.Boogie this.errorCount = 0;
this.checkingContext = new CheckingContext(null);
this.program = program;
- this.enclosingProcPhaseNum = int.MaxValue;
+ this.enclosingProc = null;
this.inAtomicSpecification = false;
+ this.inSpecification = false;
+ this.minPhaseNum = int.MaxValue;
}
public override Implementation VisitImplementation(Implementation node)
{
- enclosingProcPhaseNum = FindPhaseNumber(node.Proc);
+ this.enclosingProc = node.Proc;
return base.VisitImplementation(node);
}
public override Procedure VisitProcedure(Procedure node)
{
- enclosingProcPhaseNum = FindPhaseNumber(node);
- if (enclosingProcPhaseNum != int.MaxValue)
- {
- allPhaseNums.Add(enclosingProcPhaseNum);
- }
+ this.enclosingProc = node;
return base.VisitProcedure(node);
}
public override Cmd VisitCallCmd(CallCmd node)
{
if (!node.IsAsync)
{
+ int enclosingProcPhaseNum = FindPhaseNumber(enclosingProc);
int calleePhaseNum = FindPhaseNumber(node.Proc);
- if (enclosingProcPhaseNum > calleePhaseNum)
+ if (enclosingProcPhaseNum == int.MaxValue)
{
- procToActionInfo[node.Proc].callerPhaseNums.Add(enclosingProcPhaseNum);
+
}
- else if (enclosingProcPhaseNum < calleePhaseNum || enclosingProcPhaseNum != int.MaxValue)
+ else if (calleePhaseNum == int.MaxValue)
+ {
+ Error(node, "An atomic procedure cannot call a non-atomic procedure");
+ }
+ else if (enclosingProcPhaseNum <= calleePhaseNum)
{
Error(node, "The phase of the caller procedure must be greater than the phase of the callee");
}
+ else if (procToActionInfo[node.Proc].availableUptoPhaseNum < enclosingProcPhaseNum)
+ {
+ Error(node, "The callee is not available in the phase of the caller procedure");
+ }
}
return base.VisitCallCmd(node);
}
@@ -298,7 +313,7 @@ namespace Microsoft.Boogie if (calleePhaseNum > maxCalleePhaseNum)
maxCalleePhaseNum = calleePhaseNum;
}
-
+ int enclosingProcPhaseNum = FindPhaseNumber(enclosingProc);
if (enclosingProcPhaseNum > maxCalleePhaseNum)
{
bool isLeftMover = true;
@@ -308,24 +323,32 @@ namespace Microsoft.Boogie ActionInfo actionInfo = procToActionInfo[iter.Proc];
isLeftMover = isLeftMover && actionInfo.IsLeftMover;
isRightMover = isRightMover && actionInfo.IsRightMover;
- actionInfo.callerPhaseNums.Add(enclosingProcPhaseNum);
}
if (!isLeftMover && !isRightMover && node.CallCmds.Count > 1)
{
Error(node, "The procedures in the parallel call must be all right mover or all left mover");
}
+ return base.VisitParCallCmd(node);
+ }
+ else
+ {
+ return node;
}
- return node;
}
public override Expr VisitIdentifierExpr(IdentifierExpr node)
{
if (node.Decl is GlobalVariable)
{
- if (inAtomicSpecification && !qedGlobalVariables.Contains(node.Decl))
+ if (qedGlobalVariables.ContainsKey(node.Decl) && qedGlobalVariables[node.Decl] < minPhaseNum)
+ {
+ minPhaseNum = qedGlobalVariables[node.Decl];
+ }
+
+ if (inAtomicSpecification && !qedGlobalVariables.ContainsKey(node.Decl))
{
Error(node, "Cannot access non-qed global variable in atomic action");
}
- else if (!inAtomicSpecification && qedGlobalVariables.Contains(node.Decl))
+ else if (!inSpecification && qedGlobalVariables.ContainsKey(node.Decl))
{
Error(node, "Cannot access qed global variable in ordinary code");
}
@@ -334,47 +357,63 @@ namespace Microsoft.Boogie }
public override Ensures VisitEnsures(Ensures ensures)
{
- if (ensures.IsAtomicSpecification)
+ minPhaseNum = int.MaxValue;
+ inAtomicSpecification = procToActionInfo.ContainsKey(enclosingProc) && procToActionInfo[enclosingProc].ensures == ensures;
+ inSpecification = true;
+ Ensures ret = base.VisitEnsures(ensures);
+ inSpecification = false;
+ if (inAtomicSpecification)
{
- inAtomicSpecification = true;
- Ensures ret = base.VisitEnsures(ensures);
+ if (procToActionInfo[enclosingProc].availableUptoPhaseNum > minPhaseNum)
+ {
+ Error(ensures, "A variable being accessed is hidden before this action becomes unavailable");
+ }
inAtomicSpecification = false;
- return ret;
}
- foreach (int phaseNum in OwickiGries.FindPhaseNums(ensures.Attributes))
+ else
{
- allPhaseNums.Add(phaseNum);
- if (phaseNum > enclosingProcPhaseNum)
- {
- Error(ensures, "The phase of ensures clause cannot be greater than the phase of enclosing procedure");
- }
+ CheckAndAddPhases(ensures, ensures.Attributes);
}
- return ensures;
+ return ret;
}
public override Requires VisitRequires(Requires requires)
{
- foreach (int phaseNum in OwickiGries.FindPhaseNums(requires.Attributes))
- {
- allPhaseNums.Add(phaseNum);
- if (phaseNum > enclosingProcPhaseNum)
- {
- Error(requires, "The phase of requires clause cannot be greater than the phase of enclosing procedure");
- }
- }
- return requires;
+ minPhaseNum = int.MaxValue;
+ inSpecification = true;
+ Requires ret = base.VisitRequires(requires);
+ inSpecification = false;
+ CheckAndAddPhases(requires, requires.Attributes);
+ return ret;
}
public override Cmd VisitAssertCmd(AssertCmd node)
{
- foreach (int phaseNum in OwickiGries.FindPhaseNums(node.Attributes))
+ minPhaseNum = int.MaxValue;
+ inSpecification = true;
+ Cmd ret = base.VisitAssertCmd(node);
+ inSpecification = false;
+ CheckAndAddPhases(node, node.Attributes);
+ return ret;
+ }
+
+ private void CheckAndAddPhases(Absy node, QKeyValue attributes)
+ {
+ foreach (int phaseNum in OwickiGries.FindPhaseNums(attributes))
{
- allPhaseNums.Add(phaseNum);
- if (phaseNum > enclosingProcPhaseNum)
+ if (phaseNum > FindPhaseNumber(enclosingProc))
{
- Error(node, "The phase of assert cannot be greater than the phase of enclosing procedure");
+ Error(node, "The phase cannot be greater than the phase of enclosing procedure");
+ }
+ else if (phaseNum > minPhaseNum)
+ {
+ Error(node, "A variable being accessed is hidden before this specification becomes unavailable");
+ }
+ else
+ {
+ allPhaseNums.Add(phaseNum);
}
}
- return node;
}
+
public void Error(Absy node, string message)
{
checkingContext.Error(node, message);
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 60f76232..0bf55b17 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2364,26 +2364,7 @@ namespace Microsoft.Boogie { this.Condition.Resolve(rc);
}
- public bool IsAtomicSpecification
- {
- get
- {
- return
- QKeyValue.FindIntAttribute(this.Attributes, "atomic", int.MaxValue) != int.MaxValue ||
- QKeyValue.FindIntAttribute(this.Attributes, "right", int.MaxValue) != int.MaxValue ||
- QKeyValue.FindIntAttribute(this.Attributes, "left", int.MaxValue) != int.MaxValue ||
- QKeyValue.FindIntAttribute(this.Attributes, "both", int.MaxValue) != int.MaxValue;
- }
- }
-
public override void Typecheck(TypecheckingContext tc) {
- //Contract.Requires(tc != null);
-
- if (IsAtomicSpecification && !tc.Yields)
- {
- tc.Error(this, "atomic specification allowed only in a yielding procedure");
- return;
- }
this.Condition.Typecheck(tc);
Contract.Assert(this.Condition.Type != null); // follows from postcondition of Expr.Typecheck
if (!this.Condition.Type.Unify(Type.Bool)) {
diff --git a/Test/og/Answer b/Test/og/Answer index f50f6d98..4b880cac 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -114,7 +114,7 @@ Boogie program verifier finished with 6 verified, 0 errors -------------------- multiset.bpl --------------------
-Boogie program verifier finished with 102 verified, 0 errors
+Boogie program verifier finished with 104 verified, 0 errors
-------------------- civl-paper.bpl --------------------
diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl index 4ebaadbe..0449a166 100644 --- a/Test/og/civl-paper.bpl +++ b/Test/og/civl-paper.bpl @@ -100,7 +100,7 @@ ensures {:right 1} |{ A: assert tid != nil; assume lock == nil; b := true; lock }
procedure {:yields} CAS(tid: X, prev: bool, next: bool) returns (status: bool);
-ensures {:atomic 0} |{
+ensures {:atomic 0,1} |{
A: goto B, C;
B: assume b == prev; b := next; status := true; lock := tid; return true;
C: status := false; return true;
diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl index 161171bf..5bb056f3 100644 --- a/Test/og/multiset.bpl +++ b/Test/og/multiset.bpl @@ -41,7 +41,7 @@ ensures {:left 0} |{ A: procedure {:yields} getElt(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, elt_j:int);
-ensures {:both 0} |{ A:
+ensures {:both 0,1} |{ A:
assert 0 <= j && j < max;
assert lock[j] == tidIn;
assert tidIn != nil && tidIn != done;
@@ -52,7 +52,7 @@ ensures {:both 0} |{ A: procedure {:yields} setElt(j : int, x : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
-ensures {:both 0} |{ A:
+ensures {:both 0,1} |{ A:
assert x != null;
assert owner[j] == nil;
assert 0 <= j && j < max;
@@ -78,20 +78,6 @@ ensures {:left 0} |{ A: 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;
diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl index 3404f8e0..953230e7 100644 --- a/Test/og/ticket.bpl +++ b/Test/og/ticket.bpl @@ -95,7 +95,7 @@ ensures {:right 2} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil procedure {:yields} GetTicketAbstract({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int)
requires {:phase 1} Inv1(T, t);
ensures {:phase 1} Inv1(T, t);
-ensures {:right 1} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; return true; }|;
+ensures {:right 1,2} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; return true; }|;
{
par Yield1();
tid := tid';
@@ -125,10 +125,10 @@ procedure {:yields} Init({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} ensures {:atomic 0} |{ A: assert xls' == mapconstbool(true); xls := xls'; cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
procedure {:yields} GetTicket({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int);
-ensures {:atomic 0} |{ A: tid := tid'; m := t; t := t + 1; T[m] := true; return true; }|;
+ensures {:atomic 0,1} |{ A: tid := tid'; m := t; t := t + 1; T[m] := true; return true; }|;
procedure {:yields} WaitAndEnter({:linear "tid"} tid': X, m:int) returns ({:linear "tid"} tid: X);
-ensures {:atomic 0} |{ A: tid := tid'; assume m <= s; cs := tid; return true; }|;
+ensures {:atomic 0,2} |{ A: tid := tid'; assume m <= s; cs := tid; return true; }|;
procedure {:yields} Leave({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);
ensures {:atomic 0} |{ A: assert cs == tid'; assert tid' != nil; tid := tid'; s := s + 1; cs := nil; return true; }|;
|