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

10 files changed, 131 insertions, 73 deletions

diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs
index 1b78afc3..7e2ec984 100644
--- a/Source/Doomed/DoomCheck.cs
+++ b/Source/Doomed/DoomCheck.cs
@@ -121,6 +121,7 @@ void ObjectInvariant()
             

             try {

               outcome = m_Checker.ReadOutcome();

+              m_Checker.GoBackToIdle();

             } catch (UnexpectedProverOutputException e)

             {

               if (CommandLineOptions.Clo.TraceVerify) { 

diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs
index fadb2ea7..778ae767 100644
--- a/Source/Doomed/VCDoomed.cs
+++ b/Source/Doomed/VCDoomed.cs
@@ -34,8 +34,8 @@ namespace VC {
     /// <summary>

     /// Constructor.  Initializes the theorem prover.

     /// </summary>

-    public DCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)

-      : base(program) {

+    public DCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

+      : base(program, checkers) {

       Contract.Requires(program != null);

 

       this.appendLogFile = appendLogFile;

@@ -115,7 +115,7 @@ namespace VC {
 

       //Impl2Dot(impl, String.Format("c:/dot/{0}_fin.dot", impl.Name));

     

-      Checker checker = FindCheckerFor(impl, 1000);

+      Checker checker = FindCheckerFor(1000);

       Contract.Assert(checker != null);

       int assertionCount;

       DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks, out assertionCount);

@@ -173,7 +173,7 @@ namespace VC {
         if (restartTP)

         {

             checker.Close();

-            checker = FindCheckerFor(impl, 1000);

+            checker = FindCheckerFor(1000);

             dc.RespawnChecker(impl, checker);

             dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback);

         }

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index ab029cb0..71f8cee7 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -776,18 +776,19 @@ namespace Microsoft.Boogie
 

       var outputCollector = new OutputCollector(stablePrioritizedImpls);

       var outcome = PipelineOutcome.VerificationCompleted;

+      var checkers = new List<Checker>();

       var tasks = new Task[stablePrioritizedImpls.Length];

       for (int i = 0; i < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; i++)

       {

         var taskIndex = i;

         var t = Task.Factory.StartNew(() =>

         {

-          VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector);

+          VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector, checkers);

         });

         tasks[taskIndex] = t;

         try

         {

-          Task.WaitAll(new Task[] { t });

+          Task.WaitAll(t);

         }

         catch (AggregateException ae)

         {

@@ -804,6 +805,14 @@ namespace Microsoft.Boogie
           });

         }

       }

+      lock (checkers)

+      {

+        foreach (Checker checker in checkers)

+        {

+          Contract.Assert(checker != null);

+          checker.Close();

+        }

+      }

 

       cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();

 

@@ -815,7 +824,7 @@ namespace Microsoft.Boogie
     }

 

 

-    private static void VerifyImplementation(Program program, PipelineStatistics stats, ErrorReporterDelegate er, string requestId, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo, Implementation[] stablePrioritizedImpls, int index, OutputCollector outputCollector)

+    private static void VerifyImplementation(Program program, PipelineStatistics stats, ErrorReporterDelegate er, string requestId, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo, Implementation[] stablePrioritizedImpls, int index, OutputCollector outputCollector, List<Checker> checkers)

     {

       Implementation impl = stablePrioritizedImpls[index];

       VerificationResult verificationResult = null;

@@ -846,7 +855,7 @@ namespace Microsoft.Boogie
         verificationResult.ImplementationName = impl.Name;

         verificationResult.ImplementationToken = impl.tok;

 

-        using (var vcgen = CreateVCGen(program))

+        using (var vcgen = CreateVCGen(program, checkers))

         {

           verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;

           verificationResult.Start = DateTime.UtcNow;

@@ -987,24 +996,24 @@ namespace Microsoft.Boogie
     }

 

 

-    private static ConditionGeneration CreateVCGen(Program program)

+    private static ConditionGeneration CreateVCGen(Program program, List<Checker> checkers)

     {

       ConditionGeneration vcgen = null;

       if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)

       {

-        vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+        vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);

       }

       else if (CommandLineOptions.Clo.FixedPointEngine != null)

       {

-        vcgen = new FixedpointVC(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+        vcgen = new FixedpointVC(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);

       }

       else if (CommandLineOptions.Clo.StratifiedInlining > 0)

       {

-        vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+        vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);

       }

       else

       {

-        vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+        vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);

       }

       return vcgen;

     }

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index a9fae923..24a3c708 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -98,7 +98,7 @@ namespace Microsoft.Boogie.Houdini {
 

             Inline();

 

-            this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+            this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());

             this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1);

 

             this.proverTime = TimeSpan.Zero;

@@ -2053,7 +2053,7 @@ namespace Microsoft.Boogie.Houdini {
             if (CommandLineOptions.Clo.ProverKillTime > 0)

                 CommandLineOptions.Clo.ProverOptions.Add(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime));

 

-            this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+            this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());

             this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1);

 

             this.reporter = new AbstractHoudiniErrorReporter();

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 4dd985b4..abc5a7e8 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -349,7 +349,7 @@ namespace Microsoft.Boogie.Houdini {
 

       Inline();

 

-      this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+      this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());

       this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);

 

       vcgenFailures = new HashSet<Implementation>();

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;

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index bb2deb29..2fe32500 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -527,8 +527,8 @@ namespace VC {
       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       throw new NotImplementedException();

     }

-    public ConditionGenerationContracts(Program p)

-      : base(p) {

+    public ConditionGenerationContracts(Program p, List<Checker> checkers)

+      : base(p, checkers) {

     }

   }

 

@@ -570,7 +570,7 @@ namespace VC {
 

     public int CumulativeAssertionCount;  // for statistics

 

-    protected readonly List<Checker>/*!>!*/ checkers = new List<Checker>();

+    protected readonly List<Checker>/*!>!*/ checkers;

 

     private bool _disposed;

 

@@ -586,9 +586,10 @@ namespace VC {
 

     public static List<Model> errorModelList;

 

-    public ConditionGeneration(Program p) {

-      Contract.Requires(p != null);

+    public ConditionGeneration(Program p, List<Checker> checkers) {

+      Contract.Requires(p != null && checkers != null && cce.NonNullElements(checkers));

       program = p;

+      this.checkers = checkers;

     }

 

     /// <summary>

@@ -970,42 +971,57 @@ namespace VC {
     #endregion

 

 

-    protected Checker FindCheckerFor(Implementation impl, int timeout)

+    protected Checker FindCheckerFor(int timeout)

     {

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

 

-      // Look for existing checker.

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

+      lock (checkers)

       {

-        if (checkers[i].Closed)

+      retry:

+        // Look for existing checker.

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

         {

-          checkers.RemoveAt(i);

-          continue;

+          var c = checkers.ElementAt(i);

+          lock (c)

+          {

+            if (c.WillingToHandle(timeout, program))

+            {

+              c.GetReady();

+              return c;

+            }

+            else if (c.IsIdle || c.IsClosed)

+            {

+              checkers.RemoveAt(i);

+              if (c.IsIdle)

+              {

+                c.Close();

+              }

+              continue;

+            }

+          }

         }

-        if (!checkers[i].IsBusy && checkers[i].WillingToHandle(impl, timeout))

+

+        if (1 < checkers.Count)

         {

-          return checkers[i];

+          Monitor.Wait(checkers, 50);

+          goto retry;

         }

-      }

 

-      // Create a new checker.

-      string log = logFilePath;

-      if (log != null && !log.Contains("@PROC@") && checkers.Count > 0)

-      {

-        log = log + "." + checkers.Count;

-      }

-      Checker ch = new Checker(this, program, log, appendLogFile, timeout);

-      Contract.Assert(ch != null);

-      checkers.Add(ch);

-      return ch;

+        // Create a new checker.

+        string log = logFilePath;

+        if (log != null && !log.Contains("@PROC@") && checkers.Count > 0)

+        {

+          log = log + "." + checkers.Count;

+        }

+        Checker ch = new Checker(this, program, log, appendLogFile, timeout);

+        ch.GetReady();

+        checkers.Add(ch);

+        return ch;

+      }      

     }

 

 

     virtual public void Close() {

-      foreach (Checker checker in checkers) {

-        Contract.Assert(checker != null);

-        checker.Close();

-      }

     }

 

 

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 19feabe9..3299ef76 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -78,8 +78,8 @@ namespace Microsoft.Boogie
 

         private static Checker old_checker = null;

 

-        public FixedpointVC( Program _program, string/*?*/ logFilePath, bool appendLogFile)

-            : base(_program, logFilePath, appendLogFile) 

+        public FixedpointVC( Program _program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

+            : base(_program, logFilePath, appendLogFile, checkers) 

         {

             switch (CommandLineOptions.Clo.FixedPointMode)

             {

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 9e0dd798..b4db817f 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -309,8 +309,8 @@ namespace VC {
     public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;

     public ProverInterface prover;

 

-    public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile)

-      : base(program, logFilePath, appendLogFile) {

+    public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

+      : base(program, logFilePath, appendLogFile, checkers) {

       implName2StratifiedInliningInfo = new Dictionary<string, StratifiedInliningInfo>();

       prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);

       foreach (Declaration decl in program.TopLevelDeclarations) {

@@ -510,8 +510,8 @@ namespace VC {
 

     public StratifiedVCGen(bool usePrevCallTree, Dictionary<string, int> prevCallTree, 

                            HashSet<string> procsToSkip, Dictionary<string, int> extraRecBound,

-                           Program program, string/*?*/ logFilePath, bool appendLogFile) 

-    : this(program, logFilePath, appendLogFile)

+                           Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers) 

+    : this(program, logFilePath, appendLogFile, checkers)

     {

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

       this.extraRecBound = new Dictionary<string, int>(extraRecBound);

@@ -525,8 +525,8 @@ namespace VC {
       }

     }

 

-    public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)

-      : base(program, logFilePath, appendLogFile) {

+    public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

+      : base(program, logFilePath, appendLogFile, checkers) {

       PersistCallTree = false;

       useSummary = false;

       procsThatReachedRecBound = new HashSet<string>();

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 121cab46..fdadafac 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -26,8 +26,8 @@ namespace VC {
     /// Constructor.  Initializes the theorem prover.

     /// </summary>

     [NotDelayed]

-    public VCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)

-      : base(program)

+    public VCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

+      : base(program, checkers)

     {

       Contract.Requires(program != null);

       this.appendLogFile = appendLogFile;

@@ -291,7 +291,7 @@ namespace VC {
         ModelViewInfo mvInfo;

         parent.PassifyImpl(impl, out mvInfo);

         Hashtable label2Absy;

-        Checker ch = parent.FindCheckerFor(impl, CommandLineOptions.Clo.SmokeTimeout);

+        Checker ch = parent.FindCheckerFor(CommandLineOptions.Clo.SmokeTimeout);

         Contract.Assert(ch != null);

 

         var exprGen = ch.TheoremProver.Context.ExprGen;

@@ -315,6 +315,7 @@ namespace VC {
         ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));

         ch.ProverTask.Wait();

         ProverInterface.Outcome outcome = ch.ReadOutcome();

+        ch.GoBackToIdle();

         parent.CurrentLocalVariables = null;

 

         DateTime end = DateTime.UtcNow;

@@ -1192,7 +1193,7 @@ namespace VC {
 

         impl.Blocks = blocks;

 

-        checker = parent.FindCheckerFor(impl, timeout);

+        checker = parent.FindCheckerFor(timeout);

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

 

         ProverInterface tp = checker.TheoremProver;

@@ -1201,7 +1202,7 @@ namespace VC {
         bet.SetCodeExprConverter(

           new CodeExprConverter(

           delegate (CodeExpr codeExpr, Hashtable/*<Block, VCExprVar!>*/ blockVariables, List<VCExprLetBinding/*!*/> bindings) {

-            VCGen vcgen = new VCGen(new Program(), null, false);

+            VCGen vcgen = new VCGen(new Program(), null, false, parent.checkers);

             vcgen.variable2SequenceNumber = new Hashtable/*Variable -> int*/();

             vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();

             vcgen.CurrentLocalVariables = codeExpr.LocVars;

@@ -1507,6 +1508,8 @@ namespace VC {
             break;

           }

 

+          s.Checker.GoBackToIdle();

+

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

         }