From 5927744da636063556118f469cc8f9354b1cabe6 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Fri, 25 Sep 2015 12:05:19 -0700 Subject: added introduced and ghost local variables --- Source/Concurrency/OwickiGries.cs | 54 ++- Source/Concurrency/TypeCheck.cs | 660 ++++++++++++++++++++++++++------- Source/Concurrency/YieldTypeChecker.cs | 2 +- Test/civl/alloc.bpl | 158 ++++++++ Test/civl/alloc.bpl.expect | 2 + Test/civl/ghost.bpl | 11 +- Test/civl/lock-introduced.bpl | 10 + Test/civl/wsq.bpl | 106 +++--- 8 files changed, 786 insertions(+), 217 deletions(-) create mode 100644 Test/civl/alloc.bpl create mode 100644 Test/civl/alloc.bpl.expect 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 newCmds) @@ -291,7 +303,34 @@ namespace Microsoft.Boogie private IEnumerable AvailableLinearVars(Absy absy) { - return linearTypeChecker.AvailableLinearVars(absyMap[absy]); + HashSet availableVars = new HashSet(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 ogOldGlobalMap, Dictionary domainNameToLocalVar) @@ -739,7 +778,6 @@ namespace Microsoft.Boogie } Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap); frame = new HashSet(moverTypeChecker.SharedVariables); - HashSet introducedVars = new HashSet(); 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())).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 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 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 layers; + public AtomicProcedureInfo() + { + this.isPure = true; + this.layers = null; + } + public AtomicProcedureInfo(HashSet 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 globalVarToSharedVarInfo; Procedure enclosingProc; Implementation enclosingImpl; - public Dictionary procToActionInfo; + HashSet sharedVarsAccessed; + int introducedLocalVarsUpperBound; + int ghostVarIntroLayerAllowed; + public Program program; - bool canAccessSharedVars; - bool canAccessGhostVars; - int minLayerNum; - int maxLayerNum; + public int errorCount; + public Dictionary globalVarToSharedVarInfo; + public Dictionary procToActionInfo; + public Dictionary procToAtomicProcedureInfo; public Dictionary> absyToLayerNums; - HashSet ghostVars; - public int leastUnimplementedLayerNum; + public Dictionary 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 FindLayers(QKeyValue kv) { @@ -316,6 +423,19 @@ namespace Microsoft.Boogie return layers; } + private static int Least(IEnumerable 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(); - this.absyToLayerNums = new Dictionary>(); - this.globalVarToSharedVarInfo = new Dictionary(); - this.procToActionInfo = new Dictionary(); 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(); + this.absyToLayerNums = new Dictionary>(); + this.globalVarToSharedVarInfo = new Dictionary(); + this.procToActionInfo = new Dictionary(); + this.procToAtomicProcedureInfo = new Dictionary(); + foreach (var g in program.GlobalVariables) { List 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 allImplementedLayerNums; + public IEnumerable AllImplementedLayerNums + { + get + { + if (allImplementedLayerNums == null) + { + allImplementedLayerNums = new HashSet(); + foreach (ActionInfo actionInfo in procToActionInfo.Values) + { + if (actionInfo.hasImplementation) + { + allImplementedLayerNums.Add(actionInfo.createdAtLayerNum); + } + } + } + return allImplementedLayerNums; + } + } + private HashSet allCreatedLayerNums; public IEnumerable AllCreatedLayerNums { @@ -384,8 +525,98 @@ 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(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(); + (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; @@ -428,25 +659,21 @@ namespace Microsoft.Boogie continue; } - minLayerNum = int.MaxValue; - maxLayerNum = -1; - canAccessSharedVars = true; + sharedVarsAccessed = new HashSet(); 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 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(); - 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() == 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(); + 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(); + 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(); + 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 RemoveDuplicatesAndSort(List attrs) @@ -760,10 +1079,11 @@ namespace Microsoft.Boogie Error(node, "layer not present"); return; } + LayerRange upperBound = FindLayerRange(); absyToLayerNums[node] = new HashSet(); 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 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; -- cgit v1.2.3