From 0b4388429f5eb571fce4b1aff508be891ad75b87 Mon Sep 17 00:00:00 2001 From: Pantazis Deligiannis Date: Sun, 29 Sep 2013 11:39:05 +0100 Subject: more changes towards parallelisation of Houdini --- Source/Houdini/Checker.cs | 4 +-- Source/Houdini/ConcurrentHoudini.cs | 71 +++++++++++++++++++++++++++++++------ Source/Houdini/Houdini.cs | 6 ++-- 3 files changed, 66 insertions(+), 15 deletions(-) (limited to 'Source/Houdini') diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 170b5212..30d6062f 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -130,13 +130,13 @@ namespace Microsoft.Boogie.Houdini { return false; } - public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl, HoudiniStatistics stats) { + public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl, HoudiniStatistics stats, int houdiniID = -1) { this.descriptiveName = impl.Name; this.stats = stats; collector = new ConditionGeneration.CounterexampleCollector(); collector.OnProgress("HdnVCGen", 0, 0, 0.0); - vcgen.ConvertCFG2DAG(impl); + vcgen.ConvertCFG2DAG(impl, threadID: houdiniID); ModelViewInfo mvInfo; var gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo); diff --git a/Source/Houdini/ConcurrentHoudini.cs b/Source/Houdini/ConcurrentHoudini.cs index ab5fbdcf..a75cc054 100644 --- a/Source/Houdini/ConcurrentHoudini.cs +++ b/Source/Houdini/ConcurrentHoudini.cs @@ -6,6 +6,7 @@ using System.Diagnostics; using System.Diagnostics.Contracts; using System.Text.RegularExpressions; using System.Linq; +using VC; namespace Microsoft.Boogie.Houdini { @@ -13,13 +14,65 @@ namespace Microsoft.Boogie.Houdini { int id; -// private static ConcurrentDictionary refutedSharedAnnotations; private static ConcurrentDictionary refutedSharedAnnotations; - public ConcurrentHoudini(int id, Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.bpl") - : base(program, stats, cexTraceFile) - { + public ConcurrentHoudini(int id, Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.bpl") { + Contract.Assert(id >= 0); + this.id = id; + this.program = program; + this.cexTraceFile = cexTraceFile; + + if (CommandLineOptions.Clo.Trace) + Console.WriteLine("Collecting existential constants..."); + this.houdiniConstants = CollectExistentialConstants(); + + if (CommandLineOptions.Clo.Trace) + Console.WriteLine("Building call graph..."); + this.callGraph = Program.BuildCallGraph(program); + if (CommandLineOptions.Clo.Trace) + Console.WriteLine("Number of implementations = {0}", callGraph.Nodes.Count); + + if (CommandLineOptions.Clo.HoudiniUseCrossDependencies) + { + if (CommandLineOptions.Clo.Trace) Console.WriteLine("Computing procedure cross dependencies ..."); + this.crossDependencies = new CrossDependencies(this.houdiniConstants); + this.crossDependencies.Visit(program); + } + + Inline(); + + this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List()); + this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime); + + vcgenFailures = new HashSet(); + Dictionary houdiniSessions = new Dictionary(); + if (CommandLineOptions.Clo.Trace) + Console.WriteLine("Beginning VC generation for Houdini..."); + foreach (Implementation impl in callGraph.Nodes) { + try { + if (CommandLineOptions.Clo.Trace) + Console.WriteLine("Generating VC for {0}", impl.Name); + HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats, id); + houdiniSessions.Add(impl, session); + } + catch (VCGenException) { + if (CommandLineOptions.Clo.Trace) + Console.WriteLine("VC generation failed"); + vcgenFailures.Add(impl); + } + } + this.houdiniSessions = new ReadOnlyDictionary(houdiniSessions); + + if (CommandLineOptions.Clo.ExplainHoudini) + { + // Print results of ExplainHoudini to a dotty file + explainHoudiniDottyFile = new StreamWriter("explainHoudini.dot"); + explainHoudiniDottyFile.WriteLine("digraph explainHoudini {"); + foreach (var constant in houdiniConstants) + explainHoudiniDottyFile.WriteLine("{0} [ label = \"{0}\" color=black ];", constant.Name); + explainHoudiniDottyFile.WriteLine("TimeOut [label = \"TimeOut\" color=red ];"); + } } static ConcurrentHoudini() @@ -71,8 +124,7 @@ namespace Microsoft.Boogie.Houdini RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error); // some candidate annotation removed if (refutedAnnotation != null) { - if (CommandLineOptions.Clo.HoudiniShareRefutedCandidates) - refutedSharedAnnotations.TryAdd (refutedAnnotation.Constant.Name, refutedAnnotation); + refutedSharedAnnotations.TryAdd (refutedAnnotation.Constant.Name, refutedAnnotation); AddRelatedToWorkList(refutedAnnotation); UpdateAssignment(refutedAnnotation); dequeue = false; @@ -96,8 +148,7 @@ namespace Microsoft.Boogie.Houdini if (CommandLineOptions.Clo.DebugParallelHoudini) Console.WriteLine("# exchange set size: " + refutedSharedAnnotations.Count); - if (CommandLineOptions.Clo.HoudiniShareRefutedCandidates) - if (ExchangeRefutedAnnotations()) dequeue = false; + if (ExchangeRefutedAnnotations()) dequeue = false; break; default: @@ -145,9 +196,7 @@ namespace Microsoft.Boogie.Houdini while (currentHoudiniState.WorkQueue.Count > 0) { this.NotifyIteration(); - if (CommandLineOptions.Clo.HoudiniShareRefutedCandidates) - ExchangeRefutedAnnotations(); - + ExchangeRefutedAnnotations(); currentHoudiniState.Implementation = currentHoudiniState.WorkQueue.Peek(); this.NotifyImplementation(currentHoudiniState.Implementation); diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 60ab6a25..12c972f3 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -321,6 +321,8 @@ namespace Microsoft.Boogie.Houdini { public static TextWriter explainHoudiniDottyFile; + protected Houdini() { } + public Houdini(Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.bpl") { this.program = program; this.cexTraceFile = cexTraceFile; @@ -377,7 +379,7 @@ namespace Microsoft.Boogie.Houdini { } } - private void Inline() { + protected void Inline() { if (CommandLineOptions.Clo.InlineDepth < 0) return; @@ -434,7 +436,7 @@ namespace Microsoft.Boogie.Houdini { } } - private HashSet CollectExistentialConstants() { + protected HashSet CollectExistentialConstants() { HashSet existentialConstants = new HashSet(); foreach (Declaration decl in program.TopLevelDeclarations) { Constant constant = decl as Constant; -- cgit v1.2.3