second checkpoint

14 files changed, 322 insertions, 267 deletions

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 5170383f..5414723e 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -7,6 +7,7 @@ using System.Threading.Tasks;
 using Microsoft.Boogie;

 using System.Diagnostics;

 using System.Diagnostics.Contracts;

+using Microsoft.Boogie.GraphUtil;

 

 namespace Microsoft.Boogie

 {

@@ -15,26 +16,31 @@ namespace Microsoft.Boogie
         MoverTypeChecker moverTypeChecker;

         public int phaseNum;

         Procedure enclosingProc;

+        Implementation enclosingImpl;

         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 List<Implementation> impls;

+

         public MyDuplicator(MoverTypeChecker moverTypeChecker, int phaseNum)

         {

             this.moverTypeChecker = moverTypeChecker;

             this.phaseNum = phaseNum;

             this.enclosingProc = null;

+            this.enclosingImpl = null;

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

+            this.impls = new List<Implementation>();

         }

 

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

         {

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

+            int enclosingProcPhaseNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].phaseNum;

             Procedure originalProc = originalCallCmd.Proc;

             if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc))

             {

@@ -145,17 +151,47 @@ namespace Microsoft.Boogie
                 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[node].phaseNum < phaseNum)

+

+                ActionInfo actionInfo = moverTypeChecker.procToActionInfo[node];

+                if (actionInfo.phaseNum < phaseNum)

                 {

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

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

+                    Implementation impl;

+                    AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;

+                    if (atomicActionInfo != null)

+                    {

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

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

+                        foreach (AssertCmd assertCmd in atomicActionInfo.thisGate)

+                        {

+                            cmds.Add(new AssumeCmd(Token.NoToken, (Expr)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, proc.Name, node.TypeParameters, node.InParams, node.OutParams, action.LocVars, newBlocks);

+                    }

+                    else

+                    {

+                        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, proc.Name, node.TypeParameters, node.InParams, node.OutParams, new List<Variable>(), newBlocks);

+                    }

+                    impl.Proc = proc;

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

                 }

                 else

                 {

@@ -164,7 +200,6 @@ namespace Microsoft.Boogie
                     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)));

             }

@@ -174,7 +209,7 @@ namespace Microsoft.Boogie
         private Variable dummyLocalVar;

         public override Implementation VisitImplementation(Implementation node)

         {

-            enclosingProc = node.Proc;

+            enclosingImpl = node;

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

             Implementation impl = base.VisitImplementation(node);

             implMap[impl] = node;

@@ -246,6 +281,12 @@ namespace Microsoft.Boogie
         List<Implementation> yieldCheckerImpls;

         Procedure yieldProc;

 

+        Variable pc;

+        Variable ok;

+        Expr alpha;

+        Expr beta;

+        HashSet<Variable> frame;

+

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

         {

             this.linearTypeChecker = linearTypeChecker;

@@ -381,12 +422,6 @@ namespace Microsoft.Boogie
             }

         }

 

-        Variable pc;

-        Variable ok;

-        Expr alpha;

-        Expr beta;

-        HashSet<Variable> frame;

-

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

         {

             Expr bb = Expr.True;

@@ -600,7 +635,7 @@ namespace Microsoft.Boogie
             yieldCheckerImpls.Add(yieldCheckerImpl);

         }

 

-        private bool IsYieldingHeader(GraphUtil.Graph<Block> graph, Block header)

+        private bool IsYieldingHeader(Graph<Block> graph, Block header)

         {

             foreach (Block backEdgeNode in graph.BackEdgeNodes(header))

             {

@@ -622,28 +657,18 @@ namespace Microsoft.Boogie
             return false;

         }

 

-        private bool IsYieldingCallCmd(CallCmd callCmd)

+        private Graph<Block> ComputeYieldingLoopHeaders(Implementation impl, out HashSet<Block> yieldingHeaders)

         {

-            return true;

-        }

-

-        private void TransformImpl(Implementation impl)

-        {

-            pc = null;

-            alpha = null;

-            beta = null;

-            frame = null;

-

-            // Find the yielding loop headers

+            Graph<Block> graph; 

             impl.PruneUnreachableBlocks();

             impl.ComputePredecessorsForBlocks();

-            GraphUtil.Graph<Block> graph = Program.GraphFromImpl(impl);

+            graph = Program.GraphFromImpl(impl);

             graph.ComputeLoops();

             if (!graph.Reducible)

             {

                 throw new Exception("Irreducible flow graphs are unsupported.");

             }

-            HashSet<Block> yieldingHeaders = new HashSet<Block>();

+            yieldingHeaders = new HashSet<Block>();

             IEnumerable<Block> sortedHeaders = graph.SortHeadersByDominance();

             foreach (Block header in sortedHeaders)

             {

@@ -660,15 +685,27 @@ namespace Microsoft.Boogie
                     continue;

                 }

             }

+            return graph;

+        }

+

+        private void SetupRefinementCheck(Implementation impl, 

+            out Dictionary<Variable, Expr> map,

+            out Dictionary<string, Variable> domainNameToInputVar, out Dictionary<string, Variable> domainNameToLocalVar, out Dictionary<Variable, Variable> ogOldGlobalMap)

+        {

+            pc = null;

+            ok = null;

+            alpha = null;

+            beta = null;

+            frame = null;

 

             Program program = linearTypeChecker.program;

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

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

             foreach (Variable local in impl.LocVars)

             {

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

                 map[local] = Expr.Ident(copy);

             }

-            Dictionary<Variable, Variable> ogOldGlobalMap = new Dictionary<Variable, Variable>();

+            ogOldGlobalMap = new Dictionary<Variable, Variable>();

             foreach (IdentifierExpr ie in globalMods)

             {

                 Variable g = ie.Decl;

@@ -744,8 +781,8 @@ namespace Microsoft.Boogie
                 }

             }

 

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

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

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

+            domainNameToLocalVar = new Dictionary<string, Variable>();

             {

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

                 foreach (string domainName in linearTypeChecker.linearDomains.Keys)

@@ -758,7 +795,31 @@ namespace Microsoft.Boogie
                     i++;

                 }

             }

+        }

+

+        private void TransformImpl(Implementation impl)

+        {

+            HashSet<Block> yieldingHeaders;

+            Graph<Block> graph = ComputeYieldingLoopHeaders(impl, out yieldingHeaders);

+

+            Dictionary<Variable, Expr> map;

+            Dictionary<string, Variable> domainNameToInputVar, domainNameToLocalVar;

+            Dictionary<Variable, Variable> ogOldGlobalMap;

+            SetupRefinementCheck(impl, out map, out domainNameToInputVar, out domainNameToLocalVar, out ogOldGlobalMap);

 

+            List<List<Cmd>> yields = CollectAndDesugarYields(impl, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap);

+

+            List<Variable> oldPcs, oldOks;

+            ProcessLoopHeaders(impl, graph, yieldingHeaders, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap, out oldPcs, out oldOks);

+

+            AddInitialBlock(impl, oldPcs, oldOks, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap);

+

+            CreateYieldCheckerImpl(impl, yields, map);

+        }

+

+        private List<List<Cmd>> CollectAndDesugarYields(Implementation impl,

+            Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap)

+        {

             // Collect the yield predicates and desugar yields

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

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

@@ -792,7 +853,7 @@ namespace Microsoft.Boogie
                             cmds.Add(pcmd);

                         }

                     }

-                    

+

                     if (cmd is CallCmd)

                     {

                         CallCmd callCmd = cmd as CallCmd;

@@ -864,9 +925,15 @@ namespace Microsoft.Boogie
                 }

                 b.Cmds = newCmds;

             }

+            return yields;

+        }

 

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

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

+        private void ProcessLoopHeaders(Implementation impl, Graph<Block> graph, HashSet<Block> yieldingHeaders, 

+            Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap,

+            out List<Variable> oldPcs, out List<Variable> oldOks)

+        {

+            oldPcs = new List<Variable>();

+            oldOks = new List<Variable>();

             foreach (Block header in yieldingHeaders)

             {

                 LocalVariable oldPc = null;

@@ -914,62 +981,62 @@ namespace Microsoft.Boogie
                 newCmds.AddRange(header.Cmds);

                 header.Cmds = newCmds;

             }

+        }

 

+        private void AddInitialBlock(Implementation impl, List<Variable> oldPcs, List<Variable> oldOks,

+            Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap)

+        {

+            // Add initial block

+            List<AssignLhs> lhss = new List<AssignLhs>();

+            List<Expr> rhss = new List<Expr>();

+            if (pc != null)

             {

-                // Add initial block

-                List<AssignLhs> lhss = new List<AssignLhs>();

-                List<Expr> rhss = new List<Expr>();

-                if (pc != null)

+                lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)));

+                rhss.Add(Expr.False);

+                foreach (Variable oldPc in oldPcs)

                 {

-                    lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)));

+                    lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)));

                     rhss.Add(Expr.False);

-                    foreach (Variable oldPc in oldPcs)

-                    {

-                        lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)));

-                        rhss.Add(Expr.False);

-                    }

-                    lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok)));

-                    rhss.Add(Expr.False);

-                    foreach (Variable oldOk in oldOks)

-                    {

-                        lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)));

-                        rhss.Add(Expr.False);

-                    }

-                }

-                Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();

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

-                {

-                    domainNameToExpr[domainName] = Expr.Ident(domainNameToInputVar[domainName]);

                 }

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

+                lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok)));

+                rhss.Add(Expr.False);

+                foreach (Variable oldOk in oldOks)

                 {

-                    Variable v = impl.InParams[i];

-                    var domainName = linearTypeChecker.FindDomainName(v);

-                    if (domainName == null) continue;

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

-                    var domain = linearTypeChecker.linearDomains[domainName];

-                    if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue;

-                    Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List<Expr> { Expr.Ident(v) });

-                    domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { ie, domainNameToExpr[domainName] });

-                }

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

-                {

-                    lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName])));

-                    rhss.Add(domainNameToExpr[domainName]);

-                }

-                foreach (Variable g in ogOldGlobalMap.Keys)

-                {

-                    lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g])));

-                    rhss.Add(Expr.Ident(g));

-                }

-                if (lhss.Count > 0)

-                {

-                    Block initBlock = new Block(Token.NoToken, "og_init", new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] }));

-                    impl.Blocks.Insert(0, initBlock);

+                    lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)));

+                    rhss.Add(Expr.False);

                 }

             }

-

-            CreateYieldCheckerImpl(impl, yields, map);

+            Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();

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

+            {

+                domainNameToExpr[domainName] = Expr.Ident(domainNameToInputVar[domainName]);

+            }

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

+            {

+                Variable v = impl.InParams[i];

+                var domainName = linearTypeChecker.FindDomainName(v);

+                if (domainName == null) continue;

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

+                var domain = linearTypeChecker.linearDomains[domainName];

+                if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue;

+                Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List<Expr> { Expr.Ident(v) });

+                domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { ie, domainNameToExpr[domainName] });

+            }

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

+            {

+                lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName])));

+                rhss.Add(domainNameToExpr[domainName]);

+            }

+            foreach (Variable g in ogOldGlobalMap.Keys)

+            {

+                lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g])));

+                rhss.Add(Expr.Ident(g));

+            }

+            if (lhss.Count > 0)

+            {

+                Block initBlock = new Block(Token.NoToken, "og_init", new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] }));

+                impl.Blocks.Insert(0, initBlock);

+            }

         }

 

         private void AddYieldProcAndImpl(List<Declaration> decls) 

@@ -1039,8 +1106,9 @@ namespace Microsoft.Boogie
                 return iter;

         }

 

-        private void Collect(List<Declaration> decls)

+        private List<Declaration> Collect()

         {

+            List<Declaration> decls = new List<Declaration>();

             foreach (Procedure proc in yieldCheckerProcs)

             {

                 decls.Add(proc);

@@ -1054,6 +1122,7 @@ namespace Microsoft.Boogie
                 decls.Add(proc);

             }

             AddYieldProcAndImpl(decls);

+            return decls;

         }

 

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

@@ -1070,41 +1139,8 @@ namespace Microsoft.Boogie
                     if (proc == null || !moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue;

                     Procedure duplicateProc = duplicator.VisitProcedure(proc);

                     decls.Add(duplicateProc);

-                    ActionInfo actionInfo = moverTypeChecker.procToActionInfo[proc];

-                    if (actionInfo.phaseNum < phaseNum)

-                    {

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

-                        {

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

-                        }

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

-                        decls.Add(impl);

-                    }

                 }

+                decls.AddRange(duplicator.impls);

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

                 foreach (var decl in program.TopLevelDeclarations)

                 {

@@ -1115,7 +1151,7 @@ namespace Microsoft.Boogie
                     ogTransform.TransformImpl(duplicateImpl);

                     decls.Add(duplicateImpl);

                 }

-                ogTransform.Collect(decls);

+                decls.AddRange(ogTransform.Collect());

             }

         }

     }

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 2c4d8327..8241d42b 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -206,6 +206,7 @@ namespace Microsoft.Boogie
         public Dictionary<Variable, int> introducePhaseNums;

         public Dictionary<Variable, int> hidePhaseNums;

         Procedure enclosingProc;

+        Implementation enclosingImpl;

         public Dictionary<Procedure, ActionInfo> procToActionInfo;

         public Program program;

         bool inSpecification;

@@ -328,6 +329,7 @@ namespace Microsoft.Boogie
             this.checkingContext = new CheckingContext(null);

             this.program = program;

             this.enclosingProc = null;

+            this.enclosingImpl = null;

             this.inSpecification = false;

             this.minPhaseNum = int.MaxValue;

             this.maxPhaseNum = -1;

@@ -362,7 +364,7 @@ namespace Microsoft.Boogie
             {

                 return node;

             }

-            this.enclosingProc = node.Proc;

+            this.enclosingImpl = node;

             return base.VisitImplementation(node);

         }

         

@@ -378,7 +380,7 @@ namespace Microsoft.Boogie
 

         public override Cmd VisitCallCmd(CallCmd node)

         {

-            int enclosingProcPhaseNum = procToActionInfo[enclosingProc].phaseNum;

+            int enclosingProcPhaseNum = procToActionInfo[enclosingImpl.Proc].phaseNum;

             if (procToActionInfo.ContainsKey(node.Proc))

             {

                 ActionInfo actionInfo = procToActionInfo[node.Proc];

@@ -392,6 +394,21 @@ namespace Microsoft.Boogie
                 {

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

                 }

+                else if (enclosingProcPhaseNum == calleePhaseNum && enclosingImpl.OutParams.Count > 0)

+                {

+                    HashSet<Variable> outParams = new HashSet<Variable>(enclosingImpl.OutParams);

+                    foreach (var x in node.Outs)

+                    {

+                        if (x.Decl is GlobalVariable)

+                        {

+                            Error(node, "Aglobal variable cannot be used as output argument for this call");

+                        }

+                        else if (outParams.Contains(x.Decl))

+                        {

+                            Error(node, "An output variable of the enclosing implementation cannot be used as output argument for this call");

+                        }

+                    }

+                }

                 if (actionInfo.availableUptoPhaseNum < enclosingProcPhaseNum)

                 {

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

@@ -402,7 +419,7 @@ namespace Microsoft.Boogie
 

         public override Cmd VisitParCallCmd(ParCallCmd node)

         {

-            int enclosingProcPhaseNum = procToActionInfo[enclosingProc].phaseNum;

+            int enclosingProcPhaseNum = procToActionInfo[enclosingImpl.Proc].phaseNum;

             bool isLeftMover = true;

             bool isRightMover = true;

             int maxCalleePhaseNum = 0;

@@ -462,10 +479,11 @@ namespace Microsoft.Boogie
             inSpecification = true;

             Ensures ret = base.VisitEnsures(ensures);

             inSpecification = false;

-            AtomicActionInfo atomicActionInfo = procToActionInfo[enclosingProc] as AtomicActionInfo;

+            ActionInfo actionInfo = procToActionInfo[enclosingProc];

+            AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;

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

             {

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

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

                 {

                     // ok

                 }

@@ -476,7 +494,7 @@ namespace Microsoft.Boogie
             }

             else

             {

-                CheckAndAddPhases(ensures, ensures.Attributes);

+                CheckAndAddPhases(ensures, ensures.Attributes, actionInfo.phaseNum);

             }

             return ret;

         }

@@ -488,7 +506,7 @@ namespace Microsoft.Boogie
             inSpecification = true;

             Requires ret = base.VisitRequires(requires);

             inSpecification = false;

-            CheckAndAddPhases(requires, requires.Attributes);

+            CheckAndAddPhases(requires, requires.Attributes, procToActionInfo[enclosingProc].phaseNum);

             return ret;

         }

         

@@ -499,11 +517,11 @@ namespace Microsoft.Boogie
             inSpecification = true;

             Cmd ret = base.VisitAssertCmd(node);

             inSpecification = false;

-            CheckAndAddPhases(node, node.Attributes);

+            CheckAndAddPhases(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].phaseNum);

             return ret;

         }

 

-        private void CheckAndAddPhases(Absy node, QKeyValue attributes)

+        private void CheckAndAddPhases(Absy node, QKeyValue attributes, int enclosingProcPhaseNum)

         {

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

             if (attrs.Count == 0)

@@ -514,7 +532,7 @@ namespace Microsoft.Boogie
             absyToPhaseNums[node] = new HashSet<int>();

             foreach (int phaseNum in attrs)

             {

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

+                if (phaseNum > enclosingProcPhaseNum)

                 {

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

                 }

diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index d976dfe2..6f356626 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -22,8 +22,12 @@ namespace Microsoft.Boogie
         static YieldTypeChecker()

         {

             yieldTypeCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);

-            yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.ReadFromRanges(0, new int[] { 0 },

+            yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.ReadFromRanges(3, new int[] { 0 },

                 new int[][] {

+                    new int[] {3, 'P', 'P', 3 },

+                    new int[] {3, 'Y', 'Y', 0 },

+                    new int[] {3, 'Y', 'Y', 1 },

+                    new int[] {3, 'Y', 'Y', 2 },

                     new int[] {0, 'P', 'P', 0 },

                     new int[] {0, 'Y', 'Y', 0 },

                     new int[] {0, 'Y', 'Y', 1 },

diff --git a/Test/linear/Answer b/Test/linear/Answer
index 9fabc440..ff1246e6 100644
--- a/Test/linear/Answer
+++ b/Test/linear/Answer
@@ -10,11 +10,11 @@ typecheck.bpl(51,4): Error: Only variable can be passed to linear parameter b
 typecheck.bpl(53,4): Error: The domains of formal and actual parameters must be the same

 typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same

 typecheck.bpl(57,4): Error: Only a linear argument can be passed to linear parameter a

-typecheck.bpl(61,4): Error: Linear variable a can occur only once as an input parameter of a parallel call

-typecheck.bpl(67,0): Error: Output variable d must be available at a return

-typecheck.bpl(76,0): Error: Global variable g must be available at a return

-typecheck.bpl(81,7): Error: unavailable source for a linear read

-typecheck.bpl(82,0): Error: Output variable r must be available at a return

+typecheck.bpl(62,4): Error: Linear variable a can occur only once as an input parameter of a parallel call

+typecheck.bpl(69,0): Error: Output variable d must be available at a return

+typecheck.bpl(78,0): Error: Global variable g must be available at a return

+typecheck.bpl(83,7): Error: unavailable source for a linear read

+typecheck.bpl(84,0): Error: Output variable r must be available at a return

 15 type checking errors detected in typecheck.bpl

 

 -------------------- list.bpl --------------------

diff --git a/Test/og/Answer b/Test/og/Answer
index a02a2838..b82acad4 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -1,59 +1,58 @@
 

 -------------------- foo.bpl --------------------

-foo.bpl(14,3): Error: Non-interference check failed

+foo.bpl(28,3): Error: Non-interference check failed

 Execution trace:

-    foo.bpl(6,5): anon0

-    (0,0): inline$Impl_YieldChecker_PC_0$0$L0

+    foo.bpl(5,3): anon0

+    foo.bpl(5,3): anon0$1

+    foo.bpl(12,3): inline$Incr_1$0$this_A

+    (0,0): inline$Impl_YieldChecker_PC_1$1$L0

 

-Boogie program verifier finished with 4 verified, 1 error

+Boogie program verifier finished with 9 verified, 1 error

 

 -------------------- bar.bpl --------------------

-bar.bpl(13,3): Error: Non-interference check failed

+bar.bpl(26,3): Error: Non-interference check failed

 Execution trace:

-    bar.bpl(6,5): anon0

-    (0,0): inline$Impl_YieldChecker_PC_0$0$L0

-bar.bpl(13,3): Error: Non-interference check failed

+    bar.bpl(5,3): anon0

+    bar.bpl(5,3): anon0$1

+    bar.bpl(12,3): inline$Incr_1$0$this_A

+    (0,0): inline$Impl_YieldChecker_PC_1$1$L0

+bar.bpl(26,3): Error: Non-interference check failed

 Execution trace:

-    bar.bpl(23,5): anon0

-    (0,0): inline$Impl_YieldChecker_PC_0$0$L0

+    bar.bpl(36,3): anon0

+    bar.bpl(36,3): anon0$1

+    (0,0): inline$Impl_YieldChecker_PC_1$1$L0

 

-Boogie program verifier finished with 3 verified, 2 errors

+Boogie program verifier finished with 8 verified, 2 errors

 

 -------------------- one.bpl --------------------

 

-Boogie program verifier finished with 2 verified, 0 errors

+Boogie program verifier finished with 3 verified, 0 errors

 

 -------------------- parallel1.bpl --------------------

-parallel1.bpl(10,1): Error: Non-interference check failed

-Execution trace:

-    parallel1.bpl(6,5): anon0

-    (0,0): inline$Proc_YieldChecker_PC_0$0$L0

-parallel1.bpl(14,3): Error: Non-interference check failed

+parallel1.bpl(28,3): Error: Non-interference check failed

 Execution trace:

-    parallel1.bpl(6,5): anon0

-    (0,0): inline$Impl_YieldChecker_PC_0$0$L0

+    parallel1.bpl(5,3): anon0

+    parallel1.bpl(5,3): anon0$1

+    parallel1.bpl(12,3): inline$Incr_1$0$this_A

+    (0,0): inline$Impl_YieldChecker_PC_1$1$L0

 

-Boogie program verifier finished with 3 verified, 2 errors

+Boogie program verifier finished with 7 verified, 1 error

 

 -------------------- linear-set.bpl --------------------

 

-Boogie program verifier finished with 2 verified, 0 errors

+Boogie program verifier finished with 4 verified, 0 errors

 

 -------------------- linear-set2.bpl --------------------

 

-Boogie program verifier finished with 2 verified, 0 errors

+Boogie program verifier finished with 4 verified, 0 errors

 

 -------------------- FlanaganQadeer.bpl --------------------

 

-Boogie program verifier finished with 3 verified, 0 errors

-

--------------------- DeviceCacheSimplified.bpl --------------------

-

-Boogie program verifier finished with 5 verified, 0 errors

+Boogie program verifier finished with 6 verified, 0 errors

 

 -------------------- parallel2.bpl --------------------

 

-Boogie program verifier finished with 4 verified, 0 errors

+Boogie program verifier finished with 8 verified, 0 errors

 

 -------------------- parallel4.bpl --------------------

 parallel4.bpl(24,3): Error BP5001: This assertion might not hold.

@@ -61,40 +60,35 @@ Execution trace:
     (0,0): og_init

     parallel4.bpl(22,5): anon0$1

 

-Boogie program verifier finished with 2 verified, 1 error

+Boogie program verifier finished with 5 verified, 1 error

 

 -------------------- parallel5.bpl --------------------

 

-Boogie program verifier finished with 4 verified, 0 errors

+Boogie program verifier finished with 8 verified, 0 errors

 

 -------------------- akash.bpl --------------------

 

-Boogie program verifier finished with 3 verified, 0 errors

+Boogie program verifier finished with 6 verified, 0 errors

 

 -------------------- t1.bpl --------------------

-t1.bpl(51,5): Error: Non-interference check failed

+t1.bpl(58,5): Error: Non-interference check failed

 Execution trace:

     (0,0): og_init

-    (0,0): inline$Impl_YieldChecker_A_0$0$L1

+    t1.bpl(78,13): anon0

+    t1.bpl(78,13): anon0$1

+    (0,0): inline$SetG_1$0$Entry

+    t1.bpl(78,13): anon0$2

+    (0,0): inline$Impl_YieldChecker_A_1$1$L2

 

-Boogie program verifier finished with 2 verified, 1 error

+Boogie program verifier finished with 5 verified, 1 error

 

 -------------------- new1.bpl --------------------

 

-Boogie program verifier finished with 2 verified, 0 errors

+Boogie program verifier finished with 4 verified, 0 errors

 

 -------------------- perm.bpl --------------------

 

-Boogie program verifier finished with 2 verified, 0 errors

-

--------------------- async.bpl --------------------

-async.bpl(14,1): Error: Non-interference check failed

-Execution trace:

-    async.bpl(7,3): anon0

-    async.bpl(7,3): anon0$1

-    (0,0): inline$Proc_YieldChecker_P_0$1$L0

-

-Boogie program verifier finished with 1 verified, 1 error

+Boogie program verifier finished with 4 verified, 0 errors

 

 -------------------- DeviceCache.bpl --------------------

 

@@ -106,11 +100,11 @@ Boogie program verifier finished with 28 verified, 0 errors
 

 -------------------- lock.bpl --------------------

 

-Boogie program verifier finished with 6 verified, 0 errors

+Boogie program verifier finished with 8 verified, 0 errors

 

 -------------------- lock2.bpl --------------------

 

-Boogie program verifier finished with 6 verified, 0 errors

+Boogie program verifier finished with 8 verified, 0 errors

 

 -------------------- multiset.bpl --------------------

 

@@ -118,4 +112,4 @@ Boogie program verifier finished with 85 verified, 0 errors
 

 -------------------- civl-paper.bpl --------------------

 

-Boogie program verifier finished with 29 verified, 0 errors

+Boogie program verifier finished with 28 verified, 0 errors

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index 0f6383ef..23f36ae5 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -22,18 +22,20 @@ function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
     (ghostLock == nil <==> currsize == newsize)

 }

 

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

+procedure {:yields} {:phase 1} YieldToReadCache({:cnst "tid"} tid: X)

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

+ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;

 {

-   tid := tid';

+   yield;

+   assert {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;

 }

 

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

+procedure {:yields} {:phase 1} YieldToWriteCache({:cnst "tid"} tid: X)

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

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

 {

-    tid := tid';

+    yield;

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

 }

 

 procedure Allocate({:linear "tid"} xls': [X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

@@ -47,7 +49,8 @@ requires {:phase 1} xls' == mapconstbool(true);
 

     yield;

 

-    call xls := Init(xls');

+    xls := xls';

+    call Init(xls);

     

     yield;

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

@@ -64,134 +67,127 @@ requires {:phase 1} xls' == mapconstbool(true);
     }

 }

 

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

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

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

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

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

 {

     var start, size, bytesRead: int;

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

 

-    tid := tid';

     havoc start, size;

     assume (0 <= start && 0 <= size);

     call bytesRead := Read(tid, start, size);

 }

 

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

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

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

 ensures {:phase 1} 0 <= bytesRead && bytesRead <= size;

 {

     var i, tmp: int;

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

-    tid := tid';

 

-    par  tid := YieldToReadCache(tid);

+    par YieldToReadCache(tid);

     bytesRead := size;

-    call tid := acquire(tid);

-    call tid, i := ReadCurrsize(tid);

-    call tid, tmp := ReadNewsize(tid);

+    call acquire(tid);

+    call i := ReadCurrsize(tid);

+    call tmp := ReadNewsize(tid);

     if (start + size <= i) {

-        call tid := release(tid); 

+        call release(tid); 

     	goto COPY_TO_BUFFER;

     } else if (tmp > i) {

         bytesRead := if (start <= i) then (i - start) else 0;

-    	call tid := release(tid); 

+    	call release(tid); 

 	goto COPY_TO_BUFFER;

     } else {

-        call tid := WriteNewsize(tid, start + size);

-    	call tid := release(tid); 

+        call WriteNewsize(tid, start + size);

+    	call release(tid); 

 	goto READ_DEVICE;

     }

 

 READ_DEVICE:

-    par  tid := YieldToWriteCache(tid);

-    call tid := WriteCache(tid, start + size);

-    par  tid := YieldToWriteCache(tid);

-    call tid := acquire(tid);

-    call tid, tmp := ReadNewsize(tid);

-    call tid := WriteCurrsize(tid, tmp);

-    call tid := release(tid);

+    par YieldToWriteCache(tid);

+    call WriteCache(tid, start + size);

+    par YieldToWriteCache(tid);

+    call acquire(tid);

+    call tmp := ReadNewsize(tid);

+    call WriteCurrsize(tid, tmp);

+    call release(tid);

 

 COPY_TO_BUFFER:

-    par tid := YieldToReadCache(tid);

-    call tid := ReadCache(tid, start, bytesRead);

+    par YieldToReadCache(tid);

+    call ReadCache(tid, start, bytesRead);

 }

 

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

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

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

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

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

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

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

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

 {

     var j: int;

-    tid := tid';

 

-    par tid := YieldToWriteCache(tid);

-    call tid, j := ReadCurrsize(tid);

+    par YieldToWriteCache(tid);

+    call j := ReadCurrsize(tid);

     while (j < index)

-    invariant {:phase 1} ghostLock == tid && currsize <= j && tid == tid';

+    invariant {:phase 1} ghostLock == tid && currsize <= j && tid == tid;

     invariant {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize;

     {

-        par tid := YieldToWriteCache(tid);

-        call tid := WriteCacheEntry(tid, j);

+        par YieldToWriteCache(tid);

+        call WriteCacheEntry(tid, j);

 	j := j + 1;

     }

-    par tid := YieldToWriteCache(tid);

+    par YieldToWriteCache(tid);

 }

 

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

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

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

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

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

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

 requires {:phase 1} (bytesRead == 0 || start + bytesRead <= currsize);

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

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

 {

     var j: int;

-    tid := tid';

 

-    par tid := YieldToReadCache(tid);

+    par YieldToReadCache(tid);

 

     j := 0;

     while(j < bytesRead)

     invariant {:phase 1} 0 <= j;

     invariant {:phase 1} bytesRead == 0 || start + bytesRead <= currsize; 

-    invariant {:phase 1} Inv(ghostLock, currsize, newsize) && tid == tid';

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

     {

 	assert {:phase 1} start + j < currsize;

-        call tid := ReadCacheEntry(tid, start + j);

+        call ReadCacheEntry(tid, start + j);

         j := j + 1;

-	par tid := YieldToReadCache(tid);

+	par YieldToReadCache(tid);

     }

 

-    par tid := YieldToReadCache(tid);

+    par YieldToReadCache(tid);

 }

 

-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} {:phase 0,1} Init({:cnst "tid"} xls:[X]bool);

+ensures {:atomic} |{ A: assert xls == mapconstbool(true); currsize := 0; newsize := 0; lock := nil; ghostLock := nil; 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} {:phase 0,1} ReadCurrsize({:cnst "tid"} tid: X) returns (val: int);

+ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := currsize; 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} {:phase 0,1} ReadNewsize({:cnst "tid"} tid: X) returns (val: int);

+ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := newsize; 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} {:phase 0,1} WriteNewsize({:cnst "tid"} tid: X, val: int);

+ensures {:atomic} |{A: assert tid != nil; assert lock == tid && ghostLock == nil; newsize := val; ghostLock := tid; 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} {:phase 0,1} WriteCurrsize({:cnst "tid"} tid: X, val: int);

+ensures {:atomic} |{A: assert tid != nil; assert lock == tid && ghostLock == tid; currsize := val; ghostLock := nil; 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} {:phase 0,1} ReadCacheEntry({:cnst "tid"} tid: X, index: int);

+ensures {:atomic} |{ A: assert 0 <= index && index < currsize; 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} {:phase 0,1} WriteCacheEntry({:cnst "tid"} tid: X, index: int);

+ensures {:right} |{ A: assert tid != nil; assert currsize <= index && ghostLock == 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} {:phase 0,1} acquire({:cnst "tid"} tid: X);

+ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; 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; }|;

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

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

diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index e8df9515..2fddf217 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -17,6 +17,7 @@ procedure {:yields} {:phase 1} main()
     var {:linear "tid"} tid: X;

     var val: int;

 

+    yield;

     while (*) 

     {

         yield;

diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl
index 4a6e002d..8357d36d 100644
--- a/Test/og/lock.bpl
+++ b/Test/og/lock.bpl
@@ -2,6 +2,7 @@ var {:phase 2} b: bool;
 

 procedure {:yields} {:phase 2} main()

 {

+    yield;

     while (*)

     {

         yield;

@@ -14,6 +15,7 @@ procedure {:yields} {:phase 2} main()
 

 procedure {:yields} {:phase 2} Customer()

 {

+    yield;

     while (*) 

     {

     	yield;

@@ -26,8 +28,6 @@ procedure {:yields} {:phase 2} Customer()
 

         yield;

     }

-

-    yield;

 }

 

 procedure {:yields} {:phase 1,2} Enter() 

diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl
index b173ecd4..9f5e0be8 100644
--- a/Test/og/lock2.bpl
+++ b/Test/og/lock2.bpl
@@ -2,6 +2,7 @@ var {:phase 2} b: int;
 

 procedure {:yields} {:phase 2} main()

 {

+    yield;

     while (*)

     {

         yield;

@@ -14,6 +15,7 @@ procedure {:yields} {:phase 2} main()
 

 procedure {:yields} {:phase 2} Customer()

 {

+    yield;

     while (*) 

     {

     	yield;

@@ -26,14 +28,13 @@ procedure {:yields} {:phase 2} Customer()
 

         yield;

     }

-

-    yield;

 }

 

 procedure {:yields} {:phase 1,2} Enter() 

 ensures {:atomic} |{ A: assume b == 0; b := 1; return true; }|;

 {

     var _old, curr: int;

+    yield;

     while (true) { 

     	yield;

         call _old := CAS(0, 1);

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 3305b63f..459cb470 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -339,6 +339,8 @@ procedure {:yields} {:phase 1} Yield1()
 requires {:phase 1} Inv(valid, elt, owner);

 ensures {:phase 1} Inv(valid, elt, owner);

 {

+	yield;

+	assert {:phase 1} Inv(valid, elt, owner);

 }

 

 procedure {:yields} {:phase 2} Yield12()

diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl
index 18050e09..427dc72d 100644
--- a/Test/og/parallel1.bpl
+++ b/Test/og/parallel1.bpl
@@ -37,7 +37,8 @@ procedure {:yields} {:phase 1} PD()
 

 procedure {:yields} {:phase 1} Main()

 {

-  while (true)

+  yield;

+  while (*)

   {

     par PB() | PC() | PD();

   }

diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
index 4a3c1849..1bce7c8a 100644
--- a/Test/og/parallel2.bpl
+++ b/Test/og/parallel2.bpl
@@ -27,7 +27,7 @@ procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid
 

     yield;

     call Write(i, 42);

-    call i := Yield(i);

+    call Yield(i);

     assert {:phase 1} a[i] == 42;

 }

 

@@ -41,11 +41,9 @@ procedure {:yields} {:phase 1} u({:linear "tid"} i': int) returns ({:linear "tid
     assert {:phase 1} a[i] == 42;

 }

 

-procedure {:yields} {:phase 1} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

-ensures {:phase 1} i == i';

+procedure {:yields} {:phase 1} Yield({:cnst "tid"} i: int)

 ensures {:phase 1} old(a)[i] == a[i];

 {

-    i := i';

     yield;

     assert {:phase 1} old(a)[i] == a[i];

 }
\ No newline at end of file
diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl
index 330b970d..a73af06e 100644
--- a/Test/og/parallel5.bpl
+++ b/Test/og/parallel5.bpl
@@ -17,7 +17,7 @@ procedure {:yields} {:phase 1} main()
     var {:linear "tid"} j: int;

     call i := Allocate();

     call j := Allocate();

-    par i := t(i) | j := Yield(j);

+    par i := t(i) | Yield(j);

     par i := u(i) | j := u(j);

 }

 

@@ -27,7 +27,7 @@ procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid
 

     yield;

     call Write(i, 42);

-    call i := Yield(i);

+    call Yield(i);

     assert {:phase 1} a[i] == 42;

 }

 

@@ -41,11 +41,9 @@ procedure {:yields} {:phase 1} u({:linear "tid"} i': int) returns ({:linear "tid
     assert {:phase 1} a[i] == 42;

 }

 

-procedure {:yields} {:phase 1} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

-ensures {:phase 1} i == i';

+procedure {:yields} {:phase 1} Yield({:cnst "tid"} i: int)

 ensures {:phase 1} old(a)[i] == a[i];

 {

-    i := i';

     yield;

     assert {:phase 1} old(a)[i] == a[i];

 }
\ No newline at end of file
diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index ea08dcb5..fb347935 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -65,7 +65,8 @@ requires {:phase 3} true;
 {

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

     tid := tid';

-

+    

+    par Yield1() | Yield2() | Yield();    

     while (*) 

     invariant {:phase 1} Inv1(T, t);

     invariant {:phase 2} tid != nil && Inv2(T, s, cs);

@@ -108,18 +109,23 @@ ensures {:right} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; retu
 

 procedure {:yields} {:phase 3} Yield()

 {

+    yield;

 }

 

 procedure {:yields} {:phase 2} Yield2()

 requires {:phase 2} Inv2(T, s, cs);

 ensures {:phase 2} Inv2(T, s, cs);

 {

+    yield;

+    assert {:phase 2} Inv2(T, s, cs);

 }

 

 procedure {:yields} {:phase 1} Yield1()

 requires {:phase 1} Inv1(T, t);

 ensures {:phase 1} Inv1(T,t);

 {

+    yield;

+    assert {:phase 1} Inv1(T,t);

 }

 

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