checkpoint

31 files changed, 970 insertions, 1046 deletions

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index df2eeffd..dcc59878 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -9,53 +9,20 @@ namespace Microsoft.Boogie
 {

     public class MoverCheck

     {

-        public static MoverType GetMoverType(Ensures e, out int phaseNum, out int availableUptoPhaseNum)

-        {

-            if (FindAtomicAction(e.Attributes, "atomic", out phaseNum, out availableUptoPhaseNum))

-                return MoverType.Atomic;

-            if (FindAtomicAction(e.Attributes, "right", out phaseNum, out availableUptoPhaseNum))

-                return MoverType.Right;

-            if (FindAtomicAction(e.Attributes, "left", out phaseNum, out availableUptoPhaseNum))

-                return MoverType.Left;

-            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;

-        HashSet<Tuple<ActionInfo, ActionInfo>> commutativityCheckerCache;

-        HashSet<Tuple<ActionInfo, ActionInfo>> gatePreservationCheckerCache;

-        HashSet<Tuple<ActionInfo, ActionInfo>> failurePreservationCheckerCache;

+        HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> commutativityCheckerCache;

+        HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> gatePreservationCheckerCache;

+        HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> failurePreservationCheckerCache;

         private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)

         {

             this.linearTypeChecker = linearTypeChecker;

             this.moverTypeChecker = moverTypeChecker;

             this.decls = decls;

-            this.commutativityCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();

-            this.gatePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();

-            this.failurePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();

+            this.commutativityCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();

+            this.gatePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();

+            this.failurePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();

         }

 

         public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)

@@ -63,18 +30,20 @@ namespace Microsoft.Boogie
             if (moverTypeChecker.procToActionInfo.Count == 0)

                 return;

 

-            Dictionary<int, HashSet<ActionInfo>> pools = new Dictionary<int, HashSet<ActionInfo>>();

+            Dictionary<int, HashSet<AtomicActionInfo>> pools = new Dictionary<int, HashSet<AtomicActionInfo>>();

             foreach (ActionInfo action in moverTypeChecker.procToActionInfo.Values)

             {

-                foreach (int phaseNum in moverTypeChecker.allPhaseNums)

+                AtomicActionInfo atomicAction = action as AtomicActionInfo;

+                if (atomicAction == null) continue;

+                foreach (int phaseNum in moverTypeChecker.AllPhaseNums)

                 {

                     if (action.phaseNum < phaseNum && phaseNum <= action.availableUptoPhaseNum)

                     {

                         if (!pools.ContainsKey(phaseNum))

                         {

-                            pools[phaseNum] = new HashSet<ActionInfo>();

+                            pools[phaseNum] = new HashSet<AtomicActionInfo>();

                         }

-                        pools[phaseNum].Add(action);

+                        pools[phaseNum].Add(atomicAction);

                     }

                 }

             }

@@ -83,7 +52,7 @@ namespace Microsoft.Boogie
             MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls);

             foreach (int phaseNum1 in pools.Keys)

             {

-                foreach (ActionInfo first in pools[phaseNum1])

+                foreach (AtomicActionInfo first in pools[phaseNum1])

                 {

                     Debug.Assert(first.moverType != MoverType.Top);

                     if (first.moverType == MoverType.Atomic)

@@ -91,7 +60,7 @@ namespace Microsoft.Boogie
                     foreach (int phaseNum2 in pools.Keys)

                     {

                         if (phaseNum2 < phaseNum1) continue;

-                        foreach (ActionInfo second in pools[phaseNum2])

+                        foreach (AtomicActionInfo second in pools[phaseNum2])

                         {

                             if (second.phaseNum < phaseNum1)

                             {

@@ -111,11 +80,12 @@ namespace Microsoft.Boogie
                     }

                 }

             }

-            foreach (ActionInfo action in moverTypeChecker.procToActionInfo.Values)

+            foreach (ActionInfo actionInfo in moverTypeChecker.procToActionInfo.Values)

             {

-                if (action.IsLeftMover && action.hasAssumeCmd)

+                AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;

+                if (atomicActionInfo != null && atomicActionInfo.IsLeftMover && atomicActionInfo.hasAssumeCmd)

                 {

-                    moverChecking.CreateNonBlockingChecker(program, action);

+                    moverChecking.CreateNonBlockingChecker(program, atomicActionInfo);

                 }

             }

         }

@@ -130,38 +100,37 @@ namespace Microsoft.Boogie
                     return new OldExpr(Token.NoToken, ret);

                 }

                 else

+                {

                     return ret;

+                }

             }

         }

 

         public class TransitionRelationComputation

         {

             private Program program;

-            private ActionInfo first;  // corresponds to that*

-            private ActionInfo second; // corresponds to this*

+            private AtomicActionInfo first;  // corresponds to that*

+            private AtomicActionInfo second; // corresponds to this*

             private Stack<Cmd> cmdStack;

             private List<PathInfo> paths;

             private HashSet<Variable> frame;

+            private HashSet<Variable> postExistVars;

 

-            public TransitionRelationComputation(Program program, ActionInfo second, HashSet<Variable> frame)

+            public TransitionRelationComputation(Program program, AtomicActionInfo second, HashSet<Variable> frame, HashSet<Variable> postExistVars)

             {

+                this.postExistVars = postExistVars;

                 this.frame = frame;

                 TransitionRelationComputationHelper(program, null, second);

             }

 

-            public TransitionRelationComputation(Program program, ActionInfo second)

+            public TransitionRelationComputation(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet<Variable> frame, HashSet<Variable> postExistVars)

             {

-                this.frame = new HashSet<Variable>(program.GlobalVariables());

-                TransitionRelationComputationHelper(program, null, second);

-            }

-

-            public TransitionRelationComputation(Program program, ActionInfo first, ActionInfo second)

-            {

-                this.frame = new HashSet<Variable>(program.GlobalVariables());

+                this.postExistVars = postExistVars;

+                this.frame = frame;

                 TransitionRelationComputationHelper(program, first, second);

             }

 

-            private void TransitionRelationComputationHelper(Program program, ActionInfo first, ActionInfo second)

+            private void TransitionRelationComputationHelper(Program program, AtomicActionInfo first, AtomicActionInfo second)

             {

                 this.program = program;

                 this.first = first;

@@ -292,6 +261,7 @@ namespace Microsoft.Boogie
                 Dictionary<Variable, Expr> varToExpr = path.varToExpr;

                 foreach (Variable v in varToExpr.Keys)

                 {

+                    if (postExistVars.Contains(v)) continue;

                     IdentifierExpr ie = varToExpr[v] as IdentifierExpr;

                     if (ie != null && !existsMap.ContainsKey(ie.Decl) && existsVars.Contains(ie.Decl))

                     {

@@ -357,43 +327,6 @@ namespace Microsoft.Boogie
                 return false;

             }

 

-            public Expr LeftMoverCompute(Expr failureExpr)

-            {

-                Expr returnExpr = Expr.False;

-                foreach (PathInfo path in paths)

-                {

-                    Expr expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(path.varToExpr), failureExpr);

-                    Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();

-                    foreach (Expr x in path.pathExprs)

-                    {

-                        Variable boundVar;

-                        Expr boundVarExpr;

-                        if (InferSubstitution(x, out boundVar, out boundVarExpr) && path.existsVars.Contains(boundVar))

-                        {

-                            subst[boundVar] = boundVarExpr;

-                            path.existsVars.Remove(boundVar);

-                        }

-                        else

-                        {

-                            expr = Expr.And(expr, x);

-                            expr.Type = Type.Bool;

-                        }

-                    }

-                    expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), expr);

-                    expr = new OldExpr(Token.NoToken, expr);

-                    if (path.existsVars.Count > 0)

-                    {

-                        expr = new ExistsExpr(Token.NoToken, new List<Variable>(path.existsVars), expr);

-                    }

-                    returnExpr = Expr.Or(returnExpr, expr);

-                }

-                ResolutionContext rc = new ResolutionContext(null);

-                rc.StateMode = ResolutionContext.State.Two;

-                returnExpr.Resolve(rc);

-                returnExpr.Typecheck(new TypecheckingContext(null));

-                return returnExpr;

-            }

-

             public Expr TransitionRelationCompute()

             {

                 Expr transitionRelation = Expr.False;

@@ -483,7 +416,7 @@ namespace Microsoft.Boogie
             return otherBlocks;

         }

 

-        private List<Requires> DisjointnessRequires(Program program, ActionInfo first, ActionInfo second)

+        private List<Requires> DisjointnessRequires(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet<Variable> frame)

         {

             List<Requires> requires = new List<Requires>();

             Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();

@@ -491,16 +424,13 @@ 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())

+            foreach (Variable v in frame)

             {

                 var domainName = linearTypeChecker.FindDomainName(v);

                 if (domainName == null) continue;

                 if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

                 domainNameToScope[domainName].Add(v);

             }

-             */ 

             if (first != null)

             {

                 foreach (Variable v in first.thatInParams)

@@ -525,13 +455,13 @@ namespace Microsoft.Boogie
             return requires;

         }

 

-        private void CreateCommutativityChecker(Program program, ActionInfo first, ActionInfo second)

+        private void CreateCommutativityChecker(Program program, AtomicActionInfo first, AtomicActionInfo second)

         {

             if (first == second && first.thatInParams.Count == 0 && first.thatOutParams.Count == 0)

                 return;

             if (first.CommutesWith(second))

                 return;

-            Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);

+            Tuple<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second);

             if (commutativityCheckerCache.Contains(actionPair))

                 return;

             commutativityCheckerCache.Add(actionPair);

@@ -561,13 +491,18 @@ namespace Microsoft.Boogie
             List<Block> blocks = new List<Block>();

             blocks.AddRange(firstBlocks);

             blocks.AddRange(secondBlocks);

-            List<Requires> requires = DisjointnessRequires(program, first, second);

+            HashSet<Variable> frame = new HashSet<Variable>();

+            frame.UnionWith(first.gateUsedGlobalVars);

+            frame.UnionWith(first.actionUsedGlobalVars);

+            frame.UnionWith(second.gateUsedGlobalVars);

+            frame.UnionWith(second.actionUsedGlobalVars);

+            List<Requires> requires = DisjointnessRequires(program, first, second, frame);

             foreach (AssertCmd assertCmd in first.thatGate)

                 requires.Add(new Requires(false, assertCmd.Expr));

             foreach (AssertCmd assertCmd in second.thisGate)

                 requires.Add(new Requires(false, assertCmd.Expr));

             List<Ensures> ensures = new List<Ensures>();

-            Expr transitionRelation = (new TransitionRelationComputation(program, first, second)).TransitionRelationCompute();

+            Expr transitionRelation = (new TransitionRelationComputation(program, first, second, frame, new HashSet<Variable>())).TransitionRelationCompute();

             Ensures ensureCheck = new Ensures(false, transitionRelation);

             ensureCheck.ErrorData = string.Format("Commutativity check between {0} and {1} failed", first.proc.Name, second.proc.Name);

             ensures.Add(ensureCheck);

@@ -581,11 +516,11 @@ namespace Microsoft.Boogie
             this.decls.Add(proc);

         }

 

-        private void CreateGatePreservationChecker(Program program, ActionInfo first, ActionInfo second)

+        private void CreateGatePreservationChecker(Program program, AtomicActionInfo first, AtomicActionInfo second)

         {

             if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)

                 return;

-            Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);

+            Tuple<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second);

             if (gatePreservationCheckerCache.Contains(actionPair))

                 return;

             gatePreservationCheckerCache.Add(actionPair);

@@ -599,7 +534,11 @@ namespace Microsoft.Boogie
             List<Variable> locals = new List<Variable>();

             locals.AddRange(second.thisAction.LocVars);

             List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks);

-            List<Requires> requires = DisjointnessRequires(program, first, second);

+            HashSet<Variable> frame = new HashSet<Variable>();

+            frame.UnionWith(first.gateUsedGlobalVars);

+            frame.UnionWith(second.gateUsedGlobalVars);

+            frame.UnionWith(second.actionUsedGlobalVars);

+            List<Requires> requires = DisjointnessRequires(program, first, second, frame);

             List<Ensures> ensures = new List<Ensures>();

             foreach (AssertCmd assertCmd in first.thatGate)

             {

@@ -620,11 +559,11 @@ namespace Microsoft.Boogie
             this.decls.Add(proc);

         }

 

-        private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)

+        private void CreateFailurePreservationChecker(Program program, AtomicActionInfo first, AtomicActionInfo second)

         {

             if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)

                 return;

-            Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);

+            Tuple<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second);

             if (failurePreservationCheckerCache.Contains(actionPair))

                 return;

             failurePreservationCheckerCache.Add(actionPair);

@@ -638,7 +577,11 @@ namespace Microsoft.Boogie
             List<Variable> locals = new List<Variable>();

             locals.AddRange(second.thisAction.LocVars);

             List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks);

-            List<Requires> requires = DisjointnessRequires(program, first, second);

+            HashSet<Variable> frame = new HashSet<Variable>();

+            frame.UnionWith(first.gateUsedGlobalVars);

+            frame.UnionWith(second.gateUsedGlobalVars);

+            frame.UnionWith(second.actionUsedGlobalVars);

+            List<Requires> requires = DisjointnessRequires(program, first, second, frame);

             Expr gateExpr = Expr.True;

             foreach (AssertCmd assertCmd in first.thatGate)

             {

@@ -664,67 +607,23 @@ namespace Microsoft.Boogie
             this.decls.Add(proc);

         }

 

-        /*

-        private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)

-        {

-            if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)

-                return;

-

-            Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second); 

-            if (failurePreservationCheckerCache.Contains(actionPair))

-                return;

-            failurePreservationCheckerCache.Add(actionPair);

-

-            List<Variable> inputs = new List<Variable>();

-            inputs.AddRange(first.thatInParams);

-            inputs.AddRange(second.thisInParams);

-

-            Expr requiresExpr = Expr.True;

-            foreach (AssertCmd assertCmd in first.thatGate)

-            {

-                requiresExpr = Expr.And(assertCmd.Expr, requiresExpr);

-                requiresExpr.Type = Type.Bool;

-            }

-            Expr failureExpr = Expr.Not(requiresExpr);

-            failureExpr.Type = Type.Bool;

-            List<Requires> requires = DisjointnessRequires(program, first, second);

-            requires.Add(new Requires(false, failureExpr));

-            foreach (AssertCmd assertCmd in second.thisGate)

-            {

-                requires.Add(new Requires(false, assertCmd.Expr));

-            }

-

-            Expr ensuresExpr = (new TransitionRelationComputation(program, second)).LeftMoverCompute(failureExpr);

-            List<Ensures> ensures = new List<Ensures>();

-            Ensures ensureCheck = new Ensures(false, ensuresExpr);

-            ensureCheck.ErrorData = string.Format("Gate failure of {0} not preserved by {1}", first.proc.Name, second.proc.Name);

-            ensures.Add(ensureCheck);

-

-            List<Block> blocks = new List<Block>();

-            blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));

-            string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);

-            List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

-            program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x)));

-            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures);

-            Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);

-            impl.Proc = proc;

-            this.decls.Add(impl);

-            this.decls.Add(proc);

-        }

-        */

-        

-        private void CreateNonBlockingChecker(Program program, ActionInfo second)

+        private void CreateNonBlockingChecker(Program program, AtomicActionInfo second)

         {

             List<Variable> inputs = new List<Variable>();

             inputs.AddRange(second.thisInParams);

 

-            List<Requires> requires = DisjointnessRequires(program, null, second);

+            HashSet<Variable> frame = new HashSet<Variable>();

+            frame.UnionWith(second.gateUsedGlobalVars);

+            frame.UnionWith(second.actionUsedGlobalVars);

+            List<Requires> requires = DisjointnessRequires(program, null, second, frame);

             foreach (AssertCmd assertCmd in second.thisGate)

             {

                 requires.Add(new Requires(false, assertCmd.Expr));

             }

-

-            Expr ensuresExpr = (new TransitionRelationComputation(program, second)).LeftMoverCompute(Expr.True);

+            HashSet<Variable> postExistVars = new HashSet<Variable>();

+            postExistVars.UnionWith(frame);

+            postExistVars.UnionWith(second.thisOutParams);

+            Expr ensuresExpr = (new TransitionRelationComputation(program, second, frame, postExistVars)).TransitionRelationCompute();

             List<Ensures> ensures = new List<Ensures>();

             Ensures ensureCheck = new Ensures(false, ensuresExpr);

             ensureCheck.ErrorData = string.Format("{0} is blocking", second.proc.Name);

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 9ec07854..5170383f 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -18,6 +18,8 @@ namespace Microsoft.Boogie
         public Dictionary<Procedure, Procedure> procMap; /* Original -> Duplicate */

         public Dictionary<Absy, Absy> absyMap; /* Duplicate -> Original */

         public Dictionary<Block, Block> blockMap; /* Original -> Duplicate */

+        public Dictionary<Implementation, Implementation> implMap; /* Duplicate -> Original */

+        public HashSet<Procedure> yieldingProcs;

         public MyDuplicator(MoverTypeChecker moverTypeChecker, int phaseNum)

         {

             this.moverTypeChecker = moverTypeChecker;

@@ -26,30 +28,27 @@ namespace Microsoft.Boogie
             this.procMap = new Dictionary<Procedure, Procedure>();

             this.absyMap = new Dictionary<Absy, Absy>();

             this.blockMap = new Dictionary<Block, Block>();

+            this.implMap = new Dictionary<Implementation, Implementation>();

+            this.yieldingProcs = new HashSet<Procedure>();

         }

 

         private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List<Cmd> newCmds)

         {

-            int enclosingProcPhaseNum = moverTypeChecker.FindPhaseNumber(enclosingProc);

-            if (enclosingProcPhaseNum == int.MaxValue)

-            {

-                enclosingProcPhaseNum = moverTypeChecker.allPhaseNums.Max();

-            }

+            int enclosingProcPhaseNum = moverTypeChecker.procToActionInfo[enclosingProc].phaseNum;

             Procedure originalProc = originalCallCmd.Proc;

-            if (phaseNum == enclosingProcPhaseNum && moverTypeChecker.procToActionInfo.ContainsKey(originalProc))

+            if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc))

             {

-                ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc];

-                List<AssertCmd> gate = actionInfo.thisGate;

-                if (actionInfo.phaseNum < phaseNum && gate.Count > 0)

+                AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo;

+                if (atomicActionInfo != null && atomicActionInfo.thisGate.Count > 0 && phaseNum == enclosingProcPhaseNum)

                 {

-                    newCmds.Add(new HavocCmd(Token.NoToken, new List<IdentifierExpr>(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) } )));

+                    newCmds.Add(new HavocCmd(Token.NoToken, new List<IdentifierExpr>(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) })));

                     Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();

                     for (int i = 0; i < originalProc.InParams.Count; i++)

                     {

                         map[originalProc.InParams[i]] = callCmd.Ins[i];

                     }

                     Substitution subst = Substituter.SubstitutionFromHashtable(map);

-                    foreach (AssertCmd assertCmd in gate)

+                    foreach (AssertCmd assertCmd in atomicActionInfo.thisGate)

                     {

                         newCmds.Add(Substituter.Apply(subst, assertCmd));

                     }

@@ -63,7 +62,7 @@ namespace Microsoft.Boogie
             int maxCalleePhaseNum = 0;

             foreach (CallCmd iter in originalParCallCmd.CallCmds)

             {

-                int calleePhaseNum = moverTypeChecker.FindPhaseNumber(iter.Proc);

+                int calleePhaseNum = moverTypeChecker.procToActionInfo[iter.Proc].phaseNum;

                 if (calleePhaseNum > maxCalleePhaseNum)

                     maxCalleePhaseNum = calleePhaseNum;

             }

@@ -142,27 +141,32 @@ namespace Microsoft.Boogie
 

         public override Procedure VisitProcedure(Procedure node)

         {

-            enclosingProc = node;

-            if (!QKeyValue.FindBoolAttribute(node.Attributes, "yields"))

+            if (!moverTypeChecker.procToActionInfo.ContainsKey(node))

                 return node;

             if (!procMap.ContainsKey(node))

             {

+                Procedure savedEnclosingProc = enclosingProc;

+                enclosingProc = node;

                 Procedure proc = (Procedure)node.Clone();

                 proc.Name = string.Format("{0}_{1}", node.Name, phaseNum);

                 proc.InParams = this.VisitVariableSeq(node.InParams);

                 proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies);

                 proc.OutParams = this.VisitVariableSeq(node.OutParams);

-                if (moverTypeChecker.procToActionInfo.ContainsKey(node) && moverTypeChecker.procToActionInfo[node].phaseNum < phaseNum)

+                if (moverTypeChecker.procToActionInfo[node].phaseNum < phaseNum)

                 {

                     proc.Requires = new List<Requires>();

                     proc.Ensures = new List<Ensures>();

                 }

                 else

                 {

+                    yieldingProcs.Add(proc);

                     proc.Requires = this.VisitRequiresSeq(node.Requires);

                     proc.Ensures = this.VisitEnsuresSeq(node.Ensures);

                 }

                 procMap[node] = proc;

+                enclosingProc = savedEnclosingProc;

+                proc.Modifies = new List<IdentifierExpr>();

+                moverTypeChecker.program.GlobalVariables().Iter(x => proc.Modifies.Add(Expr.Ident(x)));

             }

             return procMap[node];

         }

@@ -173,6 +177,7 @@ namespace Microsoft.Boogie
             enclosingProc = node.Proc;

             dummyLocalVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_dummy", Type.Bool));

             Implementation impl = base.VisitImplementation(node);

+            implMap[impl] = node;

             impl.LocVars.Add(dummyLocalVar);

             impl.Name = impl.Proc.Name;

             foreach (Block block in impl.Blocks)

@@ -198,7 +203,7 @@ namespace Microsoft.Boogie
             Requires requires = base.VisitRequires(node);

             if (node.Free)

                 return requires;

-            if (!OwickiGries.FindPhaseNums(requires.Attributes).Contains(phaseNum))

+            if (!moverTypeChecker.absyToPhaseNums[node].Contains(phaseNum))

                 requires.Condition = Expr.True;

             return requires;

         }

@@ -208,8 +213,9 @@ namespace Microsoft.Boogie
             Ensures ensures = base.VisitEnsures(node);

             if (node.Free)

                 return ensures;

-            bool isAtomicSpecification = moverTypeChecker.procToActionInfo.ContainsKey(enclosingProc) && moverTypeChecker.procToActionInfo[enclosingProc].ensures == node;

-            if (isAtomicSpecification || !OwickiGries.FindPhaseNums(ensures.Attributes).Contains(phaseNum))

+            AtomicActionInfo atomicActionInfo =  moverTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo;

+            bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node;

+            if (isAtomicSpecification || !moverTypeChecker.absyToPhaseNums[node].Contains(phaseNum))

             {

                 ensures.Condition = Expr.True;

                 ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes);

@@ -220,7 +226,7 @@ namespace Microsoft.Boogie
         public override Cmd VisitAssertCmd(AssertCmd node)

         {

             AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node);

-            if (!OwickiGries.FindPhaseNums(assertCmd.Attributes).Contains(phaseNum))

+            if (!moverTypeChecker.absyToPhaseNums[node].Contains(phaseNum))

                 assertCmd.Expr = Expr.True;

             return assertCmd;

         }

@@ -231,27 +237,23 @@ namespace Microsoft.Boogie
         LinearTypeChecker linearTypeChecker;

         MoverTypeChecker moverTypeChecker;

         Dictionary<Absy, Absy> absyMap;

-        Dictionary<Procedure, Procedure> reverseProcMap;

+        Dictionary<Implementation, Implementation> implMap;

+        HashSet<Procedure> yieldingProcs;

         int phaseNum;

-        List<Declaration> decls;

         List<IdentifierExpr> globalMods;

         Dictionary<string, Procedure> asyncAndParallelCallDesugarings;

         List<Procedure> yieldCheckerProcs;

         List<Implementation> yieldCheckerImpls;

         Procedure yieldProc;

 

-        public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator, List<Declaration> decls)

+        public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator)

         {

             this.linearTypeChecker = linearTypeChecker;

             this.moverTypeChecker = moverTypeChecker;

             this.absyMap = duplicator.absyMap;

             this.phaseNum = duplicator.phaseNum;

-            this.reverseProcMap = new Dictionary<Procedure, Procedure>();

-            foreach (Procedure proc in duplicator.procMap.Keys)

-            {

-                this.reverseProcMap[duplicator.procMap[proc]] = proc;

-            }

-            this.decls = decls;

+            this.implMap = duplicator.implMap;

+            this.yieldingProcs = duplicator.yieldingProcs;

             Program program = linearTypeChecker.program;

             globalMods = new List<IdentifierExpr>();

             foreach (Variable g in program.GlobalVariables())

@@ -306,10 +308,11 @@ namespace Microsoft.Boogie
 

             if (pc != null)

             {

+                Expr aa = OldEqualityExprForGlobals(ogOldGlobalMap);

                 Expr bb = OldEqualityExpr(ogOldGlobalMap);

 

-                // assert (o_old == o && g_old == g) || beta(i, g_old, o, g);

-                AssertCmd skipOrBetaAssertCmd = new AssertCmd(tok, Expr.Or(bb, beta));

+                // assert pc || g_old == g || beta(i, g_old, o, g);

+                AssertCmd skipOrBetaAssertCmd = new AssertCmd(tok, Expr.Or(Expr.Ident(pc), Expr.Or(aa, beta)));

                 skipOrBetaAssertCmd.ErrorData = "Transition invariant in initial state violated";

                 newCmds.Add(skipOrBetaAssertCmd);

 

@@ -318,8 +321,7 @@ namespace Microsoft.Boogie
                 skipAssertCmd.ErrorData = "Transition invariant in final state violated"; ;

                 newCmds.Add(skipAssertCmd);

 

-                // pc, ok := ite(o_old == o && g_old == g, pc, true), ok || beta(i, g_old, o, g);

-                List<Expr> iteArgs = new List<Expr>(new Expr[] { bb, Expr.Ident(pc), Expr.True });

+                // pc, ok := g_old == g ==> pc, ok || beta(i, g_old, o, g);

                 List<AssignLhs> pcUpdateLHS = new List<AssignLhs>(

                     new AssignLhs[] { 

                         new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)), 

@@ -327,7 +329,7 @@ namespace Microsoft.Boogie
                     });

                 List<Expr> pcUpdateRHS = new List<Expr>(

                     new Expr[] { 

-                        new NAryExpr(Token.NoToken, new IfThenElse(Token.NoToken), iteArgs),

+                        Expr.Imp(aa, Expr.Ident(pc)),

                         Expr.Or(Expr.Ident(ok), beta)

                     });

                 newCmds.Add(new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS));

@@ -383,18 +385,34 @@ namespace Microsoft.Boogie
         Variable ok;

         Expr alpha;

         Expr beta;

+        HashSet<Variable> frame;

 

         private Expr OldEqualityExpr(Dictionary<Variable, Variable> ogOldGlobalMap)

         {

             Expr bb = Expr.True;

             foreach (Variable o in ogOldGlobalMap.Keys)

             {

+                if (o is GlobalVariable && !frame.Contains(o)) continue;

                 bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));

                 bb.Type = Type.Bool;

             }

             return bb;

         }

 

+        private Expr OldEqualityExprForGlobals(Dictionary<Variable, Variable> ogOldGlobalMap)

+        {

+            Expr bb = Expr.True;

+            foreach (Variable o in ogOldGlobalMap.Keys)

+            {

+                if (o is GlobalVariable && frame.Contains(o))

+                {

+                    bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));

+                    bb.Type = Type.Bool;

+                }

+            }

+            return bb;

+        }

+

         private void DesugarYield(YieldCmd yieldCmd, List<Cmd> cmds, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar)

         {

             AddCallToYieldProc(yieldCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);

@@ -470,8 +488,7 @@ namespace Microsoft.Boogie
                     }

                     count++;

                 }

-                proc = new Procedure(Token.NoToken, procName, new List<TypeVariable>(), inParams, outParams, requiresSeq, new List<IdentifierExpr>(), ensuresSeq);

-                proc.AddAttribute("yields");

+                proc = new Procedure(Token.NoToken, procName, new List<TypeVariable>(), inParams, outParams, requiresSeq, globalMods, ensuresSeq);

                 asyncAndParallelCallDesugarings[procName] = proc;

             }

             CallCmd dummyCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs, parCallCmd.Attributes);

@@ -479,109 +496,6 @@ namespace Microsoft.Boogie
             newCmds.Add(dummyCallCmd);

         }

 

-        private void CreateYieldCheckerImplForOldStableEnsures(Procedure proc)

-        {

-            Program program = linearTypeChecker.program;

-            Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();

-            Dictionary<Variable, Expr> oldGlobalMap = new Dictionary<Variable, Expr>();

-            Dictionary<Variable, Expr> identityGlobalMap = new Dictionary<Variable, Expr>();

-            List<Variable> locals = new List<Variable>();

-            List<Variable> inputs = new List<Variable>();

-            for (int i = 0; i < proc.InParams.Count - linearTypeChecker.linearDomains.Count; i++)

-            {

-                Variable inParam = proc.InParams[i];

-                Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));

-                locals.Add(copy);

-                map[proc.InParams[i]] = Expr.Ident(copy);

-            }

-            {

-                int i = proc.InParams.Count - linearTypeChecker.linearDomains.Count;

-                foreach (string domainName in linearTypeChecker.linearDomains.Keys)

-                {

-                    Variable inParam = proc.InParams[i];

-                    Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true);

-                    inputs.Add(copy);

-                    map[proc.InParams[i]] = Expr.Ident(copy);

-                    i++;

-                }

-            }

-            Dictionary<Variable, Expr> requiresMap = new Dictionary<Variable, Expr>(map);

-            for (int i = 0; i < proc.OutParams.Count; i++)

-            {

-                Variable outParam = proc.OutParams[i];

-                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type));

-                locals.Add(copy);

-                map[proc.OutParams[i]] = Expr.Ident(copy);

-            }

-            foreach (IdentifierExpr ie in globalMods)

-            {

-                Variable g = ie.Decl;

-                identityGlobalMap[g] = Expr.Ident(g);

-                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_local_post_{0}", g.Name), g.TypedIdent.Type));

-                locals.Add(copy);

-                map[g] = Expr.Ident(copy);

-                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type), true);

-                inputs.Add(f);

-                oldGlobalMap[g] = Expr.Ident(f);

-                requiresMap[g] = Expr.Ident(f);

-            }

-            

-            Substitution requiresSubst = Substituter.SubstitutionFromHashtable(requiresMap);

-            Substitution subst = Substituter.SubstitutionFromHashtable(map);

-            Substitution identityGlobalSubst = Substituter.SubstitutionFromHashtable(identityGlobalMap);

-            Substitution oldGlobalSubst = Substituter.SubstitutionFromHashtable(oldGlobalMap);

-            List<Block> yieldCheckerBlocks = new List<Block>();

-            List<String> labels = new List<String>();

-            List<Block> labelTargets = new List<Block>();

-            Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));

-            labels.Add(yieldCheckerBlock.Label);

-            labelTargets.Add(yieldCheckerBlock);

-            yieldCheckerBlocks.Add(yieldCheckerBlock);

-            List<Cmd> newCmds = new List<Cmd>();

-            foreach (Requires requires in proc.Requires)

-            {

-                AssumeCmd assumeCmd = new AssumeCmd(Token.NoToken, Substituter.Apply(requiresSubst, requires.Condition));

-                newCmds.Add(assumeCmd);

-            }

-            foreach (Ensures ensures in proc.Ensures)

-            {

-                AssumeCmd assumeCmd = new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(subst, identityGlobalSubst, ensures.Condition)); ;

-                newCmds.Add(assumeCmd);

-            }

-            foreach (Ensures ensures in proc.Ensures)

-            {

-                var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldGlobalSubst, ensures.Condition);

-                if (ensures.Free)

-                {

-                    newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));

-                }

-                else

-                {

-                    AssertCmd assertCmd = new AssertCmd(ensures.tok, newExpr, ensures.Attributes);

-                    assertCmd.ErrorData = "Backwards non-interference check failed";

-                    newCmds.Add(assertCmd);

-                }

-            }

-            newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False));

-            yieldCheckerBlock = new Block(Token.NoToken, "L", newCmds, new ReturnCmd(Token.NoToken));

-            labels.Add(yieldCheckerBlock.Label);

-            labelTargets.Add(yieldCheckerBlock);

-            yieldCheckerBlocks.Add(yieldCheckerBlock);

-            yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), new GotoCmd(Token.NoToken, labels, labelTargets)));

-

-            // Create the yield checker procedure

-            var yieldCheckerName = string.Format("Proc_OldStableEnsuresChecker_{0}", proc.Name);

-            var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, proc.TypeParameters, inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());

-            yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

-            yieldCheckerProcs.Add(yieldCheckerProc);

-

-            // Create the yield checker implementation

-            var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, proc.TypeParameters, inputs, new List<Variable>(), locals, yieldCheckerBlocks);

-            yieldCheckerImpl.Proc = yieldCheckerProc;

-            yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

-            yieldCheckerImpls.Add(yieldCheckerImpl);

-        }

-

         private void CreateYieldCheckerImpl(DeclWithFormals decl, List<List<Cmd>> yields, Dictionary<Variable, Expr> map)

         {

             if (yields.Count == 0) return;

@@ -700,7 +614,7 @@ namespace Microsoft.Boogie
                             return true;

                         CallCmd callCmd = cmd as CallCmd;

                         if (callCmd == null) continue;

-                        if (callCmd.IsAsync || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))

+                        if (yieldingProcs.Contains(callCmd.Proc))

                             return true;

                     }

                 }

@@ -708,9 +622,17 @@ namespace Microsoft.Boogie
             return false;

         }

 

+        private bool IsYieldingCallCmd(CallCmd callCmd)

+        {

+            return true;

+        }

+

         private void TransformImpl(Implementation impl)

         {

-            if (!QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields")) return;

+            pc = null;

+            alpha = null;

+            beta = null;

+            frame = null;

 

             // Find the yielding loop headers

             impl.PruneUnreachableBlocks();

@@ -755,55 +677,70 @@ namespace Microsoft.Boogie
                 impl.LocVars.Add(l);

             }

 

-            Procedure originalProc = reverseProcMap[impl.Proc];

-            if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc))

+            Procedure originalProc = implMap[impl].Proc;

+            ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc];

+            if (actionInfo.phaseNum == this.phaseNum)

             {

-                ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc];

-                if (actionInfo.phaseNum == this.phaseNum)

+                pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool));

+                impl.LocVars.Add(pc);

+                ok = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_ok", Type.Bool));

+                impl.LocVars.Add(ok);

+                Dictionary<Variable, Expr> alwaysMap = new Dictionary<Variable, Expr>();

+                for (int i = 0; i < originalProc.InParams.Count; i++)

                 {

-                    pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool));

-                    impl.LocVars.Add(pc);

-                    ok = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_ok", Type.Bool));

-                    impl.LocVars.Add(ok);

-                    Dictionary<Variable, Expr> alwaysMap = new Dictionary<Variable, Expr>();

-                    for (int i = 0; i < originalProc.InParams.Count; i++)

-                    {

-                        alwaysMap[originalProc.InParams[i]] = Expr.Ident(impl.InParams[i]);

-                    }

-                    for (int i = 0; i < originalProc.OutParams.Count; i++)

+                    alwaysMap[originalProc.InParams[i]] = Expr.Ident(impl.InParams[i]);

+                }

+                for (int i = 0; i < originalProc.OutParams.Count; i++)

+                {

+                    alwaysMap[originalProc.OutParams[i]] = Expr.Ident(impl.OutParams[i]);

+                }

+                Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap);

+                Dictionary<Variable, Expr> foroldMap = new Dictionary<Variable, Expr>();

+                foreach (IdentifierExpr ie in globalMods)

+                {

+                    foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);

+                }

+                Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);

+                frame = new HashSet<Variable>(program.GlobalVariables());

+                HashSet<Variable> introducedVars = new HashSet<Variable>();

+                foreach (Variable v in program.GlobalVariables())

+                {

+                    if (moverTypeChecker.hidePhaseNums[v] <= actionInfo.phaseNum || moverTypeChecker.introducePhaseNums[v] > actionInfo.phaseNum)

                     {

-                        alwaysMap[originalProc.OutParams[i]] = Expr.Ident(impl.OutParams[i]);

+                        frame.Remove(v);

                     }

-                    Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap);

-                    Dictionary<Variable, Expr> foroldMap = new Dictionary<Variable, Expr>();

-                    foreach (IdentifierExpr ie in globalMods)

+                    if (moverTypeChecker.introducePhaseNums[v] == actionInfo.phaseNum)

                     {

-                        foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);

+                        introducedVars.Add(v);

                     }

-                    Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);

-                    HashSet<Variable> frame = new HashSet<Variable>(program.GlobalVariables());

-                    foreach (Variable v in moverTypeChecker.qedGlobalVariables.Keys)

+                }

+                AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;

+                if (atomicActionInfo == null)

+                {

+                    beta = Expr.True;

+                    foreach (var v in frame)

                     {

-                        if (moverTypeChecker.qedGlobalVariables[v] <= actionInfo.phaseNum)

-                        {

-                            frame.Remove(v);

-                        }

+                        beta = Expr.And(beta, Expr.Eq(Expr.Ident(v), foroldMap[v]));

                     }

-                    Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, actionInfo, frame)).TransitionRelationCompute();

+                    alpha = Expr.True;

+                }

+                else

+                {

+                    Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, atomicActionInfo, frame, introducedVars)).TransitionRelationCompute();

                     beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr);

                     Expr alphaExpr = Expr.True;

-                    foreach (AssertCmd assertCmd in actionInfo.thisGate)

+                    foreach (AssertCmd assertCmd in atomicActionInfo.thisGate)

                     {

                         alphaExpr = Expr.And(alphaExpr, assertCmd.Expr);

                         alphaExpr.Type = Type.Bool;

                     }

                     alpha = Substituter.Apply(always, alphaExpr);

-                    foreach (Variable f in impl.OutParams)

-                    {

-                        LocalVariable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_old_{0}", f.Name), f.TypedIdent.Type));

-                        impl.LocVars.Add(copy);

-                        ogOldGlobalMap[f] = copy;

-                    }

+                }

+                foreach (Variable f in impl.OutParams)

+                {

+                    LocalVariable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_old_{0}", f.Name), f.TypedIdent.Type));

+                    impl.LocVars.Add(copy);

+                    ogOldGlobalMap[f] = copy;

                 }

             }

 

@@ -858,8 +795,8 @@ namespace Microsoft.Boogie
                     

                     if (cmd is CallCmd)

                     {

-                        CallCmd callCmd = cmd as CallCmd; 

-                        if (callCmd.IsAsync || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))

+                        CallCmd callCmd = cmd as CallCmd;

+                        if (yieldingProcs.Contains(callCmd.Proc))

                         {

                             AddCallToYieldProc(callCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);

                         }

@@ -878,7 +815,7 @@ namespace Microsoft.Boogie
                         {

                             newCmds.Add(callCmd);

                         }

-                        if (callCmd.IsAsync || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))

+                        if (yieldingProcs.Contains(callCmd.Proc))

                         {

                             HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(callCmd));

                             linearTypeChecker.AddAvailableVars(callCmd, availableLinearVars);

@@ -915,7 +852,7 @@ namespace Microsoft.Boogie
                         cmds = new List<Cmd>();

                     }

                 }

-                if (b.TransferCmd is ReturnCmd && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields"))

+                if (b.TransferCmd is ReturnCmd)

                 {

                     AddCallToYieldProc(b.TransferCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);

                     if (pc != null)

@@ -950,7 +887,7 @@ namespace Microsoft.Boogie
                     if (pc != null && !graph.BackEdgeNodes(header).Contains(pred))

                     {

                         pred.Cmds.Add(new AssignCmd(Token.NoToken, new List<AssignLhs>(

-                            new AssignLhs[] { new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)), new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)) }), 

+                            new AssignLhs[] { new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)), new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)) }),

                             new List<Expr>(new Expr[] { Expr.Ident(pc), Expr.Ident(ok) })));

                     }

                     AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);

@@ -965,7 +902,7 @@ namespace Microsoft.Boogie
                     assertCmd = new AssertCmd(header.tok, Expr.Imp(Expr.Ident(oldOk), Expr.Ident(ok)));

                     assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";

                     newCmds.Add(assertCmd);

-                } 

+                }

                 foreach (string domainName in linearTypeChecker.linearDomains.Keys)

                 {

                     newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));

@@ -1035,114 +972,7 @@ namespace Microsoft.Boogie
             CreateYieldCheckerImpl(impl, yields, map);

         }

 

-        public void TransformProc(Procedure proc)

-        {

-            if (!QKeyValue.FindBoolAttribute(proc.Attributes, "stable")) return;

-

-            Program program = linearTypeChecker.program;

-            Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();

-            {

-                int i = proc.InParams.Count - linearTypeChecker.linearDomains.Count;

-                foreach (string domainName in linearTypeChecker.linearDomains.Keys)

-                {

-                    Variable inParam = proc.InParams[i];

-                    domainNameToInputVar[domainName] = inParam;

-                    i++;

-                }

-            }

-

-            // Collect the yield predicates and desugar yields

-            List<List<Cmd>> yields = new List<List<Cmd>>();

-            List<Cmd> cmds = new List<Cmd>();

-            if (proc.Requires.Count > 0)

-            {

-                Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();

-                foreach (var domainName in linearTypeChecker.linearDomains.Keys)

-                {

-                    domainNameToScope[domainName] = new HashSet<Variable>();

-                }

-                foreach (Variable v in program.GlobalVariables())

-                {

-                    var domainName = linearTypeChecker.FindDomainName(v);

-                    if (domainName == null) continue;

-                    if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

-                    domainNameToScope[domainName].Add(v);

-                }

-                for (int i = 0; i < proc.InParams.Count - linearTypeChecker.linearDomains.Count; i++)

-                {

-                    Variable v = proc.InParams[i];

-                    var domainName = linearTypeChecker.FindDomainName(v);

-                    if (domainName == null) continue;

-                    if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

-                    domainNameToScope[domainName].Add(v);

-                }

-                foreach (string domainName in linearTypeChecker.linearDomains.Keys)

-                {

-                    cmds.Add(new AssumeCmd(Token.NoToken, linearTypeChecker.DisjointnessExpr(domainName, domainNameToInputVar[domainName], domainNameToScope[domainName])));

-                }

-                foreach (Requires r in proc.Requires)

-                {

-                    if (r.Free)

-                    {

-                        cmds.Add(new AssumeCmd(r.tok, r.Condition));

-                    }

-                    else

-                    {

-                        AssertCmd assertCmd = new AssertCmd(r.tok, r.Condition, r.Attributes);

-                        assertCmd.ErrorData = "Non-interference check failed";

-                        cmds.Add(assertCmd);

-                    }

-                }

-                yields.Add(cmds);

-                cmds = new List<Cmd>();

-            }

-            if (proc.Ensures.Count > 0)

-            {

-                Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();

-                foreach (var domainName in linearTypeChecker.linearDomains.Keys)

-                {

-                    domainNameToScope[domainName] = new HashSet<Variable>();

-                }

-                foreach (Variable v in program.GlobalVariables())

-                {

-                    var domainName = linearTypeChecker.FindDomainName(v);

-                    if (domainName == null) continue;

-                    if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

-                    domainNameToScope[domainName].Add(v);

-                }

-                for (int i = 0; i < proc.OutParams.Count; i++)

-                {

-                    Variable v = proc.OutParams[i];

-                    var domainName = linearTypeChecker.FindDomainName(v);

-                    if (domainName == null) continue;

-                    if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

-                    domainNameToScope[domainName].Add(v);

-                }

-                foreach (string domainName in linearTypeChecker.linearDomains.Keys)

-                {

-                    cmds.Add(new AssumeCmd(Token.NoToken, linearTypeChecker.DisjointnessExpr(domainName, domainNameToInputVar[domainName], domainNameToScope[domainName])));

-                }

-                foreach (Ensures e in proc.Ensures)

-                {

-                    if (e.Free)

-                    {

-                        cmds.Add(new AssumeCmd(e.tok, e.Condition));

-                    }

-                    else

-                    {

-                        AssertCmd assertCmd = new AssertCmd(e.tok, e.Condition, e.Attributes);

-                        assertCmd.ErrorData = "Non-interference check failed";

-                        cmds.Add(assertCmd);

-                    }

-                }

-                yields.Add(cmds);

-                cmds = new List<Cmd>();

-            }

-            CreateYieldCheckerImpl(proc, yields, new Dictionary<Variable, Expr>());

-            CreateYieldCheckerImplForOldStableEnsures(proc);

-        }

-

-        private void AddYieldProcAndImpl() 

+        private void AddYieldProcAndImpl(List<Declaration> decls) 

         {

             if (yieldProc == null) return;

 

@@ -1192,16 +1022,6 @@ namespace Microsoft.Boogie
             decls.Add(yieldImpl);

         }

 

-        public static HashSet<int> FindPhaseNums(QKeyValue kv)

-        {

-            HashSet<int> attrs = QKeyValue.FindIntAttributes(kv, "phase");

-            if (attrs.Count == 0)

-            {

-                attrs.Add(0); // default phase of requires, ensures and assertions is 0

-            }

-            return attrs;

-        }

-

         public static QKeyValue RemoveYieldsAttribute(QKeyValue iter)

         {

             if (iter == null) return null;

@@ -1209,20 +1029,6 @@ namespace Microsoft.Boogie
             return (iter.Key == "yields") ? iter.Next : iter;

         }

 

-        public static QKeyValue RemoveStableAttribute(QKeyValue iter)

-        {

-            if (iter == null) return null;

-            iter.Next = RemoveStableAttribute(iter.Next);

-            return (iter.Key == "stable") ? iter.Next : iter;

-        }

-

-        public static QKeyValue RemoveQedAttribute(QKeyValue iter)

-        {

-            if (iter == null) return null;

-            iter.Next = RemoveQedAttribute(iter.Next);

-            return (iter.Key == "qed") ? iter.Next : iter;

-        }

-

         public static QKeyValue RemoveMoverAttribute(QKeyValue iter)

         {

             if (iter == null) return null;

@@ -1233,19 +1039,8 @@ namespace Microsoft.Boogie
                 return iter;

         }

 

-        private void Transform(List<Implementation> impls, List<Procedure> procs)

+        private void Collect(List<Declaration> decls)

         {

-            foreach (var impl in impls)

-            {

-                pc = null;

-                alpha = null;

-                beta = null;

-                TransformImpl(impl);

-            }

-            foreach (var proc in procs)

-            {

-                TransformProc(proc);

-            }

             foreach (Procedure proc in yieldCheckerProcs)

             {

                 decls.Add(proc);

@@ -1258,70 +1053,69 @@ namespace Microsoft.Boogie
             {

                 decls.Add(proc);

             }

-            AddYieldProcAndImpl();

+            AddYieldProcAndImpl(decls);

         }

 

         public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)

         {

             Program program = linearTypeChecker.program;

-            foreach (int phaseNum in moverTypeChecker.allPhaseNums)

+            foreach (int phaseNum in moverTypeChecker.AllPhaseNums)

             {

                 if (CommandLineOptions.Clo.TrustPhasesDownto <= phaseNum || phaseNum <= CommandLineOptions.Clo.TrustPhasesUpto) continue;

 

                 MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, phaseNum);

-                List<Implementation> impls = new List<Implementation>();

-                List<Procedure> procs = new List<Procedure>();

                 foreach (var decl in program.TopLevelDeclarations)

                 {

                     Procedure proc = decl as Procedure;

-                    if (proc == null || !QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;

+                    if (proc == null || !moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue;

                     Procedure duplicateProc = duplicator.VisitProcedure(proc);

-                    procs.Add(duplicateProc);

-                    if (moverTypeChecker.procToActionInfo.ContainsKey(proc) && moverTypeChecker.procToActionInfo[proc].phaseNum < phaseNum)

+                    decls.Add(duplicateProc);

+                    ActionInfo actionInfo = moverTypeChecker.procToActionInfo[proc];

+                    if (actionInfo.phaseNum < phaseNum)

                     {

-                        duplicateProc.Attributes = null;

-                        duplicateProc.Modifies = new List<IdentifierExpr>();

-                        program.GlobalVariables().Iter(x => duplicateProc.Modifies.Add(Expr.Ident(x)));

-                        CodeExpr action = (CodeExpr)duplicator.VisitCodeExpr(moverTypeChecker.procToActionInfo[proc].thisAction);

+                        Implementation impl;

+                        AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;

+                        if (atomicActionInfo != null)

+                        {

+                            CodeExpr action = (CodeExpr)duplicator.VisitCodeExpr(atomicActionInfo.thisAction);

 

-                        List<Cmd> cmds = new List<Cmd>();

-                        foreach (AssertCmd assertCmd in moverTypeChecker.procToActionInfo[proc].thisGate)

+                            List<Cmd> cmds = new List<Cmd>();

+                            foreach (AssertCmd assertCmd in atomicActionInfo.thisGate)

+                            {

+                                cmds.Add(new AssumeCmd(Token.NoToken, (Expr)duplicator.Visit(assertCmd.Expr)));

+                            }

+                            Block newInitBlock = new Block(Token.NoToken, "_init", cmds,

+                                new GotoCmd(Token.NoToken, new List<string>(new string[] { action.Blocks[0].Label }),

+                                                           new List<Block>(new Block[] { action.Blocks[0] })));

+                            List<Block> newBlocks = new List<Block>();

+                            newBlocks.Add(newInitBlock);

+                            newBlocks.AddRange(action.Blocks);

+                            impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, action.LocVars, newBlocks);

+                        }

+                        else

                         {

-                            cmds.Add(new AssumeCmd(Token.NoToken, (Expr)duplicator.Visit(assertCmd.Expr)));

+                            Block newInitBlock = new Block(Token.NoToken, "_init", new List<Cmd>(), new ReturnCmd(Token.NoToken));

+                            List<Block> newBlocks = new List<Block>();

+                            newBlocks.Add(newInitBlock);

+                            impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, new List<Variable>(), newBlocks);

                         }

-                        Block newInitBlock = new Block(Token.NoToken, "_init", cmds, 

-                            new GotoCmd(Token.NoToken, new List<string>(new string[] { action.Blocks[0].Label }), 

-                                                       new List<Block>(new Block[] { action.Blocks[0] })));

-                        List<Block> newBlocks = new List<Block>();

-                        newBlocks.Add(newInitBlock);

-                        newBlocks.AddRange(action.Blocks);

-                        Implementation impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, action.LocVars, newBlocks);

                         impl.Proc = duplicateProc;

                         impl.Proc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

                         impl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

-                        impls.Add(impl);

+                        decls.Add(impl);

                     }

                 }

+                OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator);

                 foreach (var decl in program.TopLevelDeclarations)

                 {

                     Implementation impl = decl as Implementation;

-                    if (impl == null || 

-                        !QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields") ||

-                        (moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) && moverTypeChecker.procToActionInfo[impl.Proc].phaseNum < phaseNum)) 

+                    if (impl == null || !moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].phaseNum < phaseNum)

                         continue;

                     Implementation duplicateImpl = duplicator.VisitImplementation(impl);

-                    impls.Add(duplicateImpl);

-                }

-                OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator, decls);

-                ogTransform.Transform(impls, procs);

-                foreach (var proc in procs)

-                {

-                    decls.Add(proc);

-                }

-                foreach (var impl in impls)

-                {

-                    decls.Add(impl);

+                    ogTransform.TransformImpl(duplicateImpl);

+                    decls.Add(duplicateImpl);

                 }

+                ogTransform.Collect(decls);

             }

         }

     }

diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs
index a3a621ac..915eadda 100644
--- a/Source/Concurrency/Program.cs
+++ b/Source/Concurrency/Program.cs
@@ -9,22 +9,18 @@ namespace Microsoft.Boogie
     {

         public static void Transform(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)

         {

-            // The order in which originalDecls are computed and then *.AddCheckers are called is 

-            // apparently important.  The MyDuplicator code currently does not duplicate Attributes.

-            // Consequently, all the yield attributes are eliminated by the AddCheckers code.

-

             List<Declaration> originalDecls = new List<Declaration>();

             Program program = linearTypeChecker.program;

             foreach (var decl in program.TopLevelDeclarations)

             {

                 Procedure proc = decl as Procedure;

-                if (proc != null && QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))

+                if (proc != null && moverTypeChecker.procToActionInfo.ContainsKey(proc))

                 {

                     originalDecls.Add(proc);

                     continue;

                 }

                 Implementation impl = decl as Implementation;

-                if (impl != null && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields"))

+                if (impl != null && moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc))

                 {

                     originalDecls.Add(impl);

                 }

@@ -38,17 +34,7 @@ namespace Microsoft.Boogie
             }

             foreach (Declaration decl in decls)

             {

-                Procedure proc = decl as Procedure;

-                if (proc != null && QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))

-                {

-                    proc.Modifies = new List<IdentifierExpr>();

-                    linearTypeChecker.program.GlobalVariables().Iter(x => proc.Modifies.Add(Expr.Ident(x)));

-                }

-            }

-            foreach (Declaration decl in decls)

-            {

                 decl.Attributes = OwickiGries.RemoveYieldsAttribute(decl.Attributes);

-                decl.Attributes = OwickiGries.RemoveStableAttribute(decl.Attributes);

             }

             program.TopLevelDeclarations.RemoveAll(x => originalDecls.Contains(x));

             program.TopLevelDeclarations.AddRange(decls);

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 5a8c81f6..2c4d8327 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -20,10 +20,31 @@ namespace Microsoft.Boogie
     public class ActionInfo

     {

         public Procedure proc;

-        public Ensures ensures;

-        public MoverType moverType;

         public int phaseNum;

         public int availableUptoPhaseNum;

+

+        public ActionInfo(Procedure proc, int phaseNum, int availableUptoPhaseNum)

+        {

+            this.proc = proc;

+            this.phaseNum = phaseNum;

+            this.availableUptoPhaseNum = availableUptoPhaseNum;

+        }

+

+        public virtual bool IsRightMover

+        {

+            get { return true; }

+        }

+

+        public virtual bool IsLeftMover

+        {

+            get { return true; }

+        }

+    }

+

+    public class AtomicActionInfo : ActionInfo

+    {

+        public Ensures ensures;

+        public MoverType moverType;

         public List<AssertCmd> thisGate;

         public CodeExpr thisAction;

         public List<Variable> thisInParams;

@@ -32,38 +53,36 @@ namespace Microsoft.Boogie
         public CodeExpr thatAction;

         public List<Variable> thatInParams;

         public List<Variable> thatOutParams;

-        public HashSet<Variable> usedGlobalVars;

+        public HashSet<Variable> actionUsedGlobalVars;

         public HashSet<Variable> modifiedGlobalVars;

         public HashSet<Variable> gateUsedGlobalVars;

         public bool hasAssumeCmd;

 

-        public bool CommutesWith(ActionInfo actionInfo)

+        public bool CommutesWith(AtomicActionInfo actionInfo)

         {

-            if (this.modifiedGlobalVars.Intersect(actionInfo.usedGlobalVars).Count() > 0)

+            if (this.modifiedGlobalVars.Intersect(actionInfo.actionUsedGlobalVars).Count() > 0)

                 return false;

-            if (this.usedGlobalVars.Intersect(actionInfo.modifiedGlobalVars).Count() > 0)

+            if (this.actionUsedGlobalVars.Intersect(actionInfo.modifiedGlobalVars).Count() > 0)

                 return false;

             return true;

         }

 

-        public bool IsRightMover

+        public override bool IsRightMover

         {

             get { return moverType == MoverType.Right || moverType == MoverType.Both; }

         }

 

-        public bool IsLeftMover

+        public override bool IsLeftMover

         {

             get { return moverType == MoverType.Left || moverType == MoverType.Both; }

         }

 

-        public ActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int phaseNum, int availableUptoPhaseNum)

+        public AtomicActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int phaseNum, int availableUptoPhaseNum)

+            : base(proc, phaseNum, availableUptoPhaseNum)

         {

             CodeExpr codeExpr = ensures.Condition as CodeExpr;

-            this.proc = proc;

             this.ensures = ensures;

             this.moverType = moverType;

-            this.phaseNum = phaseNum;

-            this.availableUptoPhaseNum = availableUptoPhaseNum;

             this.thisGate = new List<AssertCmd>();

             this.thisAction = codeExpr;

             this.thisInParams = new List<Variable>();

@@ -162,7 +181,7 @@ namespace Microsoft.Boogie
             {

                 VariableCollector collector = new VariableCollector();

                 collector.Visit(codeExpr);

-                this.usedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable));

+                this.actionUsedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable));

             }

 

             List<Variable> modifiedVars = new List<Variable>();

@@ -182,35 +201,96 @@ namespace Microsoft.Boogie
 

     public class MoverTypeChecker : ReadOnlyVisitor

     {

-        public int FindPhaseNumber(Procedure proc)

-        {

-            if (procToActionInfo.ContainsKey(proc))

-                return procToActionInfo[proc].phaseNum;

-            else

-                return int.MaxValue;

-        }

-

         CheckingContext checkingContext;

         public int errorCount;

-        public Dictionary<Variable, int> qedGlobalVariables;

+        public Dictionary<Variable, int> introducePhaseNums;

+        public Dictionary<Variable, int> hidePhaseNums;

         Procedure enclosingProc;

         public Dictionary<Procedure, ActionInfo> procToActionInfo;

         public Program program;

-        public HashSet<int> allPhaseNums;

-        bool inAtomicSpecification;

         bool inSpecification;

         int minPhaseNum;

+        int maxPhaseNum;

+        public Dictionary<Absy, HashSet<int>> absyToPhaseNums;

+

+        private static List<int> FindIntAttributes(QKeyValue kv, string name)

+        {

+            Contract.Requires(name != null);

+            HashSet<int> attrs = new HashSet<int>();

+            for (; kv != null; kv = kv.Next)

+            {

+                if (kv.Key != name) continue;

+                foreach (var o in kv.Params)

+                {

+                    Expr e = o as Expr;

+                    if (e == null) continue;

+                    LiteralExpr l = e as LiteralExpr;

+                    if (l != null && l.isBigNum)

+                        attrs.Add(l.asBigNum.ToIntSafe);

+                }

+            }

+            List<int> phases = attrs.ToList();

+            phases.Sort();

+            return phases;

+        }

+

+        private static MoverType GetMoverType(Ensures e)

+        {

+            if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))

+                return MoverType.Atomic;

+            if (QKeyValue.FindBoolAttribute(e.Attributes, "right"))

+                return MoverType.Right;

+            if (QKeyValue.FindBoolAttribute(e.Attributes, "left"))

+                return MoverType.Left;

+            if (QKeyValue.FindBoolAttribute(e.Attributes, "both"))

+                return MoverType.Both;

+            return MoverType.Top;

+        }

+

+        private HashSet<int> allPhaseNums;

+        public IEnumerable<int> AllPhaseNums

+        {

+            get

+            {

+                if (allPhaseNums == null)

+                {

+                    allPhaseNums = new HashSet<int>();

+                    foreach (ActionInfo actionInfo in procToActionInfo.Values)

+                    {

+                        allPhaseNums.Add(actionInfo.phaseNum);

+                    }

+                }

+                return allPhaseNums;

+            }

+        }

 

         public void TypeCheck()

         {

             foreach (Declaration decl in program.TopLevelDeclarations)

             {

                 Procedure proc = decl as Procedure;

-                if (proc == null) continue;

+                if (proc == null || !QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;

+

+                int phaseNum = int.MaxValue;

+                int availableUptoPhaseNum = int.MaxValue;

+                List<int> attrs = FindIntAttributes(proc.Attributes, "phase");

+                if (attrs.Count == 1)

+                {

+                    phaseNum = attrs[0];

+                }

+                else if (attrs.Count == 2)

+                {

+                    phaseNum = attrs[0];

+                    availableUptoPhaseNum = attrs[1];

+                }

+                else

+                {

+                    Error(proc, "Incorrect number of phases");

+                    continue;

+                }

                 foreach (Ensures e in proc.Ensures)

                 {

-                    int phaseNum, availableUptoPhaseNum;

-                    MoverType moverType = MoverCheck.GetMoverType(e, out phaseNum, out availableUptoPhaseNum);

+                    MoverType moverType = GetMoverType(e);

                     if (moverType == MoverType.Top) continue;

                     CodeExpr codeExpr = e.Condition as CodeExpr;

                     if (codeExpr == null)

@@ -223,19 +303,16 @@ namespace Microsoft.Boogie
                         Error(proc, "A procedure can have at most one atomic action");

                         continue;

                     }

-                    if (phaseNum >= availableUptoPhaseNum)

-                    {

-                        Error(proc, "Available at phase number should be less than available up to phase number");

-                        continue;

-                    }

-                    if (phaseNum != int.MaxValue)

-                    {

-                        allPhaseNums.Add(phaseNum);

-                    }

-                    procToActionInfo[proc] = new ActionInfo(proc, e, moverType, phaseNum, availableUptoPhaseNum);

+                    procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, phaseNum, availableUptoPhaseNum);

+                }

+                if (!procToActionInfo.ContainsKey(proc))

+                {

+                    procToActionInfo[proc] = new ActionInfo(proc, phaseNum, availableUptoPhaseNum);

                 }

             }

+            if (errorCount > 0) return;

             this.VisitProgram(program);

+            if (errorCount > 0) return;

 #if QED

             YieldTypeChecker.PerformYieldSafeCheck(this);

 #endif

@@ -243,132 +320,159 @@ namespace Microsoft.Boogie
 

         public MoverTypeChecker(Program program)

         {

-            this.qedGlobalVariables = new Dictionary<Variable, int>();

+            this.absyToPhaseNums = new Dictionary<Absy, HashSet<int>>();

+            this.introducePhaseNums = new Dictionary<Variable, int>();

+            this.hidePhaseNums = new Dictionary<Variable, int>();

+            this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();

+            this.errorCount = 0;

+            this.checkingContext = new CheckingContext(null);

+            this.program = program;

+            this.enclosingProc = null;

+            this.inSpecification = false;

+            this.minPhaseNum = int.MaxValue;

+            this.maxPhaseNum = -1;

             foreach (var g in program.GlobalVariables())

             {

-                if (QKeyValue.FindBoolAttribute(g.Attributes, "qed"))

+                List<int> phaseNums = FindIntAttributes(g.Attributes, "phase");

+                this.introducePhaseNums[g] = 0;

+                this.hidePhaseNums[g] = int.MaxValue;

+                if (phaseNums.Count == 0)

                 {

-                    this.qedGlobalVariables.Add(g, int.MaxValue);

-                    g.Attributes = OwickiGries.RemoveQedAttribute(g.Attributes);

+                    // ok

+                }

+                else if (phaseNums.Count == 1)

+                {

+                    this.hidePhaseNums[g] = phaseNums[0];

+                }

+                else if (phaseNums.Count == 2)

+                {

+                    this.introducePhaseNums[g] = phaseNums[0];

+                    this.hidePhaseNums[g] = phaseNums[1];

                 }

                 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);

+                    Error(g, "Too many phase numbers");

                 }

             }

-            this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();

-            this.allPhaseNums = new HashSet<int>();

-            this.errorCount = 0;

-            this.checkingContext = new CheckingContext(null);

-            this.program = program;

-            this.enclosingProc = null;

-            this.inAtomicSpecification = false;

-            this.inSpecification = false;

-            this.minPhaseNum = int.MaxValue;

         }

+        

         public override Implementation VisitImplementation(Implementation node)

         {

+            if (!procToActionInfo.ContainsKey(node.Proc))

+            {

+                return node;

+            }

             this.enclosingProc = node.Proc;

             return base.VisitImplementation(node);

         }

+        

         public override Procedure VisitProcedure(Procedure node)

         {

+            if (!procToActionInfo.ContainsKey(node))

+            {

+                return node;

+            }

             this.enclosingProc = node;

             return base.VisitProcedure(node);

         }

+

         public override Cmd VisitCallCmd(CallCmd node)

         {

-            if (!node.IsAsync)

+            int enclosingProcPhaseNum = procToActionInfo[enclosingProc].phaseNum;

+            if (procToActionInfo.ContainsKey(node.Proc))

             {

-                int enclosingProcPhaseNum = FindPhaseNumber(enclosingProc);

-                int calleePhaseNum = FindPhaseNumber(node.Proc);

-                if (enclosingProcPhaseNum == int.MaxValue)

-                {

-

-                }

-                else if (calleePhaseNum == int.MaxValue)

+                ActionInfo actionInfo = procToActionInfo[node.Proc];

+                if (node.IsAsync && actionInfo is AtomicActionInfo)

                 {

-                    Error(node, "An atomic procedure cannot call a non-atomic procedure");

+                    Error(node, "Target of async call cannot be an atomic action");

                 }

-                else if (enclosingProcPhaseNum <= calleePhaseNum)

+                int calleePhaseNum = procToActionInfo[node.Proc].phaseNum;

+                if (enclosingProcPhaseNum < calleePhaseNum ||

+                    (enclosingProcPhaseNum == calleePhaseNum && actionInfo is AtomicActionInfo))

                 {

                     Error(node, "The phase of the caller procedure must be greater than the phase of the callee");

                 }

-                else if (procToActionInfo[node.Proc].availableUptoPhaseNum < enclosingProcPhaseNum)

+                if (actionInfo.availableUptoPhaseNum < enclosingProcPhaseNum)

                 {

                     Error(node, "The callee is not available in the phase of the caller procedure");

                 }

             }

             return base.VisitCallCmd(node);

         }

+

         public override Cmd VisitParCallCmd(ParCallCmd node)

         {

+            int enclosingProcPhaseNum = procToActionInfo[enclosingProc].phaseNum;

+            bool isLeftMover = true;

+            bool isRightMover = true;

             int maxCalleePhaseNum = 0;

+            int numAtomicActions = 0;

             foreach (CallCmd iter in node.CallCmds)

             {

-                int calleePhaseNum = FindPhaseNumber(iter.Proc);

-                if (calleePhaseNum > maxCalleePhaseNum)

-                    maxCalleePhaseNum = calleePhaseNum;

-            }

-            int enclosingProcPhaseNum = FindPhaseNumber(enclosingProc);

-            if (enclosingProcPhaseNum > maxCalleePhaseNum)

-            {

-                bool isLeftMover = true;

-                bool isRightMover = true;

-                foreach (CallCmd iter in node.CallCmds)

-                {

-                    ActionInfo actionInfo = procToActionInfo[iter.Proc];

-                    isLeftMover = isLeftMover && actionInfo.IsLeftMover;

-                    isRightMover = isRightMover && actionInfo.IsRightMover;

+                ActionInfo actionInfo = procToActionInfo[iter.Proc];

+                isLeftMover = isLeftMover && actionInfo.IsLeftMover;

+                isRightMover = isRightMover && actionInfo.IsRightMover;

+                if (actionInfo.phaseNum > maxCalleePhaseNum)

+                { 

+                    maxCalleePhaseNum = actionInfo.phaseNum; 

                 }

-                if (!isLeftMover && !isRightMover && node.CallCmds.Count > 1)

+                if (actionInfo is AtomicActionInfo)

                 {

-                    Error(node, "The procedures in the parallel call must be all right mover or all left mover");

+                    numAtomicActions++;

                 }

-                return base.VisitParCallCmd(node);

             }

-            else

+            if (!isLeftMover && !isRightMover && node.CallCmds.Count > 1)

             {

-                return node;

+                Error(node, "The procedures in the parallel call must be all right mover or all left mover");

             }

+            if (maxCalleePhaseNum == enclosingProcPhaseNum && numAtomicActions > 0)

+            {

+                Error(node, "At phase {0}, either no callee is an atomic action or no callee phase equals the phase of the enclosing procedure");

+            }

+            return base.VisitParCallCmd(node);

         }

+        

         public override Expr VisitIdentifierExpr(IdentifierExpr node)

         {

             if (node.Decl is GlobalVariable)

             {

-                if (qedGlobalVariables.ContainsKey(node.Decl) && qedGlobalVariables[node.Decl] < minPhaseNum)

-                {

-                    minPhaseNum = qedGlobalVariables[node.Decl];

-                }

-

-                if (inAtomicSpecification && !qedGlobalVariables.ContainsKey(node.Decl))

+                if (!inSpecification)

                 {

-                    Error(node, "Cannot access non-qed global variable in atomic action");

+                    Error(node, "Global variable can be accessed only in atomic actions or specifications");

                 }

-                else if (!inSpecification && qedGlobalVariables.ContainsKey(node.Decl))

+                else

                 {

-                    Error(node, "Cannot access qed global variable in ordinary code");

+                    if (hidePhaseNums[node.Decl] < minPhaseNum)

+                    {

+                        minPhaseNum = hidePhaseNums[node.Decl];

+                    }

+                    if (introducePhaseNums[node.Decl] > maxPhaseNum)

+                    {

+                        maxPhaseNum = introducePhaseNums[node.Decl];

+                    }

                 }

             }

             return base.VisitIdentifierExpr(node);

         }

+        

         public override Ensures VisitEnsures(Ensures ensures)

         {

             minPhaseNum = int.MaxValue;

-            inAtomicSpecification = procToActionInfo.ContainsKey(enclosingProc) && procToActionInfo[enclosingProc].ensures == ensures;

+            maxPhaseNum = -1;

             inSpecification = true;

             Ensures ret = base.VisitEnsures(ensures);

             inSpecification = false;

-            if (inAtomicSpecification)

+            AtomicActionInfo atomicActionInfo = procToActionInfo[enclosingProc] as AtomicActionInfo;

+            if (atomicActionInfo != null && atomicActionInfo.ensures == ensures)

             {

-                if (procToActionInfo[enclosingProc].availableUptoPhaseNum > minPhaseNum)

+                if (maxPhaseNum <= atomicActionInfo.phaseNum && atomicActionInfo.availableUptoPhaseNum <= minPhaseNum)

+                {

+                    // ok

+                }

+                else 

                 {

                     Error(ensures, "A variable being accessed is hidden before this action becomes unavailable");

                 }

-                inAtomicSpecification = false;

             }

             else

             {

@@ -376,18 +480,22 @@ namespace Microsoft.Boogie
             }

             return ret;

         }

+        

         public override Requires VisitRequires(Requires requires)

         {

             minPhaseNum = int.MaxValue;

+            maxPhaseNum = -1;

             inSpecification = true;

             Requires ret = base.VisitRequires(requires);

             inSpecification = false;

             CheckAndAddPhases(requires, requires.Attributes);

             return ret;

         }

+        

         public override Cmd VisitAssertCmd(AssertCmd node)

         {

             minPhaseNum = int.MaxValue;

+            maxPhaseNum = -1;

             inSpecification = true;

             Cmd ret = base.VisitAssertCmd(node);

             inSpecification = false;

@@ -397,19 +505,26 @@ namespace Microsoft.Boogie
 

         private void CheckAndAddPhases(Absy node, QKeyValue attributes)

         {

-            foreach (int phaseNum in OwickiGries.FindPhaseNums(attributes))

+            List<int> attrs = FindIntAttributes(attributes, "phase");

+            if (attrs.Count == 0)

+            {

+                Error(node, "phase not present");

+                return;

+            }

+            absyToPhaseNums[node] = new HashSet<int>();

+            foreach (int phaseNum in attrs)

             {

-                if (phaseNum > FindPhaseNumber(enclosingProc))

+                if (phaseNum > procToActionInfo[enclosingProc].phaseNum)

                 {

                     Error(node, "The phase cannot be greater than the phase of enclosing procedure");

                 }

-                else if (phaseNum > minPhaseNum)

+                else if (maxPhaseNum < phaseNum && phaseNum <= minPhaseNum)

                 {

-                    Error(node, "A variable being accessed is hidden before this specification becomes unavailable");

+                    absyToPhaseNums[node].Add(phaseNum);

                 }

                 else

                 {

-                    allPhaseNums.Add(phaseNum);

+                    Error(node, string.Format("A variable being accessed in this specification is unavailable at phase {0}", phaseNum));

                 }

             }

         }

diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index 4ba23c2e..d976dfe2 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -75,7 +75,7 @@ namespace Microsoft.Boogie
             yieldTypeCheckerAutomatonEdges.Add(new Tuple<int, int, int>(source, label, dest));

         }

 

-        public void IsYieldTypeSafe()

+        private void IsYieldTypeSafe()

         {

             List<int[]> transitions = new List<int[]>();

             foreach (Tuple<int, int> e in edgeLabels.Keys)

@@ -150,7 +150,7 @@ namespace Microsoft.Boogie
             }

         }

 

-        static bool IsTerminatingLoopHeader(Block block)

+        private static bool IsTerminatingLoopHeader(Block block)

         {

             foreach (Cmd cmd in block.Cmds)

             {

@@ -163,7 +163,7 @@ namespace Microsoft.Boogie
             return false;

         }

         

-        public string PrintErrorTrace(Automaton<BvSet> errorAutomaton)

+        private string PrintErrorTrace(Automaton<BvSet> errorAutomaton)

         {

             String s = "\nBody of " + impl.Proc.Name + " is not yield_type_safe at phase " + currPhaseNum.ToString() + "\n";

             foreach (var move in errorAutomaton.GetMoves())

@@ -182,29 +182,19 @@ namespace Microsoft.Boogie
             foreach (var decl in moverTypeChecker.program.TopLevelDeclarations)

             {

                 Implementation impl = decl as Implementation;

-                if (impl == null) continue;

+                if (impl == null || !moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].phaseNum == 0) continue;

                 impl.PruneUnreachableBlocks();

                 Graph<Block> implGraph = Program.GraphFromImpl(impl);

                 implGraph.ComputeLoops();

-                int phaseNumSpecImpl = moverTypeChecker.FindPhaseNumber(impl.Proc);

-                foreach (int phaseNum in moverTypeChecker.allPhaseNums)

+                int specPhaseNum = moverTypeChecker.procToActionInfo[impl.Proc].phaseNum;

+                foreach (int phaseNum in moverTypeChecker.AllPhaseNums)

                 {

-                    if (phaseNum > phaseNumSpecImpl) continue;

+                    if (phaseNum > specPhaseNum) continue;

                     YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, phaseNum, implGraph.Headers);

                 }

             }

         }

 

-        public MoverType FindMoverType(Procedure proc)

-        {

-            if (!moverTypeChecker.procToActionInfo.ContainsKey(proc))

-                return MoverType.Top;

-            ActionInfo actionInfo = moverTypeChecker.procToActionInfo[proc];

-            if (actionInfo.phaseNum >= currPhaseNum)

-                return MoverType.Top;

-            return actionInfo.moverType;

-        }

-

         int stateCounter;

         MoverTypeChecker moverTypeChecker;

         Implementation impl;

@@ -216,7 +206,7 @@ namespace Microsoft.Boogie
         Dictionary<Tuple<int, int>, int> edgeLabels;

         IEnumerable<Block> loopHeaders;

 

-        public YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currPhaseNum, IEnumerable<Block> loopHeaders)

+        private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currPhaseNum, IEnumerable<Block> loopHeaders)

         {

             this.moverTypeChecker = moverTypeChecker;

             this.impl = impl;

@@ -283,11 +273,33 @@ namespace Microsoft.Boogie
                         CallCmd callCmd = cmd as CallCmd;

                         if (callCmd.IsAsync)

                         {

+                            ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];

+                            if (currPhaseNum <= actionInfo.phaseNum)

+                                edgeLabels[edge] = 'L';

+                            else

+                                edgeLabels[edge] = 'B';

+                        }

+                        else if (!moverTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc))

+                        {

                             edgeLabels[edge] = 'P';

                         }

                         else

                         {

-                            switch (FindMoverType(callCmd.Proc))

+                            MoverType moverType;

+                            ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];

+                            if (actionInfo.phaseNum >= currPhaseNum)

+                            {

+                                moverType = MoverType.Top;

+                            }

+                            else

+                            {

+                                AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;

+                                if (atomicActionInfo == null)

+                                    moverType = MoverType.Both;

+                                else

+                                    moverType = atomicActionInfo.moverType;

+                            }

+                            switch (moverType)

                             {

                                 case MoverType.Atomic:

                                     edgeLabels[edge] = 'A';

@@ -302,8 +314,7 @@ namespace Microsoft.Boogie
                                     edgeLabels[edge] = 'R';

                                     break;

                                 case MoverType.Top:

-                                    finalStates.Add(curr);

-                                    initialStates.Add(next);

+                                    edgeLabels[edge] = 'Y';

                                     break;

                             }

                         }

@@ -316,8 +327,7 @@ namespace Microsoft.Boogie
                         bool isLeftMover = true;

                         foreach (CallCmd callCmd in parCallCmd.CallCmds)

                         {

-                            int phaseSpecCallee = moverTypeChecker.FindPhaseNumber(callCmd.Proc);

-                            if (phaseSpecCallee >= currPhaseNum)

+                            if (moverTypeChecker.procToActionInfo[callCmd.Proc].phaseNum >= currPhaseNum)

                             {

                                 isYield = true;

                             }

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index cd7a8edd..72dc7c86 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1843,10 +1843,6 @@ namespace Microsoft.Boogie {
                   {

                       tc.Error(callCmd, "target procedure of a parallel call must yield");

                   }

-                  if (!QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "stable"))

-                  {

-                      tc.Error(callCmd, "target procedure of a parallel call must be stable");

-                  }

               }

           }

           foreach (CallCmd callCmd in CallCmds)

@@ -2134,10 +2130,6 @@ namespace Microsoft.Boogie {
             {

                 tc.Error(this, "target procedure of an async call must yield");

             }

-            if (!QKeyValue.FindBoolAttribute(Proc.Attributes, "stable"))

-            {

-                tc.Error(this, "target procedure of an async call must be stable");

-            }

         }

     }

 

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 10a13511..397d8eba 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -321,37 +321,6 @@ namespace Microsoft.Boogie {
       return defl;

     }

 

-    public static HashSet<Expr> FindExprAttributes(QKeyValue kv, string name)

-    {

-        Contract.Requires(name != null);

-        HashSet<Expr> attrs = new HashSet<Expr>();

-        for (; kv != null; kv = kv.Next)

-        {

-            if (kv.Key == name)

-            {

-                if (kv.Params.Count == 1 && kv.Params[0] is Expr)

-                {

-                    attrs.Add((Expr)kv.Params[0]);

-                }

-            }

-        }

-        return attrs;

-    }

-

-    public static HashSet<int> FindIntAttributes(QKeyValue kv, string name)

-    {

-        Contract.Requires(name != null);

-        HashSet<int> attrs = new HashSet<int>();

-        HashSet<Expr> es = FindExprAttributes(kv, name);

-        foreach (Expr e in es)

-        {

-            LiteralExpr l = e as LiteralExpr;

-            if (l != null && l.isBigNum)

-                attrs.Add(l.asBigNum.ToIntSafe);

-        }

-        return attrs;

-    }

-

     public override Absy Clone() {

       List<object> newParams = new List<object>();

       foreach (object o in Params)

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index e14d4fd3..c32a921b 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -42,7 +42,6 @@ namespace Microsoft.Boogie {
     static Procedure enclosingProc;

     static Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ modSets;

     static HashSet<Procedure> yieldingProcs;

-    static HashSet<Procedure> asyncAndParallelCallTargetProcs;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullDictionaryAndValues(modSets));

@@ -70,7 +69,6 @@ namespace Microsoft.Boogie {
 

       modSets = new Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>();

       yieldingProcs = new HashSet<Procedure>();

-      asyncAndParallelCallTargetProcs = new HashSet<Procedure>();

 

       HashSet<Procedure/*!*/> implementedProcs = new HashSet<Procedure/*!*/>();

       foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {

@@ -124,13 +122,6 @@ namespace Microsoft.Boogie {
               x.AddAttribute("yields");

           }

       }

-      foreach (Procedure x in asyncAndParallelCallTargetProcs)

-      {

-          if (!QKeyValue.FindBoolAttribute(x.Attributes, "stable"))

-          {

-              x.AddAttribute("stable");

-          }

-      }

 

 #if DEBUG_PRINT

       Console.WriteLine("Number of procedures with nonempty modsets = {0}", modSets.Keys.Count);

@@ -213,7 +204,6 @@ namespace Microsoft.Boogie {
       }

       if (callCmd.IsAsync)

       {

-          asyncAndParallelCallTargetProcs.Add(callCmd.Proc);

           if (!yieldingProcs.Contains(callCmd.Proc))

           {

               yieldingProcs.Add(callCmd.Proc);

@@ -234,7 +224,6 @@ namespace Microsoft.Boogie {
         }

         foreach (CallCmd callCmd in node.CallCmds)

         {

-            asyncAndParallelCallTargetProcs.Add(callCmd.Proc);

             if (!yieldingProcs.Contains(callCmd.Proc))

             {

                 yieldingProcs.Add(callCmd.Proc);

diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index 187b3ff8..c8510909 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -20,7 +20,7 @@ procedure C()
 

 function f(X): X;

 

-procedure {:yields} D()

+procedure {:yields} {:phase 1} D()

 {

     var {:linear "D"} a: X;

     var {:linear "D"} x: X;

@@ -58,7 +58,9 @@ procedure {:yields} D()
 

     call c, x := E(a, x);

 

+    yield;

     par a := F(a) | x := F(a);

+    yield;

 }

 

 procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)

@@ -66,9 +68,9 @@ procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X,
     c := a;

 }

 

-procedure {:yields} {:stable} F({:linear "D"} a: X) returns ({:linear "D"} c: X);

+procedure {:yields} {:phase 0} F({:linear "D"} a: X) returns ({:linear "D"} c: X);

 

-var{:linear "x"} g:int;

+var {:linear "x"} g:int;

 

 procedure G(i:int) returns({:linear "x"} r:int)

 {

@@ -81,23 +83,29 @@ modifies g;
   g := r;

 }

 

-procedure {:yields} {:stable} I({:linear ""} x:int) returns({:linear ""} x':int)

+procedure {:yields} {:phase 0} I({:linear ""} x:int) returns({:linear ""} x':int)

 {

   x' := x;

 }

 

-procedure {:yields} {:stable} J()

+procedure {:yields} {:phase 0} J()

 {

 }

 

-procedure {:yields} P1({:linear ""} x:int) returns({:linear ""} x':int)

+procedure {:yields} {:phase 1} P1({:linear ""} x:int) returns({:linear ""} x':int)

 {

+  yield;

   par x' := I(x) | J();

+  yield;

   call x' := I(x');

+  yield;

 }

 

-procedure {:yields} P2({:linear ""} x:int) returns({:linear ""} x':int)

+procedure {:yields} {:phase 1} P2({:linear ""} x:int) returns({:linear ""} x':int)

 {

+  yield;

   call x' := I(x);

+  yield;

   par x' := I(x') | J();

+  yield;

 }

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index dd2968ee..0f6383ef 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -1,10 +1,10 @@
 type X;

 function {:builtin "MapConst"} mapconstbool(bool): [X]bool;

 const nil: X;

-var {:qed} ghostLock: X;

-var {:qed} lock: X;

-var {:qed} currsize: int;

-var {:qed} newsize: int;

+var {:phase 1} ghostLock: X;

+var {:phase 1} lock: X;

+var {:phase 1} currsize: int;

+var {:phase 1} newsize: int;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

@@ -22,14 +22,14 @@ function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
     (ghostLock == nil <==> currsize == newsize)

 }

 

-procedure {:stable} {:yields} YieldToReadCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

+procedure {:yields} {:phase 1} YieldToReadCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

 requires {:phase 1} Inv(ghostLock, currsize, newsize) && tid' != nil;

 ensures {:phase 1} Inv(ghostLock, currsize, newsize) && tid != nil && tid == tid' && old(currsize) <= currsize;

 {

    tid := tid';

 }

 

-procedure {:stable} {:yields} YieldToWriteCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

+procedure {:yields} {:phase 1} YieldToWriteCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

 requires {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid' && tid' != nil;

 ensures {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && tid != nil && tid == tid' && old(currsize) == currsize && old(newsize) == newsize;

 {

@@ -39,7 +39,7 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && tid
 procedure Allocate({:linear "tid"} xls': [X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

 ensures {:phase 1} xl != nil;

 

-procedure {:entrypoint} {:yields} main({:linear "tid"} xls':[X]bool)

+procedure {:yields} {:phase 1} main({:linear "tid"} xls':[X]bool)

 requires {:phase 1} xls' == mapconstbool(true);

 {

     var {:linear "tid"} tid: X;

@@ -56,11 +56,15 @@ requires {:phase 1} xls' == mapconstbool(true);
     invariant {:phase 1} Inv(ghostLock, currsize, newsize);

     {

         call xls, tid := Allocate(xls);

+	yield;

+    	assert {:phase 1} Inv(ghostLock, currsize, newsize);

         async call Thread(tid);

+	yield;

+    	assert {:phase 1} Inv(ghostLock, currsize, newsize);

     }

 }

 

-procedure {:yields} {:stable} Thread({:linear "tid"} tid': X)

+procedure {:yields} {:phase 1} Thread({:linear "tid"} tid': X)

 requires {:phase 1} tid' != nil;

 requires {:phase 1} Inv(ghostLock, currsize, newsize);

 {

@@ -73,7 +77,7 @@ requires {:phase 1} Inv(ghostLock, currsize, newsize);
     call bytesRead := Read(tid, start, size);

 }

 

-procedure {:yields} Read({:linear "tid"} tid': X, start : int, size : int) returns (bytesRead : int)

+procedure {:yields} {:phase 1} Read({:linear "tid"} tid': X, start : int, size : int) returns (bytesRead : int)

 requires {:phase 1} tid' != nil;

 requires {:phase 1} 0 <= start && 0 <= size;

 requires {:phase 1} Inv(ghostLock, currsize, newsize);

@@ -115,7 +119,7 @@ COPY_TO_BUFFER:
     call tid := ReadCache(tid, start, bytesRead);

 }

 

-procedure {:yields} WriteCache({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X)

+procedure {:yields} {:phase 1} WriteCache({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X)

 requires {:phase 1} Inv(ghostLock, currsize, newsize);

 requires {:phase 1} ghostLock == tid' && tid' != nil;

 ensures {:phase 1} tid == tid' && ghostLock == tid;

@@ -137,7 +141,7 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsiz
     par tid := YieldToWriteCache(tid);

 }

 

-procedure {:yields} ReadCache({:linear "tid"} tid': X, start: int, bytesRead: int) returns ({:linear "tid"} tid: X)

+procedure {:yields} {:phase 1} ReadCache({:linear "tid"} tid': X, start: int, bytesRead: int) returns ({:linear "tid"} tid: X)

 requires {:phase 1} Inv(ghostLock, currsize, newsize);

 requires {:phase 1} tid' != nil;

 requires {:phase 1} 0 <= start && 0 <= bytesRead;

@@ -165,29 +169,29 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize);
     par tid := YieldToReadCache(tid);

 }

 

-procedure {:yields} Init({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool);

-ensures {:atomic 0} |{ A: assert xls' == mapconstbool(true); xls := xls'; currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|;

+procedure {:yields} {:phase 0,1} Init({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool);

+ensures {:atomic} |{ A: assert xls' == mapconstbool(true); xls := xls'; currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|;

 

-procedure {:yields} ReadCurrsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);

-ensures {:right 0} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := currsize; return true; }|;

+procedure {:yields} {:phase 0,1} ReadCurrsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);

+ensures {:right} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := currsize; return true; }|;

 

-procedure {:yields} ReadNewsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);

-ensures {:right 0} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := newsize; return true; }|;

+procedure {:yields} {:phase 0,1} ReadNewsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);

+ensures {:right} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := newsize; return true; }|;

 

-procedure {:yields} WriteNewsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);

-ensures {:atomic 0} |{A: assert tid' != nil; assert lock == tid' && ghostLock == nil; tid := tid'; newsize := val; ghostLock := tid; return true; }|;

+procedure {:yields} {:phase 0,1} WriteNewsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);

+ensures {:atomic} |{A: assert tid' != nil; assert lock == tid' && ghostLock == nil; tid := tid'; newsize := val; ghostLock := tid; return true; }|;

 

-procedure {:yields} WriteCurrsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);

-ensures {:atomic 0} |{A: assert tid' != nil; assert lock == tid' && ghostLock == tid'; tid := tid'; currsize := val; ghostLock := nil; return true; }|;

+procedure {:yields} {:phase 0,1} WriteCurrsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);

+ensures {:atomic} |{A: assert tid' != nil; assert lock == tid' && ghostLock == tid'; tid := tid'; currsize := val; ghostLock := nil; return true; }|;

 

-procedure {:yields} ReadCacheEntry({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X);

-ensures {:atomic 0} |{ A: assert 0 <= index && index < currsize; tid := tid'; return true; }|;

+procedure {:yields} {:phase 0,1} ReadCacheEntry({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X);

+ensures {:atomic} |{ A: assert 0 <= index && index < currsize; tid := tid'; return true; }|;

 

-procedure {:yields} WriteCacheEntry({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X);

-ensures {:right 0} |{ A: assert tid' != nil; assert currsize <= index && ghostLock == tid'; tid := tid'; return true; }|;

+procedure {:yields} {:phase 0,1} WriteCacheEntry({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X);

+ensures {:right} |{ A: assert tid' != nil; assert currsize <= index && ghostLock == tid'; tid := tid'; return true; }|;

 

-procedure {:yields} acquire({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);

-ensures {:right 0} |{ A: assert tid' != nil; tid := tid'; assume lock == nil; lock := tid; return true; }|;

+procedure {:yields} {:phase 0,1} acquire({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);

+ensures {:right} |{ A: assert tid' != nil; tid := tid'; assume lock == nil; lock := tid; return true; }|;

 

-procedure {:yields} release({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);

-ensures {:left 0} |{ A: assert tid' != nil; assert lock == tid'; tid := tid'; lock := nil; return true; }|;

+procedure {:yields} {:phase 0,1} release({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);

+ensures {:left} |{ A: assert tid' != nil; assert lock == tid'; tid := tid'; lock := nil; return true; }|;

diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index a263467c..e8df9515 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -1,7 +1,7 @@
 type X;

 const nil: X;

-var l: X;

-var x: int;

+var {:phase 1} l: X;

+var {:phase 1} x: int;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

@@ -10,44 +10,55 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
 }

 

 procedure Allocate() returns ({:linear "tid"} xls: X);

-ensures xls != nil;

+ensures {:phase 1} xls != nil;

 

-procedure {:entrypoint} {:yields} main()

+procedure {:yields} {:phase 1} main()

 {

     var {:linear "tid"} tid: X;

     var val: int;

 

     while (*) 

     {

+        yield;

         call tid := Allocate();

         havoc val;

         async call foo(tid, val);

+	yield;

     }

 }

+procedure {:yields} {:phase 0,1} Lock(tid: X);

+ensures {:atomic} |{A: assume l == nil; l := tid; return true; }|;

 

-procedure {:yields} {:stable} foo({:linear "tid"} tid': X, val: int)

-requires tid' != nil;

+procedure {:yields} {:phase 0,1} Unlock();

+ensures {:atomic} |{A: l := nil; return true; }|;

+

+procedure {:yields} {:phase 0,1} Set(val: int);

+ensures {:atomic} |{A: x := val; return true; }|;

+

+procedure {:yields} {:phase 1} foo({:linear "tid"} tid': X, val: int)

+requires {:phase 1} tid' != nil;

 {

     var {:linear "tid"} tid: X;

     tid := tid';

-    

-    assume l == nil;

-    l := tid;

+

+    yield;

+    call Lock(tid);    

     call tid := Yield(tid);

-    x := val;

+    call Set(val);

     call tid := Yield(tid);

-    assert x == val;

+    assert {:phase 1} x == val;

     call tid := Yield(tid);

-    l := nil;

+    call Unlock();

+    yield;

 }

 

-procedure {:yields} Yield({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

-requires tid' != nil;

-ensures tid == tid';

-ensures old(l) == tid ==> old(l) == l && old(x) == x;

+procedure {:yields} {:phase 1} Yield({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

+requires {:phase 1} tid' != nil;

+ensures {:phase 1} tid == tid';

+ensures {:phase 1} old(l) == tid ==> old(l) == l && old(x) == x;

 {

     tid := tid';

     yield;

-    assert tid != nil;

-    assert (old(l) == tid ==> old(l) == l && old(x) == x);

+    assert {:phase 1} tid != nil;

+    assert {:phase 1} (old(l) == tid ==> old(l) == l && old(x) == x);

 }
\ No newline at end of file
diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl
index d31c20ee..90ccfebe 100644
--- a/Test/og/akash.bpl
+++ b/Test/og/akash.bpl
@@ -17,18 +17,24 @@ function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool
 }

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

-ensures xls != 0;

+ensures {:phase 1} xls != 0;

 

 procedure Allocate_1() returns ({:linear "1"} xls: [int]bool);

-ensures xls == mapconstbool(true);

+ensures {:phase 1} xls == mapconstbool(true);

 

 procedure Allocate_2() returns ({:linear "2"} xls: [int]bool);

-ensures xls == mapconstbool(true);

+ensures {:phase 1} xls == mapconstbool(true);

 

-var g: int;

-var h: int;

+var {:phase 1} g: int;

+var {:phase 1} h: int;

 

-procedure {:yields} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

+procedure {:yields} {:phase 0,1} SetG(val:int);

+ensures {:atomic} |{A: g := val; return true; }|;

+

+procedure {:yields} {:phase 0,1} SetH(val:int);

+ensures {:atomic} |{A: h := val; return true; }|;

+

+procedure {:yields} {:phase 1} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

 {

     var {:linear "1"} x: [int]bool;

     var {:linear "2"} y: [int]bool;

@@ -37,51 +43,62 @@ procedure {:yields} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_
     call x := Allocate_1();

     call y := Allocate_2();

 

-    g := 0;

     yield;

-    assert g == 0 && x == mapconstbool(true);    

+    call SetG(0);

+    yield;

+    assert {:phase 1} g == 0 && x == mapconstbool(true);    

 

     yield;

     call tid_child := Allocate();

     async call B(tid_child, x);

 

     yield;

-    h := 0;

+    call SetH(0);

 

     yield;

-    assert h == 0 && y == mapconstbool(true);    

+    assert {:phase 1} h == 0 && y == mapconstbool(true);    

 

     yield;

     call tid_child := Allocate();

     async call C(tid_child, y);

+

+    yield;

 }

 

-procedure {:yields} {:stable} B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool) 

-requires x_in != mapconstbool(false);

+procedure {:yields} {:phase 1} B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool) 

+requires {:phase 1} x_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

     var {:linear "1"} x: [int]bool;

     tid_out := tid_in;

     x := x_in;    

 

-    g := 1;

+    yield;

+

+    call SetG(1);

 

     yield;

 

-    g := 2;

+    call SetG(2);

+

+    yield;

 }

 

-procedure {:yields} {:stable} C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool) 

-requires y_in != mapconstbool(false);

+procedure {:yields} {:phase 1} C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool) 

+requires {:phase 1} y_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

     var {:linear "2"} y: [int]bool;

     tid_out := tid_in;

     y := y_in;    

 

-    h := 1;

+    yield;

+

+    call SetH(1);

 

     yield;

 

-    h := 2;

+    call SetH(2);

+

+    yield;

 }
\ No newline at end of file
diff --git a/Test/og/async.bpl b/Test/og/async.bpl
index 32f609bc..4ca43d30 100644
--- a/Test/og/async.bpl
+++ b/Test/og/async.bpl
@@ -1,8 +1,7 @@
-var x: int;

-var y: int;

+var {:phase 1} x: int;

+var {:phase 1} y: int;

 

-procedure {:entrypoint} {:yields} foo()

-modifies x, y; 

+procedure {:yields} {:phase 1} foo()

 {

   assume x == y;

   x := x + 1;

@@ -10,8 +9,8 @@ modifies x, y;
   y := y + 1;

 }

 

-procedure {:yields} {:stable} P()

+procedure {:yields} {:phase 1} P()

 requires x != y;

 {

-  assert x != y;

+  assert {:phase 1} x != y;

 }
\ No newline at end of file
diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl
index 920fc32c..22751d29 100644
--- a/Test/og/bar.bpl
+++ b/Test/og/bar.bpl
@@ -1,36 +1,55 @@
-var g:int;

+var {:phase 1} g:int;

 

-procedure {:yields} {:stable} PB()

-modifies g;

+procedure {:yields} {:phase 1} PB()

 {

-  g := g + 1;

+  yield;

+  call Incr();

+  yield;

 }

 

-procedure {:yields} PC()

-ensures g == old(g);

+procedure {:yields} {:phase 0,1} Incr();

+ensures {:atomic}

+|{A:

+  g := g + 1; return true;

+}|;

+

+procedure {:yields} {:phase 0,1} Set(v: int);

+ensures {:atomic}

+|{A:

+  g := v; return true;

+}|;

+

+procedure {:yields} {:phase 1} PC()

+ensures {:phase 1} g == old(g);

 {

   yield;

-  assert g == old(g);

+  assert {:phase 1} g == old(g);

 }

 

-procedure {:yields} {:stable} PE()

+procedure {:yields} {:phase 1} PE()

 {

   call PC();

 }

 

-procedure {:yields} {:stable} PD()

+procedure {:yields} {:phase 1} PD()

 {

-  g := 3;

+  yield;

+  call Set(3);

   call PC();

-  assert g == 3;

+  assert {:phase 1} g == 3;

 }

 

-procedure{:entrypoint} {:yields} Main2()

+procedure {:yields} {:phase 1} Main2()

 {

+  yield;

   while (*)

   {

+    yield;

     async call PB();

+    yield;

     async call PE();

+    yield;

     async call PD();

+    yield;

   }

 }

diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl
index 27c700f3..378bb8b5 100644
--- a/Test/og/civl-paper.bpl
+++ b/Test/og/civl-paper.bpl
@@ -13,31 +13,31 @@ 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 {:qed} {:linear "mem"} g: lmap;

+var {:phase 2} {:linear "mem"} g: lmap;

 

 const p: int;

 

-procedure {:yields} TransferToGlobal({:cnst "tid"} tid: X, {:linear "mem"} l: lmap);

-ensures {:both 1} |{ A: assert tid != nil && lock == tid; g := l; return true; }|;

+procedure {:yields} {:phase 1,2} TransferToGlobal({:cnst "tid"} tid: X, {:linear "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);

 

-procedure {:yields} TransferFromGlobal({:cnst "tid"} tid: X) returns ({:linear "mem"} l: lmap);

-ensures {:both 1} |{ A: assert tid != nil && lock == tid; l := g; return true; }|;

+procedure {:yields} {:phase 1,2} TransferFromGlobal({:cnst "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);

 

-procedure {:yields} Load({:cnst "mem"} l: lmap, a: int) returns (v: int);

-ensures {:both 1} |{ A: v := map(l)[a]; return true; }|;

+procedure {:yields} {:phase 1} Load({:cnst "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} Store({:linear "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);

-ensures {:both 1} |{ A: assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|;

+procedure {:yields} {:phase 1} Store({:linear "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} P({:cnst "tid"} tid: X)

+procedure {:yields} {:phase 2} P({:cnst "tid"} tid: X)

 requires {:phase 1} InvLock(lock, b);

 ensures {:phase 1} InvLock(lock, b);

 requires {:phase 2} tid != nil && Inv(g);

@@ -58,7 +58,7 @@ ensures {:phase 2} Inv(g);
     par Yield() | YieldLock();

 }

 

-procedure {:yields} {:stable} Yield()

+procedure {:yields} {:phase 2} Yield()

 requires {:phase 2} Inv(g);

 ensures {:phase 2} Inv(g);

 {

@@ -72,13 +72,13 @@ function {:inline} Inv(g: lmap) : bool
 }

 

 

-var {:qed 1} b: bool;

-var {:qed} lock: X;

+var {:phase 1} b: bool;

+var {:phase 2} lock: X;

 

-procedure {:yields} Acquire({:cnst "tid"} tid: X)

+procedure {:yields} {:phase 1,2} Acquire({:cnst "tid"} tid: X)

 requires {:phase 1} InvLock(lock, b);

 ensures {:phase 1} InvLock(lock, b);

-ensures {:right 1} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;

+ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;

 {

     var status: bool;

     var tmp: X;

@@ -100,8 +100,8 @@ ensures {:right 1} |{ A: assert tid != nil; assume lock == nil; lock := tid; ret
 	goto L;

 }

 

-procedure {:yields} Release({:cnst "tid"} tid: X)

-ensures {:left 1} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|;

+procedure {:yields} {:phase 1,2} Release({:cnst "tid"} tid: X)

+ensures {:left} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|;

 requires {:phase 1} InvLock(lock, b);

 ensures {:phase 1} InvLock(lock, b);

 {

@@ -110,19 +110,19 @@ ensures {:phase 1} InvLock(lock, b);
     par YieldLock();

 }

 

-procedure {:yields} CAS(tid: X, prev: bool, next: bool) returns (status: bool);

-ensures {:atomic 0,1} |{ 

+procedure {:yields} {:phase 0,1} CAS(tid: X, prev: bool, next: bool) returns (status: bool);

+ensures {:atomic} |{ 

 A: goto B, C; 

 B: assume b == prev; b := next; status := true; lock := tid; return true; 

 C: status := false; return true; 

 }|;

 

-procedure {:yields} CLEAR(tid: X, next: bool);

-ensures {:atomic 0,1} |{ 

+procedure {:yields} {:phase 0,1} CLEAR(tid: X, next: bool);

+ensures {:atomic} |{ 

 A: b := next; lock := nil; return true; 

 }|;

 

-procedure {:yields} {:stable} YieldLock()

+procedure {:yields} {:phase 1} YieldLock()

 requires {:phase 1} InvLock(lock, b);

 ensures {:phase 1} InvLock(lock, b);

 {

diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl
index 831d2b97..400f5a4e 100644
--- a/Test/og/foo.bpl
+++ b/Test/og/foo.bpl
@@ -1,37 +1,55 @@
-var g:int;

+var {:phase 1} g:int;

 

-procedure {:yields} {:stable} PB()

-modifies g;

+procedure {:yields} {:phase 1} PB()

 {

-  g := g + 1;

+  yield;

+  call Incr();

+  yield;

 }

 

-procedure {:yields} PC()

-ensures g == 3;

+procedure {:yields} {:phase 0,1} Incr();

+ensures {:atomic}

+|{A:

+  g := g + 1; return true;

+}|;

+

+procedure {:yields} {:phase 0,1} Set(v: int);

+ensures {:atomic}

+|{A:

+  g := v; return true;

+}|;

+

+procedure {:yields} {:phase 1} PC()

+ensures {:phase 1} g == 3;

 {

-  g := 3;

   yield;

-  assert g == 3;

+  call Set(3);

+  yield;

+  assert {:phase 1} g == 3;

 }

 

-procedure {:yields} {:stable} PE()

+procedure {:yields} {:phase 1} PE()

 {

   call PC();

 }

 

-procedure {:yields} {:stable} PD()

+procedure {:yields} {:phase 1} PD()

 {

   call PC();

-  assert g == 3;

-  yield;

+  assert {:phase 1} g == 3;

 }

 

-procedure {:entrypoint} {:yields} Main()

+procedure {:yields} {:phase 1} Main()

 {

+  yield;

   while (*)

   {

+    yield;

     async call PB();

+    yield;

     async call PE();

+    yield;

     async call PD();

+    yield;

   }

 }

diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index ff3f5b1e..9effc04d 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -18,16 +18,26 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool
   xs

 }

 

-var x: int;

-var l: [X]bool;

+var {:phase 1} x: int;

+var {:phase 1} l: [X]bool;

 

 procedure Split({:linear "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);

 ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();

 

 procedure Allocate() returns ({:linear "tid"} xls: [X]bool);

 

-procedure {:entrypoint} {:yields} main({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool) 

-requires tidls' != None() && xls' == All();

+procedure {:yields} {:phase 0,1} Set(v: int);

+ensures {:atomic} |{A: x := v; return true; }|;

+

+procedure {:yields} {:phase 0,1} Lock(tidls: [X]bool);

+ensures {:atomic} |{A: assume l == None(); l := tidls; return true; }|;

+

+procedure {:yields} {:phase 0,1} Unlock();

+ensures {:atomic} |{A: l := None(); return true; }|;

+

+

+procedure {:yields} {:phase 1} main({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool) 

+requires {:phase 1} tidls' != None() && xls' == All();

 {

     var {:linear "tid"} tidls: [X]bool;

     var {:linear "x"} xls: [X]bool;

@@ -37,22 +47,25 @@ requires tidls' != None() && xls' == All();
 

     tidls := tidls';

     xls := xls';

-

-    x := 42;

     yield;

-    assert xls == All();

-    assert x == 42;

+    call Set(42);

+    yield;

+    assert {:phase 1} xls == All();

+    assert {:phase 1} x == 42;

     call xls1, xls2 := Split(xls);

     call lsChild := Allocate();

     assume (lsChild != None());

+    yield;

     async call thread(lsChild, xls1);

     call lsChild := Allocate();

     assume (lsChild != None());

+    yield;

     async call thread(lsChild, xls2);

+    yield;

 }

 

-procedure {:yields} {:stable} thread({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool)

-requires tidls' != None() && xls' != None();

+procedure {:yields} {:phase 1} thread({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool)

+requires {:phase 1} tidls' != None() && xls' != None();

 {

     var {:linear "x"} xls: [X]bool;

     var {:linear "tid"} tidls: [X]bool;

@@ -60,15 +73,15 @@ requires tidls' != None() && xls' != None();
     tidls := tidls';

     xls := xls';

 

-    assume l == None();

-    l := tidls;

     yield;

-    assert tidls != None() && xls != None();

-    x := 0;

+    call Lock(tidls);

+    yield;

+    assert {:phase 1} tidls != None() && xls != None();

+    call Set(0);

     yield;

-    assert tidls != None() && xls != None();

-    assert x == 0;

+    assert {:phase 1} tidls != None() && xls != None();

+    assert {:phase 1} x == 0;

+    assert {:phase 1} tidls != None() && xls != None();

+    call Unlock();

     yield;

-    assert tidls != None() && xls != None();

-    l := None();

 }

diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index 04406609..36a8f9c7 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -18,8 +18,8 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool
   xs

 }

 

-var x: int;

-var l: X;

+var {:phase 1} x: int;

+var {:phase 1} l: X;

 const nil: X;

 

 procedure Split({:linear "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);

@@ -28,8 +28,17 @@ ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
 procedure Allocate() returns ({:linear "tid"} xls: X);

 ensures xls != nil;

 

-procedure {:entrypoint}  {:yields} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool) 

-requires tidls' != nil && xls' == All();

+procedure {:yields} {:phase 0,1} Set(v: int);

+ensures {:atomic} |{A: x := v; return true; }|;

+

+procedure {:yields} {:phase 0,1} Lock(tidls: X);

+ensures {:atomic} |{A: assume l == nil; l := tidls; return true; }|;

+

+procedure {:yields} {:phase 0,1} Unlock();

+ensures {:atomic} |{A: l := nil; return true; }|;

+

+procedure {:yields} {:phase 1} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool) 

+requires {:phase 1} tidls' != nil && xls' == All();

 {

     var {:linear "tid"} tidls: X;

     var {:linear "x"} xls: [X]bool;

@@ -40,19 +49,23 @@ requires tidls' != nil && xls' == All();
     tidls := tidls';

     xls := xls';

 

-    x := 42;

     yield;

-    assert xls == All();

-    assert x == 42;

+    call Set(42);

+    yield;

+    assert {:phase 1} xls == All();

+    assert {:phase 1} x == 42;

     call xls1, xls2 := Split(xls);

     call lsChild := Allocate();

+    yield;

     async call thread(lsChild, xls1);

     call lsChild := Allocate();

+    yield;

     async call thread(lsChild, xls2);

+    yield;

 }

 

-procedure {:yields} {:stable} thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)

-requires tidls' != nil && xls' != None();

+procedure {:yields} {:phase 1} thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)

+requires {:phase 1} tidls' != nil && xls' != None();

 {

     var {:linear "x"} xls: [X]bool;

     var {:linear "tid"} tidls: X;

@@ -60,15 +73,16 @@ requires tidls' != nil && xls' != None();
     tidls := tidls';

     xls := xls';

 

-    assume l == nil;

-    l := tidls;

     yield;

-    assert tidls != nil && xls != None();

-    x := 0;

+    call Lock(tidls);

+    yield;

+    assert {:phase 1} tidls != nil && xls != None();

+    call Set(0);

+    yield;

+    assert {:phase 1} tidls != nil && xls != None();

+    assert {:phase 1} x == 0;

     yield;

-    assert tidls != nil && xls != None();

-    assert x == 0;

+    assert {:phase 1} tidls != nil && xls != None();

+    call Unlock();

     yield;

-    assert tidls != nil && xls != None();

-    l := nil;

 }

diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl
index 92b803a4..4a6e002d 100644
--- a/Test/og/lock.bpl
+++ b/Test/og/lock.bpl
@@ -1,14 +1,18 @@
-var {:qed} b: bool;

+var {:phase 2} b: bool;

 

-procedure {:yields} {:entrypoint} main()

+procedure {:yields} {:phase 2} main()

 {

     while (*)

     {

+        yield;

+

         async call Customer();

+

+        yield;

     }

 }

 

-procedure {:yields} {:stable} Customer()

+procedure {:yields} {:phase 2} Customer()

 {

     while (*) 

     {

@@ -19,13 +23,15 @@ procedure {:yields} {:stable} Customer()
     	yield;

 

     	call Leave();

+

+        yield;

     }

 

     yield;

 }

 

-procedure {:yields} Enter() 

-ensures {:atomic 1} |{ A: assume !b; b := true; return true; }|;

+procedure {:yields} {:phase 1,2} Enter() 

+ensures {:atomic} |{ A: assume !b; b := true; return true; }|;

 {

     var status: bool;

     yield;

@@ -44,12 +50,12 @@ ensures {:atomic 1} |{ A: assume !b; b := true; return true; }|;
 	goto L;

 }

 

-procedure {:yields} CAS(prev: bool, next: bool) returns (status: bool);

-ensures {:atomic 0} |{ 

+procedure {:yields} {:phase 0,2} CAS(prev: bool, next: bool) returns (status: bool);

+ensures {:atomic} |{ 

 A: goto B, C; 

 B: assume b == prev; b := next; status := true; return true; 

 C: status := false; return true; 

 }|;

 

-procedure {:yields} Leave();

-ensures {:atomic 0} |{ A: b := false; return true; }|;

+procedure {:yields} {:phase 0,2} Leave();

+ensures {:atomic} |{ A: b := false; return true; }|;

diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl
index 307d55c8..b173ecd4 100644
--- a/Test/og/lock2.bpl
+++ b/Test/og/lock2.bpl
@@ -1,14 +1,18 @@
-var {:qed} b: int;

+var {:phase 2} b: int;

 

-procedure {:yields} {:entrypoint} main()

+procedure {:yields} {:phase 2} main()

 {

     while (*)

     {

+        yield;

+

         async call Customer();

+

+        yield;

     }

 }

 

-procedure {:yields} {:stable} Customer()

+procedure {:yields} {:phase 2} Customer()

 {

     while (*) 

     {

@@ -19,13 +23,15 @@ procedure {:yields} {:stable} Customer()
     	yield;

 

     	call Leave();

+

+        yield;

     }

 

     yield;

 }

 

-procedure {:yields} Enter() 

-ensures {:atomic 1} |{ A: assume b == 0; b := 1; return true; }|;

+procedure {:yields} {:phase 1,2} Enter() 

+ensures {:atomic} |{ A: assume b == 0; b := 1; return true; }|;

 {

     var _old, curr: int;

     while (true) { 

@@ -46,15 +52,15 @@ ensures {:atomic 1} |{ A: assume b == 0; b := 1; return true; }|;
     }

 }

 

-procedure {:yields} Read() returns (val: int);

-ensures {:atomic 0} |{ A: val := b; return true; }|;

+procedure {:yields} {:phase 0,2} Read() returns (val: int);

+ensures {:atomic} |{ A: val := b; return true; }|;

 

-procedure {:yields} CAS(prev: int, next: int) returns (_old: int);

-ensures {:atomic 0} |{ 

+procedure {:yields} {:phase 0,2} CAS(prev: int, next: int) returns (_old: int);

+ensures {:atomic} |{ 

 A: _old := b; goto B, C; 

 B: assume _old == prev; b := next; return true; 

 C: assume _old != prev; return true; 

 }|;

 

-procedure {:yields} Leave();

-ensures {:atomic 0} |{ A: b := 0; return true; }|;

+procedure {:yields} {:phase 0,2} Leave();

+ensures {:atomic} |{ A: b := 0; return true; }|;

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 5bb056f3..3305b63f 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -4,10 +4,10 @@ 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;

+var elt : [int]int;

+var valid : [int]bool;

+var lock : [int]X;

+var owner : [int]X;

 const max : int;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

@@ -18,8 +18,8 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
 

 axiom (max > 0);

 

-procedure {:yields} acquire(i : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

-ensures {:right 0} |{ A: 

+procedure {:yields} {:phase 0} acquire(i : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+ensures {:right} |{ A: 

                       assert 0 <= i && i < max;

                       assert tidIn != nil && tidIn != done;

                       assume lock[i] == nil;

@@ -29,8 +29,8 @@ ensures {:right 0} |{ A:
                     }|;

 

 

-procedure {:yields} release(i : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

-ensures {:left 0} |{ A: 

+procedure {:yields} {:phase 0} release(i : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+ensures {:left} |{ A: 

                      assert 0 <= i && i < max;

                      assert lock[i] == tidIn;

                      assert tidIn != nil && tidIn != done; 

@@ -40,8 +40,8 @@ ensures {:left 0} |{ A:
                     }|;

 

 

-procedure {:yields} getElt(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, elt_j:int);

-ensures {:both 0,1} |{ A: 

+procedure {:yields} {:phase 0,1} getElt(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, elt_j:int);

+ensures {:both} |{ A: 

                      assert 0 <= j && j < max;

                      assert lock[j] == tidIn;

                      assert tidIn != nil && tidIn != done;

@@ -51,8 +51,8 @@ ensures {:both 0,1} |{ A:
                     }|;

 

 

-procedure {:yields} setElt(j : int, x : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

-ensures {:both 0,1} |{ A: 

+procedure {:yields} {:phase 0,1} setElt(j : int, x : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+ensures {:both} |{ A: 

                      assert x != null;

                      assert owner[j] == nil;

                      assert 0 <= j && j < max;

@@ -65,8 +65,8 @@ ensures {:both 0,1} |{ A:
                     }|;

 

 

-procedure {:yields} setEltToNull(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

-ensures {:left 0} |{ A: 

+procedure {:yields} {:phase 0} setEltToNull(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+ensures {:left} |{ A: 

                      assert owner[j] == tidIn;

                      assert 0 <= j && j < max;

                      assert lock[j] == tidIn;

@@ -78,8 +78,8 @@ ensures {:left 0} |{ A:
                      return true;

                     }|;

 

-procedure {:yields} setValid(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

-ensures {:both 0} |{ A: 

+procedure {:yields} {:phase 0} setValid(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+ensures {:both} |{ A: 

                      assert 0 <= j && j < max;

                      assert lock[j] == tidIn;

                      assert tidIn != nil && tidIn != done;

@@ -90,8 +90,8 @@ ensures {:both 0} |{ A:
                      return true;

                     }|;

 

-procedure {:yields} isEltThereAndValid(j : int, x : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, fnd:bool);

-ensures {:both 0} |{ A: 

+procedure {:yields} {:phase 0} isEltThereAndValid(j : int, x : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, fnd:bool);

+ensures {:both} |{ A: 

                        assert 0 <= j && j < max;

                        assert lock[j] == tidIn;

                        assert tidIn != nil && tidIn != done;

@@ -100,10 +100,10 @@ ensures {:both 0} |{ A:
                        return true;

                     }|;

 

-procedure {:yields} FindSlot(x : int, {:linear "tid"} tidIn: X) returns (r : int, {:linear "tid"} tidOut: X)

+procedure {:yields} {:phase 1} 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; 

+ensures {:right}  |{ A: assert tidIn != nil && tidIn != done; 

                           assert x != null; 

 			  goto B, C;

                        B: assume (0 <= r && r < max); 

@@ -159,12 +159,12 @@ ensures {:right 1}  |{ A: assert tidIn != nil && tidIn != done;
 	return;

 }

 

-procedure {:yields} Insert(x : int, {:linear "tid"} tidIn: X) returns (result : bool, {:linear "tid"} tidOut: X) 

+procedure {:yields} {:phase 2} Insert(x : int, {:linear "tid"} tidIn: X) returns (result : bool, {: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;

+ensures {:atomic}  |{ var r:int;

                         A: assert tidIn != nil && tidIn != done; 

                            assert x != null;

                            goto B, C;

@@ -204,7 +204,7 @@ ensures {:atomic 2}  |{ var r:int;
 	return;

 }

 

-procedure {:yields} InsertPair(x : int, 

+procedure {:yields} {:phase 2} InsertPair(x : int, 

                                y : int, 

                                {:linear "tid"} tidIn: X) 

                                returns (result : bool, 

@@ -213,7 +213,7 @@ 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;

+ensures {:atomic}  |{ var rx:int;

                         var ry:int;

                         A: assert tidIn != nil && tidIn != done; 

                            assert x != null && y != null;

@@ -285,12 +285,12 @@ ensures {:atomic 2}  |{ var rx:int;
 	return;

 }

 

-procedure {:yields} LookUp(x : int, {:linear "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"} tidIn: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool, {:linear "tid"} tidOut: X)

 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);

 ensures {:phase 1} {:phase 2} Inv(valid, elt, owner);

-ensures {:atomic 2}  |{ A: assert tidIn != nil && tidIn != done; 

+ensures {:atomic}  |{ A: assert tidIn != nil && tidIn != 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));

@@ -335,14 +335,13 @@ ensures {:atomic 2}  |{ A: assert tidIn != nil && tidIn != done;
 	return;

 }

 

-procedure {:yields} {:stable} Yield1()

+procedure {:yields} {:phase 1} Yield1()

 requires {:phase 1} Inv(valid, elt, owner);

 ensures {:phase 1} Inv(valid, elt, owner);

-ensures {:both 1} |{ A: return true; }|;

 {

 }

 

-procedure {:yields} {:stable} Yield12()

+procedure {:yields} {:phase 2} Yield12()

 requires {:phase 1} {:phase 2} Inv(valid, elt, owner);

 ensures {:phase 1} {:phase 2} Inv(valid, elt, owner);

 {

@@ -355,7 +354,7 @@ 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} {:stable} YieldLookUp(old_valid: [int]bool, old_elt: [int]int)

+procedure {:yields} {:phase 2} YieldLookUp(old_valid: [int]bool, old_elt: [int]int)

 requires {:phase 1} {:phase 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

 ensures {:phase 1} {:phase 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

 {

diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl
index 3ba0840d..6854e29c 100644
--- a/Test/og/new1.bpl
+++ b/Test/og/new1.bpl
@@ -1,6 +1,6 @@
 function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;

 

-var g:int;

+var {:phase 1} g:int;

 

 function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool

 {

@@ -11,30 +11,37 @@ procedure Allocate_Perm({:linear "Perm"} Permissions: [int]bool) returns ({:line
 requires Permissions == mapconstbool(true);

 ensures xls == mapconstbool(true);

 

-procedure {:yields} {:stable} PB({:linear "Perm"} permVar_in:[int]bool)

-requires permVar_in[0] && g == 0;

+procedure {:yields} {:phase 1} PB({:linear "Perm"} permVar_in:[int]bool)

+requires {:phase 1} permVar_in[0] && g == 0;

 {

   var {:linear "Perm"} permVar_out: [int]bool;

   permVar_out := permVar_in;

 

   yield;

-  assert permVar_out[0];

-  assert g == 0;

+  assert {:phase 1} permVar_out[0];

+  assert {:phase 1} g == 0;

 

-  g := g + 1;

+  call IncrG();

 

   yield;

-  assert permVar_out[0];

-  assert g == 1;

+  assert {:phase 1} permVar_out[0];

+  assert {:phase 1} g == 1;

 }

 

-procedure{:entrypoint} {:yields} Main({:linear "Perm"} Permissions: [int]bool)

-requires Permissions == mapconstbool(true);

+procedure {:yields} {:phase 1} Main({:linear "Perm"} Permissions: [int]bool)

+requires {:phase 0,1} Permissions == mapconstbool(true);

 {

   var {:linear "Perm"} permVar_out: [int]bool;

 

   call permVar_out := Allocate_Perm(Permissions);

-

-  g := 0;

+  yield;

+  call SetG(0);

   async call PB(permVar_out);

+  yield;

 }

+

+procedure {:yields} {:phase 0,1} SetG(val:int);

+ensures {:atomic} |{A: g := val; return true; }|;

+

+procedure {:yields} {:phase 0,1} IncrG();

+ensures {:atomic} |{A: g := g + 1; return true; }|;

diff --git a/Test/og/one.bpl b/Test/og/one.bpl
index 2a63d60d..1da2f116 100644
--- a/Test/og/one.bpl
+++ b/Test/og/one.bpl
@@ -1,4 +1,10 @@
-var x:int;

+var {:phase 1} x:int;

+

+procedure {:yields} {:phase 0,1} Set(v: int);

+ensures {:atomic}

+|{A:

+  x := v; return true;

+}|;

 

 procedure A()

 modifies x;

@@ -6,10 +12,11 @@ modifies x;
   x := x;

 }

 

-procedure {:yields} B()

+procedure {:yields} {:phase 1} B()

 {

-  x := 5;

   yield;

-  assert x == 5;

+  call Set(5);

+  yield;

+  assert {:phase 1} x == 5;

 }

 

diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl
index fc33d6cc..18050e09 100644
--- a/Test/og/parallel1.bpl
+++ b/Test/og/parallel1.bpl
@@ -1,27 +1,41 @@
-var g:int;

+var {:phase 1} g:int;

 

-procedure {:yields} {:stable} PB()

-modifies g;

+procedure {:yields} {:phase 1} PB()

 {

-  g := g + 1;

+  yield;

+  call Incr();

+  yield;

 }

 

-procedure {:yields} {:stable} PC()

-ensures g == 3;

+procedure {:yields} {:phase 0,1} Incr();

+ensures {:atomic}

+|{A:

+  g := g + 1; return true;

+}|;

+

+procedure {:yields} {:phase 0,1} Set(v: int);

+ensures {:atomic}

+|{A:

+  g := v; return true;

+}|;

+

+procedure {:yields} {:phase 1} PC()

+ensures {:phase 1} g == 3;

 {

-  g := 3;

   yield;

-  assert g == 3;

+  call Set(3);

+  yield;

+  assert {:phase 1} g == 3;

 }

 

-procedure {:yields} {:stable} PD()

+procedure {:yields} {:phase 1} PD()

 {

   call PC();

-  assert g == 3;

+  assert {:phase 1} g == 3;

   yield;

 }

 

-procedure {:entrypoint} {:yields} Main()

+procedure {:yields} {:phase 1} Main()

 {

   while (true)

   {

diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
index 07864511..4a3c1849 100644
--- a/Test/og/parallel2.bpl
+++ b/Test/og/parallel2.bpl
@@ -1,4 +1,4 @@
-var a:[int]int;

+var {:phase 1} a:[int]int;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

 function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

@@ -8,7 +8,10 @@ function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

-procedure {:entrypoint} {:yields} main() 

+procedure {:yields} {:phase 0,1} Write(idx: int, val: int);

+ensures {:atomic} |{A: a[idx] := val; return true; }|;

+

+procedure {:yields} {:phase 1} main() 

 {

     var {:linear "tid"} i: int;

     var {:linear "tid"} j: int;

@@ -18,29 +21,31 @@ procedure {:entrypoint} {:yields} main()
     par i := u(i) | j := u(j);

 }

 

-procedure {:yields} {:stable} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 {

     i := i';

 

-    a[i] := 42;

+    yield;

+    call Write(i, 42);

     call i := Yield(i);

-    assert a[i] == 42;

+    assert {:phase 1} a[i] == 42;

 }

 

-procedure {:yields} {:stable} u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

+procedure {:yields} {:phase 1} u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

 {

     i := i';

 

-    a[i] := 42;

     yield;

-    assert a[i] == 42;

+    call Write(i, 42);

+    yield;

+    assert {:phase 1} a[i] == 42;

 }

 

-procedure {:yields} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

-ensures i == i';

-ensures old(a)[i] == a[i];

+procedure {:yields} {:phase 1} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+ensures {:phase 1} i == i';

+ensures {:phase 1} old(a)[i] == a[i];

 {

     i := i';

     yield;

-    assert old(a)[i] == a[i];

+    assert {:phase 1} old(a)[i] == a[i];

 }
\ No newline at end of file
diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl
index 1069399f..2a2feb2d 100644
--- a/Test/og/parallel4.bpl
+++ b/Test/og/parallel4.bpl
@@ -1,4 +1,4 @@
-var a:int;

+var {:phase 1} a:int;

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

@@ -8,7 +8,7 @@ function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
   MapConstBool(false)[x := true]

 }

 

-procedure {:entrypoint} {:yields} main() 

+procedure {:yields} {:phase 1} main() 

 {

   var {:linear "tid"} i: int;

   var {:linear "tid"} j: int;

@@ -17,15 +17,19 @@ procedure {:entrypoint} {:yields} main()
   par i := t(i) | j := t(j);

 }

 

-procedure {:yields} {:stable} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 {

   i := i';

   call Yield();

-  assert a == old(a);

-  a := a + 1;

+  assert {:phase 1} a == old(a);

+  call Incr();

+  yield;

 }

 

-procedure {:yields} Yield()

+procedure {:yields} {:phase 0,1} Incr();

+ensures {:atomic} |{A: a := a + 1; return true; }|;

+

+procedure {:yields} {:phase 1} Yield()

 {

   yield;

 }

diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl
index 01bbe74d..330b970d 100644
--- a/Test/og/parallel5.bpl
+++ b/Test/og/parallel5.bpl
@@ -1,4 +1,4 @@
-var a:[int]int;

+var {:phase 1} a:[int]int;

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

@@ -8,7 +8,10 @@ function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
   MapConstBool(false)[x := true]

 }

 

-procedure {:entrypoint} {:yields} main() 

+procedure {:yields} {:phase 0,1} Write(idx: int, val: int);

+ensures {:atomic} |{A: a[idx] := val; return true; }|;

+

+procedure {:yields} {:phase 1} main() 

 {

     var {:linear "tid"} i: int;

     var {:linear "tid"} j: int;

@@ -18,29 +21,31 @@ procedure {:entrypoint} {:yields} main()
     par i := u(i) | j := u(j);

 }

 

-procedure {:yields} {:stable} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 {

     i := i';

 

-    a[i] := 42;

+    yield;

+    call Write(i, 42);

     call i := Yield(i);

-    assert a[i] == 42;

+    assert {:phase 1} a[i] == 42;

 }

 

-procedure {:yields} {:stable} u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

+procedure {:yields} {:phase 1} u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

 {

     i := i';

 

-    a[i] := 42;

     yield;

-    assert a[i] == 42;

+    call Write(i, 42);

+    yield;

+    assert {:phase 1} a[i] == 42;

 }

 

-procedure {:yields} {:stable} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

-ensures i == i';

-ensures old(a)[i] == a[i];

+procedure {:yields} {:phase 1} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+ensures {:phase 1} i == i';

+ensures {:phase 1} old(a)[i] == a[i];

 {

     i := i';

     yield;

-    assert old(a)[i] == a[i];

+    assert {:phase 1} old(a)[i] == a[i];

 }
\ No newline at end of file
diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl
index 8b77ce1b..6d07ca75 100644
--- a/Test/og/perm.bpl
+++ b/Test/og/perm.bpl
@@ -1,4 +1,4 @@
-var x: int;

+var {:phase 1} x: int;

 function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool;

 

 function {:builtin "MapOr"} ch_mapunion(x: [int]bool, y: [int]bool) : [int]bool;

@@ -12,44 +12,44 @@ procedure Split({:linear "Perm"} xls: [int]bool) returns ({:linear "Perm"} xls1:
   ensures xls == ch_mapunion(xls1, xls2) && xls1 != ch_mapconstbool(false) && xls2 != ch_mapconstbool(false);

 

 

-procedure {:entrypoint} {:yields} mainE({:linear "Perm"} permVar_in: [int]bool)

-   free requires permVar_in == ch_mapconstbool(true);

-   free requires permVar_in[0];

-  modifies x;

+procedure {:yields} {:phase 1} mainE({:linear "Perm"} permVar_in: [int]bool)

+   free requires {:phase 1} permVar_in == ch_mapconstbool(true);

+   free requires {:phase 1} permVar_in[0];

+   free requires {:phase 1} x == 0;

 {

     var {:linear "Perm"} permVar_out: [int]bool;

     var {:linear "Perm"} permVarOut2: [int]bool;

 

     permVar_out := permVar_in;

 

-    assume x == 0;

-

     yield;

-    assert x == 0;

-    assert permVar_out[0];

-    assert permVar_out == ch_mapconstbool(true);

+    assert {:phase 1} x == 0;

+    assert {:phase 1} permVar_out[0];

+    assert {:phase 1} permVar_out == ch_mapconstbool(true);

 

     call permVar_out, permVarOut2 := Split(permVar_out);

     async call foo(permVarOut2);

+    yield;

 }

 

-procedure {:yields} {:stable} foo({:linear "Perm"} permVar_in: [int]bool) 

-  free requires permVar_in != ch_mapconstbool(false);

-  free requires permVar_in[1];

-  requires x == 0;

-  modifies x;

+procedure {:yields} {:phase 1} foo({:linear "Perm"} permVar_in: [int]bool) 

+  free requires {:phase 1} permVar_in != ch_mapconstbool(false);

+  free requires {:phase 1} permVar_in[1];

+  requires {:phase 1} x == 0;

 {

   var {:linear "Perm"} permVar_out: [int]bool;

   permVar_out := permVar_in;

   

   yield;

-  assert permVar_out[1];

-  assert x == 0;

+  assert {:phase 1} permVar_out[1];

+  assert {:phase 1} x == 0;

 

-  x := x + 1;

+  call Incr();

 

   yield;

-  assert permVar_out[1];

-  assert x == 1;

+  assert {:phase 1} permVar_out[1];

+  assert {:phase 1} x == 1;

 }

 

+procedure {:yields} {:phase 0,1} Incr();

+ensures {:atomic} |{A: x := x + 1; return true; }|;
\ No newline at end of file
diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat
index 80f614ae..2a1d8ebb 100644
--- a/Test/og/runtest.bat
+++ b/Test/og/runtest.bat
@@ -9,7 +9,7 @@ for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl) do (
   %BGEXE% %* /nologo /noinfer %%f

 )

 

-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl akash.bpl t1.bpl new1.bpl perm.bpl async.bpl DeviceCache.bpl ticket.bpl lock.bpl lock2.bpl multiset.bpl civl-paper.bpl) do (

+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl parallel2.bpl parallel4.bpl parallel5.bpl akash.bpl t1.bpl new1.bpl perm.bpl DeviceCache.bpl ticket.bpl lock.bpl lock2.bpl multiset.bpl civl-paper.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f

diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl
index 43758a91..c7e30dd9 100644
--- a/Test/og/t1.bpl
+++ b/Test/og/t1.bpl
@@ -17,18 +17,24 @@ function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool
 }

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

-ensures xls != 0;

+ensures {:phase 1} xls != 0;

 

 procedure Allocate_1() returns ({:linear "1"} xls: [int]bool);

-ensures xls == mapconstbool(true);

+ensures {:phase 1} xls == mapconstbool(true);

 

 procedure Allocate_2() returns ({:linear "2"} xls: [int]bool);

-ensures xls == mapconstbool(true);

+ensures {:phase 1} xls == mapconstbool(true);

 

-var g: int;

-var h: int;

+var {:phase 1} g: int;

+var {:phase 1} h: int;

 

-procedure {:yields} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

+procedure {:yields} {:phase 0,1} SetG(val:int);

+ensures {:atomic} |{A: g := val; return true; }|;

+

+procedure {:yields} {:phase 0,1} SetH(val:int);

+ensures {:atomic} |{A: h := val; return true; }|;

+

+procedure {:yields} {:phase 1} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

 {

     var {:linear "1"} x: [int]bool;

     var {:linear "2"} y: [int]bool;

@@ -37,48 +43,55 @@ procedure {:yields} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_
     call x := Allocate_1();

     call y := Allocate_2();

 

-    g := 0;

     yield;

-    assert x == mapconstbool(true);    

-    assert g == 0;    

+    call SetG(0);

+    yield;

+    assert {:phase 1} x == mapconstbool(true);    

+    assert {:phase 1} g == 0;    

 

     yield;

     call tid_child := Allocate();

     async call B(tid_child, x);

 

     yield;

-    assert x == mapconstbool(true);    

-    assert g == 0;

+    assert {:phase 1} x == mapconstbool(true);    

+    assert {:phase 1} g == 0;

 

     yield;

-    h := 0;

+    call SetH(0);

 

     yield;

-    assert h == 0 && y == mapconstbool(true);    

+    assert {:phase 1} h == 0 && y == mapconstbool(true);    

 

     yield;

     call tid_child := Allocate();

     async call C(tid_child, y);

+

+    yield;

 }

 

-procedure {:yields} {:stable} B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool) 

-requires x_in != mapconstbool(false);

+procedure {:yields} {:phase 1} B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool) 

+requires {:phase 1} x_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

     var {:linear "1"} x: [int]bool;

     tid_out := tid_in;

     x := x_in;    

 

-    g := 1;

+    yield;

+    call SetG(1);

+    yield;

 }

 

-procedure {:yields} {:stable} C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool) 

-requires y_in != mapconstbool(false);

+procedure {:yields} {:phase 1} C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool) 

+requires {:phase 1} y_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

     var {:linear "2"} y: [int]bool;

     tid_out := tid_in;

     y := y_in;   

 

-    h := 1;

+    yield;

+    call SetH(1);

+    yield;

 }

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index 953230e7..ea08dcb5 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -6,10 +6,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 {:qed} t: int;

-var {:qed} s: int;

-var {:qed} cs: X;

-var {:qed} T: [int]bool;

+var {:phase 3} t: int;

+var {:phase 3} s: int;

+var {:phase 3} cs: X;

+var {:phase 3} T: [int]bool;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

@@ -34,7 +34,7 @@ function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool)
 procedure Allocate({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

 ensures {:phase 1} {:phase 2} xl != nil;

 

-procedure {:yields} {:entrypoint} main({:linear "tid"} xls':[X]bool)

+procedure {:yields} {:phase 3} main({:linear "tid"} xls':[X]bool)

 requires {:phase 3} xls' == mapconstbool(true);

 {

     var {:linear "tid"} tid: X;

@@ -50,12 +50,15 @@ requires {:phase 3} xls' == mapconstbool(true);
     invariant {:phase 1} Inv1(T, t);

     invariant {:phase 2} Inv2(T, s, cs);

     {

+	par Yield1() | Yield2() | Yield();

         call xls, tid := Allocate(xls);

         async call Customer(tid);

+    	par Yield1() | Yield2() | Yield();

+

     }

 }

 

-procedure {:yields} {:stable} Customer({:linear "tid"} tid': X)

+procedure {:yields} {:phase 3} Customer({:linear "tid"} tid': X)

 requires {:phase 1} Inv1(T, t);

 requires {:phase 2} tid' != nil && Inv2(T, s, cs);

 requires {:phase 3} true;

@@ -75,12 +78,12 @@ requires {:phase 3} true;
     }

 }

 

-procedure {:yields} Enter({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

+procedure {:yields} {:phase 2,3} Enter({:linear "tid"} tid': X) returns ({: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 2} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil; cs := tid; return true; }|;

+ensures {:right} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil; cs := tid; return true; }|;

 {

     var m: int;

 

@@ -92,10 +95,10 @@ ensures {:right 2} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil
     par Yield1() | Yield2();

 }

 

-procedure {:yields} GetTicketAbstract({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int)

+procedure {:yields} {:phase 1,2} 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,2} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; return true; }|;

+ensures {:right} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; return true; }|;

 {

     par Yield1();

     tid := tid';

@@ -103,33 +106,31 @@ ensures {:right 1,2} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true;
     par Yield1();

 }

 

-procedure {:yields} {:stable} Yield()

+procedure {:yields} {:phase 3} Yield()

 {

 }

 

-procedure {:yields} {:stable} Yield2()

+procedure {:yields} {:phase 2} Yield2()

 requires {:phase 2} Inv2(T, s, cs);

 ensures {:phase 2} Inv2(T, s, cs);

-ensures {:both 2} |{ A: return true; }|;

 {

 }

 

-procedure {:yields} {:stable} Yield1()

+procedure {:yields} {:phase 1} Yield1()

 requires {:phase 1} Inv1(T, t);

 ensures {:phase 1} Inv1(T,t);

-ensures {:both 1} |{ A: return true; }|;

 {

 }

 

-procedure {:yields} Init({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool);

-ensures {:atomic 0} |{ A: assert xls' == mapconstbool(true); xls := xls'; cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;

+procedure {:yields} {:phase 0,3} Init({:linear "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} GetTicket({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int);

-ensures {:atomic 0,1} |{ A: tid := tid'; m := t; t := t + 1; T[m] := true; return true; }|;

+procedure {:yields} {:phase 0,1} GetTicket({:linear "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} WaitAndEnter({:linear "tid"} tid': X, m:int) returns ({:linear "tid"} tid: X);

-ensures {:atomic 0,2} |{ A: tid := tid'; assume m <= s; cs := tid; return true; }|;

+procedure {:yields} {:phase 0,2} WaitAndEnter({:linear "tid"} tid': X, m:int) returns ({:linear "tid"} tid: X);

+ensures {:atomic} |{ 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; }|;

+procedure {:yields} {:phase 0,3} Leave({:linear "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; }|;