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 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 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 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/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; - -/// Provides a work-stealing scheduler. -public class WorkStealingTaskScheduler : TaskScheduler, IDisposable -{ - private readonly int stackSize; - private readonly int m_concurrencyLevel; - private readonly Queue m_queue = new Queue(); - private WorkStealingQueue[] m_wsQueues = new WorkStealingQueue[Environment.ProcessorCount]; - private Lazy m_threads; - private int m_threadsWaiting; - private bool m_shutdown; - [ThreadStatic] - private static WorkStealingQueue m_wsq; - - /// Initializes a new instance of the WorkStealingTaskScheduler class. - /// This constructors defaults to using twice as many threads as there are processors. - public WorkStealingTaskScheduler(int stackSize) : this(stackSize, Environment.ProcessorCount * 2) { } - - /// Initializes a new instance of the WorkStealingTaskScheduler class. - /// The number of threads to use in the scheduler. - 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(() => - { - 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; - }); - } - - /// Queues a task to the scheduler. - /// The task to be scheduled. - 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 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); - } - } - } - } - } - - /// Executes a task on the current thread. - /// The task to be executed. - /// Ignored. - /// Whether the task could be executed. - 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 wsq = m_wsq; - // return wsq != null && wsq.TryFindAndPop(task) && TryExecuteTask(task); - } - - /// Gets the maximum concurrency level supported by this scheduler. - public override int MaximumConcurrencyLevel - { - get { return m_concurrencyLevel; } - } - - /// Gets all of the tasks currently scheduled to this scheduler. - /// An enumerable containing all of the scheduled tasks. - protected override IEnumerable GetScheduledTasks() - { - // Keep track of all of the tasks we find - List tasks = new List(); - - // 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[] queues = m_wsQueues; - for (int i = 0; i < queues.Length; i++) - { - WorkStealingQueue wsq = queues[i]; - if (wsq != null) { - tasks.AddRange(wsq.ToArray()); - } - } - - // Return to the debugger all of the collected task instances - return tasks; - } - - /// Adds a work-stealing queue to the set of queues. - /// The queue to be added. - private void AddWsq(WorkStealingQueue 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[] queues = new WorkStealingQueue[i * 2]; - Array.Copy(m_wsQueues, queues, i); - queues[i] = wsq; - m_wsQueues = queues; - } - } - - /// Remove a work-stealing queue from the set of queues. - /// The work-stealing queue to remove. - private void RemoveWsq(WorkStealingQueue 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; - } - } - } - } - - /// - /// The dispatch loop run by each thread in the scheduler. - /// - 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 wsq = new WorkStealingQueue(); - 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[] wsQueues = m_wsQueues; - int i; - for (i = 0; i < wsQueues.Length; i++) - { - WorkStealingQueue 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); - } - } - - /// Signal the scheduler to shutdown and wait for all threads to finish. - 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