diff --git a/Source/Core/Runtime/CoyoteRuntime.cs b/Source/Core/Runtime/CoyoteRuntime.cs index 2d4bad4c..e75a9d20 100644 --- a/Source/Core/Runtime/CoyoteRuntime.cs +++ b/Source/Core/Runtime/CoyoteRuntime.cs @@ -918,6 +918,7 @@ namespace Microsoft.Coyote.Runtime internal void DelayOperation() { int delay = 0; + AsyncOperation current = null; lock (this.SyncObject) { if (!this.IsAttached) @@ -925,7 +926,7 @@ namespace Microsoft.Coyote.Runtime 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 @@ namespace Microsoft.Coyote.Runtime } } - 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 @@ namespace Microsoft.Coyote.Runtime // 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 @@ namespace Microsoft.Coyote.Runtime /// 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 a8e70143..1cf0b23e 100644 --- a/Source/Core/Runtime/Scheduling/OperationScheduler.cs +++ b/Source/Core/Runtime/Scheduling/OperationScheduler.cs @@ -164,12 +164,13 @@ namespace Microsoft.Coyote.Runtime /// /// 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 493d5ea5..fc4422e3 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 @@ namespace Microsoft.Coyote.Testing.Fuzzing /// 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 dd64cea1..6512c85b 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 @@ namespace Microsoft.Coyote.Testing.Fuzzing /// /// 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 f4d0dfe9..109c7d34 100644 --- a/Source/Core/Testing/Fuzzing/PCTStrategy.cs +++ b/Source/Core/Testing/Fuzzing/PCTStrategy.cs @@ -77,7 +77,8 @@ namespace Microsoft.Coyote.Testing.Fuzzing } /// - 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 0cc7064d..daec9e6a 100644 --- a/Source/Core/Testing/Fuzzing/QLearningStrategy.cs +++ b/Source/Core/Testing/Fuzzing/QLearningStrategy.cs @@ -26,11 +26,6 @@ namespace Microsoft.Coyote.Testing.Fuzzing /// 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 @@ namespace Microsoft.Coyote.Testing.Fuzzing { 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 @@ namespace Microsoft.Coyote.Testing.Fuzzing } /// - 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 @@ namespace Microsoft.Coyote.Testing.Fuzzing 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 @@ namespace Microsoft.Coyote.Testing.Fuzzing /// 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 @@ namespace Microsoft.Coyote.Testing.Fuzzing // 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 @@ namespace Microsoft.Coyote.Testing.Fuzzing /// 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 @@ namespace Microsoft.Coyote.Testing.Fuzzing 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 d38c4394..90963b4d 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 @@ namespace Microsoft.Coyote.Testing.Fuzzing } /// - 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 82212ff4..69d5d9f8 100644 --- a/Source/Core/Testing/Systematic/QLearningStrategy.cs +++ b/Source/Core/Testing/Systematic/QLearningStrategy.cs @@ -359,14 +359,10 @@ namespace Microsoft.Coyote.Testing.Systematic /// 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;