From e5e07af52dc1e27689c55ff3ff581e39b61e17b8 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Wed, 30 Jul 2014 07:55:48 -0700
Subject: removed /doNotUseParallelism

---
 Source/ExecutionEngine/ExecutionEngine.cs | 90 ++++++++++++++-----------------
 1 file changed, 40 insertions(+), 50 deletions(-)

(limited to 'Source/ExecutionEngine/ExecutionEngine.cs')

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index de69412e..dedb3981 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -900,67 +900,57 @@ namespace Microsoft.Boogie
 
       try
       {
-          if (CommandLineOptions.Clo.UseParallelism)
+          var cts = new CancellationTokenSource();
+          RequestIdToCancellationTokenSource.AddOrUpdate(requestId, cts, (k, ov) => cts);
+
+          var tasks = new Task[stablePrioritizedImpls.Length];
+          // 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 cts = new CancellationTokenSource();
-              RequestIdToCancellationTokenSource.AddOrUpdate(requestId, cts, (k, ov) => cts);
-
-              var tasks = new Task[stablePrioritizedImpls.Length];
-              // 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[taskIndex].Id;
+
+              CancellationTokenSource old;
+              if (ImplIdToCancellationTokenSource.TryGetValue(id, out old))
               {
-                  var taskIndex = i;
-                  var id = stablePrioritizedImpls[taskIndex].Id;
-                  
-                  CancellationTokenSource old;
-                  if (ImplIdToCancellationTokenSource.TryGetValue(id, out old))
+                  old.Cancel();
+              }
+              ImplIdToCancellationTokenSource.AddOrUpdate(id, cts, (k, ov) => cts);
+
+              var t = new Task((dummy) =>
                   {
-                      old.Cancel();
-                  }
-                  ImplIdToCancellationTokenSource.AddOrUpdate(id, cts, (k, ov) => cts);
-                  
-                  var t = new Task((dummy) =>
+                      try
                       {
-                          try
+                          if (outcome == PipelineOutcome.FatalError)
                           {
-                              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);
+                              return;
                           }
-                          finally
+                          if (cts.Token.IsCancellationRequested)
                           {
-                              semaphore.Release();
+                              cts.Token.ThrowIfCancellationRequested();
                           }
-                      }, 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);
+                          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;
           }
-          else
+
+          // Execute the tasks.
+          for (int i = 0; i < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; i++)
           {
-              for (int i = 0; i < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; i++)
-              {
-                  VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, i, outputCollector, Checkers, programId);
-              }
+              semaphore.Wait(cts.Token);
+              tasks[i].Start(TaskScheduler.Default);
           }
+
+          Task.WaitAll(tasks);
       }
       catch (AggregateException ae)
       {
-- 
cgit v1.2.3