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" } }