diff options
| author |  qadeer <unknown> | 2014-07-30 07:55:48 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-07-30 07:55:48 -0700 |
| commit | e5e07af52dc1e27689c55ff3ff581e39b61e17b8 (patch) | |
| tree | ec8d7bc1d8718b12602be391b829d4464bb11db3 /Source/ExecutionEngine/ExecutionEngine.cs | |
| parent | 3549c8261b47aa0bd48d8d9198e5cedcabbd988e (diff) | |
removed /doNotUseParallelism
Diffstat (limited to 'Source/ExecutionEngine/ExecutionEngine.cs')
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 90 |
1 files changed, 40 insertions, 50 deletions
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)
{
|