From 3549c8261b47aa0bd48d8d9198e5cedcabbd988e Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Wed, 30 Jul 2014 15:19:46 +0200
Subject: Made it bound the number of executing tasks by the number of cores
 specified (vcsCores).

---
 Source/ExecutionEngine/ExecutionEngine.cs | 87 ++++++++++++++++++++-----------
 1 file changed, 57 insertions(+), 30 deletions(-)

(limited to 'Source')

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);
-        }
       }
     }
 
-- 
cgit v1.2.3