From 28d4e2ad2598ff377f121ff2a2a9b0794f386110 Mon Sep 17 00:00:00 2001 From: qadeer Date: Sun, 4 May 2014 21:17:12 -0700 Subject: second checkpoint --- Source/Concurrency/OwickiGries.cs | 270 +++++++++++++++++++++----------------- 1 file changed, 153 insertions(+), 117 deletions(-) (limited to 'Source/Concurrency/OwickiGries.cs') diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index 5170383f..5414723e 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -7,6 +7,7 @@ using System.Threading.Tasks; using Microsoft.Boogie; using System.Diagnostics; using System.Diagnostics.Contracts; +using Microsoft.Boogie.GraphUtil; namespace Microsoft.Boogie { @@ -15,26 +16,31 @@ namespace Microsoft.Boogie MoverTypeChecker moverTypeChecker; public int phaseNum; Procedure enclosingProc; + Implementation enclosingImpl; public Dictionary procMap; /* Original -> Duplicate */ public Dictionary absyMap; /* Duplicate -> Original */ public Dictionary blockMap; /* Original -> Duplicate */ public Dictionary implMap; /* Duplicate -> Original */ public HashSet yieldingProcs; + public List impls; + public MyDuplicator(MoverTypeChecker moverTypeChecker, int phaseNum) { this.moverTypeChecker = moverTypeChecker; this.phaseNum = phaseNum; this.enclosingProc = null; + this.enclosingImpl = null; this.procMap = new Dictionary(); this.absyMap = new Dictionary(); this.blockMap = new Dictionary(); this.implMap = new Dictionary(); this.yieldingProcs = new HashSet(); + this.impls = new List(); } private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List newCmds) { - int enclosingProcPhaseNum = moverTypeChecker.procToActionInfo[enclosingProc].phaseNum; + int enclosingProcPhaseNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].phaseNum; Procedure originalProc = originalCallCmd.Proc; if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc)) { @@ -145,17 +151,47 @@ namespace Microsoft.Boogie return node; if (!procMap.ContainsKey(node)) { - Procedure savedEnclosingProc = enclosingProc; enclosingProc = node; Procedure proc = (Procedure)node.Clone(); proc.Name = string.Format("{0}_{1}", node.Name, phaseNum); proc.InParams = this.VisitVariableSeq(node.InParams); proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies); proc.OutParams = this.VisitVariableSeq(node.OutParams); - if (moverTypeChecker.procToActionInfo[node].phaseNum < phaseNum) + + ActionInfo actionInfo = moverTypeChecker.procToActionInfo[node]; + if (actionInfo.phaseNum < phaseNum) { proc.Requires = new List(); proc.Ensures = new List(); + Implementation impl; + AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; + if (atomicActionInfo != null) + { + CodeExpr action = (CodeExpr)VisitCodeExpr(atomicActionInfo.thisAction); + List cmds = new List(); + foreach (AssertCmd assertCmd in atomicActionInfo.thisGate) + { + cmds.Add(new AssumeCmd(Token.NoToken, (Expr)Visit(assertCmd.Expr))); + } + Block newInitBlock = new Block(Token.NoToken, "_init", cmds, + new GotoCmd(Token.NoToken, new List(new string[] { action.Blocks[0].Label }), + new List(new Block[] { action.Blocks[0] }))); + List newBlocks = new List(); + newBlocks.Add(newInitBlock); + newBlocks.AddRange(action.Blocks); + impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, action.LocVars, newBlocks); + } + else + { + Block newInitBlock = new Block(Token.NoToken, "_init", new List(), new ReturnCmd(Token.NoToken)); + List newBlocks = new List(); + newBlocks.Add(newInitBlock); + impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, new List(), newBlocks); + } + impl.Proc = proc; + impl.Proc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + impl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + impls.Add(impl); } else { @@ -164,7 +200,6 @@ namespace Microsoft.Boogie proc.Ensures = this.VisitEnsuresSeq(node.Ensures); } procMap[node] = proc; - enclosingProc = savedEnclosingProc; proc.Modifies = new List(); moverTypeChecker.program.GlobalVariables().Iter(x => proc.Modifies.Add(Expr.Ident(x))); } @@ -174,7 +209,7 @@ namespace Microsoft.Boogie private Variable dummyLocalVar; public override Implementation VisitImplementation(Implementation node) { - enclosingProc = node.Proc; + enclosingImpl = node; dummyLocalVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_dummy", Type.Bool)); Implementation impl = base.VisitImplementation(node); implMap[impl] = node; @@ -246,6 +281,12 @@ namespace Microsoft.Boogie List yieldCheckerImpls; Procedure yieldProc; + Variable pc; + Variable ok; + Expr alpha; + Expr beta; + HashSet frame; + public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator) { this.linearTypeChecker = linearTypeChecker; @@ -381,12 +422,6 @@ namespace Microsoft.Boogie } } - Variable pc; - Variable ok; - Expr alpha; - Expr beta; - HashSet frame; - private Expr OldEqualityExpr(Dictionary ogOldGlobalMap) { Expr bb = Expr.True; @@ -600,7 +635,7 @@ namespace Microsoft.Boogie yieldCheckerImpls.Add(yieldCheckerImpl); } - private bool IsYieldingHeader(GraphUtil.Graph graph, Block header) + private bool IsYieldingHeader(Graph graph, Block header) { foreach (Block backEdgeNode in graph.BackEdgeNodes(header)) { @@ -622,28 +657,18 @@ namespace Microsoft.Boogie return false; } - private bool IsYieldingCallCmd(CallCmd callCmd) + private Graph ComputeYieldingLoopHeaders(Implementation impl, out HashSet yieldingHeaders) { - return true; - } - - private void TransformImpl(Implementation impl) - { - pc = null; - alpha = null; - beta = null; - frame = null; - - // Find the yielding loop headers + Graph graph; impl.PruneUnreachableBlocks(); impl.ComputePredecessorsForBlocks(); - GraphUtil.Graph graph = Program.GraphFromImpl(impl); + graph = Program.GraphFromImpl(impl); graph.ComputeLoops(); if (!graph.Reducible) { throw new Exception("Irreducible flow graphs are unsupported."); } - HashSet yieldingHeaders = new HashSet(); + yieldingHeaders = new HashSet(); IEnumerable sortedHeaders = graph.SortHeadersByDominance(); foreach (Block header in sortedHeaders) { @@ -660,15 +685,27 @@ namespace Microsoft.Boogie continue; } } + return graph; + } + + private void SetupRefinementCheck(Implementation impl, + out Dictionary map, + out Dictionary domainNameToInputVar, out Dictionary domainNameToLocalVar, out Dictionary ogOldGlobalMap) + { + pc = null; + ok = null; + alpha = null; + beta = null; + frame = null; Program program = linearTypeChecker.program; - Dictionary map = new Dictionary(); + map = new Dictionary(); foreach (Variable local in impl.LocVars) { var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type)); map[local] = Expr.Ident(copy); } - Dictionary ogOldGlobalMap = new Dictionary(); + ogOldGlobalMap = new Dictionary(); foreach (IdentifierExpr ie in globalMods) { Variable g = ie.Decl; @@ -744,8 +781,8 @@ namespace Microsoft.Boogie } } - Dictionary domainNameToInputVar = new Dictionary(); - Dictionary domainNameToLocalVar = new Dictionary(); + domainNameToInputVar = new Dictionary(); + domainNameToLocalVar = new Dictionary(); { int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count; foreach (string domainName in linearTypeChecker.linearDomains.Keys) @@ -758,7 +795,31 @@ namespace Microsoft.Boogie i++; } } + } + + private void TransformImpl(Implementation impl) + { + HashSet yieldingHeaders; + Graph graph = ComputeYieldingLoopHeaders(impl, out yieldingHeaders); + + Dictionary map; + Dictionary domainNameToInputVar, domainNameToLocalVar; + Dictionary ogOldGlobalMap; + SetupRefinementCheck(impl, out map, out domainNameToInputVar, out domainNameToLocalVar, out ogOldGlobalMap); + List> yields = CollectAndDesugarYields(impl, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap); + + List oldPcs, oldOks; + ProcessLoopHeaders(impl, graph, yieldingHeaders, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap, out oldPcs, out oldOks); + + AddInitialBlock(impl, oldPcs, oldOks, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap); + + CreateYieldCheckerImpl(impl, yields, map); + } + + private List> CollectAndDesugarYields(Implementation impl, + Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap) + { // Collect the yield predicates and desugar yields List> yields = new List>(); List cmds = new List(); @@ -792,7 +853,7 @@ namespace Microsoft.Boogie cmds.Add(pcmd); } } - + if (cmd is CallCmd) { CallCmd callCmd = cmd as CallCmd; @@ -864,9 +925,15 @@ namespace Microsoft.Boogie } b.Cmds = newCmds; } + return yields; + } - List oldPcs = new List(); - List oldOks = new List(); + private void ProcessLoopHeaders(Implementation impl, Graph graph, HashSet yieldingHeaders, + Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap, + out List oldPcs, out List oldOks) + { + oldPcs = new List(); + oldOks = new List(); foreach (Block header in yieldingHeaders) { LocalVariable oldPc = null; @@ -914,62 +981,62 @@ namespace Microsoft.Boogie newCmds.AddRange(header.Cmds); header.Cmds = newCmds; } + } + private void AddInitialBlock(Implementation impl, List oldPcs, List oldOks, + Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap) + { + // Add initial block + List lhss = new List(); + List rhss = new List(); + if (pc != null) { - // Add initial block - List lhss = new List(); - List rhss = new List(); - if (pc != null) + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc))); + rhss.Add(Expr.False); + foreach (Variable oldPc in oldPcs) { - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc))); + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc))); rhss.Add(Expr.False); - foreach (Variable oldPc in oldPcs) - { - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc))); - rhss.Add(Expr.False); - } - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok))); - rhss.Add(Expr.False); - foreach (Variable oldOk in oldOks) - { - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk))); - rhss.Add(Expr.False); - } - } - Dictionary domainNameToExpr = new Dictionary(); - foreach (var domainName in linearTypeChecker.linearDomains.Keys) - { - domainNameToExpr[domainName] = Expr.Ident(domainNameToInputVar[domainName]); } - for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++) + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok))); + rhss.Add(Expr.False); + foreach (Variable oldOk in oldOks) { - Variable v = impl.InParams[i]; - var domainName = linearTypeChecker.FindDomainName(v); - if (domainName == null) continue; - if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue; - var domain = linearTypeChecker.linearDomains[domainName]; - if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue; - Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List { Expr.Ident(v) }); - domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { ie, domainNameToExpr[domainName] }); - } - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName]))); - rhss.Add(domainNameToExpr[domainName]); - } - foreach (Variable g in ogOldGlobalMap.Keys) - { - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g]))); - rhss.Add(Expr.Ident(g)); - } - if (lhss.Count > 0) - { - Block initBlock = new Block(Token.NoToken, "og_init", new List { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] })); - impl.Blocks.Insert(0, initBlock); + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk))); + rhss.Add(Expr.False); } } - - CreateYieldCheckerImpl(impl, yields, map); + Dictionary domainNameToExpr = new Dictionary(); + foreach (var domainName in linearTypeChecker.linearDomains.Keys) + { + domainNameToExpr[domainName] = Expr.Ident(domainNameToInputVar[domainName]); + } + for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++) + { + Variable v = impl.InParams[i]; + var domainName = linearTypeChecker.FindDomainName(v); + if (domainName == null) continue; + if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue; + var domain = linearTypeChecker.linearDomains[domainName]; + if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue; + Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List { Expr.Ident(v) }); + domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { ie, domainNameToExpr[domainName] }); + } + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName]))); + rhss.Add(domainNameToExpr[domainName]); + } + foreach (Variable g in ogOldGlobalMap.Keys) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g]))); + rhss.Add(Expr.Ident(g)); + } + if (lhss.Count > 0) + { + Block initBlock = new Block(Token.NoToken, "og_init", new List { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] })); + impl.Blocks.Insert(0, initBlock); + } } private void AddYieldProcAndImpl(List decls) @@ -1039,8 +1106,9 @@ namespace Microsoft.Boogie return iter; } - private void Collect(List decls) + private List Collect() { + List decls = new List(); foreach (Procedure proc in yieldCheckerProcs) { decls.Add(proc); @@ -1054,6 +1122,7 @@ namespace Microsoft.Boogie decls.Add(proc); } AddYieldProcAndImpl(decls); + return decls; } public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List decls) @@ -1070,41 +1139,8 @@ namespace Microsoft.Boogie if (proc == null || !moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue; Procedure duplicateProc = duplicator.VisitProcedure(proc); decls.Add(duplicateProc); - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[proc]; - if (actionInfo.phaseNum < phaseNum) - { - Implementation impl; - AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; - if (atomicActionInfo != null) - { - CodeExpr action = (CodeExpr)duplicator.VisitCodeExpr(atomicActionInfo.thisAction); - - List cmds = new List(); - foreach (AssertCmd assertCmd in atomicActionInfo.thisGate) - { - cmds.Add(new AssumeCmd(Token.NoToken, (Expr)duplicator.Visit(assertCmd.Expr))); - } - Block newInitBlock = new Block(Token.NoToken, "_init", cmds, - new GotoCmd(Token.NoToken, new List(new string[] { action.Blocks[0].Label }), - new List(new Block[] { action.Blocks[0] }))); - List newBlocks = new List(); - newBlocks.Add(newInitBlock); - newBlocks.AddRange(action.Blocks); - impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, action.LocVars, newBlocks); - } - else - { - Block newInitBlock = new Block(Token.NoToken, "_init", new List(), new ReturnCmd(Token.NoToken)); - List newBlocks = new List(); - newBlocks.Add(newInitBlock); - impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, new List(), newBlocks); - } - impl.Proc = duplicateProc; - impl.Proc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); - impl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); - decls.Add(impl); - } } + decls.AddRange(duplicator.impls); OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator); foreach (var decl in program.TopLevelDeclarations) { @@ -1115,7 +1151,7 @@ namespace Microsoft.Boogie ogTransform.TransformImpl(duplicateImpl); decls.Add(duplicateImpl); } - ogTransform.Collect(decls); + decls.AddRange(ogTransform.Collect()); } } } -- cgit v1.2.3