diff --git a/Source/Core/Runtime/CoyoteRuntime.cs b/Source/Core/Runtime/CoyoteRuntime.cs
index 2d4bad4cb..324bce2b8 100644
--- a/Source/Core/Runtime/CoyoteRuntime.cs
+++ b/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,13 +911,17 @@ internal void ResumeScheduling()
///
/// Delays the currently executing operation for a nondeterministically chosen amount of time.
///
+ /// Choice to keep delays positive.
///
/// The delay is chosen nondeterministically by an underlying fuzzing strategy.
/// If a delay of 0 is chosen, then the operation is not delayed.
///
- 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)
@@ -925,20 +929,32 @@ internal void DelayOperation()
throw new ThreadInterruptedException();
}
- var current = this.GetExecutingOperation();
+ current = this.GetExecutingOperation();
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(" 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)
///
/// Returns a controlled nondeterministic delay for the specified operation.
///
- 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(ulong id)
/// This operation is thread safe because the systematic testing
/// runtime serializes the execution.
///
- internal IEnumerable GetRegisteredOperations()
+ private IEnumerable GetRegisteredOperations()
{
lock (this.SyncObject)
{
diff --git a/Source/Core/Runtime/Scheduling/OperationScheduler.cs b/Source/Core/Runtime/Scheduling/OperationScheduler.cs
index a8e701433..8ac19899a 100644
--- a/Source/Core/Runtime/Scheduling/OperationScheduler.cs
+++ b/Source/Core/Runtime/Scheduling/OperationScheduler.cs
@@ -164,12 +164,24 @@ internal bool GetNextIntegerChoice(AsyncOperation current, int maxValue, out int
///
/// Returns the next delay.
///
+ /// Operations executing during the current test iteration.
/// The operation requesting the delay.
/// The max value.
+ /// Choice for positive delays.
+ /// ...
/// The next delay.
/// True if there is a next delay, else false.
- internal bool GetNextDelay(AsyncOperation current, int maxValue, out int next) =>
- (this.Strategy as FuzzingStrategy).GetNextDelay(current, maxValue, out next);
+ internal bool GetNextDelay(IEnumerable ops, AsyncOperation current, int maxValue,
+ bool positiveDelay, bool isRecursive, out int next) =>
+ (this.Strategy as FuzzingStrategy).GetNextDelay(ops, current, maxValue, positiveDelay, isRecursive, out next);
+
+ ///
+ /// Chooses whether to delay the current operation for longer.
+ ///
+ /// Operations executing during the current test iteration.
+ /// The operation requesting the delay.
+ internal bool GetNextRecursiveDelayChoice(IEnumerable ops, AsyncOperation current) =>
+ (this.Strategy as FuzzingStrategy).GetNextRecursiveDelayChoice(ops, current);
///
/// Returns a description of the scheduling strategy in text format.
diff --git a/Source/Core/Testing/Fuzzing/BoundedRandomStrategy.cs b/Source/Core/Testing/Fuzzing/BoundedRandomStrategy.cs
index 493d5ea59..5413098de 100644
--- a/Source/Core/Testing/Fuzzing/BoundedRandomStrategy.cs
+++ b/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.
///
- internal override bool GetNextDelay(AsyncOperation current, int maxValue, out int next)
+ internal override bool GetNextDelay(IEnumerable 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 ops, AsyncOperation current)
+ {
+ return this.RandomValueGenerator.Next(2) is 0 ? true : false;
+ }
+
///
internal override int GetStepCount() => this.StepCount;
diff --git a/Source/Core/Testing/Fuzzing/FuzzingStrategy.cs b/Source/Core/Testing/Fuzzing/FuzzingStrategy.cs
index 83919cb80..42f8127b1 100644
--- a/Source/Core/Testing/Fuzzing/FuzzingStrategy.cs
+++ b/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);
}
}
///
/// Returns the next delay.
///
+ /// Operations executing during the current test iteration.
/// The operation requesting the delay.
/// The max value.
+ /// Choice for positive delays.
+ /// ...
/// The next delay.
/// True if there is a next delay, else false.
- internal abstract bool GetNextDelay(AsyncOperation current, int maxValue, out int next);
+ internal abstract bool GetNextDelay(IEnumerable ops, AsyncOperation current,
+ int maxValue, bool positiveDelay, bool isRecursive, out int next);
+
+ ///
+ /// Returns a boolean choice to delay the current operation further.
+ ///
+ /// Operations executing during the current test iteration.
+ /// The operation requesting the delay.
+ /// True if current operation should be delayed further, ekse false.
+ internal abstract bool GetNextRecursiveDelayChoice(IEnumerable ops, AsyncOperation current);
///
/// Returns the current operation id.
diff --git a/Source/Core/Testing/Fuzzing/PCTStrategy.cs b/Source/Core/Testing/Fuzzing/PCTStrategy.cs
index f4d0dfe9d..197517e70 100644
--- a/Source/Core/Testing/Fuzzing/PCTStrategy.cs
+++ b/Source/Core/Testing/Fuzzing/PCTStrategy.cs
@@ -3,119 +3,310 @@
using System;
using System.Collections.Generic;
+using System.Linq;
+using Microsoft.Coyote.IO;
using Microsoft.Coyote.Runtime;
namespace Microsoft.Coyote.Testing.Fuzzing
{
///
- /// A probabilistic fuzzing strategy.
+ /// A probabilistic priority-based scheduling strategy.
///
- internal class PCTStrategy : FuzzingStrategy
+ ///
+ /// This strategy is described in the following paper:
+ /// https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/asplos277-pct.pdf.
+ ///
+ internal sealed class PCTStrategy : FuzzingStrategy
{
///
/// Random value generator.
///
- protected IRandomValueGenerator RandomValueGenerator;
+ private readonly IRandomValueGenerator RandomValueGenerator;
///
/// The maximum number of steps to explore.
///
- protected readonly int MaxSteps;
+ private readonly int MaxSteps;
///
- /// The maximum number of steps after which we should reshuffle the probabilities.
+ /// The number of exploration steps.
///
- protected readonly int PriorityChangePoints;
+ private int StepCount;
///
- /// Set of low priority operations.
+ /// Max number of priority switch points.
///
- ///
- /// Tasks in this set will experience more delay.
- ///
- private readonly List LowPrioritySet;
+ private readonly int MaxPrioritySwitchPoints;
///
- /// Set of high priority operations.
+ /// Approximate length of the schedule across all iterations.
///
- private readonly List HighPrioritySet;
+ private int ScheduleLength;
///
- /// Probability with which operations should be alloted to the low priority set.
+ /// List of prioritized operations.
///
- private double LowPriorityProbability;
+ private List PrioritizedOperations;
///
- /// The number of exploration steps.
+ /// List of operations that have made critical delay requests post creation.
///
- protected int StepCount;
+ private Dictionary CriticalDelayRequest;
+
+ ///
+ /// Scheduling points in the current execution where a priority change should occur.
+ ///
+ private readonly HashSet PriorityChangePoints;
///
/// Initializes a new instance of the class.
///
- internal PCTStrategy(int maxDelays, IRandomValueGenerator random, int priorityChangePoints)
+ internal PCTStrategy(int maxSteps, IRandomValueGenerator generator, int maxPrioritySwitchPoints)
{
- this.RandomValueGenerator = random;
- this.MaxSteps = maxDelays;
- this.PriorityChangePoints = priorityChangePoints;
- this.HighPrioritySet = new List();
- this.LowPrioritySet = new List();
- this.LowPriorityProbability = 0;
+ this.RandomValueGenerator = generator;
+ this.MaxSteps = maxSteps;
+ this.StepCount = 0;
+ this.ScheduleLength = 0;
+ this.MaxPrioritySwitchPoints = maxPrioritySwitchPoints;
+ this.PrioritizedOperations = new List();
+ this.PriorityChangePoints = new HashSet();
+ this.CriticalDelayRequest = new Dictionary();
}
///
internal override bool InitializeNextIteration(uint iteration)
{
- this.StepCount = 0;
- this.LowPrioritySet.Clear();
- this.HighPrioritySet.Clear();
+ // The first iteration has no knowledge of the execution, so only initialize from the second
+ // iteration and onwards. Note that although we could initialize the first length based on a
+ // heuristic, its not worth it, as the strategy will typically explore thousands of iterations,
+ // plus its also interesting to explore a schedule with no forced priority switch points.
+ if (iteration > 0)
+ {
+ this.ScheduleLength = Math.Max(this.ScheduleLength, this.StepCount);
+ this.StepCount = 0;
+
+ this.PrioritizedOperations.Clear();
+ this.PriorityChangePoints.Clear();
+ // Remove the operations that do not make critical delay requests
+ this.CriticalDelayRequest = this.CriticalDelayRequest.Where(kvp => kvp.Value).ToDictionary(op => op.Key, op => op.Value);
+
+ var range = Enumerable.Range(0, this.ScheduleLength);
+ foreach (int point in this.Shuffle(range).Take(this.MaxPrioritySwitchPoints))
+ {
+ this.PriorityChangePoints.Add(point);
+ }
- // Change the probability of a task to be assigned to the low priority set after each iteration.
- this.LowPriorityProbability = this.LowPriorityProbability >= 0.8 ? 0 : this.LowPriorityProbability + 0.1;
+ this.DebugPrintPriorityChangePoints();
+ }
return true;
}
- ///
- internal override bool GetNextDelay(AsyncOperation current, int maxValue, out int next)
+ internal override bool GetNextDelay(IEnumerable ops, AsyncOperation current,
+ int maxValue, bool positiveDelay, bool isRecursive, out int next)
{
- Guid id = this.GetOperationId();
+ Console.WriteLine($"Current operation: {current.Name}");
- this.StepCount++;
-
- // Reshuffle the probabilities after every (this.MaxSteps / this.PriorityChangePoints) steps.
- if (this.StepCount % (this.MaxSteps / this.PriorityChangePoints) == 0)
+ // if all operations except current have acquired statuses that are perpetually blocked, then assign zero delay
+ if (ops.Where(op => !op.Equals(current) &&
+ (op.Status is AsyncOperationStatus.Delayed || op.Status is AsyncOperationStatus.Enabled)).Count() is 0)
{
- this.LowPrioritySet.Clear();
- this.HighPrioritySet.Clear();
+ next = 0;
+ // Count as step only if the operation belongs to the benchmark
+ this.StepCount += (current.Name is "'Task(0)'") ? 0 : 1;
+ return true;
}
- // If this task is not assigned to any priority set, then randomly assign it to one of the two sets.
- if (!this.LowPrioritySet.Contains(id) && !this.HighPrioritySet.Contains(id))
+ // if the operation has not yet asked a critical delay request, include it as a potential operation
+ // (critical request status: false).
+ // If it has been included already, then update its critical request status to true
+ if (!isRecursive)
{
- if (this.RandomValueGenerator.NextDouble() < this.LowPriorityProbability)
+ if (!this.CriticalDelayRequest.ContainsKey(current))
{
- this.LowPrioritySet.Add(id);
+ this.CriticalDelayRequest[current] = false;
}
else
{
- this.HighPrioritySet.Add(id);
+ this.CriticalDelayRequest[current] = true;
}
}
- // Choose a random delay if this task is in the low priority set.
- if (this.LowPrioritySet.Contains(id))
+ // Console.WriteLine($"Freq: {this.CriticalDelayRequest[current].ToString()}");
+ // Console.WriteLine($"OpId: {current.Id} Status: {current.Status}");
+
+ // Update the priority list with new operations and return the highest priority operation
+ this.UpdateAndGetHighestPriorityEnabledOperation(ops, current, out AsyncOperation highestEnabledOperation);
+
+ // Console.WriteLine($"{highestEnabledOperation.Name}");
+
+ // if the current operation is making a non-critical request (request for delay before creation) then assign zero delay.
+ // In a message passing system operation creation delay does not make a difference.
+ if (!this.CriticalDelayRequest[current])
{
- next = this.RandomValueGenerator.Next(maxValue) * 5;
+ next = 0;
+ this.StepCount += (current.Name is "'Task(0)'") ? 0 : 1;
+ return true;
}
- else
+
+ // Assign zero delay if the current operation is the highest enabled operation otherwise delay it.
+ if (highestEnabledOperation.Equals(current))
{
next = 0;
}
+ else
+ {
+ next = 1;
+ }
+
+ // if the current delay request is a primary one, then increase the step count indicating that the opn was scheduled.
+ // The operation can get out of recursive loop only if it chooses a zero delay.
+ // However, we increase step count even when the operation might never get out of the loop and hence get scheduled.
+ // The only cost for this inaccuracy is redundant consumption of step count by at most #(total operations).
+ if (!isRecursive)
+ {
+ this.StepCount += (current.Name is "'Task(0)'") ? 0 : 1;
+ }
return true;
}
+ internal override bool GetNextRecursiveDelayChoice(IEnumerable ops, AsyncOperation current)
+ {
+ this.UpdateAndGetHighestPriorityEnabledOperation(ops, current, out AsyncOperation highestEnabledOperation);
+
+ if (highestEnabledOperation.Equals(current))
+ {
+ return true;
+ }
+
+ return this.RandomValueGenerator.Next(2) is 0 ? true : false;
+ }
+
+ ///
+ internal bool UpdateAndGetHighestPriorityEnabledOperation(IEnumerable ops, AsyncOperation current,
+ out AsyncOperation highestEnabledOperation)
+ {
+ highestEnabledOperation = null;
+ // enumerate all operations which are either sleeping or enabled and have made a critical delay request so far.
+ var criticalOps = ops.Where(op
+ => (op.Status is AsyncOperationStatus.Enabled || op.Status is AsyncOperationStatus.Delayed) &&
+ this.CriticalDelayRequest.ContainsKey(op) && this.CriticalDelayRequest[op]).ToList();
+
+ if (criticalOps.Count is 0)
+ {
+ return false;
+ }
+
+ this.SetNewOperationPriorities(criticalOps, current);
+ this.DeprioritizeEnabledOperationWithHighestPriority(criticalOps);
+ this.DebugPrintOperationPriorityList();
+
+ // highestEnabledOperation = this.GetEnabledOperationWithLowestPriority(criticalOps); // Case: (n-1) PCT
+ highestEnabledOperation = this.GetEnabledOperationWithHighestPriority(criticalOps); // Case: (1) PCT
+ return true;
+ }
+
+ ///
+ /// Sets the priority of new operations, if there are any.
+ ///
+ private void SetNewOperationPriorities(List ops, AsyncOperation current)
+ {
+ if (this.PrioritizedOperations.Count is 0)
+ {
+ this.PrioritizedOperations.Add(current);
+ }
+
+ // Randomize the priority of all new operations.
+ foreach (var op in ops.Where(op => !this.PrioritizedOperations.Contains(op)))
+ {
+ // Randomly choose a priority for this operation between the lowest and the highest priority.
+ int index = this.RandomValueGenerator.Next(this.PrioritizedOperations.Count) + 1;
+ this.PrioritizedOperations.Insert(index, op);
+ Debug.WriteLine(" chose priority '{0}' for new operation '{1}'.", index, op.Name);
+ }
+ }
+
+ ///
+ /// Deprioritizes the enabled operation with the highest priority, if there is a
+ /// priotity change point installed on the current execution step.
+ ///
+ private void DeprioritizeEnabledOperationWithHighestPriority(List ops)
+ {
+ if (ops.Count <= 1)
+ {
+ // Nothing to do, there is only one enabled operation available.
+ return;
+ }
+
+ AsyncOperation deprioritizedOperation = null;
+ if (this.PriorityChangePoints.Contains(this.StepCount))
+ {
+ // This scheduling step was chosen as a priority switch point.
+ deprioritizedOperation = this.GetEnabledOperationWithHighestPriority(ops);
+ Debug.WriteLine(" operation '{0}' is deprioritized.", deprioritizedOperation.Name);
+ }
+
+ if (deprioritizedOperation != null)
+ {
+ // Deprioritize the operation by putting it in the end of the list.
+ this.PrioritizedOperations.Remove(deprioritizedOperation);
+ this.PrioritizedOperations.Add(deprioritizedOperation);
+ }
+ }
+
+ ///
+ /// Returns the enabled operation with the lowest priority.
+ ///
+ private AsyncOperation GetEnabledOperationWithLowestPriority(List ops)
+ {
+ foreach (var entity in this.PrioritizedOperations.Reverse())
+ {
+ if (ops.Any(m => m == entity))
+ {
+ return entity;
+ }
+ }
+
+ return null;
+ }
+
+ ///
+ /// Returns the enabled operation with the highest priority.
+ ///
+ private AsyncOperation GetEnabledOperationWithHighestPriority(List ops)
+ {
+ foreach (var entity in this.PrioritizedOperations)
+ {
+ if (ops.Any(m => m == entity))
+ {
+ return entity;
+ }
+ }
+
+ return null;
+ }
+
+ // ///
+ // internal override bool GetNextBooleanChoice(AsyncOperation current, int maxValue, out bool next)
+ // {
+ // next = false;
+ // if (this.RandomValueGenerator.Next(maxValue) is 0)
+ // {
+ // next = true;
+ // }
+ // this.StepCount++;
+ // return true;
+ // }
+
+ // ///
+ // internal override bool GetNextIntegerChoice(AsyncOperation current, int maxValue, out int next)
+ // {
+ // next = this.RandomValueGenerator.Next(maxValue);
+ // this.StepCount++;
+ // return true;
+ // }
+
///
internal override int GetStepCount() => this.StepCount;
@@ -131,9 +322,79 @@ internal override bool IsMaxStepsReached()
}
///
- internal override bool IsFair() => true;
+ internal override bool IsFair() => false;
///
- internal override string GetDescription() => $"pct[seed '{this.RandomValueGenerator.Seed}']";
+ internal override string GetDescription()
+ {
+ var text = $"pct[seed '" + this.RandomValueGenerator.Seed + "']";
+ return text;
+ }
+
+ ///
+ /// Shuffles the specified range using the Fisher-Yates algorithm.
+ ///
+ ///
+ /// See https://en.wikipedia.org/wiki/Fisher%E2%80%93Yates_shuffle.
+ ///
+ private IList Shuffle(IEnumerable range)
+ {
+ var result = new List(range);
+ for (int idx = result.Count - 1; idx >= 1; idx--)
+ {
+ int point = this.RandomValueGenerator.Next(result.Count);
+ int temp = result[idx];
+ result[idx] = result[point];
+ result[point] = temp;
+ }
+
+ return result;
+ }
+
+ // ///
+ // internal override void Reset()
+ // {
+ // this.ScheduleLength = 0;
+ // this.StepCount = 0;
+ // this.PrioritizedOperations.Clear();
+ // this.PriorityChangePoints.Clear();
+ // }
+
+ ///
+ /// Print the operation priority list, if debug is enabled.
+ ///
+ private void DebugPrintOperationPriorityList()
+ {
+ if (Debug.IsEnabled)
+ {
+ Debug.Write(" operation priority list: ");
+ for (int idx = 0; idx < this.PrioritizedOperations.Count; idx++)
+ {
+ if (idx < this.PrioritizedOperations.Count - 1)
+ {
+ Debug.Write("'{0}', ", this.PrioritizedOperations[idx].Name);
+ }
+ else
+ {
+ Debug.WriteLine("'{0}'.", this.PrioritizedOperations[idx].Name);
+ }
+ }
+ }
+ }
+
+ ///
+ /// Print the priority change points, if debug is enabled.
+ ///
+ private void DebugPrintPriorityChangePoints()
+ {
+ if (Debug.IsEnabled)
+ {
+ // Sort them before printing for readability.
+ var sortedChangePoints = this.PriorityChangePoints.ToArray();
+ Array.Sort(sortedChangePoints);
+ Debug.WriteLine(" next priority change points ('{0}' in total): {1}",
+ sortedChangePoints.Length, string.Join(", ", sortedChangePoints));
+ }
+ }
}
}
diff --git a/Source/Core/Testing/Fuzzing/QLearningStrategy.cs b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs
new file mode 100644
index 000000000..7ea762d72
--- /dev/null
+++ b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs
@@ -0,0 +1,553 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using Microsoft.Coyote.Actors;
+using Microsoft.Coyote.Runtime;
+
+namespace Microsoft.Coyote.Testing.Fuzzing
+{
+ ///
+ /// A probabilistic scheduling strategy that uses Q-learning.
+ ///
+ internal sealed class QLearningStrategy : RandomStrategy
+ {
+ ///
+ /// Map from program states to a map from next operations to their quality values.
+ ///
+ private readonly Dictionary> OperationQTable;
+
+ ///
+ /// The path that is being executed during the current iteration. Each
+ /// step of the execution is represented by an operation and a value
+ /// representing the program state after the operation executed.
+ ///
+ private readonly LinkedList<(ulong op, AsyncOperationType type, int state)> ExecutionPath;
+
+ ///
+ /// Map from values representing program states to their transition
+ /// frequency in the current execution path.
+ ///
+ private readonly Dictionary TransitionFrequencies;
+
+ ///
+ /// The previously chosen operation.
+ ///
+ private ulong PreviousOperation;
+
+ ///
+ /// The value of the learning rate.
+ ///
+ private readonly double LearningRate;
+
+ ///
+ /// The value of the discount factor.
+ ///
+ private readonly double Gamma;
+
+ ///
+ /// The op value denoting a true boolean choice.
+ ///
+ private readonly ulong TrueChoiceOpValue;
+
+ ///
+ /// The op value denoting a false boolean choice.
+ ///
+ private readonly ulong FalseChoiceOpValue;
+
+ ///
+ /// The op value denoting the min integer choice.
+ ///
+ private readonly ulong MinIntegerChoiceOpValue;
+
+ ///
+ /// List of operations that have made critical delay requests post creation.
+ ///
+ private Dictionary CriticalDelayRequest;
+
+ ///
+ /// The basic action reward.
+ ///
+ private readonly double BasicActionReward;
+
+ ///
+ /// Number of times an operation asking for a delay has been snoozed recursively.
+ ///
+ private Dictionary RecursiveDelayCount;
+
+ ///
+ /// Hashes of the operations each computed at their last corresponding delay point.
+ ///
+ private Dictionary OperationHashes;
+
+ ///
+ /// The failure injection reward.
+ ///
+ private readonly double FailureInjectionReward;
+
+ ///
+ /// The number of explored executions.
+ ///
+ private int Epochs;
+
+ ///
+ /// Initializes a new instance of the class.
+ /// It uses the specified random number generator.
+ ///
+ public QLearningStrategy(int maxSteps, IRandomValueGenerator random)
+ : base(maxSteps, random)
+ {
+ this.OperationQTable = new Dictionary>();
+ this.ExecutionPath = new LinkedList<(ulong, AsyncOperationType, int)>();
+ this.TransitionFrequencies = new Dictionary();
+ this.PreviousOperation = 0;
+ this.LearningRate = 0.3;
+ this.Gamma = 0.7;
+ this.TrueChoiceOpValue = ulong.MaxValue;
+ this.FalseChoiceOpValue = ulong.MaxValue - 1;
+ this.MinIntegerChoiceOpValue = ulong.MaxValue - 2;
+ this.BasicActionReward = -1;
+ this.FailureInjectionReward = -1000;
+ this.Epochs = 0;
+ this.CriticalDelayRequest = new Dictionary();
+ this.RecursiveDelayCount = new Dictionary();
+ this.OperationHashes = new Dictionary();
+ }
+
+ ///
+ internal override bool GetNextDelay(IEnumerable ops, AsyncOperation current,
+ int maxValue, bool positiveDelay, bool isRecursive, out int next)
+ {
+ Console.WriteLine($"Current Operation: {current.Name}");
+
+ // if the operation has not yet asked a critical delay request, include it as a potential operation
+ // for scheduling.
+ // If it has been included already, then update its critical request status to true.
+ if (!isRecursive)
+ {
+ if (!this.CriticalDelayRequest.ContainsKey(current))
+ {
+ this.CriticalDelayRequest[current] = false;
+ }
+ else
+ {
+ this.CriticalDelayRequest[current] = true;
+ this.OperationHashes[current] = GetOperationHash(current);
+ }
+ }
+
+ // enumerate those operations which are not perpetually blocked. The current operation is enabled.
+ var enabledOps = ops.Where(op
+ => (op.Status is AsyncOperationStatus.Delayed || op.Status is AsyncOperationStatus.Enabled)
+ && this.CriticalDelayRequest.ContainsKey(op) && this.CriticalDelayRequest[op]);
+
+ this.GetNextOperation(enabledOps, current, out AsyncOperation nextOp);
+
+ if (nextOp is null)
+ {
+ next = 0;
+ }
+ else
+ {
+ if (nextOp.Equals(current))
+ {
+ next = 0;
+ this.PreviousOperation = nextOp.Id;
+ }
+ else
+ {
+ next = 1;
+
+ if (!this.RecursiveDelayCount.ContainsKey(current))
+ {
+ this.RecursiveDelayCount.Add(current, 0);
+ }
+
+ this.RecursiveDelayCount[current]++;
+ }
+ }
+
+ if (!isRecursive)
+ {
+ this.StepCount++;
+ }
+
+ return true;
+ }
+
+ ///
+ internal bool GetNextOperation(IEnumerable ops, AsyncOperation current, out AsyncOperation nextOp)
+ {
+ int state = this.CaptureExecutionStep(ops, current);
+ this.InitializeOperationQValues(state, ops);
+
+ if (ops.Count() is 0)
+ {
+ nextOp = null;
+ }
+ else
+ {
+ nextOp = this.GetNextOperationByPolicy(state, ops);
+ Console.WriteLine($"Chosen operation: {nextOp.Name}");
+ }
+
+ return true;
+ }
+
+ ///
+ internal bool GetNextBooleanChoice(IEnumerable ops, AsyncOperation current, out bool next)
+ {
+ int state = this.CaptureExecutionStep(ops, current);
+ this.InitializeBooleanChoiceQValues(state);
+
+ next = this.GetNextBooleanChoiceByPolicy(state);
+
+ this.PreviousOperation = next ? this.TrueChoiceOpValue : this.FalseChoiceOpValue;
+ this.StepCount++;
+ return true;
+ }
+
+ ///
+ internal bool GetNextIntegerChoice(IEnumerable ops, AsyncOperation current, int maxValue, out int next)
+ {
+ int state = this.CaptureExecutionStep(ops, current);
+ this.InitializeIntegerChoiceQValues(state, maxValue);
+
+ next = this.GetNextIntegerChoiceByPolicy(state, maxValue);
+
+ this.PreviousOperation = this.MinIntegerChoiceOpValue - (ulong)next;
+ this.StepCount++;
+ return true;
+ }
+
+ ///
+ /// Returns the next operation to schedule by drawing from the probability
+ /// distribution over the specified state and enabled operations.
+ ///
+ private AsyncOperation GetNextOperationByPolicy(int state, IEnumerable ops)
+ {
+ var opIds = new List();
+ var qValues = new List();
+ foreach (var pair in this.OperationQTable[state])
+ {
+ // Consider only the Q values of enabled operations.
+ if (ops.Any(op => op.Id == pair.Key))
+ {
+ opIds.Add(pair.Key);
+ qValues.Add(pair.Value);
+ }
+ }
+
+ int idx = this.ChooseQValueIndexFromDistribution(qValues);
+ return ops.FirstOrDefault(op => op.Id == opIds[idx]);
+ }
+
+ ///
+ /// Returns the next boolean choice by drawing from the probability
+ /// distribution over the specified state and boolean choices.
+ ///
+ private bool GetNextBooleanChoiceByPolicy(int state)
+ {
+ double trueQValue = this.OperationQTable[state][this.TrueChoiceOpValue];
+ double falseQValue = this.OperationQTable[state][this.FalseChoiceOpValue];
+
+ var qValues = new List(2)
+ {
+ trueQValue,
+ falseQValue
+ };
+
+ int idx = this.ChooseQValueIndexFromDistribution(qValues);
+ return idx == 0 ? true : false;
+ }
+
+ ///
+ /// Returns the next integer choice by drawing from the probability
+ /// distribution over the specified state and integer choices.
+ ///
+ private int GetNextIntegerChoiceByPolicy(int state, int maxValue)
+ {
+ var qValues = new List(maxValue);
+ for (ulong i = 0; i < (ulong)maxValue; i++)
+ {
+ qValues.Add(this.OperationQTable[state][this.MinIntegerChoiceOpValue - i]);
+ }
+
+ return this.ChooseQValueIndexFromDistribution(qValues);
+ }
+
+ ///
+ /// Returns an index of a Q value by drawing from the probability distribution
+ /// over the specified Q values.
+ ///
+ private int ChooseQValueIndexFromDistribution(List qValues)
+ {
+ double sum = 0;
+ for (int i = 0; i < qValues.Count; i++)
+ {
+ qValues[i] = Math.Exp(qValues[i]);
+ sum += qValues[i];
+ }
+
+ for (int i = 0; i < qValues.Count; i++)
+ {
+ qValues[i] /= sum;
+ }
+
+ sum = 0;
+
+ // First, change the shape of the distribution probability array to be cumulative.
+ // For example, instead of [0.1, 0.2, 0.3, 0.4], we get [0.1, 0.3, 0.6, 1.0].
+ var cumulative = qValues.Select(c =>
+ {
+ var result = c + sum;
+ sum += c;
+ return result;
+ }).ToList();
+
+ // Generate a random double value between 0.0 to 1.0.
+ var rvalue = this.RandomValueGenerator.NextDouble();
+
+ // Find the first index in the cumulative array that is greater
+ // or equal than the generated random value.
+ var idx = cumulative.BinarySearch(rvalue);
+
+ if (idx < 0)
+ {
+ // If an exact match is not found, List.BinarySearch will return the index
+ // of the first items greater than the passed value, but in a specific form
+ // (negative) we need to apply ~ to this negative value to get real index.
+ idx = ~idx;
+ }
+
+ if (idx > cumulative.Count - 1)
+ {
+ // Very rare case when probabilities do not sum to 1 because of
+ // double precision issues (so sum is 0.999943 and so on).
+ idx = cumulative.Count - 1;
+ }
+
+ return idx;
+ }
+
+ ///
+ /// Captures metadata related to the current execution step, and returns
+ /// a value representing the current program state.
+ ///
+ private int CaptureExecutionStep(IEnumerable ops, AsyncOperation current)
+ {
+ int state = this.ComputeStateHash(ops);
+
+ // Update the execution path with the current state.
+ this.ExecutionPath.AddLast((this.PreviousOperation, current.Type, state));
+
+ if (!this.TransitionFrequencies.ContainsKey(state))
+ {
+ this.TransitionFrequencies.Add(state, 0);
+ }
+
+ // Increment the state transition frequency.
+ this.TransitionFrequencies[state]++;
+
+ return state;
+ }
+
+ ///
+ /// Computes a hash representing the current program state.
+ ///
+ private int ComputeStateHash(IEnumerable ops)
+ {
+ unchecked
+ {
+ int hash = 19;
+
+ // Compute the global state hashes using the last updated statehashes of the operations
+ // Ideally sort the operation list by their unique IDs. Currently using their names.
+ foreach (var op in ops.OrderBy(op => op.Name))
+ {
+ hash = this.OperationHashes.ContainsKey(op) ? (hash * 31) + this.OperationHashes[op] : hash;
+ }
+
+ // Add the hash of the current operation.
+ // hash = (hash * 31) + operation.Name.GetHashCode();
+
+ foreach (var kvp in this.RecursiveDelayCount)
+ {
+ int delayCountHash = 19 + kvp.Key.GetHashCode();
+ delayCountHash = (delayCountHash * 31) + kvp.Value.GetHashCode();
+ hash *= delayCountHash;
+ }
+
+ // foreach (var kvp in this.OperationStatusMap)
+ // {
+ // // Console.WriteLine($">>>>>>> Hashing: id {kvp.Key} - status {kvp.Value}");
+ // // int operationHash = 31 + kvp.Key.GetHashCode();
+ // // removing inactive actors from statehash
+ // // operationHash = !(kvp.Value is ActorStatus.Inactive) ? (operationHash * 31) + kvp.Value.GetHashCode() : operationHash;
+ // // including inactive actors in statehash
+ // // operationHash = (operationHash * 31) + kvp.Value.GetHashCode();
+ // // hash *= operationHash;
+ // }
+
+ return hash;
+ }
+ }
+
+ ///
+ /// Initializes the Q values of all enabled operations that can be chosen
+ /// at the specified state that have not been previously encountered.
+ ///
+ private void InitializeOperationQValues(int state, IEnumerable ops)
+ {
+ if (!this.OperationQTable.TryGetValue(state, out Dictionary qValues))
+ {
+ qValues = new Dictionary();
+ this.OperationQTable.Add(state, qValues);
+ }
+
+ foreach (var op in ops)
+ {
+ // Assign the same initial probability for all new enabled operations.
+ if (op.Status == AsyncOperationStatus.Enabled && !qValues.ContainsKey(op.Id))
+ {
+ qValues.Add(op.Id, 0);
+ }
+ }
+ }
+
+ ///
+ /// Initializes the Q values of all boolean choices that can be chosen
+ /// at the specified state that have not been previously encountered.
+ ///
+ private void InitializeBooleanChoiceQValues(int state)
+ {
+ if (!this.OperationQTable.TryGetValue(state, out Dictionary qValues))
+ {
+ qValues = new Dictionary();
+ this.OperationQTable.Add(state, qValues);
+ }
+
+ if (!qValues.ContainsKey(this.TrueChoiceOpValue))
+ {
+ qValues.Add(this.TrueChoiceOpValue, 0);
+ }
+
+ if (!qValues.ContainsKey(this.FalseChoiceOpValue))
+ {
+ qValues.Add(this.FalseChoiceOpValue, 0);
+ }
+ }
+
+ ///
+ /// Initializes the Q values of all integer choices that can be chosen
+ /// at the specified state that have not been previously encountered.
+ ///
+ private void InitializeIntegerChoiceQValues(int state, int maxValue)
+ {
+ if (!this.OperationQTable.TryGetValue(state, out Dictionary qValues))
+ {
+ qValues = new Dictionary();
+ this.OperationQTable.Add(state, qValues);
+ }
+
+ for (ulong i = 0; i < (ulong)maxValue; i++)
+ {
+ ulong opValue = this.MinIntegerChoiceOpValue - i;
+ if (!qValues.ContainsKey(opValue))
+ {
+ qValues.Add(opValue, 0);
+ }
+ }
+ }
+
+ ///
+ internal override bool InitializeNextIteration(uint iteration)
+ {
+ this.LearnQValues();
+ this.ExecutionPath.Clear();
+ this.PreviousOperation = 0;
+ this.Epochs++;
+ // Remove the operations that do not make critical delay requests
+ this.CriticalDelayRequest = this.CriticalDelayRequest.Where(kvp => kvp.Value).ToDictionary(op => op.Key, op => op.Value);
+ this.RecursiveDelayCount.Clear();
+ this.OperationHashes.Clear();
+
+ return base.InitializeNextIteration(iteration);
+ }
+
+ ///
+ /// Learn Q values using data from the current execution.
+ ///
+ private void LearnQValues()
+ {
+ int idx = 0;
+ var node = this.ExecutionPath.First;
+ while (node?.Next != null)
+ {
+ var (_, _, state) = node.Value;
+ var (nextOp, nextType, nextState) = node.Next.Value;
+
+ // Compute the max Q value.
+ double maxQ = double.MinValue;
+ foreach (var nextOpQValuePair in this.OperationQTable[nextState])
+ {
+ if (nextOpQValuePair.Value > maxQ)
+ {
+ maxQ = nextOpQValuePair.Value;
+ }
+ }
+
+ // Compute the reward. Program states that are visited with higher frequency result into lesser rewards.
+ var freq = this.TransitionFrequencies[nextState];
+ double reward = (nextType == AsyncOperationType.InjectFailure ?
+ this.FailureInjectionReward : this.BasicActionReward) * freq;
+ if (reward > 0)
+ {
+ // The reward has underflowed.
+ reward = double.MinValue;
+ }
+
+ // Get the operations that are available from the current execution step.
+ var currOpQValues = this.OperationQTable[state];
+ if (!currOpQValues.ContainsKey(nextOp))
+ {
+ currOpQValues.Add(nextOp, 0);
+ }
+
+ // Update the Q value of the next operation.
+ // Q = [(1-a) * Q] + [a * (rt + (g * maxQ))]
+ currOpQValues[nextOp] = ((1 - this.LearningRate) * currOpQValues[nextOp]) +
+ (this.LearningRate * (reward + (this.Gamma * maxQ)));
+
+ node = node.Next;
+ idx++;
+ }
+ }
+
+ internal static int GetOperationHash(AsyncOperation operation)
+ {
+ unchecked
+ {
+ int hash = 19;
+
+ if (operation is ActorOperation actorOperation)
+ {
+ int operationHash = 31 + actorOperation.Actor.GetHashedState();
+ operationHash = (operationHash * 31) + actorOperation.Type.GetHashCode();
+ hash *= operationHash;
+ }
+ else if (operation is TaskOperation taskOperation)
+ {
+ hash *= 31 + taskOperation.Type.GetHashCode();
+ }
+
+ return hash;
+ }
+ }
+
+ ///
+ internal override string GetDescription() => $"RL[seed '{this.RandomValueGenerator.Seed}']";
+ }
+}
diff --git a/Source/Core/Testing/Fuzzing/RandomStrategy.cs b/Source/Core/Testing/Fuzzing/RandomStrategy.cs
index d38c43945..02f8d669b 100644
--- a/Source/Core/Testing/Fuzzing/RandomStrategy.cs
+++ b/Source/Core/Testing/Fuzzing/RandomStrategy.cs
@@ -1,6 +1,7 @@
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
+using System.Collections.Generic;
using Microsoft.Coyote.Runtime;
namespace Microsoft.Coyote.Testing.Fuzzing
@@ -42,13 +43,24 @@ internal override bool InitializeNextIteration(uint iteration)
}
///
- internal override bool GetNextDelay(AsyncOperation current, int maxValue, out int next)
+ internal override bool GetNextDelay(IEnumerable ops, AsyncOperation current,
+ int maxValue, bool positiveDelay, bool isRecursive, out int next)
{
next = this.RandomValueGenerator.Next(maxValue);
- this.StepCount++;
+
+ if (!isRecursive)
+ {
+ this.StepCount++;
+ }
+
return true;
}
+ internal override bool GetNextRecursiveDelayChoice(IEnumerable ops, AsyncOperation current)
+ {
+ return this.RandomValueGenerator.Next(2) is 0 ? true : false;
+ }
+
///
internal override int GetStepCount() => this.StepCount;
diff --git a/Source/Core/Testing/Systematic/QLearningStrategy.cs b/Source/Core/Testing/Systematic/QLearningStrategy.cs
index 82212ff42..69d5d9f82 100644
--- a/Source/Core/Testing/Systematic/QLearningStrategy.cs
+++ b/Source/Core/Testing/Systematic/QLearningStrategy.cs
@@ -359,14 +359,10 @@ internal override bool InitializeNextIteration(uint iteration)
///
private void LearnQValues()
{
- var pathBuilder = new System.Text.StringBuilder();
-
int idx = 0;
var node = this.ExecutionPath.First;
while (node?.Next != null)
{
- pathBuilder.Append($"{node.Value.op},");
-
var (_, _, state) = node.Value;
var (nextOp, nextType, nextState) = node.Next.Value;
diff --git a/global.json b/global.json
index e52d340bc..e0a11efb7 100644
--- a/global.json
+++ b/global.json
@@ -1,5 +1,5 @@
{
"sdk": {
- "version": "6.0.101"
+ "version": "6.0.102"
}
}