strengthened type checking

cleaned up the generation of mover checks (based on example from Chris)
added two examples from Chris to regressions

4 files changed, 137 insertions, 81 deletions

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index b10cd6cd..971e7271 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -30,52 +30,57 @@ namespace Microsoft.Boogie
             if (moverTypeChecker.procToActionInfo.Count == 0)

                 return;

 

+            List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo));

+            sortedByCreatedLayerNum.Sort((x, y) => { return (x.createdAtLayerNum == y.createdAtLayerNum) ? 0 : (x.createdAtLayerNum < y.createdAtLayerNum) ? -1 : 1; });

+            List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo));

+            sortedByAvailableUptoLayerNum.Sort((x, y) => { return (x.availableUptoLayerNum == y.availableUptoLayerNum) ? 0 : (x.availableUptoLayerNum < y.availableUptoLayerNum) ? -1 : 1; });

+

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

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

+            int indexIntoSortedByCreatedLayerNum = 0;

+            int indexIntoSortedByAvailableUptoLayerNum = 0;

+            HashSet<AtomicActionInfo> currPool = new HashSet<AtomicActionInfo>();

+            while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count)

             {

-                AtomicActionInfo atomicAction = action as AtomicActionInfo;

-                if (atomicAction == null) continue;

-                foreach (int layerNum in moverTypeChecker.AllLayerNums)

+                var currLayerNum = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum].createdAtLayerNum;

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

+                while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count)

                 {

-                    if (action.createdAtLayerNum < layerNum && layerNum <= action.availableUptoLayerNum)

-                    {

-                        if (!pools.ContainsKey(layerNum))

-                        {

-                            pools[layerNum] = new HashSet<AtomicActionInfo>();

-                        }

-                        pools[layerNum].Add(atomicAction);

-                    }

+                    var actionInfo = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum] as AtomicActionInfo;

+                    if (actionInfo.createdAtLayerNum > currLayerNum) break;

+                    pools[currLayerNum].Add(actionInfo);

+                    indexIntoSortedByCreatedLayerNum++;

                 }

+                while (indexIntoSortedByAvailableUptoLayerNum < sortedByAvailableUptoLayerNum.Count)

+                {

+                    var actionInfo = sortedByAvailableUptoLayerNum[indexIntoSortedByAvailableUptoLayerNum] as AtomicActionInfo;

+                    if (actionInfo.availableUptoLayerNum > currLayerNum) break;

+                    pools[currLayerNum].Remove(actionInfo);

+                    indexIntoSortedByAvailableUptoLayerNum++;

+                }

+                currPool = pools[currLayerNum];

             }

 

             Program program = moverTypeChecker.program;

             MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls);

-            foreach (int layerNum1 in pools.Keys)

+            foreach (int layerNum in pools.Keys)

             {

-                foreach (AtomicActionInfo first in pools[layerNum1])

+                foreach (AtomicActionInfo first in pools[layerNum])

                 {

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

                     if (first.moverType == MoverType.Atomic)

                         continue;

-                    foreach (int layerNum2 in pools.Keys)

+                    foreach (AtomicActionInfo second in pools[layerNum])

                     {

-                        if (layerNum2 < layerNum1) continue;

-                        foreach (AtomicActionInfo second in pools[layerNum2])

+                        if (first.IsRightMover)

+                        {

+                            moverChecking.CreateCommutativityChecker(program, first, second);

+                            moverChecking.CreateGatePreservationChecker(program, second, first);

+                        }

+                        if (first.IsLeftMover)

                         {

-                            if (second.createdAtLayerNum < layerNum1)

-                            {

-                                if (first.IsRightMover)

-                                {

-                                    moverChecking.CreateCommutativityChecker(program, first, second);

-                                    moverChecking.CreateGatePreservationChecker(program, second, first);

-                                }

-                                if (first.IsLeftMover)

-                                {

-                                    moverChecking.CreateCommutativityChecker(program, second, first);

-                                    moverChecking.CreateGatePreservationChecker(program, first, second);

-                                    moverChecking.CreateFailurePreservationChecker(program, second, first);

-                                }

-                            }

+                            moverChecking.CreateCommutativityChecker(program, second, first);

+                            moverChecking.CreateGatePreservationChecker(program, first, second);

+                            moverChecking.CreateFailurePreservationChecker(program, second, first);

                         }

                     }

                 }

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 8865b69e..dbd1dcbd 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -1160,7 +1160,7 @@ namespace Microsoft.Boogie
         public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)

         {

             Program program = linearTypeChecker.program;

-            foreach (int layerNum in moverTypeChecker.AllLayerNums.Except(new int[] { 0 }))

+            foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))

             {

                 if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue;

 

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 8eb93e09..13356aff 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -22,12 +22,14 @@ namespace Microsoft.Boogie
         public Procedure proc;

         public int createdAtLayerNum;

         public int availableUptoLayerNum;

+        public bool hasImplementation;

 

         public ActionInfo(Procedure proc, int createdAtLayerNum, int availableUptoLayerNum)

         {

             this.proc = proc;

             this.createdAtLayerNum = createdAtLayerNum;

             this.availableUptoLayerNum = availableUptoLayerNum;

+            this.hasImplementation = false;

         }

 

         public virtual bool IsRightMover

@@ -226,6 +228,7 @@ namespace Microsoft.Boogie
         int maxLayerNum;

         public Dictionary<Absy, HashSet<int>> absyToLayerNums;

         HashSet<Variable> auxVars;

+        public int leastUnimplementedLayerNum;

 

         private static List<int> FindLayers(QKeyValue kv)

         {

@@ -260,20 +263,58 @@ namespace Microsoft.Boogie
             return MoverType.Top;

         }

 

-        private HashSet<int> allLayerNums;

-        public IEnumerable<int> AllLayerNums

+        public MoverTypeChecker(Program program)

+        {

+            this.auxVars = new HashSet<Variable>();

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

+            this.globalVarToSharedVarInfo = new Dictionary<Variable, SharedVariableInfo>();

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

+            this.errorCount = 0;

+            this.checkingContext = new CheckingContext(null);

+            this.program = program;

+            this.enclosingProc = null;

+            this.enclosingImpl = null;

+            this.canAccessSharedVars = false;

+            this.canAccessAuxVars = false;

+            this.minLayerNum = int.MaxValue;

+            this.maxLayerNum = -1;

+            this.leastUnimplementedLayerNum = int.MaxValue;

+            foreach (var g in program.GlobalVariables)

+            {

+                List<int> layerNums = FindLayers(g.Attributes);

+                if (layerNums.Count == 0)

+                {

+                    // Cannot access atomic actions

+                }

+                else if (layerNums.Count == 1)

+                {

+                    this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], int.MaxValue);

+                }

+                else if (layerNums.Count == 2)

+                {

+                    this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], layerNums[1]);

+                }

+                else

+                {

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

+                }

+            }

+        }

+        

+        private HashSet<int> allCreatedLayerNums;

+        public IEnumerable<int> AllCreatedLayerNums

         {

             get

             {

-                if (allLayerNums == null)

+                if (allCreatedLayerNums == null)

                 {

-                    allLayerNums = new HashSet<int>();

+                    allCreatedLayerNums = new HashSet<int>();

                     foreach (ActionInfo actionInfo in procToActionInfo.Values)

                     {

-                        allLayerNums.Add(actionInfo.createdAtLayerNum);

+                        allCreatedLayerNums.Add(actionInfo.createdAtLayerNum);

                     }

                 }

-                return allLayerNums;

+                return allCreatedLayerNums;

             }

         }

 

@@ -300,6 +341,11 @@ namespace Microsoft.Boogie
                     Error(proc, "Incorrect number of layers");

                     continue;

                 }

+                if (availableUptoLayerNum <= createdAtLayerNum)

+                {

+                    Error(proc, "Creation layer number must be less than the available upto layer number");

+                    continue;

+                }

                 foreach (Ensures e in proc.Ensures)

                 {

                     MoverType moverType = GetMoverType(e);

@@ -323,68 +369,69 @@ namespace Microsoft.Boogie
                     enclosingImpl = null;

                     base.VisitEnsures(e);

                     canAccessSharedVars = false;

-                    if (maxLayerNum <= createdAtLayerNum && availableUptoLayerNum <= minLayerNum)

+                    if (maxLayerNum > createdAtLayerNum)

                     {

-                        // ok

+                        Error(e, "A variable being accessed is introduced after this action is created");

                     }

-                    else

+                    else if (availableUptoLayerNum > minLayerNum)

                     {

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

                     }

-

-                    procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum);

+                    else

+                    {

+                        procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum);

+                    }

                 }

+                if (errorCount > 0) continue;

                 if (!procToActionInfo.ContainsKey(proc))

                 {

                     procToActionInfo[proc] = new ActionInfo(proc, createdAtLayerNum, availableUptoLayerNum);

                 }

             }

             if (errorCount > 0) return;

-            this.VisitProgram(program);

-            if (errorCount > 0) return;

-            YieldTypeChecker.PerformYieldSafeCheck(this);

-        }

-

-        public IEnumerable<Variable> SharedVariables

-        {

-            get { return this.globalVarToSharedVarInfo.Keys;  }

-        }

-

-        public MoverTypeChecker(Program program)

-        {

-            this.auxVars = new HashSet<Variable>();

-            this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>();

-            this.globalVarToSharedVarInfo = new Dictionary<Variable, SharedVariableInfo>();

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

-            this.errorCount = 0;

-            this.checkingContext = new CheckingContext(null);

-            this.program = program;

-            this.enclosingProc = null;

-            this.enclosingImpl = null;

-            this.canAccessSharedVars = false;

-            this.canAccessAuxVars = false;

-            this.minLayerNum = int.MaxValue;

-            this.maxLayerNum = -1;

-            foreach (var g in program.GlobalVariables)

+            foreach (var impl in program.Implementations)

             {

-                List<int> layerNums = FindLayers(g.Attributes);

-                if (layerNums.Count == 0)

+                if (!procToActionInfo.ContainsKey(impl.Proc)) continue;

+                procToActionInfo[impl.Proc].hasImplementation = true;

+            }

+            foreach (var proc in procToActionInfo.Keys)

+            {

+                ActionInfo actionInfo = procToActionInfo[proc];

+                if (actionInfo.hasImplementation) continue;

+                if (leastUnimplementedLayerNum == int.MaxValue)

                 {

-                    // Cannot access atomic actions

+                    leastUnimplementedLayerNum = actionInfo.createdAtLayerNum;

                 }

-                else if (layerNums.Count == 1)

+                else if (leastUnimplementedLayerNum == actionInfo.createdAtLayerNum)

                 {

-                    this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], int.MaxValue);

+                    // do nothing

                 }

-                else if (layerNums.Count == 2)

+                else

                 {

-                    this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], layerNums[1]);

+                    Error(proc, "All unimplemented atomic actions must be created at the same layer");

                 }

-                else

+            }

+            foreach (var g in this.globalVarToSharedVarInfo.Keys)

+            {

+                var info = globalVarToSharedVarInfo[g];

+                if (!this.AllCreatedLayerNums.Contains(info.introLayerNum))

                 {

-                    Error(g, "Too many layer numbers");

+                    Error(g, "Variable must be introduced with creation of some atomic action");

+                }

+                if (info.hideLayerNum != int.MaxValue && !this.AllCreatedLayerNums.Contains(info.hideLayerNum))

+                {

+                    Error(g, "Variable must be hidden with creation of some atomic action");

                 }

             }

+            if (errorCount > 0) return;

+            this.VisitProgram(program);

+            if (errorCount > 0) return;

+            YieldTypeChecker.PerformYieldSafeCheck(this);

+        }

+

+        public IEnumerable<Variable> SharedVariables

+        {

+            get { return this.globalVarToSharedVarInfo.Keys;  }

         }

         

         public override Implementation VisitImplementation(Implementation node)

@@ -602,7 +649,11 @@ namespace Microsoft.Boogie
             absyToLayerNums[node] = new HashSet<int>();

             foreach (int layerNum in attrs)

             {

-                if (layerNum > enclosingProcLayerNum)

+                if (layerNum == leastUnimplementedLayerNum || !AllCreatedLayerNums.Contains(layerNum))

+                {

+                    Error(node, "Illegal layer number");

+                }

+                else if (layerNum > enclosingProcLayerNum)

                 {

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

                 }

diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index 8e844ede..95884626 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -136,12 +136,12 @@ namespace Microsoft.Boogie
         {

             foreach (var impl in moverTypeChecker.program.Implementations)

             {

-                if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum == 0) continue;

+                if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue;

                 impl.PruneUnreachableBlocks();

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

                 implGraph.ComputeLoops();

                 int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum;

-                foreach (int layerNum in moverTypeChecker.AllLayerNums)

+                foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))

                 {

                     if (layerNum > specLayerNum) continue;

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