diff --git a/Source/Core/Runtime/CoyoteRuntime.cs b/Source/Core/Runtime/CoyoteRuntime.cs index 183bdd72..03e9c6ad 100644 --- a/Source/Core/Runtime/CoyoteRuntime.cs +++ b/Source/Core/Runtime/CoyoteRuntime.cs @@ -818,10 +818,12 @@ namespace Microsoft.Coyote.Runtime /// The type of the scheduling point. /// True if the interleaving can be suppressed, else false. /// True if the current operation is yielding, else false. + /// True if an operation other than the current was scheduled, else false. /// /// An enabled operation is one that is not paused nor completed. /// - 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; } } diff --git a/Source/Test/Rewriting/Passes/Rewriting/Types/TypeRewritingPass.cs b/Source/Test/Rewriting/Passes/Rewriting/Types/TypeRewritingPass.cs index d498288a..f831bf3f 100644 --- a/Source/Test/Rewriting/Passes/Rewriting/Types/TypeRewritingPass.cs +++ b/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); diff --git a/Source/Test/Rewriting/Passes/Rewriting/UncontrolledInvocationRewritingPass.cs b/Source/Test/Rewriting/Passes/Rewriting/UncontrolledInvocationRewritingPass.cs index 7b274b5e..dc599389 100644 --- a/Source/Test/Rewriting/Passes/Rewriting/UncontrolledInvocationRewritingPass.cs +++ b/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) || diff --git a/Source/Test/Rewriting/Types/NameCache.cs b/Source/Test/Rewriting/Types/NameCache.cs index 2072ba6f..14ae6d08 100644 --- a/Source/Test/Rewriting/Types/NameCache.cs +++ b/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; diff --git a/Source/Test/Rewriting/Types/Threading/Thread.cs b/Source/Test/Rewriting/Types/Threading/Thread.cs new file mode 100644 index 00000000..d7d6b1f3 --- /dev/null +++ b/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 +{ + /// + /// Provides methods for creating threads that can be controlled during testing. + /// + /// This type is intended for compiler use rather than use directly in code. + [System.ComponentModel.EditorBrowsable(System.ComponentModel.EditorBrowsableState.Never)] + public static class Thread + { + /// + /// Causes the calling thread to yield execution to another thread that is ready + /// to run on the current processor. + /// + 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(); + } + } +} diff --git a/Tests/Tests.BugFinding/Threading/Locks/LockStatementTests.cs b/Tests/Tests.BugFinding/Locks/LockStatementTests.cs similarity index 100% rename from Tests/Tests.BugFinding/Threading/Locks/LockStatementTests.cs rename to Tests/Tests.BugFinding/Locks/LockStatementTests.cs diff --git a/Tests/Tests.BugFinding/Threading/Locks/MonitorTests.cs b/Tests/Tests.BugFinding/Locks/MonitorTests.cs similarity index 100% rename from Tests/Tests.BugFinding/Threading/Locks/MonitorTests.cs rename to Tests/Tests.BugFinding/Locks/MonitorTests.cs diff --git a/Tests/Tests.BugFinding/Threading/Locks/SemaphoreSlimTests.cs b/Tests/Tests.BugFinding/Locks/SemaphoreSlimTests.cs similarity index 100% rename from Tests/Tests.BugFinding/Threading/Locks/SemaphoreSlimTests.cs rename to Tests/Tests.BugFinding/Locks/SemaphoreSlimTests.cs diff --git a/Tests/Tests.BugFinding/PartialControl/UncontrolledInvocationsTests.cs b/Tests/Tests.BugFinding/PartialControl/UncontrolledInvocationsTests.cs index 482e9cdd..9f46f43c 100644 --- a/Tests/Tests.BugFinding/PartialControl/UncontrolledInvocationsTests.cs +++ b/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); }); } diff --git a/Tests/Tests.BugFinding/Threads/ThreadYieldTests.cs b/Tests/Tests.BugFinding/Threads/ThreadYieldTests.cs new file mode 100644 index 00000000..102dbf73 --- /dev/null +++ b/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); + } + } +} diff --git a/Tests/compare-rewriting-diff-logs.ps1 b/Tests/compare-rewriting-diff-logs.ps1 index 55304d74..e1ad5498 100644 --- a/Tests/compare-rewriting-diff-logs.ps1 +++ b/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" }