merge

5 files changed, 544 insertions, 176 deletions

diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs
index 09cef241..9a2eb404 100644
--- a/Source/Houdini/CandidateDependenceAnalyser.cs
+++ b/Source/Houdini/CandidateDependenceAnalyser.cs
@@ -6,13 +6,13 @@ using Microsoft.Boogie.GraphUtil;
 using Microsoft.Basetypes;

 using System.Diagnostics;

 

-namespace Microsoft.Boogie {

+namespace Microsoft.Boogie.Houdini {

 

   public class CandidateDependenceAnalyser {

 

-    private const int COARSE_STAGES = 1;

-    private const int FINE_STAGES = 2;

-    private const int BALANCED_STAGES = 3;

+    private const string COARSE_STAGES = "COARSE";

+    private const string FINE_STAGES = "FINE";

+    private const string BALANCED_STAGES = "BALANCED";

 

     private Program prog;

     private IVariableDependenceAnalyser varDepAnalyser;

@@ -22,6 +22,7 @@ namespace Microsoft.Boogie {
     private Graph<string> CandidateDependences;

     private StronglyConnectedComponents<string> SCCs;

     private Graph<SCC<string>> StagesDAG;

+    private StagedHoudiniPlan Plan;

 

     public CandidateDependenceAnalyser(Program prog) {

       this.prog = prog;

@@ -193,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);

               }

             }

@@ -206,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);

           }

         }

@@ -355,35 +356,33 @@ namespace Microsoft.Boogie {
     }

 

 

-    public void ApplyStages() {

+    public StagedHoudiniPlan ApplyStages() {

 

         if (NoStages())

         {

-            return;

+            return null;

         }

 

         #region Assign candidates to stages at a given level of granularity

-

-        Dictionary<string, int> candidateToStage;

       

         switch(CommandLineOptions.Clo.StagedHoudini) {

           case COARSE_STAGES:

-            candidateToStage = ComputeCoarseStages();

+            Plan = ComputeCoarseStages();

             break;

           case FINE_STAGES:

-            candidateToStage = ComputeFineStages();

+            Plan = ComputeFineStages();

             break;

           case BALANCED_STAGES:

-            candidateToStage = ComputeBalancedStages();

+            Plan = ComputeBalancedStages();

             break;

           default:

             Debug.Assert(false);

-            candidateToStage = null;

+            Plan = null;

             break;

         }

         

         foreach(var c in candidates) {

-          Debug.Assert(candidateToStage.ContainsKey(c));

+          Debug.Assert(Plan.StageForCandidate(c) != null);

         }

         #endregion

 

@@ -391,21 +390,21 @@ namespace Microsoft.Boogie {
         var stageToActiveBoolean = new Dictionary<int, Constant>();

         var stageToCompleteBoolean = new Dictionary<int, Constant>();

 

-        foreach (var stage in new HashSet<int>(candidateToStage.Values))

+        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)) });

+            stageActive.AddAttribute("stage_active", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(stage.GetId())) });

             prog.TopLevelDeclarations.Add(stageActive);

-            stageToActiveBoolean[stage] = 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)) });

+            stageComplete.AddAttribute("stage_complete", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(stage.GetId())) });

             prog.TopLevelDeclarations.Add(stageComplete);

-            stageToCompleteBoolean[stage] = stageComplete;

+            stageToCompleteBoolean[stage.GetId()] = stageComplete;

         }

         #endregion

 

@@ -417,12 +416,12 @@ 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,

-                        new IdentifierExpr(Token.NoToken, stageToActiveBoolean[candidateToStage[c]]), c), a.Attributes));

-                    newCmds.Add(new AssumeCmd(a.tok, Houdini.Houdini.AddConditionToCandidate(a.Expr,

-                        new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[candidateToStage[c]]), c), a.Attributes));

+                    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.AddConditionToCandidate(a.Expr,

+                        new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[Plan.StageForCandidate(c).GetId()]), c), a.Attributes));

                 }

                 else

                 {

@@ -441,14 +440,14 @@ 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,

-                new IdentifierExpr(Token.NoToken, stageToActiveBoolean[candidateToStage[c]]), c),

+                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,

-                new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[candidateToStage[c]]), c),

+                Houdini.AddConditionToCandidate(r.Condition,

+                new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[Plan.StageForCandidate(c).GetId()]), c),

                 r.Comment, r.Attributes));

             } else {

               newRequires.Add(r);

@@ -461,16 +460,16 @@ namespace Microsoft.Boogie {
           EnsuresSeq newEnsures = new EnsuresSeq();

           foreach(Ensures e in p.Ensures) {

             string c;

-            if (Houdini.Houdini.MatchCandidate(e.Condition, candidates, out c)) {

-              int stage = candidateToStage[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,

-                new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[candidateToStage[c]]), c),

+                Houdini.AddConditionToCandidate(e.Condition,

+                new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[stage]), c),

                 e.Comment, e.Attributes));

             } else {

               newEnsures.Add(e);

@@ -482,6 +481,8 @@ namespace Microsoft.Boogie {
         }

         #endregion

 

+        return Plan;

+

     }

 

     private int FindLargestStage() {

@@ -489,78 +490,110 @@ namespace Microsoft.Boogie {
     }

 

 

-    private Dictionary<string, int> ComputeCoarseStages()

+    private StagedHoudiniPlan ComputeCoarseStages()

     {

-        var result = new Dictionary<string, int>();

-        HashSet<SCC<string>> done = new HashSet<SCC<string>> { GetStartNodeOfStagesDAG() };

-        for(int stageId = 0; done.Count() != StagesDAG.Nodes.Count(); stageId++)

+        foreach(var n in StagesDAG.Nodes) {

+          Debug.Assert(!StagesDAG.Successors(n).Contains(n));

+        }

+

+        Graph<ScheduledStage> Dependences = new Graph<ScheduledStage>();

+

+        var done = new Dictionary<SCC<string>, ScheduledStage>();

+        done[GetStartNodeOfStagesDAG()] = new ScheduledStage(0, new HashSet<string>());

+

+        for(int stageId = 1; done.Count() != StagesDAG.Nodes.Count(); stageId++)

         {

-            foreach (var n in StagesDAG.Nodes.Where(Item => !done.Contains(Item)))

+            var Stage = new ScheduledStage(stageId, new HashSet<string>());

+            HashSet<SCC<string>> AssignedToThisStage = new HashSet<SCC<string>>();

+

+            foreach (var n in StagesDAG.Nodes.Where(Item => !done.ContainsKey(Item)))

             {

-              if(StagesDAG.Successors(n).Where(Item => !done.Contains(Item)).Count() == 0) {

+              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)

                 {

-                    result[c] = stageId;

+                  Stage.AddCandidate(c);

                 }

-                done.Add(n);

+                Console.Write(n.Count() + ", ");

+                AssignedToThisStage.Add(n);

               }

             }

+

+            Console.WriteLine("total: " + Stage.Count());

+

+            foreach(var n in AssignedToThisStage) {

+              done[n] = Stage;

+            }

         }

-        return result;

+        return new StagedHoudiniPlan(Dependences);

     }

 

-    private Dictionary<string, int> ComputeBalancedStages()

+    private StagedHoudiniPlan ComputeBalancedStages()

     {

-        int maxStageSize = 200;

-        var result = new Dictionary<string, int>();

-        HashSet<SCC<string>> done = new HashSet<SCC<string>> { GetStartNodeOfStagesDAG() };

-        for(int stageId = 0; done.Count() != StagesDAG.Nodes.Count(); stageId++)

+      Graph<ScheduledStage> Dependences = new Graph<ScheduledStage>();

+      var done = new Dictionary<SCC<string>, ScheduledStage>();

+      done[GetStartNodeOfStagesDAG()] = new ScheduledStage(0, new HashSet<string>());

+

+      int maxStageSize = 200;

+

+      for(int stageId = 1; done.Count() != StagesDAG.Nodes.Count(); stageId++)

+      {

+        int stageSize = 0;

+        ScheduledStage Stage = new ScheduledStage(stageId, new HashSet<string>());

+        HashSet<SCC<string>> AddedToThisStage = new HashSet<SCC<string>>();

+

+        foreach (var n in StagesDAG.Nodes.Where(Item => !done.ContainsKey(Item)))

         {

-          int stageSize = 0;

-          foreach (var n in StagesDAG.Nodes.Where(Item => !done.Contains(Item)))

-          {

-            if(stageSize + n.Count() > maxStageSize) {

-              continue;

+          if(stageSize + n.Count() > maxStageSize) {

+            continue;

+          }

+          if(StagesDAG.Successors(n).Where(Item => !done.ContainsKey(Item)).Count() == 0) {

+            foreach (var c in n)

+            {

+              Stage.AddCandidate(c);

+              stageSize++;

             }

-            if(StagesDAG.Successors(n).Where(Item => !done.Contains(Item)).Count() == 0) {

-              foreach (var c in n)

-              {

-                result[c] = stageId;

-                stageSize++;

-              }

-              done.Add(n);

+            foreach(var s in StagesDAG.Successors(n)) {

+              Dependences.AddEdge(Stage, done[s]);

             }

+            AddedToThisStage.Add(n);

           }

-          if(stageSize == 0) {

-            maxStageSize *= 2;

-          }

         }

-        return result;

+        foreach(var n in AddedToThisStage) {

+          done[n] = Stage;

+        }

+        if(stageSize == 0) {

+          maxStageSize *= 2;

+        }

+      }

+      return new StagedHoudiniPlan(Dependences);

     }

 

-    private Dictionary<string, int> ComputeFineStages()

+    private StagedHoudiniPlan ComputeFineStages()

     {

-      

-        var result = new Dictionary<string, int>();

-        List<SCC<string>> components = StagesDAG.TopologicalSort().ToList();

-        components.Reverse();

+      Graph<ScheduledStage> Dependences = new Graph<ScheduledStage>();

+      var done = new Dictionary<SCC<string>, ScheduledStage>();

 

-        System.Diagnostics.Debug.Assert(components[0].Count() == 0);

-        for (int i = 1; i < components.Count(); i++)

-        {

-            foreach (var c in components[i])

-            {

-                result[c] = i - 1;

-            }

+      List<SCC<string>> components = StagesDAG.TopologicalSort().ToList();

+      components.Reverse();

 

+      for (int i = 0; i < components.Count(); i++)

+      {

+        ScheduledStage Stage = new ScheduledStage(i, new HashSet<string>());

+        done[components[i]] = Stage;

+        foreach (var c in components[i])

+        {

+          Stage.AddCandidate(c);

         }

-

-        foreach(var c in candidates) {

-          Debug.Assert(result.ContainsKey(c));

+        foreach(var s in StagesDAG.Successors(components[i])) {

+          Dependences.AddEdge(Stage, done[s]);

         }

-

-        return result;

-

+      }

+      return new StagedHoudiniPlan(Dependences);

     }

 

     private SCC<string> GetStartNodeOfStagesDAG()

@@ -608,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);

             }

           }

@@ -619,7 +652,7 @@ namespace Microsoft.Boogie {
       foreach(var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {

         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<string, PrePost>(proc.Name, PrePost.PRE));

           }

         }

@@ -629,7 +662,7 @@ namespace Microsoft.Boogie {
       foreach(var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {

         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<string, PrePost>(proc.Name, PrePost.POST));

           }

         }

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index a64cece0..b29aa933 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -94,14 +94,20 @@ namespace Microsoft.Boogie.Houdini {
     }

   }

 

+

+

   public class HoudiniSession {

-    public static double proverTime = 0;

-    public static int numProverQueries = 0;

-    public static double unsatCoreProverTime = 0;

-    public static int numUnsatCoreProverQueries = 0;

-    public static int numUnsatCorePrunings = 0;

+

+    public class HoudiniStatistics {

+      public double proverTime = 0;

+      public int numProverQueries = 0;

+      public double unsatCoreProverTime = 0;

+      public int numUnsatCoreProverQueries = 0;

+      public int numUnsatCorePrunings = 0;

+    }

 

     public string descriptiveName;

+    public HoudiniStatistics stats;

     private VCExpr conjecture;

     private ProverInterface.ErrorHandler handler;

     ConditionGeneration.CounterexampleCollector collector;

@@ -115,20 +121,18 @@ namespace Microsoft.Boogie.Houdini {
     private HashSet<Variable> explainConstantsNegative;

     private Dictionary<string, Tuple<Variable, Variable>> constantToControl;

 

-    Houdini houdini;

-    Implementation implementation;

-

     public bool InUnsatCore(Variable constant) {

       if (unsatCoreSet == null)

         return true;

       if (unsatCoreSet.Contains(constant))

         return true;

-      numUnsatCorePrunings++;

+      stats.numUnsatCorePrunings++;

       return false;

     }

 

-    public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl) {

-      descriptiveName = impl.Name;

+    public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl, HoudiniStatistics stats) {

+      this.descriptiveName = impl.Name;

+      this.stats = stats;

       collector = new ConditionGeneration.CounterexampleCollector();

       collector.OnProgress("HdnVCGen", 0, 0, 0.0);

 

@@ -170,8 +174,6 @@ namespace Microsoft.Boogie.Houdini {
         handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, proverInterface.Context, program);

       }

 

-      this.houdini = houdini;

-      this.implementation = impl;

     }

 

     private VCExpr BuildAxiom(ProverInterface proverInterface, Dictionary<Variable, bool> currentAssignment) {

@@ -213,6 +215,10 @@ namespace Microsoft.Boogie.Houdini {
       }

        */

 

+      if(CommandLineOptions.Clo.Trace) {

+        Console.WriteLine("Houdini assignment axiom: " + expr);

+      }

+

       return expr;

     }

 

@@ -229,8 +235,8 @@ namespace Microsoft.Boogie.Houdini {
       ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler);

 

       double queryTime = (DateTime.UtcNow - now).TotalSeconds;

-      proverTime += queryTime;

-      numProverQueries++;

+      stats.proverTime += queryTime;

+      stats.numProverQueries++;

       if (CommandLineOptions.Clo.Trace) {

         Console.WriteLine("Time taken = " + queryTime);

       }

@@ -387,20 +393,20 @@ namespace Microsoft.Boogie.Houdini {
             }

             foreach (var r in reason)

             {

-                Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, r, implementation.Name);

+                Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, r, descriptiveName);

             }

         } while (false);

 

         if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || outcome == ProverInterface.Outcome.Undetermined)

         {

-            Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, "TimeOut", implementation.Name);

+            Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, "TimeOut", descriptiveName);

         }

 

         CommandLineOptions.Clo.ProverCCLimit = el;

 

         double queryTime = (DateTime.UtcNow - now).TotalSeconds;

-        proverTime += queryTime;

-        numProverQueries++;

+        stats.proverTime += queryTime;

+        stats.numProverQueries++;

         if (CommandLineOptions.Clo.Trace)

         {

             Console.WriteLine("Time taken = " + queryTime);

@@ -434,8 +440,8 @@ namespace Microsoft.Boogie.Houdini {
       proverInterface.Pop();

 

       double unsatCoreQueryTime = (DateTime.UtcNow - now).TotalSeconds;

-      unsatCoreProverTime += unsatCoreQueryTime;

-      numUnsatCoreProverQueries++;

+      stats.unsatCoreProverTime += unsatCoreQueryTime;

+      stats.numUnsatCoreProverQueries++;

     }

 

   }

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index abc5a7e8..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<Variable, bool> 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) {

+    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...");

@@ -360,7 +355,7 @@ namespace Microsoft.Boogie.Houdini {
         try {

           if (CommandLineOptions.Clo.Trace)

             Console.WriteLine("Generating VC for {0}", impl.Name);

-          HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl);

+          HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats);

           houdiniSessions.Add(impl, session);

         }

         catch (VCGenException) {

@@ -370,7 +365,6 @@ namespace Microsoft.Boogie.Houdini {
         }

       }

       this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(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<int> 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<Counterexample> 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<string> blackList;

-      private Dictionary<Variable, bool> _assignment;

-      private int _stage;

-      private Implementation _implementation;

-      private HoudiniOutcome _outcome;

+      public WorkQueue _workQueue;

+      public HashSet<string> blackList;

+      public Dictionary<Variable, bool> _assignment;

+      public Implementation _implementation;

+      public HoudiniOutcome _outcome;

 

       public HoudiniState(WorkQueue workQueue, Dictionary<Variable, bool> currentAssignment) {

         this._workQueue = workQueue;

         this._assignment = currentAssignment;

-        this._stage = 0;

         this._implementation = null;

         this._outcome = new HoudiniOutcome();

         this.blackList = new HashSet<string>();

@@ -842,9 +834,6 @@ namespace Microsoft.Boogie.Houdini {
       public Dictionary<Variable, bool> 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<int> completedStages = null,

+                                                  Dictionary<string, bool> 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<string, bool> assignment = new Dictionary<string, bool>();

       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<Counterexample> errors) {

+    private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> 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<Variable, bool> GetAssignmentWithStages()

+    private Dictionary<Variable, bool> GetAssignmentWithStages(int currentStage, IEnumerable<int> completedStages)

     {

       Dictionary<Variable, bool> result = new Dictionary<Variable, bool>(currentHoudiniState.Assignment);

       foreach (var c in program.TopLevelDeclarations.OfType<Constant>())

@@ -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<int> completedStages) {

       while (true) {

         this.NotifyAssignment(currentHoudiniState.Assignment);

 

         //check the VC with the current assignment

         List<Counterexample> 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 e4840d1d..6c98c2a8 100644
--- a/Source/Houdini/Houdini.csproj
+++ b/Source/Houdini/Houdini.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>

+<?xml version="1.0" encoding="utf-8"?>

 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

   <PropertyGroup>

     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

@@ -84,6 +84,7 @@
     <Compile Include="Checker.cs" />

     <Compile Include="CandidateDependenceAnalyser.cs" />

     <Compile Include="Houdini.cs" />

+    <Compile Include="StagedHoudini.cs" />

   </ItemGroup>

   <ItemGroup>

     <ProjectReference Include="..\Basetypes\Basetypes.csproj">

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<string, Program> ProgramFromFile;

+    private StagedHoudiniPlan plan;

+    private List<Houdini>[] houdiniInstances;

+    private List<StagedHoudiniTask> tasks = new List<StagedHoudiniTask>();

+    private Dictionary<ScheduledStage, HoudiniOutcome> outcomes = new Dictionary<ScheduledStage,HoudiniOutcome>();

+

+    private const string tempFilename = "__stagedHoudiniTemp.bpl";

+

+    public StagedHoudini(Program program, Func<string, Program> ProgramFromFile) {

+      this.program = program;

+      this.ProgramFromFile = ProgramFromFile;

+      this.houdiniInstances = new List<Houdini>[CommandLineOptions.Clo.StagedHoudiniThreads];

+      for (int i = 0; i < CommandLineOptions.Clo.StagedHoudiniThreads; i++) {

+        houdiniInstances[i] = new List<Houdini>();

+      }

+

+      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<string,bool>();

+      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<string,VCGenOutcome>();

+      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<Houdini> 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<string, bool> mergedAssignment = null;

+

+      List<Dictionary<string, bool>> relevantAssignments;

+      IEnumerable<int> 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<string, bool>();

+        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<Houdini> h)

+    {

+      Monitor.Exit(h);

+    }

+

+    private List<Houdini> AcquireHoudiniInstance()

+    {

+      List<Houdini> 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<ScheduledStage> {

+

+    private Graph<ScheduledStage> ScheduledStages;

+    private Dictionary<string, ScheduledStage> CandidateToStage;

+

+    internal StagedHoudiniPlan(Graph<ScheduledStage> ScheduledStages) {

+      this.ScheduledStages = ScheduledStages;

+      this.CandidateToStage = new Dictionary<string, ScheduledStage>();

+      foreach(var s in this) {

+        Debug.Assert(!GetDependences(s).Contains(s));

+      }

+    }

+

+    public IEnumerable<ScheduledStage> GetDependences(ScheduledStage s) {

+      IEnumerable<ScheduledStage> 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<ScheduledStage> GetEnumerator() {

+      List<ScheduledStage> 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<string> Candidates;

+

+    public ScheduledStage(int Id, HashSet<string> 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;

+    }

+  }

+

+

+}