Use hand written custom stack size pool task scheduler

Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs

@@ -0,0 +1,73 @@
+using System;
+using System.Collections.Concurrent;
+using System.Collections.Generic;
+using System.Threading;
+using System.Threading.Tasks;
+
+namespace Microsoft.Boogie;
+
+public class CustomStackSizePoolTaskScheduler : TaskScheduler, IDisposable
+{
+  private readonly int threadCount;
+  private readonly ConcurrentQueue<Task> queue = new();
+  private readonly SemaphoreSlim isWorkAvailable = new(0);
+  private readonly Thread[] threads;
+
+  public static CustomStackSizePoolTaskScheduler Create(int stackSize, int threadCount)
+  {
+    return new CustomStackSizePoolTaskScheduler(stackSize, threadCount);
+  }
+
+  private CustomStackSizePoolTaskScheduler(int stackSize, int threadCount)
+  {
+    this.threadCount = threadCount;
+
+    threads = new Thread[this.threadCount];
+    for (int i = 0; i < threads.Length; i++)
+    {
+      threads[i] = new Thread(WorkLoop, stackSize) { IsBackground = true };
+      threads[i].Start();
+    }
+  }
+
+  protected override void QueueTask(Task task)
+  {
+    queue.Enqueue(task);
+    isWorkAvailable.Release(1);
+  }
+
+  protected override bool TryExecuteTaskInline(Task task, bool taskWasPreviouslyQueued)
+  {
+    return TryExecuteTask(task);
+  }
+
+  public override int MaximumConcurrencyLevel => threadCount;
+
+  protected override IEnumerable<Task> GetScheduledTasks()
+  {
+    return queue;
+  }
+
+  private void WorkLoop()
+  {
+    while (true)
+    {
+      var task = BlockUntilTaskIsAvailable();
+      TryExecuteTask(task);
+    }
+  }
+
+  private Task BlockUntilTaskIsAvailable()
+  {
+    isWorkAvailable.Wait();
+    queue.TryDequeue(out var task);
+    return task;
+  }
+
+  public void Dispose()
+  {
+    for (int i = 0; i < threads.Length; i++) {
+      threads[i].Join();
+    }
+  }
+}

Source/ExecutionEngine/ExecutionEngine.cs

@@ -26,14 +26,14 @@ public ProcessedProgram(Program program) : this(program, (_, _, _) => { }) {
 
   public class ExecutionEngine : IDisposable
   {
-    private static readonly WorkStealingTaskScheduler LargeThreadScheduler = new(16 * 1024 * 1024);
-    private static readonly TaskFactory LargeThreadTaskFactory = new(
+    private static readonly CustomStackSizePoolTaskScheduler largeThreadScheduler = CustomStackSizePoolTaskScheduler.Create(16 * 1024 * 1024, Environment.ProcessorCount);
+    private static readonly TaskFactory largeThreadTaskFactory = new(
       CancellationToken.None, TaskCreationOptions.DenyChildAttach,
-      TaskContinuationOptions.None, LargeThreadScheduler);
+      TaskContinuationOptions.None, largeThreadScheduler);
 
     static int autoRequestIdCount;
 
-    static readonly string AutoRequestIdPrefix = "auto_request_id_";
+    private const string AutoRequestIdPrefix = "auto_request_id_";
 
     public static string FreshRequestId() {
       var id = Interlocked.Increment(ref autoRequestIdCount);
@@ -874,7 +874,7 @@ private IObservable<IVerificationStatus> VerifyImplementationWithoutCaching(Proc
       var verificationResult = new VerificationResult(impl, programId);
 
       var batchCompleted = new Subject<(Split split, VCResult vcResult)>();
-      var completeVerification = LargeThreadTaskFactory.StartNew(async () =>
+      var completeVerification = largeThreadTaskFactory.StartNew(async () =>
       {
         var vcgen = new VCGen(processedProgram.Program, checkerPool);
         vcgen.CachingActionCounts = stats.CachingActionCounts;