simplified yield type chcking and added treiber stack (not fully done)

20 files changed, 363 insertions, 151 deletions

diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs
index fc44468c..6675e809 100644
--- a/Source/Concurrency/LinearSets.cs
+++ b/Source/Concurrency/LinearSets.cs
@@ -154,6 +154,16 @@ namespace Microsoft.Boogie
         }

         public override Implementation VisitImplementation(Implementation node)

         {

+            node.PruneUnreachableBlocks();

+            node.ComputePredecessorsForBlocks();

+            GraphUtil.Graph<Block> graph = Program.GraphFromImpl(node);

+            graph.ComputeLoops();

+            if (!graph.Reducible)

+            {

+                Error(node, "A loop in the implementation is not reducible");

+                return node;

+            }

+

             HashSet<Variable> start = new HashSet<Variable>(globalVarToDomainName.Keys);

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

             {

@@ -223,6 +233,15 @@ namespace Microsoft.Boogie
                     }

                 }

             }

+

+            foreach (Block header in graph.Headers)

+            {

+                foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(availableLinearVars[header]))

+                {

+                    Error(header, string.Format("Global variable {0} must be available at a loop head", g.Name));

+                }

+            }

+

             return impl;

         }

         public void AddAvailableVars(CallCmd callCmd, HashSet<Variable> start)

@@ -566,6 +585,12 @@ namespace Microsoft.Boogie
                 var domainName = FindDomainName(v);

                 domainNameToScope[domainName].Add(v);

             }

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

+            {

+                var domainName = FindDomainName(v);

+                if (domainName == null) continue;

+                domainNameToScope[domainName].Add(v);

+            }

             foreach (string domainName in linearDomains.Keys)

             {

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

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 167d9f2c..1147760f 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -640,7 +640,7 @@ namespace Microsoft.Boogie
             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("{0}_YieldChecker_{1}", impl is Procedure ? "Proc" : "Impl", impl.Name);

+            var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", "Impl", impl.Name);

             var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, impl.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);

diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index d278ad69..98657706 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -13,91 +13,109 @@ namespace Microsoft.Boogie
 {

     class YieldTypeChecker

     {

-        static List<Tuple<int, int, int>> yieldTypeCheckerAutomatonEdges;

+        static List<Tuple<int, int, int>> ASpec;

+        static List<Tuple<int, int, int>> BSpec;

+        static List<Tuple<int, int, int>> CSpec;

         static YieldTypeChecker()

         {

-            yieldTypeCheckerAutomatonEdges = new List<Tuple<int, int, int>>();

-            AddEdge(0, 'P', 0);

-            AddEdge(0, 'Y', 0);

-            AddEdge(0, 'Y', 1);

-            AddEdge(0, 'Y', 2);

-            AddEdge(1, 'P', 1);

-            AddEdge(1, 'R', 1);

-            AddEdge(1, 'B', 1);

-            AddEdge(1, 'Y', 1);

-            AddEdge(1, 'Y', 0);

-            AddEdge(1, 'A', 2);

-            AddEdge(1, 'P', 2);

-            AddEdge(1, 'R', 2);

-            AddEdge(1, 'B', 2);

-            AddEdge(1, 'Y', 2);

-            AddEdge(2, 'L', 2);

-            AddEdge(2, 'B', 2);

-            AddEdge(2, 'P', 2);

-            AddEdge(2, 'Y', 2);

-            AddEdge(2, 'Y', 1);

-            AddEdge(2, 'Y', 0);

-        }

-        private static void AddEdge(int source, int label, int dest)

-        {

-            yieldTypeCheckerAutomatonEdges.Add(new Tuple<int, int, int>(source, label, dest));

+            // initial: 0, final: 1

+            ASpec = new List<Tuple<int,int,int>>();

+            ASpec.Add(new Tuple<int, int, int>(0, 'Y', 1));

+            ASpec.Add(new Tuple<int, int, int>(1, 'Y', 1));

+            ASpec.Add(new Tuple<int, int, int>(1, 'B', 1));

+            ASpec.Add(new Tuple<int, int, int>(1, 'R', 1));

+            ASpec.Add(new Tuple<int, int, int>(1, 'L', 1));

+            ASpec.Add(new Tuple<int, int, int>(1, 'A', 1));

+            ASpec.Add(new Tuple<int, int, int>(0, 'P', 0));

+            ASpec.Add(new Tuple<int, int, int>(1, 'P', 1));

+

+            // initial: 1, final: 0

+            BSpec = new List<Tuple<int, int, int>>();

+            BSpec.Add(new Tuple<int, int, int>(1, 'Y', 0));

+            BSpec.Add(new Tuple<int, int, int>(1, 'Y', 1));

+            BSpec.Add(new Tuple<int, int, int>(1, 'B', 1));

+            BSpec.Add(new Tuple<int, int, int>(1, 'R', 1));

+            BSpec.Add(new Tuple<int, int, int>(1, 'L', 1));

+            BSpec.Add(new Tuple<int, int, int>(1, 'A', 1));

+            BSpec.Add(new Tuple<int, int, int>(0, 'P', 0));

+            BSpec.Add(new Tuple<int, int, int>(1, 'P', 1));

+

+            // initial: {0, 1}, final: {0, 1}

+            CSpec = new List<Tuple<int,int,int>>();

+            CSpec.Add(new Tuple<int, int, int>(0, 'B', 0));

+            CSpec.Add(new Tuple<int, int, int>(0, 'R', 0));

+            CSpec.Add(new Tuple<int, int, int>(0, 'Y', 0));

+            CSpec.Add(new Tuple<int, int, int>(0, 'B', 1));

+            CSpec.Add(new Tuple<int, int, int>(0, 'R', 1));

+            CSpec.Add(new Tuple<int, int, int>(0, 'L', 1));

+            CSpec.Add(new Tuple<int, int, int>(0, 'A', 1));

+            CSpec.Add(new Tuple<int, int, int>(1, 'B', 1));

+            CSpec.Add(new Tuple<int, int, int>(1, 'L', 1));

+            CSpec.Add(new Tuple<int, int, int>(1, 'Y', 0));

+            CSpec.Add(new Tuple<int, int, int>(0, 'P', 0));

+            CSpec.Add(new Tuple<int, int, int>(1, 'P', 1));

         }

 

         private void IsYieldTypeSafe()

         {

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

+            List<Tuple<int, int, int>> implEdges = new List<Tuple<int, int, int>>();

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

             {

-                int label = edgeLabels[e];

-                int[] transition = new int[4];

-                transition[0] = e.Item1;

-                transition[1] = label;

-                transition[2] = label;

-                transition[3] = e.Item2;

-                transitions.Add(transition);

+                implEdges.Add(new Tuple<int, int, int>(e.Item1, edgeLabels[e], e.Item2));

             }

+            //Console.WriteLine(PrintGraph(impl, implEdges, initialState, finalStates));

+            ASpecCheck(implEdges);

+            BSpecCheck(implEdges);

+            CSpecCheck(implEdges);

+        }

 

-            int dummyInitial = stateCounter;

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

+        private void ASpecCheck(List<Tuple<int, int, int>> implEdges)

+        {

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

+            initialConstraints[initialState] = new HashSet<int>(new int[] { 0 });

+            foreach (var finalState in finalStates)

             {

-                if (initialStates.Contains(e.Item1))

-                {

-                    int[] transition = new int[4];

-                    transition[0] = dummyInitial;

-                    transition[1] = edgeLabels[e];

-                    transition[2] = edgeLabels[e];

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

+                initialConstraints[finalState] = new HashSet<int>(new int[] { 1 });

             }

-

-            List<Tuple<int, int, int>> implEdges = new List<Tuple<int, int, int>>();

-            foreach (int[] transition in transitions)

+            SimulationRelation<int, int, int> x = new SimulationRelation<int, int, int>(implEdges, ASpec, initialConstraints);

+            Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();

+            if (simulationRelation[initialState].Count == 0)

             {

-                implEdges.Add(new Tuple<int, int, int>(transition[0], transition[1], transition[3]));

+                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at phase {1}. An action must be preceded by a yield.\n", impl.Name, currPhaseNum));

             }

+        }

+

+        private void BSpecCheck(List<Tuple<int, int, int>> implEdges)

+        {

             Dictionary<int, HashSet<int>> initialConstraints = new Dictionary<int, HashSet<int>>();

-            initialConstraints[dummyInitial] = new HashSet<int>(new int[] {0});

+            initialConstraints[initialState] = new HashSet<int>(new int[] { 1 });

             foreach (var finalState in finalStates)

             {

                 initialConstraints[finalState] = new HashSet<int>(new int[] { 0 });

             }

+            SimulationRelation<int, int, int> x = new SimulationRelation<int, int, int>(implEdges, BSpec, initialConstraints);

+            Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();

+            if (simulationRelation[initialState].Count == 0)

+            {

+                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at phase {1}. An action must be succeeded by a yield.\n", impl.Name, currPhaseNum));

+            }

+        }

+

+        private void CSpecCheck(List<Tuple<int, int, int>> implEdges)

+        {

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

             foreach (Block block in loopHeaders)

             {

                 if (!IsTerminatingLoopHeader(block))

                 {

-                    initialConstraints[absyToNode[block]] = new HashSet<int>(new int[] { 0, 1 });

+                    initialConstraints[absyToNode[block]] = new HashSet<int>(new int[] { 0 });

                 }

             }

-            SimulationRelation<int, int, int> x = new SimulationRelation<int, int, int>(implEdges, yieldTypeCheckerAutomatonEdges, initialConstraints);

+            SimulationRelation<int, int, int> x = new SimulationRelation<int, int, int>(implEdges, CSpec, initialConstraints);

             Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();

-            foreach (Block block in loopHeaders)

+            if (simulationRelation[initialState].Count == 0)

             {

-                if (simulationRelation[absyToNode[block]].Count == 0)

-                {

-                    IToken tok = block.tok;

-                    moverTypeChecker.Error(impl, string.Format("Loop at {0}({1}, {2}) not simulated appropriately at phase {3}\n", tok.filename, tok.line, tok.col, currPhaseNum));

-                }

+                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at phase {1}. Transactions must be separated by a yield.\n", impl.Name, currPhaseNum));

             }

         }

 

@@ -138,7 +156,7 @@ namespace Microsoft.Boogie
         int currPhaseNum;

         Dictionary<Absy, int> absyToNode;

         Dictionary<int, Absy> nodeToAbsy;

-        HashSet<int> initialStates;

+        int initialState;

         HashSet<int> finalStates;

         Dictionary<Tuple<int, int>, int> edgeLabels;

         IEnumerable<Block> loopHeaders;

@@ -151,8 +169,7 @@ namespace Microsoft.Boogie
             this.loopHeaders = loopHeaders;

             this.stateCounter = 0;

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

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

-            initialStates.Add(0);

+            this.initialState = 0;

             this.finalStates = new HashSet<int>();

             this.edgeLabels = new Dictionary<Tuple<int, int>, int>(); 

             

@@ -312,13 +329,35 @@ namespace Microsoft.Boogie
             }

         }

 

-        private static string PrintGraph(Implementation yTypeChecked, Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels)

+        private static string PrintGraph(Implementation impl, List<Tuple<int, int, int>> edges, int initialState, HashSet<int> finalStates)

         {

             var s = new StringBuilder();

-            s.AppendLine("\nImplementation " + yTypeChecked.Proc.Name + " digraph G {");

-            foreach (var e in graph.Edges)

-                s.AppendLine("  \"" + e.Item1.ToString() + "\" -- " + edgeLabels[e] + " --> " + "  \"" + e.Item2.ToString() + "\";");

+            s.AppendLine("\nImplementation " + impl.Proc.Name + " digraph G {");

+            foreach (var e in edges)

+            {

+                string label = "P";

+                switch (e.Item2)

+                {

+                    case 'P': label = "P"; break;

+                    case 'Y': label = "Y"; break;

+                    case 'B': label = "B"; break;

+                    case 'R': label = "R"; break;

+                    case 'L': label = "L"; break;

+                    case 'A': label = "A"; break;

+                    default: Debug.Assert(false); break;

+                }

+                s.AppendLine("  \"" + e.Item1.ToString() + "\" -- " + label + " --> " + "  \"" + e.Item3.ToString() + "\";");

+            }

             s.AppendLine("}");

+            s.AppendLine("Initial state: " + initialState);

+            s.Append("Final states: ");

+            bool first = true;

+            foreach (int finalState in finalStates)

+            { 

+                s.Append((first ? "" : ", ") + finalState);

+                first = false;

+            }

+            s.AppendLine();

             return s.ToString();

         }

     }

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index 62101cba..e7e3abe9 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -67,6 +67,7 @@ requires {:phase 1} xls' == mapconstbool(true);
 	yield;

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

     }

+    yield;

 }

 

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

diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index bbae8b04..de2faaa8 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -22,12 +22,12 @@ procedure {:yields} {:phase 1} main()
     yield;

     while (*) 

     {

-        yield;

         call tid := Allocate();

         havoc val;

         async call foo(tid, val);

 	yield;

     }

+    yield;

 }

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

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

diff --git a/Test/og/Program1.bpl b/Test/og/Program1.bpl
index 56620da2..5a3ba93d 100644
--- a/Test/og/Program1.bpl
+++ b/Test/og/Program1.bpl
@@ -15,11 +15,15 @@ ensures {:phase 1} x >= 8;
     yield;

     assert {:phase 1} x >= 7;

     call Incr(1); 

+    yield;

+    assert {:phase 1} x >= 8; 

 }

 

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

 { 

+    yield;

     call Incr(3); 

+    yield;

 }

 

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

diff --git a/Test/og/Program2.bpl b/Test/og/Program2.bpl
index 7713a5d2..e4380655 100644
--- a/Test/og/Program2.bpl
+++ b/Test/og/Program2.bpl
@@ -12,11 +12,14 @@ ensures {:phase 1} x >= 8;
     call Incr(1); 

     call yield_x(7);

     call Incr(1); 

+    call yield_x(8);

 }

 

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

 { 

+    yield;

     call Incr(3); 

+    yield;

 }

 

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

diff --git a/Test/og/Program3.bpl b/Test/og/Program3.bpl
index e1b014b7..e2c55c8e 100644
--- a/Test/og/Program3.bpl
+++ b/Test/og/Program3.bpl
@@ -12,11 +12,14 @@ ensures {:phase 1} x >= 8;
     call Incr(1); 

     call yield_x();

     call Incr(1); 

+    call yield_x();

 }

 

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

 { 

+    yield;

     call Incr(3); 

+    yield;

 }

 

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

diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl
index 6130b69b..c936cab7 100644
--- a/Test/og/Program4.bpl
+++ b/Test/og/Program4.bpl
@@ -36,10 +36,14 @@ ensures {:phase 1} a[tid] == old(a)[tid] + 1;
 { 

     var t:int;

 

+    yield;

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

     call t := Read(tid); 

     yield;

-    assert {:phase 1} t == a[tid]; 

+    assert {:phase 1} a[tid] == t; 

     call Write(tid, t + 1); 

+    yield;

+    assert {:phase 1} a[tid] == t + 1; 

 }

 

 procedure {:yields} {:phase 0,1} Read({:cnst "tid"} tid: Tid) returns (val: int);

diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl
index b348075e..1d2c9a03 100644
--- a/Test/og/bar.bpl
+++ b/Test/og/bar.bpl
@@ -46,7 +46,6 @@ procedure {:yields} {:phase 1} Main2()
   yield;

   while (*)

   {

-    yield;

     async call PB();

     yield;

     async call PE();

@@ -54,4 +53,5 @@ procedure {:yields} {:phase 1} Main2()
     async call PD();

     yield;

   }

+  yield;

 }

diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl
index 5ddc75c0..eae47e12 100644
--- a/Test/og/foo.bpl
+++ b/Test/og/foo.bpl
@@ -46,7 +46,6 @@ procedure {:yields} {:phase 1} Main()
   yield;

   while (*)

   {

-    yield;

     async call PB();

     yield;

     async call PE();

@@ -54,4 +53,5 @@ procedure {:yields} {:phase 1} Main()
     async call PD();

     yield;

   }

+  yield;

 }

diff --git a/Test/og/lock-introduced.bpl b/Test/og/lock-introduced.bpl
index 0b4e39f3..d424f9a3 100644
--- a/Test/og/lock-introduced.bpl
+++ b/Test/og/lock-introduced.bpl
@@ -21,16 +21,13 @@ ensures {:phase 2} InvLock(lock, b);
     while (*) 

     invariant {:phase 2} InvLock(lock, b);

     {

-    	yield;

-    	assert {:phase 2} InvLock(lock, b);

-

         call Enter(tid);

-

     	call Leave(tid);

-

         yield;

 	assert {:phase 2} InvLock(lock, b);

-    }

+    }    

+    yield;

+    assert {:phase 2} InvLock(lock, b);

 }

 

 function {:inline} InvLock(lock: X, b: bool) : bool

diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl
index 90357d4c..86c382d8 100644
--- a/Test/og/lock.bpl
+++ b/Test/og/lock.bpl
@@ -7,12 +7,10 @@ procedure {:yields} {:phase 2} main()
     yield;

     while (*)

     {

-        yield;

-

         async call Customer();

-

         yield;

     }

+    yield;

 }

 

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

@@ -20,16 +18,12 @@ procedure {:yields} {:phase 2} Customer()
     yield;

     while (*) 

     {

-    	yield;

-

         call Enter();

-

     	yield;

-

     	call Leave();

-

         yield;

     }

+    yield;

 }

 

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

diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl
index 87538a20..354821e7 100644
--- a/Test/og/lock2.bpl
+++ b/Test/og/lock2.bpl
@@ -7,12 +7,10 @@ procedure {:yields} {:phase 2} main()
     yield;

     while (*)

     {

-        yield;

-

         async call Customer();

-

         yield;

     }

+    yield;

 }

 

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

@@ -20,16 +18,12 @@ procedure {:yields} {:phase 2} Customer()
     yield;

     while (*) 

     {

-    	yield;

-

         call Enter();

-

     	yield;

-

     	call Leave();

-

         yield;

     }

+    yield;

 }

 

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

@@ -38,21 +32,21 @@ ensures {:atomic} |{ A: assume b == 0; b := 1; return true; }|;
     var _old, curr: int;

     yield;

     while (true) { 

-    	yield;

         call _old := CAS(0, 1);

 	yield;

         if (_old == 0) {

-	    return;

+	    break;

 	}

 	while (true) {

-	    yield;

 	    call curr := Read();

 	    yield;

 	    if (curr == 0) {

 	        break;

 	    }

 	}

+	yield;

     }

+    yield;

 }

 

 procedure {:yields} {:phase 0,2} Read() returns (val: int);

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index c54782e5..fc97f9fb 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -135,8 +135,6 @@ ensures {:right}  |{ A: assert tidIn != nil && tidIn != done;
         invariant {:phase 1} Inv(valid, elt, owner);

 	invariant {:phase 1} 0 <= j;

 	{

-                par Yield1();

-

                 call tidTmp := acquire(j, tidTmp);

                 call tidTmp, elt_j := getElt(j, tidTmp);

 		if(elt_j == null)

@@ -147,7 +145,6 @@ ensures {:right}  |{ A: assert tidIn != nil && tidIn != done;
                         tidOut := tidTmp;

 

                         par Yield1();

-

 			return;		

 		}

 		call tidTmp := release(j,tidTmp);

@@ -158,6 +155,8 @@ ensures {:right}  |{ A: assert tidIn != nil && tidIn != done;
 	}

 	r := -1;

         tidOut := tidTmp;

+

+        par Yield1();

 	return;

 }

 

@@ -316,8 +315,6 @@ ensures {:atomic}  |{ A: assert tidIn != nil && tidIn != done;
 	invariant {:phase 1} {:phase 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

 	invariant {:phase 1} {:phase 2} 0 <= j;

 	{

-                par Yield12() | YieldLookUp(old_valid, old_elt);

-

                 call tidTmp := acquire(j, tidTmp);

                 call tidTmp, isThere := isEltThereAndValid(j, x, tidTmp);

 		if(isThere)

@@ -334,6 +331,8 @@ ensures {:atomic}  |{ A: assert tidIn != nil && tidIn != done;
 	}

 	found := false;

         tidOut := tidTmp;

+

+        par Yield12() | YieldLookUp(old_valid, old_elt);

 	return;

 }

 

diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl
index 1cd0a5c8..6b2ea3a8 100644
--- a/Test/og/parallel1.bpl
+++ b/Test/og/parallel1.bpl
@@ -44,4 +44,5 @@ procedure {:yields} {:phase 1} Main()
   {

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

   }

+  yield;

 }

diff --git a/Test/og/termination.bpl.expect b/Test/og/termination.bpl.expect
index a924f8cf..ab90b536 100644
--- a/Test/og/termination.bpl.expect
+++ b/Test/og/termination.bpl.expect
@@ -1,3 +1,3 @@
-termination.bpl(9,31): Error: Loop at termination.bpl(12, 3) not simulated appropriately at phase 1
+termination.bpl(9,31): Error: Implementation main fails simulation check C at phase 1. Transactions must be separated by a yield.
 

 1 type checking errors detected in termination.bpl

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index d532c5a2..02341e91 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -52,12 +52,11 @@ 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();

-

     }

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

 }

 

 procedure {:yields} {:phase 3} Customer({:linear "tid"} tid': X)

@@ -73,12 +72,12 @@ requires {:phase 3} true;
     invariant {:phase 1} Inv1(T, t);

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

     {

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

         call tid := Enter(tid);

         par Yield1() | Yield2();

     	call tid := Leave(tid);

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

     }

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

 }

 

 procedure {:yields} {:phase 2,3} Enter({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl
index 942bae67..8e5f059a 100644
--- a/Test/og/treiber-stack.bpl
+++ b/Test/og/treiber-stack.bpl
@@ -1,80 +1,221 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

-// XFAIL: *

-type Node;

+type Node = int;

+const unique null: Node;

 type lmap;

 function {:linear "Node"} dom(lmap): [Node]bool;

 function map(lmap): [Node]Node;

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

 

-procedure {:yields} Load(i:Node) returns(v:Node);

-requires dom(stack)[i];

-ensures {:atomic 0} v == map(stack)[i];

+function EmptyLmap(): (lmap);

+axiom (dom(EmptyLmap()) == MapConstBool(false));

 

-procedure {:yields} Store({:linear "Node"} l_in:lmap, i:Node, v:Node) returns({:linear "Node"} l_out:lmap);

-requires dom(l_in)[i];

-ensures {:atomic 0} dom(l_out) == dom(l_in) && map(l_out) == map(l_in)[i := v];

+function Add(x: lmap, i: Node, v: Node): (lmap);

+axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]);

 

-procedure {:yields} TransferToStack(oldVal: Node, newVal: Node, {:linear "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);

-requires dom(l_in)[newVal];

-modifies stack, TOP;

-ensures {:atomic 0} if oldVal == old(TOP)

-		    then newVal == TOP && dom(stack) == dom(old(stack))[newVal := true] && map(stack) == map(old(stack))[newVal := map(l_in)[newVal]]

-                    else TOP == old(TOP) && stack == old(stack) && l_out == l_in;

+function Remove(x: lmap, i: Node): (lmap);

+axiom (forall x: lmap, i: Node :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));

 

-procedure {:yields} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool, {:linear "Node"} l_out:lmap);

-requires dom(stack)[oldVal];

-modifies stack, TOP;

-ensures {:atomic 0} if oldVal == old(TOP)

-		    then dom(stack) == dom(old(stack))[oldVal := false] && map(stack) == map(old(stack)) && dom(l_out)[oldVal] && map(l_out)[oldVal] == map(old(stack))[oldVal]

-		    else TOP == old(TOP) && stack == old(stack);

+procedure {:yields} {:phase 0} ReadTopOfStack() returns (v:Node);

+ensures {:both} |{ A: /*v := TopOfStack;*/ return true; }|;

 

-procedure Alloc() returns (d: Node, {:linear "Node"} l: lmap);

-ensures dom(l)[d];

+procedure {:yields} {:phase 0} Load(i:Node) returns (v:Node);

+ensures {:right} |{ A: goto B,C;

+	           B: assume dom(Stack)[i]; v := map(Stack)[i]; return true; 

+		   C: assume !dom(Stack)[i]; return true; }|;

 

-procedure Free(d: Node, {:linear "Node"} l: lmap);

+procedure {:yields} {:phase 0} Store({:linear "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);

+ensures {:both} |{ A: assert dom(l_in)[i]; l_out := Add(l_in, i, v); return true; }|;

 

-const unique null: Node;

+procedure {:yields} {:phase 0} MakeEmpty() returns ({:linear "Node"} l_out:lmap);

+ensures {:both} |{ A: l_out := EmptyLmap(); return true; }|;

+

+procedure {:yields} {:phase 0} TransferToStack(oldVal: Node, newVal: Node, {:linear "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);

+ensures {:atomic} |{ A: assert dom(l_in)[newVal];

+		        goto B,C;

+                        B: assume oldVal == TopOfStack; TopOfStack := newVal; l_out := EmptyLmap(); Stack := Add(Stack, newVal, map(l_in)[newVal]); r := true; return true;

+			C: assume oldVal != TopOfStack; l_out := l_in; r := false; return true; }|;

+

+procedure {:yields} {:phase 0} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool, {:linear "Node"} l_out:lmap);

+ensures {:atomic} |{ A: goto B,C;

+                        B: assume oldVal == TopOfStack; TopOfStack := newVal; l_out := Add(EmptyLmap(), oldVal, map(Stack)[oldVal]); Stack := Remove(Stack, oldVal); r := true; return true;

+		        C: assume oldVal != TopOfStack; l_out := EmptyLmap(); r := false; return true; }|;

+

+var TopOfStack: Node;

+var {:linear "Node"} Stack: lmap;

 

-var {:qed} TOP: Node;

-var {:qed} {:linear "Node"} stack: lmap;

 

-procedure {:yields} push()

+function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool)

 {

-  var t, x: Node;

-  var g: bool;

-  var {:linear "Node"} x_lmap: lmap;

+  BetweenSet(map(Stack), TopOfStack, null)[TopOfStack] &&

+  Subset(Difference(BetweenSet(map(Stack), TopOfStack, null), Singleton(null)), dom(Stack))

+}

 

-  call x, x_lmap := Alloc();

+procedure {:yields} {:phase 1} push(x: Node, {:linear "Node"} x_lmap: lmap)

+requires {:phase 1} dom(x_lmap)[x];

+requires {:phase 1} Inv(TopOfStack, Stack);

+ensures {:phase 1} Inv(TopOfStack, Stack);

+ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; return true; }|;

+{

+  var t: Node;

+  var g: bool;

+  var {:linear "Node"} t_lmap: lmap;

 

-  while(true)

+  yield;

+  assert {:phase 1} Inv(TopOfStack, Stack);

+  t_lmap := x_lmap;

+  while (true)

+  invariant {:phase 1} dom(t_lmap) == dom(x_lmap);

+  invariant {:phase 1} Inv(TopOfStack, Stack);

   {

-    t := TOP;		

-    call x_lmap := Store(x_lmap, x, t);

-    call g, x_lmap := TransferToStack(t, x, x_lmap); 

-    if (g) { 

-      break; 

+    call t := ReadTopOfStack();

+    call t_lmap := Store(t_lmap, x, t);

+    call g, t_lmap := TransferToStack(t, x, t_lmap); 

+    if (g) {

+      assert {:phase 1} map(Stack)[x] == t;

+      break;

     }

+    yield; 

+    assert {:phase 1} dom(t_lmap) == dom(x_lmap);

+    assert {:phase 1} Inv(TopOfStack, Stack);

   }

+  yield; 

+  assert {:expand} {:phase 1} Inv(TopOfStack, Stack);

 }

 

-procedure {:yields} pop()

+procedure {:yields} {:phase 1} pop() returns (t: Node, {:linear "Node"} t_lmap: lmap)

+requires {:phase 1} Inv(TopOfStack, Stack);

+ensures {:phase 1} Inv(TopOfStack, Stack);

+ensures {:atomic} |{ A: goto B,C;

+                     B: t_lmap := EmptyLmap(); return true;

+                     C: assume TopOfStack != null; t := TopOfStack; t_lmap := Add(EmptyLmap(), t, map(Stack)[t]); TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|;

 {

-  var t, x: Node;

   var g: bool;

-  var {:linear "Node"} t_lmap: lmap;

+  var x: Node;

 

-  while(true)

+  yield;

+  assert {:phase 1} Inv(TopOfStack, Stack);

+  call t_lmap := MakeEmpty();

+  while (true)

+  invariant {:phase 1} Inv(TopOfStack, Stack);

   {

-    t := TOP;		

-    if (t == null)

-    {

-      return;

+    call t := ReadTopOfStack();

+    if (t == null) {

+      break;

     }

     call x := Load(t);

     call g, t_lmap := TransferFromStack(t, x); 

     if (g) { 

-      call Free(t, t_lmap);

-      break; 

+      break;

     }

+    yield;

+    assert {:phase 1} Inv(TopOfStack, Stack);

   }

+  yield;

+  assert {:phase 1} Inv(TopOfStack, Stack);

 }

+

+function Equal([int]bool, [int]bool) returns (bool);

+function Subset([int]bool, [int]bool) returns (bool);

+function Disjoint([int]bool, [int]bool) returns (bool);

+

+function Empty() returns ([int]bool);

+function SetTrue() returns ([int]bool);

+function Singleton(int) returns ([int]bool);

+function Reachable([int,int]bool, int) returns ([int]bool);

+function Union([int]bool, [int]bool) returns ([int]bool);

+function Intersection([int]bool, [int]bool) returns ([int]bool);

+function Difference([int]bool, [int]bool) returns ([int]bool);

+function Inverse(f:[int]int, x:int) returns ([int]bool);

+

+axiom(forall x:int :: !Empty()[x]);

+axiom(forall x:int :: SetTrue()[x]);

+

+axiom(forall x:int, y:int :: {Singleton(y)[x]} Singleton(y)[x] <==> x == y);

+axiom(forall y:int :: {Singleton(y)} Singleton(y)[y]);

+

+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Union(S,T)[x]}{Union(S,T),S[x]}{Union(S,T),T[x]} Union(S,T)[x] <==> S[x] || T[x]);

+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Intersection(S,T)[x]}{Intersection(S,T),S[x]}{Intersection(S,T),T[x]} Intersection(S,T)[x] <==>  S[x] && T[x]);

+axiom(forall x:int, S:[int]bool, T:[int]bool :: {Difference(S,T)[x]}{Difference(S,T),S[x]}{Difference(S,T),T[x]} Difference(S,T)[x] <==> S[x] && !T[x]);

+

+axiom(forall S:[int]bool, T:[int]bool :: {Equal(S,T)} Equal(S,T) <==> Subset(S,T) && Subset(T,S));

+axiom(forall x:int, S:[int]bool, T:[int]bool :: {S[x],Subset(S,T)}{T[x],Subset(S,T)} S[x] && Subset(S,T) ==> T[x]);

+axiom(forall S:[int]bool, T:[int]bool :: {Subset(S,T)} Subset(S,T) || (exists x:int :: S[x] && !T[x]));

+axiom(forall x:int, S:[int]bool, T:[int]bool :: {S[x],Disjoint(S,T)}{T[x],Disjoint(S,T)} !(S[x] && Disjoint(S,T) && T[x]));

+axiom(forall S:[int]bool, T:[int]bool :: {Disjoint(S,T)} Disjoint(S,T) || (exists x:int :: S[x] && T[x]));

+

+axiom(forall f:[int]int, x:int :: {Inverse(f,f[x])} Inverse(f,f[x])[x]);

+axiom(forall f:[int]int, x:int, y:int :: {Inverse(f,y), f[x]} Inverse(f,y)[x] ==> f[x] == y);

+axiom(forall f:[int]int, x:int, y:int :: {Inverse(f[x := y],y)} Equal(Inverse(f[x := y],y), Union(Inverse(f,y), Singleton(x))));

+axiom(forall f:[int]int, x:int, y:int, z:int :: {Inverse(f[x := y],z)} y == z || Equal(Inverse(f[x := y],z), Difference(Inverse(f,z), Singleton(x))));

+

+////////////////////

+// Between predicate

+//////////////////// 

+function Between(f: [int]int, x: int, y: int, z: int) returns (bool);

+function Avoiding(f: [int]int, x: int, y: int, z: int) returns (bool);

+

+

+//////////////////////////

+// Between set constructor

+//////////////////////////

+function BetweenSet(f: [int]int, x: int, z: int) returns ([int]bool);

+

+////////////////////////////////////////////////////

+// axioms relating Between and BetweenSet

+////////////////////////////////////////////////////

+axiom(forall f: [int]int, x: int, y: int, z: int :: {BetweenSet(f, x, z)[y]} BetweenSet(f, x, z)[y] <==> Between(f, x, y, z));

+axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z), BetweenSet(f, x, z)} Between(f, x, y, z) ==> BetweenSet(f, x, z)[y]);

+axiom(forall f: [int]int, x: int, z: int :: {BetweenSet(f, x, z)} Between(f, x, x, x));

+axiom(forall f: [int]int, x: int, z: int :: {BetweenSet(f, x, z)} Between(f, z, z, z));

+

+

+//////////////////////////

+// Axioms for Between

+//////////////////////////

+

+// reflexive

+axiom(forall f: [int]int, x: int :: Between(f, x, x, x));

+

+// step

+//axiom(forall f: [int]int, x: int :: {f[x]} Between(f, x, f[x], f[x])); 

+axiom(forall f: [int]int, x: int, y: int, z: int, w:int :: {Between(f, y, z, w), f[x]} Between(f, x, f[x], f[x])); 

+

+// reach

+axiom(forall f: [int]int, x: int, y: int :: {f[x], Between(f, x, y, y)} Between(f, x, y, y) ==> x == y || Between(f, x, f[x], y));

+

+// cycle

+axiom(forall f: [int]int, x: int, y:int :: {f[x], Between(f, x, y, y)} f[x] == x && Between(f, x, y, y) ==> x == y);

+

+// sandwich

+axiom(forall f: [int]int, x: int, y: int :: {Between(f, x, y, x)} Between(f, x, y, x) ==> x == y);

+

+// order1

+axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, y), Between(f, x, z, z)} Between(f, x, y, y) && Between(f, x, z, z) ==> Between(f, x, y, z) || Between(f, x, z, y));

+

+// order2

+axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z)} Between(f, x, y, z) ==> Between(f, x, y, y) && Between(f, y, z, z));

+

+// transitive1

+axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, y), Between(f, y, z, z)} Between(f, x, y, y) && Between(f, y, z, z) ==> Between(f, x, z, z));

+

+// transitive2

+axiom(forall f: [int]int, x: int, y: int, z: int, w: int :: {Between(f, x, y, z), Between(f, y, w, z)} Between(f, x, y, z) && Between(f, y, w, z) ==> Between(f, x, y, w) && Between(f, x, w, z));

+

+// transitive3

+axiom(forall f: [int]int, x: int, y: int, z: int, w: int :: {Between(f, x, y, z), Between(f, x, w, y)} Between(f, x, y, z) && Between(f, x, w, y) ==> Between(f, x, w, z) && Between(f, w, y, z));

+

+// This axiom is required to deal with the incompleteness of the trigger for the reflexive axiom.  

+// It cannot be proved using the rest of the axioms.

+axiom(forall f: [int]int, u:int, x: int :: {Between(f, u, x, x)} Between(f, u, x, x) ==> Between(f, u, u, x));

+

+// relation between Avoiding and Between

+axiom(forall f: [int]int, x: int, y: int, z: int :: {Avoiding(f, x, y, z)} Avoiding(f, x, y, z) <==> (Between(f, x, y, z) || (Between(f, x, y, y) && !Between(f, x, z, z))));

+axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z)} Between(f, x, y, z) <==> (Avoiding(f, x, y, z) && Avoiding(f, x, z, z)));

+

+// update

+axiom(forall f: [int]int, u: int, v: int, x: int, p: int, q: int :: {Avoiding(f[p := q], u, v, x)} Avoiding(f[p := q], u, v, x) <==> ((Avoiding(f, u, v, p) && Avoiding(f, u, v, x)) || (Avoiding(f, u, p, x) && p != x && Avoiding(f, q, v, p) && Avoiding(f, q, v, x))));

+

+axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} Avoiding(f, u, w, p) ==> Equal(BetweenSet(f[p := q], u, w), BetweenSet(f, u, w)));

+axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} p != w && Avoiding(f, u, p, w) && Avoiding(f, q, w, p) ==> Equal(BetweenSet(f[p := q], u, w), Union(BetweenSet(f, u, p), BetweenSet(f, q, w))));

+axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} Avoiding(f, u, w, p) || (p != w && Avoiding(f, u, p, w) && Avoiding(f, q, w, p)) || Equal(BetweenSet(f[p := q], u, w), Empty()));
\ No newline at end of file
diff --git a/Test/og/treiber-stack.bpl.expect b/Test/og/treiber-stack.bpl.expect
new file mode 100644
index 00000000..ed4a9b00
--- /dev/null
+++ b/Test/og/treiber-stack.bpl.expect
@@ -0,0 +1,8 @@
+(0,0): Error BP5003: A postcondition might not hold on this return path.

+(0,0): Related location: Commutativity check between Load and TransferToStack failed

+Execution trace:

+    (0,0): that_C

+    (0,0): this_A

+    (0,0): this_B

+

+Boogie program verifier finished with 3 verified, 1 error