Revamp of staged Houdini, and completion of parallel support.

8 files changed, 505 insertions, 172 deletions

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<CancellationTokenSource>();

 

-      #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<string> { 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<ScheduledStage> Dependences = new Graph<ScheduledStage>();

 

         var done = new Dictionary<SCC<string>, 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<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.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<string>());

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

+

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

           }

         }

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

           }

         }

@@ -712,68 +731,4 @@ namespace Microsoft.Boogie {
     }

   }

 

-  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>();

-    }

-

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

-      return ScheduledStages.Successors(s);

-    }

-

-    public IEnumerator<ScheduledStage> 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<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;

-    }

-  }

-

 }

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<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, 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<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 06d68dba..75518155 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>

@@ -82,6 +82,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;

+    }

+  }

+

+

+}

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;

         }