Dhruv/rl fuzzing

Source/Core/Runtime/CoyoteRuntime.cs

@@ -441,7 +441,7 @@ internal void Schedule(Action callback)
 
                     if (this.SchedulingPolicy is SchedulingPolicy.Fuzzing)
                     {
-                        this.DelayOperation();
+                        // this.DelayOperation();
                     }
 
                     callback();
@@ -504,7 +504,7 @@ internal void ScheduleTask(Task task)
 
                     if (this.SchedulingPolicy is SchedulingPolicy.Fuzzing)
                     {
-                        this.DelayOperation();
+                        // this.DelayOperation();
                     }
 
                     this.ControlledTaskScheduler.ExecuteTask(task);
@@ -911,34 +911,50 @@ internal void ResumeScheduling()
         /// <summary>
         /// Delays the currently executing operation for a nondeterministically chosen amount of time.
         /// </summary>
+        /// <param name="positiveDelay"> Choice to keep delays positive.</param>
         /// <remarks>
         /// The delay is chosen nondeterministically by an underlying fuzzing strategy.
         /// If a delay of 0 is chosen, then the operation is not delayed.
         /// </remarks>
-        internal void DelayOperation()
+        internal void DelayOperation(bool positiveDelay = false)
         {
+        RecursiveDelay:
             int delay = 0;
+            int numDelays = 0;
+            AsyncOperation current = null;
             lock (this.SyncObject)
             {
                 if (!this.IsAttached)
                 {
                     throw new ThreadInterruptedException();
                 }
 
-                var current = this.GetExecutingOperation<AsyncOperation>();
+                current = this.GetExecutingOperation<AsyncOperation>();
                 if (current != null)
                 {
                     // Choose the next delay to inject. The value is in milliseconds.
-                    delay = this.GetNondeterministicDelay(current, (int)this.Configuration.TimeoutDelay);
+                    delay = this.GetNondeterministicDelay(current, (int)this.Configuration.TimeoutDelay,
+                        numDelays > 0, positiveDelay);
                     IO.Debug.WriteLine("<CoyoteDebug> Delaying operation '{0}' on thread '{1}' by {2}ms.",
                         current.Name, Thread.CurrentThread.ManagedThreadId, delay);
                 }
-            }
 
-            if (delay > 0)
-            {
-                // Only sleep if a non-zero delay was chosen.
-                Thread.Sleep(delay);
+                // Only sleep the executing operation if a non-zero delay was chosen.
+                if (delay > 0 && current != null)
+                {
+                    var previousStatus = current.Status;
+                    current.Status = AsyncOperationStatus.Delayed;
+                    // Thread.Sleep(delay);
+                    SyncMonitor.Wait(this.SyncObject, delay);
+                    current.Status = previousStatus;
+                    numDelays++;
+                    goto RecursiveDelay;
+                    // // Choose whether to delay the executing operation for longer. If true, positively delay the operation.
+                    // if (this.Scheduler.GetNextRecursiveDelayChoice(this.OperationMap.Values, current))
+                    // {
+                    //     this.DelayOperation(true);
+                    // }
+                }
             }
         }
 
@@ -1021,7 +1037,7 @@ internal int GetNextNondeterministicIntegerChoice(int maxValue)
         /// <summary>
         /// Returns a controlled nondeterministic delay for the specified operation.
         /// </summary>
-        private int GetNondeterministicDelay(AsyncOperation op, int maxValue)
+        private int GetNondeterministicDelay(AsyncOperation op, int maxValue, bool isRecursive = false, bool positiveDelay = false)
         {
             lock (this.SyncObject)
             {
@@ -1030,7 +1046,7 @@ private int GetNondeterministicDelay(AsyncOperation op, int maxValue)
 
                 // Choose the next delay to inject.
                 int maxDelay = maxValue > 0 ? (int)this.Configuration.TimeoutDelay : 1;
-                if (!this.Scheduler.GetNextDelay(op, maxDelay, out int next))
+                if (!this.Scheduler.GetNextDelay(this.OperationMap.Values, op, maxDelay, positiveDelay, isRecursive, out int next))
                 {
                     this.Detach(SchedulerDetachmentReason.BoundReached);
                 }
@@ -1251,7 +1267,7 @@ internal TAsyncOperation GetOperationWithId<TAsyncOperation>(ulong id)
         /// This operation is thread safe because the systematic testing
         /// runtime serializes the execution.
         /// </remarks>
-        internal IEnumerable<AsyncOperation> GetRegisteredOperations()
+        private IEnumerable<AsyncOperation> GetRegisteredOperations()
         {
             lock (this.SyncObject)
             {

Source/Core/Runtime/Scheduling/OperationScheduler.cs

@@ -164,12 +164,24 @@ internal void SetSpecificationEngine(SpecificationEngine specificationEngine)
         /// <summary>
         /// Returns the next delay.
         /// </summary>
+        /// <param name="ops">Operations executing during the current test iteration.</param>
         /// <param name="current">The operation requesting the delay.</param>
         /// <param name="maxValue">The max value.</param>
+        /// <param name="positiveDelay">Choice for positive delays.</param>
+        /// <param name="isRecursive">...</param>
         /// <param name="next">The next delay.</param>
         /// <returns>True if there is a next delay, else false.</returns>
-        internal bool GetNextDelay(AsyncOperation current, int maxValue, out int next) =>
-            (this.Strategy as FuzzingStrategy).GetNextDelay(current, maxValue, out next);
+        internal bool GetNextDelay(IEnumerable<AsyncOperation> ops, AsyncOperation current, int maxValue,
+            bool positiveDelay, bool isRecursive, out int next) =>
+            (this.Strategy as FuzzingStrategy).GetNextDelay(ops, current, maxValue, positiveDelay, isRecursive, out next);
+
+        /// <summary>
+        /// Chooses whether to delay the current operation for longer.
+        /// </summary>
+        /// <param name="ops">Operations executing during the current test iteration.</param>
+        /// <param name="current">The operation requesting the delay.</param>
+        internal bool GetNextRecursiveDelayChoice(IEnumerable<AsyncOperation> ops, AsyncOperation current) =>
+            (this.Strategy as FuzzingStrategy).GetNextRecursiveDelayChoice(ops, current);
 
         /// <summary>
         /// Returns a description of the scheduling strategy in text format.

Source/Core/Testing/Fuzzing/BoundedRandomStrategy.cs

@@ -3,6 +3,7 @@
 
 using System;
 using System.Collections.Concurrent;
+using System.Collections.Generic;
 using Microsoft.Coyote.Runtime;
 
 namespace Microsoft.Coyote.Testing.Fuzzing
@@ -55,7 +56,7 @@ internal override bool InitializeNextIteration(uint iteration)
         /// The delay has an injection probability of 0.05 and is in the range of [10, maxValue * 10]
         /// with an increment of 10 and an upper bound of 5000ms per operation.
         /// </remarks>
-        internal override bool GetNextDelay(AsyncOperation current, int maxValue, out int next)
+        internal override bool GetNextDelay(IEnumerable<AsyncOperation> ops, AsyncOperation current, int maxValue, bool positiveDelay, bool isRecursive, out int next)
         {
             Guid id = this.GetOperationId();
 
@@ -78,10 +79,19 @@ internal override bool GetNextDelay(AsyncOperation current, int maxValue, out in
                 this.TotalTaskDelayMap.TryUpdate(id, maxDelay + next, maxDelay);
             }
 
-            this.StepCount++;
+            if (!isRecursive)
+            {
+                this.StepCount++;
+            }
+
             return true;
         }
 
+        internal override bool GetNextRecursiveDelayChoice(IEnumerable<AsyncOperation> ops, AsyncOperation current)
+        {
+            return this.RandomValueGenerator.Next(2) is 0 ? true : false;
+        }
+
         /// <inheritdoc/>
         internal override int GetStepCount() => this.StepCount;
 

Source/Core/Testing/Fuzzing/FuzzingStrategy.cs

@@ -3,6 +3,7 @@
 
 using System;
 using System.Collections.Concurrent;
+using System.Collections.Generic;
 using System.Threading;
 using System.Threading.Tasks;
 using Microsoft.Coyote.Runtime;
@@ -39,22 +40,36 @@ internal static FuzzingStrategy Create(Configuration configuration, IRandomValue
         {
             switch (configuration.SchedulingStrategy)
             {
+                case "rl":
+                    return new QLearningStrategy(configuration.MaxUnfairSchedulingSteps, generator);
                 case "pct":
                     return new PCTStrategy(configuration.MaxUnfairSchedulingSteps, generator, configuration.StrategyBound);
                 default:
-                    // return new RandomStrategy(configuration.MaxFairSchedulingSteps, generator);
-                    return new BoundedRandomStrategy(configuration.MaxUnfairSchedulingSteps, generator);
+                    // return new BoundedRandomStrategy(configuration.MaxUnfairSchedulingSteps, generator);
+                    return new RandomStrategy(configuration.MaxFairSchedulingSteps, generator);
             }
         }
 
         /// <summary>
         /// Returns the next delay.
         /// </summary>
+        /// <param name="ops">Operations executing during the current test iteration.</param>
         /// <param name="current">The operation requesting the delay.</param>
         /// <param name="maxValue">The max value.</param>
+        /// <param name="positiveDelay">Choice for positive delays.</param>
+        /// <param name="isRecursive">...</param>
         /// <param name="next">The next delay.</param>
         /// <returns>True if there is a next delay, else false.</returns>
-        internal abstract bool GetNextDelay(AsyncOperation current, int maxValue, out int next);
+        internal abstract bool GetNextDelay(IEnumerable<AsyncOperation> ops, AsyncOperation current,
+            int maxValue, bool positiveDelay, bool isRecursive, out int next);
+
+        /// <summary>
+        /// Returns a boolean choice to delay the current operation further.
+        /// </summary>
+        /// <param name="ops">Operations executing during the current test iteration.</param>
+        /// <param name="current">The operation requesting the delay.</param>
+        /// <returns>True if current operation should be delayed further, ekse false.</returns>
+        internal abstract bool GetNextRecursiveDelayChoice(IEnumerable<AsyncOperation> ops, AsyncOperation current);
 
         /// <summary>
         /// Returns the current operation id.