support for wait handles (#460)

Source/Core/Runtime/CoyoteRuntime.cs

@@ -1921,7 +1921,9 @@ private void CheckIfExecutionHasDeadlocked(IEnumerable<ControlledOperation> ops)
  }
 
  var pausedOperations = ops.Where(op => op.Status is OperationStatus.Paused).ToList();
- var pausedOnResources = ops.Where(op => op.Status is OperationStatus.PausedOnResource).ToList();
+ var pausedOnResources = ops.Where(op =>
+ op.Status is OperationStatus.PausedOnAnyResource ||
+ op.Status is OperationStatus.PausedOnAllResources).ToList();
  var pausedOnReceiveOperations = ops.Where(op => op.Status is OperationStatus.PausedOnReceive).ToList();
 
  var totalCount = pausedOperations.Count + pausedOnResources.Count + pausedOnReceiveOperations.Count;

Source/Core/Runtime/Operations/ControlledOperation.cs

@@ -64,6 +64,11 @@ internal class ControlledOperation : IEquatable<ControlledOperation>, IDisposabl
  /// </summary>
  internal readonly List<string> VisitedCallSites;
 
+ /// <summary>
+ /// Resources that must be signaled before this operation can resume executing.
+ /// </summary>
+ private readonly HashSet<Guid> AwaitedResources;
+
  /// <summary>
  /// Dependency that must get resolved before this operation can resume executing.
  /// </summary>
@@ -134,7 +139,8 @@ internal class ControlledOperation : IEquatable<ControlledOperation>, IDisposabl
  internal bool IsPaused =>
  this.Status is OperationStatus.Paused ||
  this.Status is OperationStatus.PausedOnDelay ||
- this.Status is OperationStatus.PausedOnResource ||
+ this.Status is OperationStatus.PausedOnAnyResource ||
+ this.Status is OperationStatus.PausedOnAllResources ||
  this.Status is OperationStatus.PausedOnReceive;
 
  /// <summary>
@@ -154,6 +160,7 @@ internal ControlledOperation(ulong operationId, string name, OperationGroup grou
  this.Group = group ?? OperationGroup.Create(this);
  this.Continuations = new Queue<Action>();
  this.VisitedCallSites = new List<string>();
+ this.AwaitedResources = new HashSet<Guid>();
  this.SyncEvent = new ManualResetEventSlim(false);
  this.LastSchedulingPoint = SchedulingPointType.Start;
  this.LastHashedProgramState = 0;
@@ -187,30 +194,6 @@ internal ControlledOperation(ulong operationId, string name, OperationGroup grou
  this.Runtime.RegisterNewOperation(this);
  }
 
- /// <summary>
- /// Pauses the execution of this operation until it receives a signal.
- /// </summary>
- /// <remarks>
- /// It is assumed that this method is invoked by the same thread executing this operation.
- /// </remarks>
- internal void WaitSignal()
- {
- try
- {
- this.SyncEvent.Wait();
- this.SyncEvent.Reset();
- }
- catch (ObjectDisposedException)
- {
- // The handler was disposed, so we can ignore this exception.
- }
- }
-
- /// <summary>
- /// Signals this operation to resume its execution.
- /// </summary>
- internal void Signal() => this.SyncEvent.Set();
-
  /// <summary>
  /// Pauses this operation and sets a callback that returns true when the
  /// dependency causing the pause has been resolved.
@@ -232,6 +215,24 @@ internal void PauseWithDelay(uint delay)
  this.DelayedStepsCount = delay > int.MaxValue ? int.MaxValue : (int)delay;
  }
 
+ /// <summary>
+ /// Pauses this operation until the specified resource is released.
+ /// </summary>
+ internal void PauseWithResource(Guid resourceId)
+ {
+ this.Status = OperationStatus.PausedOnAllResources;
+ this.AwaitedResources.Add(resourceId);
+ }
+
+ /// <summary>
+ /// Pauses this operation until any or all of the specified resources are released.
+ /// </summary>
+ internal void PauseWithResources(IEnumerable<Guid> resourceIds, bool waitForAll)
+ {
+ this.Status = waitForAll ? OperationStatus.PausedOnAllResources : OperationStatus.PausedOnAnyResource;
+ this.AwaitedResources.UnionWith(resourceIds);
+ }
+
  /// <summary>
  /// Tries to enable this operation if its dependency has been resolved.
  /// </summary>
@@ -247,6 +248,34 @@ internal bool TryEnable()
  return this.Status is OperationStatus.Enabled;
  }
 
+ /// <summary>
+ /// Tries to enable this operation if all the resources it is waiting for have been signaled.
+ /// </summary>
+ internal bool TryEnable(Guid resourceId)
+ {
+ bool enabled = false;
+ if (this.AwaitedResources.Contains(resourceId))
+ {
+ if (this.Status is OperationStatus.PausedOnAnyResource)
+ {
+ this.AwaitedResources.Clear();
+ this.Status = OperationStatus.Enabled;
+ enabled = true;
+ }
+ else if (this.Status is OperationStatus.PausedOnAllResources)
+ {
+ this.AwaitedResources.Remove(resourceId);
+ if (this.AwaitedResources.Count is 0)
+ {
+ this.Status = OperationStatus.Enabled;
+ enabled = true;
+ }
+ }
+ }
+
+ return enabled;
+ }
+
  /// <summary>
  /// Sets a callback that executes the next continuation of this operation.
  /// </summary>
@@ -266,6 +295,30 @@ internal void ExecuteContinuations()
  }
  }
 
+ /// <summary>
+ /// Pauses the execution of this operation until it receives a signal.
+ /// </summary>
+ /// <remarks>
+ /// It is assumed that this method is invoked by the same thread executing this operation.
+ /// </remarks>
+ internal void WaitSignal()
+ {
+ try
+ {
+ this.SyncEvent.Wait();
+ this.SyncEvent.Reset();
+ }
+ catch (ObjectDisposedException)
+ {
+ // The handler was disposed, so we can ignore this exception.
+ }
+ }
+
+ /// <summary>
+ /// Signals this operation to resume its execution.
+ /// </summary>
+ internal void Signal() => this.SyncEvent.Set();
+
  /// <summary>
  /// Registers the specified call site as visited.
  /// </summary>

Source/Core/Runtime/Operations/OperationStatus.cs

@@ -29,9 +29,14 @@ internal enum OperationStatus
  PausedOnDelay,
 
  /// <summary>
- /// The operation is paused until it acquires a resource.
+ /// The operation is paused until it gets signaled by any awaited resource.
  /// </summary>
- PausedOnResource,
+ PausedOnAnyResource,
+
+ /// <summary>
+ /// The operation is paused until it gets signaled by all awaited resources.
+ /// </summary>
+ PausedOnAllResources,
 
  /// <summary>
  /// The operation is paused until receives an event.

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

@@ -82,6 +82,10 @@ internal TypeRewritingPass(RewritingOptions options, IEnumerable<AssemblyInfo> v
  this.KnownTypes[NameCache.Monitor] = typeof(Types.Threading.Monitor);
  this.KnownTypes[NameCache.SemaphoreSlim] = typeof(Types.Threading.SemaphoreSlim);
  this.KnownTypes[NameCache.Interlocked] = typeof(Types.Threading.Interlocked);
+ this.KnownTypes[NameCache.AutoResetEvent] = typeof(Types.Threading.AutoResetEvent);
+ this.KnownTypes[NameCache.ManualResetEvent] = typeof(Types.Threading.ManualResetEvent);
+ this.KnownTypes[NameCache.EventWaitHandle] = typeof(Types.Threading.EventWaitHandle);
+ this.KnownTypes[NameCache.WaitHandle] = typeof(Types.Threading.WaitHandle);
 
 #if NET || NETCOREAPP3_1
  // Populate the map with the known HTTP and web-related types.

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

@@ -144,9 +144,18 @@ member.Name is nameof(System.Threading.ThreadPool.UnsafeRegisterWaitForSingleObj
  {
  return true;
  }
- else if (type.Name is nameof(System.Threading.EventWaitHandle) ||
- type.Name is nameof(System.Threading.ExecutionContext) ||
- type.Name is nameof(System.Threading.ManualResetEvent) ||
+ else if (type.Name is nameof(System.Threading.EventWaitHandle) && member != null &&
+ (member.Name is nameof(System.Threading.EventWaitHandle.OpenExisting) ||
+ member.Name is nameof(System.Threading.EventWaitHandle.TryOpenExisting)))
+ {
+ return true;
+ }
+ else if (type.Name is nameof(System.Threading.WaitHandle) && member != null &&
+ (member.Name is nameof(System.Threading.WaitHandle.SignalAndWait)))
+ {
+ return true;
+ }
+ else if (type.Name is nameof(System.Threading.ExecutionContext) ||
  type.Name is nameof(System.Threading.ManualResetEventSlim) ||
  type.Name is nameof(System.Threading.Mutex) ||
  type.Name is nameof(System.Threading.ReaderWriterLock) ||
@@ -156,8 +165,7 @@ type.Name is nameof(System.Threading.Semaphore) ||
  type.Name is nameof(System.Threading.SpinLock) ||
  type.Name is nameof(System.Threading.SpinWait) ||
  type.Name is nameof(System.Threading.SynchronizationContext) ||
- type.Name is nameof(System.Threading.Timer) ||
- type.Name is nameof(System.Threading.WaitHandle))
+ type.Name is nameof(System.Threading.Timer))
  {
  return true;
  }

Source/Test/Rewriting/Types/NameCache.cs

@@ -73,6 +73,10 @@ internal static class NameCache
  internal static string Monitor { get; } = typeof(SystemThreading.Monitor).FullName;
  internal static string SemaphoreSlim { get; } = typeof(SystemThreading.SemaphoreSlim).FullName;
  internal static string Interlocked { get; } = typeof(SystemThreading.Interlocked).FullName;
+ internal static string AutoResetEvent { get; } = typeof(SystemThreading.AutoResetEvent).FullName;
+ internal static string ManualResetEvent { get; } = typeof(SystemThreading.ManualResetEvent).FullName;
+ internal static string EventWaitHandle { get; } = typeof(SystemThreading.EventWaitHandle).FullName;
+ internal static string WaitHandle { get; } = typeof(SystemThreading.WaitHandle).FullName;
 
  internal static string GenericList { get; } = typeof(SystemGenericCollections.List<>).FullName;
  internal static string GenericDictionary { get; } = typeof(SystemGenericCollections.Dictionary<,>).FullName;

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

@@ -0,0 +1,50 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using Microsoft.Coyote.Runtime;
+using SystemAutoResetEvent = System.Threading.AutoResetEvent;
+using SystemEventResetMode = System.Threading.EventResetMode;
+using SystemWaitHandle = System.Threading.WaitHandle;
+
+namespace Microsoft.Coyote.Rewriting.Types.Threading
+{
+ /// <summary>
+ /// Represents a thread synchronization event that, when signaled, resets automatically
+ /// after releasing a single waiting thread.
+ /// </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 AutoResetEvent
+ {
+ /// <summary>
+ /// Initializes a new instance of the <see cref="AutoResetEvent"/> class, with a value
+ /// indicating whether to set the initial state to signaled.
+ /// </summary>
+ public static SystemAutoResetEvent Create(bool initialState)
+ {
+ var instance = new SystemAutoResetEvent(initialState);
+ var runtime = CoyoteRuntime.Current;
+ if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving)
+ {
+ Resource resource = new Resource(runtime, instance, initialState);
+ Resource.Add(resource);
+ }
+
+ return instance;
+ }
+
+ /// <summary>
+ /// Resource that is used to control a <see cref="SystemAutoResetEvent"/> during testing.
+ /// </summary>
+ internal class Resource : EventWaitHandle.Resource
+ {
+ /// <summary>
+ /// Initializes a new instance of the <see cref="Resource"/> class.
+ /// </summary>
+ internal Resource(CoyoteRuntime runtime, SystemWaitHandle handle, bool initialState)
+ : base(runtime, handle, initialState, SystemEventResetMode.AutoReset)
+ {
+ }
+ }
+ }
+}