more changes towards parallelisation of Houdini

3 files changed, 66 insertions, 15 deletions

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<RefutedAnnotation, int> refutedSharedAnnotations;
     private static ConcurrentDictionary<string, RefutedAnnotation> 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<Checker>());
+      this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
+
+      vcgenFailures = new HashSet<Implementation>();
+      Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
+      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<Implementation, HoudiniSession>(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<Variable> CollectExistentialConstants() {

+    protected HashSet<Variable> CollectExistentialConstants() {

       HashSet<Variable> existentialConstants = new HashSet<Variable>();

       foreach (Declaration decl in program.TopLevelDeclarations) {

         Constant constant = decl as Constant;