Pdeligia/pct

Source/Core/Actors/ActorExecutionContext.cs

@@ -1154,8 +1154,10 @@ private EnqueueStatus EnqueueEvent(ActorId targetId, Event e, Actor sender, Even
                     "Cannot send event '{0}' to actor id '{1}' that is not bound to an actor instance.",
                     e.GetType().FullName, targetId.Value);
 
+                sender?.Operation.RacingResourceSet.Add(target.Operation.ResourceId);
                 this.Runtime.ScheduleNextOperation(sender?.Operation, SchedulingPointType.Send);
                 this.ResetProgramCounter(sender as StateMachine);
+                sender?.Operation.RacingResourceSet.Remove(target.Operation.ResourceId);
 
                 // If no group is provided we default to passing along the group from the sender.
                 if (eventGroup is null && sender != null)

Source/Core/Configuration.cs

@@ -202,6 +202,12 @@ public class Configuration
         [DataMember]
         internal bool IsProgramStateHashingEnabled;
 
+        /// <summary>
+        /// If this option is enabled, the tester is hashing the custom program state.
+        /// </summary>
+        [DataMember]
+        internal bool IsCustomProgramStateHashingEnabled;
+
         /// <summary>
         /// If this option is enabled, (safety) monitors are used in the production runtime.
         /// </summary>
@@ -296,6 +302,7 @@ protected Configuration()
             this.LivenessTemperatureThreshold = 50000;
             this.UserExplicitlySetLivenessTemperatureThreshold = false;
             this.IsProgramStateHashingEnabled = false;
+            this.IsCustomProgramStateHashingEnabled = false;
             this.IsMonitoringEnabledInInProduction = false;
             this.AttachDebugger = false;
 
@@ -389,6 +396,45 @@ public Configuration WithPrioritizationStrategy(bool isFair = false, uint priori
             return this;
         }
 
+        /// <summary>
+        /// Updates the configuration to use the group-priority-based scheduling strategy during systematic testing.
+        /// You can specify if you want to enable liveness checking, which is disabled by default, and an upper
+        /// bound of possible priority changes, which by default can be up to 10.
+        /// </summary>
+        /// <param name="isFair">If true, enable liveness checking by using fair scheduling.</param>
+        /// <param name="priorityChangeBound">Upper bound of possible priority changes per test iteration.</param>
+        public Configuration WithGroupPrioritizationStrategy(bool isFair = false, uint priorityChangeBound = 10)
+        {
+            this.SchedulingStrategy = isFair ? "fair-group-prioritization" : "group-prioritization";
+            this.StrategyBound = (int)priorityChangeBound;
+            return this;
+        }
+
+        /// <summary>
+        /// Updates the configuration to use the delay-bounding scheduling strategy during systematic testing.
+        /// You can specify if you want to enable liveness checking, which is disabled by default, and an upper
+        /// bound of possible delay points, which by default can be up to 10.
+        /// </summary>
+        /// <param name="isFair">If true, enable liveness checking by using fair scheduling.</param>
+        /// <param name="delayBound">Upper bound of possible delay points per test iteration.</param>
+        public Configuration WithDelayBoundingStrategy(bool isFair = false, uint delayBound = 10)
+        {
+            this.SchedulingStrategy = isFair ? "fair-delay-bounding" : "delay-bounding";
+            this.StrategyBound = (int)delayBound;
+            return this;
+        }
+
+        /// <summary>
+        /// Updates the configuration to use the partial-order sampling scheduling strategy during systematic testing.
+        /// You can specify if you want to enable liveness checking, which is disabled by default.
+        /// </summary>
+        /// <param name="isFair">If true, enable liveness checking by using fair scheduling.</param>
+        public Configuration WithPartialOrderSamplingStrategy(bool isFair = false)
+        {
+            this.SchedulingStrategy = isFair ? "fair-partial-order-sampling" : "partial-order-sampling";
+            return this;
+        }
+
         /// <summary>
         /// Updates the configuration to use the reinforcement learning (RL) scheduling strategy
         /// during systematic testing.
@@ -475,6 +521,16 @@ public Configuration WithSharedStateReductionEnabled(bool isEnabled = true)
             return this;
         }
 
+        /// <summary>
+        /// Updates the configuration with custom program state hashing enabled or disabled.
+        /// </summary>
+        /// <param name="isEnabled">If true, then custom program state hashing is enabled.</param>
+        public Configuration WithCustomProgramStateHashingEnabled(bool isEnabled = true)
+        {
+            this.IsCustomProgramStateHashingEnabled = isEnabled;
+            return this;
+        }
+
         /// <summary>
         /// Updates the configuration with the ability to reproduce bug traces enabled or disabled.
         /// Disabling reproducibility allows skipping errors due to uncontrolled concurrency, for

Source/Core/Runtime/CoyoteRuntime.cs

@@ -169,6 +169,11 @@ internal sealed class CoyoteRuntime : ICoyoteRuntime, IDisposable
         /// </summary>
         private readonly List<TaskLivenessMonitor> TaskLivenessMonitors;
 
+        /// <summary>
+        /// List of state hashing functions for enriching the hashed program state.
+        /// </summary>
+        private readonly List<Func<int>> StateHashers;
+
         /// <summary>
         /// The runtime completion source.
         /// </summary>
@@ -265,6 +270,9 @@ public ILogger Logger
         /// <inheritdoc/>
         public event OnFailureHandler OnFailure;
 
+        internal ThreadLocal<ControlledOperation> ThreadLocalEndingControlledOpForLastTask =
+            new ThreadLocal<ControlledOperation>(false);
+
         /// <summary>
         /// Initializes a new instance of the <see cref="CoyoteRuntime"/> class.
         /// </summary>
@@ -321,6 +329,7 @@ private CoyoteRuntime(Configuration configuration, OperationScheduler scheduler,
             this.ValueGenerator = valueGenerator;
             this.SpecificationMonitors = new List<Specifications.Monitor>();
             this.TaskLivenessMonitors = new List<TaskLivenessMonitor>();
+            this.StateHashers = new List<Func<int>>();
 
             this.ControlledTaskScheduler = new ControlledTaskScheduler(this);
             this.SyncContext = new ControlledSynchronizationContext(this);
@@ -432,7 +441,9 @@ internal void Schedule(Task task)
         /// </summary>
         internal void Schedule(Action continuation)
         {
-            ControlledOperation op = this.CreateControlledOperation();
+            ControlledOperation op = this.CreateControlledOperation(
+                this.Scheduler.Strategy is Microsoft.Coyote.Testing.Interleaving.GroupPrioritizationStrategy ?
+                this.ThreadLocalEndingControlledOpForLastTask.Value?.Group : null);
             this.ScheduleOperation(op, continuation);
             this.ScheduleNextOperation(default, SchedulingPointType.ContinueWith);
         }
@@ -526,7 +537,7 @@ internal Task ScheduleDelay(TimeSpan delay, CancellationToken cancellationToken)
                 }
 
                 // TODO: cache the dummy delay action to optimize memory.
-                ControlledOperation op = this.CreateControlledOperation(timeout);
+                ControlledOperation op = this.CreateControlledOperation(null, timeout);
                 return this.TaskFactory.StartNew(state =>
                 {
                     var delayedOp = state as ControlledOperation;
@@ -593,15 +604,10 @@ internal void RegisterKnownControlledTask(Task task)
         /// <summary>
         /// Creates a new controlled operation with an optional delay.
         /// </summary>
-        internal ControlledOperation CreateControlledOperation(uint delay = 0)
+        internal ControlledOperation CreateControlledOperation(OperationGroup group = null, uint delay = 0)
         {
             using (SynchronizedSection.Enter(this.RuntimeLock))
             {
-                // Assign the operation group associated with the execution context of the
-                // current thread, if such a group exists, else the group of the currently
-                // executing operation, if such an operation exists.
-                OperationGroup group = OperationGroup.Current ?? ExecutingOperation.Value?.Group;
-
                 // Create a new controlled operation using the next available operation id.
                 ulong operationId = this.GetNextOperationId();
                 ControlledOperation op = delay > 0 ?
@@ -1458,6 +1464,12 @@ internal TControlledOperation GetOperationWithId<TControlledOperation>(ulong ope
             return default;
         }
 
+        internal ControlledOperation GetOperationFromTask(Task task)
+        {
+            this.ControlledTasks.TryGetValue(task, out var operation);
+            return operation;
+        }
+
         /// <summary>
         /// Returns all registered operations.
         /// </summary>
@@ -1502,7 +1514,11 @@ private int GetHashedProgramState()
                     }
                     else
                     {
-                        hash *= 31 + operation.LastSchedulingPoint.GetHashCode();
+                        int operationHash = 19;
+                        operationHash = (operationHash * 31) + operation.Status.GetHashCode();
+                        operationHash = (operationHash * 31) + operation.LastSchedulingPoint.GetHashCode();
+                        operationHash = (operationHash * 31) + operation.RacingResourceSet.Count.GetHashCode();
+                        hash *= operationHash;
                     }
                 }
 
@@ -1511,10 +1527,23 @@ private int GetHashedProgramState()
                     hash *= 31 + monitor.GetHashedState();
                 }
 
+                if (this.Configuration.IsCustomProgramStateHashingEnabled)
+                {
+                    foreach (var hasher in this.StateHashers)
+                    {
+                        hash *= 31 + hasher();
+                    }
+                }
+
                 return hash;
             }
         }
 
+        /// <summary>
+        /// Registers the specified state hashing function for enriching the hashed program state.
+        /// </summary>
+        internal void RegisterStateHasher(Func<int> hasher) => this.StateHashers.Add(hasher);
+
         /// <inheritdoc/>
         public void RegisterMonitor<T>()
             where T : Specifications.Monitor =>
@@ -2037,6 +2066,7 @@ internal void NotifyAssertionFailure(string text)
                         Debugger.Break();
                     }
 
+                    this.Scheduler.Cleanup();
                     this.Detach(ExecutionStatus.BugFound);
                 }
             }
@@ -2276,7 +2306,9 @@ internal void PopulateTestReport(ITestReport report)
             using (SynchronizedSection.Enter(this.RuntimeLock))
             {
                 bool isBugFound = this.ExecutionStatus is ExecutionStatus.BugFound;
-                report.SetSchedulingStatistics(isBugFound, this.BugReport, this.OperationMap.Count,
+                int numGroups = this.OperationMap.Values.Select(op => op.Group).Distinct().Count();
+                int numStates = this.Scheduler.GetNumVisitedStates();
+                report.SetSchedulingStatistics(isBugFound, this.BugReport, this.OperationMap.Count, numGroups, numStates,
                     (int)this.MaxConcurrencyDegree, this.Scheduler.StepCount, this.Scheduler.IsMaxStepsReached,
                     this.Scheduler.IsScheduleFair);
                 if (isBugFound)
@@ -2430,6 +2462,7 @@ private void Dispose(bool disposing)
                     this.UncontrolledInvocations.Clear();
                     this.SpecificationMonitors.Clear();
                     this.TaskLivenessMonitors.Clear();
+                    this.StateHashers.Clear();
 
                     this.DefaultActorExecutionContext.Dispose();
                     this.ControlledTaskScheduler.Dispose();

Source/Core/Runtime/ExecutionTrace.cs

@@ -131,6 +131,11 @@ private void Push(Step step)
         {
             if (this.Length > 0)
             {
+                if (this.Steps[this.Length - 1] is null)
+                {
+                    return;
+                }
+
                 this.Steps[this.Length - 1].Next = step;
                 step.Previous = this.Steps[this.Length - 1];
             }

Source/Core/Runtime/Operations/ControlledOperation.cs

@@ -44,6 +44,10 @@ internal class ControlledOperation : IEquatable<ControlledOperation>, IDisposabl
         /// </summary>
         private readonly Queue<Action> Continuations;
 
+        internal readonly Guid ResourceId;
+
+        internal HashSet<Guid> RacingResourceSet;
+
         /// <summary>
         /// Dependency that must get resolved before this operation can resume executing.
         /// </summary>
@@ -105,6 +109,8 @@ internal ControlledOperation(ulong operationId, string name, OperationGroup grou
             this.Status = OperationStatus.None;
             this.Group = group ?? OperationGroup.Create(this);
             this.Continuations = new Queue<Action>();
+            this.ResourceId = Guid.NewGuid();
+            this.RacingResourceSet = new HashSet<Guid> { this.ResourceId };
             this.SyncEvent = new ManualResetEventSlim(false);
             this.LastSchedulingPoint = SchedulingPointType.Start;
             this.LastHashedProgramState = 0;
@@ -180,11 +186,25 @@ internal bool TryEnable()
                 this.Dependency = null;
                 this.IsDependencyUncontrolled = false;
                 this.Status = OperationStatus.Enabled;
+                this.RacingResourceSet.Clear();
+                this.RacingResourceSet.Add(this.ResourceId);
             }
 
             return this.Status is OperationStatus.Enabled;
         }
 
+        internal static bool IsRacing(ControlledOperation op1, ControlledOperation op2)
+        {
+            if (op1.RacingResourceSet.Count is 0 || op2.RacingResourceSet.Count is 0)
+            {
+                return false;
+            }
+
+            var temp = new HashSet<Guid>(op1.RacingResourceSet);
+            temp.IntersectWith(op2.RacingResourceSet);
+            return temp.Count > 0;
+        }
+
         /// <summary>
         /// Returns the hashed state of this operation for the specified policy.
         /// </summary>

Source/Core/Runtime/Operations/OperationGroup.cs

@@ -4,6 +4,7 @@
 using System;
 using System.Collections;
 using System.Collections.Generic;
+using System.Linq;
 using System.Threading;
 
 namespace Microsoft.Coyote.Runtime
@@ -86,6 +87,11 @@ public IEnumerator<ControlledOperation> GetEnumerator()
         /// </summary>
         internal bool IsMember(ControlledOperation operation) => this.Members.Contains(operation);
 
+        /// <summary>
+        /// Determines whether all members of this group have completed.
+        /// </summary>
+        internal bool IsCompleted() => this.Members.All(op => op.Status is OperationStatus.Completed);
+
         /// <summary>
         /// Associates the specified operation group with the currently executing thread,
         /// allowing future retrieval in the same thread, as well as across threads that

Source/Core/Runtime/Resource.cs

@@ -1,6 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
+using System;
 using System.Collections.Generic;
 
 namespace Microsoft.Coyote.Runtime
@@ -15,6 +16,11 @@ internal class Resource
         /// </summary>
         internal readonly CoyoteRuntime Runtime;
 
+        /// <summary>
+        /// The unique id of this resource.
+        /// </summary>
+        internal readonly Guid Id;
+
         /// <summary>
         /// Set of asynchronous operations that are waiting on the resource to be released.
         /// </summary>
@@ -26,6 +32,7 @@ internal class Resource
         internal Resource()
         {
             this.Runtime = CoyoteRuntime.Current;
+            this.Id = Guid.NewGuid();
             this.AwaitingOperations = new HashSet<ControlledOperation>();
         }
 

Source/Core/Runtime/Scheduling/OperationScheduler.cs

@@ -23,7 +23,7 @@ internal sealed class OperationScheduler
         /// <summary>
         /// The installed program exploration strategy.
         /// </summary>
-        private readonly ExplorationStrategy Strategy;
+        internal readonly ExplorationStrategy Strategy;
 
         /// <summary>
         /// The installed schedule reducers, if any.
@@ -237,5 +237,9 @@ internal bool GetNextDelay(IEnumerable<ControlledOperation> ops, ControlledOpera
         /// Returns the last scheduling error, or the empty string if there is none.
         /// </summary>
         internal string GetLastError() => this.Strategy.ErrorText;
+
+        internal int GetNumVisitedStates() => (this.Strategy as QLearningStrategy)?.GetNumVisitedStates() ?? 0;
+
+        internal void Cleanup() => (this.Strategy as QLearningStrategy)?.Cleanup();
     }
 }

Source/Core/Runtime/Scheduling/SchedulingPoint.cs

@@ -1,6 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
+using System;
 using System.Collections.Generic;
 
 namespace Microsoft.Coyote.Runtime
@@ -156,6 +157,19 @@ public static void SetCheckpoint()
             }
         }
 
+        /// <summary>
+        /// Registers the specified state hashing function. The testing engine may use this function
+        /// to enrich the hashed program state used by specific exploration strategies.
+        /// </summary>
+        public static void RegisterStateHasher(Func<int> hasher)
+        {
+            var runtime = CoyoteRuntime.Current;
+            if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving)
+            {
+                runtime.RegisterStateHasher(hasher);
+            }
+        }
+
         /// <summary>
         /// Returns true if the specified scheduling point is used-defined.
         /// </summary>