From 0f5809abee55aa22f2b496c826ea5b8f1a222e7d Mon Sep 17 00:00:00 2001 From: allydonaldson Date: Thu, 18 Jul 2013 17:27:41 +0100 Subject: Revamp of staged Houdini, and completion of parallel support. --- Source/Core/CommandLineOptions.cs | 6 + Source/ExecutionEngine/ExecutionEngine.cs | 84 +++++-- Source/Houdini/CandidateDependenceAnalyser.cs | 123 +++------ Source/Houdini/Checker.cs | 4 + Source/Houdini/Houdini.cs | 108 ++++---- Source/Houdini/Houdini.csproj | 3 +- Source/Houdini/StagedHoudini.cs | 348 ++++++++++++++++++++++++++ Source/Provers/SMTLib/SMTLibProcess.cs | 1 + 8 files changed, 505 insertions(+), 172 deletions(-) create mode 100644 Source/Houdini/StagedHoudini.cs diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 51034bf3..d09678dc 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -401,6 +401,7 @@ namespace Microsoft.Boogie { public bool DebugStagedHoudini = false; public bool StagedHoudiniReachabilityAnalysis = false; public bool StagedHoudiniMergeIgnoredCandidates = false; + public int StagedHoudiniThreads = 2; public string VariableDependenceIgnore = null; public string AbstractHoudini = null; public bool UseUnsatCoreForContractInfer = false; @@ -901,6 +902,11 @@ namespace Microsoft.Boogie { return true; } + case "stagedHoudiniThreads": { + ps.GetNumericArgument(ref StagedHoudiniThreads); + return true; + } + case "stagedHoudiniReachabilityAnalysis": { if (ps.ConfirmArgumentCount(0)) { StagedHoudiniReachabilityAnalysis = true; diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 79043832..e988c638 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -709,24 +709,6 @@ namespace Microsoft.Boogie } RequestIdToCancellationTokenSources[requestId] = new List(); - #region Compute information required to run staged Houdini - StagedHoudiniPlan stagedHoudiniPlan = null; - if (CommandLineOptions.Clo.StagedHoudini != null) - { - var candidateDependenceAnalyser = new CandidateDependenceAnalyser(program); - candidateDependenceAnalyser.Analyse(); - stagedHoudiniPlan = candidateDependenceAnalyser.ApplyStages(); - if (CommandLineOptions.Clo.Trace) - { - candidateDependenceAnalyser.dump(); - int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured; - CommandLineOptions.Clo.PrintUnstructured = 2; - PrintBplFile("staged.bpl", program, false, false); - CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured; - } - } - #endregion - #region Infer invariants using Abstract Interpretation // Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch) @@ -1109,9 +1091,68 @@ namespace Microsoft.Boogie { return RunAbstractHoudini(program, stats, er); } + + if (CommandLineOptions.Clo.StagedHoudini != null) + { + return RunStagedHoudini(program, stats, er); + } + Houdini.HoudiniSession.HoudiniStatistics houdiniStats = new Houdini.HoudiniSession.HoudiniStatistics(); Houdini.Houdini houdini = new Houdini.Houdini(program, houdiniStats); Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference(); + houdini.Close(); + + if (CommandLineOptions.Clo.PrintAssignment) + { + Console.WriteLine("Assignment computed by Houdini:"); + foreach (var x in outcome.assignment) + { + Console.WriteLine(x.Key + " = " + x.Value); + } + } + + if (CommandLineOptions.Clo.Trace) + { + int numTrueAssigns = 0; + foreach (var x in outcome.assignment) + { + if (x.Value) + numTrueAssigns++; + } + Console.WriteLine("Number of true assignments = " + numTrueAssigns); + Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns)); + Console.WriteLine("Prover time = " + houdiniStats.proverTime.ToString("F2")); + Console.WriteLine("Unsat core prover time = " + houdiniStats.unsatCoreProverTime.ToString("F2")); + Console.WriteLine("Number of prover queries = " + houdiniStats.numProverQueries); + Console.WriteLine("Number of unsat core prover queries = " + houdiniStats.numUnsatCoreProverQueries); + Console.WriteLine("Number of unsat core prunings = " + houdiniStats.numUnsatCorePrunings); + } + + foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values) + { + ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er); + ProcessErrors(x.errors, x.outcome, Console.Out, er); + } + + return PipelineOutcome.Done; + } + + private static Program ProgramFromFile(string filename) { + Program p = ParseBoogieProgram(new List { filename }, false); + System.Diagnostics.Debug.Assert(p != null); + LinearTypechecker linearTypechecker; + PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypechecker); + System.Diagnostics.Debug.Assert(oc == PipelineOutcome.ResolvedAndTypeChecked); + return p; + } + + private static PipelineOutcome RunStagedHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er) + { + Houdini.HoudiniSession.HoudiniStatistics houdiniStats = new Houdini.HoudiniSession.HoudiniStatistics(); + // TODO - pass this in somewhere + + Houdini.StagedHoudini houdini = new Houdini.StagedHoudini(program, ProgramFromFile); + Houdini.HoudiniOutcome outcome = houdini.PerformStagedHoudiniInference(); if (CommandLineOptions.Clo.PrintAssignment) { @@ -1144,12 +1185,9 @@ namespace Microsoft.Boogie ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er); ProcessErrors(x.errors, x.outcome, Console.Out, er); } - //errorCount = outcome.ErrorCount; - //verified = outcome.Verified; - //inconclusives = outcome.Inconclusives; - //timeOuts = outcome.TimeOuts; - //outOfMemories = 0; + return PipelineOutcome.Done; + } diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs index 05b66e1b..9a2eb404 100644 --- a/Source/Houdini/CandidateDependenceAnalyser.cs +++ b/Source/Houdini/CandidateDependenceAnalyser.cs @@ -6,7 +6,7 @@ using Microsoft.Boogie.GraphUtil; using Microsoft.Basetypes; using System.Diagnostics; -namespace Microsoft.Boogie { +namespace Microsoft.Boogie.Houdini { public class CandidateDependenceAnalyser { @@ -194,7 +194,7 @@ namespace Microsoft.Boogie { if (p != null) { string c; - if(Houdini.Houdini.MatchCandidate(p.Expr, candidates, out c)) { + if(Houdini.MatchCandidate(p.Expr, candidates, out c)) { yield return new CandidateInstance(c, impl.Name, p.Expr); } } @@ -207,14 +207,14 @@ namespace Microsoft.Boogie { foreach (Requires r in proc.Requires) { string c; - if(Houdini.Houdini.MatchCandidate(r.Condition, candidates, out c)) { + if(Houdini.MatchCandidate(r.Condition, candidates, out c)) { yield return new CandidateInstance(c, proc.Name, r.Condition); } } foreach (Ensures e in proc.Ensures) { string c; - if(Houdini.Houdini.MatchCandidate(e.Condition, candidates, out c)) { + if(Houdini.MatchCandidate(e.Condition, candidates, out c)) { yield return new CandidateInstance(c, proc.Name, e.Condition); } } @@ -393,14 +393,14 @@ namespace Microsoft.Boogie { foreach (var stage in Plan) { var stageActive = new Constant(Token.NoToken, - new TypedIdent(Token.NoToken, "_stage_" + stage + "_active", Type.Bool), + new TypedIdent(Token.NoToken, "_stage_" + stage.GetId() + "_active", Type.Bool), false); stageActive.AddAttribute("stage_active", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(stage.GetId())) }); prog.TopLevelDeclarations.Add(stageActive); stageToActiveBoolean[stage.GetId()] = stageActive; var stageComplete = new Constant(Token.NoToken, - new TypedIdent(Token.NoToken, "_stage_" + stage + "_complete", Type.Bool), + new TypedIdent(Token.NoToken, "_stage_" + stage.GetId() + "_complete", Type.Bool), false); stageComplete.AddAttribute("stage_complete", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(stage.GetId())) }); prog.TopLevelDeclarations.Add(stageComplete); @@ -416,11 +416,11 @@ namespace Microsoft.Boogie { { var a = cmd as AssertCmd; string c; - if (a != null && (Houdini.Houdini.MatchCandidate(a.Expr, candidates, out c))) + if (a != null && (Houdini.MatchCandidate(a.Expr, candidates, out c))) { - newCmds.Add(new AssertCmd(a.tok, Houdini.Houdini.AddConditionToCandidate(a.Expr, + newCmds.Add(new AssertCmd(a.tok, Houdini.AddConditionToCandidate(a.Expr, new IdentifierExpr(Token.NoToken, stageToActiveBoolean[Plan.StageForCandidate(c).GetId()]), c), a.Attributes)); - newCmds.Add(new AssumeCmd(a.tok, Houdini.Houdini.AddConditionToCandidate(a.Expr, + newCmds.Add(new AssumeCmd(a.tok, Houdini.AddConditionToCandidate(a.Expr, new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[Plan.StageForCandidate(c).GetId()]), c), a.Attributes)); } else @@ -440,13 +440,13 @@ namespace Microsoft.Boogie { RequiresSeq newRequires = new RequiresSeq(); foreach(Requires r in p.Requires) { string c; - if (Houdini.Houdini.MatchCandidate(r.Condition, candidates, out c)) { + if (Houdini.MatchCandidate(r.Condition, candidates, out c)) { newRequires.Add(new Requires(r.tok, false, - Houdini.Houdini.AddConditionToCandidate(r.Condition, + Houdini.AddConditionToCandidate(r.Condition, new IdentifierExpr(Token.NoToken, stageToActiveBoolean[Plan.StageForCandidate(c).GetId()]), c), r.Comment, r.Attributes)); newRequires.Add(new Requires(r.tok, true, - Houdini.Houdini.AddConditionToCandidate(r.Condition, + Houdini.AddConditionToCandidate(r.Condition, new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[Plan.StageForCandidate(c).GetId()]), c), r.Comment, r.Attributes)); } else { @@ -460,15 +460,15 @@ namespace Microsoft.Boogie { EnsuresSeq newEnsures = new EnsuresSeq(); foreach(Ensures e in p.Ensures) { string c; - if (Houdini.Houdini.MatchCandidate(e.Condition, candidates, out c)) { + if (Houdini.MatchCandidate(e.Condition, candidates, out c)) { int stage = Plan.StageForCandidate(c).GetId(); Constant activeBoolean = stageToActiveBoolean[stage]; newEnsures.Add(new Ensures(e.tok, false, - Houdini.Houdini.AddConditionToCandidate(e.Condition, + Houdini.AddConditionToCandidate(e.Condition, new IdentifierExpr(Token.NoToken, activeBoolean), c), e.Comment, e.Attributes)); newEnsures.Add(new Ensures(e.tok, true, - Houdini.Houdini.AddConditionToCandidate(e.Condition, + Houdini.AddConditionToCandidate(e.Condition, new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[stage]), c), e.Comment, e.Attributes)); } else { @@ -492,6 +492,10 @@ namespace Microsoft.Boogie { private StagedHoudiniPlan ComputeCoarseStages() { + foreach(var n in StagesDAG.Nodes) { + Debug.Assert(!StagesDAG.Successors(n).Contains(n)); + } + Graph Dependences = new Graph(); var done = new Dictionary, ScheduledStage>(); @@ -500,20 +504,30 @@ namespace Microsoft.Boogie { for(int stageId = 1; done.Count() != StagesDAG.Nodes.Count(); stageId++) { var Stage = new ScheduledStage(stageId, new HashSet()); + HashSet> AssignedToThisStage = new HashSet>(); foreach (var n in StagesDAG.Nodes.Where(Item => !done.ContainsKey(Item))) { if(StagesDAG.Successors(n).Where(Item => !done.ContainsKey(Item)).Count() == 0) { foreach(var s in StagesDAG.Successors(n)) { + Debug.Assert(s != n); + Debug.Assert(Stage != done[s]); Dependences.AddEdge(Stage, done[s]); } foreach (var c in n) { Stage.AddCandidate(c); } - done[n] = Stage; + Console.Write(n.Count() + ", "); + AssignedToThisStage.Add(n); } } + + Console.WriteLine("total: " + Stage.Count()); + + foreach(var n in AssignedToThisStage) { + done[n] = Stage; + } } return new StagedHoudiniPlan(Dependences); } @@ -530,6 +544,8 @@ namespace Microsoft.Boogie { { int stageSize = 0; ScheduledStage Stage = new ScheduledStage(stageId, new HashSet()); + HashSet> AddedToThisStage = new HashSet>(); + foreach (var n in StagesDAG.Nodes.Where(Item => !done.ContainsKey(Item))) { if(stageSize + n.Count() > maxStageSize) { @@ -544,9 +560,12 @@ namespace Microsoft.Boogie { foreach(var s in StagesDAG.Successors(n)) { Dependences.AddEdge(Stage, done[s]); } - done[n] = Stage; + AddedToThisStage.Add(n); } } + foreach(var n in AddedToThisStage) { + done[n] = Stage; + } if(stageSize == 0) { maxStageSize *= 2; } @@ -622,7 +641,7 @@ namespace Microsoft.Boogie { AssertCmd assertCmd = cmd as AssertCmd; if(assertCmd != null) { string c; - if(Houdini.Houdini.MatchCandidate(assertCmd.Expr, candidates, out c)) { + if(Houdini.MatchCandidate(assertCmd.Expr, candidates, out c)) { AddCandidateOccurrence(c, b); } } @@ -633,7 +652,7 @@ namespace Microsoft.Boogie { foreach(var proc in prog.TopLevelDeclarations.OfType()) { foreach(Requires r in proc.Requires) { string c; - if(Houdini.Houdini.MatchCandidate(r.Condition, candidates, out c)) { + if(Houdini.MatchCandidate(r.Condition, candidates, out c)) { AddCandidateOccurrence(c, new Tuple(proc.Name, PrePost.PRE)); } } @@ -643,7 +662,7 @@ namespace Microsoft.Boogie { foreach(var proc in prog.TopLevelDeclarations.OfType()) { foreach(Ensures e in proc.Ensures) { string c; - if(Houdini.Houdini.MatchCandidate(e.Condition, candidates, out c)) { + if(Houdini.MatchCandidate(e.Condition, candidates, out c)) { AddCandidateOccurrence(c, new Tuple(proc.Name, PrePost.POST)); } } @@ -712,68 +731,4 @@ namespace Microsoft.Boogie { } } - public class StagedHoudiniPlan : IEnumerable { - - private Graph ScheduledStages; - private Dictionary CandidateToStage; - - internal StagedHoudiniPlan(Graph ScheduledStages) { - this.ScheduledStages = ScheduledStages; - this.CandidateToStage = new Dictionary(); - } - - public IEnumerable GetDependences(ScheduledStage s) { - return ScheduledStages.Successors(s); - } - - public IEnumerator GetEnumerator() { - var sort = ScheduledStages.TopologicalSort().ToList(); - sort.Reverse(); - foreach(var s in sort) { - yield return s; - } - } - - System.Collections.IEnumerator System.Collections.IEnumerable.GetEnumerator() - { - return this.GetEnumerator(); - } - - internal ScheduledStage StageForCandidate(string c) { - if(CandidateToStage.ContainsKey(c)) { - return CandidateToStage[c]; - } - foreach(var s in ScheduledStages.Nodes) { - if(s.ContainsCandidate(c)) { - CandidateToStage[c] = s; - return s; - } - } - return null; - } - - } - - public class ScheduledStage { - private int Id; - private HashSet Candidates; - - public ScheduledStage(int Id, HashSet Candidates) { - this.Id = Id; - this.Candidates = Candidates; - } - - internal void AddCandidate(string c) { - Candidates.Add(c); - } - - internal bool ContainsCandidate(string c) { - return Candidates.Contains(c); - } - - public int GetId() { - return Id; - } - } - } diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 52fb3796..b29aa933 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -215,6 +215,10 @@ namespace Microsoft.Boogie.Houdini { } */ + if(CommandLineOptions.Clo.Trace) { + Console.WriteLine("Houdini assignment axiom: " + expr); + } + return expr; } diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index ee1bdb90..a91c0082 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -38,7 +38,6 @@ namespace Microsoft.Boogie.Houdini { public abstract class HoudiniObserver { public virtual void UpdateStart(Program program, int numConstants) { } - public virtual void UpdateStage(int stage) { } public virtual void UpdateIteration() { } public virtual void UpdateImplementation(Implementation implementation) { } public virtual void UpdateAssignment(Dictionary assignment) { } @@ -133,10 +132,6 @@ namespace Microsoft.Boogie.Houdini { currentIteration = -1; wr.Flush(); } - public override void UpdateStage(int stage) { - wr.WriteLine("Houdini stage " + stage); - wr.Flush(); - } public override void UpdateIteration() { currentIteration++; wr.WriteLine("---------------------------------------"); @@ -215,9 +210,6 @@ namespace Microsoft.Boogie.Houdini { NotifyDelegate notifyDelegate = (NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateStart(program, numConstants); }; Notify(notifyDelegate); } - protected void NotifyStage(int stage) { - Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateStage(stage); }); - } protected void NotifyIteration() { Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateIteration(); }); } @@ -323,12 +315,15 @@ namespace Microsoft.Boogie.Houdini { private HoudiniState currentHoudiniState; private CrossDependencies crossDependencies; + private string cexTraceFile; + public HoudiniState CurrentHoudiniState { get { return currentHoudiniState; } } public static TextWriter explainHoudiniDottyFile; - public Houdini(Program program, HoudiniSession.HoudiniStatistics stats) { + public Houdini(Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.bpl") { this.program = program; + this.cexTraceFile = cexTraceFile; if (CommandLineOptions.Clo.Trace) Console.WriteLine("Collecting existential constants..."); @@ -370,7 +365,6 @@ namespace Microsoft.Boogie.Houdini { } } this.houdiniSessions = new ReadOnlyDictionary(houdiniSessions); - currentHoudiniState = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants)); if (CommandLineOptions.Clo.ExplainHoudini) { @@ -683,7 +677,7 @@ namespace Microsoft.Boogie.Houdini { return nonCandidateErrors.Count > 0; } - private void FlushWorkList() { + private void FlushWorkList(int stage, IEnumerable completedStages) { this.NotifyFlushStart(); while (currentHoudiniState.WorkQueue.Count > 0) { this.NotifyIteration(); @@ -694,7 +688,7 @@ namespace Microsoft.Boogie.Houdini { HoudiniSession session; houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out session); List errors; - ProverInterface.Outcome outcome = TryCatchVerify(session, out errors); + ProverInterface.Outcome outcome = TryCatchVerify(session, stage, completedStages, out errors); UpdateHoudiniOutcome(currentHoudiniState.Outcome, currentHoudiniState.Implementation, outcome, errors); this.NotifyOutcome(outcome); @@ -707,7 +701,7 @@ namespace Microsoft.Boogie.Houdini { private void UpdateAssignment(RefutedAnnotation refAnnot) { if (CommandLineOptions.Clo.Trace) { Console.WriteLine("Removing " + refAnnot.Constant); - using (var cexWriter = new System.IO.StreamWriter("houdiniCexTrace.bpl", true)) + using (var cexWriter = new System.IO.StreamWriter(cexTraceFile, true)) cexWriter.WriteLine("Removing " + refAnnot.Constant); } currentHoudiniState.Assignment.Remove(refAnnot.Constant); @@ -750,7 +744,7 @@ namespace Microsoft.Boogie.Houdini { #region Extra debugging output if (CommandLineOptions.Clo.Trace) { - using (var cexWriter = new System.IO.StreamWriter("houdiniCexTrace.bpl", true)) + using (var cexWriter = new System.IO.StreamWriter(cexTraceFile, true)) { cexWriter.WriteLine("Counter example for " + refutedAnnotation.Constant); cexWriter.Write(error.ToString()); @@ -820,17 +814,15 @@ namespace Microsoft.Boogie.Houdini { } public class HoudiniState { - private WorkQueue _workQueue; - private HashSet blackList; - private Dictionary _assignment; - private int _stage; - private Implementation _implementation; - private HoudiniOutcome _outcome; + public WorkQueue _workQueue; + public HashSet blackList; + public Dictionary _assignment; + public Implementation _implementation; + public HoudiniOutcome _outcome; public HoudiniState(WorkQueue workQueue, Dictionary currentAssignment) { this._workQueue = workQueue; this._assignment = currentAssignment; - this._stage = 0; this._implementation = null; this._outcome = new HoudiniOutcome(); this.blackList = new HashSet(); @@ -842,9 +834,6 @@ namespace Microsoft.Boogie.Houdini { public Dictionary Assignment { get { return this._assignment; } } - public int Stage { - get { return this._stage; } - } public Implementation Implementation { get { return this._implementation; } set { this._implementation = value; } @@ -858,53 +847,45 @@ namespace Microsoft.Boogie.Houdini { public void addToBlackList(string funcName) { blackList.Add(funcName); } - internal void incrementStage() { - _stage++; - } } - public HoudiniOutcome PerformHoudiniInference() { + public HoudiniOutcome PerformHoudiniInference(int stage = 0, + IEnumerable completedStages = null, + Dictionary initialAssignment = null) { this.NotifyStart(program, houdiniConstants.Count); - foreach (Implementation impl in vcgenFailures) { - currentHoudiniState.addToBlackList(impl.Name); - } - while(currentHoudiniState.Stage < NumberOfStages()) { + currentHoudiniState = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants)); - if (CommandLineOptions.Clo.Trace) { - Console.WriteLine("Current stage is " + currentHoudiniState.Stage + " of " + (NumberOfStages() - 1)); + if(initialAssignment != null) { + foreach(var v in CurrentHoudiniState.Assignment.Keys.ToList()) { + CurrentHoudiniState.Assignment[v] = initialAssignment[v.Name]; } + } - this.NotifyStage(currentHoudiniState.Stage); - - while (currentHoudiniState.WorkQueue.Count > 0) { - this.NotifyIteration(); - - currentHoudiniState.Implementation = currentHoudiniState.WorkQueue.Peek(); - this.NotifyImplementation(currentHoudiniState.Implementation); - - HoudiniSession session; - this.houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out session); - HoudiniVerifyCurrent(session); - } + foreach (Implementation impl in vcgenFailures) { + currentHoudiniState.addToBlackList(impl.Name); + } - currentHoudiniState.incrementStage(); + while (currentHoudiniState.WorkQueue.Count > 0) { + this.NotifyIteration(); - #region Re-populate work list for next stage - if (currentHoudiniState.Stage < NumberOfStages()) { - var workList = BuildWorkList(program); - while(workList.Count > 0) { - currentHoudiniState.WorkQueue.Enqueue(workList.Dequeue()); - } - } - #endregion + currentHoudiniState.Implementation = currentHoudiniState.WorkQueue.Peek(); + this.NotifyImplementation(currentHoudiniState.Implementation); + HoudiniSession session; + this.houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out session); + HoudiniVerifyCurrent(session, stage, completedStages); } + this.NotifyEnd(true); Dictionary assignment = new Dictionary(); foreach (var x in currentHoudiniState.Assignment) assignment[x.Key.Name] = x.Value; currentHoudiniState.Outcome.assignment = assignment; + return currentHoudiniState.Outcome; + } + + public void Close() { vcgen.Close(); proverInterface.Close(); if (CommandLineOptions.Clo.ExplainHoudini) @@ -912,7 +893,6 @@ namespace Microsoft.Boogie.Houdini { explainHoudiniDottyFile.WriteLine("};"); explainHoudiniDottyFile.Close(); } - return currentHoudiniState.Outcome; } private int NumberOfStages() @@ -1067,10 +1047,10 @@ namespace Microsoft.Boogie.Houdini { return null; } - private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, out List errors) { + private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable completedStages, out List errors) { ProverInterface.Outcome outcome; try { - outcome = session.Verify(proverInterface, GetAssignmentWithStages(), out errors); + outcome = session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), out errors); } catch (UnexpectedProverOutputException upo) { Contract.Assume(upo != null); @@ -1080,7 +1060,7 @@ namespace Microsoft.Boogie.Houdini { return outcome; } - private Dictionary GetAssignmentWithStages() + private Dictionary GetAssignmentWithStages(int currentStage, IEnumerable completedStages) { Dictionary result = new Dictionary(currentHoudiniState.Assignment); foreach (var c in program.TopLevelDeclarations.OfType()) @@ -1088,24 +1068,24 @@ namespace Microsoft.Boogie.Houdini { int stageActive = QKeyValue.FindIntAttribute(c.Attributes, "stage_active", -1); if (stageActive != -1) { - result[c] = (stageActive == currentHoudiniState.Stage); + result[c] = (stageActive == currentStage); } int stageComplete = QKeyValue.FindIntAttribute(c.Attributes, "stage_complete", -1); if (stageComplete != -1) { - result[c] = (stageComplete < currentHoudiniState.Stage); + result[c] = (completedStages.Contains(stageComplete)); } } return result; } - private void HoudiniVerifyCurrent(HoudiniSession session) { + private void HoudiniVerifyCurrent(HoudiniSession session, int stage, IEnumerable completedStages) { while (true) { this.NotifyAssignment(currentHoudiniState.Assignment); //check the VC with the current assignment List errors; - ProverInterface.Outcome outcome = TryCatchVerify(session, out errors); + ProverInterface.Outcome outcome = TryCatchVerify(session, stage, completedStages, out errors); this.NotifyOutcome(outcome); DebugRefutedCandidates(currentHoudiniState.Implementation, errors); @@ -1133,7 +1113,7 @@ namespace Microsoft.Boogie.Houdini { if (UpdateHoudiniOutcome(currentHoudiniState.Outcome, currentHoudiniState.Implementation, outcome, errors)) { // abort currentHoudiniState.WorkQueue.Dequeue(); this.NotifyDequeue(); - FlushWorkList(); + FlushWorkList(stage, completedStages); return; } else if (UpdateAssignmentWorkList(outcome, errors)) { diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj index 06d68dba..75518155 100644 --- a/Source/Houdini/Houdini.csproj +++ b/Source/Houdini/Houdini.csproj @@ -1,4 +1,4 @@ - + Debug @@ -82,6 +82,7 @@ + diff --git a/Source/Houdini/StagedHoudini.cs b/Source/Houdini/StagedHoudini.cs new file mode 100644 index 00000000..39915f7f --- /dev/null +++ b/Source/Houdini/StagedHoudini.cs @@ -0,0 +1,348 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Diagnostics.Contracts; +using System.Diagnostics; +using System.Threading.Tasks; +using System.Threading; +using Microsoft.Boogie; +using Microsoft.Boogie.GraphUtil; + +namespace Microsoft.Boogie.Houdini +{ + public class StagedHoudini + { + + private Program program; + private Func ProgramFromFile; + private StagedHoudiniPlan plan; + private List[] houdiniInstances; + private List tasks = new List(); + private Dictionary outcomes = new Dictionary(); + + private const string tempFilename = "__stagedHoudiniTemp.bpl"; + + public StagedHoudini(Program program, Func ProgramFromFile) { + this.program = program; + this.ProgramFromFile = ProgramFromFile; + this.houdiniInstances = new List[CommandLineOptions.Clo.StagedHoudiniThreads]; + for (int i = 0; i < CommandLineOptions.Clo.StagedHoudiniThreads; i++) { + houdiniInstances[i] = new List(); + } + + var candidateDependenceAnalyser = new CandidateDependenceAnalyser(program); + candidateDependenceAnalyser.Analyse(); + this.plan = candidateDependenceAnalyser.ApplyStages(); + if (CommandLineOptions.Clo.Trace) + { + candidateDependenceAnalyser.dump(); + EmitProgram("staged.bpl"); + } + } + + public HoudiniOutcome PerformStagedHoudiniInference() + { + + EmitProgram(tempFilename); + + #region Prepare the tasks, but do not launch them + foreach (var s in plan) { + Debug.Assert(!plan.GetDependences(s).Contains(s)); + tasks.Add(new StagedHoudiniTask(s, new Task(() => { + ExecuteStage(s); + }, TaskCreationOptions.LongRunning))); + } + #endregion + + #region Launch the tasks, and wait for them to finish + foreach (var t in tasks) { + t.parallelTask.Start(); + } + Task.WaitAll(tasks.Select(Item => Item.parallelTask).ToArray()); + int count = 0; + foreach(var h in houdiniInstances) { + if(h.Count() > 0) { + count++; + System.Diagnostics.Debug.Assert(h.Count() == 1); + h[0].Close(); + } + } + Console.WriteLine("Used " + count + " houdini instances"); + #endregion + + return UnifyOutcomes(); + + } + + private HoudiniOutcome UnifyOutcomes() + { + HoudiniOutcome result = new HoudiniOutcome(); + var scheduledStages = outcomes.Keys.ToList(); + + result.assignment = new Dictionary(); + foreach(var c in outcomes[scheduledStages[0]].assignment.Keys) { + result.assignment[c] = outcomes.Select(Item => Item.Value).Select(Item => Item.assignment[c]).All(Item => Item); + } + + result.implementationOutcomes = new Dictionary(); + foreach(var p in outcomes[scheduledStages[0]].implementationOutcomes.Keys) { + var unifiedImplementationOutcome = outcomes[scheduledStages[0]].implementationOutcomes[p]; + for(int i = 1; i < scheduledStages.Count(); i++) { + unifiedImplementationOutcome = ChooseOutcome(unifiedImplementationOutcome, + outcomes[scheduledStages[i]].implementationOutcomes[p]); + } + result.implementationOutcomes[p] = unifiedImplementationOutcome; + } + + return result; + } + + private void ExecuteStage(ScheduledStage s) + { + Task.WaitAll(tasks.Where( + Item => plan.GetDependences(s).Contains(Item.stage)). + Select(Item => Item.parallelTask).ToArray()); + + List h = AcquireHoudiniInstance(); + + if (h.Count() == 0) + { + h.Add(new Houdini(ProgramFromFile(tempFilename), new HoudiniSession.HoudiniStatistics(), "houdiniCexTrace_" + s.GetId() + ".bpl")); + } + + System.Diagnostics.Debug.Assert(h.Count() == 1); + + Dictionary mergedAssignment = null; + + List> relevantAssignments; + IEnumerable completedStages; + lock (outcomes) + { + relevantAssignments = + outcomes.Where(Item => plan.Contains(Item.Key)). + Select(Item => Item.Value). + Select(Item => Item.assignment).ToList(); + //outcomes.Values.Select(Item => Item.assignment).ToList(); + completedStages = plan.GetDependences(s).Select(Item => Item.GetId()); + //completedStages = outcomes.Keys.Select(Item => Item.GetId()); + } + + if (relevantAssignments.Count() > 0) + { + mergedAssignment = new Dictionary(); + foreach (var v in relevantAssignments[0].Keys) + { + mergedAssignment[v] = relevantAssignments.Select(Item => Item[v]).ToList().All(Item => Item); + } + } + + HoudiniOutcome outcome = h[0].PerformHoudiniInference( + s.GetId(), + completedStages, + mergedAssignment); + + lock (outcomes) + { + outcomes[s] = outcome; + } + + ReleaseHoudiniInstance(h); + + } + + private static void ReleaseHoudiniInstance(List h) + { + Monitor.Exit(h); + } + + private List AcquireHoudiniInstance() + { + List h = null; + do + { + foreach (var houdini in houdiniInstances) + { + if (Monitor.TryEnter(houdini)) + { + h = houdini; + break; + } + else + { + Thread.Sleep(20); + } + } + } while (h == null); + return h; + } + + private void EmitProgram(string filename) + { + using (TokenTextWriter writer = new TokenTextWriter(filename, true)) + { + int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured; + CommandLineOptions.Clo.PrintUnstructured = 2; + program.Emit(writer); + CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured; + } + } + + + private static VCGenOutcome ChooseOutcome(VCGenOutcome o1, VCGenOutcome o2) { + var vcOutcome1 = o1.outcome; + var vcOutcome2 = o2.outcome; + + if(vcOutcome1 == vcOutcome2) { + return o1; + } + + // Errors trump everything else + if(vcOutcome1 == VC.ConditionGeneration.Outcome.Errors) { + return o1; + } + if(vcOutcome2 == VC.ConditionGeneration.Outcome.Errors) { + return o2; + } + + // If one outcome is Correct, return the other in case it is "worse" + if(vcOutcome1 == VC.ConditionGeneration.Outcome.Correct) { + return o2; + } + if(vcOutcome2 == VC.ConditionGeneration.Outcome.Correct) { + return o1; + } + + // Neither outcome is correct, so if one outcome is ReachedBound, return the other in case it is "worse" + if(vcOutcome1 == VC.ConditionGeneration.Outcome.ReachedBound) { + return o2; + } + if(vcOutcome2 == VC.ConditionGeneration.Outcome.ReachedBound) { + return o1; + } + + // Both outcomes must be timeout or memout; arbitrarily choose the first + return o1; + } + + internal class StagedHoudiniTask { + internal ScheduledStage stage; + internal Task parallelTask; + internal StagedHoudiniTask(ScheduledStage stage, Task parallelTask) { + this.stage = stage; + this.parallelTask = parallelTask; + } + } + + } + + public class StagedHoudiniPlan : IEnumerable { + + private Graph ScheduledStages; + private Dictionary CandidateToStage; + + internal StagedHoudiniPlan(Graph ScheduledStages) { + this.ScheduledStages = ScheduledStages; + this.CandidateToStage = new Dictionary(); + foreach(var s in this) { + Debug.Assert(!GetDependences(s).Contains(s)); + } + } + + public IEnumerable GetDependences(ScheduledStage s) { + IEnumerable result; + lock(ScheduledStages) { + result = ScheduledStages.Successors(s); + } + return result; + } + + + private static int CompareStages(ScheduledStage s1, ScheduledStage s2) { + if(s1.GetId() < s2.GetId()) { + return -1; + } + if(s2.GetId() < s1.GetId()) { + return 1; + } + return 0; + } + + public IEnumerator GetEnumerator() { + List sortedStages = ScheduledStages.Nodes.ToList(); + sortedStages.Sort(CompareStages); + return sortedStages.GetEnumerator(); + } + + System.Collections.IEnumerator System.Collections.IEnumerable.GetEnumerator() + { + return this.GetEnumerator(); + } + + internal ScheduledStage StageForCandidate(string c) { + if(CandidateToStage.ContainsKey(c)) { + return CandidateToStage[c]; + } + foreach(var s in ScheduledStages.Nodes) { + if(s.ContainsCandidate(c)) { + CandidateToStage[c] = s; + return s; + } + } + return null; + } + + public override string ToString() + { + string result = ""; + foreach(ScheduledStage s in this) { + result += "Stage " + s; + + result += " depends on stages: "; + foreach(var id in GetDependences(s).Select(Item => Item.GetId())) { + result += id + " "; + } + result += "\n"; + } + return result; + } + } + + public class ScheduledStage { + private int Id; + private HashSet Candidates; + + public ScheduledStage(int Id, HashSet Candidates) { + this.Id = Id; + this.Candidates = Candidates; + } + + internal void AddCandidate(string c) { + Candidates.Add(c); + } + + internal bool ContainsCandidate(string c) { + return Candidates.Contains(c); + } + + public int GetId() { + return Id; + } + + public int Count() { + return Candidates.Count(); + } + + public override string ToString() + { + string result = "ID: " + Id + "{ "; + foreach(var c in Candidates) { + result += c + " "; + } + result += "}\n"; + return result; + } + } + + +} diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index 2374a157..48a07820 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -114,6 +114,7 @@ namespace Microsoft.Boogie.SMTLib var sx = GetProverResponse(); if (sx == null) { this.NeedsRestart = true; + Debug.Assert(false); HandleError("Prover died"); return; } -- cgit v1.2.3