From 71fc5f5b32a5939ad488d6070a6acaf4d7cb443a Mon Sep 17 00:00:00 2001 From: qadeer Date: Fri, 26 Dec 2014 00:56:32 -0800 Subject: strengthened type checking cleaned up the generation of mover checks (based on example from Chris) added two examples from Chris to regressions --- Source/Concurrency/MoverCheck.cs | 67 ++++++++------- Source/Concurrency/OwickiGries.cs | 2 +- Source/Concurrency/TypeCheck.cs | 145 ++++++++++++++++++++++----------- Source/Concurrency/YieldTypeChecker.cs | 4 +- 4 files changed, 137 insertions(+), 81 deletions(-) (limited to 'Source/Concurrency') diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index b10cd6cd..971e7271 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -30,52 +30,57 @@ namespace Microsoft.Boogie if (moverTypeChecker.procToActionInfo.Count == 0) return; + List sortedByCreatedLayerNum = new List(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo)); + sortedByCreatedLayerNum.Sort((x, y) => { return (x.createdAtLayerNum == y.createdAtLayerNum) ? 0 : (x.createdAtLayerNum < y.createdAtLayerNum) ? -1 : 1; }); + List sortedByAvailableUptoLayerNum = new List(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo)); + sortedByAvailableUptoLayerNum.Sort((x, y) => { return (x.availableUptoLayerNum == y.availableUptoLayerNum) ? 0 : (x.availableUptoLayerNum < y.availableUptoLayerNum) ? -1 : 1; }); + Dictionary> pools = new Dictionary>(); - foreach (ActionInfo action in moverTypeChecker.procToActionInfo.Values) + int indexIntoSortedByCreatedLayerNum = 0; + int indexIntoSortedByAvailableUptoLayerNum = 0; + HashSet currPool = new HashSet(); + while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count) { - AtomicActionInfo atomicAction = action as AtomicActionInfo; - if (atomicAction == null) continue; - foreach (int layerNum in moverTypeChecker.AllLayerNums) + var currLayerNum = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum].createdAtLayerNum; + pools[currLayerNum] = new HashSet(currPool); + while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count) { - if (action.createdAtLayerNum < layerNum && layerNum <= action.availableUptoLayerNum) - { - if (!pools.ContainsKey(layerNum)) - { - pools[layerNum] = new HashSet(); - } - pools[layerNum].Add(atomicAction); - } + var actionInfo = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum] as AtomicActionInfo; + if (actionInfo.createdAtLayerNum > currLayerNum) break; + pools[currLayerNum].Add(actionInfo); + indexIntoSortedByCreatedLayerNum++; } + while (indexIntoSortedByAvailableUptoLayerNum < sortedByAvailableUptoLayerNum.Count) + { + var actionInfo = sortedByAvailableUptoLayerNum[indexIntoSortedByAvailableUptoLayerNum] as AtomicActionInfo; + if (actionInfo.availableUptoLayerNum > currLayerNum) break; + pools[currLayerNum].Remove(actionInfo); + indexIntoSortedByAvailableUptoLayerNum++; + } + currPool = pools[currLayerNum]; } Program program = moverTypeChecker.program; MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls); - foreach (int layerNum1 in pools.Keys) + foreach (int layerNum in pools.Keys) { - foreach (AtomicActionInfo first in pools[layerNum1]) + foreach (AtomicActionInfo first in pools[layerNum]) { Debug.Assert(first.moverType != MoverType.Top); if (first.moverType == MoverType.Atomic) continue; - foreach (int layerNum2 in pools.Keys) + foreach (AtomicActionInfo second in pools[layerNum]) { - if (layerNum2 < layerNum1) continue; - foreach (AtomicActionInfo second in pools[layerNum2]) + if (first.IsRightMover) + { + moverChecking.CreateCommutativityChecker(program, first, second); + moverChecking.CreateGatePreservationChecker(program, second, first); + } + if (first.IsLeftMover) { - if (second.createdAtLayerNum < layerNum1) - { - if (first.IsRightMover) - { - moverChecking.CreateCommutativityChecker(program, first, second); - moverChecking.CreateGatePreservationChecker(program, second, first); - } - if (first.IsLeftMover) - { - moverChecking.CreateCommutativityChecker(program, second, first); - moverChecking.CreateGatePreservationChecker(program, first, second); - moverChecking.CreateFailurePreservationChecker(program, second, first); - } - } + moverChecking.CreateCommutativityChecker(program, second, first); + moverChecking.CreateGatePreservationChecker(program, first, second); + moverChecking.CreateFailurePreservationChecker(program, second, first); } } } diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index 8865b69e..dbd1dcbd 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -1160,7 +1160,7 @@ namespace Microsoft.Boogie public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List decls) { Program program = linearTypeChecker.program; - foreach (int layerNum in moverTypeChecker.AllLayerNums.Except(new int[] { 0 })) + foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum })) { if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue; diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 8eb93e09..13356aff 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -22,12 +22,14 @@ namespace Microsoft.Boogie public Procedure proc; public int createdAtLayerNum; public int availableUptoLayerNum; + public bool hasImplementation; public ActionInfo(Procedure proc, int createdAtLayerNum, int availableUptoLayerNum) { this.proc = proc; this.createdAtLayerNum = createdAtLayerNum; this.availableUptoLayerNum = availableUptoLayerNum; + this.hasImplementation = false; } public virtual bool IsRightMover @@ -226,6 +228,7 @@ namespace Microsoft.Boogie int maxLayerNum; public Dictionary> absyToLayerNums; HashSet auxVars; + public int leastUnimplementedLayerNum; private static List FindLayers(QKeyValue kv) { @@ -260,20 +263,58 @@ namespace Microsoft.Boogie return MoverType.Top; } - private HashSet allLayerNums; - public IEnumerable AllLayerNums + public MoverTypeChecker(Program program) + { + this.auxVars = 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.canAccessAuxVars = false; + this.minLayerNum = int.MaxValue; + this.maxLayerNum = -1; + this.leastUnimplementedLayerNum = int.MaxValue; + foreach (var g in program.GlobalVariables) + { + List layerNums = FindLayers(g.Attributes); + if (layerNums.Count == 0) + { + // Cannot access atomic actions + } + else if (layerNums.Count == 1) + { + this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], int.MaxValue); + } + else if (layerNums.Count == 2) + { + this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], layerNums[1]); + } + else + { + Error(g, "Too many layer numbers"); + } + } + } + + private HashSet allCreatedLayerNums; + public IEnumerable AllCreatedLayerNums { get { - if (allLayerNums == null) + if (allCreatedLayerNums == null) { - allLayerNums = new HashSet(); + allCreatedLayerNums = new HashSet(); foreach (ActionInfo actionInfo in procToActionInfo.Values) { - allLayerNums.Add(actionInfo.createdAtLayerNum); + allCreatedLayerNums.Add(actionInfo.createdAtLayerNum); } } - return allLayerNums; + return allCreatedLayerNums; } } @@ -300,6 +341,11 @@ namespace Microsoft.Boogie Error(proc, "Incorrect number of layers"); continue; } + if (availableUptoLayerNum <= createdAtLayerNum) + { + Error(proc, "Creation layer number must be less than the available upto layer number"); + continue; + } foreach (Ensures e in proc.Ensures) { MoverType moverType = GetMoverType(e); @@ -323,68 +369,69 @@ namespace Microsoft.Boogie enclosingImpl = null; base.VisitEnsures(e); canAccessSharedVars = false; - if (maxLayerNum <= createdAtLayerNum && availableUptoLayerNum <= minLayerNum) + if (maxLayerNum > createdAtLayerNum) { - // ok + Error(e, "A variable being accessed is introduced after this action is created"); } - else + else if (availableUptoLayerNum > minLayerNum) { Error(e, "A variable being accessed is hidden before this action becomes unavailable"); } - - procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum); + else + { + procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum); + } } + if (errorCount > 0) continue; if (!procToActionInfo.ContainsKey(proc)) { procToActionInfo[proc] = new ActionInfo(proc, createdAtLayerNum, availableUptoLayerNum); } } if (errorCount > 0) return; - this.VisitProgram(program); - if (errorCount > 0) return; - YieldTypeChecker.PerformYieldSafeCheck(this); - } - - public IEnumerable SharedVariables - { - get { return this.globalVarToSharedVarInfo.Keys; } - } - - public MoverTypeChecker(Program program) - { - this.auxVars = 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.canAccessAuxVars = false; - this.minLayerNum = int.MaxValue; - this.maxLayerNum = -1; - foreach (var g in program.GlobalVariables) + foreach (var impl in program.Implementations) { - List layerNums = FindLayers(g.Attributes); - if (layerNums.Count == 0) + if (!procToActionInfo.ContainsKey(impl.Proc)) continue; + procToActionInfo[impl.Proc].hasImplementation = true; + } + foreach (var proc in procToActionInfo.Keys) + { + ActionInfo actionInfo = procToActionInfo[proc]; + if (actionInfo.hasImplementation) continue; + if (leastUnimplementedLayerNum == int.MaxValue) { - // Cannot access atomic actions + leastUnimplementedLayerNum = actionInfo.createdAtLayerNum; } - else if (layerNums.Count == 1) + else if (leastUnimplementedLayerNum == actionInfo.createdAtLayerNum) { - this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], int.MaxValue); + // do nothing } - else if (layerNums.Count == 2) + else { - this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], layerNums[1]); + Error(proc, "All unimplemented atomic actions must be created at the same layer"); } - else + } + foreach (var g in this.globalVarToSharedVarInfo.Keys) + { + var info = globalVarToSharedVarInfo[g]; + if (!this.AllCreatedLayerNums.Contains(info.introLayerNum)) { - Error(g, "Too many layer numbers"); + Error(g, "Variable must be introduced with creation of some atomic action"); + } + if (info.hideLayerNum != int.MaxValue && !this.AllCreatedLayerNums.Contains(info.hideLayerNum)) + { + Error(g, "Variable must be hidden with creation of some atomic action"); } } + if (errorCount > 0) return; + this.VisitProgram(program); + if (errorCount > 0) return; + YieldTypeChecker.PerformYieldSafeCheck(this); + } + + public IEnumerable SharedVariables + { + get { return this.globalVarToSharedVarInfo.Keys; } } public override Implementation VisitImplementation(Implementation node) @@ -602,7 +649,11 @@ namespace Microsoft.Boogie absyToLayerNums[node] = new HashSet(); foreach (int layerNum in attrs) { - if (layerNum > enclosingProcLayerNum) + if (layerNum == leastUnimplementedLayerNum || !AllCreatedLayerNums.Contains(layerNum)) + { + Error(node, "Illegal layer number"); + } + else if (layerNum > enclosingProcLayerNum) { Error(node, "The layer cannot be greater than the layer of enclosing procedure"); } diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index 8e844ede..95884626 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -136,12 +136,12 @@ namespace Microsoft.Boogie { foreach (var impl in moverTypeChecker.program.Implementations) { - if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum == 0) continue; + if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue; impl.PruneUnreachableBlocks(); Graph implGraph = Program.GraphFromImpl(impl); implGraph.ComputeLoops(); int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum; - foreach (int layerNum in moverTypeChecker.AllLayerNums) + foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum })) { if (layerNum > specLayerNum) continue; YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, layerNum, implGraph.Headers); -- cgit v1.2.3