diff --git a/Source/Core/Configuration.cs b/Source/Core/Configuration.cs
index 0dc23b149..4a2837ec8 100644
--- a/Source/Core/Configuration.cs
+++ b/Source/Core/Configuration.cs
@@ -241,6 +241,12 @@ public class Configuration
[DataMember]
internal bool IsActorQuiescenceCheckingEnabledOutsideTesting;
+ ///
+ /// If enabled, the runtime can bypass scheduling suppression to avoid deadlocking during testing.
+ ///
+ [DataMember]
+ internal bool IsSchedulingSuppressionWeak;
+
///
/// Attaches the debugger during trace replay.
///
@@ -347,6 +353,7 @@ protected Configuration()
this.IsImplicitProgramStateHashingEnabled = false;
this.IsMonitoringEnabledOutsideTesting = false;
this.IsActorQuiescenceCheckingEnabledOutsideTesting = false;
+ this.IsSchedulingSuppressionWeak = false;
this.AttachDebugger = false;
this.IsUncontrolledInvocationStackTraceLoggingEnabled = false;
@@ -866,6 +873,15 @@ internal Configuration WithMonitoringEnabledOutsideTesting(bool isEnabled = true
return this;
}
+ ///
+ /// Updates the configuration to enable weak scheduling suppression during testing.
+ ///
+ public Configuration WithWeakSchedulingSuppressionEnabled(bool isEnabled = true)
+ {
+ this.IsSchedulingSuppressionWeak = isEnabled;
+ return this;
+ }
+
///
/// Updates the configuration to allow the runtime to check for actor quiescence
/// outside the scope of the testing engine.
diff --git a/Source/Core/Runtime/CompilerServices/SignalAwaitable.cs b/Source/Core/Runtime/CompilerServices/SignalAwaitable.cs
new file mode 100644
index 000000000..747122deb
--- /dev/null
+++ b/Source/Core/Runtime/CompilerServices/SignalAwaitable.cs
@@ -0,0 +1,118 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Runtime.CompilerServices;
+
+namespace Microsoft.Coyote.Runtime.CompilerServices
+{
+ ///
+ /// Provides an awaitable object that pauses the executing operation until a signal happens.
+ ///
+ /// This type is intended for compiler use only.
+ [System.ComponentModel.EditorBrowsable(System.ComponentModel.EditorBrowsableState.Never)]
+ public readonly struct SignalAwaitable
+{
+ ///
+ /// The paused operation awaiter.
+ ///
+ private readonly SignalAwaiter Awaiter;
+
+ ///
+ /// Initializes a new instance of the struct.
+ ///
+ internal SignalAwaitable(CoyoteRuntime runtime, ControlledOperation op, string name) =>
+ this.Awaiter = new SignalAwaiter(runtime, op, name);
+
+ ///
+ /// Returns an awaiter for this awaitable object.
+ ///
+ /// The awaiter.
+ public SignalAwaiter GetAwaiter() => this.Awaiter;
+
+ ///
+ /// Provides an awaiter that that pauses the this.Operationly executing operation until a signal happens.
+ ///
+ /// This type is intended for compiler use only.
+ public struct SignalAwaiter : IControllableAwaiter, ICriticalNotifyCompletion, INotifyCompletion
+ {
+ ///
+ /// The runtime managing the paused operation.
+ ///
+ private readonly CoyoteRuntime Runtime;
+
+ ///
+ /// The paused operation.
+ ///
+ private readonly ControlledOperation Operation;
+
+ ///
+ /// The name of the signal being awaited.
+ ///
+ private readonly string Name;
+
+ ///
+ /// The yield awaiter.
+ ///
+ private readonly YieldAwaitable.YieldAwaiter Awaiter;
+
+ ///
+ /// True if the awaiter has completed, else false.
+ ///
+#pragma warning disable CA1822 // Mark members as static
+ public bool IsCompleted => false;
+#pragma warning restore CA1822 // Mark members as static
+
+ ///
+ bool IControllableAwaiter.IsControlled => true;
+
+ ///
+ /// Initializes a new instance of the struct.
+ ///
+ internal SignalAwaiter(CoyoteRuntime runtime, ControlledOperation op, string name)
+ {
+ this.Runtime = runtime;
+ this.Operation = op;
+ this.Name = name;
+ this.Awaiter = default;
+ }
+
+ ///
+ /// Ends asynchronously waiting for the completion of the awaiter.
+ ///
+ public void GetResult() => this.Awaiter.GetResult();
+
+ ///
+ /// Sets the action to perform when the controlled task completes.
+ ///
+ public void OnCompleted(Action continuation)
+ {
+ if (this.Runtime is null || this.Operation is null)
+ {
+ this.Awaiter.OnCompleted(continuation);
+ }
+ else
+ {
+ this.Runtime.Schedule(continuation, preCondition: this.WaitSignal);
+ }
+ }
+
+ ///
+ /// Schedules the continuation action that is invoked when the controlled task completes.
+ ///
+ public void UnsafeOnCompleted(Action continuation)
+ {
+ if (this.Runtime is null || this.Operation is null)
+ {
+ this.Awaiter.UnsafeOnCompleted(continuation);
+ }
+ else
+ {
+ this.Runtime.Schedule(continuation, preCondition: this.WaitSignal);
+ }
+ }
+
+ private void WaitSignal() => SchedulingPoint.Wait(this.Name);
+ }
+ }
+}
diff --git a/Source/Core/Runtime/CoyoteRuntime.cs b/Source/Core/Runtime/CoyoteRuntime.cs
index 389f3a212..daf42e0b6 100644
--- a/Source/Core/Runtime/CoyoteRuntime.cs
+++ b/Source/Core/Runtime/CoyoteRuntime.cs
@@ -145,6 +145,16 @@ internal sealed class CoyoteRuntime : ICoyoteRuntime, IDisposable
///
private readonly HashSet UncontrolledInvocations;
+ ///
+ /// Map from signal names to their corresponding counters.
+ ///
+ internal readonly Dictionary SignalMap;
+
+ ///
+ /// Map from operation ids to the name of the signal they are awaiting.
+ ///
+ internal readonly Dictionary OperationSignalAwaiters;
+
///
/// The currently scheduled operation during systematic testing.
///
@@ -320,6 +330,8 @@ private CoyoteRuntime(Configuration configuration, OperationScheduler scheduler,
this.ControlledTasks = new ConcurrentDictionary();
this.UncontrolledTasks = new ConcurrentDictionary();
this.UncontrolledInvocations = new HashSet();
+ this.SignalMap = new Dictionary();
+ this.OperationSignalAwaiters = new Dictionary();
this.CompletionSource = new TaskCompletionSource();
if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)
@@ -431,10 +443,10 @@ internal void Schedule(Task task)
///
/// Schedules the specified continuation to execute on the controlled thread pool.
///
- internal void Schedule(Action continuation)
+ internal void Schedule(Action continuation, Action preCondition = null, Action postCondition = null)
{
ControlledOperation op = this.CreateControlledOperation(group: ExecutingOperation?.Group);
- this.ScheduleOperation(op, continuation);
+ this.ScheduleOperation(op, continuation, preCondition, postCondition);
this.ScheduleNextOperation(default, SchedulingPointType.ContinueWith);
}
@@ -456,9 +468,6 @@ private void ScheduleOperation(ControlledOperation op, Action action, Action pre
{
try
{
- // Execute the optional pre-condition.
- preCondition?.Invoke();
-
// Start the operation.
this.StartOperation(op);
@@ -469,6 +478,9 @@ private void ScheduleOperation(ControlledOperation op, Action action, Action pre
this.DelayOperation(op);
}
+ // Execute the optional pre-condition.
+ preCondition?.Invoke();
+
// Execute the controlled action.
action.Invoke();
@@ -1313,6 +1325,27 @@ private bool TryEnableOperationsWithResolvedDependencies(ControlledOperation cur
break;
}
+ if (enabledOpsCount is 0 && this.OperationMap.Values.Any(op => op.Status is OperationStatus.Suppressed))
+ {
+ if (this.Configuration.IsSchedulingSuppressionWeak)
+ {
+ // Enable all suppressed operations, to avoid deadlocking the program.
+ foreach (var op in this.OperationMap.Values)
+ {
+ if (op.Status is OperationStatus.Suppressed)
+ {
+ op.Status = OperationStatus.Enabled;
+ }
+ }
+
+ this.OperationSignalAwaiters.Clear();
+ }
+ else
+ {
+ this.NotifyAssertionFailure("Only suppressed operations remain.");
+ }
+ }
+
this.LogWriter.LogDebug("[coyote::debug] There are {0} enabled operations in runtime '{1}'.",
enabledOpsCount, this.Id);
this.MaxConcurrencyDegree = Math.Max(this.MaxConcurrencyDegree, enabledOpsCount);
@@ -2604,6 +2637,8 @@ private void Dispose(bool disposing)
this.SpecificationMonitors.Clear();
this.TaskLivenessMonitors.Clear();
this.StateHashingFunctions.Clear();
+ this.SignalMap.Clear();
+ this.OperationSignalAwaiters.Clear();
if (!(this.Extension is NullRuntimeExtension))
{
diff --git a/Source/Core/Runtime/Operations/OperationStatus.cs b/Source/Core/Runtime/Operations/OperationStatus.cs
index d002e8fa9..c765bf1de 100644
--- a/Source/Core/Runtime/Operations/OperationStatus.cs
+++ b/Source/Core/Runtime/Operations/OperationStatus.cs
@@ -38,6 +38,11 @@ internal enum OperationStatus
///
PausedOnReceive,
+ ///
+ /// The operation is suppressed until it is resumed.
+ ///
+ Suppressed,
+
///
/// The operation is completed.
///
diff --git a/Source/Core/Runtime/Scheduling/SchedulingPoint.cs b/Source/Core/Runtime/Scheduling/SchedulingPoint.cs
index 47e95b2c9..e01f47537 100644
--- a/Source/Core/Runtime/Scheduling/SchedulingPoint.cs
+++ b/Source/Core/Runtime/Scheduling/SchedulingPoint.cs
@@ -2,6 +2,8 @@
// Licensed under the MIT License.
using System.Collections.Generic;
+using System.Linq;
+using Microsoft.Coyote.Runtime.CompilerServices;
namespace Microsoft.Coyote.Runtime
{
@@ -107,6 +109,85 @@ public static void Write(string state, IEqualityComparer comparer = defa
}
}
+ ///
+ /// Waits for a signal to a resource with the specified name.
+ ///
+ [System.ComponentModel.EditorBrowsable(System.ComponentModel.EditorBrowsableState.Never)]
+ public static void Wait(string name)
+ {
+ var runtime = CoyoteRuntime.Current;
+ if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving &&
+ runtime.TryGetExecutingOperation(out ControlledOperation current))
+ {
+ using (runtime.EnterSynchronizedSection())
+ {
+ if (!runtime.SignalMap.TryGetValue(name, out var signal))
+ {
+ runtime.SignalMap.Add(name, 0);
+ }
+
+ runtime.SignalMap[name]--;
+ if (runtime.SignalMap[name] < 0)
+ {
+ runtime.LogWriter.LogDebug("[coyote::debug] Operation '{0}' is waiting a signal for '{1}'.",
+ current.Name, name);
+ runtime.SignalMap[name] = 0;
+ current.Status = OperationStatus.Suppressed;
+ runtime.OperationSignalAwaiters.Add(current.Id, name);
+ runtime.ScheduleNextOperation(current, SchedulingPointType.Default, isSuppressible: false);
+ }
+ }
+ }
+ }
+
+ ///
+ /// Waits asynchronously for a signal to a resource with the specified name.
+ ///
+ [System.ComponentModel.EditorBrowsable(System.ComponentModel.EditorBrowsableState.Never)]
+ public static SignalAwaitable WaitAsync(string name)
+ {
+ var runtime = CoyoteRuntime.Current;
+ if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving &&
+ runtime.TryGetExecutingOperation(out ControlledOperation current))
+ {
+ return new SignalAwaitable(runtime, current, name);
+ }
+
+ return new SignalAwaitable(null, null, name);
+ }
+
+ ///
+ /// Signals a resource with the specified name.
+ ///
+ [System.ComponentModel.EditorBrowsable(System.ComponentModel.EditorBrowsableState.Never)]
+ public static void Signal(string name)
+ {
+ var runtime = CoyoteRuntime.Current;
+ if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving &&
+ runtime.TryGetExecutingOperation(out ControlledOperation current))
+ {
+ using (runtime.EnterSynchronizedSection())
+ {
+ foreach (var kvp in runtime.OperationSignalAwaiters.Where(kvp => kvp.Value == name).ToList())
+ {
+ var op = runtime.GetOperationWithId(kvp.Key);
+ runtime.LogWriter.LogDebug("[coyote::debug] Operation '{0}' is signaled for '{1}'.",
+ op.Name, name);
+ op.Status = OperationStatus.Enabled;
+ runtime.OperationSignalAwaiters.Remove(kvp.Key);
+ }
+
+ if (!runtime.SignalMap.TryGetValue(name, out var signal))
+ {
+ runtime.SignalMap.Add(name, 0);
+ }
+
+ runtime.SignalMap[name]++;
+ runtime.ScheduleNextOperation(current, SchedulingPointType.Default, isSuppressible: false);
+ }
+ }
+ }
+
///
/// Suppresses interleavings until is invoked.
///