From 29befa8c6b21184e2d8d8d2f5dd464f0e30ff762 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 29 Mar 2023 17:41:10 +0200
Subject: [PATCH 1/9] Use large threads for processing Boogie programs

---
 Source/ExecutionEngine/ExecutionEngine.cs     |  12 +-
 Source/ExecutionEngine/WorkStealingQueue.cs   | 219 +++++++++++++
 .../WorkStealingTaskScheduler.cs              | 303 ++++++++++++++++++
 3 files changed, 530 insertions(+), 4 deletions(-)
 create mode 100644 Source/ExecutionEngine/WorkStealingQueue.cs
 create mode 100644 Source/ExecutionEngine/WorkStealingTaskScheduler.cs

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index dbe4ecdf7..7d3b308f0 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -10,7 +10,6 @@
 using BoogiePL = Microsoft.Boogie;
 using System.Runtime.Caching;
 using System.Diagnostics;
-using System.Runtime.CompilerServices;
 using VCGeneration;
 
 namespace Microsoft.Boogie
@@ -20,7 +19,12 @@ public ProcessedProgram(Program program) : this(program, (_, _, _) => { }) {
     }
   }
 
-  public class ExecutionEngine : IDisposable {
+  public class ExecutionEngine : IDisposable
+  {
+    private static readonly WorkStealingTaskScheduler LargeThreadScheduler = new(16 * 1024 * 1024);
+    private static readonly TaskFactory LargeThreadTaskFactory = new(
+      CancellationToken.None, TaskCreationOptions.DenyChildAttach,
+      TaskContinuationOptions.None, LargeThreadScheduler);
 
     static int autoRequestIdCount;
 
@@ -731,9 +735,9 @@ public async Task<Task<VerificationResult>> EnqueueVerifyImplementation(
 
       await verifyImplementationSemaphore.WaitAsync(cancellationToken);
 
-      var coreTask = Task.Run(() => VerifyImplementation(processedProgram, stats, er, cancellationToken,
+      var coreTask = LargeThreadTaskFactory.StartNew(() => VerifyImplementation(processedProgram, stats, er, cancellationToken,
         implementation,
-        programId, taskWriter), cancellationToken);
+        programId, taskWriter), cancellationToken).Unwrap();
 
       var _ = coreTask.ContinueWith(t => {
         verifyImplementationSemaphore.Release();
diff --git a/Source/ExecutionEngine/WorkStealingQueue.cs b/Source/ExecutionEngine/WorkStealingQueue.cs
new file mode 100644
index 000000000..807d4227c
--- /dev/null
+++ b/Source/ExecutionEngine/WorkStealingQueue.cs
@@ -0,0 +1,219 @@
+using System.Collections.Generic;
+using System.Threading;
+
+namespace Microsoft.Boogie; 
+
+/// <summary>A work-stealing queue.</summary>
+/// <typeparam name="T">Specifies the type of data stored in the queue.</typeparam>
+internal class WorkStealingQueue<T> where T : class
+{
+    private const int INITIAL_SIZE = 32;
+    private T[] m_array = new T[INITIAL_SIZE];
+    private int m_mask = INITIAL_SIZE - 1;
+    private volatile int m_headIndex = 0;
+    private volatile int m_tailIndex = 0;
+
+    private object m_foreignLock = new object();
+
+    internal void LocalPush(T obj)
+    {
+        int tail = m_tailIndex;
+
+        // When there are at least 2 elements' worth of space, we can take the fast path.
+        if (tail < m_headIndex + m_mask)
+        {
+            m_array[tail & m_mask] = obj;
+            m_tailIndex = tail + 1;
+        }
+        else
+        {
+            // We need to contend with foreign pops, so we lock.
+            lock (m_foreignLock)
+            {
+                int head = m_headIndex;
+                int count = m_tailIndex - m_headIndex;
+
+                // If there is still space (one left), just add the element.
+                if (count >= m_mask)
+                {
+                    // We're full; expand the queue by doubling its size.
+                    T[] newArray = new T[m_array.Length << 1];
+                    for (int i = 0; i < m_array.Length; i++) {
+                      newArray[i] = m_array[(i + head) & m_mask];
+                    }
+
+                    // Reset the field values, incl. the mask.
+                    m_array = newArray;
+                    m_headIndex = 0;
+                    m_tailIndex = tail = count;
+                    m_mask = (m_mask << 1) | 1;
+                }
+
+                m_array[tail & m_mask] = obj;
+                m_tailIndex = tail + 1;
+            }
+        }
+    }
+
+    internal bool LocalPop(ref T obj)
+    {
+        while (true)
+        {
+            // Decrement the tail using a fence to ensure subsequent read doesn't come before.
+            int tail = m_tailIndex;
+            if (m_headIndex >= tail)
+            {
+                obj = null;
+                return false;
+            }
+
+            tail -= 1;
+#pragma warning disable 0420
+            Interlocked.Exchange(ref m_tailIndex, tail);
+#pragma warning restore 0420
+
+            // If there is no interaction with a take, we can head down the fast path.
+            if (m_headIndex <= tail)
+            {
+                int idx = tail & m_mask;
+                obj = m_array[idx];
+
+                // Check for nulls in the array.
+                if (obj == null) {
+                  continue;
+                }
+
+                m_array[idx] = null;
+                return true;
+            }
+            else
+            {
+                // Interaction with takes: 0 or 1 elements left.
+                lock (m_foreignLock)
+                {
+                    if (m_headIndex <= tail)
+                    {
+                        // Element still available. Take it.
+                        int idx = tail & m_mask;
+                        obj = m_array[idx];
+
+                        // Check for nulls in the array.
+                        if (obj == null) {
+                          continue;
+                        }
+
+                        m_array[idx] = null;
+                        return true;
+                    }
+                    else
+                    {
+                        // We lost the race, element was stolen, restore the tail.
+                        m_tailIndex = tail + 1;
+                        obj = null;
+                        return false;
+                    }
+                }
+            }
+        }
+    }
+
+    internal bool TrySteal(ref T obj)
+    {
+        obj = null;
+
+        while (true)
+        {
+            if (m_headIndex >= m_tailIndex) {
+              return false;
+            }
+
+            lock (m_foreignLock)
+            {
+                // Increment head, and ensure read of tail doesn't move before it (fence).
+                int head = m_headIndex;
+#pragma warning disable 0420
+                Interlocked.Exchange(ref m_headIndex, head + 1);
+#pragma warning restore 0420
+
+                if (head < m_tailIndex)
+                {
+                    int idx = head & m_mask;
+                    obj = m_array[idx];
+
+                    // Check for nulls in the array.
+                    if (obj == null) {
+                      continue;
+                    }
+
+                    m_array[idx] = null;
+                    return true;
+                }
+                else
+                {
+                    // Failed, restore head.
+                    m_headIndex = head;
+                    obj = null;
+                }
+            }
+
+            return false;
+        }
+    }
+
+    internal bool TryFindAndPop(T obj)
+    {
+        // We do an O(N) search for the work item. The theory of work stealing and our
+        // inlining logic is that most waits will happen on recently queued work.  And
+        // since recently queued work will be close to the tail end (which is where we
+        // begin our search), we will likely find it quickly.  In the worst case, we
+        // will traverse the whole local queue; this is typically not going to be a
+        // problem (although degenerate cases are clearly an issue) because local work
+        // queues tend to be somewhat shallow in length, and because if we fail to find
+        // the work item, we are about to block anyway (which is very expensive).
+
+        for (int i = m_tailIndex - 1; i >= m_headIndex; i--)
+        {
+            if (m_array[i & m_mask] == obj)
+            {
+                // If we found the element, block out steals to avoid interference.
+                lock (m_foreignLock)
+                {
+                    // If we lost the race, bail.
+                    if (m_array[i & m_mask] == null)
+                    {
+                        return false;
+                    }
+
+                    // Otherwise, null out the element.
+                    m_array[i & m_mask] = null;
+
+                    // And then check to see if we can fix up the indexes (if we're at
+                    // the edge).  If we can't, we just leave nulls in the array and they'll
+                    // get filtered out eventually (but may lead to superflous resizing).
+                    if (i == m_tailIndex) {
+                      m_tailIndex -= 1;
+                    } else if (i == m_headIndex) {
+                      m_headIndex += 1;
+                    }
+
+                    return true;
+                }
+            }
+        }
+
+        return false;
+    }
+
+    internal T[] ToArray()
+    {
+        List<T> list = new List<T>();
+        for (int i = m_tailIndex - 1; i >= m_headIndex; i--)
+        {
+            T obj = m_array[i & m_mask];
+            if (obj != null) {
+              list.Add(obj);
+            }
+        }
+        return list.ToArray();
+    }
+}
\ No newline at end of file
diff --git a/Source/ExecutionEngine/WorkStealingTaskScheduler.cs b/Source/ExecutionEngine/WorkStealingTaskScheduler.cs
new file mode 100644
index 000000000..48d074a70
--- /dev/null
+++ b/Source/ExecutionEngine/WorkStealingTaskScheduler.cs
@@ -0,0 +1,303 @@
+using System;
+using System.Collections.Generic;
+using System.Threading;
+using System.Threading.Tasks;
+
+namespace Microsoft.Boogie;
+
+/// <summary>Provides a work-stealing scheduler.</summary>
+public class WorkStealingTaskScheduler : TaskScheduler, IDisposable
+{
+  private readonly int stackSize;
+  private readonly int m_concurrencyLevel;
+  private readonly Queue<Task> m_queue = new Queue<Task>();
+  private WorkStealingQueue<Task>[] m_wsQueues = new WorkStealingQueue<Task>[Environment.ProcessorCount];
+  private Lazy<Thread[]> m_threads;
+  private int m_threadsWaiting;
+  private bool m_shutdown;
+  [ThreadStatic]
+  private static WorkStealingQueue<Task> m_wsq;
+
+  /// <summary>Initializes a new instance of the WorkStealingTaskScheduler class.</summary>
+  /// <remarks>This constructors defaults to using twice as many threads as there are processors.</remarks>
+  public WorkStealingTaskScheduler(int stackSize) : this(stackSize, Environment.ProcessorCount * 2) { }
+
+  /// <summary>Initializes a new instance of the WorkStealingTaskScheduler class.</summary>
+  /// <param name="concurrencyLevel">The number of threads to use in the scheduler.</param>
+  public WorkStealingTaskScheduler(int stackSize, int concurrencyLevel)
+  {
+    // Store the concurrency level
+    if (concurrencyLevel <= 0) {
+      throw new ArgumentOutOfRangeException("concurrencyLevel");
+    }
+
+    this.stackSize = stackSize;
+    m_concurrencyLevel = concurrencyLevel;
+
+    // Set up threads
+    m_threads = new Lazy<Thread[]>(() =>
+    {
+      var threads = new Thread[m_concurrencyLevel];
+      for (int i = 0; i < threads.Length; i++)
+      {
+        threads[i] = new Thread(DispatchLoop, stackSize) { IsBackground = true };
+        threads[i].Start();
+      }
+      return threads;
+    });
+  }
+
+  /// <summary>Queues a task to the scheduler.</summary>
+  /// <param name="task">The task to be scheduled.</param>
+  protected override void QueueTask(Task task)
+  {
+    // Make sure the pool is started, e.g. that all threads have been created.
+    var threads = m_threads.Value;
+
+    // If the task is marked as long-running, give it its own dedicated thread
+    // rather than queueing it.
+    if ((task.CreationOptions & TaskCreationOptions.LongRunning) != 0)
+    {
+      new Thread(state => base.TryExecuteTask((Task)state)) { IsBackground = true }.Start(task);
+    }
+    else
+    {
+      // Otherwise, insert the work item into a queue, possibly waking a thread.
+      // If there's a local queue and the task does not prefer to be in the global queue,
+      // add it to the local queue.
+      WorkStealingQueue<Task> wsq = m_wsq;
+      if (wsq != null && ((task.CreationOptions & TaskCreationOptions.PreferFairness) == 0))
+      {
+        // Add to the local queue and notify any waiting threads that work is available.
+        // Races may occur which result in missed event notifications, but they're benign in that
+        // this thread will eventually pick up the work item anyway, as will other threads when another
+        // work item notification is received.
+        wsq.LocalPush(task);
+        if (m_threadsWaiting > 0) // OK to read lock-free.
+        {
+          lock (m_queue) { Monitor.Pulse(m_queue); }
+        }
+      }
+      // Otherwise, add the work item to the global queue
+      else
+      {
+        lock (m_queue)
+        {
+          m_queue.Enqueue(task);
+          if (m_threadsWaiting > 0) {
+            Monitor.Pulse(m_queue);
+          }
+        }
+      }
+    }
+  }
+
+  /// <summary>Executes a task on the current thread.</summary>
+  /// <param name="task">The task to be executed.</param>
+  /// <param name="taskWasPreviouslyQueued">Ignored.</param>
+  /// <returns>Whether the task could be executed.</returns>
+  protected override bool TryExecuteTaskInline(Task task, bool taskWasPreviouslyQueued)
+  {
+    return TryExecuteTask(task);
+
+    // // Optional replacement: Instead of always trying to execute the task (which could
+    // // benignly leave a task in the queue that's already been executed), we
+    // // can search the current work-stealing queue and remove the task,
+    // // executing it inline only if it's found.
+    // WorkStealingQueue<Task> wsq = m_wsq;
+    // return wsq != null && wsq.TryFindAndPop(task) && TryExecuteTask(task);
+  }
+
+  /// <summary>Gets the maximum concurrency level supported by this scheduler.</summary>
+  public override int MaximumConcurrencyLevel
+  {
+    get { return m_concurrencyLevel; }
+  }
+
+  /// <summary>Gets all of the tasks currently scheduled to this scheduler.</summary>
+  /// <returns>An enumerable containing all of the scheduled tasks.</returns>
+  protected override IEnumerable<Task> GetScheduledTasks()
+  {
+    // Keep track of all of the tasks we find
+    List<Task> tasks = new List<Task>();
+
+    // Get all of the global tasks.  We use TryEnter so as not to hang
+    // a debugger if the lock is held by a frozen thread.
+    bool lockTaken = false;
+    try
+    {
+      Monitor.TryEnter(m_queue, ref lockTaken);
+      if (lockTaken) {
+        tasks.AddRange(m_queue.ToArray());
+      } else {
+        throw new NotSupportedException();
+      }
+    }
+    finally
+    {
+      if (lockTaken) {
+        Monitor.Exit(m_queue);
+      }
+    }
+
+    // Now get all of the tasks from the work-stealing queues
+    WorkStealingQueue<Task>[] queues = m_wsQueues;
+    for (int i = 0; i < queues.Length; i++)
+    {
+      WorkStealingQueue<Task> wsq = queues[i];
+      if (wsq != null) {
+        tasks.AddRange(wsq.ToArray());
+      }
+    }
+
+    // Return to the debugger all of the collected task instances
+    return tasks;
+  }
+
+  /// <summary>Adds a work-stealing queue to the set of queues.</summary>
+  /// <param name="wsq">The queue to be added.</param>
+  private void AddWsq(WorkStealingQueue<Task> wsq)
+  {
+    lock (m_wsQueues)
+    {
+      // Find the next open slot in the array. If we find one,
+      // store the queue and we're done.
+      int i;
+      for (i = 0; i < m_wsQueues.Length; i++)
+      {
+        if (m_wsQueues[i] == null)
+        {
+          m_wsQueues[i] = wsq;
+          return;
+        }
+      }
+
+      // We couldn't find an open slot, so double the length 
+      // of the array by creating a new one, copying over,
+      // and storing the new one. Here, i == m_wsQueues.Length.
+      WorkStealingQueue<Task>[] queues = new WorkStealingQueue<Task>[i * 2];
+      Array.Copy(m_wsQueues, queues, i);
+      queues[i] = wsq;
+      m_wsQueues = queues;
+    }
+  }
+
+  /// <summary>Remove a work-stealing queue from the set of queues.</summary>
+  /// <param name="wsq">The work-stealing queue to remove.</param>
+  private void RemoveWsq(WorkStealingQueue<Task> wsq)
+  {
+    lock (m_wsQueues)
+    {
+      // Find the queue, and if/when we find it, null out its array slot
+      for (int i = 0; i < m_wsQueues.Length; i++)
+      {
+        if (m_wsQueues[i] == wsq)
+        {
+          m_wsQueues[i] = null;
+        }
+      }
+    }
+  }
+
+  /// <summary>
+  /// The dispatch loop run by each thread in the scheduler.
+  /// </summary>
+  private void DispatchLoop()
+  {
+    // Create a new queue for this thread, store it in TLS for later retrieval,
+    // and add it to the set of queues for this scheduler.
+    WorkStealingQueue<Task> wsq = new WorkStealingQueue<Task>();
+    m_wsq = wsq;
+    AddWsq(wsq);
+
+    try
+    {
+      // Until there's no more work to do...
+      while (true)
+      {
+        Task wi = null;
+
+        // Search order: (1) local WSQ, (2) global Q, (3) steals from other queues.
+        if (!wsq.LocalPop(ref wi))
+        {
+          // We weren't able to get a task from the local WSQ
+          bool searchedForSteals = false;
+          while (true)
+          {
+            lock (m_queue)
+            {
+              // If shutdown was requested, exit the thread.
+              if (m_shutdown) {
+                return;
+              }
+
+              // (2) try the global queue.
+              if (m_queue.Count != 0)
+              {
+                // We found a work item! Grab it ...
+                wi = m_queue.Dequeue();
+                break;
+              }
+              else if (searchedForSteals)
+              {
+                // Note that we're not waiting for work, and then wait
+                m_threadsWaiting++;
+                try { Monitor.Wait(m_queue); }
+                finally { m_threadsWaiting--; }
+
+                // If we were signaled due to shutdown, exit the thread.
+                if (m_shutdown) {
+                  return;
+                }
+
+                searchedForSteals = false;
+                continue;
+              }
+            }
+
+            // (3) try to steal.
+            WorkStealingQueue<Task>[] wsQueues = m_wsQueues;
+            int i;
+            for (i = 0; i < wsQueues.Length; i++)
+            {
+              WorkStealingQueue<Task> q = wsQueues[i];
+              if (q != null && q != wsq && q.TrySteal(ref wi)) {
+                break;
+              }
+            }
+
+            if (i != wsQueues.Length) {
+              break;
+            }
+
+            searchedForSteals = true;
+          }
+        }
+
+        // ...and Invoke it.
+        TryExecuteTask(wi);
+      }
+    }
+    finally
+    {
+      RemoveWsq(wsq);
+    }
+  }
+
+  /// <summary>Signal the scheduler to shutdown and wait for all threads to finish.</summary>
+  public void Dispose()
+  {
+    m_shutdown = true;
+    if (m_queue != null && m_threads.IsValueCreated)
+    {
+      var threads = m_threads.Value;
+      lock (m_queue) {
+        Monitor.PulseAll(m_queue);
+      }
+
+      for (int i = 0; i < threads.Length; i++) {
+        threads[i].Join();
+      }
+    }
+  }
+}
\ No newline at end of file

From fa566bf0e397fc7f0fd8a5457b31a1ab8dcecb96 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 29 Mar 2023 19:25:42 +0200
Subject: [PATCH 2/9] Update nesting expect file to trigger stack overflow

---
 Test/stackoverflow/nesting.bpl        | 42 +++++++++++++++++++++++++++
 Test/stackoverflow/nesting.bpl.expect | 36 +++++++++++------------
 2 files changed, 60 insertions(+), 18 deletions(-)

diff --git a/Test/stackoverflow/nesting.bpl b/Test/stackoverflow/nesting.bpl
index 2178a6045..108e20d22 100644
--- a/Test/stackoverflow/nesting.bpl
+++ b/Test/stackoverflow/nesting.bpl
@@ -1,5 +1,10 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
+
+type Ref;
+type Field A B;
+type HeapType = <A, B> [Ref, Field A B]B;
+
 procedure foo(n: int)
   requires true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true
   || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true ||
@@ -14,6 +19,43 @@ procedure foo(n: int)
           true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true
             || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true ||
             n == 2;
+  requires true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+  ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+  true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+    ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+    true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+      ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+      true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+        ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+        true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+          ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+          true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+            ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+            ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+              ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+              true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                  ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                  true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                    ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                    true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                      ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                      true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                        ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                        ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                          ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                          true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                            ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                            true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                              ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                              true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                                ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                                true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                                  ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==>
+                                  true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true
+                                    ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true ==> true;
+                                    
 {
   if (n == 2) {
     if (n == 2) {
diff --git a/Test/stackoverflow/nesting.bpl.expect b/Test/stackoverflow/nesting.bpl.expect
index 5e5ed1ea9..50f0657eb 100644
--- a/Test/stackoverflow/nesting.bpl.expect
+++ b/Test/stackoverflow/nesting.bpl.expect
@@ -1,21 +1,21 @@
-nesting.bpl(46,35): Error: this assertion could not be proved
+nesting.bpl(88,35): Error: this assertion could not be proved
 Execution trace:
-    nesting.bpl(18,3): anon0
-    nesting.bpl(19,5): anon17_Then
-    nesting.bpl(20,7): anon18_Then
-    nesting.bpl(21,9): anon19_Then
-    nesting.bpl(22,11): anon20_Then
-    nesting.bpl(23,13): anon21_Then
-    nesting.bpl(24,15): anon22_Then
-    nesting.bpl(25,17): anon23_Then
-    nesting.bpl(26,19): anon24_Then
-    nesting.bpl(27,21): anon25_Then
-    nesting.bpl(28,23): anon26_Then
-    nesting.bpl(29,25): anon27_Then
-    nesting.bpl(30,27): anon28_Then
-    nesting.bpl(31,29): anon29_Then
-    nesting.bpl(32,31): anon30_Then
-    nesting.bpl(33,33): anon31_Then
-    nesting.bpl(46,35): anon32_Then
+    nesting.bpl(60,3): anon0
+    nesting.bpl(61,5): anon17_Then
+    nesting.bpl(62,7): anon18_Then
+    nesting.bpl(63,9): anon19_Then
+    nesting.bpl(64,11): anon20_Then
+    nesting.bpl(65,13): anon21_Then
+    nesting.bpl(66,15): anon22_Then
+    nesting.bpl(67,17): anon23_Then
+    nesting.bpl(68,19): anon24_Then
+    nesting.bpl(69,21): anon25_Then
+    nesting.bpl(70,23): anon26_Then
+    nesting.bpl(71,25): anon27_Then
+    nesting.bpl(72,27): anon28_Then
+    nesting.bpl(73,29): anon29_Then
+    nesting.bpl(74,31): anon30_Then
+    nesting.bpl(75,33): anon31_Then
+    nesting.bpl(88,35): anon32_Then
 
 Boogie program verifier finished with 0 verified, 1 error

From bf9e6738670260a818ada9d9f8330e90f2350a4b Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 29 Mar 2023 19:26:02 +0200
Subject: [PATCH 3/9] Update Boogie version

---
 Source/Directory.Build.props | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
index 397fe202f..48ce71ff3 100644
--- a/Source/Directory.Build.props
+++ b/Source/Directory.Build.props
@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>2.16.3</Version>
+    <Version>2.16.4</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

From d8783c016ed8ffd4cee93688846508ba3dddefd5 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 29 Mar 2023 19:27:52 +0200
Subject: [PATCH 4/9] Add comment to test file

---
 Test/stackoverflow/nesting.bpl | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Test/stackoverflow/nesting.bpl b/Test/stackoverflow/nesting.bpl
index 108e20d22..cf4c9f020 100644
--- a/Test/stackoverflow/nesting.bpl
+++ b/Test/stackoverflow/nesting.bpl
@@ -3,7 +3,7 @@
 
 type Ref;
 type Field A B;
-type HeapType = <A, B> [Ref, Field A B]B;
+type HeapType = <A, B> [Ref, Field A B]B; // Using type parameters and the ==> operator can trigger the OpTypeEraser visitor which can cause stack overflows.
 
 procedure foo(n: int)
   requires true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true || true

From 9e8fc99e0f46955c1e497beb56539a78caee13d1 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 29 Mar 2023 19:30:36 +0200
Subject: [PATCH 5/9] Add license and attribution

---
 .../WorkStealingTaskScheduler.cs              | 22 +++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/Source/ExecutionEngine/WorkStealingTaskScheduler.cs b/Source/ExecutionEngine/WorkStealingTaskScheduler.cs
index 48d074a70..23ff1ae4f 100644
--- a/Source/ExecutionEngine/WorkStealingTaskScheduler.cs
+++ b/Source/ExecutionEngine/WorkStealingTaskScheduler.cs
@@ -1,3 +1,25 @@
+// Code taken from https://github.com/ChadBurggraf/parallel-extensions-extras/blob/ec803e58eee28c698e44f55f49c5ad6671b1aa58/TaskSchedulers/WorkStealingTaskScheduler.cs
+//
+// This license governs use of code marked as “sample” or “example” available on this web site without a license agreement, as provided under the section above titled “NOTICE SPECIFIC TO SOFTWARE AVAILABLE ON THIS WEB SITE.” If you use such code (the “software”), you accept this license. If you do not accept the license, do not use the software.
+//
+// 1. Definitions
+// The terms “reproduce,” “reproduction,” “derivative works,” and “distribution” have the same meaning here as under U.S. copyright law.
+// A “contribution” is the original software, or any additions or changes to the software.
+// A “contributor” is any person that distributes its contribution under this license.
+// “Licensed patents” are a contributor’s patent claims that read directly on its contribution.
+//
+// 2. Grant of Rights
+// (A) Copyright Grant - Subject to the terms of this license, including the license conditions and limitations in section 3, each contributor grants you a non-exclusive, worldwide, royalty-free copyright license to reproduce its contribution, prepare derivative works of its contribution, and distribute its contribution or any derivative works that you create.
+// (B) Patent Grant - Subject to the terms of this license, including the license conditions and limitations in section 3, each contributor grants you a non-exclusive, worldwide, royalty-free license under its licensed patents to make, have made, use, sell, offer for sale, import, and/or otherwise dispose of its contribution in the software or derivative works of the contribution in the software.
+//
+// 3. Conditions and Limitations
+// (A) No Trademark License- This license does not grant you rights to use any contributors’ name, logo, or trademarks.
+// (B) If you bring a patent claim against any contributor over patents that you claim are infringed by the software, your patent license from such contributor to the software ends automatically.
+// (C) If you distribute any portion of the software, you must retain all copyright, patent, trademark, and attribution notices that are present in the software.
+// (D) If you distribute any portion of the software in source code form, you may do so only under this license by including a complete copy of this license with your distribution. If you distribute any portion of the software in compiled or object code form, you may only do so under a license that complies with this license.
+// (E) The software is licensed “as-is.” You bear the risk of using it. The contributors give no express warranties, guarantees or conditions. You may have additional consumer rights under your local laws which this license cannot change. To the extent permitted under your local laws, the contributors exclude the implied warranties of merchantability, fitness for a particular purpose and non-infringement.
+// (F) Platform Limitation - The licenses granted in sections 2(A) and 2(B) extend only to the software or derivative works that you create that run directly on a Microsoft Windows operating system product, Microsoft run-time technology (such as the .NET Framework or Silverlight), or Microsoft application platform (such as Microsoft Office or Microsoft Dynamics).
+
 using System;
 using System.Collections.Generic;
 using System.Threading;

From 1aab6f69f3795f1676af5f0af66c1496632fbe89 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 30 Mar 2023 10:36:56 +0200
Subject: [PATCH 6/9] Use hand written custom stack size pool task scheduler

---
 .../CustomStackSizePoolTaskScheduler.cs       |  73 ++++
 Source/ExecutionEngine/ExecutionEngine.cs     |  10 +-
 Source/ExecutionEngine/WorkStealingQueue.cs   | 219 ------------
 .../WorkStealingTaskScheduler.cs              | 325 ------------------
 4 files changed, 78 insertions(+), 549 deletions(-)
 create mode 100644 Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs
 delete mode 100644 Source/ExecutionEngine/WorkStealingQueue.cs
 delete mode 100644 Source/ExecutionEngine/WorkStealingTaskScheduler.cs

diff --git a/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs
new file mode 100644
index 000000000..7a0330f9f
--- /dev/null
+++ b/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();
+    }
+  }
+}
\ No newline at end of file
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index fe237333c..77f36b33e 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/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;
diff --git a/Source/ExecutionEngine/WorkStealingQueue.cs b/Source/ExecutionEngine/WorkStealingQueue.cs
deleted file mode 100644
index 807d4227c..000000000
--- a/Source/ExecutionEngine/WorkStealingQueue.cs
+++ /dev/null
@@ -1,219 +0,0 @@
-using System.Collections.Generic;
-using System.Threading;
-
-namespace Microsoft.Boogie; 
-
-/// <summary>A work-stealing queue.</summary>
-/// <typeparam name="T">Specifies the type of data stored in the queue.</typeparam>
-internal class WorkStealingQueue<T> where T : class
-{
-    private const int INITIAL_SIZE = 32;
-    private T[] m_array = new T[INITIAL_SIZE];
-    private int m_mask = INITIAL_SIZE - 1;
-    private volatile int m_headIndex = 0;
-    private volatile int m_tailIndex = 0;
-
-    private object m_foreignLock = new object();
-
-    internal void LocalPush(T obj)
-    {
-        int tail = m_tailIndex;
-
-        // When there are at least 2 elements' worth of space, we can take the fast path.
-        if (tail < m_headIndex + m_mask)
-        {
-            m_array[tail & m_mask] = obj;
-            m_tailIndex = tail + 1;
-        }
-        else
-        {
-            // We need to contend with foreign pops, so we lock.
-            lock (m_foreignLock)
-            {
-                int head = m_headIndex;
-                int count = m_tailIndex - m_headIndex;
-
-                // If there is still space (one left), just add the element.
-                if (count >= m_mask)
-                {
-                    // We're full; expand the queue by doubling its size.
-                    T[] newArray = new T[m_array.Length << 1];
-                    for (int i = 0; i < m_array.Length; i++) {
-                      newArray[i] = m_array[(i + head) & m_mask];
-                    }
-
-                    // Reset the field values, incl. the mask.
-                    m_array = newArray;
-                    m_headIndex = 0;
-                    m_tailIndex = tail = count;
-                    m_mask = (m_mask << 1) | 1;
-                }
-
-                m_array[tail & m_mask] = obj;
-                m_tailIndex = tail + 1;
-            }
-        }
-    }
-
-    internal bool LocalPop(ref T obj)
-    {
-        while (true)
-        {
-            // Decrement the tail using a fence to ensure subsequent read doesn't come before.
-            int tail = m_tailIndex;
-            if (m_headIndex >= tail)
-            {
-                obj = null;
-                return false;
-            }
-
-            tail -= 1;
-#pragma warning disable 0420
-            Interlocked.Exchange(ref m_tailIndex, tail);
-#pragma warning restore 0420
-
-            // If there is no interaction with a take, we can head down the fast path.
-            if (m_headIndex <= tail)
-            {
-                int idx = tail & m_mask;
-                obj = m_array[idx];
-
-                // Check for nulls in the array.
-                if (obj == null) {
-                  continue;
-                }
-
-                m_array[idx] = null;
-                return true;
-            }
-            else
-            {
-                // Interaction with takes: 0 or 1 elements left.
-                lock (m_foreignLock)
-                {
-                    if (m_headIndex <= tail)
-                    {
-                        // Element still available. Take it.
-                        int idx = tail & m_mask;
-                        obj = m_array[idx];
-
-                        // Check for nulls in the array.
-                        if (obj == null) {
-                          continue;
-                        }
-
-                        m_array[idx] = null;
-                        return true;
-                    }
-                    else
-                    {
-                        // We lost the race, element was stolen, restore the tail.
-                        m_tailIndex = tail + 1;
-                        obj = null;
-                        return false;
-                    }
-                }
-            }
-        }
-    }
-
-    internal bool TrySteal(ref T obj)
-    {
-        obj = null;
-
-        while (true)
-        {
-            if (m_headIndex >= m_tailIndex) {
-              return false;
-            }
-
-            lock (m_foreignLock)
-            {
-                // Increment head, and ensure read of tail doesn't move before it (fence).
-                int head = m_headIndex;
-#pragma warning disable 0420
-                Interlocked.Exchange(ref m_headIndex, head + 1);
-#pragma warning restore 0420
-
-                if (head < m_tailIndex)
-                {
-                    int idx = head & m_mask;
-                    obj = m_array[idx];
-
-                    // Check for nulls in the array.
-                    if (obj == null) {
-                      continue;
-                    }
-
-                    m_array[idx] = null;
-                    return true;
-                }
-                else
-                {
-                    // Failed, restore head.
-                    m_headIndex = head;
-                    obj = null;
-                }
-            }
-
-            return false;
-        }
-    }
-
-    internal bool TryFindAndPop(T obj)
-    {
-        // We do an O(N) search for the work item. The theory of work stealing and our
-        // inlining logic is that most waits will happen on recently queued work.  And
-        // since recently queued work will be close to the tail end (which is where we
-        // begin our search), we will likely find it quickly.  In the worst case, we
-        // will traverse the whole local queue; this is typically not going to be a
-        // problem (although degenerate cases are clearly an issue) because local work
-        // queues tend to be somewhat shallow in length, and because if we fail to find
-        // the work item, we are about to block anyway (which is very expensive).
-
-        for (int i = m_tailIndex - 1; i >= m_headIndex; i--)
-        {
-            if (m_array[i & m_mask] == obj)
-            {
-                // If we found the element, block out steals to avoid interference.
-                lock (m_foreignLock)
-                {
-                    // If we lost the race, bail.
-                    if (m_array[i & m_mask] == null)
-                    {
-                        return false;
-                    }
-
-                    // Otherwise, null out the element.
-                    m_array[i & m_mask] = null;
-
-                    // And then check to see if we can fix up the indexes (if we're at
-                    // the edge).  If we can't, we just leave nulls in the array and they'll
-                    // get filtered out eventually (but may lead to superflous resizing).
-                    if (i == m_tailIndex) {
-                      m_tailIndex -= 1;
-                    } else if (i == m_headIndex) {
-                      m_headIndex += 1;
-                    }
-
-                    return true;
-                }
-            }
-        }
-
-        return false;
-    }
-
-    internal T[] ToArray()
-    {
-        List<T> list = new List<T>();
-        for (int i = m_tailIndex - 1; i >= m_headIndex; i--)
-        {
-            T obj = m_array[i & m_mask];
-            if (obj != null) {
-              list.Add(obj);
-            }
-        }
-        return list.ToArray();
-    }
-}
\ No newline at end of file
diff --git a/Source/ExecutionEngine/WorkStealingTaskScheduler.cs b/Source/ExecutionEngine/WorkStealingTaskScheduler.cs
deleted file mode 100644
index 23ff1ae4f..000000000
--- a/Source/ExecutionEngine/WorkStealingTaskScheduler.cs
+++ /dev/null
@@ -1,325 +0,0 @@
-// Code taken from https://github.com/ChadBurggraf/parallel-extensions-extras/blob/ec803e58eee28c698e44f55f49c5ad6671b1aa58/TaskSchedulers/WorkStealingTaskScheduler.cs
-//
-// This license governs use of code marked as “sample” or “example” available on this web site without a license agreement, as provided under the section above titled “NOTICE SPECIFIC TO SOFTWARE AVAILABLE ON THIS WEB SITE.” If you use such code (the “software”), you accept this license. If you do not accept the license, do not use the software.
-//
-// 1. Definitions
-// The terms “reproduce,” “reproduction,” “derivative works,” and “distribution” have the same meaning here as under U.S. copyright law.
-// A “contribution” is the original software, or any additions or changes to the software.
-// A “contributor” is any person that distributes its contribution under this license.
-// “Licensed patents” are a contributor’s patent claims that read directly on its contribution.
-//
-// 2. Grant of Rights
-// (A) Copyright Grant - Subject to the terms of this license, including the license conditions and limitations in section 3, each contributor grants you a non-exclusive, worldwide, royalty-free copyright license to reproduce its contribution, prepare derivative works of its contribution, and distribute its contribution or any derivative works that you create.
-// (B) Patent Grant - Subject to the terms of this license, including the license conditions and limitations in section 3, each contributor grants you a non-exclusive, worldwide, royalty-free license under its licensed patents to make, have made, use, sell, offer for sale, import, and/or otherwise dispose of its contribution in the software or derivative works of the contribution in the software.
-//
-// 3. Conditions and Limitations
-// (A) No Trademark License- This license does not grant you rights to use any contributors’ name, logo, or trademarks.
-// (B) If you bring a patent claim against any contributor over patents that you claim are infringed by the software, your patent license from such contributor to the software ends automatically.
-// (C) If you distribute any portion of the software, you must retain all copyright, patent, trademark, and attribution notices that are present in the software.
-// (D) If you distribute any portion of the software in source code form, you may do so only under this license by including a complete copy of this license with your distribution. If you distribute any portion of the software in compiled or object code form, you may only do so under a license that complies with this license.
-// (E) The software is licensed “as-is.” You bear the risk of using it. The contributors give no express warranties, guarantees or conditions. You may have additional consumer rights under your local laws which this license cannot change. To the extent permitted under your local laws, the contributors exclude the implied warranties of merchantability, fitness for a particular purpose and non-infringement.
-// (F) Platform Limitation - The licenses granted in sections 2(A) and 2(B) extend only to the software or derivative works that you create that run directly on a Microsoft Windows operating system product, Microsoft run-time technology (such as the .NET Framework or Silverlight), or Microsoft application platform (such as Microsoft Office or Microsoft Dynamics).
-
-using System;
-using System.Collections.Generic;
-using System.Threading;
-using System.Threading.Tasks;
-
-namespace Microsoft.Boogie;
-
-/// <summary>Provides a work-stealing scheduler.</summary>
-public class WorkStealingTaskScheduler : TaskScheduler, IDisposable
-{
-  private readonly int stackSize;
-  private readonly int m_concurrencyLevel;
-  private readonly Queue<Task> m_queue = new Queue<Task>();
-  private WorkStealingQueue<Task>[] m_wsQueues = new WorkStealingQueue<Task>[Environment.ProcessorCount];
-  private Lazy<Thread[]> m_threads;
-  private int m_threadsWaiting;
-  private bool m_shutdown;
-  [ThreadStatic]
-  private static WorkStealingQueue<Task> m_wsq;
-
-  /// <summary>Initializes a new instance of the WorkStealingTaskScheduler class.</summary>
-  /// <remarks>This constructors defaults to using twice as many threads as there are processors.</remarks>
-  public WorkStealingTaskScheduler(int stackSize) : this(stackSize, Environment.ProcessorCount * 2) { }
-
-  /// <summary>Initializes a new instance of the WorkStealingTaskScheduler class.</summary>
-  /// <param name="concurrencyLevel">The number of threads to use in the scheduler.</param>
-  public WorkStealingTaskScheduler(int stackSize, int concurrencyLevel)
-  {
-    // Store the concurrency level
-    if (concurrencyLevel <= 0) {
-      throw new ArgumentOutOfRangeException("concurrencyLevel");
-    }
-
-    this.stackSize = stackSize;
-    m_concurrencyLevel = concurrencyLevel;
-
-    // Set up threads
-    m_threads = new Lazy<Thread[]>(() =>
-    {
-      var threads = new Thread[m_concurrencyLevel];
-      for (int i = 0; i < threads.Length; i++)
-      {
-        threads[i] = new Thread(DispatchLoop, stackSize) { IsBackground = true };
-        threads[i].Start();
-      }
-      return threads;
-    });
-  }
-
-  /// <summary>Queues a task to the scheduler.</summary>
-  /// <param name="task">The task to be scheduled.</param>
-  protected override void QueueTask(Task task)
-  {
-    // Make sure the pool is started, e.g. that all threads have been created.
-    var threads = m_threads.Value;
-
-    // If the task is marked as long-running, give it its own dedicated thread
-    // rather than queueing it.
-    if ((task.CreationOptions & TaskCreationOptions.LongRunning) != 0)
-    {
-      new Thread(state => base.TryExecuteTask((Task)state)) { IsBackground = true }.Start(task);
-    }
-    else
-    {
-      // Otherwise, insert the work item into a queue, possibly waking a thread.
-      // If there's a local queue and the task does not prefer to be in the global queue,
-      // add it to the local queue.
-      WorkStealingQueue<Task> wsq = m_wsq;
-      if (wsq != null && ((task.CreationOptions & TaskCreationOptions.PreferFairness) == 0))
-      {
-        // Add to the local queue and notify any waiting threads that work is available.
-        // Races may occur which result in missed event notifications, but they're benign in that
-        // this thread will eventually pick up the work item anyway, as will other threads when another
-        // work item notification is received.
-        wsq.LocalPush(task);
-        if (m_threadsWaiting > 0) // OK to read lock-free.
-        {
-          lock (m_queue) { Monitor.Pulse(m_queue); }
-        }
-      }
-      // Otherwise, add the work item to the global queue
-      else
-      {
-        lock (m_queue)
-        {
-          m_queue.Enqueue(task);
-          if (m_threadsWaiting > 0) {
-            Monitor.Pulse(m_queue);
-          }
-        }
-      }
-    }
-  }
-
-  /// <summary>Executes a task on the current thread.</summary>
-  /// <param name="task">The task to be executed.</param>
-  /// <param name="taskWasPreviouslyQueued">Ignored.</param>
-  /// <returns>Whether the task could be executed.</returns>
-  protected override bool TryExecuteTaskInline(Task task, bool taskWasPreviouslyQueued)
-  {
-    return TryExecuteTask(task);
-
-    // // Optional replacement: Instead of always trying to execute the task (which could
-    // // benignly leave a task in the queue that's already been executed), we
-    // // can search the current work-stealing queue and remove the task,
-    // // executing it inline only if it's found.
-    // WorkStealingQueue<Task> wsq = m_wsq;
-    // return wsq != null && wsq.TryFindAndPop(task) && TryExecuteTask(task);
-  }
-
-  /// <summary>Gets the maximum concurrency level supported by this scheduler.</summary>
-  public override int MaximumConcurrencyLevel
-  {
-    get { return m_concurrencyLevel; }
-  }
-
-  /// <summary>Gets all of the tasks currently scheduled to this scheduler.</summary>
-  /// <returns>An enumerable containing all of the scheduled tasks.</returns>
-  protected override IEnumerable<Task> GetScheduledTasks()
-  {
-    // Keep track of all of the tasks we find
-    List<Task> tasks = new List<Task>();
-
-    // Get all of the global tasks.  We use TryEnter so as not to hang
-    // a debugger if the lock is held by a frozen thread.
-    bool lockTaken = false;
-    try
-    {
-      Monitor.TryEnter(m_queue, ref lockTaken);
-      if (lockTaken) {
-        tasks.AddRange(m_queue.ToArray());
-      } else {
-        throw new NotSupportedException();
-      }
-    }
-    finally
-    {
-      if (lockTaken) {
-        Monitor.Exit(m_queue);
-      }
-    }
-
-    // Now get all of the tasks from the work-stealing queues
-    WorkStealingQueue<Task>[] queues = m_wsQueues;
-    for (int i = 0; i < queues.Length; i++)
-    {
-      WorkStealingQueue<Task> wsq = queues[i];
-      if (wsq != null) {
-        tasks.AddRange(wsq.ToArray());
-      }
-    }
-
-    // Return to the debugger all of the collected task instances
-    return tasks;
-  }
-
-  /// <summary>Adds a work-stealing queue to the set of queues.</summary>
-  /// <param name="wsq">The queue to be added.</param>
-  private void AddWsq(WorkStealingQueue<Task> wsq)
-  {
-    lock (m_wsQueues)
-    {
-      // Find the next open slot in the array. If we find one,
-      // store the queue and we're done.
-      int i;
-      for (i = 0; i < m_wsQueues.Length; i++)
-      {
-        if (m_wsQueues[i] == null)
-        {
-          m_wsQueues[i] = wsq;
-          return;
-        }
-      }
-
-      // We couldn't find an open slot, so double the length 
-      // of the array by creating a new one, copying over,
-      // and storing the new one. Here, i == m_wsQueues.Length.
-      WorkStealingQueue<Task>[] queues = new WorkStealingQueue<Task>[i * 2];
-      Array.Copy(m_wsQueues, queues, i);
-      queues[i] = wsq;
-      m_wsQueues = queues;
-    }
-  }
-
-  /// <summary>Remove a work-stealing queue from the set of queues.</summary>
-  /// <param name="wsq">The work-stealing queue to remove.</param>
-  private void RemoveWsq(WorkStealingQueue<Task> wsq)
-  {
-    lock (m_wsQueues)
-    {
-      // Find the queue, and if/when we find it, null out its array slot
-      for (int i = 0; i < m_wsQueues.Length; i++)
-      {
-        if (m_wsQueues[i] == wsq)
-        {
-          m_wsQueues[i] = null;
-        }
-      }
-    }
-  }
-
-  /// <summary>
-  /// The dispatch loop run by each thread in the scheduler.
-  /// </summary>
-  private void DispatchLoop()
-  {
-    // Create a new queue for this thread, store it in TLS for later retrieval,
-    // and add it to the set of queues for this scheduler.
-    WorkStealingQueue<Task> wsq = new WorkStealingQueue<Task>();
-    m_wsq = wsq;
-    AddWsq(wsq);
-
-    try
-    {
-      // Until there's no more work to do...
-      while (true)
-      {
-        Task wi = null;
-
-        // Search order: (1) local WSQ, (2) global Q, (3) steals from other queues.
-        if (!wsq.LocalPop(ref wi))
-        {
-          // We weren't able to get a task from the local WSQ
-          bool searchedForSteals = false;
-          while (true)
-          {
-            lock (m_queue)
-            {
-              // If shutdown was requested, exit the thread.
-              if (m_shutdown) {
-                return;
-              }
-
-              // (2) try the global queue.
-              if (m_queue.Count != 0)
-              {
-                // We found a work item! Grab it ...
-                wi = m_queue.Dequeue();
-                break;
-              }
-              else if (searchedForSteals)
-              {
-                // Note that we're not waiting for work, and then wait
-                m_threadsWaiting++;
-                try { Monitor.Wait(m_queue); }
-                finally { m_threadsWaiting--; }
-
-                // If we were signaled due to shutdown, exit the thread.
-                if (m_shutdown) {
-                  return;
-                }
-
-                searchedForSteals = false;
-                continue;
-              }
-            }
-
-            // (3) try to steal.
-            WorkStealingQueue<Task>[] wsQueues = m_wsQueues;
-            int i;
-            for (i = 0; i < wsQueues.Length; i++)
-            {
-              WorkStealingQueue<Task> q = wsQueues[i];
-              if (q != null && q != wsq && q.TrySteal(ref wi)) {
-                break;
-              }
-            }
-
-            if (i != wsQueues.Length) {
-              break;
-            }
-
-            searchedForSteals = true;
-          }
-        }
-
-        // ...and Invoke it.
-        TryExecuteTask(wi);
-      }
-    }
-    finally
-    {
-      RemoveWsq(wsq);
-    }
-  }
-
-  /// <summary>Signal the scheduler to shutdown and wait for all threads to finish.</summary>
-  public void Dispose()
-  {
-    m_shutdown = true;
-    if (m_queue != null && m_threads.IsValueCreated)
-    {
-      var threads = m_threads.Value;
-      lock (m_queue) {
-        Monitor.PulseAll(m_queue);
-      }
-
-      for (int i = 0; i < threads.Length; i++) {
-        threads[i].Join();
-      }
-    }
-  }
-}
\ No newline at end of file

From 1c05ad46662da9a4ee471898c0d2add5be2149d2 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 30 Mar 2023 10:40:05 +0200
Subject: [PATCH 7/9] Refactoring

---
 .../ExecutionEngine/CustomStackSizePoolTaskScheduler.cs  | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs
index 7a0330f9f..07e1f9344 100644
--- a/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs
+++ b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs
@@ -6,6 +6,10 @@
 
 namespace Microsoft.Boogie;
 
+/// <summary>
+/// Uses a thread pool of a configurable size, with threads with a configurable stack size,
+/// to queue tasks.
+/// </summary>
 public class CustomStackSizePoolTaskScheduler : TaskScheduler, IDisposable
 {
   private readonly int threadCount;
@@ -66,8 +70,9 @@ private Task BlockUntilTaskIsAvailable()
 
   public void Dispose()
   {
-    for (int i = 0; i < threads.Length; i++) {
-      threads[i].Join();
+    foreach (var thread in threads)
+    {
+      thread.Join();
     }
   }
 }
\ No newline at end of file

From ca0e62cacb5d288b344100792cffe59b3e5f4dee Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Fri, 31 Mar 2023 10:31:46 +0200
Subject: [PATCH 8/9] Use AsyncQueue instead of SemaphoreSlim and
 ConcurrentQueue

---
 Source/Core/AsyncQueue.cs                         | 11 +++++++++++
 .../CustomStackSizePoolTaskScheduler.cs           | 15 +++------------
 Source/ExecutionEngine/ExecutionEngine.cs         |  4 ++++
 3 files changed, 18 insertions(+), 12 deletions(-)

diff --git a/Source/Core/AsyncQueue.cs b/Source/Core/AsyncQueue.cs
index 787f648a1..38bc3a590 100644
--- a/Source/Core/AsyncQueue.cs
+++ b/Source/Core/AsyncQueue.cs
@@ -36,6 +36,17 @@ public void Enqueue(T value)
     }
   }
 
+  public IEnumerable<T> Items
+  {
+    get
+    {
+      lock (myLock)
+      {
+        return items.ToArray();
+      }
+    }
+  }
+
   public Task<T> Dequeue(CancellationToken cancellationToken)
   {
     lock (myLock) {
diff --git a/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs
index 07e1f9344..83cd1f1ea 100644
--- a/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs
+++ b/Source/ExecutionEngine/CustomStackSizePoolTaskScheduler.cs
@@ -13,8 +13,7 @@ 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 AsyncQueue<Task> queue = new();
   private readonly Thread[] threads;
 
   public static CustomStackSizePoolTaskScheduler Create(int stackSize, int threadCount)
@@ -37,7 +36,6 @@ private CustomStackSizePoolTaskScheduler(int stackSize, int threadCount)
   protected override void QueueTask(Task task)
   {
     queue.Enqueue(task);
-    isWorkAvailable.Release(1);
   }
 
   protected override bool TryExecuteTaskInline(Task task, bool taskWasPreviouslyQueued)
@@ -49,25 +47,18 @@ protected override bool TryExecuteTaskInline(Task task, bool taskWasPreviouslyQu
 
   protected override IEnumerable<Task> GetScheduledTasks()
   {
-    return queue;
+    return queue.Items;
   }
   
   private void WorkLoop()
   {
     while (true)
     {
-      var task = BlockUntilTaskIsAvailable();
+      var task = queue.Dequeue(CancellationToken.None).Result;
       TryExecuteTask(task);
     }
   }
 
-  private Task BlockUntilTaskIsAvailable()
-  {
-    isWorkAvailable.Wait();
-    queue.TryDequeue(out var task);
-    return task;
-  }
-
   public void Dispose()
   {
     foreach (var thread in threads)
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 77f36b33e..31e226ada 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -26,6 +26,10 @@ public ProcessedProgram(Program program) : this(program, (_, _, _) => { }) {
 
   public class ExecutionEngine : IDisposable
   {
+    /// <summary>
+    /// Boogie traverses the Boogie and VCExpr AST using the call-stack,
+    /// so it needs to use a large stack to prevent stack overflows.
+    /// </summary>
     private static readonly CustomStackSizePoolTaskScheduler largeThreadScheduler = CustomStackSizePoolTaskScheduler.Create(16 * 1024 * 1024, Environment.ProcessorCount);
     private static readonly TaskFactory largeThreadTaskFactory = new(
       CancellationToken.None, TaskCreationOptions.DenyChildAttach,

From b0b2d0b565d720bdd4c94712e604178527bd3eb9 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Fri, 31 Mar 2023 10:56:52 +0200
Subject: [PATCH 9/9] Limit amount of large threads to configured amount

---
 Source/ExecutionEngine/ExecutionEngine.cs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 31e226ada..3e2e8d357 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -30,10 +30,7 @@ public class ExecutionEngine : IDisposable
     /// Boogie traverses the Boogie and VCExpr AST using the call-stack,
     /// so it needs to use a large stack to prevent stack overflows.
     /// </summary>
-    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);
+    private readonly TaskFactory largeThreadTaskFactory;
 
     static int autoRequestIdCount;
 
@@ -71,6 +68,9 @@ public ExecutionEngine(ExecutionEngineOptions options, VerificationResultCache c
       Cache = cache;
       checkerPool = new CheckerPool(options);
       verifyImplementationSemaphore = new SemaphoreSlim(Options.VcsCores);
+      
+      var largeThreadScheduler = CustomStackSizePoolTaskScheduler.Create(16 * 1024 * 1024, Options.VcsCores);
+      largeThreadTaskFactory = new(CancellationToken.None, TaskCreationOptions.DenyChildAttach, TaskContinuationOptions.None, largeThreadScheduler);
     }
 
     public static ExecutionEngine CreateWithoutSharedCache(ExecutionEngineOptions options) {