more changes towards parallelisation of Houdini

7 files changed, 95 insertions, 38 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4eb62682..5f60d93e 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -397,9 +397,9 @@ namespace Microsoft.Boogie {
     public bool IntraproceduralInfer = true;

     public bool ContractInfer = false;

     public bool ExplainHoudini = false;

-    public bool HoudiniShareRefutedCandidates = false;

+    public bool ConcurrentHoudini = false;

     public bool DisableLoopInvMaintainedAssert = false;

-    public bool ReverseTopologicalSorting = false;

+    public bool ModifyTopologicalSorting = false;

     public bool DebugParallelHoudini = false;

     public bool HoudiniUseCrossDependencies = false;

     public string StagedHoudini = null;

@@ -647,6 +647,15 @@ namespace Microsoft.Boogie {
     }

     public AiFlags/*!*/ Ai = new AiFlags();

 

+    public class ConcurrentHoudiniOptions

+    {

+      public int ProverCCLimit = 5;

+      public bool DisableLoopInvMaintainedAssert = false;

+      public bool ModifyTopologicalSorting = false;

+      public int LoopUnrollCount = -1;

+    }

+    public List<ConcurrentHoudiniOptions> Cho = new List<ConcurrentHoudiniOptions>();

+

     protected override bool ParseOption(string name, CommandLineOptionEngine.CommandLineParseState ps) {

       var args = ps.args;  // convenient synonym

       switch (name) {

@@ -1169,21 +1178,15 @@ namespace Microsoft.Boogie {
           }

           return true;

 

-        case "sharedRefutation":

-          if (ps.ConfirmArgumentCount(0)) {

-            HoudiniShareRefutedCandidates = true;

-          }

-          return true;

-

-        case "disableLoopInvMaintainedAssert":

+        case "concurrentHoudini":

           if (ps.ConfirmArgumentCount(0)) {

-            DisableLoopInvMaintainedAssert = true;

+            ConcurrentHoudini = true;

           }

           return true;

 

-        case "reverseTopologicalSorting":

+        case "modifyTopologicalSorting":

           if (ps.ConfirmArgumentCount(0)) {

-            ReverseTopologicalSorting = true;

+            ModifyTopologicalSorting = true;

           }

           return true;

 

@@ -1680,14 +1683,6 @@ namespace Microsoft.Boogie {
   /printInstrumented

                 print Boogie program after it has been instrumented with

                 invariants

-  /sharedRefutation

-                Enables sharing of refuted candidate invariants between multiple threads.

-  /disableLoopInvMaintainedAssert

-                Disables the loop invariant check to maintain the invariant after iteration.

-                This is an under-approximation feature

-  /reverseTopologicalSorting

-                Reverses the order that roots are found in the Topological Sorting algorithm.

-                Can be used to potentially change the order that Houdini refutes candidates

 

   ---- Debugging and general tracing options ---------------------------------

 

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 2bd7519e..f3056e4f 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -407,7 +407,7 @@ namespace Microsoft.Boogie {
       }

 

       IEnumerable<Block> sortedNodes;

-      if (CommandLineOptions.Clo.ReverseTopologicalSorting) {

+      if (CommandLineOptions.Clo.ModifyTopologicalSorting) {

         sortedNodes = dag.TopologicalSort(true);

       } else {

         sortedNodes = dag.TopologicalSort();

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;

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index e0ef2aed..8fe4a5c6 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1344,7 +1344,7 @@ namespace VC {
       }

 

       IEnumerable sortedNodes;

-      if (CommandLineOptions.Clo.ReverseTopologicalSorting) {

+      if (CommandLineOptions.Clo.ModifyTopologicalSorting) {

         sortedNodes = dag.TopologicalSort(true);

       } else {

         sortedNodes = dag.TopologicalSort();

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 3d9698fd..5880eb16 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1875,7 +1875,7 @@ namespace VC {
           }

       }

 

-    public void ConvertCFG2DAG(Implementation impl, Dictionary<Block,List<Block>> edgesCut = null)

+    public void ConvertCFG2DAG(Implementation impl, Dictionary<Block,List<Block>> edgesCut = null, int threadID = -1)

     {

     Contract.Requires(impl != null);

       impl.PruneUnreachableBlocks();  // This is needed for VCVariety.BlockNested, and is otherwise just an optimization

@@ -1945,6 +1945,17 @@ namespace VC {
               b.ErrorData = c.ErrorData;

               prefixOfPredicateCmdsInit.Add(b);

 

+              if (CommandLineOptions.Clo.ConcurrentHoudini) {

+                if (CommandLineOptions.Clo.Cho[threadID].DisableLoopInvMaintainedAssert)

+                  b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, Expr.True);

+                else

+                  b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);

+              } else {

+                b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);

+              }

+

+              if (threadID >= 0 && CommandLineOptions.Clo.DisableLoopInvMaintainedAssert)

+

               if (CommandLineOptions.Clo.DisableLoopInvMaintainedAssert)

                 b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, Expr.True);

               else