Did some refactoring in the execution engine and worked on the parallelization.

1 files changed, 45 insertions, 16 deletions

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 0a1059fe..d214517a 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -18,6 +18,15 @@ using Microsoft.Basetypes;
 using System.Threading.Tasks;

 

 namespace Microsoft.Boogie {

+

+  enum CheckerStatus

+  {

+    Idle,

+    Ready,

+    Busy,

+    Closed

+  }

+

   /// <summary>

   /// Interface to the theorem prover specialized to Boogie.

   ///

@@ -38,18 +47,32 @@ namespace Microsoft.Boogie {
 

     // state for the async interface

     private volatile ProverInterface.Outcome outcome;

-    private volatile bool busy;

     private volatile bool hasOutput;

     private volatile UnexpectedProverOutputException outputExn;

     private DateTime proverStart;

     private TimeSpan proverRunTime;

     private volatile ProverInterface.ErrorHandler handler;

-    private volatile bool closed;

+    private volatile CheckerStatus status;

+    public readonly Program Program;

+

+    public void GetReady()

+    {

+      Contract.Requires(status == CheckerStatus.Idle);

+

+      status = CheckerStatus.Ready;

+    }

+

+    public void GoBackToIdle()

+    {

+      Contract.Requires(IsBusy);

+

+      status = CheckerStatus.Idle;

+    }

 

     public Task ProverTask { get; set; }

 

-    public bool WillingToHandle(Implementation impl, int timeout) {

-      return !closed && timeout == this.timeout;

+    public bool WillingToHandle(int timeout, Program prog) {

+      return status == CheckerStatus.Idle && timeout == this.timeout && (prog == null || Program == prog);

     }

 

     public VCExpressionGenerator VCExprGen {

@@ -107,6 +130,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(vcgen != null);

       Contract.Requires(prog != null);

       this.timeout = timeout;

+      this.Program = prog;

 

       ProverOptions options = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();

 

@@ -195,9 +219,9 @@ namespace Microsoft.Boogie {
     /// <summary>

     /// Clean-up.

     /// </summary>

-    public void Close() {

-      this.closed = true;

+    public void Close() {      

       thmProver.Close();

+      status = CheckerStatus.Closed;

     }

 

     /// <summary>

@@ -212,13 +236,21 @@ namespace Microsoft.Boogie {
 

     public bool IsBusy {

       get {

-        return busy;

+        return status == CheckerStatus.Busy;

       }

     }

 

-    public bool Closed {

+    public bool IsClosed {

       get {

-        return closed;

+        return status == CheckerStatus.Closed;

+      }

+    }

+

+    public bool IsIdle

+    {

+      get

+      {

+        return status == CheckerStatus.Idle;

       }

     }

 

@@ -259,7 +291,6 @@ namespace Microsoft.Boogie {
           break;

       }

 

-      Contract.Assert(busy);

       hasOutput = true;

       proverRunTime = DateTime.UtcNow - proverStart;

     }

@@ -268,10 +299,9 @@ namespace Microsoft.Boogie {
       Contract.Requires(descriptiveName != null);

       Contract.Requires(vc != null);

       Contract.Requires(handler != null);

+      Contract.Requires(status == CheckerStatus.Ready);

 

-      Contract.Requires(!IsBusy);

-      Contract.Assert(!busy);

-      busy = true;

+      status = CheckerStatus.Busy;

       hasOutput = false;

       outputExn = null;

       this.handler = handler;

@@ -280,16 +310,15 @@ namespace Microsoft.Boogie {
       thmProver.BeginCheck(descriptiveName, vc, handler);

       //  gen.ClearSharedFormulas();    PR: don't know yet what to do with this guy

 

-      ProverTask = Task.Factory.StartNew(() => { WaitForOutput(null); });

+      ProverTask = Task.Factory.StartNew(() => { WaitForOutput(null); }/* , TaskCreationOptions.LongRunning*/);

     }

 

     public ProverInterface.Outcome ReadOutcome() {

-

       Contract.Requires(IsBusy);

       Contract.Requires(HasOutput);

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

+

       hasOutput = false;

-      busy = false;

 

       if (outputExn != null) {

         throw outputExn;