From 639a26ca7198d74fab145e2f0f58dacdff7cccc8 Mon Sep 17 00:00:00 2001 From: Pantazis Deligiannis Date: Wed, 19 Jan 2022 19:31:38 -0800 Subject: [PATCH 01/16] initial ql fuzzing --- .../Core/Testing/Fuzzing/FuzzingStrategy.cs | 6 +- .../Core/Testing/Fuzzing/QLearningStrategy.cs | 299 ++++++++++++++++++ 2 files changed, 303 insertions(+), 2 deletions(-) create mode 100644 Source/Core/Testing/Fuzzing/QLearningStrategy.cs diff --git a/Source/Core/Testing/Fuzzing/FuzzingStrategy.cs b/Source/Core/Testing/Fuzzing/FuzzingStrategy.cs index 83919cb80..dd64cea19 100644 --- a/Source/Core/Testing/Fuzzing/FuzzingStrategy.cs +++ b/Source/Core/Testing/Fuzzing/FuzzingStrategy.cs @@ -39,11 +39,13 @@ 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); } } diff --git a/Source/Core/Testing/Fuzzing/QLearningStrategy.cs b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs new file mode 100644 index 000000000..0cc7064dc --- /dev/null +++ b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs @@ -0,0 +1,299 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +using System; +using System.Collections.Concurrent; +using System.Collections.Generic; +using System.Linq; +using Microsoft.Coyote.Runtime; + +namespace Microsoft.Coyote.Testing.Fuzzing +{ + /// + /// A probabilistic fuzzing strategy that uses Q-learning. + /// + internal class QLearningStrategy : RandomStrategy + { + /// + /// Map from program states to a map from next delays 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 a delay value and a value + /// representing the program state after the delay happened. + /// + private readonly LinkedList<(int delay, int state)> ExecutionPath; + + /// + /// Map of operation ids to their current activity status. + /// + private readonly ConcurrentDictionary ActivityStatusMap; + + /// + /// The previously chosen delay. + /// + private int PreviousDelay; + + /// + /// The value of the learning rate. + /// + private readonly double LearningRate; + + /// + /// The value of the discount factor. + /// + private readonly double Gamma; + + /// + /// The basic action reward. + /// + private readonly double BasicActionReward; + + /// + /// The number of explored executions. + /// + private int Epochs; + + /// + /// Initializes a new instance of the class. + /// It uses the specified random number generator. + /// + internal QLearningStrategy(int maxSteps, IRandomValueGenerator random) + : base(maxSteps, random) + { + this.OperationQTable = new Dictionary>(); + this.ExecutionPath = new LinkedList<(int, int)>(); + this.ActivityStatusMap = new ConcurrentDictionary(); + this.PreviousDelay = 0; + this.LearningRate = 0.3; + this.Gamma = 0.7; + this.BasicActionReward = -1; + this.Epochs = 0; + } + + /// + internal override bool GetNextDelay(AsyncOperation current, int maxValue, out int next) + { + int state = this.CaptureExecutionStep(current); + this.InitializeDelayQValues(state, maxValue); + + next = this.GetNextDelayByPolicy(state, maxValue); + this.PreviousDelay = next; + + this.StepCount++; + return true; + } + + // /// + // /// Notifies the activity status of the current operation. + // /// + // // internal override void NotifyActivityStatus(AsyncOperation current, ActivityStatus status) + // // { + // // this.ActivityStatusMap.AddOrUpdate(current.Name, status, (id, old) => status); + // // } + + /// + /// Returns the next delay by drawing from the probability distribution + /// over the specified state and range of delays. + /// + private int GetNextDelayByPolicy(int state, int maxValue) + { + var qValues = new List(maxValue); + for (int i = 0; i < maxValue; i++) + { + qValues.Add(this.OperationQTable[state][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(AsyncOperation operation) + { + int state = ComputeStateHash(operation); + + // Update the list of chosen delays with the current state. + this.ExecutionPath.AddLast((this.PreviousDelay, state)); + return state; + } + + /// + /// Computes a hash representing the current program state. + /// + private static int ComputeStateHash(AsyncOperation operation) + { + unchecked + { + int hash = 19; + + // Add the hash of the current operation. + hash = (hash * 31) + operation.Name.GetHashCode(); + + // foreach (var kvp in this.ActivityStatusMap) + // { + // // 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 delays that can be chosen at the specified state + /// that have not been previously encountered. + /// + private void InitializeDelayQValues(int state, int maxValue) + { + if (!this.OperationQTable.TryGetValue(state, out Dictionary qValues)) + { + qValues = new Dictionary(); + this.OperationQTable.Add(state, qValues); + } + + for (int i = 0; i < maxValue; i++) + { + if (!qValues.ContainsKey(i)) + { + qValues.Add(i, 0); + } + } + } + + /// + internal override bool InitializeNextIteration(uint iteration) + { + this.LearnQValues(); + this.ExecutionPath.Clear(); + this.PreviousDelay = 0; + this.Epochs++; + + return base.InitializeNextIteration(iteration); + } + + /// + /// Learn Q values using data from the current execution. + /// + 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.delay},"); + + var (_, state) = node.Value; + var (nextDelay, 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. + double reward = this.BasicActionReward; + if (reward > 0) + { + // The reward has underflowed. + reward = double.MinValue; + } + + // Get the delays that are available from the current execution step. + var currOpQValues = this.OperationQTable[state]; + if (!currOpQValues.ContainsKey(nextDelay)) + { + currOpQValues.Add(nextDelay, 0); + } + + // Update the Q value of the next delay. + // Q = [(1-a) * Q] + [a * (rt + (g * maxQ))] + currOpQValues[nextDelay] = ((1 - this.LearningRate) * currOpQValues[nextDelay]) + + (this.LearningRate * (reward + (this.Gamma * maxQ))); + + node = node.Next; + idx++; + } + } + + /// + internal override string GetDescription() => $"RL[seed '{this.RandomValueGenerator.Seed}']"; + + private enum ActivityStatus + { + ActiveAwake, + ActiveSleeping, + Inactive + } + } +} From b213da48674186076929e86831c7509c30fb54e3 Mon Sep 17 00:00:00 2001 From: Pantazis Deligiannis Date: Wed, 19 Jan 2022 22:05:25 -0800 Subject: [PATCH 02/16] progress --- Source/Core/Runtime/CoyoteRuntime.cs | 14 +++--- .../Runtime/Scheduling/OperationScheduler.cs | 5 ++- .../Testing/Fuzzing/BoundedRandomStrategy.cs | 4 +- .../Core/Testing/Fuzzing/FuzzingStrategy.cs | 5 ++- Source/Core/Testing/Fuzzing/PCTStrategy.cs | 3 +- .../Core/Testing/Fuzzing/QLearningStrategy.cs | 43 +++++++------------ Source/Core/Testing/Fuzzing/RandomStrategy.cs | 4 +- .../Testing/Systematic/QLearningStrategy.cs | 4 -- 8 files changed, 40 insertions(+), 42 deletions(-) diff --git a/Source/Core/Runtime/CoyoteRuntime.cs b/Source/Core/Runtime/CoyoteRuntime.cs index 2d4bad4cb..e75a9d20d 100644 --- a/Source/Core/Runtime/CoyoteRuntime.cs +++ b/Source/Core/Runtime/CoyoteRuntime.cs @@ -918,6 +918,7 @@ internal void ResumeScheduling() internal void DelayOperation() { int delay = 0; + AsyncOperation current = null; lock (this.SyncObject) { if (!this.IsAttached) @@ -925,7 +926,7 @@ 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. @@ -935,10 +936,13 @@ internal void DelayOperation() } } - if (delay > 0) + // Only sleep the executing operation if a non-zero delay was . + if (delay > 0 && current != null) { - // Only sleep if a non-zero delay was chosen. + var previousStatus = current.Status; + current.Status = AsyncOperationStatus.Delayed; Thread.Sleep(delay); + current.Status = previousStatus; } } @@ -1030,7 +1034,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, out int next)) { this.Detach(SchedulerDetachmentReason.BoundReached); } @@ -1251,7 +1255,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..1cf0b23ec 100644 --- a/Source/Core/Runtime/Scheduling/OperationScheduler.cs +++ b/Source/Core/Runtime/Scheduling/OperationScheduler.cs @@ -164,12 +164,13 @@ 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. /// 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, out int next) => + (this.Strategy as FuzzingStrategy).GetNextDelay(ops, current, maxValue, out next); /// /// 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..fc4422e3a 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,8 @@ 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, out int next) { Guid id = this.GetOperationId(); diff --git a/Source/Core/Testing/Fuzzing/FuzzingStrategy.cs b/Source/Core/Testing/Fuzzing/FuzzingStrategy.cs index dd64cea19..6512c85b2 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; @@ -52,11 +53,13 @@ internal static FuzzingStrategy Create(Configuration configuration, IRandomValue /// /// Returns the next delay. /// + /// Operations executing during the current test iteration. /// The operation requesting the delay. /// The max value. /// 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, out int next); /// /// Returns the current operation id. diff --git a/Source/Core/Testing/Fuzzing/PCTStrategy.cs b/Source/Core/Testing/Fuzzing/PCTStrategy.cs index f4d0dfe9d..109c7d34e 100644 --- a/Source/Core/Testing/Fuzzing/PCTStrategy.cs +++ b/Source/Core/Testing/Fuzzing/PCTStrategy.cs @@ -77,7 +77,8 @@ 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, out int next) { Guid id = this.GetOperationId(); diff --git a/Source/Core/Testing/Fuzzing/QLearningStrategy.cs b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs index 0cc7064dc..daec9e6a5 100644 --- a/Source/Core/Testing/Fuzzing/QLearningStrategy.cs +++ b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs @@ -26,11 +26,6 @@ internal class QLearningStrategy : RandomStrategy /// private readonly LinkedList<(int delay, int state)> ExecutionPath; - /// - /// Map of operation ids to their current activity status. - /// - private readonly ConcurrentDictionary ActivityStatusMap; - /// /// The previously chosen delay. /// @@ -65,7 +60,6 @@ internal QLearningStrategy(int maxSteps, IRandomValueGenerator random) { this.OperationQTable = new Dictionary>(); this.ExecutionPath = new LinkedList<(int, int)>(); - this.ActivityStatusMap = new ConcurrentDictionary(); this.PreviousDelay = 0; this.LearningRate = 0.3; this.Gamma = 0.7; @@ -74,9 +68,10 @@ internal QLearningStrategy(int maxSteps, IRandomValueGenerator random) } /// - internal override bool GetNextDelay(AsyncOperation current, int maxValue, out int next) + internal override bool GetNextDelay(IEnumerable ops, AsyncOperation current, + int maxValue, out int next) { - int state = this.CaptureExecutionStep(current); + int state = this.CaptureExecutionStep(ops, current); this.InitializeDelayQValues(state, maxValue); next = this.GetNextDelayByPolicy(state, maxValue); @@ -86,14 +81,6 @@ internal override bool GetNextDelay(AsyncOperation current, int maxValue, out in return true; } - // /// - // /// Notifies the activity status of the current operation. - // /// - // // internal override void NotifyActivityStatus(AsyncOperation current, ActivityStatus status) - // // { - // // this.ActivityStatusMap.AddOrUpdate(current.Name, status, (id, old) => status); - // // } - /// /// Returns the next delay by drawing from the probability distribution /// over the specified state and range of delays. @@ -167,10 +154,16 @@ private int ChooseQValueIndexFromDistribution(List qValues) /// Captures metadata related to the current execution step, and returns /// a value representing the current program state. /// - private int CaptureExecutionStep(AsyncOperation operation) + private int CaptureExecutionStep(IEnumerable ops, AsyncOperation operation) { int state = ComputeStateHash(operation); + Console.WriteLine($">---> {operation.Name}: state: {state}"); + foreach (var op in ops) + { + Console.WriteLine($" |---> {op.Name}: status: {op.Status}"); + } + // Update the list of chosen delays with the current state. this.ExecutionPath.AddLast((this.PreviousDelay, state)); return state; @@ -188,7 +181,7 @@ private static int ComputeStateHash(AsyncOperation operation) // Add the hash of the current operation. hash = (hash * 31) + operation.Name.GetHashCode(); - // foreach (var kvp in this.ActivityStatusMap) + // foreach (var kvp in this.OperationStatusMap) // { // // Console.WriteLine($">>>>>>> Hashing: id {kvp.Key} - status {kvp.Value}"); // // int operationHash = 31 + kvp.Key.GetHashCode(); @@ -240,13 +233,13 @@ internal override bool InitializeNextIteration(uint iteration) /// private void LearnQValues() { - var pathBuilder = new System.Text.StringBuilder(); + // var pathBuilder = new System.Text.StringBuilder(); int idx = 0; var node = this.ExecutionPath.First; while (node?.Next != null) { - pathBuilder.Append($"{node.Value.delay},"); + // pathBuilder.Append($"({node.Value.delay},{node.Value.state}), "); var (_, state) = node.Value; var (nextDelay, nextState) = node.Next.Value; @@ -284,16 +277,12 @@ private void LearnQValues() node = node.Next; idx++; } + + Console.WriteLine($"Visited {this.OperationQTable.Count} states."); + // Console.WriteLine(pathBuilder.ToString()); } /// internal override string GetDescription() => $"RL[seed '{this.RandomValueGenerator.Seed}']"; - - private enum ActivityStatus - { - ActiveAwake, - ActiveSleeping, - Inactive - } } } diff --git a/Source/Core/Testing/Fuzzing/RandomStrategy.cs b/Source/Core/Testing/Fuzzing/RandomStrategy.cs index d38c43945..90963b4dc 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,7 +43,8 @@ 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, out int next) { next = this.RandomValueGenerator.Next(maxValue); 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; From 4a7267b0258356f979356b86c25d4492c797694b Mon Sep 17 00:00:00 2001 From: notDhruv Date: Wed, 26 Jan 2022 16:11:57 +0000 Subject: [PATCH 03/16] new fuzzing framework without parameterized bound on delayed operations --- Source/Core/Runtime/CoyoteRuntime.cs | 22 +- .../Runtime/Scheduling/OperationScheduler.cs | 13 +- .../Testing/Fuzzing/BoundedRandomStrategy.cs | 7 +- .../Core/Testing/Fuzzing/FuzzingStrategy.cs | 11 +- Source/Core/Testing/Fuzzing/PCTStrategy.cs | 289 ++++++++++++++---- .../Core/Testing/Fuzzing/QLearningStrategy.cs | 2 +- Source/Core/Testing/Fuzzing/RandomStrategy.cs | 17 +- 7 files changed, 294 insertions(+), 67 deletions(-) diff --git a/Source/Core/Runtime/CoyoteRuntime.cs b/Source/Core/Runtime/CoyoteRuntime.cs index e75a9d20d..8556a1b12 100644 --- a/Source/Core/Runtime/CoyoteRuntime.cs +++ b/Source/Core/Runtime/CoyoteRuntime.cs @@ -911,11 +911,12 @@ 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) { int delay = 0; AsyncOperation current = null; @@ -930,13 +931,13 @@ internal void DelayOperation() 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, positiveDelay); IO.Debug.WriteLine(" Delaying operation '{0}' on thread '{1}' by {2}ms.", current.Name, Thread.CurrentThread.ManagedThreadId, delay); } } - // Only sleep the executing operation if a non-zero delay was . + // Only sleep the executing operation if a non-zero delay was chosen. if (delay > 0 && current != null) { var previousStatus = current.Status; @@ -944,6 +945,12 @@ internal void DelayOperation() Thread.Sleep(delay); current.Status = previousStatus; } + + // 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); + } } /// @@ -1025,16 +1032,21 @@ 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 positiveDelay = false) { lock (this.SyncObject) { // Checks if the scheduling steps bound has been reached. this.CheckIfSchedulingStepsBoundIsReached(); + if (this.OperationMap.Values.Where(v => v.Status is AsyncOperationStatus.Enabled).Count() is 1) + { + return 0; + } + // Choose the next delay to inject. int maxDelay = maxValue > 0 ? (int)this.Configuration.TimeoutDelay : 1; - if (!this.Scheduler.GetNextDelay(this.OperationMap.Values, op, maxDelay, out int next)) + if (!this.Scheduler.GetNextDelay(this.OperationMap.Values, op, maxDelay, positiveDelay, out int next)) { this.Detach(SchedulerDetachmentReason.BoundReached); } diff --git a/Source/Core/Runtime/Scheduling/OperationScheduler.cs b/Source/Core/Runtime/Scheduling/OperationScheduler.cs index 1cf0b23ec..2eab49f66 100644 --- a/Source/Core/Runtime/Scheduling/OperationScheduler.cs +++ b/Source/Core/Runtime/Scheduling/OperationScheduler.cs @@ -167,10 +167,19 @@ internal bool GetNextIntegerChoice(AsyncOperation current, int maxValue, out int /// 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(IEnumerable ops, AsyncOperation current, int maxValue, out int next) => - (this.Strategy as FuzzingStrategy).GetNextDelay(ops, current, maxValue, out next); + internal bool GetNextDelay(IEnumerable ops, AsyncOperation current, int maxValue, bool positiveDelay, out int next) => + (this.Strategy as FuzzingStrategy).GetNextDelay(ops, current, maxValue, positiveDelay, 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 fc4422e3a..015e21015 100644 --- a/Source/Core/Testing/Fuzzing/BoundedRandomStrategy.cs +++ b/Source/Core/Testing/Fuzzing/BoundedRandomStrategy.cs @@ -57,7 +57,7 @@ internal override bool InitializeNextIteration(uint iteration) /// with an increment of 10 and an upper bound of 5000ms per operation. /// internal override bool GetNextDelay(IEnumerable ops, AsyncOperation current, - int maxValue, out int next) + int maxValue, bool positiveDelay, out int next) { Guid id = this.GetOperationId(); @@ -84,6 +84,11 @@ internal override bool GetNextDelay(IEnumerable ops, AsyncOperat 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 6512c85b2..443cc912a 100644 --- a/Source/Core/Testing/Fuzzing/FuzzingStrategy.cs +++ b/Source/Core/Testing/Fuzzing/FuzzingStrategy.cs @@ -56,10 +56,19 @@ internal static FuzzingStrategy Create(Configuration configuration, IRandomValue /// 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(IEnumerable ops, AsyncOperation current, - int maxValue, out int next); + int maxValue, bool positiveDelay, 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 109c7d34e..eba844d13 100644 --- a/Source/Core/Testing/Fuzzing/PCTStrategy.cs +++ b/Source/Core/Testing/Fuzzing/PCTStrategy.cs @@ -3,120 +3,229 @@ 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 readonly List PrioritizedOperations; /// - /// The number of exploration steps. + /// Scheduling points in the current execution where a priority change should occur. /// - protected int StepCount; + 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(); } /// 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(); + + 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(IEnumerable ops, AsyncOperation current, - int maxValue, out int next) + int maxValue, bool positiveDelay, out int next) { - Guid id = this.GetOperationId(); + this.UpdateAndGetHighestPriorityEnabledOperation(ops, current, out AsyncOperation highestEnabledOperation); + + if (positiveDelay) + { + next = this.RandomValueGenerator.Next(maxValue - 1) + 1; + } + else + { + next = this.RandomValueGenerator.Next(maxValue); + } + + return true; + } - this.StepCount++; + internal override bool GetNextRecursiveDelayChoice(IEnumerable ops, AsyncOperation current) + { + this.UpdateAndGetHighestPriorityEnabledOperation(ops, current, out AsyncOperation highestEnabledOperation); - // Reshuffle the probabilities after every (this.MaxSteps / this.PriorityChangePoints) steps. - if (this.StepCount % (this.MaxSteps / this.PriorityChangePoints) == 0) + if (highestEnabledOperation.Equals(current)) { - this.LowPrioritySet.Clear(); - this.HighPrioritySet.Clear(); + 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)) + return this.RandomValueGenerator.Next(2) is 0 ? true : false; + } + + /// + internal bool UpdateAndGetHighestPriorityEnabledOperation(IEnumerable ops, AsyncOperation current, + out AsyncOperation highestEnabledOperation) + { + highestEnabledOperation = null; + var enabledOps = ops.Where(op => op.Status is AsyncOperationStatus.Enabled).ToList(); + if (enabledOps.Count is 0) { - if (this.RandomValueGenerator.NextDouble() < this.LowPriorityProbability) - { - this.LowPrioritySet.Add(id); - } - else - { - this.HighPrioritySet.Add(id); - } + return false; } - // Choose a random delay if this task is in the low priority set. - if (this.LowPrioritySet.Contains(id)) + this.SetNewOperationPriorities(enabledOps, current); + this.DeprioritizeEnabledOperationWithHighestPriority(enabledOps); + this.DebugPrintOperationPriorityList(); + + highestEnabledOperation = this.GetEnabledOperationWithHighestPriority(enabledOps); + 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) { - next = this.RandomValueGenerator.Next(maxValue) * 5; + this.PrioritizedOperations.Add(current); } - else + + // Randomize the priority of all new operations. + foreach (var op in ops.Where(op => !this.PrioritizedOperations.Contains(op))) { - next = 0; + // Randomly choose a priority for this operation. + 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); } + } - return true; + /// + /// 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 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; @@ -132,9 +241,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 index daec9e6a5..71358a255 100644 --- a/Source/Core/Testing/Fuzzing/QLearningStrategy.cs +++ b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs @@ -69,7 +69,7 @@ internal QLearningStrategy(int maxSteps, IRandomValueGenerator random) /// internal override bool GetNextDelay(IEnumerable ops, AsyncOperation current, - int maxValue, out int next) + int maxValue, bool positiveDelay, out int next) { int state = this.CaptureExecutionStep(ops, current); this.InitializeDelayQValues(state, maxValue); diff --git a/Source/Core/Testing/Fuzzing/RandomStrategy.cs b/Source/Core/Testing/Fuzzing/RandomStrategy.cs index 90963b4dc..c26394e61 100644 --- a/Source/Core/Testing/Fuzzing/RandomStrategy.cs +++ b/Source/Core/Testing/Fuzzing/RandomStrategy.cs @@ -44,13 +44,26 @@ internal override bool InitializeNextIteration(uint iteration) /// internal override bool GetNextDelay(IEnumerable ops, AsyncOperation current, - int maxValue, out int next) + int maxValue, bool positiveDelay, out int next) { - next = this.RandomValueGenerator.Next(maxValue); + if (positiveDelay) + { + next = this.RandomValueGenerator.Next(maxValue - 1) + 1; + } + else + { + next = this.RandomValueGenerator.Next(maxValue); + } + 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; From 192af2b0fef964bf75ea7bc6fb0156e20d7b06e4 Mon Sep 17 00:00:00 2001 From: notDhruv Date: Thu, 27 Jan 2022 14:42:26 +0000 Subject: [PATCH 04/16] New PCT fuzzing framework added --- Source/Core/Runtime/CoyoteRuntime.cs | 13 ++++---- Source/Core/Testing/Fuzzing/PCTStrategy.cs | 37 ++++++++++++++++------ 2 files changed, 34 insertions(+), 16 deletions(-) diff --git a/Source/Core/Runtime/CoyoteRuntime.cs b/Source/Core/Runtime/CoyoteRuntime.cs index 8556a1b12..72e833f45 100644 --- a/Source/Core/Runtime/CoyoteRuntime.cs +++ b/Source/Core/Runtime/CoyoteRuntime.cs @@ -918,6 +918,7 @@ internal void ResumeScheduling() /// internal void DelayOperation(bool positiveDelay = false) { + RecursiveDelay: int delay = 0; AsyncOperation current = null; lock (this.SyncObject) @@ -944,12 +945,12 @@ internal void DelayOperation(bool positiveDelay = false) current.Status = AsyncOperationStatus.Delayed; Thread.Sleep(delay); current.Status = previousStatus; - } - - // 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); + 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); + // } } } diff --git a/Source/Core/Testing/Fuzzing/PCTStrategy.cs b/Source/Core/Testing/Fuzzing/PCTStrategy.cs index eba844d13..24c5aabdb 100644 --- a/Source/Core/Testing/Fuzzing/PCTStrategy.cs +++ b/Source/Core/Testing/Fuzzing/PCTStrategy.cs @@ -97,9 +97,10 @@ internal override bool InitializeNextIteration(uint iteration) internal override bool GetNextDelay(IEnumerable ops, AsyncOperation current, int maxValue, bool positiveDelay, out int next) { - this.UpdateAndGetHighestPriorityEnabledOperation(ops, current, out AsyncOperation highestEnabledOperation); + this.UpdateAndGetLowestPriorityEnabledOperation(ops, current, out AsyncOperation lowestEnabledOperation); - if (positiveDelay) + // if (positiveDelay) + if (lowestEnabledOperation.Equals(current)) { next = this.RandomValueGenerator.Next(maxValue - 1) + 1; } @@ -113,9 +114,9 @@ internal override bool GetNextDelay(IEnumerable ops, AsyncOperat internal override bool GetNextRecursiveDelayChoice(IEnumerable ops, AsyncOperation current) { - this.UpdateAndGetHighestPriorityEnabledOperation(ops, current, out AsyncOperation highestEnabledOperation); + this.UpdateAndGetLowestPriorityEnabledOperation(ops, current, out AsyncOperation lowestEnabledOperation); - if (highestEnabledOperation.Equals(current)) + if (lowestEnabledOperation.Equals(current)) { return true; } @@ -124,10 +125,10 @@ internal override bool GetNextRecursiveDelayChoice(IEnumerable o } /// - internal bool UpdateAndGetHighestPriorityEnabledOperation(IEnumerable ops, AsyncOperation current, - out AsyncOperation highestEnabledOperation) + internal bool UpdateAndGetLowestPriorityEnabledOperation(IEnumerable ops, AsyncOperation current, + out AsyncOperation lowestEnabledOperation) { - highestEnabledOperation = null; + lowestEnabledOperation = null; var enabledOps = ops.Where(op => op.Status is AsyncOperationStatus.Enabled).ToList(); if (enabledOps.Count is 0) { @@ -138,7 +139,7 @@ internal bool UpdateAndGetHighestPriorityEnabledOperation(IEnumerable ops, AsyncOperation // 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. - int index = this.RandomValueGenerator.Next(this.PrioritizedOperations.Count) + 1; + // Randomly choose a priority for this operation between the lowest and the highest priority. + int index = this.RandomValueGenerator.Next(this.PrioritizedOperations.Count - 1) + 1; this.PrioritizedOperations.Insert(index, op); Debug.WriteLine(" chose priority '{0}' for new operation '{1}'.", index, op.Name); } @@ -190,6 +191,22 @@ private void DeprioritizeEnabledOperationWithHighestPriority(List + /// 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. /// From 47e908af90970012491529542398dbdb8cfacf18 Mon Sep 17 00:00:00 2001 From: notDhruv Date: Thu, 27 Jan 2022 14:59:14 +0000 Subject: [PATCH 05/16] New PCT fuzzing framework --- Source/Core/Testing/Fuzzing/PCTStrategy.cs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Source/Core/Testing/Fuzzing/PCTStrategy.cs b/Source/Core/Testing/Fuzzing/PCTStrategy.cs index 24c5aabdb..8150a6574 100644 --- a/Source/Core/Testing/Fuzzing/PCTStrategy.cs +++ b/Source/Core/Testing/Fuzzing/PCTStrategy.cs @@ -97,6 +97,12 @@ internal override bool InitializeNextIteration(uint iteration) internal override bool GetNextDelay(IEnumerable ops, AsyncOperation current, int maxValue, bool positiveDelay, out int next) { + // if the number of delayed operations exceeds k, then don't delay the current operation. k has been chosen to be 1. + if (ops.Where(op => op.Status is AsyncOperationStatus.Delayed).Count() > 1) + { + next = 0; + } + this.UpdateAndGetLowestPriorityEnabledOperation(ops, current, out AsyncOperation lowestEnabledOperation); // if (positiveDelay) From 212d1aa292a2c4529f0988fa4efeca00389ee8d6 Mon Sep 17 00:00:00 2001 From: notDhruv Date: Thu, 27 Jan 2022 16:38:46 +0000 Subject: [PATCH 06/16] New PCT fuzzing framework --- Source/Core/Testing/Fuzzing/PCTStrategy.cs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Source/Core/Testing/Fuzzing/PCTStrategy.cs b/Source/Core/Testing/Fuzzing/PCTStrategy.cs index 8150a6574..c33c919dc 100644 --- a/Source/Core/Testing/Fuzzing/PCTStrategy.cs +++ b/Source/Core/Testing/Fuzzing/PCTStrategy.cs @@ -97,14 +97,14 @@ internal override bool InitializeNextIteration(uint iteration) internal override bool GetNextDelay(IEnumerable ops, AsyncOperation current, int maxValue, bool positiveDelay, out int next) { + this.UpdateAndGetLowestPriorityEnabledOperation(ops, current, out AsyncOperation lowestEnabledOperation); + // if the number of delayed operations exceeds k, then don't delay the current operation. k has been chosen to be 1. if (ops.Where(op => op.Status is AsyncOperationStatus.Delayed).Count() > 1) { next = 0; } - this.UpdateAndGetLowestPriorityEnabledOperation(ops, current, out AsyncOperation lowestEnabledOperation); - // if (positiveDelay) if (lowestEnabledOperation.Equals(current)) { @@ -115,6 +115,7 @@ internal override bool GetNextDelay(IEnumerable ops, AsyncOperat next = this.RandomValueGenerator.Next(maxValue); } + this.StepCount++; return true; } From 355b79f654b5c887523089814511903192819c6f Mon Sep 17 00:00:00 2001 From: notDhruv Date: Wed, 2 Feb 2022 16:58:00 +0000 Subject: [PATCH 07/16] . --- Source/Core/Runtime/CoyoteRuntime.cs | 2 +- Source/Core/Testing/Fuzzing/PCTStrategy.cs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/Core/Runtime/CoyoteRuntime.cs b/Source/Core/Runtime/CoyoteRuntime.cs index 72e833f45..8f2c56b85 100644 --- a/Source/Core/Runtime/CoyoteRuntime.cs +++ b/Source/Core/Runtime/CoyoteRuntime.cs @@ -1040,7 +1040,7 @@ private int GetNondeterministicDelay(AsyncOperation op, int maxValue, bool posit // Checks if the scheduling steps bound has been reached. this.CheckIfSchedulingStepsBoundIsReached(); - if (this.OperationMap.Values.Where(v => v.Status is AsyncOperationStatus.Enabled).Count() is 1) + if (this.OperationMap.Values.Where(v => v.Status is AsyncOperationStatus.Enabled).Count() is 1 || op.Name == "Example.Calculator(1)") { return 0; } diff --git a/Source/Core/Testing/Fuzzing/PCTStrategy.cs b/Source/Core/Testing/Fuzzing/PCTStrategy.cs index c33c919dc..c4d087be6 100644 --- a/Source/Core/Testing/Fuzzing/PCTStrategy.cs +++ b/Source/Core/Testing/Fuzzing/PCTStrategy.cs @@ -100,7 +100,7 @@ internal override bool GetNextDelay(IEnumerable ops, AsyncOperat this.UpdateAndGetLowestPriorityEnabledOperation(ops, current, out AsyncOperation lowestEnabledOperation); // if the number of delayed operations exceeds k, then don't delay the current operation. k has been chosen to be 1. - if (ops.Where(op => op.Status is AsyncOperationStatus.Delayed).Count() > 1) + if (ops.Where(op => op.Status is AsyncOperationStatus.Delayed).Count() == 1) { next = 0; } From 205806011fc59c9427bec06a382c0d4abafb97d5 Mon Sep 17 00:00:00 2001 From: notDhruv Date: Wed, 2 Feb 2022 17:18:42 +0000 Subject: [PATCH 08/16] . --- Source/Core/Runtime/CoyoteRuntime.cs | 29 ++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/Source/Core/Runtime/CoyoteRuntime.cs b/Source/Core/Runtime/CoyoteRuntime.cs index 8f2c56b85..2de1c471f 100644 --- a/Source/Core/Runtime/CoyoteRuntime.cs +++ b/Source/Core/Runtime/CoyoteRuntime.cs @@ -936,21 +936,22 @@ internal void DelayOperation(bool positiveDelay = false) IO.Debug.WriteLine(" Delaying operation '{0}' on thread '{1}' by {2}ms.", current.Name, Thread.CurrentThread.ManagedThreadId, 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); - current.Status = previousStatus; - 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); - // } + // 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; + 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); + // } + } } } From 84b97c854e3dffd3d18b5bde191b8dc4957b881a Mon Sep 17 00:00:00 2001 From: Pantazis Deligiannis Date: Wed, 2 Feb 2022 10:05:43 -0800 Subject: [PATCH 09/16] progress --- Source/Core/Runtime/CoyoteRuntime.cs | 11 +++++++---- Source/Core/Runtime/Scheduling/OperationScheduler.cs | 6 ++++-- Source/Core/Testing/Fuzzing/BoundedRandomStrategy.cs | 3 +-- Source/Core/Testing/Fuzzing/FuzzingStrategy.cs | 3 ++- Source/Core/Testing/Fuzzing/PCTStrategy.cs | 10 +++++++--- Source/Core/Testing/Fuzzing/QLearningStrategy.cs | 2 +- Source/Core/Testing/Fuzzing/RandomStrategy.cs | 2 +- 7 files changed, 23 insertions(+), 14 deletions(-) diff --git a/Source/Core/Runtime/CoyoteRuntime.cs b/Source/Core/Runtime/CoyoteRuntime.cs index 2de1c471f..1f15b31d6 100644 --- a/Source/Core/Runtime/CoyoteRuntime.cs +++ b/Source/Core/Runtime/CoyoteRuntime.cs @@ -918,8 +918,9 @@ internal void ResumeScheduling() /// internal void DelayOperation(bool positiveDelay = false) { - RecursiveDelay: + RecursiveDelay: int delay = 0; + int numDelays = 0; AsyncOperation current = null; lock (this.SyncObject) { @@ -932,7 +933,8 @@ internal void DelayOperation(bool positiveDelay = false) if (current != null) { // Choose the next delay to inject. The value is in milliseconds. - delay = this.GetNondeterministicDelay(current, (int)this.Configuration.TimeoutDelay, positiveDelay); + 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); } @@ -945,6 +947,7 @@ internal void DelayOperation(bool positiveDelay = false) // 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)) @@ -1034,7 +1037,7 @@ internal int GetNextNondeterministicIntegerChoice(int maxValue) /// /// Returns a controlled nondeterministic delay for the specified operation. /// - private int GetNondeterministicDelay(AsyncOperation op, int maxValue, bool positiveDelay = false) + private int GetNondeterministicDelay(AsyncOperation op, int maxValue, bool isRecursive = false, bool positiveDelay = false) { lock (this.SyncObject) { @@ -1048,7 +1051,7 @@ private int GetNondeterministicDelay(AsyncOperation op, int maxValue, bool posit // Choose the next delay to inject. int maxDelay = maxValue > 0 ? (int)this.Configuration.TimeoutDelay : 1; - if (!this.Scheduler.GetNextDelay(this.OperationMap.Values, op, maxDelay, positiveDelay, out int next)) + if (!this.Scheduler.GetNextDelay(this.OperationMap.Values, op, maxDelay, positiveDelay, isRecursive, out int next)) { this.Detach(SchedulerDetachmentReason.BoundReached); } diff --git a/Source/Core/Runtime/Scheduling/OperationScheduler.cs b/Source/Core/Runtime/Scheduling/OperationScheduler.cs index 2eab49f66..8ac19899a 100644 --- a/Source/Core/Runtime/Scheduling/OperationScheduler.cs +++ b/Source/Core/Runtime/Scheduling/OperationScheduler.cs @@ -168,10 +168,12 @@ internal bool GetNextIntegerChoice(AsyncOperation current, int maxValue, out int /// 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(IEnumerable ops, AsyncOperation current, int maxValue, bool positiveDelay, out int next) => - (this.Strategy as FuzzingStrategy).GetNextDelay(ops, current, maxValue, positiveDelay, 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. diff --git a/Source/Core/Testing/Fuzzing/BoundedRandomStrategy.cs b/Source/Core/Testing/Fuzzing/BoundedRandomStrategy.cs index 015e21015..93214eecd 100644 --- a/Source/Core/Testing/Fuzzing/BoundedRandomStrategy.cs +++ b/Source/Core/Testing/Fuzzing/BoundedRandomStrategy.cs @@ -56,8 +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(IEnumerable ops, AsyncOperation current, - int maxValue, bool positiveDelay, out int next) + internal override bool GetNextDelay(IEnumerable ops, AsyncOperation current, int maxValue, bool positiveDelay, bool isRecursive, out int next) { Guid id = this.GetOperationId(); diff --git a/Source/Core/Testing/Fuzzing/FuzzingStrategy.cs b/Source/Core/Testing/Fuzzing/FuzzingStrategy.cs index 443cc912a..42f8127b1 100644 --- a/Source/Core/Testing/Fuzzing/FuzzingStrategy.cs +++ b/Source/Core/Testing/Fuzzing/FuzzingStrategy.cs @@ -57,10 +57,11 @@ internal static FuzzingStrategy Create(Configuration configuration, IRandomValue /// 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(IEnumerable ops, AsyncOperation current, - int maxValue, bool positiveDelay, out int next); + int maxValue, bool positiveDelay, bool isRecursive, out int next); /// /// Returns a boolean choice to delay the current operation further. diff --git a/Source/Core/Testing/Fuzzing/PCTStrategy.cs b/Source/Core/Testing/Fuzzing/PCTStrategy.cs index c4d087be6..d7aaa093b 100644 --- a/Source/Core/Testing/Fuzzing/PCTStrategy.cs +++ b/Source/Core/Testing/Fuzzing/PCTStrategy.cs @@ -95,7 +95,7 @@ internal override bool InitializeNextIteration(uint iteration) } internal override bool GetNextDelay(IEnumerable ops, AsyncOperation current, - int maxValue, bool positiveDelay, out int next) + int maxValue, bool positiveDelay, bool isRecursive, out int next) { this.UpdateAndGetLowestPriorityEnabledOperation(ops, current, out AsyncOperation lowestEnabledOperation); @@ -112,10 +112,14 @@ internal override bool GetNextDelay(IEnumerable ops, AsyncOperat } else { - next = this.RandomValueGenerator.Next(maxValue); + next = 0; + } + + if (!isRecursive) + { + this.StepCount++; } - this.StepCount++; return true; } diff --git a/Source/Core/Testing/Fuzzing/QLearningStrategy.cs b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs index 71358a255..cda271d32 100644 --- a/Source/Core/Testing/Fuzzing/QLearningStrategy.cs +++ b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs @@ -69,7 +69,7 @@ internal QLearningStrategy(int maxSteps, IRandomValueGenerator random) /// internal override bool GetNextDelay(IEnumerable ops, AsyncOperation current, - int maxValue, bool positiveDelay, out int next) + int maxValue, bool positiveDelay, bool isRecursive, out int next) { int state = this.CaptureExecutionStep(ops, current); this.InitializeDelayQValues(state, maxValue); diff --git a/Source/Core/Testing/Fuzzing/RandomStrategy.cs b/Source/Core/Testing/Fuzzing/RandomStrategy.cs index c26394e61..cda9bc09b 100644 --- a/Source/Core/Testing/Fuzzing/RandomStrategy.cs +++ b/Source/Core/Testing/Fuzzing/RandomStrategy.cs @@ -44,7 +44,7 @@ internal override bool InitializeNextIteration(uint iteration) /// internal override bool GetNextDelay(IEnumerable ops, AsyncOperation current, - int maxValue, bool positiveDelay, out int next) + int maxValue, bool positiveDelay, bool isRecursive, out int next) { if (positiveDelay) { From d654406637b65fb0ee81405bafe9fd53c16470b7 Mon Sep 17 00:00:00 2001 From: notDhruv Date: Sun, 13 Feb 2022 08:44:11 +0000 Subject: [PATCH 10/16] Acivation mode for concurrency fuzzing --- Source/Core/Runtime/CoyoteRuntime.cs | 9 +- .../Testing/Fuzzing/BoundedRandomStrategy.cs | 6 +- Source/Core/Testing/Fuzzing/PCTStrategy.cs | 89 +++++++++++++++---- .../Core/Testing/Fuzzing/QLearningStrategy.cs | 6 +- Source/Core/Testing/Fuzzing/RandomStrategy.cs | 11 +-- global.json | 2 +- 6 files changed, 88 insertions(+), 35 deletions(-) diff --git a/Source/Core/Runtime/CoyoteRuntime.cs b/Source/Core/Runtime/CoyoteRuntime.cs index 1f15b31d6..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); @@ -1044,11 +1044,6 @@ private int GetNondeterministicDelay(AsyncOperation op, int maxValue, bool isRec // Checks if the scheduling steps bound has been reached. this.CheckIfSchedulingStepsBoundIsReached(); - if (this.OperationMap.Values.Where(v => v.Status is AsyncOperationStatus.Enabled).Count() is 1 || op.Name == "Example.Calculator(1)") - { - return 0; - } - // Choose the next delay to inject. int maxDelay = maxValue > 0 ? (int)this.Configuration.TimeoutDelay : 1; if (!this.Scheduler.GetNextDelay(this.OperationMap.Values, op, maxDelay, positiveDelay, isRecursive, out int next)) diff --git a/Source/Core/Testing/Fuzzing/BoundedRandomStrategy.cs b/Source/Core/Testing/Fuzzing/BoundedRandomStrategy.cs index 93214eecd..5413098de 100644 --- a/Source/Core/Testing/Fuzzing/BoundedRandomStrategy.cs +++ b/Source/Core/Testing/Fuzzing/BoundedRandomStrategy.cs @@ -79,7 +79,11 @@ internal override bool GetNextDelay(IEnumerable ops, AsyncOperat this.TotalTaskDelayMap.TryUpdate(id, maxDelay + next, maxDelay); } - this.StepCount++; + if (!isRecursive) + { + this.StepCount++; + } + return true; } diff --git a/Source/Core/Testing/Fuzzing/PCTStrategy.cs b/Source/Core/Testing/Fuzzing/PCTStrategy.cs index d7aaa093b..a3043ffac 100644 --- a/Source/Core/Testing/Fuzzing/PCTStrategy.cs +++ b/Source/Core/Testing/Fuzzing/PCTStrategy.cs @@ -46,7 +46,12 @@ internal sealed class PCTStrategy : FuzzingStrategy /// /// List of prioritized operations. /// - private readonly List PrioritizedOperations; + private List PrioritizedOperations; + + /// + /// List of operations that have made critical delay requests post creation. + /// + private Dictionary CriticalDelayRequest; /// /// Scheduling points in the current execution where a priority change should occur. @@ -65,6 +70,7 @@ internal PCTStrategy(int maxSteps, IRandomValueGenerator generator, int maxPrior this.MaxPrioritySwitchPoints = maxPrioritySwitchPoints; this.PrioritizedOperations = new List(); this.PriorityChangePoints = new HashSet(); + this.CriticalDelayRequest = new Dictionary(); } /// @@ -81,6 +87,8 @@ internal override bool InitializeNextIteration(uint iteration) 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)) @@ -97,27 +105,67 @@ internal override bool InitializeNextIteration(uint iteration) internal override bool GetNextDelay(IEnumerable ops, AsyncOperation current, int maxValue, bool positiveDelay, bool isRecursive, out int next) { - this.UpdateAndGetLowestPriorityEnabledOperation(ops, current, out AsyncOperation lowestEnabledOperation); + Console.WriteLine($"Current operation: {current.Name}"); - // if the number of delayed operations exceeds k, then don't delay the current operation. k has been chosen to be 1. - if (ops.Where(op => op.Status is AsyncOperationStatus.Delayed).Count() == 1) + // 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) { 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 (positiveDelay) - if (lowestEnabledOperation.Equals(current)) + // 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) { - next = this.RandomValueGenerator.Next(maxValue - 1) + 1; + if (!this.CriticalDelayRequest.ContainsKey(current)) + { + this.CriticalDelayRequest[current] = false; + } + else + { + this.CriticalDelayRequest[current] = true; + } } - else + + // 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.UpdateAndGetLowestPriorityEnabledOperation(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 = 0; + this.StepCount += (current.Name is "'Task(0)'") ? 0 : 1; + return true; } + // 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++; + this.StepCount += (current.Name is "'Task(0)'") ? 0 : 1; } return true; @@ -125,9 +173,9 @@ internal override bool GetNextDelay(IEnumerable ops, AsyncOperat internal override bool GetNextRecursiveDelayChoice(IEnumerable ops, AsyncOperation current) { - this.UpdateAndGetLowestPriorityEnabledOperation(ops, current, out AsyncOperation lowestEnabledOperation); + this.UpdateAndGetLowestPriorityEnabledOperation(ops, current, out AsyncOperation HighestEnabledOperation); - if (lowestEnabledOperation.Equals(current)) + if (HighestEnabledOperation.Equals(current)) { return true; } @@ -137,20 +185,25 @@ internal override bool GetNextRecursiveDelayChoice(IEnumerable o /// internal bool UpdateAndGetLowestPriorityEnabledOperation(IEnumerable ops, AsyncOperation current, - out AsyncOperation lowestEnabledOperation) + out AsyncOperation HighestEnabledOperation) { - lowestEnabledOperation = null; - var enabledOps = ops.Where(op => op.Status is AsyncOperationStatus.Enabled).ToList(); - if (enabledOps.Count is 0) + 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(enabledOps, current); - this.DeprioritizeEnabledOperationWithHighestPriority(enabledOps); + this.SetNewOperationPriorities(criticalOps, current); + this.DeprioritizeEnabledOperationWithHighestPriority(criticalOps); this.DebugPrintOperationPriorityList(); - lowestEnabledOperation = this.GetEnabledOperationWithLowestPriority(enabledOps); + // HighestEnabledOperation = this.GetEnabledOperationWithLowestPriority(criticalOps); // Case: (n-1) PCT + HighestEnabledOperation = this.GetEnabledOperationWithHighestPriority(criticalOps); // Case: (1) PCT return true; } diff --git a/Source/Core/Testing/Fuzzing/QLearningStrategy.cs b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs index cda271d32..07b11e237 100644 --- a/Source/Core/Testing/Fuzzing/QLearningStrategy.cs +++ b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs @@ -77,7 +77,11 @@ internal override bool GetNextDelay(IEnumerable ops, AsyncOperat next = this.GetNextDelayByPolicy(state, maxValue); this.PreviousDelay = next; - this.StepCount++; + if (!isRecursive) + { + this.StepCount++; + } + return true; } diff --git a/Source/Core/Testing/Fuzzing/RandomStrategy.cs b/Source/Core/Testing/Fuzzing/RandomStrategy.cs index cda9bc09b..02f8d669b 100644 --- a/Source/Core/Testing/Fuzzing/RandomStrategy.cs +++ b/Source/Core/Testing/Fuzzing/RandomStrategy.cs @@ -46,16 +46,13 @@ internal override bool InitializeNextIteration(uint iteration) internal override bool GetNextDelay(IEnumerable ops, AsyncOperation current, int maxValue, bool positiveDelay, bool isRecursive, out int next) { - if (positiveDelay) - { - next = this.RandomValueGenerator.Next(maxValue - 1) + 1; - } - else + next = this.RandomValueGenerator.Next(maxValue); + + if (!isRecursive) { - next = this.RandomValueGenerator.Next(maxValue); + this.StepCount++; } - this.StepCount++; return true; } 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" } } From a1047cbfc0d38310dabd9a175707f29f0b687249 Mon Sep 17 00:00:00 2001 From: notDhruv Date: Sun, 13 Feb 2022 08:51:00 +0000 Subject: [PATCH 11/16] . --- Source/Core/Testing/Fuzzing/PCTStrategy.cs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/Core/Testing/Fuzzing/PCTStrategy.cs b/Source/Core/Testing/Fuzzing/PCTStrategy.cs index a3043ffac..51ce51669 100644 --- a/Source/Core/Testing/Fuzzing/PCTStrategy.cs +++ b/Source/Core/Testing/Fuzzing/PCTStrategy.cs @@ -136,7 +136,7 @@ internal override bool GetNextDelay(IEnumerable ops, AsyncOperat // Console.WriteLine($"OpId: {current.Id} Status: {current.Status}"); // Update the priority list with new operations and return the highest priority operation - this.UpdateAndGetLowestPriorityEnabledOperation(ops, current, out AsyncOperation HighestEnabledOperation); + this.UpdateAndGetHighestPriorityEnabledOperation(ops, current, out AsyncOperation HighestEnabledOperation); // Console.WriteLine($"{HighestEnabledOperation.Name}"); @@ -173,7 +173,7 @@ internal override bool GetNextDelay(IEnumerable ops, AsyncOperat internal override bool GetNextRecursiveDelayChoice(IEnumerable ops, AsyncOperation current) { - this.UpdateAndGetLowestPriorityEnabledOperation(ops, current, out AsyncOperation HighestEnabledOperation); + this.UpdateAndGetHighestPriorityEnabledOperation(ops, current, out AsyncOperation HighestEnabledOperation); if (HighestEnabledOperation.Equals(current)) { @@ -184,7 +184,7 @@ internal override bool GetNextRecursiveDelayChoice(IEnumerable o } /// - internal bool UpdateAndGetLowestPriorityEnabledOperation(IEnumerable ops, AsyncOperation current, + internal bool UpdateAndGetHighestPriorityEnabledOperation(IEnumerable ops, AsyncOperation current, out AsyncOperation HighestEnabledOperation) { HighestEnabledOperation = null; From 9ff5a575652497ad9bb5e8fd6e3e550c3fdd304a Mon Sep 17 00:00:00 2001 From: notDhruv Date: Sun, 13 Feb 2022 09:38:48 +0000 Subject: [PATCH 12/16] Debug priority list --- Source/Core/Testing/Fuzzing/PCTStrategy.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/Core/Testing/Fuzzing/PCTStrategy.cs b/Source/Core/Testing/Fuzzing/PCTStrategy.cs index 51ce51669..2285564e9 100644 --- a/Source/Core/Testing/Fuzzing/PCTStrategy.cs +++ b/Source/Core/Testing/Fuzzing/PCTStrategy.cs @@ -221,7 +221,7 @@ private void SetNewOperationPriorities(List ops, AsyncOperation 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) + 1; + 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); } From 0d8bf5ebb2be1963498e0af2ae050e5ca2474a73 Mon Sep 17 00:00:00 2001 From: notDhruv Date: Sun, 13 Feb 2022 09:41:40 +0000 Subject: [PATCH 13/16] Debugging --- Source/Core/Testing/Fuzzing/PCTStrategy.cs | 24 +++++++++++----------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/Source/Core/Testing/Fuzzing/PCTStrategy.cs b/Source/Core/Testing/Fuzzing/PCTStrategy.cs index 2285564e9..197517e70 100644 --- a/Source/Core/Testing/Fuzzing/PCTStrategy.cs +++ b/Source/Core/Testing/Fuzzing/PCTStrategy.cs @@ -118,7 +118,7 @@ internal override bool GetNextDelay(IEnumerable ops, AsyncOperat } // if the operation has not yet asked a critical delay request, include it as a potential operation - // (critical request status: false). + // (critical request status: false). // If it has been included already, then update its critical request status to true if (!isRecursive) { @@ -136,11 +136,11 @@ internal override bool GetNextDelay(IEnumerable ops, AsyncOperat // 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); + this.UpdateAndGetHighestPriorityEnabledOperation(ops, current, out AsyncOperation highestEnabledOperation); - // Console.WriteLine($"{HighestEnabledOperation.Name}"); + // Console.WriteLine($"{highestEnabledOperation.Name}"); - // if the current operation is making a non-critical request (request for delay before creation) then assign zero delay. + // 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]) { @@ -150,7 +150,7 @@ internal override bool GetNextDelay(IEnumerable ops, AsyncOperat } // Assign zero delay if the current operation is the highest enabled operation otherwise delay it. - if (HighestEnabledOperation.Equals(current)) + if (highestEnabledOperation.Equals(current)) { next = 0; } @@ -173,9 +173,9 @@ internal override bool GetNextDelay(IEnumerable ops, AsyncOperat internal override bool GetNextRecursiveDelayChoice(IEnumerable ops, AsyncOperation current) { - this.UpdateAndGetHighestPriorityEnabledOperation(ops, current, out AsyncOperation HighestEnabledOperation); + this.UpdateAndGetHighestPriorityEnabledOperation(ops, current, out AsyncOperation highestEnabledOperation); - if (HighestEnabledOperation.Equals(current)) + if (highestEnabledOperation.Equals(current)) { return true; } @@ -185,12 +185,12 @@ internal override bool GetNextRecursiveDelayChoice(IEnumerable o /// internal bool UpdateAndGetHighestPriorityEnabledOperation(IEnumerable ops, AsyncOperation current, - out AsyncOperation HighestEnabledOperation) + out AsyncOperation highestEnabledOperation) { - HighestEnabledOperation = null; + 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) && + => (op.Status is AsyncOperationStatus.Enabled || op.Status is AsyncOperationStatus.Delayed) && this.CriticalDelayRequest.ContainsKey(op) && this.CriticalDelayRequest[op]).ToList(); if (criticalOps.Count is 0) @@ -202,8 +202,8 @@ internal bool UpdateAndGetHighestPriorityEnabledOperation(IEnumerable Date: Wed, 16 Feb 2022 15:18:30 +0000 Subject: [PATCH 14/16] basic rl-fuzzing --- .../Core/Testing/Fuzzing/QLearningStrategy.cs | 367 +++++++++++++++--- 1 file changed, 311 insertions(+), 56 deletions(-) diff --git a/Source/Core/Testing/Fuzzing/QLearningStrategy.cs b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs index 07b11e237..475671999 100644 --- a/Source/Core/Testing/Fuzzing/QLearningStrategy.cs +++ b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs @@ -2,34 +2,40 @@ // Licensed under the MIT License. using System; -using System.Collections.Concurrent; using System.Collections.Generic; using System.Linq; +using Microsoft.Coyote.Actors; using Microsoft.Coyote.Runtime; namespace Microsoft.Coyote.Testing.Fuzzing { /// - /// A probabilistic fuzzing strategy that uses Q-learning. + /// A probabilistic scheduling strategy that uses Q-learning. /// - internal class QLearningStrategy : RandomStrategy + internal sealed class QLearningStrategy : RandomStrategy { /// - /// Map from program states to a map from next delays to their quality values. + /// Map from program states to a map from next operations to their quality values. /// - private readonly Dictionary> OperationQTable; + private readonly Dictionary> OperationQTable; /// /// The path that is being executed during the current iteration. Each - /// step of the execution is represented by a delay value and a value - /// representing the program state after the delay happened. + /// step of the execution is represented by an operation and a value + /// representing the program state after the operation executed. /// - private readonly LinkedList<(int delay, int state)> ExecutionPath; + private readonly LinkedList<(ulong op, AsyncOperationType type, int state)> ExecutionPath; /// - /// The previously chosen delay. + /// Map from values representing program states to their transition + /// frequency in the current execution path. /// - private int PreviousDelay; + private readonly Dictionary TransitionFrequencies; + + /// + /// The previously chosen operation. + /// + private ulong PreviousOperation; /// /// The value of the learning rate. @@ -41,11 +47,43 @@ internal class QLearningStrategy : RandomStrategy /// 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; + + private Dictionary OperationHashes; + + /// + /// The failure injection reward. + /// + private readonly double FailureInjectionReward; + /// /// The number of explored executions. /// @@ -55,27 +93,77 @@ internal class QLearningStrategy : RandomStrategy /// Initializes a new instance of the class. /// It uses the specified random number generator. /// - internal QLearningStrategy(int maxSteps, IRandomValueGenerator random) + public QLearningStrategy(int maxSteps, IRandomValueGenerator random) : base(maxSteps, random) { - this.OperationQTable = new Dictionary>(); - this.ExecutionPath = new LinkedList<(int, int)>(); - this.PreviousDelay = 0; + 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) { - int state = this.CaptureExecutionStep(ops, current); - this.InitializeDelayQValues(state, maxValue); + 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]); - next = this.GetNextDelayByPolicy(state, maxValue); - this.PreviousDelay = next; + this.GetNextOperation(enabledOps, current, out AsyncOperation nextOp); + + if (nextOp is null) + { + next = 0; + return true; + } + + 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) { @@ -85,16 +173,102 @@ internal override bool GetNextDelay(IEnumerable ops, AsyncOperat 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 && op.Status == AsyncOperationStatus.Enabled)) + { + 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 delay by drawing from the probability distribution - /// over the specified state and range of delays. + /// Returns the next integer choice by drawing from the probability + /// distribution over the specified state and integer choices. /// - private int GetNextDelayByPolicy(int state, int maxValue) + private int GetNextIntegerChoiceByPolicy(int state, int maxValue) { var qValues = new List(maxValue); - for (int i = 0; i < maxValue; i++) + for (ulong i = 0; i < (ulong)maxValue; i++) { - qValues.Add(this.OperationQTable[state][i]); + qValues.Add(this.OperationQTable[state][this.MinIntegerChoiceOpValue - i]); } return this.ChooseQValueIndexFromDistribution(qValues); @@ -158,32 +332,47 @@ private int ChooseQValueIndexFromDistribution(List qValues) /// Captures metadata related to the current execution step, and returns /// a value representing the current program state. /// - private int CaptureExecutionStep(IEnumerable ops, AsyncOperation operation) + private int CaptureExecutionStep(IEnumerable ops, AsyncOperation current) { - int state = ComputeStateHash(operation); + int state = this.ComputeStateHash(ops); - Console.WriteLine($">---> {operation.Name}: state: {state}"); - foreach (var op in ops) + // Update the execution path with the current state. + this.ExecutionPath.AddLast((this.PreviousOperation, current.Type, state)); + + if (!this.TransitionFrequencies.ContainsKey(state)) { - Console.WriteLine($" |---> {op.Name}: status: {op.Status}"); + this.TransitionFrequencies.Add(state, 0); } - // Update the list of chosen delays with the current state. - this.ExecutionPath.AddLast((this.PreviousDelay, state)); + // Increment the state transition frequency. + this.TransitionFrequencies[state]++; + return state; } /// /// Computes a hash representing the current program state. /// - private static int ComputeStateHash(AsyncOperation operation) + private int ComputeStateHash(IEnumerable ops) { unchecked { int hash = 19; + 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(); + // 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) // { @@ -201,22 +390,68 @@ private static int ComputeStateHash(AsyncOperation operation) } /// - /// Initializes the Q values of all delays that can be chosen at the specified state - /// that have not been previously encountered. + /// Initializes the Q values of all enabled operations that can be chosen + /// at the specified state that have not been previously encountered. /// - private void InitializeDelayQValues(int state, int maxValue) + private void InitializeOperationQValues(int state, IEnumerable ops) { - if (!this.OperationQTable.TryGetValue(state, out Dictionary qValues)) + if (!this.OperationQTable.TryGetValue(state, out Dictionary qValues)) { - qValues = new Dictionary(); + qValues = new Dictionary(); this.OperationQTable.Add(state, qValues); } - for (int i = 0; i < maxValue; i++) + foreach (var op in ops) { - if (!qValues.ContainsKey(i)) + // Assign the same initial probability for all new enabled operations. + if (op.Status == AsyncOperationStatus.Enabled && !qValues.ContainsKey(op.Id)) { - qValues.Add(i, 0); + 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); } } } @@ -226,8 +461,12 @@ internal override bool InitializeNextIteration(uint iteration) { this.LearnQValues(); this.ExecutionPath.Clear(); - this.PreviousDelay = 0; + 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); } @@ -237,16 +476,12 @@ 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.delay},{node.Value.state}), "); - - var (_, state) = node.Value; - var (nextDelay, nextState) = node.Next.Value; + var (_, _, state) = node.Value; + var (nextOp, nextType, nextState) = node.Next.Value; // Compute the max Q value. double maxQ = double.MinValue; @@ -258,32 +493,52 @@ private void LearnQValues() } } - // Compute the reward. - double reward = this.BasicActionReward; + // 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 delays that are available from the current execution step. + // Get the operations that are available from the current execution step. var currOpQValues = this.OperationQTable[state]; - if (!currOpQValues.ContainsKey(nextDelay)) + if (!currOpQValues.ContainsKey(nextOp)) { - currOpQValues.Add(nextDelay, 0); + currOpQValues.Add(nextOp, 0); } - // Update the Q value of the next delay. + // Update the Q value of the next operation. // Q = [(1-a) * Q] + [a * (rt + (g * maxQ))] - currOpQValues[nextDelay] = ((1 - this.LearningRate) * currOpQValues[nextDelay]) + + currOpQValues[nextOp] = ((1 - this.LearningRate) * currOpQValues[nextOp]) + (this.LearningRate * (reward + (this.Gamma * maxQ))); node = node.Next; idx++; } + } - Console.WriteLine($"Visited {this.OperationQTable.Count} states."); - // Console.WriteLine(pathBuilder.ToString()); + 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; + } } /// From e2f0d3ccb8cee6d2678b1e3ea79e163f01bdfe4a Mon Sep 17 00:00:00 2001 From: notDhruv Date: Tue, 22 Feb 2022 07:23:27 +0000 Subject: [PATCH 15/16] . --- .../Core/Testing/Fuzzing/QLearningStrategy.cs | 25 ++++++++++--------- 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/Source/Core/Testing/Fuzzing/QLearningStrategy.cs b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs index 475671999..9d4446232 100644 --- a/Source/Core/Testing/Fuzzing/QLearningStrategy.cs +++ b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs @@ -145,24 +145,25 @@ internal override bool GetNextDelay(IEnumerable ops, AsyncOperat if (nextOp is null) { next = 0; - return true; - } - - if (nextOp.Equals(current)) - { - next = 0; - this.PreviousOperation = nextOp.Id; } else { - next = 1; - - if (!this.RecursiveDelayCount.ContainsKey(current)) + if (nextOp.Equals(current)) { - this.RecursiveDelayCount.Add(current, 0); + next = 0; + this.PreviousOperation = nextOp.Id; } + else + { + next = 1; - this.RecursiveDelayCount[current]++; + if (!this.RecursiveDelayCount.ContainsKey(current)) + { + this.RecursiveDelayCount.Add(current, 0); + } + + this.RecursiveDelayCount[current]++; + } } if (!isRecursive) From 1d20ae7b4aa3ce0e889850106cfafc25346b0322 Mon Sep 17 00:00:00 2001 From: notDhruv Date: Fri, 25 Feb 2022 11:42:22 +0000 Subject: [PATCH 16/16] minor changes in ql strategy --- Source/Core/Testing/Fuzzing/QLearningStrategy.cs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Source/Core/Testing/Fuzzing/QLearningStrategy.cs b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs index 9d4446232..7ea762d72 100644 --- a/Source/Core/Testing/Fuzzing/QLearningStrategy.cs +++ b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs @@ -77,6 +77,9 @@ internal sealed class QLearningStrategy : RandomStrategy /// private Dictionary RecursiveDelayCount; + /// + /// Hashes of the operations each computed at their last corresponding delay point. + /// private Dictionary OperationHashes; /// @@ -230,7 +233,7 @@ private AsyncOperation GetNextOperationByPolicy(int state, IEnumerable op.Id == pair.Key && op.Status == AsyncOperationStatus.Enabled)) + if (ops.Any(op => op.Id == pair.Key)) { opIds.Add(pair.Key); qValues.Add(pair.Value); @@ -360,6 +363,8 @@ private int ComputeStateHash(IEnumerable ops) { 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;