thread yield rewriting (#418)

Source/Core/Runtime/CoyoteRuntime.cs

@@ -818,10 +818,12 @@ namespace Microsoft.Coyote.Runtime
         /// <param name="type">The type of the scheduling point.</param>
         /// <param name="isSuppressible">True if the interleaving can be suppressed, else false.</param>
         /// <param name="isYielding">True if the current operation is yielding, else false.</param>
+        /// <returns>True if an operation other than the current was scheduled, else false.</returns>
         /// <remarks>
         /// An enabled operation is one that is not paused nor completed.
         /// </remarks>
-        internal void ScheduleNextOperation(ControlledOperation current, SchedulingPointType type, bool isSuppressible = true, bool isYielding = false)
+        internal bool ScheduleNextOperation(ControlledOperation current, SchedulingPointType type,
+            bool isSuppressible = true, bool isYielding = false)
         {
             using (SynchronizedSection.Enter(this.RuntimeLock))
             {
@@ -832,7 +834,7 @@ namespace Microsoft.Coyote.Runtime
                 {
                     // Cannot schedule the next operation if the scheduler is not attached,
                     // or if the scheduling policy is not systematic.
-                    return;
+                    return false;
                 }
 
                 // Check if the currently executing thread is uncontrolled.
@@ -857,7 +859,7 @@ namespace Microsoft.Coyote.Runtime
                         this.LogWriter.LogDebug("[coyote::debug] Postponing scheduling point '{0}' in uncontrolled thread '{1}'.",
                             type, Thread.CurrentThread.ManagedThreadId);
                         this.LastPostponedSchedulingPoint = type;
-                        return;
+                        return false;
                     }
 
                     isThreadUncontrolled = true;
@@ -869,14 +871,14 @@ namespace Microsoft.Coyote.Runtime
                 if (current is null)
                 {
                     // Cannot proceed without having access to the currently executing operation.
-                    return;
+                    return false;
                 }
 
                 if (current != this.ScheduledOperation)
                 {
                     // The currently executing operation is not scheduled, so send it to sleep.
                     this.PauseOperation(current);
-                    return;
+                    return false;
                 }
 
                 if (this.IsSchedulerSuppressed && this.LastPostponedSchedulingPoint is null &&
@@ -884,7 +886,7 @@ namespace Microsoft.Coyote.Runtime
                 {
                     // Suppress the scheduling point.
                     this.LogWriter.LogDebug("[coyote::debug] Suppressing scheduling point in operation '{0}'.", current.Name);
-                    return;
+                    return false;
                 }
 
                 this.Assert(!this.IsSpecificationInvoked, "Executing a specification monitor must be atomic.");
@@ -918,7 +920,7 @@ namespace Microsoft.Coyote.Runtime
                             type, current);
                         this.LastPostponedSchedulingPoint = type;
                         this.PauseOperation(current);
-                        return;
+                        return false;
                     }
 
                     // Check if the execution has deadlocked.
@@ -939,7 +941,8 @@ namespace Microsoft.Coyote.Runtime
 
                 this.LogWriter.LogDebug("[coyote::debug] Scheduling operation '{0}' of group '{1}'.",
                     next.Name, next.Group);
-                if (current != next)
+                bool isNextOperationScheduled = current != next;
+                if (isNextOperationScheduled)
                 {
                     // Pause the currently scheduled operation, and enable the next one.
                     this.ScheduledOperation = next;
@@ -952,6 +955,8 @@ namespace Microsoft.Coyote.Runtime
                     // is uncontrolled, then we need to signal the current operation to resume execution.
                     next.Signal();
                 }
+
+                return isNextOperationScheduled;
             }
         }
 

Source/Test/Rewriting/Passes/Rewriting/Types/TypeRewritingPass.cs

@@ -75,6 +75,9 @@ namespace Microsoft.Coyote.Rewriting
             this.KnownTypes[NameCache.GenericTaskFactory] = typeof(Types.Threading.Tasks.TaskFactory<>);
             this.KnownTypes[NameCache.TaskParallel] = typeof(Types.Threading.Tasks.Parallel);
 
+            // Populate the map with the default thread-based types.
+            this.KnownTypes[NameCache.Thread] = typeof(Types.Threading.Thread);
+
             // Populate the map with the known synchronization types.
             this.KnownTypes[NameCache.Monitor] = typeof(Types.Threading.Monitor);
             this.KnownTypes[NameCache.SemaphoreSlim] = typeof(Types.Threading.SemaphoreSlim);

Source/Test/Rewriting/Passes/Rewriting/UncontrolledInvocationRewritingPass.cs

@@ -126,7 +126,6 @@ namespace Microsoft.Coyote.Rewriting
                     method.Name is nameof(System.Threading.Thread.Join) ||
                     method.Name is nameof(System.Threading.Thread.SpinWait) ||
                     method.Name is nameof(System.Threading.Thread.Sleep) ||
-                    method.Name is nameof(System.Threading.Thread.Yield) ||
                     method.Name is nameof(System.Threading.Thread.Interrupt) ||
                     method.Name is nameof(System.Threading.Thread.Suspend) ||
                     method.Name is nameof(System.Threading.Thread.Resume) ||

Source/Test/Rewriting/Types/NameCache.cs

@@ -21,29 +21,29 @@ namespace Microsoft.Coyote.Rewriting.Types
         internal static string SystemCompilerNamespace { get; } = typeof(SystemCompiler.AsyncTaskMethodBuilder).Namespace;
         internal static string SystemTasksNamespace { get; } = typeof(SystemTasks.Task).Namespace;
 
-        internal static string TaskName { get; } = typeof(SystemTasks.Task).Name;
         internal static string Task { get; } = typeof(SystemTasks.Task).FullName;
+        internal static string TaskName { get; } = typeof(SystemTasks.Task).Name;
         internal static string GenericTask { get; } = typeof(SystemTasks.Task<>).FullName;
-        internal static string ValueTaskName { get; } = typeof(SystemTasks.ValueTask).Name;
         internal static string ValueTask { get; } = typeof(SystemTasks.ValueTask).FullName;
+        internal static string ValueTaskName { get; } = typeof(SystemTasks.ValueTask).Name;
         internal static string GenericValueTask { get; } = typeof(SystemTasks.ValueTask<>).FullName;
 #if NET
         internal static string TaskCompletionSource { get; } = typeof(SystemTasks.TaskCompletionSource).FullName;
 #endif
         internal static string GenericTaskCompletionSource { get; } = typeof(SystemTasks.TaskCompletionSource<>).FullName;
 
-        internal static string AsyncTaskMethodBuilderName { get; } = typeof(SystemCompiler.AsyncTaskMethodBuilder).Name;
         internal static string AsyncTaskMethodBuilder { get; } = typeof(SystemCompiler.AsyncTaskMethodBuilder).FullName;
+        internal static string AsyncTaskMethodBuilderName { get; } = typeof(SystemCompiler.AsyncTaskMethodBuilder).Name;
         internal static string GenericAsyncTaskMethodBuilder { get; } = typeof(SystemCompiler.AsyncTaskMethodBuilder<>).FullName;
-        internal static string AsyncValueTaskMethodBuilderName { get; } = typeof(SystemCompiler.AsyncValueTaskMethodBuilder).Name;
         internal static string AsyncValueTaskMethodBuilder { get; } = typeof(SystemCompiler.AsyncValueTaskMethodBuilder).FullName;
+        internal static string AsyncValueTaskMethodBuilderName { get; } = typeof(SystemCompiler.AsyncValueTaskMethodBuilder).Name;
         internal static string GenericAsyncValueTaskMethodBuilder { get; } = typeof(SystemCompiler.AsyncValueTaskMethodBuilder<>).FullName;
 
-        internal static string TaskAwaiterName { get; } = typeof(SystemCompiler.TaskAwaiter).Name;
         internal static string TaskAwaiter { get; } = typeof(SystemCompiler.TaskAwaiter).FullName;
+        internal static string TaskAwaiterName { get; } = typeof(SystemCompiler.TaskAwaiter).Name;
         internal static string GenericTaskAwaiter { get; } = typeof(SystemCompiler.TaskAwaiter<>).FullName;
-        internal static string ValueTaskAwaiterName { get; } = typeof(SystemCompiler.ValueTaskAwaiter).Name;
         internal static string ValueTaskAwaiter { get; } = typeof(SystemCompiler.ValueTaskAwaiter).FullName;
+        internal static string ValueTaskAwaiterName { get; } = typeof(SystemCompiler.ValueTaskAwaiter).Name;
         internal static string GenericValueTaskAwaiter { get; } = typeof(SystemCompiler.ValueTaskAwaiter<>).FullName;
 
         internal static string ConfiguredTaskAwaitable { get; } = typeof(SystemCompiler.ConfiguredTaskAwaitable).FullName;
@@ -68,6 +68,8 @@ namespace Microsoft.Coyote.Rewriting.Types
         internal static string GenericTaskFactory { get; } = typeof(SystemTasks.TaskFactory<>).FullName;
         internal static string TaskParallel { get; } = typeof(SystemTasks.Parallel).FullName;
 
+        internal static string Thread { get; } = typeof(SystemThreading.Thread).FullName;
+
         internal static string Monitor { get; } = typeof(SystemThreading.Monitor).FullName;
         internal static string SemaphoreSlim { get; } = typeof(SystemThreading.SemaphoreSlim).FullName;
 

Source/Test/Rewriting/Types/Threading/Thread.cs

@@ -0,0 +1,32 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using Microsoft.Coyote.Runtime;
+using SystemThread = System.Threading.Thread;
+
+namespace Microsoft.Coyote.Rewriting.Types.Threading
+{
+    /// <summary>
+    /// Provides methods for creating threads that can be controlled during testing.
+    /// </summary>
+    /// <remarks>This type is intended for compiler use rather than use directly in code.</remarks>
+    [System.ComponentModel.EditorBrowsable(System.ComponentModel.EditorBrowsableState.Never)]
+    public static class Thread
+    {
+        /// <summary>
+        /// Causes the calling thread to yield execution to another thread that is ready
+        /// to run on the current processor.
+        /// </summary>
+        public static bool Yield()
+        {
+            var runtime = CoyoteRuntime.Current;
+            if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving &&
+                runtime.TryGetExecutingOperation(out ControlledOperation current))
+            {
+                return runtime.ScheduleNextOperation(current, SchedulingPointType.Yield, true, true);
+            }
+
+            return SystemThread.Yield();
+        }
+    }
+}

Tests/Tests.BugFinding/PartialControl/UncontrolledInvocationsTests.cs

@@ -45,11 +45,11 @@ namespace Microsoft.Coyote.BugFinding.Tests
         }
 
         [Fact(Timeout = 5000)]
-        public void TestUncontrolledThreadYieldInvocation()
+        public void TestUncontrolledThreadSpinWaitInvocation()
         {
             this.Test(() =>
             {
-                Thread.Yield();
+                Thread.SpinWait(10);
             },
             configuration: this.GetConfiguration()
                 .WithPartiallyControlledConcurrencyAllowed()
@@ -57,15 +57,15 @@ namespace Microsoft.Coyote.BugFinding.Tests
         }
 
         [Fact(Timeout = 5000)]
-        public void TestUncontrolledThreadYieldInvocationWithNoPartialControl()
+        public void TestUncontrolledThreadSpinWaitInvocationWithNoPartialControl()
         {
             this.TestWithError(() =>
             {
-                Thread.Yield();
+                Thread.SpinWait(10);
             },
             errorChecker: (e) =>
             {
-                var expectedMethodName = GetFullyQualifiedMethodName(typeof(Thread), nameof(Thread.Yield));
+                var expectedMethodName = GetFullyQualifiedMethodName(typeof(Thread), nameof(Thread.SpinWait));
                 Assert.StartsWith($"Invoking '{expectedMethodName}' is not intercepted", e);
             });
         }

Tests/Tests.BugFinding/Threads/ThreadYieldTests.cs

@@ -0,0 +1,54 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System.Threading;
+using System.Threading.Tasks;
+using Xunit;
+using Xunit.Abstractions;
+
+namespace Microsoft.Coyote.BugFinding.Tests
+{
+    public class ThreadYieldTests : BaseBugFindingTest
+    {
+        public ThreadYieldTests(ITestOutputHelper output)
+            : base(output)
+        {
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestThreadYield()
+        {
+            this.Test(() =>
+            {
+                Thread.Yield();
+            },
+            configuration: this.GetConfiguration().WithTestingIterations(10));
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestCooperativeThreadYield()
+        {
+            Configuration config = this.GetConfiguration().WithTestingIterations(10)
+                .WithPartiallyControlledConcurrencyAllowed(true);
+            this.Test(() =>
+            {
+                bool isDone = false;
+                Task t1 = Task.Run(() =>
+                {
+                    isDone = true;
+                });
+
+                Task t2 = Task.Run(() =>
+                {
+                    while (!isDone)
+                    {
+                        Thread.Yield();
+                    }
+                });
+
+                Task.WaitAll(t1, t2);
+            },
+            config);
+        }
+    }
+}

Tests/compare-rewriting-diff-logs.ps1

@@ -15,7 +15,7 @@ $targets = [ordered]@{
 $expected_hashes = [ordered]@{
     "rewriting" = "81B3B708113A55B3E7D597EC93E8E2B1FA669CD146F84663BF340E03BFB9A93A"
     "rewriting-helpers" = "9D6638DF52487AC25377D31BA8D0B1532C85F7BB5119751010D53ED02E247B17"
-    "testing" = "22C55B6369A5D82B2A1DE1B84FE8DD19514A53C086B2BBDC97DB16EEF8279C0F"
+    "testing" = "D27A38A5366A5C8FF30F187E191471FA0B9E049E3236202FD532DA684B8205A1"
     "actors" = "DED07E1858B24CFCA349A030A244F53174219463ACE92E2C62CA3C45CB94562C"
     "actors-testing" = "79017E9E5C3D2FFDFABBC6316B04FBE83A1C8E2C434ECEC8E3686895C4BF82BE"
 }