Made it bound the number of executing tasks by the number of cores specified (vcsCores).

1 files changed, 57 insertions, 30 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index a568176b..de69412e 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -417,10 +417,9 @@ namespace Microsoft.Boogie
     

     static List<Checker> Checkers = new List<Checker>();

 

-    static IDictionary<string, CancellationTokenSource> ImplIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();

-

-    static IDictionary<string, IList<CancellationTokenSource>> RequestIdToCancellationTokenSources = new ConcurrentDictionary<string, IList<CancellationTokenSource>>();

+    static readonly ConcurrentDictionary<string, CancellationTokenSource> ImplIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();

 

+    static readonly ConcurrentDictionary<string, CancellationTokenSource> RequestIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();

 

     public static void ProcessFiles(List<string> fileNames, bool lookForSnapshots = true, string programId = null)

     {

@@ -811,8 +810,6 @@ namespace Microsoft.Boogie
         requestId = FreshRequestId();

       }

 

-      RequestIdToCancellationTokenSources[requestId] = new List<CancellationTokenSource>();

-

       #region Do some pre-abstract-interpretation preprocessing on the program

       // Doing lambda expansion before abstract interpretation means that the abstract interpreter

       // never needs to see any lambda expressions.  (On the other hand, if it were useful for it

@@ -905,30 +902,56 @@ namespace Microsoft.Boogie
       {

           if (CommandLineOptions.Clo.UseParallelism)

           {

+              var cts = new CancellationTokenSource();

+              RequestIdToCancellationTokenSource.AddOrUpdate(requestId, cts, (k, ov) => cts);

+

               var tasks = new Task[stablePrioritizedImpls.Length];

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

+              // We use this semaphore to limit the number of tasks that are currently executing.

+              var semaphore = new SemaphoreSlim(CommandLineOptions.Clo.VcsCores);

+              

+              // Create a task per implementation.

+              for (int i = 0; i < stablePrioritizedImpls.Length; i++)

               {

                   var taskIndex = i;

-                  var id = stablePrioritizedImpls[i].Id;

-                  CancellationTokenSource src;

-                  if (ImplIdToCancellationTokenSource.TryGetValue(id, out src))

+                  var id = stablePrioritizedImpls[taskIndex].Id;

+                  

+                  CancellationTokenSource old;

+                  if (ImplIdToCancellationTokenSource.TryGetValue(id, out old))

                   {

-                      src.Cancel();

+                      old.Cancel();

                   }

-                  src = new CancellationTokenSource();

-                  RequestIdToCancellationTokenSources[requestId].Add(src);

-                  ImplIdToCancellationTokenSource[id] = src;

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

-                  {

-                      if (src.Token.IsCancellationRequested)

+                  ImplIdToCancellationTokenSource.AddOrUpdate(id, cts, (k, ov) => cts);

+                  

+                  var t = new Task((dummy) =>

                       {

-                          src.Token.ThrowIfCancellationRequested();

-                      }

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

-                      ImplIdToCancellationTokenSource.Remove(id);

-                  }, src.Token, TaskCreationOptions.LongRunning);

+                          try

+                          {

+                              if (outcome == PipelineOutcome.FatalError)

+                              {

+                                  return;

+                              }

+                              if (cts.Token.IsCancellationRequested)

+                              {

+                                  cts.Token.ThrowIfCancellationRequested();

+                              }

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

+                              ImplIdToCancellationTokenSource.TryRemove(id, out old);

+                          }

+                          finally

+                          {

+                              semaphore.Release();

+                          }

+                      }, cts.Token, TaskCreationOptions.LongRunning);

                   tasks[taskIndex] = t;

               }

+

+              // Execute the tasks.

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

+              {

+                  semaphore.Wait(cts.Token);

+                  tasks[i].Start(TaskScheduler.Default);

+              }

+

               Task.WaitAll(tasks);

           }

           else

@@ -958,6 +981,9 @@ namespace Microsoft.Boogie
               return false;

           });

       }

+      catch (OperationCanceledException)

+      {

+      }

       finally

       {

         CleanupCheckers(requestId);

@@ -981,10 +1007,10 @@ namespace Microsoft.Boogie
     {

       Contract.Requires(requestId != null);

 

-      IList<CancellationTokenSource> ctss;

-      if (RequestIdToCancellationTokenSources.TryGetValue(requestId, out ctss))

+      CancellationTokenSource cts;

+      if (RequestIdToCancellationTokenSource.TryGetValue(requestId, out cts))

       {

-        ctss.Iter(cts => cts.Cancel());

+        cts.Cancel();

 

         CleanupCheckers(requestId);

       }

@@ -993,9 +1019,14 @@ namespace Microsoft.Boogie
 

     private static void CleanupCheckers(string requestId)

     {

-      lock (RequestIdToCancellationTokenSources)

+      if (requestId != null)

       {

-        if (RequestIdToCancellationTokenSources.Count == 1)

+        CancellationTokenSource old;

+        RequestIdToCancellationTokenSource.TryRemove(requestId, out old);

+      }

+      lock (RequestIdToCancellationTokenSource)

+      {

+        if (RequestIdToCancellationTokenSource.IsEmpty)

         {

           lock (Checkers)

           {

@@ -1006,10 +1037,6 @@ namespace Microsoft.Boogie
             }

           }

         }

-        if (requestId != null)

-        {

-          RequestIdToCancellationTokenSources.Remove(requestId);

-        }

       }

     }