added introduced and ghost local variables

8 files changed, 786 insertions, 217 deletions

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 2ad08024..d861e2f3 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -40,7 +40,15 @@ namespace Microsoft.Boogie
         {
             int enclosingProcLayerNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum;
             Procedure originalProc = originalCallCmd.Proc;
-            if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc))
+            
+            if (moverTypeChecker.procToAtomicProcedureInfo.ContainsKey(originalProc))
+            {
+                if (moverTypeChecker.CallExists(originalCallCmd, enclosingProcLayerNum, layerNum))
+                {
+                    newCmds.Add(callCmd);
+                }
+            }
+            else if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc))
             {
                 AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo;
                 if (atomicActionInfo != null && atomicActionInfo.gate.Count > 0 && layerNum == enclosingProcLayerNum)
@@ -57,8 +65,12 @@ namespace Microsoft.Boogie
                         newCmds.Add(Substituter.Apply(subst, assertCmd));
                     }
                 }
+                newCmds.Add(callCmd);
+            }
+            else
+            {
+                Debug.Assert(false);
             }
-            newCmds.Add(callCmd);
         }
 
         private void ProcessParCallCmd(ParCallCmd originalParCallCmd, ParCallCmd parCallCmd, List<Cmd> newCmds)
@@ -291,7 +303,34 @@ namespace Microsoft.Boogie
 
         private IEnumerable<Variable> AvailableLinearVars(Absy absy)
         {
-            return linearTypeChecker.AvailableLinearVars(absyMap[absy]);
+            HashSet<Variable> availableVars = new HashSet<Variable>(linearTypeChecker.AvailableLinearVars(absyMap[absy]));
+            foreach (var g in moverTypeChecker.globalVarToSharedVarInfo.Keys)
+            {
+                SharedVariableInfo info = moverTypeChecker.globalVarToSharedVarInfo[g];
+                if (!(info.introLayerNum <= layerNum && layerNum <= info.hideLayerNum))
+                {
+                    availableVars.Remove(g);
+                }
+            }
+            foreach (var v in moverTypeChecker.localVarToLocalVariableInfo.Keys)
+            {
+                LocalVariableInfo info = moverTypeChecker.localVarToLocalVariableInfo[v];
+                if (info.isGhost)
+                {
+                    if (info.layer != layerNum)
+                    {
+                        availableVars.Remove(v);
+                    }
+                }
+                else
+                {
+                    if (layerNum < info.layer)
+                    {
+                        availableVars.Remove(v);
+                    }
+                }
+            }
+            return availableVars;
         }
 
         private CallCmd CallToYieldProc(IToken tok, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
@@ -739,7 +778,6 @@ namespace Microsoft.Boogie
                 }
                 Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);
                 frame = new HashSet<Variable>(moverTypeChecker.SharedVariables);
-                HashSet<Variable> introducedVars = new HashSet<Variable>();
                 foreach (Variable v in moverTypeChecker.SharedVariables)
                 {
                     if (moverTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || 
@@ -747,10 +785,6 @@ namespace Microsoft.Boogie
                     {
                         frame.Remove(v);
                     }
-                    if (moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum == actionInfo.createdAtLayerNum)
-                    {
-                        introducedVars.Add(v);
-                    }
                 }
                 AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
                 if (atomicActionInfo == null)
@@ -764,7 +798,7 @@ namespace Microsoft.Boogie
                 }
                 else
                 {
-                    Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, atomicActionInfo, frame, introducedVars)).TransitionRelationCompute(true);
+                    Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, atomicActionInfo, frame, new HashSet<Variable>())).TransitionRelationCompute(true);
                     beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr);
                     Expr alphaExpr = Expr.True;
                     foreach (AssertCmd assertCmd in atomicActionInfo.gate)
@@ -1178,7 +1212,7 @@ namespace Microsoft.Boogie
         public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
         {
             Program program = linearTypeChecker.program;
-            foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))
+            foreach (int layerNum in moverTypeChecker.AllImplementedLayerNums)
             {
                 if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue;
 
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index c821117a..10127d33 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -280,22 +280,129 @@ namespace Microsoft.Boogie
         }
     }
 
+    public class LayerRange
+    {
+        public int lowerLayerNum;
+        public int upperLayerNum;
+        public LayerRange(int layer)
+        {
+            this.lowerLayerNum = layer;
+            this.upperLayerNum = layer;
+        }
+        public LayerRange(int lower, int upper)
+        {
+            this.lowerLayerNum = lower;
+            this.upperLayerNum = upper;
+        }
+        public LayerRange(IEnumerable<int> layerNums)
+        {
+            int min = int.MaxValue;
+            int max = int.MinValue;
+            foreach (var layerNum in layerNums)
+            {
+                if (layerNum < min)
+                {
+                    min = layerNum;
+                }
+                if (max < layerNum)
+                {
+                    max = layerNum;
+                }
+            }
+            this.lowerLayerNum = min;
+            this.upperLayerNum = max;
+        }
+        public bool Contains(int layerNum)
+        {
+            return lowerLayerNum <= layerNum && layerNum <= upperLayerNum;
+        }
+        public bool Subset(int lower, int upper)
+        {
+            return lower <= lowerLayerNum && upperLayerNum <= upper;
+        }
+        public bool Equal(int lower, int upper)
+        {
+            return lower == lowerLayerNum && upperLayerNum == upper;
+        }
+        public bool Subset(LayerRange info)
+        {
+            return info.lowerLayerNum <= lowerLayerNum && upperLayerNum <= info.upperLayerNum;
+        }
+    }
+
+    public class AtomicProcedureInfo
+    {
+        public bool isPure;
+        public HashSet<int> layers;
+        public AtomicProcedureInfo()
+        {
+            this.isPure = true;
+            this.layers = null;
+        }
+        public AtomicProcedureInfo(HashSet<int> layers)
+        {
+            this.isPure = false;
+            this.layers = layers;
+        }
+    }
+
+    public class LocalVariableInfo
+    {
+        public bool isGhost;
+        public int layer;
+        public LocalVariableInfo(bool isGhost, int layer)
+        {
+            this.isGhost = isGhost;
+            this.layer = layer;
+        }
+    }
+
     public class MoverTypeChecker : ReadOnlyVisitor
     {
         CheckingContext checkingContext;
-        public int errorCount;
-        public Dictionary<Variable, SharedVariableInfo> globalVarToSharedVarInfo;
         Procedure enclosingProc;
         Implementation enclosingImpl;
-        public Dictionary<Procedure, ActionInfo> procToActionInfo;
+        HashSet<Variable> sharedVarsAccessed;
+        int introducedLocalVarsUpperBound;
+        int ghostVarIntroLayerAllowed;
+
         public Program program;
-        bool canAccessSharedVars;
-        bool canAccessGhostVars;
-        int minLayerNum;
-        int maxLayerNum;
+        public int errorCount;
+        public Dictionary<Variable, SharedVariableInfo> globalVarToSharedVarInfo;
+        public Dictionary<Procedure, ActionInfo> procToActionInfo;
+        public Dictionary<Procedure, AtomicProcedureInfo> procToAtomicProcedureInfo;
         public Dictionary<Absy, HashSet<int>> absyToLayerNums;
-        HashSet<Variable> ghostVars;
-        public int leastUnimplementedLayerNum;
+        public Dictionary<Variable, LocalVariableInfo> localVarToLocalVariableInfo;
+
+        public bool CallExists(CallCmd callCmd, int enclosingProcLayerNum, int layerNum)
+        {
+            if (!procToAtomicProcedureInfo.ContainsKey(callCmd.Proc))
+                return true;
+            var atomicProcedureInfo = procToAtomicProcedureInfo[callCmd.Proc];
+            if (atomicProcedureInfo.isPure)
+            {
+                return true;
+            }
+            else if (callCmd.Proc.Modifies.Count == 0)
+            {
+                if (callCmd.Outs.Count == 0)
+                    return false;
+                var outputVar = callCmd.Outs[0].Decl;
+                Debug.Assert(localVarToLocalVariableInfo.ContainsKey(outputVar));
+                if (localVarToLocalVariableInfo[outputVar].isGhost)
+                {
+                    return localVarToLocalVariableInfo[outputVar].layer == layerNum;
+                }
+                else
+                {
+                    return enclosingProcLayerNum == layerNum;
+                }
+            }
+            else
+            {
+                return enclosingProcLayerNum == layerNum;
+            }
+        }
 
         private static List<int> FindLayers(QKeyValue kv)
         {
@@ -316,6 +423,19 @@ namespace Microsoft.Boogie
             return layers;
         }
 
+        private static int Least(IEnumerable<int> layerNums)
+        {
+            int least = int.MaxValue;
+            foreach (var layer in layerNums)
+            {
+                if (layer < least)
+                {
+                    least = layer;
+                }
+            }
+            return least;
+        }
+
         private static MoverType GetMoverType(Ensures e)
         {
             if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))
@@ -331,26 +451,27 @@ namespace Microsoft.Boogie
 
         public MoverTypeChecker(Program program)
         {
-            this.ghostVars = 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.canAccessGhostVars = false;
-            this.minLayerNum = int.MaxValue;
-            this.maxLayerNum = -1;
-            this.leastUnimplementedLayerNum = int.MaxValue;
+            this.sharedVarsAccessed = null;
+            this.introducedLocalVarsUpperBound = int.MinValue;
+            this.ghostVarIntroLayerAllowed = int.MinValue;
+
+            this.localVarToLocalVariableInfo = new Dictionary<Variable, LocalVariableInfo>();
+            this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>();
+            this.globalVarToSharedVarInfo = new Dictionary<Variable, SharedVariableInfo>();
+            this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();
+            this.procToAtomicProcedureInfo = new Dictionary<Procedure, AtomicProcedureInfo>(); 
+            
             foreach (var g in program.GlobalVariables)
             {
                 List<int> layerNums = FindLayers(g.Attributes);
                 if (layerNums.Count == 0)
                 {
-                    // Cannot access atomic actions
+                    // Inaccessible from  yielding and atomic procedures
                 }
                 else if (layerNums.Count == 1)
                 {
@@ -366,7 +487,27 @@ namespace Microsoft.Boogie
                 }
             }
         }
-        
+
+        private HashSet<int> allImplementedLayerNums;
+        public IEnumerable<int> AllImplementedLayerNums
+        {
+            get
+            {
+                if (allImplementedLayerNums == null)
+                {
+                    allImplementedLayerNums = new HashSet<int>();
+                    foreach (ActionInfo actionInfo in procToActionInfo.Values)
+                    {
+                        if (actionInfo.hasImplementation)
+                        {
+                            allImplementedLayerNums.Add(actionInfo.createdAtLayerNum);
+                        }
+                    }
+                }
+                return allImplementedLayerNums;
+            }
+        }
+
         private HashSet<int> allCreatedLayerNums;
         public IEnumerable<int> AllCreatedLayerNums
         {
@@ -384,10 +525,100 @@ namespace Microsoft.Boogie
             }
         }
 
+        private LayerRange FindLayerRange()
+        {
+            int maxIntroLayerNum = int.MinValue;
+            int minHideLayerNum = int.MaxValue;
+            foreach (var g in sharedVarsAccessed)
+            {
+                if (globalVarToSharedVarInfo[g].introLayerNum > maxIntroLayerNum)
+                {
+                    maxIntroLayerNum = globalVarToSharedVarInfo[g].introLayerNum;
+                }
+                if (globalVarToSharedVarInfo[g].hideLayerNum < minHideLayerNum)
+                {
+                    minHideLayerNum = globalVarToSharedVarInfo[g].hideLayerNum;
+                }
+            }
+            return new LayerRange(maxIntroLayerNum, minHideLayerNum);
+        }
+
         public void TypeCheck()
         {
             foreach (var proc in program.Procedures)
             {
+                if (!QKeyValue.FindBoolAttribute(proc.Attributes, "pure")) continue;
+                if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))
+                {
+                    Error(proc, "Pure procedure must not yield");
+                    continue;
+                }
+                if (QKeyValue.FindBoolAttribute(proc.Attributes, "layer"))
+                {
+                    Error(proc, "Pure procedure must not have layers");
+                    continue;
+                }
+                if (proc.Modifies.Count > 0)
+                {
+                    Error(proc, "Pure procedure must not modify a global variable");
+                    continue;
+                }
+                procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo();
+            }
+            foreach (var proc in program.Procedures)
+            {
+                if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
+                var procLayerNums = RemoveDuplicatesAndSort(FindLayers(proc.Attributes));
+                if (procLayerNums.Count == 0) continue;
+                foreach (IdentifierExpr ie in proc.Modifies)
+                {
+                    if (!globalVarToSharedVarInfo.ContainsKey(ie.Decl))
+                    {
+                        Error(proc, "Atomic procedure cannot modify a global variable without layer numbers");
+                    }
+                    else if (globalVarToSharedVarInfo[ie.Decl].introLayerNum != procLayerNums[0])
+                    {
+                        Error(proc, "The introduction layer of a modified global variable must be identical to the layer of the atomic procedure");
+                    }
+                }
+                if (proc.Modifies.Count == 0 || procLayerNums.Count == 1)
+                {
+                    procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo(new HashSet<int>(procLayerNums));
+                }
+                else
+                {
+                    Error(proc, "An atomic procedure with more than one layer must not modify a global variable");
+                }
+            }
+            if (errorCount > 0) return;
+
+            foreach (Implementation impl in program.Implementations)
+            {
+                if (!procToAtomicProcedureInfo.ContainsKey(impl.Proc)) continue;
+                var atomicProcedureInfo = procToAtomicProcedureInfo[impl.Proc];
+                if (atomicProcedureInfo.isPure)
+                {
+                    this.enclosingImpl = impl;
+                    (new PurityChecker(this)).VisitImplementation(impl);
+                }
+                else 
+                {
+                    this.enclosingImpl = impl;
+                    this.sharedVarsAccessed = new HashSet<Variable>();
+                    (new PurityChecker(this)).VisitImplementation(impl);
+                    LayerRange upperBound = FindLayerRange();
+                    LayerRange lowerBound = new LayerRange(atomicProcedureInfo.layers);
+                    if (!lowerBound.Subset(upperBound))
+                    {
+                        Error(impl, "Atomic procedure cannot access global variable");
+                    }
+                    this.sharedVarsAccessed = null;
+                }
+            }
+            if (errorCount > 0) return; 
+            
+            foreach (var proc in program.Procedures)
+            {
                 if (!QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
 
                 int createdAtLayerNum;  // must be initialized by the following code, otherwise it is an error
@@ -428,25 +659,21 @@ namespace Microsoft.Boogie
                         continue;
                     }
 
-                    minLayerNum = int.MaxValue;
-                    maxLayerNum = -1;
-                    canAccessSharedVars = true;
+                    sharedVarsAccessed = new HashSet<Variable>();
                     enclosingProc = proc;
                     enclosingImpl = null;
                     base.VisitEnsures(e);
-                    canAccessSharedVars = false;
-                    if (maxLayerNum > createdAtLayerNum)
-                    {
-                        Error(e, "A variable being accessed is introduced after this action is created");
-                    }
-                    else if (availableUptoLayerNum > minLayerNum)
+                    LayerRange upperBound = FindLayerRange();
+                    LayerRange lowerBound = new LayerRange(createdAtLayerNum, availableUptoLayerNum);
+                    if (lowerBound.Subset(upperBound))
                     {
-                        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);
+                        Error(e, "A variable being accessed in this action is unavailable");
                     }
+                    sharedVarsAccessed = null;
                 }
                 if (errorCount > 0) continue;
                 if (!procToActionInfo.ContainsKey(proc))
@@ -463,27 +690,41 @@ namespace Microsoft.Boogie
                 }
             }
             if (errorCount > 0) return;
-            foreach (var impl in program.Implementations)
+            foreach (Implementation node in program.Implementations)
             {
-                if (!procToActionInfo.ContainsKey(impl.Proc)) continue;
-                procToActionInfo[impl.Proc].hasImplementation = true;
-            }
-            foreach (var proc in procToActionInfo.Keys)
-            {
-                ActionInfo actionInfo = procToActionInfo[proc];
-                if (actionInfo.isExtern && actionInfo.hasImplementation)
+                if (!procToActionInfo.ContainsKey(node.Proc)) continue;
+                foreach (Variable v in node.LocVars)
                 {
-                    Error(proc, "Extern procedure cannot have an implementation");
-                    continue;
+                    var layer = FindLocalVariableLayer(node, v, procToActionInfo[node.Proc].createdAtLayerNum);
+                    if (layer == int.MinValue) continue;
+                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(QKeyValue.FindBoolAttribute(node.Attributes, "ghost"), layer);
                 }
-                if (actionInfo.isExtern || actionInfo.hasImplementation) continue;
-                if (leastUnimplementedLayerNum == int.MaxValue)
+                for (int i = 0; i < node.Proc.InParams.Count; i++)
                 {
-                    leastUnimplementedLayerNum = actionInfo.createdAtLayerNum;
+                    Variable v = node.Proc.InParams[i];
+                    var layer = FindLocalVariableLayer(node.Proc, v, procToActionInfo[node.Proc].createdAtLayerNum);
+                    if (layer == int.MinValue) continue;
+                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer);
+                    localVarToLocalVariableInfo[node.InParams[i]] = new LocalVariableInfo(false, layer);
                 }
-                else if (leastUnimplementedLayerNum != actionInfo.createdAtLayerNum)
+                for (int i = 0; i < node.Proc.OutParams.Count; i++)
+                {
+                    Variable v = node.Proc.OutParams[i];
+                    var layer = FindLocalVariableLayer(node.Proc, v, procToActionInfo[node.Proc].createdAtLayerNum);
+                    if (layer == int.MinValue) continue;
+                    localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer);
+                    localVarToLocalVariableInfo[node.OutParams[i]] = new LocalVariableInfo(false, layer);
+                }
+            }
+            if (errorCount > 0) return;
+            foreach (var impl in program.Implementations)
+            {
+                if (!procToActionInfo.ContainsKey(impl.Proc)) continue;
+                ActionInfo actionInfo = procToActionInfo[impl.Proc];
+                procToActionInfo[impl.Proc].hasImplementation = true;
+                if (actionInfo.isExtern)
                 {
-                    Error(proc, "All unimplemented atomic actions must be created at the same layer");
+                    Error(impl.Proc, "Extern procedure cannot have an implementation");
                 }
             }
             foreach (var g in this.globalVarToSharedVarInfo.Keys)
@@ -500,15 +741,6 @@ namespace Microsoft.Boogie
             }
             if (errorCount > 0) return;
             this.VisitProgram(program);
-            foreach (Procedure proc in program.Procedures)
-            {
-                if (procToActionInfo.ContainsKey(proc)) continue;
-                foreach (var ie in proc.Modifies)
-                {
-                    if (!SharedVariables.Contains(ie.Decl)) continue;
-                    Error(proc, "A ghost procedure must not modify a global variable with layer annotation");
-                }
-            }
             if (errorCount > 0) return;
             YieldTypeChecker.PerformYieldSafeCheck(this);
             new LayerEraser().VisitProgram(program);
@@ -516,9 +748,26 @@ namespace Microsoft.Boogie
 
         public IEnumerable<Variable> SharedVariables
         {
-            get { return this.globalVarToSharedVarInfo.Keys;  }
+            get { return this.globalVarToSharedVarInfo.Keys; }
+        }
+
+        private int FindLocalVariableLayer(Declaration decl, Variable v, int enclosingProcLayerNum)
+        {
+            var layers = FindLayers(v.Attributes);
+            if (layers.Count == 0) return int.MinValue;
+            if (layers.Count > 1)
+            {
+                Error(decl, "Incorrect number of layers");
+                return int.MinValue;
+            }
+            if (layers[0] > enclosingProcLayerNum)
+            {
+                Error(decl, "Layer of local variable cannot be greater than the creation layer of enclosing procedure");
+                return int.MinValue;
+            }
+            return layers[0];
         }
-        
+
         public override Implementation VisitImplementation(Implementation node)
         {
             if (!procToActionInfo.ContainsKey(node.Proc))
@@ -527,17 +776,9 @@ namespace Microsoft.Boogie
             }
             this.enclosingImpl = node;
             this.enclosingProc = null;
-            ghostVars = new HashSet<Variable>();
-            foreach (Variable v in node.LocVars)
-            {
-                if (QKeyValue.FindBoolAttribute(v.Attributes, "ghost"))
-                {
-                    ghostVars.Add(v);
-                }
-            }
             return base.VisitImplementation(node);
         }
-        
+
         public override Procedure VisitProcedure(Procedure node)
         {
             if (!procToActionInfo.ContainsKey(node))
@@ -584,23 +825,106 @@ namespace Microsoft.Boogie
                 {
                     Error(node, "The callee is not available in the caller procedure");
                 }
-                return base.VisitCallCmd(node);
+                for (int i = 0; i < node.Ins.Count; i++)
+                {
+                    var formal = node.Proc.InParams[i];
+                    if (localVarToLocalVariableInfo.ContainsKey(formal))
+                    {
+                        introducedLocalVarsUpperBound = localVarToLocalVariableInfo[formal].layer;
+                    }
+                    Visit(node.Ins[i]);
+                    introducedLocalVarsUpperBound = int.MinValue;
+                }
+                for (int i = 0; i < node.Outs.Count; i++)
+                {
+                    var formal = node.Proc.OutParams[i];
+                    if (!localVarToLocalVariableInfo.ContainsKey(formal)) continue;
+                    var actual = node.Outs[i].Decl;
+                    if (localVarToLocalVariableInfo.ContainsKey(actual) && 
+                        localVarToLocalVariableInfo[formal].layer <= localVarToLocalVariableInfo[actual].layer)
+                        continue;
+                    Error(node, "Formal parameter of call must be introduced no later than the actual parameter");
+                }
+                return node;
             }
-            else
+            else if (procToAtomicProcedureInfo.ContainsKey(node.Proc))
             {
+                // 1. Outputs are either all ghost or all introduced.
+                // 2. All outputs have the same layer; call it output layer.
+                // 3. If callee is impure and has outputs, output layer is a member of layer set of callee.
+                // 4. If callee is impure and has introduced outputs, then creation number of caller belongs to layer set of callee.
+                // 5. If callee is impure and modifies globals, then creation number of caller belongs to layer set of callee.
+                
+                Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+                bool isGhost = false; // This assignment stops the compiler from complaining.
+                                      // In the absence of errors, isGhost is initialized by loop below.
                 foreach (var ie in node.Outs)
                 {
-                    if (ghostVars.Contains(ie.Decl)) continue;
-                    Error(node, "The output of a ghost procedure must be assigned to a ghost variable");
+                    if (localVarToLocalVariableInfo.ContainsKey(ie.Decl))
+                    {
+                        var localVariableInfo = localVarToLocalVariableInfo[ie.Decl];
+                        if (introducedLocalVarsUpperBound == int.MinValue)
+                        {
+                            introducedLocalVarsUpperBound = localVariableInfo.layer;
+                            isGhost = localVariableInfo.isGhost;
+                            var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc];
+                            if (!atomicProcedureInfo.isPure)
+                            {
+                                if (!atomicProcedureInfo.layers.Contains(introducedLocalVarsUpperBound))
+                                {
+                                    Error(node, "Layer of output variable must be a layer of the callee");
+                                }
+                                if (!isGhost && !atomicProcedureInfo.layers.Contains(enclosingProcLayerNum))
+                                {
+                                    Error(node, "The creation layer of caller must be a layer of the callee");
+                                }
+                            }
+                        }
+                        else
+                        {
+                            if (localVariableInfo.layer != introducedLocalVarsUpperBound)
+                            {
+                                Error(node, "All outputs must have the same layer");
+                            }
+                            if (localVariableInfo.isGhost != isGhost)
+                            {
+                                Error(node, "Outputs are either all ghost or all introduced");
+                            }
+                        }
+                    }
+                    else
+                    {
+                        Error(node, "Output variable must be a ghost or introduced local variable");
+                    }
+                }
+
+                if (node.Proc.Modifies.Count > 0)
+                {
+                    var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc];
+                    if (procToActionInfo[enclosingImpl.Proc] is AtomicActionInfo)
+                    {
+                        if (!atomicProcedureInfo.layers.Contains(enclosingProcLayerNum))
+                        {
+                            Error(node, "The layer of called atomic procedure must be identical to the creation layer of callee");
+                        }
+                    }
+                    else
+                    {
+                        Error(node, "Enclosing implementation must refine an atomic action");
+                    }
+                    introducedLocalVarsUpperBound = enclosingProcLayerNum;
+                }
+                foreach (var e in node.Ins)
+                {
+                    Visit(e);
                 }
-                bool savedCanAccessSharedVars = canAccessSharedVars;
-                bool savedCanAccessAuxVars = canAccessGhostVars;
-                canAccessSharedVars = true;
-                canAccessGhostVars = true;
-                var retVal = base.VisitCallCmd(node);
-                canAccessSharedVars = savedCanAccessSharedVars;
-                canAccessGhostVars = savedCanAccessAuxVars;
-                return retVal;
+                introducedLocalVarsUpperBound = int.MinValue;
+                return node;
+            }
+            else  
+            {
+                Error(node, "A yielding procedure can call only atomic or yielding procedures");
+                return node;
             }
         }
 
@@ -618,8 +942,8 @@ namespace Microsoft.Boogie
                 isLeftMover = isLeftMover && actionInfo.IsLeftMover;
                 isRightMover = isRightMover && actionInfo.IsRightMover;
                 if (actionInfo.createdAtLayerNum > maxCalleeLayerNum)
-                { 
-                    maxCalleeLayerNum = actionInfo.createdAtLayerNum; 
+                {
+                    maxCalleeLayerNum = actionInfo.createdAtLayerNum;
                 }
                 if (actionInfo is AtomicActionInfo)
                 {
@@ -645,66 +969,46 @@ namespace Microsoft.Boogie
             return base.VisitParCallCmd(node);
         }
 
-        public override Cmd VisitAssignCmd(AssignCmd node)
-        {
-            Contract.Ensures(Contract.Result<Cmd>() == node);
-            for (int i = 0; i < node.Lhss.Count; ++i)
-            {
-                bool savedCanAccessSharedVars = canAccessSharedVars;
-                bool savedCanAccessAuxVars = canAccessGhostVars;
-                Variable v = node.Lhss[i].DeepAssignedVariable;
-                if (v is LocalVariable && ghostVars.Contains(v))
-                {
-                    canAccessSharedVars = true;
-                    canAccessGhostVars = true;
-                }
-                this.Visit(node.Lhss[i]);
-                this.Visit(node.Rhss[i]);
-                canAccessSharedVars = savedCanAccessSharedVars;
-                canAccessGhostVars = savedCanAccessAuxVars;
-            }
-            return node;
-        }
-
         public override Expr VisitIdentifierExpr(IdentifierExpr node)
         {
             if (node.Decl is GlobalVariable)
             {
-                if (!canAccessSharedVars)
+                if (sharedVarsAccessed == null)
                 {
                     Error(node, "Shared variable can be accessed only in atomic actions or specifications");
                 }
                 else if (this.globalVarToSharedVarInfo.ContainsKey(node.Decl))
                 {
-                    if (this.globalVarToSharedVarInfo[node.Decl].hideLayerNum < minLayerNum)
-                    {
-                        minLayerNum = this.globalVarToSharedVarInfo[node.Decl].hideLayerNum;
-                    }
-                    if (this.globalVarToSharedVarInfo[node.Decl].introLayerNum > maxLayerNum)
-                    {
-                        maxLayerNum = this.globalVarToSharedVarInfo[node.Decl].introLayerNum;
-                    }
+                    sharedVarsAccessed.Add(node.Decl);
                 }
                 else
                 {
                     Error(node, "Accessed shared variable must have layer annotation");
                 }
             }
-            else if (node.Decl is LocalVariable && ghostVars.Contains(node.Decl) && !canAccessGhostVars)
+            else if ((node.Decl is Formal || node.Decl is Variable) && localVarToLocalVariableInfo.ContainsKey(node.Decl))
             {
-                Error(node, "Ghost variable can be accessed only in assertions");
-            }
-
+                var localVariableInfo = localVarToLocalVariableInfo[node.Decl];
+                if (localVariableInfo.isGhost)
+                {
+                    if (ghostVarIntroLayerAllowed != localVariableInfo.layer)
+                    {
+                        Error(node, "Ghost variable inaccessible");
+                    }
+                }
+                else
+                {
+                    if (introducedLocalVarsUpperBound < localVariableInfo.layer)
+                    {
+                        Error(node, "Introduced variable inaccessible");
+                    }
+                }
+            } 
             return base.VisitIdentifierExpr(node);
         }
-        
+
         public override Ensures VisitEnsures(Ensures ensures)
         {
-            minLayerNum = int.MaxValue;
-            maxLayerNum = -1;
-            canAccessSharedVars = true;
-            Ensures ret = base.VisitEnsures(ensures);
-            canAccessSharedVars = false;
             ActionInfo actionInfo = procToActionInfo[enclosingProc];
             AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
             if (atomicActionInfo != null && atomicActionInfo.ensures == ensures)
@@ -713,35 +1017,50 @@ namespace Microsoft.Boogie
             }
             else
             {
+                sharedVarsAccessed = new HashSet<Variable>();
+                Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+                introducedLocalVarsUpperBound = Least(FindLayers(ensures.Attributes));
+                base.VisitEnsures(ensures); 
                 CheckAndAddLayers(ensures, ensures.Attributes, actionInfo.createdAtLayerNum);
+                introducedLocalVarsUpperBound = int.MinValue;
+                sharedVarsAccessed = null;
             }
-            return ret;
+            return ensures;
         }
-        
+
         public override Requires VisitRequires(Requires requires)
         {
-            minLayerNum = int.MaxValue;
-            maxLayerNum = -1;
-            canAccessSharedVars = true;
-            Requires ret = base.VisitRequires(requires);
-            canAccessSharedVars = false;
+            sharedVarsAccessed = new HashSet<Variable>();
+            Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+            introducedLocalVarsUpperBound = Least(FindLayers(requires.Attributes));
+            base.VisitRequires(requires);
             CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].createdAtLayerNum);
-            return ret;
+            introducedLocalVarsUpperBound = int.MinValue;
+            sharedVarsAccessed = null;
+            return requires;
         }
 
         public override Cmd VisitAssertCmd(AssertCmd node)
         {
             if (enclosingImpl == null)
+            {
+                // in this case, we are visiting an assert inside a CodeExpr
                 return base.VisitAssertCmd(node);
-            minLayerNum = int.MaxValue;
-            maxLayerNum = -1;
-            canAccessSharedVars = true;
-            canAccessGhostVars = true;
-            Cmd ret = base.VisitAssertCmd(node);
-            canAccessGhostVars = false;
-            canAccessSharedVars = false;
+            }
+            sharedVarsAccessed = new HashSet<Variable>();
+            Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+            var layerNums = FindLayers(node.Attributes);
+            introducedLocalVarsUpperBound = Least(layerNums);
+            if (layerNums.Count == 1)
+            {
+                ghostVarIntroLayerAllowed = layerNums[0];
+            }
+            base.VisitAssertCmd(node);
             CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].createdAtLayerNum);
-            return ret;
+            introducedLocalVarsUpperBound = int.MinValue;
+            ghostVarIntroLayerAllowed = int.MinValue;
+            sharedVarsAccessed = null;
+            return node;
         }
 
         private List<int> RemoveDuplicatesAndSort(List<int> attrs)
@@ -760,10 +1079,11 @@ namespace Microsoft.Boogie
                 Error(node, "layer not present");
                 return;
             }
+            LayerRange upperBound = FindLayerRange();
             absyToLayerNums[node] = new HashSet<int>();
             foreach (int layerNum in attrs)
             {
-                if (layerNum == leastUnimplementedLayerNum || !AllCreatedLayerNums.Contains(layerNum))
+                if (!AllImplementedLayerNums.Contains(layerNum))
                 {
                     Error(node, "Illegal layer number");
                 }
@@ -771,7 +1091,7 @@ namespace Microsoft.Boogie
                 {
                     Error(node, "The layer cannot be greater than the layer of enclosing procedure");
                 }
-                else if (maxLayerNum < layerNum && layerNum <= minLayerNum)
+                else if (upperBound.Contains(layerNum))
                 {
                     absyToLayerNums[node].Add(layerNum);
                 }
@@ -787,5 +1107,67 @@ namespace Microsoft.Boogie
             checkingContext.Error(node, message);
             errorCount++;
         }
+
+        private class PurityChecker : StandardVisitor
+        {
+            private MoverTypeChecker moverTypeChecker;
+
+            public PurityChecker(MoverTypeChecker moverTypeChecker)
+            {
+                this.moverTypeChecker = moverTypeChecker;
+            }
+            
+            public override Cmd VisitCallCmd(CallCmd node)
+            {
+                Procedure enclosingProc = moverTypeChecker.enclosingImpl.Proc;
+                if (!moverTypeChecker.procToAtomicProcedureInfo.ContainsKey(node.Proc))
+                {
+                    moverTypeChecker.Error(node, "Atomic procedure can only call an atomic procedure");
+                    return base.VisitCallCmd(node);
+                }
+                var callerInfo = moverTypeChecker.procToAtomicProcedureInfo[enclosingProc];
+                var calleeInfo = moverTypeChecker.procToAtomicProcedureInfo[node.Proc];
+                if (calleeInfo.isPure)
+                {
+                    // do nothing
+                }
+                else if (callerInfo.isPure)
+                {
+                    moverTypeChecker.Error(node, "Pure procedure can only call pure procedures");
+                }
+                else if (!callerInfo.layers.IsSubsetOf(calleeInfo.layers))
+                {
+                    moverTypeChecker.Error(node, "Caller layers must be subset of callee layers");
+                }
+                return base.VisitCallCmd(node);
+            }
+
+            public override Cmd VisitParCallCmd(ParCallCmd node)
+            {
+                moverTypeChecker.Error(node, "Atomic procedures cannot make parallel calls");
+                return node;
+            }
+
+            public override Expr VisitIdentifierExpr(IdentifierExpr node)
+            {
+                Procedure enclosingProc = moverTypeChecker.enclosingImpl.Proc;
+                if (node.Decl is GlobalVariable)
+                {
+                    if (moverTypeChecker.procToAtomicProcedureInfo[enclosingProc].isPure)
+                    {
+                        moverTypeChecker.Error(node, "Pure procedure cannot access global variables");
+                    } 
+                    else if (!moverTypeChecker.globalVarToSharedVarInfo.ContainsKey(node.Decl))
+                    {
+                        moverTypeChecker.Error(node, "Atomic procedure cannot access a global variable without layer numbers");
+                    } 
+                    else 
+                    {
+                        moverTypeChecker.sharedVarsAccessed.Add(node.Decl);
+                    }
+                }
+                return node;
+            }
+        }
     }
-}
\ No newline at end of file
+}
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index a698c8fd..5b479ed5 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -141,7 +141,7 @@ namespace Microsoft.Boogie
                 Graph<Block> implGraph = Program.GraphFromImpl(impl);
                 implGraph.ComputeLoops();
                 int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum;
-                foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))
+                foreach (int layerNum in moverTypeChecker.AllImplementedLayerNums)
                 {
                     if (layerNum > specLayerNum) continue;
                     YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, layerNum, implGraph.Headers);
diff --git a/Test/civl/alloc.bpl b/Test/civl/alloc.bpl
new file mode 100644
index 00000000..33535b00
--- /dev/null
+++ b/Test/civl/alloc.bpl
@@ -0,0 +1,158 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
+
+type lmap;
+function {:linear "mem"} dom(lmap): [int]bool;
+function map(lmap): [int]int;
+function cons([int]bool, [int]int) : lmap;
+axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && map(cons(x,y)) == y);
+
+function EmptyLmap(): (lmap);
+axiom (dom(EmptyLmap()) == MapConstBool(false));
+
+function Add(x: lmap, i: int, v: int): (lmap);
+axiom (forall x: lmap, i: int, v: int :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]);
+
+function Remove(x: lmap, i: int): (lmap);
+axiom (forall x: lmap, i: int :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));
+
+procedure {:yields} {:layer 2} Main()
+requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+{
+   var {:layer 1} {:linear "mem"} l: lmap;
+   var i: int;
+   par Yield() | Dummy();
+   while (*)
+   invariant {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+   {
+      call  l, i := Alloc();
+      async call Thread(l, i);
+      par Yield() | Dummy();
+   }
+   par Yield() | Dummy();
+}
+
+procedure {:yields} {:layer 2} Thread({:layer 1} {:linear_in "mem"} local_in: lmap, i: int)
+requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} dom(local_in)[i] && map(local_in)[i] == mem[i];
+requires {:layer 2} dom(local_in)[i];
+{
+    var y, o: int;
+    var {:layer 1} {:linear "mem"} local: lmap;
+    var {:layer 1} {:linear "mem"} l: lmap;
+
+    par YieldMem(local_in, i) | Dummy();
+    call local := Copy(local_in);
+    call local := Write(local, i, 42);
+    call o := Read(local, i);
+    assert {:layer 2} o == 42;
+    while (*)
+    invariant {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+    {
+        call l, y := Alloc();
+        call l := Write(l, y, 42);
+	call o := Read(l, y);
+	assert {:layer 2} o == 42;
+        call Free(l);
+	par Yield() | Dummy();
+    }
+    par Yield() | Dummy();
+}
+
+procedure {:pure} {:inline 1} Copy({:linear_in "mem"} l: lmap) returns ({:linear "mem"} l': lmap)
+{
+    l' := l;
+}
+
+procedure {:yields} {:layer 1,2} Alloc() returns ({:layer 1} {:linear "mem"} l: lmap, i: int)
+requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+ensures {:right} |{ A: assume dom(l)[i]; return true; }|;
+{
+    call Yield();
+    call i := PickAddr();
+    call l := AllocLinear(i);
+    call YieldMem(l, i);
+}
+
+procedure {:yields} {:layer 1,2} Free({:layer 1} {:linear_in "mem"} l: lmap)
+requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:both} |{ A: return true; }|;
+{
+    call Yield();
+}
+
+procedure {:yields} {:layer 1,2} Read({:layer 1} {:linear "mem"} l: lmap, i: int) returns (o: int)
+requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+ensures {:both} |{ A: assert dom(l)[i]; o := map(l)[i]; return true; }|;
+{
+    call YieldMem(l, i);
+    call o := ReadLow(i);
+    call YieldMem(l, i);
+}
+
+procedure {:yields} {:layer 1,2} Write({:layer 1} {:linear_in "mem"} l: lmap, i: int, o: int) returns ({:layer 1} {:linear "mem"} l': lmap)
+requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+ensures {:layer 1} dom(l')[i] && map(l')[i] == mem[i];
+ensures {:both} |{ A: assert dom(l)[i]; l' := cons(dom(l), map(l)[i := o]); return true; }|;
+{
+    call YieldMem(l, i);
+    call WriteLow(i, o);
+    call l' := WriteLinear(l, i, o);
+    call YieldMem(l', i);
+}
+
+procedure {:layer 1} AllocLinear(i: int) returns ({:linear "mem"} l: lmap);
+modifies pool;
+requires dom(pool)[i];
+ensures pool == Remove(old(pool), i) && dom(l)[i] && map(l)[i] == mem[i];
+
+procedure {:layer 1} WriteLinear({:layer 1} {:linear_in "mem"} l: lmap, i: int, o: int) returns ({:layer 1} {:linear "mem"} l': lmap);
+requires dom(l)[i];
+ensures l' == cons(dom(l), map(l)[i := o]);
+
+procedure {:yields} {:layer 1} Yield()
+requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+{
+    yield;
+    assert {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+}
+
+procedure {:yields} {:layer 1} YieldMem({:layer 1} {:linear "mem"} l: lmap, i: int)
+requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+ensures {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+{
+    yield;
+    assert {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+    assert {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+}
+
+procedure {:yields} {:layer 2} Dummy()
+{
+    yield;
+}
+
+var {:layer 1, 1} pool: lmap;
+var {:layer 0, 1} mem:[int]int;
+var {:layer 0, 1} unallocated:[int]bool;
+
+procedure {:yields} {:layer 0, 1} ReadLow(i: int) returns (o: int);
+ensures {:atomic} |{ A: o := mem[i]; return true; }|;
+
+procedure {:yields} {:layer 0, 1} WriteLow(i: int, o: int);
+ensures {:atomic} |{ A: mem[i] := o; return true; }|;
+
+procedure {:yields} {:layer 0, 1} PickAddr() returns (i: int);
+ensures {:atomic} |{ A: assume unallocated[i]; unallocated[i] := false; return true; }|;
\ No newline at end of file
diff --git a/Test/civl/alloc.bpl.expect b/Test/civl/alloc.bpl.expect
new file mode 100644
index 00000000..f08c6e00
--- /dev/null
+++ b/Test/civl/alloc.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 12 verified, 0 errors
diff --git a/Test/civl/ghost.bpl b/Test/civl/ghost.bpl
index 74d16acf..1468fa56 100644
--- a/Test/civl/ghost.bpl
+++ b/Test/civl/ghost.bpl
@@ -5,7 +5,7 @@ var {:layer 0} x: int;
 procedure {:yields} {:layer 0,1} Incr();
 ensures {:right} |{ A: x := x + 1; return true; }|;
 
-procedure ghost(y: int) returns (z: int)
+procedure {:pure} ghost(y: int) returns (z: int)
 requires y == 1;
 ensures z == 2;
 {
@@ -15,8 +15,7 @@ ensures z == 2;
 procedure {:yields} {:layer 1,2} Incr2() 
 ensures {:right} |{ A: x := x + 2; return true; }|;
 {
-  var {:ghost} a: int;
-  var {:ghost} b: int;
+  var {:layer 1} a: int;
 
   yield;
   call a := ghost(1);
@@ -25,7 +24,7 @@ ensures {:right} |{ A: x := x + 2; return true; }|;
   yield;
 }
 
-procedure ghost_0() returns (z: int)
+procedure {:layer 1} ghost_0() returns (z: int)
 ensures z == x;
 {
   z := x;
@@ -34,8 +33,8 @@ ensures z == x;
 procedure {:yields} {:layer 1,2} Incr2_0() 
 ensures {:right} |{ A: x := x + 2; return true; }|;
 {
-  var {:ghost} a: int;
-  var {:ghost} b: int;
+  var {:layer 1} a: int;
+  var {:layer 1} b: int;
 
   yield;
   call a := ghost_0();
diff --git a/Test/civl/lock-introduced.bpl b/Test/civl/lock-introduced.bpl
index fa0a3977..5403e5d4 100644
--- a/Test/civl/lock-introduced.bpl
+++ b/Test/civl/lock-introduced.bpl
@@ -67,6 +67,9 @@ ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|;
     yield;
     L: 
         call status := CAS(false, true);
+        if (status) {
+	    call SetLock(tid);
+	}
 	yield;
         goto A, B;
 
@@ -85,9 +88,16 @@ ensures {:atomic} |{ A: b := false; lock := nil; return true; }|;
 {
     yield;
     call SET(false);
+    call SetLock(nil);
     yield;
 }
 
+procedure {:layer 1} {:inline 1} SetLock(v: X)
+modifies lock;
+{
+    lock := v;
+}
+
 procedure {:yields} {:layer 0,1} CAS(prev: bool, next: bool) returns (status: bool);
 ensures {:atomic} |{ 
 A: goto B, C; 
diff --git a/Test/civl/wsq.bpl b/Test/civl/wsq.bpl
index 17f53401..39dad919 100644
--- a/Test/civl/wsq.bpl
+++ b/Test/civl/wsq.bpl
@@ -89,13 +89,11 @@ ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
 ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := IN_Q; return true; }|;
 {
    var t: int;
-   var {:ghost} oldH:int;
-   var {:ghost} oldT:int;
-   var {:ghost} oldStatusT:bool;
+   var {:ghost} {:layer 3} oldH:int;
+   var {:ghost} {:layer 3} oldT:int;
+   var {:ghost} {:layer 3} oldStatusT:bool;
    
-
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
    assert {:layer 3} {:expand} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -104,8 +102,7 @@ ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := I
 
    call t := readT_put(tid);
 
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && put_in_cs;
    assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -115,9 +112,8 @@ ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := I
    
    call writeItems_put(tid,t, task);
 
-   oldH := H;
-   oldT := T;
-   oldStatusT := status[T];
+   call oldH, oldT := GhostRead();
+   call oldStatusT := GhostReadStatus();
    yield;
    assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && t == T && tid == ptTid && !take_in_cs && put_in_cs;
    assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -128,8 +124,7 @@ ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := I
    
    call writeT_put(tid, t+1);
 
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
    assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -147,11 +142,10 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 {
    var h, t: int;
    var chk: bool;
-   var {:ghost} oldH:int;
-   var {:ghost} oldT:int;
+   var {:ghost} {:layer 3} oldH:int;
+   var {:ghost} {:layer 3} oldT:int;
 
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
    assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -164,8 +158,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
    invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
    {
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
     assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -173,8 +166,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
     
        call t := readT_take_init(tid);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
        assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
@@ -185,8 +177,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        t := t-1;
        call writeT_take(tid, t);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !take_in_cs && !put_in_cs && t_ss[tid] == t;
        assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
@@ -196,8 +187,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
     
        call h := readH_take(tid);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs  && !put_in_cs && h_ss[tid] == h && t_ss[tid] == t;  
        assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
@@ -214,8 +204,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
            call writeT_take_abort(tid, h);
            task := EMPTY;
  
-           oldH := H;
-           oldT := T;
+           call oldH, oldT := GhostRead();
            yield;
         assert {:layer 3} h <= H;
            assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; 
@@ -227,8 +216,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 
        call task, taskstatus := readItems(tid, t);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} H >= h;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs && h_ss[tid] == h && t_ss[tid] == t;  
@@ -240,8 +228,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        if(t>h) {
         call takeExitCS(tid);
 
-           oldH := H;
-           oldT := T;    
+           call oldH, oldT := GhostRead();    
            yield;
            assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && h_ss[tid] == h && t_ss[tid] == t;  
         assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -250,8 +237,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
            return;
        }
 	   call writeT_take_eq(tid, h+1);
-	   oldH := H;
-       oldT := T;
+	   call oldH, oldT := GhostRead();
 	   
 	   yield;
 	   assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;
@@ -265,8 +251,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        call chk := CAS_H_take(tid, h,h+1);
 
 
-       oldH := H;
-       oldT := T;    
+       call oldH, oldT := GhostRead();    
        yield;
 	assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == oldH -1 && task != EMPTY);
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;  
@@ -279,8 +264,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 
        if(!chk) {
     
-          oldH := H;
-          oldT := T;    
+          call oldH, oldT := GhostRead();    
           yield;
           assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;  
          assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -290,8 +274,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
           goto LOOP_ENTRY_1;
        }
 
-       oldH := H;
-       oldT := T;    
+       call oldH, oldT := GhostRead();    
        yield;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;  
     assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -301,8 +284,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        return;
    }
    
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !put_in_cs;
    assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -322,11 +304,10 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 {
    var h, t: int;
    var chk: bool;
-   var {:ghost} oldH:int;
-   var {:ghost} oldT:int;
+   var {:ghost} {:layer 3} oldH:int;
+   var {:ghost} {:layer 3} oldT:int;
 
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} stealerTid(tid);
    assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
@@ -341,8 +322,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
    invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
    invariant {:layer 3} !steal_in_cs[tid];
    {
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} stealerTid(tid);
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
@@ -352,8 +332,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
     
        call h := readH_steal(tid);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} H >= h;
     assert {:layer 3} !steal_in_cs[tid];
@@ -365,8 +344,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        call t := readT_steal(tid);
 
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} steal_in_cs[tid];
     assert {:layer 3} stealerTid(tid) && H >= h && steal_in_cs[tid] && h_ss[tid] == h;
@@ -381,8 +359,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
            task := EMPTY;
         call stealExitCS(tid);
 
-           oldH := H;
-           oldT := T;
+        call oldH, oldT := GhostRead();
            yield;
         assert {:layer 3} !steal_in_cs[tid];
         assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid] && h_ss[tid] == h;
@@ -395,8 +372,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        call task, taskstatus := readItems(tid, h);
 
 
-       oldH := H;
-       oldT := T;
+    call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} stealerTid(tid) && steal_in_cs[tid] && h_ss[tid] == h;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
@@ -408,8 +384,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 
        call chk := CAS_H_steal(tid, h,h+1);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} h_ss[tid] == h;
     assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == h && task != EMPTY && taskstatus == IN_Q);
@@ -423,8 +398,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
           goto LOOP_ENTRY_2;
        }
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid];
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
@@ -433,14 +407,24 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        return;
    }
    
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} chk && task != EMPTY;
    assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid];
    assert {:layer 3} oldH <= H;
 }
 
+procedure {:layer 3} {:inline 1} GhostRead() returns (oldH: int, oldT: int)
+{
+   oldH := H;
+   oldT := T;
+}
+
+procedure {:layer 3} {:inline 1} GhostReadStatus() returns (oldStatus: bool)
+{
+   oldStatus := status[T];
+}
+
 procedure {:yields}{:layer 0,3} readH_take({:linear "tid"} tid:Tid) returns (y: int);
 ensures {:atomic} |{A:  assert tid == ptTid;
                        y := H;