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

1 files changed, 104 insertions, 65 deletions

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

         }

     }