diff options
Diffstat (limited to 'Source/Concurrency')
| -rw-r--r-- | Source/Concurrency/CivlRefinement.cs (renamed from Source/Concurrency/OwickiGries.cs) | 106 | ||||
| -rw-r--r-- | Source/Concurrency/CivlTypeChecker.cs (renamed from Source/Concurrency/TypeCheck.cs) | 679 | ||||
| -rw-r--r-- | Source/Concurrency/Concurrency.csproj | 8 | ||||
| -rw-r--r-- | Source/Concurrency/LinearSets.cs | 3 | ||||
| -rw-r--r-- | Source/Concurrency/MoverCheck.cs | 26 | ||||
| -rw-r--r-- | Source/Concurrency/Program.cs | 12 | ||||
| -rw-r--r-- | Source/Concurrency/YieldTypeChecker.cs | 36 |
7 files changed, 631 insertions, 239 deletions
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/CivlRefinement.cs index 2ad08024..75ff2358 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/CivlRefinement.cs @@ -13,7 +13,7 @@ namespace Microsoft.Boogie { public class MyDuplicator : Duplicator { - MoverTypeChecker moverTypeChecker; + CivlTypeChecker civlTypeChecker; public int layerNum; Procedure enclosingProc; Implementation enclosingImpl; @@ -23,9 +23,9 @@ namespace Microsoft.Boogie public HashSet<Procedure> yieldingProcs; public List<Implementation> impls; - public MyDuplicator(MoverTypeChecker moverTypeChecker, int layerNum) + public MyDuplicator(CivlTypeChecker civlTypeChecker, int layerNum) { - this.moverTypeChecker = moverTypeChecker; + this.civlTypeChecker = civlTypeChecker; this.layerNum = layerNum; this.enclosingProc = null; this.enclosingImpl = null; @@ -38,11 +38,19 @@ namespace Microsoft.Boogie private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List<Cmd> newCmds) { - int enclosingProcLayerNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum; + int enclosingProcLayerNum = civlTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum; Procedure originalProc = originalCallCmd.Proc; - if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc)) + + if (civlTypeChecker.procToAtomicProcedureInfo.ContainsKey(originalProc)) + { + if (civlTypeChecker.CallExists(originalCallCmd, enclosingProcLayerNum, layerNum)) + { + newCmds.Add(callCmd); + } + } + else if (civlTypeChecker.procToActionInfo.ContainsKey(originalProc)) { - AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo; + AtomicActionInfo atomicActionInfo = civlTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo; if (atomicActionInfo != null && atomicActionInfo.gate.Count > 0 && layerNum == enclosingProcLayerNum) { newCmds.Add(new HavocCmd(Token.NoToken, new List<IdentifierExpr>(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) }))); @@ -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) @@ -66,7 +78,7 @@ namespace Microsoft.Boogie int maxCalleeLayerNum = 0; foreach (CallCmd iter in originalParCallCmd.CallCmds) { - int calleeLayerNum = moverTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum; + int calleeLayerNum = civlTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum; if (calleeLayerNum > maxCalleeLayerNum) maxCalleeLayerNum = calleeLayerNum; } @@ -144,7 +156,7 @@ namespace Microsoft.Boogie public override Procedure VisitProcedure(Procedure node) { - if (!moverTypeChecker.procToActionInfo.ContainsKey(node)) + if (!civlTypeChecker.procToActionInfo.ContainsKey(node)) return node; if (!procMap.ContainsKey(node)) { @@ -155,7 +167,7 @@ namespace Microsoft.Boogie proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies); proc.OutParams = this.VisitVariableSeq(node.OutParams); - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[node]; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[node]; if (actionInfo.createdAtLayerNum < layerNum) { proc.Requires = new List<Requires>(); @@ -198,7 +210,7 @@ namespace Microsoft.Boogie } procMap[node] = proc; proc.Modifies = new List<IdentifierExpr>(); - moverTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x))); + civlTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x))); } return procMap[node]; } @@ -220,7 +232,7 @@ namespace Microsoft.Boogie Requires requires = base.VisitRequires(node); if (node.Free) return requires; - if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) + if (!civlTypeChecker.absyToLayerNums[node].Contains(layerNum)) requires.Condition = Expr.True; return requires; } @@ -230,12 +242,12 @@ namespace Microsoft.Boogie Ensures ensures = base.VisitEnsures(node); if (node.Free) return ensures; - AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo; + AtomicActionInfo atomicActionInfo = civlTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo; bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node; - if (isAtomicSpecification || !moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) + if (isAtomicSpecification || !civlTypeChecker.absyToLayerNums[node].Contains(layerNum)) { ensures.Condition = Expr.True; - ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes); + ensures.Attributes = CivlRefinement.RemoveMoverAttribute(ensures.Attributes); } return ensures; } @@ -243,16 +255,16 @@ namespace Microsoft.Boogie public override Cmd VisitAssertCmd(AssertCmd node) { AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node); - if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) + if (!civlTypeChecker.absyToLayerNums[node].Contains(layerNum)) assertCmd.Expr = Expr.True; return assertCmd; } } - public class OwickiGries + public class CivlRefinement { LinearTypeChecker linearTypeChecker; - MoverTypeChecker moverTypeChecker; + CivlTypeChecker civlTypeChecker; Dictionary<Absy, Absy> absyMap; Dictionary<Implementation, Implementation> implMap; HashSet<Procedure> yieldingProcs; @@ -269,17 +281,17 @@ namespace Microsoft.Boogie Expr beta; HashSet<Variable> frame; - public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator) + public CivlRefinement(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, MyDuplicator duplicator) { this.linearTypeChecker = linearTypeChecker; - this.moverTypeChecker = moverTypeChecker; + this.civlTypeChecker = civlTypeChecker; this.absyMap = duplicator.absyMap; this.layerNum = duplicator.layerNum; this.implMap = duplicator.implMap; this.yieldingProcs = duplicator.yieldingProcs; Program program = linearTypeChecker.program; globalMods = new List<IdentifierExpr>(); - foreach (Variable g in moverTypeChecker.SharedVariables) + foreach (Variable g in civlTypeChecker.SharedVariables) { globalMods.Add(Expr.Ident(g)); } @@ -291,7 +303,24 @@ 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 civlTypeChecker.globalVarToSharedVarInfo.Keys) + { + SharedVariableInfo info = civlTypeChecker.globalVarToSharedVarInfo[g]; + if (!(info.introLayerNum <= layerNum && layerNum <= info.hideLayerNum)) + { + availableVars.Remove(g); + } + } + foreach (var v in civlTypeChecker.localVarToLocalVariableInfo.Keys) + { + LocalVariableInfo info = civlTypeChecker.localVarToLocalVariableInfo[v]; + if (layerNum < info.layer) + { + availableVars.Remove(v); + } + } + return availableVars; } private CallCmd CallToYieldProc(IToken tok, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar) @@ -715,7 +744,7 @@ namespace Microsoft.Boogie } Procedure originalProc = implMap[impl].Proc; - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc]; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[originalProc]; if (actionInfo.createdAtLayerNum == this.layerNum) { pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool)); @@ -738,19 +767,14 @@ namespace Microsoft.Boogie foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]); } Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap); - frame = new HashSet<Variable>(moverTypeChecker.SharedVariables); - HashSet<Variable> introducedVars = new HashSet<Variable>(); - foreach (Variable v in moverTypeChecker.SharedVariables) + frame = new HashSet<Variable>(civlTypeChecker.SharedVariables); + foreach (Variable v in civlTypeChecker.SharedVariables) { - if (moverTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || - moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum) + if (civlTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || + civlTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum) { frame.Remove(v); } - if (moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum == actionInfo.createdAtLayerNum) - { - introducedVars.Add(v); - } } AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; if (atomicActionInfo == null) @@ -764,7 +788,7 @@ namespace Microsoft.Boogie } else { - Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, atomicActionInfo, frame, introducedVars)).TransitionRelationCompute(true); + Expr betaExpr = (new MoverCheck.TransitionRelationComputation(civlTypeChecker.program, atomicActionInfo, frame, new HashSet<Variable>())).TransitionRelationCompute(true); beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr); Expr alphaExpr = Expr.True; foreach (AssertCmd assertCmd in atomicActionInfo.gate) @@ -1175,31 +1199,31 @@ namespace Microsoft.Boogie return decls; } - public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls) + public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls) { Program program = linearTypeChecker.program; - foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum })) + foreach (int layerNum in civlTypeChecker.AllLayerNums) { if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue; - MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, layerNum); + MyDuplicator duplicator = new MyDuplicator(civlTypeChecker, layerNum); foreach (var proc in program.Procedures) { - if (!moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue; + if (!civlTypeChecker.procToActionInfo.ContainsKey(proc)) continue; Procedure duplicateProc = duplicator.VisitProcedure(proc); decls.Add(duplicateProc); } decls.AddRange(duplicator.impls); - OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator); + CivlRefinement civlTransform = new CivlRefinement(linearTypeChecker, civlTypeChecker, duplicator); foreach (var impl in program.Implementations) { - if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum) + if (!civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum) continue; Implementation duplicateImpl = duplicator.VisitImplementation(impl); - ogTransform.TransformImpl(duplicateImpl); + civlTransform.TransformImpl(duplicateImpl); decls.Add(duplicateImpl); } - decls.AddRange(ogTransform.Collect()); + decls.AddRange(civlTransform.Collect()); } } } diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/CivlTypeChecker.cs index c821117a..b426d9ed 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/CivlTypeChecker.cs @@ -280,22 +280,111 @@ namespace Microsoft.Boogie } } - public class MoverTypeChecker : ReadOnlyVisitor + 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 LayerRange layerRange; + public AtomicProcedureInfo() + { + this.isPure = true; + this.layerRange = null; + } + public AtomicProcedureInfo(LayerRange layerRange) + { + this.isPure = false; + this.layerRange = layerRange; + } + } + + public class LocalVariableInfo + { + public int layer; + public LocalVariableInfo(int layer) + { + this.layer = layer; + } + } + + public class CivlTypeChecker : 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; + 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; + Dictionary<CallCmd, int> pureCallLayer; + + public bool CallExists(CallCmd callCmd, int enclosingProcLayerNum, int layerNum) + { + Debug.Assert(procToAtomicProcedureInfo.ContainsKey(callCmd.Proc)); + var atomicProcedureInfo = procToAtomicProcedureInfo[callCmd.Proc]; + if (atomicProcedureInfo.isPure) + { + return pureCallLayer[callCmd] <= layerNum; + } + else + { + return enclosingProcLayerNum == layerNum; + } + } private static List<int> FindLayers(QKeyValue kv) { @@ -316,6 +405,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")) @@ -329,28 +431,29 @@ namespace Microsoft.Boogie return MoverType.Top; } - public MoverTypeChecker(Program program) + public CivlTypeChecker(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.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>(); + this.pureCallLayer = new Dictionary<CallCmd, int>(); + 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,28 +469,137 @@ namespace Microsoft.Boogie } } } - - private HashSet<int> allCreatedLayerNums; - public IEnumerable<int> AllCreatedLayerNums + + private HashSet<int> allLayerNums; + public IEnumerable<int> AllLayerNums { get { - if (allCreatedLayerNums == null) + if (allLayerNums == null) { - allCreatedLayerNums = new HashSet<int>(); + allLayerNums = new HashSet<int>(); foreach (ActionInfo actionInfo in procToActionInfo.Values) { - allCreatedLayerNums.Add(actionInfo.createdAtLayerNum); + allLayerNums.Add(actionInfo.createdAtLayerNum); + } + foreach (var layerNums in absyToLayerNums.Values) + { + foreach (var layer in layerNums) + { + allLayerNums.Add(layer); + } } } - return allCreatedLayerNums; + return allLayerNums; + } + } + + 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 = 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"); + continue; + } + } + int lower, upper; + if (procLayerNums.Count == 1) + { + lower = procLayerNums[0]; + upper = procLayerNums[0]; + } + else if (procLayerNums.Count == 2) + { + lower = procLayerNums[0]; + upper = procLayerNums[1]; + if (lower >= upper) + { + Error(proc, "Lower layer must be less than upper layer"); + continue; + } + } + else + { + Error(proc, "Atomic procedure must specify a layer range"); + continue; + } + LayerRange layerRange = new LayerRange(lower, upper); + procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo(layerRange); + } + 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 = atomicProcedureInfo.layerRange; + 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 +640,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,52 +671,63 @@ namespace Microsoft.Boogie } } 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; - } - foreach (var proc in procToActionInfo.Keys) - { - ActionInfo actionInfo = procToActionInfo[proc]; - if (actionInfo.isExtern && actionInfo.hasImplementation) + if (actionInfo.isExtern) { - Error(proc, "Extern procedure cannot have an implementation"); - continue; + Error(impl.Proc, "Extern procedure cannot have an implementation"); } - if (actionInfo.isExtern || actionInfo.hasImplementation) continue; - if (leastUnimplementedLayerNum == int.MaxValue) + } + if (errorCount > 0) return; + + foreach (Procedure proc in procToActionInfo.Keys) + { + for (int i = 0; i < proc.InParams.Count; i++) { - leastUnimplementedLayerNum = actionInfo.createdAtLayerNum; + Variable v = proc.InParams[i]; + var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum); + if (layer == int.MinValue) continue; + localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer); } - else if (leastUnimplementedLayerNum != actionInfo.createdAtLayerNum) + for (int i = 0; i < proc.OutParams.Count; i++) { - Error(proc, "All unimplemented atomic actions must be created at the same layer"); + Variable v = proc.OutParams[i]; + var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum); + if (layer == int.MinValue) continue; + localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer); } } - foreach (var g in this.globalVarToSharedVarInfo.Keys) + foreach (Implementation node in program.Implementations) { - var info = globalVarToSharedVarInfo[g]; - if (!this.AllCreatedLayerNums.Contains(info.introLayerNum)) + if (!procToActionInfo.ContainsKey(node.Proc)) continue; + foreach (Variable v in node.LocVars) { - Error(g, "Variable must be introduced with creation of some atomic action"); + var layer = FindLocalVariableLayer(node, v, procToActionInfo[node.Proc].createdAtLayerNum); + if (layer == int.MinValue) continue; + localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer); } - if (info.hideLayerNum != int.MaxValue && !this.AllCreatedLayerNums.Contains(info.hideLayerNum)) + for (int i = 0; i < node.Proc.InParams.Count; i++) { - Error(g, "Variable must be hidden with creation of some atomic action"); + Variable v = node.Proc.InParams[i]; + if (!localVarToLocalVariableInfo.ContainsKey(v)) continue; + var layer = localVarToLocalVariableInfo[v].layer; + localVarToLocalVariableInfo[node.InParams[i]] = new LocalVariableInfo(layer); } - } - if (errorCount > 0) return; - this.VisitProgram(program); - foreach (Procedure proc in program.Procedures) - { - if (procToActionInfo.ContainsKey(proc)) continue; - foreach (var ie in proc.Modifies) + for (int i = 0; i < node.Proc.OutParams.Count; i++) { - if (!SharedVariables.Contains(ie.Decl)) continue; - Error(proc, "A ghost procedure must not modify a global variable with layer annotation"); + Variable v = node.Proc.OutParams[i]; + if (!localVarToLocalVariableInfo.ContainsKey(v)) continue; + var layer = localVarToLocalVariableInfo[v].layer; + localVarToLocalVariableInfo[node.OutParams[i]] = new LocalVariableInfo(layer); } } + if (errorCount > 0) return; + + this.VisitProgram(program); if (errorCount > 0) return; YieldTypeChecker.PerformYieldSafeCheck(this); new LayerEraser().VisitProgram(program); @@ -516,9 +735,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 +763,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 +812,117 @@ 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++) + { + Visit(node.Ins[i]); + if (introducedLocalVarsUpperBound != int.MinValue) + { + var formal = node.Proc.InParams[i]; + if (!localVarToLocalVariableInfo.ContainsKey(formal) || + introducedLocalVarsUpperBound > localVarToLocalVariableInfo[formal].layer) + { + Error(node, "An introduced local variable is accessed but not available"); + } + 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)) { - foreach (var ie in node.Outs) + var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc]; + if (atomicProcedureInfo.isPure) { - if (ghostVars.Contains(ie.Decl)) continue; - Error(node, "The output of a ghost procedure must be assigned to a ghost variable"); + if (node.Outs.Count > 0) + { + int inferredLayer = int.MinValue; + foreach (var ie in node.Outs) + { + if (!localVarToLocalVariableInfo.ContainsKey(ie.Decl)) continue; + if (inferredLayer < localVarToLocalVariableInfo[ie.Decl].layer) + { + inferredLayer = localVarToLocalVariableInfo[ie.Decl].layer; + } + } + pureCallLayer[node] = inferredLayer; + if (inferredLayer != int.MinValue) + { + foreach (var ie in node.Outs) + { + if (!localVarToLocalVariableInfo.ContainsKey(ie.Decl)) + { + Error(node, "Output variable must be introduced"); + } + else if (inferredLayer != localVarToLocalVariableInfo[ie.Decl].layer) + { + Error(node, "All output variables must be introduced at the same layer"); + } + } + } + Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); + foreach (var e in node.Ins) + { + Visit(e); + if (inferredLayer < introducedLocalVarsUpperBound) + { + Error(node, "An introduced local variable is not accessible"); + } + introducedLocalVarsUpperBound = int.MinValue; + } + } + else + { + Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); + int inferredLayer = int.MinValue; + foreach (var e in node.Ins) + { + Visit(e); + if (inferredLayer < introducedLocalVarsUpperBound) + { + inferredLayer = introducedLocalVarsUpperBound; + } + introducedLocalVarsUpperBound = int.MinValue; + } + pureCallLayer[node] = inferredLayer; + } } - bool savedCanAccessSharedVars = canAccessSharedVars; - bool savedCanAccessAuxVars = canAccessGhostVars; - canAccessSharedVars = true; - canAccessGhostVars = true; - var retVal = base.VisitCallCmd(node); - canAccessSharedVars = savedCanAccessSharedVars; - canAccessGhostVars = savedCanAccessAuxVars; - return retVal; + else + { + if (enclosingProcLayerNum != atomicProcedureInfo.layerRange.upperLayerNum) + { + Error(node, "Creation layer of caller must be the upper bound of the layer range of callee"); + } + foreach (var ie in node.Proc.Modifies) + { + if (enclosingProcLayerNum != globalVarToSharedVarInfo[ie.Decl].introLayerNum) + { + Error(node, "Creation layer of caller must be identical to the introduction layer of modified variable"); + } + } + foreach (var ie in node.Outs) + { + if (localVarToLocalVariableInfo.ContainsKey(ie.Decl) && + enclosingProcLayerNum == localVarToLocalVariableInfo[ie.Decl].layer) + continue; + Error(node, "Output variable must be introduced at the creation layer of caller"); + } + } + return node; + } + else + { + Error(node, "A yielding procedure can call only atomic or yielding procedures"); + return node; } } @@ -618,8 +940,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 +967,36 @@ 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 (introducedLocalVarsUpperBound < localVariableInfo.layer) + { + introducedLocalVarsUpperBound = localVariableInfo.layer; + } + } 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 +1005,53 @@ namespace Microsoft.Boogie } else { + sharedVarsAccessed = new HashSet<Variable>(); + Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); + base.VisitEnsures(ensures); CheckAndAddLayers(ensures, ensures.Attributes, actionInfo.createdAtLayerNum); + if (introducedLocalVarsUpperBound > Least(FindLayers(ensures.Attributes))) + { + Error(ensures, "An introduced local variable is accessed but not available"); + } + 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); + base.VisitRequires(requires); CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].createdAtLayerNum); - return ret; + if (introducedLocalVarsUpperBound > Least(FindLayers(requires.Attributes))) + { + Error(requires, "An introduced local variable is accessed but not available"); + } + 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); + base.VisitAssertCmd(node); CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].createdAtLayerNum); - return ret; + if (introducedLocalVarsUpperBound > Least(FindLayers(node.Attributes))) + { + Error(node, "An introduced local variable is accessed but not available"); + } + introducedLocalVarsUpperBound = int.MinValue; + sharedVarsAccessed = null; + return node; } private List<int> RemoveDuplicatesAndSort(List<int> attrs) @@ -760,18 +1070,15 @@ 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)) - { - Error(node, "Illegal layer number"); - } - else if (layerNum > enclosingProcLayerNum) + if (layerNum > enclosingProcLayerNum) { 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 +1094,67 @@ namespace Microsoft.Boogie checkingContext.Error(node, message); errorCount++; } + + private class PurityChecker : StandardVisitor + { + private CivlTypeChecker civlTypeChecker; + + public PurityChecker(CivlTypeChecker civlTypeChecker) + { + this.civlTypeChecker = civlTypeChecker; + } + + public override Cmd VisitCallCmd(CallCmd node) + { + Procedure enclosingProc = civlTypeChecker.enclosingImpl.Proc; + if (!civlTypeChecker.procToAtomicProcedureInfo.ContainsKey(node.Proc)) + { + civlTypeChecker.Error(node, "Atomic procedure can only call an atomic procedure"); + return base.VisitCallCmd(node); + } + var callerInfo = civlTypeChecker.procToAtomicProcedureInfo[enclosingProc]; + var calleeInfo = civlTypeChecker.procToAtomicProcedureInfo[node.Proc]; + if (calleeInfo.isPure) + { + // do nothing + } + else if (callerInfo.isPure) + { + civlTypeChecker.Error(node, "Pure procedure can only call pure procedures"); + } + else if (!callerInfo.layerRange.Subset(calleeInfo.layerRange)) + { + civlTypeChecker.Error(node, "Caller layers must be subset of callee layers"); + } + return base.VisitCallCmd(node); + } + + public override Cmd VisitParCallCmd(ParCallCmd node) + { + civlTypeChecker.Error(node, "Atomic procedures cannot make parallel calls"); + return node; + } + + public override Expr VisitIdentifierExpr(IdentifierExpr node) + { + Procedure enclosingProc = civlTypeChecker.enclosingImpl.Proc; + if (node.Decl is GlobalVariable) + { + if (civlTypeChecker.procToAtomicProcedureInfo[enclosingProc].isPure) + { + civlTypeChecker.Error(node, "Pure procedure cannot access global variables"); + } + else if (!civlTypeChecker.globalVarToSharedVarInfo.ContainsKey(node.Decl)) + { + civlTypeChecker.Error(node, "Atomic procedure cannot access a global variable without layer numbers"); + } + else + { + civlTypeChecker.sharedVarsAccessed.Add(node.Decl); + } + } + return node; + } + } } -}
\ No newline at end of file +} diff --git a/Source/Concurrency/Concurrency.csproj b/Source/Concurrency/Concurrency.csproj index f15ebca3..113019fd 100644 --- a/Source/Concurrency/Concurrency.csproj +++ b/Source/Concurrency/Concurrency.csproj @@ -1,4 +1,4 @@ -<?xml version="1.0" encoding="utf-8"?> +<?xml version="1.0" encoding="utf-8"?> <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" /> <PropertyGroup> @@ -73,11 +73,11 @@ <ItemGroup> <Compile Include="LinearSets.cs" /> <Compile Include="MoverCheck.cs" /> - <Compile Include="OwickiGries.cs" /> + <Compile Include="CivlRefinement.cs" /> <Compile Include="Program.cs" /> <Compile Include="Properties\AssemblyInfo.cs" /> <Compile Include="SimulationRelation.cs" /> - <Compile Include="TypeCheck.cs" /> + <Compile Include="CivlTypeChecker.cs" /> <Compile Include="YieldTypeChecker.cs" /> </ItemGroup> <ItemGroup> @@ -112,4 +112,4 @@ <Target Name="AfterBuild"> </Target> --> -</Project>
\ No newline at end of file +</Project> diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs index 0fa04b1b..f654b688 100644 --- a/Source/Concurrency/LinearSets.cs +++ b/Source/Concurrency/LinearSets.cs @@ -626,10 +626,9 @@ namespace Microsoft.Boogie var domainName = FindDomainName(v); domainNameToScope[domainName].Add(v); } - foreach (Variable v in program.GlobalVariables) + foreach (Variable v in globalVarToDomainName.Keys) { var domainName = FindDomainName(v); - if (domainName == null) continue; domainNameToScope[domainName].Add(v); } foreach (string domainName in linearDomains.Keys) diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 7c6d4ac4..732bcaa4 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -10,29 +10,29 @@ namespace Microsoft.Boogie public class MoverCheck { LinearTypeChecker linearTypeChecker; - MoverTypeChecker moverTypeChecker; + CivlTypeChecker civlTypeChecker; List<Declaration> decls; HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> commutativityCheckerCache; HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> gatePreservationCheckerCache; HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> failurePreservationCheckerCache; - private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls) + private MoverCheck(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls) { this.linearTypeChecker = linearTypeChecker; - this.moverTypeChecker = moverTypeChecker; + this.civlTypeChecker = civlTypeChecker; this.decls = decls; this.commutativityCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>(); this.gatePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>(); this.failurePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>(); } - public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls) + public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls) { - if (moverTypeChecker.procToActionInfo.Count == 0) + if (civlTypeChecker.procToActionInfo.Count == 0) return; - List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); + List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(civlTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); sortedByCreatedLayerNum.Sort((x, y) => { return (x.createdAtLayerNum == y.createdAtLayerNum) ? 0 : (x.createdAtLayerNum < y.createdAtLayerNum) ? -1 : 1; }); - List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); + List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(civlTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); sortedByAvailableUptoLayerNum.Sort((x, y) => { return (x.availableUptoLayerNum == y.availableUptoLayerNum) ? 0 : (x.availableUptoLayerNum < y.availableUptoLayerNum) ? -1 : 1; }); Dictionary<int, HashSet<AtomicActionInfo>> pools = new Dictionary<int, HashSet<AtomicActionInfo>>(); @@ -60,8 +60,8 @@ namespace Microsoft.Boogie currPool = pools[currLayerNum]; } - Program program = moverTypeChecker.program; - MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls); + Program program = civlTypeChecker.program; + MoverCheck moverChecking = new MoverCheck(linearTypeChecker, civlTypeChecker, decls); foreach (int layerNum in pools.Keys) { foreach (AtomicActionInfo first in pools[layerNum]) @@ -537,7 +537,7 @@ namespace Microsoft.Boogie ensures.Add(ensureCheck); string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name); List<IdentifierExpr> globalVars = new List<IdentifierExpr>(); - moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, blocks); impl.Proc = proc; @@ -580,7 +580,7 @@ namespace Microsoft.Boogie requires.Add(new Requires(false, assertCmd.Expr)); string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name); List<IdentifierExpr> globalVars = new List<IdentifierExpr>(); - moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks); impl.Proc = proc; @@ -628,7 +628,7 @@ namespace Microsoft.Boogie requires.Add(new Requires(false, assertCmd.Expr)); string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name); List<IdentifierExpr> globalVars = new List<IdentifierExpr>(); - moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks); impl.Proc = proc; @@ -662,7 +662,7 @@ namespace Microsoft.Boogie blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken))); string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name); List<IdentifierExpr> globalVars = new List<IdentifierExpr>(); - moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks); impl.Proc = proc; diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs index b56e1cf3..1be7cc07 100644 --- a/Source/Concurrency/Program.cs +++ b/Source/Concurrency/Program.cs @@ -7,20 +7,20 @@ namespace Microsoft.Boogie { public class Concurrency { - public static void Transform(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker) + public static void Transform(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker) { List<Declaration> originalDecls = new List<Declaration>(); Program program = linearTypeChecker.program; foreach (var decl in program.TopLevelDeclarations) { Procedure proc = decl as Procedure; - if (proc != null && moverTypeChecker.procToActionInfo.ContainsKey(proc)) + if (proc != null && civlTypeChecker.procToActionInfo.ContainsKey(proc)) { originalDecls.Add(proc); continue; } Implementation impl = decl as Implementation; - if (impl != null && moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) + if (impl != null && civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) { originalDecls.Add(impl); } @@ -29,12 +29,12 @@ namespace Microsoft.Boogie List<Declaration> decls = new List<Declaration>(); if (!CommandLineOptions.Clo.TrustAtomicityTypes) { - MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls); + MoverCheck.AddCheckers(linearTypeChecker, civlTypeChecker, decls); } - OwickiGries.AddCheckers(linearTypeChecker, moverTypeChecker, decls); + CivlRefinement.AddCheckers(linearTypeChecker, civlTypeChecker, decls); foreach (Declaration decl in decls) { - decl.Attributes = OwickiGries.RemoveYieldsAttribute(decl.Attributes); + decl.Attributes = CivlRefinement.RemoveYieldsAttribute(decl.Attributes); } program.RemoveTopLevelDeclarations(x => originalDecls.Contains(x)); program.AddTopLevelDeclarations(decls); diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index a698c8fd..ed59d3ad 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -81,7 +81,7 @@ namespace Microsoft.Boogie Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation(); if (simulationRelation[initialState].Count == 0) { - moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum)); + civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum)); } } @@ -97,7 +97,7 @@ namespace Microsoft.Boogie Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation(); if (simulationRelation[initialState].Count == 0) { - moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum)); + civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum)); } } @@ -115,7 +115,7 @@ namespace Microsoft.Boogie Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation(); if (simulationRelation[initialState].Count == 0) { - moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum)); + civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum)); } } @@ -124,7 +124,7 @@ namespace Microsoft.Boogie foreach (Cmd cmd in block.Cmds) { AssertCmd assertCmd = cmd as AssertCmd; - if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && moverTypeChecker.absyToLayerNums[assertCmd].Contains(currLayerNum)) + if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && civlTypeChecker.absyToLayerNums[assertCmd].Contains(currLayerNum)) { return true; } @@ -132,25 +132,25 @@ namespace Microsoft.Boogie return false; } - public static void PerformYieldSafeCheck(MoverTypeChecker moverTypeChecker) + public static void PerformYieldSafeCheck(CivlTypeChecker civlTypeChecker) { - foreach (var impl in moverTypeChecker.program.Implementations) + foreach (var impl in civlTypeChecker.program.Implementations) { - if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue; + if (!civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue; impl.PruneUnreachableBlocks(); Graph<Block> implGraph = Program.GraphFromImpl(impl); implGraph.ComputeLoops(); - int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum; - foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum })) + int specLayerNum = civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum; + foreach (int layerNum in civlTypeChecker.AllLayerNums) { if (layerNum > specLayerNum) continue; - YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, layerNum, implGraph.Headers); + YieldTypeChecker executor = new YieldTypeChecker(civlTypeChecker, impl, layerNum, implGraph.Headers); } } } int stateCounter; - MoverTypeChecker moverTypeChecker; + CivlTypeChecker civlTypeChecker; Implementation impl; int currLayerNum; Dictionary<Absy, int> absyToNode; @@ -160,9 +160,9 @@ namespace Microsoft.Boogie Dictionary<Tuple<int, int>, int> edgeLabels; IEnumerable<Block> loopHeaders; - private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currLayerNum, IEnumerable<Block> loopHeaders) + private YieldTypeChecker(CivlTypeChecker civlTypeChecker, Implementation impl, int currLayerNum, IEnumerable<Block> loopHeaders) { - this.moverTypeChecker = moverTypeChecker; + this.civlTypeChecker = civlTypeChecker; this.impl = impl; this.currLayerNum = currLayerNum; this.loopHeaders = loopHeaders; @@ -226,20 +226,20 @@ namespace Microsoft.Boogie CallCmd callCmd = cmd as CallCmd; if (callCmd.IsAsync) { - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc]; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc]; if (currLayerNum <= actionInfo.createdAtLayerNum) edgeLabels[edge] = 'L'; else edgeLabels[edge] = 'B'; } - else if (!moverTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc)) + else if (!civlTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc)) { edgeLabels[edge] = 'P'; } else { MoverType moverType; - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc]; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc]; if (actionInfo.createdAtLayerNum >= currLayerNum) { moverType = MoverType.Top; @@ -280,7 +280,7 @@ namespace Microsoft.Boogie bool isLeftMover = true; foreach (CallCmd callCmd in parCallCmd.CallCmds) { - if (moverTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum) + if (civlTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum) { isYield = true; } @@ -294,7 +294,7 @@ namespace Microsoft.Boogie int numAtomicActions = 0; foreach (CallCmd callCmd in parCallCmd.CallCmds) { - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc]; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc]; isRightMover = isRightMover && actionInfo.IsRightMover; isLeftMover = isLeftMover && actionInfo.IsLeftMover; if (actionInfo is AtomicActionInfo) |