experimental scheduling wait and signal apis (#440)

Source/Core/Configuration.cs

@@ -241,6 +241,12 @@ namespace Microsoft.Coyote
         [DataMember]
         internal bool IsActorQuiescenceCheckingEnabledOutsideTesting;
 
+        /// <summary>
+        /// If enabled, the runtime can bypass scheduling suppression to avoid deadlocking during testing.
+        /// </summary>
+        [DataMember]
+        internal bool IsSchedulingSuppressionWeak;
+
         /// <summary>
         /// Attaches the debugger during trace replay.
         /// </summary>
@@ -347,6 +353,7 @@ namespace Microsoft.Coyote
             this.IsImplicitProgramStateHashingEnabled = false;
             this.IsMonitoringEnabledOutsideTesting = false;
             this.IsActorQuiescenceCheckingEnabledOutsideTesting = false;
+            this.IsSchedulingSuppressionWeak = false;
             this.AttachDebugger = false;
 
             this.IsUncontrolledInvocationStackTraceLoggingEnabled = false;
@@ -866,6 +873,15 @@ namespace Microsoft.Coyote
             return this;
         }
 
+        /// <summary>
+        /// Updates the configuration to enable weak scheduling suppression during testing.
+        /// </summary>
+        public Configuration WithWeakSchedulingSuppressionEnabled(bool isEnabled = true)
+        {
+            this.IsSchedulingSuppressionWeak = isEnabled;
+            return this;
+        }
+
         /// <summary>
         /// Updates the configuration to allow the runtime to check for actor quiescence
         /// outside the scope of the testing engine.

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
+{
+    /// <summary>
+    /// Provides an awaitable object that pauses the executing operation until a signal happens.
+    /// </summary>
+    /// <remarks>This type is intended for compiler use only.</remarks>
+    [System.ComponentModel.EditorBrowsable(System.ComponentModel.EditorBrowsableState.Never)]
+    public readonly struct SignalAwaitable
+{
+        /// <summary>
+        /// The paused operation awaiter.
+        /// </summary>
+        private readonly SignalAwaiter Awaiter;
+
+        /// <summary>
+        /// Initializes a new instance of the <see cref="SignalAwaitable"/> struct.
+        /// </summary>
+        internal SignalAwaitable(CoyoteRuntime runtime, ControlledOperation op, string name) =>
+            this.Awaiter = new SignalAwaiter(runtime, op, name);
+
+        /// <summary>
+        /// Returns an awaiter for this awaitable object.
+        /// </summary>
+        /// <returns>The awaiter.</returns>
+        public SignalAwaiter GetAwaiter() => this.Awaiter;
+
+        /// <summary>
+        /// Provides an awaiter that that pauses the this.Operationly executing operation until a signal happens.
+        /// </summary>
+        /// <remarks>This type is intended for compiler use only.</remarks>
+        public struct SignalAwaiter : IControllableAwaiter, ICriticalNotifyCompletion, INotifyCompletion
+        {
+            /// <summary>
+            /// The runtime managing the paused operation.
+            /// </summary>
+            private readonly CoyoteRuntime Runtime;
+
+            /// <summary>
+            /// The paused operation.
+            /// </summary>
+            private readonly ControlledOperation Operation;
+
+            /// <summary>
+            /// The name of the signal being awaited.
+            /// </summary>
+            private readonly string Name;
+
+            /// <summary>
+            /// The yield awaiter.
+            /// </summary>
+            private readonly YieldAwaitable.YieldAwaiter Awaiter;
+
+            /// <summary>
+            /// True if the awaiter has completed, else false.
+            /// </summary>
+#pragma warning disable CA1822 // Mark members as static
+            public bool IsCompleted => false;
+#pragma warning restore CA1822 // Mark members as static
+
+            /// <inheritdoc/>
+            bool IControllableAwaiter.IsControlled => true;
+
+            /// <summary>
+            /// Initializes a new instance of the <see cref="SignalAwaiter"/> struct.
+            /// </summary>
+            internal SignalAwaiter(CoyoteRuntime runtime, ControlledOperation op, string name)
+            {
+                this.Runtime = runtime;
+                this.Operation = op;
+                this.Name = name;
+                this.Awaiter = default;
+            }
+
+            /// <summary>
+            /// Ends asynchronously waiting for the completion of the awaiter.
+            /// </summary>
+            public void GetResult() => this.Awaiter.GetResult();
+
+            /// <summary>
+            /// Sets the action to perform when the controlled task completes.
+            /// </summary>
+            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);
+                }
+            }
+
+            /// <summary>
+            /// Schedules the continuation action that is invoked when the controlled task completes.
+            /// </summary>
+            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);
+        }
+    }
+}

Source/Core/Runtime/CoyoteRuntime.cs

@@ -145,6 +145,16 @@ namespace Microsoft.Coyote.Runtime
         /// </summary>
         private readonly HashSet<string> UncontrolledInvocations;
 
+        /// <summary>
+        /// Map from signal names to their corresponding counters.
+        /// </summary>
+        internal readonly Dictionary<string, int> SignalMap;
+
+        /// <summary>
+        /// Map from operation ids to the name of the signal they are awaiting.
+        /// </summary>
+        internal readonly Dictionary<ulong, string> OperationSignalAwaiters;
+
         /// <summary>
         /// The currently scheduled operation during systematic testing.
         /// </summary>
@@ -320,6 +330,8 @@ namespace Microsoft.Coyote.Runtime
             this.ControlledTasks = new ConcurrentDictionary<Task, ControlledOperation>();
             this.UncontrolledTasks = new ConcurrentDictionary<Task, string>();
             this.UncontrolledInvocations = new HashSet<string>();
+            this.SignalMap = new Dictionary<string, int>();
+            this.OperationSignalAwaiters = new Dictionary<ulong, string>();
             this.CompletionSource = new TaskCompletionSource<bool>();
 
             if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)
@@ -431,10 +443,10 @@ namespace Microsoft.Coyote.Runtime
         /// <summary>
         /// Schedules the specified continuation to execute on the controlled thread pool.
         /// </summary>
-        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 @@ namespace Microsoft.Coyote.Runtime
                 {
                     try
                     {
-                        // Execute the optional pre-condition.
-                        preCondition?.Invoke();
-
                         // Start the operation.
                         this.StartOperation(op);
 
@@ -469,6 +478,9 @@ namespace Microsoft.Coyote.Runtime
                             this.DelayOperation(op);
                         }
 
+                        // Execute the optional pre-condition.
+                        preCondition?.Invoke();
+
                         // Execute the controlled action.
                         action.Invoke();
 
@@ -1313,6 +1325,27 @@ namespace Microsoft.Coyote.Runtime
                 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 @@ namespace Microsoft.Coyote.Runtime
                     this.SpecificationMonitors.Clear();
                     this.TaskLivenessMonitors.Clear();
                     this.StateHashingFunctions.Clear();
+                    this.SignalMap.Clear();
+                    this.OperationSignalAwaiters.Clear();
 
                     if (!(this.Extension is NullRuntimeExtension))
                     {

Source/Core/Runtime/Operations/OperationStatus.cs

@@ -38,6 +38,11 @@ namespace Microsoft.Coyote.Runtime
         /// </summary>
         PausedOnReceive,
 
+        /// <summary>
+        /// The operation is suppressed until it is resumed.
+        /// </summary>
+        Suppressed,
+
         /// <summary>
         /// The operation is completed.
         /// </summary>

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 @@ namespace Microsoft.Coyote.Runtime
             }
         }
 
+        /// <summary>
+        /// Waits for a signal to a resource with the specified name.
+        /// </summary>
+        [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);
+                    }
+                }
+            }
+        }
+
+        /// <summary>
+        /// Waits asynchronously for a signal to a resource with the specified name.
+        /// </summary>
+        [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);
+        }
+
+        /// <summary>
+        /// Signals a resource with the specified name.
+        /// </summary>
+        [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);
+                }
+            }
+        }
+
         /// <summary>
         /// Suppresses interleavings until <see cref="Resume"/> is invoked.
         /// </summary>