diff --git a/Source/Core/Actors/ActorExecutionContext.cs b/Source/Core/Actors/ActorExecutionContext.cs index caebecf59..04c1f55d1 100644 --- a/Source/Core/Actors/ActorExecutionContext.cs +++ b/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) diff --git a/Source/Core/Configuration.cs b/Source/Core/Configuration.cs index 8470d14c9..a9db400d5 100644 --- a/Source/Core/Configuration.cs +++ b/Source/Core/Configuration.cs @@ -202,6 +202,12 @@ public class Configuration [DataMember] internal bool IsProgramStateHashingEnabled; + /// + /// If this option is enabled, the tester is hashing the custom program state. + /// + [DataMember] + internal bool IsCustomProgramStateHashingEnabled; + /// /// If this option is enabled, (safety) monitors are used in the production runtime. /// @@ -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; } + /// + /// 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. + /// + /// If true, enable liveness checking by using fair scheduling. + /// Upper bound of possible priority changes per test iteration. + public Configuration WithGroupPrioritizationStrategy(bool isFair = false, uint priorityChangeBound = 10) + { + this.SchedulingStrategy = isFair ? "fair-group-prioritization" : "group-prioritization"; + this.StrategyBound = (int)priorityChangeBound; + return this; + } + + /// + /// 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. + /// + /// If true, enable liveness checking by using fair scheduling. + /// Upper bound of possible delay points per test iteration. + public Configuration WithDelayBoundingStrategy(bool isFair = false, uint delayBound = 10) + { + this.SchedulingStrategy = isFair ? "fair-delay-bounding" : "delay-bounding"; + this.StrategyBound = (int)delayBound; + return this; + } + + /// + /// 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. + /// + /// If true, enable liveness checking by using fair scheduling. + public Configuration WithPartialOrderSamplingStrategy(bool isFair = false) + { + this.SchedulingStrategy = isFair ? "fair-partial-order-sampling" : "partial-order-sampling"; + return this; + } + /// /// 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; } + /// + /// Updates the configuration with custom program state hashing enabled or disabled. + /// + /// If true, then custom program state hashing is enabled. + public Configuration WithCustomProgramStateHashingEnabled(bool isEnabled = true) + { + this.IsCustomProgramStateHashingEnabled = isEnabled; + return this; + } + /// /// Updates the configuration with the ability to reproduce bug traces enabled or disabled. /// Disabling reproducibility allows skipping errors due to uncontrolled concurrency, for diff --git a/Source/Core/Runtime/CoyoteRuntime.cs b/Source/Core/Runtime/CoyoteRuntime.cs index 4818bd6ae..b4849a3bd 100644 --- a/Source/Core/Runtime/CoyoteRuntime.cs +++ b/Source/Core/Runtime/CoyoteRuntime.cs @@ -169,6 +169,11 @@ internal sealed class CoyoteRuntime : ICoyoteRuntime, IDisposable /// private readonly List TaskLivenessMonitors; + /// + /// List of state hashing functions for enriching the hashed program state. + /// + private readonly List> StateHashers; + /// /// The runtime completion source. /// @@ -265,6 +270,9 @@ public ILogger Logger /// public event OnFailureHandler OnFailure; + internal ThreadLocal ThreadLocalEndingControlledOpForLastTask = + new ThreadLocal(false); + /// /// Initializes a new instance of the class. /// @@ -321,6 +329,7 @@ private CoyoteRuntime(Configuration configuration, OperationScheduler scheduler, this.ValueGenerator = valueGenerator; this.SpecificationMonitors = new List(); this.TaskLivenessMonitors = new List(); + this.StateHashers = new List>(); this.ControlledTaskScheduler = new ControlledTaskScheduler(this); this.SyncContext = new ControlledSynchronizationContext(this); @@ -432,7 +441,9 @@ internal void Schedule(Task task) /// 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) /// /// Creates a new controlled operation with an optional delay. /// - 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(ulong ope return default; } + internal ControlledOperation GetOperationFromTask(Task task) + { + this.ControlledTasks.TryGetValue(task, out var operation); + return operation; + } + /// /// Returns all registered operations. /// @@ -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; } } + /// + /// Registers the specified state hashing function for enriching the hashed program state. + /// + internal void RegisterStateHasher(Func hasher) => this.StateHashers.Add(hasher); + /// public void RegisterMonitor() 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(); diff --git a/Source/Core/Runtime/ExecutionTrace.cs b/Source/Core/Runtime/ExecutionTrace.cs index 54220f63c..968a071ac 100644 --- a/Source/Core/Runtime/ExecutionTrace.cs +++ b/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]; } diff --git a/Source/Core/Runtime/Operations/ControlledOperation.cs b/Source/Core/Runtime/Operations/ControlledOperation.cs index b7ec08b66..a6c548e89 100644 --- a/Source/Core/Runtime/Operations/ControlledOperation.cs +++ b/Source/Core/Runtime/Operations/ControlledOperation.cs @@ -44,6 +44,10 @@ internal class ControlledOperation : IEquatable, IDisposabl /// private readonly Queue Continuations; + internal readonly Guid ResourceId; + + internal HashSet RacingResourceSet; + /// /// Dependency that must get resolved before this operation can resume executing. /// @@ -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(); + this.ResourceId = Guid.NewGuid(); + this.RacingResourceSet = new HashSet { 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(op1.RacingResourceSet); + temp.IntersectWith(op2.RacingResourceSet); + return temp.Count > 0; + } + /// /// Returns the hashed state of this operation for the specified policy. /// diff --git a/Source/Core/Runtime/Operations/OperationGroup.cs b/Source/Core/Runtime/Operations/OperationGroup.cs index e92e67b68..2edfc82cf 100644 --- a/Source/Core/Runtime/Operations/OperationGroup.cs +++ b/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 GetEnumerator() /// internal bool IsMember(ControlledOperation operation) => this.Members.Contains(operation); + /// + /// Determines whether all members of this group have completed. + /// + internal bool IsCompleted() => this.Members.All(op => op.Status is OperationStatus.Completed); + /// /// Associates the specified operation group with the currently executing thread, /// allowing future retrieval in the same thread, as well as across threads that diff --git a/Source/Core/Runtime/Resource.cs b/Source/Core/Runtime/Resource.cs index eed3cdbaa..17187dacb 100644 --- a/Source/Core/Runtime/Resource.cs +++ b/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 /// internal readonly CoyoteRuntime Runtime; + /// + /// The unique id of this resource. + /// + internal readonly Guid Id; + /// /// Set of asynchronous operations that are waiting on the resource to be released. /// @@ -26,6 +32,7 @@ internal class Resource internal Resource() { this.Runtime = CoyoteRuntime.Current; + this.Id = Guid.NewGuid(); this.AwaitingOperations = new HashSet(); } diff --git a/Source/Core/Runtime/Scheduling/OperationScheduler.cs b/Source/Core/Runtime/Scheduling/OperationScheduler.cs index 85db516a5..867a8fd6b 100644 --- a/Source/Core/Runtime/Scheduling/OperationScheduler.cs +++ b/Source/Core/Runtime/Scheduling/OperationScheduler.cs @@ -23,7 +23,7 @@ internal sealed class OperationScheduler /// /// The installed program exploration strategy. /// - private readonly ExplorationStrategy Strategy; + internal readonly ExplorationStrategy Strategy; /// /// The installed schedule reducers, if any. @@ -237,5 +237,9 @@ internal bool GetNextDelay(IEnumerable ops, ControlledOpera /// Returns the last scheduling error, or the empty string if there is none. /// internal string GetLastError() => this.Strategy.ErrorText; + + internal int GetNumVisitedStates() => (this.Strategy as QLearningStrategy)?.GetNumVisitedStates() ?? 0; + + internal void Cleanup() => (this.Strategy as QLearningStrategy)?.Cleanup(); } } diff --git a/Source/Core/Runtime/Scheduling/SchedulingPoint.cs b/Source/Core/Runtime/Scheduling/SchedulingPoint.cs index 47e95b2c9..88480e5ed 100644 --- a/Source/Core/Runtime/Scheduling/SchedulingPoint.cs +++ b/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() } } + /// + /// Registers the specified state hashing function. The testing engine may use this function + /// to enrich the hashed program state used by specific exploration strategies. + /// + public static void RegisterStateHasher(Func hasher) + { + var runtime = CoyoteRuntime.Current; + if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving) + { + runtime.RegisterStateHasher(hasher); + } + } + /// /// Returns true if the specified scheduling point is used-defined. /// diff --git a/Source/Core/Testing/ITestReport.cs b/Source/Core/Testing/ITestReport.cs index 88ccafcaf..c68feee6b 100644 --- a/Source/Core/Testing/ITestReport.cs +++ b/Source/Core/Testing/ITestReport.cs @@ -14,8 +14,8 @@ internal interface ITestReport /// /// Sets the specified scheduling statistics. /// - void SetSchedulingStatistics(bool isBugFound, string bugReport, int numOperations, int concurrencyDegree, - int scheduledSteps, bool isMaxScheduledStepsBoundReached, bool isScheduleFair); + void SetSchedulingStatistics(bool isBugFound, string bugReport, int numOperations, int numGroups, int numStates, + int concurrencyDegree, int scheduledSteps, bool isMaxScheduledStepsBoundReached, bool isScheduleFair); /// /// Sets the specified unhandled exception. diff --git a/Source/Core/Testing/Interleaving/DelayBoundingStrategy.cs b/Source/Core/Testing/Interleaving/DelayBoundingStrategy.cs new file mode 100644 index 000000000..553b8d5ec --- /dev/null +++ b/Source/Core/Testing/Interleaving/DelayBoundingStrategy.cs @@ -0,0 +1,161 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +using System; +using System.Collections.Generic; +using System.Linq; +using Microsoft.Coyote.IO; +using Microsoft.Coyote.Runtime; + +namespace Microsoft.Coyote.Testing.Interleaving +{ + /// + /// A delay-bounded scheduling strategy. + /// + /// + /// This strategy implements delay-bounded scheduling as described in the following paper: + /// https://dl.acm.org/doi/10.1145/1925844.1926432. + /// + internal sealed class DelayBoundingStrategy : RandomStrategy + { + /// + /// Ordered list of controlled operations. + /// + private readonly List Operations; + + /// + /// Scheduling points in the current iteration where a delay should occur. + /// + private readonly List RemainingDelays; + + /// + /// Number of potential delay points in the current iteration. + /// + private int NumDelayPoints; + + /// + /// Max number of potential delay points across all iterations. + /// + private int MaxDelayPoints; + + /// + /// Max number of delays per iteration. + /// + private readonly int MaxDelays; + + /// + /// Initializes a new instance of the class. + /// + internal DelayBoundingStrategy(Configuration configuration, IRandomValueGenerator generator, bool isFair) + : base(configuration, generator, isFair) + { + this.Operations = new List(); + this.RemainingDelays = new List(); + this.NumDelayPoints = 0; + this.MaxDelayPoints = 0; + this.MaxDelays = configuration.StrategyBound; + } + + /// + internal override bool InitializeNextIteration(uint iteration) + { + // 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 delay points inserted. + if (iteration > 0) + { + this.Operations.Clear(); + this.RemainingDelays.Clear(); + + this.MaxDelayPoints = Math.Max(this.MaxDelayPoints, this.NumDelayPoints); + if (this.MaxDelays > 0) + { + var delays = this.MaxDelays; + for (int i = 0; i < delays; i++) + { + this.RemainingDelays.Add(this.RandomValueGenerator.Next(this.MaxDelayPoints + 1)); + } + + this.RemainingDelays.Sort(); + } + + this.DebugPrintDelayPoints(); + } + + this.NumDelayPoints = 0; + return base.InitializeNextIteration(iteration); + } + + /// + internal override bool NextOperation(IEnumerable ops, ControlledOperation current, + bool isYielding, out ControlledOperation next) + { + if (this.IsFair && this.StepCount >= this.Configuration.MaxUnfairSchedulingSteps) + { + return base.NextOperation(ops, current, isYielding, out next); + } + + foreach (var op in ops) + { + if (!this.Operations.Contains(op)) + { + this.Operations.Add(op); + } + } + + // Get a shifted ordered list starting at the current operation to perform round-robin. + var currentIdx = this.Operations.IndexOf(current); + var orderedOps = this.Operations.GetRange(currentIdx, this.Operations.Count - currentIdx); + if (currentIdx != 0) + { + orderedOps.AddRange(this.Operations.GetRange(0, currentIdx)); + } + + int idx = 0; + var enabledOps = orderedOps.Where(op => op.Status == OperationStatus.Enabled).ToList(); + while (this.RemainingDelays.Count > 0 && this.NumDelayPoints == this.RemainingDelays.First()) + { + idx = (idx + 1) % enabledOps.Count; + this.RemainingDelays.RemoveAt(0); + Debug.WriteLine($" Inserted delay, '{this.RemainingDelays.Count}' remaining."); + } + + next = enabledOps[idx]; + this.NumDelayPoints++; + return true; + } + + /// + internal override string GetDescription() => + $"DelayBounding[fair:{this.IsFair},bound:{this.MaxDelays},seed:{this.RandomValueGenerator.Seed}]"; + + /// + internal override void Reset() + { + this.NumDelayPoints = 0; + this.RemainingDelays.Clear(); + base.Reset(); + } + + /// + /// Print the delay points, if debug is enabled. + /// + private void DebugPrintDelayPoints() + { + if (Debug.IsEnabled && this.RemainingDelays.Count > 0) + { + if (this.RemainingDelays.Count > 0) + { + var delayPoints = this.RemainingDelays.ToArray(); + Debug.WriteLine(" Assigned {0} delay points: {1}.", + delayPoints.Length, string.Join(", ", delayPoints)); + } + else + { + Debug.WriteLine(" Assigned 0 delay points."); + } + } + } + } +} diff --git a/Source/Core/Testing/Interleaving/GroupPrioritizationStrategy.cs b/Source/Core/Testing/Interleaving/GroupPrioritizationStrategy.cs new file mode 100644 index 000000000..540c46838 --- /dev/null +++ b/Source/Core/Testing/Interleaving/GroupPrioritizationStrategy.cs @@ -0,0 +1,29 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +using System; +using System.Collections.Generic; +using System.Linq; +using Microsoft.Coyote.IO; +using Microsoft.Coyote.Runtime; + +namespace Microsoft.Coyote.Testing.Interleaving +{ + /// + /// A (fair) group-based probabilistic priority-based scheduling strategy. + /// + internal sealed class GroupPrioritizationStrategy : PrioritizationStrategy + { + /// + /// Initializes a new instance of the class. + /// + internal GroupPrioritizationStrategy(Configuration configuration, IRandomValueGenerator generator, bool isFair) + : base(configuration, generator, isFair) + { + } + + /// + internal override string GetDescription() => + $"group-prioritization[fair:{this.IsFair},bound:{this.MaxPriorityChanges},seed:{this.RandomValueGenerator.Seed}]"; + } +} diff --git a/Source/Core/Testing/Interleaving/InterleavingStrategy.cs b/Source/Core/Testing/Interleaving/InterleavingStrategy.cs index 75e5243f0..7cbbb0fe8 100644 --- a/Source/Core/Testing/Interleaving/InterleavingStrategy.cs +++ b/Source/Core/Testing/Interleaving/InterleavingStrategy.cs @@ -37,6 +37,10 @@ internal static InterleavingStrategy Create(Configuration configuration, IRandom { strategy = new RandomStrategy(configuration, generator); } + else if (configuration.SchedulingStrategy is "probabilistic") + { + strategy = new ProbabilisticRandomStrategy(configuration, generator); + } else if (configuration.SchedulingStrategy is "prioritization") { strategy = new PrioritizationStrategy(configuration, generator, false); @@ -45,9 +49,29 @@ internal static InterleavingStrategy Create(Configuration configuration, IRandom { strategy = new PrioritizationStrategy(configuration, generator, true); } - else if (configuration.SchedulingStrategy is "probabilistic") + else if (configuration.SchedulingStrategy is "group-prioritization") { - strategy = new ProbabilisticRandomStrategy(configuration, generator); + strategy = new GroupPrioritizationStrategy(configuration, generator, false); + } + else if (configuration.SchedulingStrategy is "fair-group-prioritization") + { + strategy = new GroupPrioritizationStrategy(configuration, generator, true); + } + else if (configuration.SchedulingStrategy is "delay-bounding") + { + strategy = new DelayBoundingStrategy(configuration, generator, false); + } + else if (configuration.SchedulingStrategy is "fair-delay-bounding") + { + strategy = new DelayBoundingStrategy(configuration, generator, true); + } + else if (configuration.SchedulingStrategy is "partial-order-sampling") + { + strategy = new PartialOrderSamplingStrategy(configuration, generator, false); + } + else if (configuration.SchedulingStrategy is "fair-partial-order-sampling") + { + strategy = new PartialOrderSamplingStrategy(configuration, generator, true); } else if (configuration.SchedulingStrategy is "rl") { diff --git a/Source/Core/Testing/Interleaving/PartialOrderSamplingStrategy.cs b/Source/Core/Testing/Interleaving/PartialOrderSamplingStrategy.cs new file mode 100644 index 000000000..ab2bdb9ee --- /dev/null +++ b/Source/Core/Testing/Interleaving/PartialOrderSamplingStrategy.cs @@ -0,0 +1,177 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +using System; +using System.Collections.Generic; +using System.Linq; +using Microsoft.Coyote.IO; +using Microsoft.Coyote.Runtime; + +namespace Microsoft.Coyote.Testing.Interleaving +{ + /// + /// A partial-order sampling scheduling strategy. + /// + /// + /// This strategy implements partial-order sampling as described in the following paper: + /// https://link.springer.com/chapter/10.1007/978-3-319-96142-2_20. + /// + internal sealed class PartialOrderSamplingStrategy : RandomStrategy + { + /// + /// List of prioritized operations. + /// + private readonly List PrioritizedOperations; + + /// + /// Initializes a new instance of the class. + /// + internal PartialOrderSamplingStrategy(Configuration configuration, IRandomValueGenerator generator, bool isFair) + : base(configuration, generator, isFair) + { + this.PrioritizedOperations = new List(); + } + + /// + internal override bool InitializeNextIteration(uint iteration) + { + this.PrioritizedOperations.Clear(); + return base.InitializeNextIteration(iteration); + } + + /// + internal override bool NextOperation(IEnumerable ops, ControlledOperation current, + bool isYielding, out ControlledOperation next) + { + if (this.IsFair && this.StepCount >= this.Configuration.MaxUnfairSchedulingSteps) + { + return base.NextOperation(ops, current, isYielding, out next); + } + + // Set the priority of any new operations. + this.SetNewOperationPriorities(ops, current); + + // Get the highest priority operation. + ControlledOperation prioritized = this.GetOperationWithHighestPriority(ops); + + // Reset the priority of all racing operations. + foreach (var op in ops) + { + if (op != prioritized && ControlledOperation.IsRacing(prioritized, op)) + { + if (Debug.IsEnabled) + { + Debug.WriteLine($" {prioritized} and {op} are racing."); + Debug.WriteLine($" Resetting priority of {op}."); + } + + this.PrioritizedOperations.Remove(op); + } + } + + this.PrioritizedOperations.Remove(prioritized); + Debug.WriteLine($" Resetting priority of {prioritized}."); + + next = ops.First(op => op == prioritized); + return true; + } + + /// + /// Returns the operation with the highest priority. + /// + private ControlledOperation GetOperationWithHighestPriority(IEnumerable ops) + { + foreach (var operation in this.PrioritizedOperations) + { + if (ops.Any(op => op == operation)) + { + return operation; + } + } + + return null; + } + + /// + /// Sets a random priority to any new operations. + /// + private void SetNewOperationPriorities(IEnumerable ops, ControlledOperation current) + { + this.PrioritizedOperations.RemoveAll(op => op.Status is OperationStatus.Completed); + + int count = this.PrioritizedOperations.Count; + if (count is 0) + { + this.PrioritizedOperations.Add(current); + } + + // Randomize the priority of all new operations. + foreach (var op in ops.Where(o => !this.PrioritizedOperations.Contains(o))) + { + // Randomly choose a priority for this operation. + int index = this.RandomValueGenerator.Next(this.PrioritizedOperations.Count + 1); + this.PrioritizedOperations.Insert(index, op); + Debug.WriteLine(" Assigned priority '{0}' for operation '{1}'.", index, op); + } + + if (this.PrioritizedOperations.Count > count) + { + this.DebugPrintOperationPriorityList(); + } + } + + /// + /// 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 string GetDescription() => + $"PartialOrderSampling[fair:{this.IsFair},seed:{this.RandomValueGenerator.Seed}]"; + + /// + internal override void Reset() + { + this.PrioritizedOperations.Clear(); + base.Reset(); + } + + /// + /// Print the operation priority list, if debug is enabled. + /// + private void DebugPrintOperationPriorityList() + { + if (Debug.IsEnabled) + { + Debug.WriteLine(" Updated operation priority list: "); + for (int idx = 0; idx < this.PrioritizedOperations.Count; idx++) + { + var op = this.PrioritizedOperations[idx]; + if (op.Status is OperationStatus.Enabled) + { + Debug.WriteLine(" |_ [{0}] operation with id '{1}' [enabled]", idx, op); + } + else if (op.Status != OperationStatus.Completed) + { + Debug.WriteLine(" |_ [{0}] operation with id '{1}'", idx, op); + } + } + } + } + } +} diff --git a/Source/Core/Testing/Interleaving/PrioritizationStrategy.cs b/Source/Core/Testing/Interleaving/PrioritizationStrategy.cs index f2464412e..7dd591e11 100644 --- a/Source/Core/Testing/Interleaving/PrioritizationStrategy.cs +++ b/Source/Core/Testing/Interleaving/PrioritizationStrategy.cs @@ -16,32 +16,32 @@ namespace Microsoft.Coyote.Testing.Interleaving /// This strategy is based on the PCT algorithm described in the following paper: /// https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/asplos277-pct.pdf. /// - internal sealed class PrioritizationStrategy : RandomStrategy + internal class PrioritizationStrategy : RandomStrategy { /// /// List of prioritized operation groups. /// - private readonly List PrioritizedOperationGroups; + protected readonly List PrioritizedOperationGroups; /// /// Scheduling points in the current execution where a priority change should occur. /// - private readonly HashSet PriorityChangePoints; + protected readonly HashSet PriorityChangePoints; /// /// Number of potential priority change points in the current iteration. /// - private int NumPriorityChangePoints; + protected int NumPriorityChangePoints; /// /// Max number of potential priority change points across all iterations. /// - private int MaxPriorityChangePoints; + protected int MaxPriorityChangePoints; /// /// Max number of priority changes per iteration. /// - private readonly int MaxPriorityChanges; + protected readonly int MaxPriorityChanges; /// /// Initializes a new instance of the class. @@ -72,7 +72,8 @@ internal override bool InitializeNextIteration(uint iteration) this.MaxPriorityChangePoints, this.NumPriorityChangePoints); if (this.MaxPriorityChanges > 0) { - var priorityChanges = this.RandomValueGenerator.Next(this.MaxPriorityChanges) + 1; + // var priorityChanges = this.RandomValueGenerator.Next(this.MaxPriorityChanges) + 1; + var priorityChanges = this.MaxPriorityChanges; var range = Enumerable.Range(0, this.MaxPriorityChangePoints); foreach (int point in this.Shuffle(range).Take(priorityChanges)) { @@ -143,6 +144,8 @@ private OperationGroup GetOperationGroupWithHighestPriority(IEnumerable private void SetNewOperationGroupPriorities(IEnumerable ops, ControlledOperation current) { + this.PrioritizedOperationGroups.RemoveAll(group => group.IsCompleted()); + int count = this.PrioritizedOperationGroups.Count; if (count is 0) { @@ -153,7 +156,7 @@ private void SetNewOperationGroupPriorities(IEnumerable ops foreach (var group in ops.Select(op => op.Group).Where(g => !this.PrioritizedOperationGroups.Contains(g))) { // Randomly choose a priority for this group. - int index = this.RandomValueGenerator.Next(this.PrioritizedOperationGroups.Count) + 1; + int index = this.RandomValueGenerator.Next(this.PrioritizedOperationGroups.Count + 1); this.PrioritizedOperationGroups.Insert(index, group); Debug.WriteLine("[coyote::strategy] Assigned priority '{0}' for operation group '{1}'.", index, group); } @@ -190,10 +193,6 @@ private bool TryPrioritizeNextOperationGroup(IEnumerable op return false; } - /// - internal override string GetDescription() => - $"prioritization[fair:{this.IsFair},bound:{this.MaxPriorityChanges},seed:{this.RandomValueGenerator.Seed}]"; - /// /// Shuffles the specified range using the Fisher-Yates algorithm. /// @@ -214,6 +213,10 @@ private IList Shuffle(IEnumerable range) return result; } + /// + internal override string GetDescription() => + $"prioritization[fair:{this.IsFair},bound:{this.MaxPriorityChanges},seed:{this.RandomValueGenerator.Seed}]"; + /// internal override void Reset() { diff --git a/Source/Core/Testing/Interleaving/QLearningStrategy.cs b/Source/Core/Testing/Interleaving/QLearningStrategy.cs index d785bcc88..855eb0b59 100644 --- a/Source/Core/Testing/Interleaving/QLearningStrategy.cs +++ b/Source/Core/Testing/Interleaving/QLearningStrategy.cs @@ -80,6 +80,8 @@ internal sealed class QLearningStrategy : RandomStrategy /// private int Epochs; + private readonly HashSet VisitedStates; + /// /// Initializes a new instance of the class. /// It uses the specified random number generator. @@ -99,6 +101,7 @@ public QLearningStrategy(Configuration configuration, IRandomValueGenerator gene this.BasicActionReward = -1; this.FailureInjectionReward = -1000; this.Epochs = 0; + this.VisitedStates = new HashSet(); } /// @@ -116,6 +119,7 @@ internal override bool NextOperation(IEnumerable ops, Contr bool isYielding, out ControlledOperation next) { int state = this.CaptureExecutionStep(current); + this.VisitedStates.Add(state); this.InitializeOperationQValues(state, ops); next = this.GetNextOperationByPolicy(state, ops); @@ -127,6 +131,7 @@ internal override bool NextOperation(IEnumerable ops, Contr internal override bool NextBoolean(ControlledOperation current, out bool next) { int state = this.CaptureExecutionStep(current); + this.VisitedStates.Add(state); this.InitializeBooleanChoiceQValues(state); next = this.GetNextBooleanChoiceByPolicy(state); this.LastOperation = next ? this.TrueChoiceOpValue : this.FalseChoiceOpValue; @@ -137,6 +142,7 @@ internal override bool NextBoolean(ControlledOperation current, out bool next) internal override bool NextInteger(ControlledOperation current, int maxValue, out int next) { int state = this.CaptureExecutionStep(current); + this.VisitedStates.Add(state); this.InitializeIntegerChoiceQValues(state, maxValue); next = this.GetNextIntegerChoiceByPolicy(state, maxValue); this.LastOperation = this.MinIntegerChoiceOpValue - (ulong)next; @@ -392,5 +398,14 @@ private void LearnQValues() /// internal override string GetDescription() => $"rl[seed:{this.RandomValueGenerator.Seed}]"; + + internal int GetNumVisitedStates() => this.VisitedStates.Count; + + internal void Cleanup() + { + this.OperationQTable.Clear(); + this.TransitionFrequencies.Clear(); + this.ExecutionPath.Clear(); + } } } diff --git a/Source/Test/Rewriting/Types/Runtime/CompilerServices/AsyncTaskMethodBuilder.cs b/Source/Test/Rewriting/Types/Runtime/CompilerServices/AsyncTaskMethodBuilder.cs index b314170cd..485434c50 100644 --- a/Source/Test/Rewriting/Types/Runtime/CompilerServices/AsyncTaskMethodBuilder.cs +++ b/Source/Test/Rewriting/Types/Runtime/CompilerServices/AsyncTaskMethodBuilder.cs @@ -81,6 +81,13 @@ public void SetResult() IO.Debug.WriteLine("[coyote::debug] Set state machine task '{0}' from thread '{1}'.", this.MethodBuilder.Task.Id, SystemThreading.Thread.CurrentThread.ManagedThreadId); this.MethodBuilder.SetResult(); + if (this.Runtime != null) + { + // We store the Executing Controlled Operation in a data member of the runtime + // so that we can access it in the Schedule(Action callback) method which will be called immediately + // after this SetResult method is called because the task has now completed. + this.Runtime.ThreadLocalEndingControlledOpForLastTask.Value = this.Runtime.GetExecutingOperation(); + } } /// @@ -203,6 +210,13 @@ public void SetResult(TResult result) IO.Debug.WriteLine("[coyote::debug] Set state machine task '{0}' from thread '{1}'.", this.MethodBuilder.Task.Id, SystemThreading.Thread.CurrentThread.ManagedThreadId); this.MethodBuilder.SetResult(result); + if (this.Runtime != null) + { + // We store the Executing Controlled Operation in a data member of the runtime + // so that we can access it in the Schedule(Action callback) method which will be called immediately + // after this SetResult method is called because the task has now completed. + this.Runtime.ThreadLocalEndingControlledOpForLastTask.Value = this.Runtime.GetExecutingOperation(); + } } /// diff --git a/Source/Test/Rewriting/Types/Runtime/CompilerServices/YieldAwaitable.cs b/Source/Test/Rewriting/Types/Runtime/CompilerServices/YieldAwaitable.cs index aea33c5d8..e9e677888 100644 --- a/Source/Test/Rewriting/Types/Runtime/CompilerServices/YieldAwaitable.cs +++ b/Source/Test/Rewriting/Types/Runtime/CompilerServices/YieldAwaitable.cs @@ -2,6 +2,7 @@ // Licensed under the MIT License. using System; +using Microsoft.Coyote.Runtime; using Microsoft.Coyote.Runtime.CompilerServices; using SystemCompiler = System.Runtime.CompilerServices; using SystemTask = System.Threading.Tasks.Task; @@ -60,6 +61,12 @@ public struct YieldAwaiter : IControllableAwaiter, SystemCompiler.ICriticalNotif /// internal YieldAwaiter(ref SystemCompiler.YieldAwaitable.YieldAwaiter awaiter) { + if (RuntimeProvider.TryGetFromSynchronizationContext(out CoyoteRuntime runtime)) + { + // Upon await Task.Yield(), we want the continuation after yield to execute with the same priority as the code before await Task.Yield(). + runtime.ThreadLocalEndingControlledOpForLastTask.Value = runtime.GetExecutingOperation(); + } + this.Awaiter = awaiter; } diff --git a/Source/Test/Rewriting/Types/Threading/Monitor.cs b/Source/Test/Rewriting/Types/Threading/Monitor.cs index 90723593d..db1fabd2d 100644 --- a/Source/Test/Rewriting/Types/Threading/Monitor.cs +++ b/Source/Test/Rewriting/Types/Threading/Monitor.cs @@ -450,6 +450,9 @@ private SynchronizedBlock EnterLock() this.IsLockTaken = true; SystemInterlocked.Increment(ref this.UseCount); + var op = this.Resource.Runtime.GetExecutingOperation(); + op.RacingResourceSet.Add(this.Resource.Id); + if (this.Owner is null) { // If this operation is trying to acquire this lock while it is free, then inject a scheduling @@ -459,31 +462,28 @@ private SynchronizedBlock EnterLock() if (this.Owner != null) { - var op = this.Resource.Runtime.GetExecutingOperation(); if (this.Owner == op) { // The owner is re-entering the lock. this.LockCountMap[op]++; return this; } - else + + // Another op has the lock right now, so add the executing op + // to the ready queue and block it. + this.WaitQueue.Remove(op); + if (!this.ReadyQueue.Contains(op)) { - // Another op has the lock right now, so add the executing op - // to the ready queue and block it. - this.WaitQueue.Remove(op); - if (!this.ReadyQueue.Contains(op)) - { - this.ReadyQueue.Add(op); - } - - this.Resource.Wait(); - this.LockCountMap.Add(op, 1); - return this; + this.ReadyQueue.Add(op); } + + this.Resource.Wait(); + this.LockCountMap.Add(op, 1); + return this; } // The executing op acquired the lock and can proceed. - this.Owner = this.Resource.Runtime.GetExecutingOperation(); + this.Owner = op; this.LockCountMap.Add(this.Owner, 1); return this; } @@ -665,6 +665,7 @@ internal void Exit() { // Only release the lock if the invocation is not reentrant. this.LockCountMap.Remove(op); + op.RacingResourceSet.Remove(this.Resource.Id); this.UnlockNextReady(); this.Resource.Runtime.ScheduleNextOperation(op, SchedulingPointType.Release); } diff --git a/Source/Test/SystematicTesting/Reports/TestReport.cs b/Source/Test/SystematicTesting/Reports/TestReport.cs index 43c73fd0c..67b3c6a06 100644 --- a/Source/Test/SystematicTesting/Reports/TestReport.cs +++ b/Source/Test/SystematicTesting/Reports/TestReport.cs @@ -76,6 +76,30 @@ public class TestReport : ITestReport [DataMember] public int TotalControlledOperations { get; internal set; } + /// + /// The min number of operation groups. + /// + [DataMember] + public int MinOperationGroups { get; internal set; } + + /// + /// The max number of operation groups. + /// + [DataMember] + public int MaxOperationGroups { get; internal set; } + + /// + /// The total number of operation groups. + /// + [DataMember] + public int TotalOperationGroups { get; internal set; } + + /// + /// The total number of visited program states. + /// + [DataMember] + public int TotalVisitedStates { get; internal set; } + /// /// The min degree of concurrency. /// @@ -182,6 +206,10 @@ public TestReport(Configuration configuration) this.MinControlledOperations = -1; this.MaxControlledOperations = -1; this.TotalControlledOperations = 0; + this.MinOperationGroups = -1; + this.MaxOperationGroups = -1; + this.TotalOperationGroups = 0; + this.TotalVisitedStates = 0; this.MinConcurrencyDegree = -1; this.MaxConcurrencyDegree = -1; this.TotalConcurrencyDegree = 0; @@ -201,7 +229,7 @@ public TestReport(Configuration configuration) } /// - void ITestReport.SetSchedulingStatistics(bool isBugFound, string bugReport, int numOperations, + void ITestReport.SetSchedulingStatistics(bool isBugFound, string bugReport, int numOperations, int numGroups, int numStates, int concurrencyDegree, int scheduledSteps, bool isMaxScheduledStepsBoundReached, bool isScheduleFair) { if (isBugFound) @@ -218,6 +246,16 @@ void ITestReport.SetSchedulingStatistics(bool isBugFound, string bugReport, int this.MinControlledOperations = numOperations; } + this.TotalOperationGroups += numGroups; + this.MaxOperationGroups = Math.Max(this.MaxOperationGroups, numGroups); + if (this.MinOperationGroups < 0 || + this.MinOperationGroups > numGroups) + { + this.MinOperationGroups = numGroups; + } + + this.TotalVisitedStates = numStates; + this.TotalConcurrencyDegree += concurrencyDegree; this.MaxConcurrencyDegree = Math.Max(this.MaxConcurrencyDegree, concurrencyDegree); if (this.MinConcurrencyDegree < 0 || @@ -307,6 +345,18 @@ public bool Merge(TestReport testReport) this.MinControlledOperations = testReport.MinControlledOperations; } + this.TotalOperationGroups += testReport.TotalOperationGroups; + this.MaxOperationGroups = Math.Max(this.MaxOperationGroups, testReport.MaxOperationGroups); + if (testReport.MinOperationGroups >= 0 && + (this.MinOperationGroups < 0 || + this.MinOperationGroups > testReport.MinOperationGroups)) + { + this.MinOperationGroups = testReport.MinOperationGroups; + } + + // TODO: this is not accurate when merging to a non-empty report. + this.TotalVisitedStates = testReport.TotalVisitedStates; + this.TotalConcurrencyDegree += testReport.TotalConcurrencyDegree; this.MaxConcurrencyDegree = Math.Max(this.MaxConcurrencyDegree, testReport.MaxConcurrencyDegree); if (testReport.MinConcurrencyDegree >= 0 && @@ -417,6 +467,19 @@ public string GetText(Configuration configuration, string prefix = "") this.MaxControlledOperations); } + if (this.TotalOperationGroups > 0) + { + report.AppendLine(); + report.AppendFormat( + "{0} Created {1} operation group{2}: {3} (min), {4} (avg), {5} (max).", + prefix.Equals("...") ? "....." : prefix, + this.TotalOperationGroups, + this.TotalOperationGroups is 1 ? string.Empty : "s", + this.MinOperationGroups, + this.TotalOperationGroups / totalExploredSchedules, + this.MaxOperationGroups); + } + if (this.TotalConcurrencyDegree > 0) { report.AppendLine(); diff --git a/Source/Test/SystematicTesting/Reports/TraceReport.cs b/Source/Test/SystematicTesting/Reports/TraceReport.cs index d24d6b213..fec30ae38 100644 --- a/Source/Test/SystematicTesting/Reports/TraceReport.cs +++ b/Source/Test/SystematicTesting/Reports/TraceReport.cs @@ -62,6 +62,11 @@ internal static string GetJson(ExecutionTrace trace, Configuration configuration for (int idx = 0; idx < trace.Length; idx++) { ExecutionTrace.Step step = trace[idx]; + if (step is null) + { + continue; + } + if (step.Type == ExecutionTrace.DecisionType.SchedulingChoice) { report.Decisions.Add($"op({step.ScheduledOperationId})"); diff --git a/Source/Test/SystematicTesting/TestingEngine.cs b/Source/Test/SystematicTesting/TestingEngine.cs index 4a0aa61be..bd90c4cbc 100644 --- a/Source/Test/SystematicTesting/TestingEngine.cs +++ b/Source/Test/SystematicTesting/TestingEngine.cs @@ -311,8 +311,8 @@ public void Run() { aex.Handle((ex) => { - IO.Debug.WriteLine(ex.Message); - IO.Debug.WriteLine(ex.StackTrace); + Error.Report(ex.Message); + Error.Report(ex.StackTrace); return true; }); @@ -322,7 +322,7 @@ public void Run() throw; } - Error.Report("Unhandled or internal exception was thrown. Please enable debug verbosity to print more information."); + Error.Report("Unhandled or internal exception was thrown."); throw; } catch (Exception ex) @@ -525,11 +525,6 @@ runtime.SchedulingPolicy is SchedulingPolicy.Interleaving && this.Logger.WriteLine(LogSeverity.Important, $"..... Iteration #{iteration + 1} " + $"enables systematic fuzzing due to uncontrolled concurrency"); } - else if (runtime.ExecutionStatus is ExecutionStatus.BoundReached) - { - this.Logger.WriteLine(LogSeverity.Important, $"..... Iteration #{iteration + 1} " + - $"hit bound of '{this.Scheduler.StepCount}' scheduling steps"); - } else if (runtime.ExecutionStatus is ExecutionStatus.BugFound) { if (!this.Scheduler.IsReplaying) diff --git a/Tools/Coyote/Cli/CommandLineParser.cs b/Tools/Coyote/Cli/CommandLineParser.cs index fe73beceb..4c82f36c2 100644 --- a/Tools/Coyote/Cli/CommandLineParser.cs +++ b/Tools/Coyote/Cli/CommandLineParser.cs @@ -210,9 +210,15 @@ private Command CreateTestCommand(Configuration configuration) var allowedStrategies = new HashSet { "random", + "probabilistic", "prioritization", "fair-prioritization", - "probabilistic", + "group-prioritization", + "fair-group-prioritization", + "delay-bounding", + "fair-delay-bounding", + "partial-order-sampling", + "fair-partial-order-sampling", "rl", "portfolio" }; @@ -231,6 +237,7 @@ private Command CreateTestCommand(Configuration configuration) aliases: new[] { "-sv", "--strategy-value" }, description: "Set exploration strategy specific value. Supported strategies (and values): " + "(fair-)prioritization (maximum number of priority change points per iteration), " + + "(fair-)group-prioritization (maximum number of priority change points per iteration), " + "probabilistic (probability of deviating from a scheduled operation).") { ArgumentHelpName = "VALUE" @@ -822,18 +829,22 @@ private void UpdateConfigurationsWithParsedOption(OptionResult result) string strategy = result.GetValueOrDefault(); switch (strategy) { - case "prioritization": - case "fair-prioritization": + case "probabilistic": if (strategyBound is null) { - this.Configuration.StrategyBound = 10; + this.Configuration.StrategyBound = 3; } break; - case "probabilistic": + case "prioritization": + case "fair-prioritization": + case "group-prioritization": + case "fair-group-prioritization": + case "delay-bounding": + case "fair-delay-bounding": if (strategyBound is null) { - this.Configuration.StrategyBound = 3; + this.Configuration.StrategyBound = 10; } break; @@ -843,6 +854,8 @@ private void UpdateConfigurationsWithParsedOption(OptionResult result) case "portfolio": strategy = "random"; break; + case "partial-order-sampling": + case "fair-partial-order-sampling": default: break; }