Worked on the parallelization.

3 files changed, 152 insertions, 69 deletions

diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs
index 7e2ec984..b317dc71 100644
--- a/Source/Doomed/DoomCheck.cs
+++ b/Source/Doomed/DoomCheck.cs
@@ -115,21 +115,26 @@ void ObjectInvariant()
 

             // Todo: Check if vc is trivial true or false            

             outcome = ProverInterface.Outcome.Undetermined;

-            Contract.Assert( m_ErrorHandler !=null);

-            m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);

-            m_Checker.ProverTask.Wait();

-            

-            try {

+            Contract.Assert(m_ErrorHandler != null);

+            try

+            {

+              m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);

+              m_Checker.ProverTask.Wait();

               outcome = m_Checker.ReadOutcome();

-              m_Checker.GoBackToIdle();

-            } catch (UnexpectedProverOutputException e)

+            }

+            catch (UnexpectedProverOutputException e)

             {

-              if (CommandLineOptions.Clo.TraceVerify) { 

+              if (CommandLineOptions.Clo.TraceVerify)

+              {

                 Console.WriteLine("Prover is unable to check {0}! Reason:", lv[0].Name);

                 Console.WriteLine(e.ToString());

               }

               return false;

-            }                        

+            }

+            finally

+            {

+              m_Checker.GoBackToIdle();

+            }

             return true;

         }

     }

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 5bc5eba3..62f180d7 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -972,10 +972,11 @@ namespace VC {
     #endregion

 

 

-    protected Checker FindCheckerFor(int timeout)

+    protected Checker FindCheckerFor(int timeout, bool isBlocking = true)

     {

       Contract.Ensures(Contract.Result<Checker>() != null);

 

+      var maxRetries = 3;

       lock (checkers)

       {

       retry:

@@ -1008,8 +1009,16 @@ namespace VC {
 

         if (Cores <= checkers.Count)

         {

-          Monitor.Wait(checkers, 50);

-          goto retry;

+          if (isBlocking || 0 < maxRetries)

+          {

+            Monitor.Wait(checkers, 50);

+            maxRetries--;

+            goto retry;

+          }

+          else

+          {

+            return null;

+          }

         }

 

         // Create a new checker.

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 5369d13e..d40b1008 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -312,10 +312,22 @@ namespace VC {
             System.Console.WriteLine(" --- smoke #{0}, after passify", id);

             Emit();

           }

-          ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));

-          ch.ProverTask.Wait();

+          try

+          {

+            ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));

+            ch.ProverTask.Wait();

+          }

+          catch

+          {

+            throw;

+          }

+          finally

+          {

+            ch.GoBackToIdle();

+          }

+          

           ProverInterface.Outcome outcome = ch.ReadOutcome();

-          ch.GoBackToIdle();

+          

           parent.CurrentLocalVariables = null;

 

           DateTime end = DateTime.UtcNow;

@@ -1190,13 +1202,16 @@ namespace VC {
       /// <summary>

       /// As a side effect, updates "this.parent.CumulativeAssertionCount".

       /// </summary>

-      public void BeginCheck(VerifierCallback callback, ModelViewInfo mvInfo, int no, int timeout) {

+      public void BeginCheck(Checker checker, VerifierCallback callback, ModelViewInfo mvInfo, int no, int timeout) {

+        Contract.Requires(checker != null);

         Contract.Requires(callback != null);

+

         splitNo = no;

 

         impl.Blocks = blocks;

 

-        checker = parent.FindCheckerFor(timeout);

+        this.checker = checker;

+

         lock (checker)

         {

           Hashtable/*<int, Absy!>*/ label2absy = new Hashtable/*<int, Absy!>*/();

@@ -1240,7 +1255,7 @@ namespace VC {
               }

               return vce;

             }

-        ));

+          ));

 

           var exprGen = ctx.ExprGen;

           VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);

@@ -1457,101 +1472,155 @@ namespace VC {
         remaining_cost = work.Peek().Cost;

       }

 

-      while (work.Any() || currently_running.Any()) {

+      while (work.Any() || currently_running.Any())

+      {

         bool prover_failed = false;

-        Split s;

+        Split s = null;

+        var isWaiting = !work.Any();

 

-        if (work.Any() && currently_running.Count < Cores) {

-          s = work.Pop();

+        if (!isWaiting)

+        {

+          s = work.Peek();

 

-          if (first_round && max_splits > 1) {

+          if (first_round && max_splits > 1)

+          {

             prover_failed = true;

             remaining_cost -= s.Cost;

-          } else {

-            if (CommandLineOptions.Clo.Trace && no >= 0) {

-              System.Console.WriteLine("    checking split {1}/{2}, {3:0.00}%, {0} ...", 

+          }

+          else

+          {

+            var timeout = (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :

+                  keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :

+                  CommandLineOptions.Clo.ProverKillTime;

+

+            var checker = s.parent.FindCheckerFor(timeout, false);

+            if (checker == null)

+            {

+              isWaiting = true;

+              goto waiting;

+            }

+            else

+            {

+              s = work.Pop();

+            }

+

+            if (CommandLineOptions.Clo.Trace && no >= 0)

+            {

+              System.Console.WriteLine("    checking split {1}/{2}, {3:0.00}%, {0} ...",

                                    s.Stats, no + 1, total, 100 * proven_cost / (proven_cost + remaining_cost));

             }

             callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));

 

             Contract.Assert(s.parent == this);

-            s.BeginCheck(callback, mvInfo, no,

-                (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :

-                  keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :

-                  CommandLineOptions.Clo.ProverKillTime);

+            s.BeginCheck(checker, callback, mvInfo, no, timeout);

 

             no++;

 

             currently_running.Add(s);

           }

-        } else {

+        }

+

+      waiting:

+        if (isWaiting)

+        {

           // Wait for one split to terminate.

           var tasks = currently_running.Select(splt => splt.ProverTask).ToArray();

-          int index = Task.WaitAny(tasks);          

-          s = currently_running[index];

-          currently_running.RemoveAt(index);

 

-          if (do_splitting) {

-            remaining_cost -= s.Cost;

-          }

+          if (tasks.Any())

+          {

+            try

+            {

+              int index = Task.WaitAny(tasks);

+              s = currently_running[index];

+              currently_running.RemoveAt(index);

 

-          s.ReadOutcome(ref outcome, out prover_failed);

+              if (do_splitting)

+              {

+                remaining_cost -= s.Cost;

+              }

 

-          if (do_splitting) {

-            if (prover_failed) {

-              // even if the prover fails, we have learned something, i.e., it is 

-              // annoying to watch Boogie say Timeout, 0.00% a couple of times

-              proven_cost += s.Cost / 100;

-            } else {

-              proven_cost += s.Cost;

-            }

-          }

-          callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));

+              s.ReadOutcome(ref outcome, out prover_failed);

 

-          if (prover_failed && !first_round && s.LastChance) {

-            string msg = "some timeout";

-            if (s.reporter != null && s.reporter.resourceExceededMessage != null) {

-              msg = s.reporter.resourceExceededMessage;

-            }

-            callback.OnCounterexample(s.ToCounterexample(s.Checker.TheoremProver.Context), msg);

-            outcome = Outcome.Errors;

-            break;

-          }

+              if (do_splitting)

+              {

+                if (prover_failed)

+                {

+                  // even if the prover fails, we have learned something, i.e., it is 

+                  // annoying to watch Boogie say Timeout, 0.00% a couple of times

+                  proven_cost += s.Cost / 100;

+                }

+                else

+                {

+                  proven_cost += s.Cost;

+                }

+              }

+              callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));

 

-          s.Checker.GoBackToIdle();

+              if (prover_failed && !first_round && s.LastChance)

+              {

+                string msg = "some timeout";

+                if (s.reporter != null && s.reporter.resourceExceededMessage != null)

+                {

+                  msg = s.reporter.resourceExceededMessage;

+                }

+                callback.OnCounterexample(s.ToCounterexample(s.Checker.TheoremProver.Context), msg);

+                outcome = Outcome.Errors;

+                break;

+              }

+            }

+            catch

+            {

+              throw;

+            }

+            finally

+            {

+              s.Checker.GoBackToIdle();

+            }

 

-          Contract.Assert( prover_failed || outcome == Outcome.Correct || outcome == Outcome.Errors || outcome == Outcome.Inconclusive);

+            Contract.Assert(prover_failed || outcome == Outcome.Correct || outcome == Outcome.Errors || outcome == Outcome.Inconclusive);

+          }

         }

 

-        if (prover_failed) { 

+        if (prover_failed)

+        {

           int splits = first_round && max_splits > 1 ? max_splits : max_kg_splits;

 

-          if (splits > 1) {

+          if (splits > 1)

+          {

             List<Split> tmp = Split.DoSplit(s, max_vc_cost, splits);

             Contract.Assert(tmp != null);

             max_vc_cost = 1.0; // for future

             first_round = false;

             //tmp.Sort(new Comparison<Split!>(Split.Compare));

-            foreach (Split a in tmp) {

+            foreach (Split a in tmp)

+            {

               Contract.Assert(a != null);

               work.Push(a);

               total++;

               remaining_cost += a.Cost;

             }

-            if (outcome != Outcome.Errors) {

+            if (outcome != Outcome.Errors)

+            {

               outcome = Outcome.Correct;

             }

-          } else {

-            Contract.Assert( outcome != Outcome.Correct);

-            if (outcome == Outcome.TimedOut) {

+          }

+          else

+          {

+            Contract.Assert(outcome != Outcome.Correct);

+            if (outcome == Outcome.TimedOut)

+            {

               string msg = "some timeout";

-              if (s.reporter != null && s.reporter.resourceExceededMessage != null) {

+              if (s.reporter != null && s.reporter.resourceExceededMessage != null)

+              {

                 msg = s.reporter.resourceExceededMessage;

               }

               callback.OnTimeout(msg);

-            } else if (outcome == Outcome.OutOfMemory) {

+            }

+            else if (outcome == Outcome.OutOfMemory)

+            {

               string msg = "out of memory";

-              if (s.reporter != null && s.reporter.resourceExceededMessage != null) {

+              if (s.reporter != null && s.reporter.resourceExceededMessage != null)

+              {

                 msg = s.reporter.resourceExceededMessage;

               }

               callback.OnOutOfMemory(msg);