microsoft
/
coyote
зеркало из
1
0
Форкнуть 0
Код Задачи Пакеты Проекты Релизы Вики Активность

nested partial order sampling strategy (#447)

This commit is contained in:
Pantazis Deligiannis 2023-01-11 06:04:32 -08:00 коммит произвёл GitHub
Родитель b6d3a83c74
Коммит 7e45bcd264
Не найден ключ, соответствующий данной подписи
Идентификатор ключа GPG: 4AEE18F83AFDEB23
13 изменённых файлов: 206 добавлений и 303 удалений
Показать статистику Скачать Patch файл Скачать Diff файл Показать все файлы Свернуть все файлы

72
Source/Core/Configuration.cs
Просмотреть файл

@ -135,10 +135,16 @@ namespace Microsoft.Coyote
internal bool IsAtomicOperationRaceCheckingEnabled;
/// <summary>
/// If enabled, shared state reduction is enabled during systematic testing.
/// If enabled, execution trace cycle reduction is enabled during systematic testing.
/// </summary>
[DataMember]
internal bool IsSharedStateReductionEnabled;
internal bool IsExecutionTraceCycleReductionEnabled;
/// <summary>
/// If enabled, partial-order sampling is enabled during systematic testing.
/// </summary>
[DataMember]
internal bool IsPartialOrderSamplingEnabled;
/// <summary>
/// If true, the tester runs all iterations up to a bound, even if a bug is found.
@ -167,11 +173,10 @@ namespace Microsoft.Coyote
internal bool UserExplicitlySetMaxFairSchedulingSteps;
/// <summary>
/// If true, then the Coyote tester will consider an execution
/// that hits the depth bound as buggy.
/// If true, then hitting the max steps bound is treated as a bug.
/// </summary>
[DataMember]
internal bool ConsiderDepthBoundHitAsBug;
internal bool FailOnMaxStepsBound;
/// <summary>
/// Value that controls the probability of triggering a timeout during systematic testing.
@ -241,12 +246,6 @@ namespace Microsoft.Coyote
[DataMember]
internal bool IsActorQuiescenceCheckingEnabledOutsideTesting;
/// <summary>
/// If enabled, the runtime can bypass scheduling suppression to avoid deadlocking during testing.
/// </summary>
[DataMember]
internal bool IsSchedulingSuppressionWeak;
/// <summary>
/// Attaches the debugger during trace replay.
/// </summary>
@ -292,7 +291,7 @@ namespace Microsoft.Coyote
internal bool IsCoverageInfoSerialized;
/// <summary>
/// If true, requests a DGML graph of the iteration that contains a bug, if a bug is found.
/// If true, requests a visual graph of the iteration that contains a bug, if a bug is found.
/// This is different from a coverage activity graph, as it will also show actor instances.
/// </summary>
[DataMember]
@ -336,12 +335,13 @@ namespace Microsoft.Coyote
this.IsCollectionAccessRaceCheckingEnabled = true;
this.IsLockAccessRaceCheckingEnabled = true;
this.IsAtomicOperationRaceCheckingEnabled = true;
this.IsSharedStateReductionEnabled = false;
this.IsExecutionTraceCycleReductionEnabled = false;
this.IsPartialOrderSamplingEnabled = false;
this.RunTestIterationsToCompletion = false;
this.MaxUnfairSchedulingSteps = 10000;
this.MaxFairSchedulingSteps = 100000; // 10 times the unfair steps.
this.UserExplicitlySetMaxFairSchedulingSteps = false;
this.ConsiderDepthBoundHitAsBug = false;
this.FailOnMaxStepsBound = false;
this.StrategyBound = 0;
this.TimeoutDelay = 10;
this.DeadlockTimeout = 1000;
@ -353,7 +353,6 @@ namespace Microsoft.Coyote
this.IsImplicitProgramStateHashingEnabled = false;
this.IsMonitoringEnabledOutsideTesting = false;
this.IsActorQuiescenceCheckingEnabledOutsideTesting = false;
this.IsSchedulingSuppressionWeak = false;
this.AttachDebugger = false;
this.IsUncontrolledInvocationStackTraceLoggingEnabled = false;
@ -633,15 +632,37 @@ namespace Microsoft.Coyote
}
/// <summary>
/// Updates the configuration with shared state reduction enabled or disabled. If this
/// Updates the configuration with execution trace reduction enabled or disabled. If this
/// reduction strategy is enabled, then the runtime will attempt to reduce the schedule
/// space by taking into account any 'READ' and 'WRITE' operations declared by invoking
/// space by identifying and de-prioritizing cycles in the execution trace.
/// </summary>
/// <param name="isEnabled">If true, then execution trace reduction is enabled.</param>
public Configuration WithExecutionTraceCycleReductionEnabled(bool isEnabled = true)
{
this.IsExecutionTraceCycleReductionEnabled = isEnabled;
return this;
}
/// <summary>
/// Updates the configuration with partial-order sampling enabled or disabled. If this
/// reduction strategy is enabled, then the runtime will attempt to reduce the schedule
/// space by taking into account any 'READ' and 'WRITE' races declared by invoking
/// <see cref="SchedulingPoint.Read"/> and <see cref="SchedulingPoint.Write"/>.
/// </summary>
/// <param name="isEnabled">If true, then shared state reduction is enabled.</param>
public Configuration WithSharedStateReductionEnabled(bool isEnabled = true)
/// <param name="isEnabled">If true, then partial-order sampling is enabled.</param>
public Configuration WithPartialOrderSamplingEnabled(bool isEnabled = true)
{
this.IsSharedStateReductionEnabled = isEnabled;
this.IsPartialOrderSamplingEnabled = isEnabled;
return this;
}
/// <summary>
/// Updates the configuration to treat reaching the execution steps bound as a bug during testing.
/// </summary>
/// <param name="isEnabled">If true, then reaching the execution steps bound is treated as a bug.</param>
public Configuration WithFailureOnMaxStepsBoundEnabled(bool isEnabled = true)
{
this.FailOnMaxStepsBound = isEnabled;
return this;
}
@ -833,7 +854,7 @@ namespace Microsoft.Coyote
/// <summary>
/// Updates the configuration with trace visualization enabled or disabled.
/// If enabled, the testing engine can produce a DGML graph representing
/// If enabled, the testing engine can produce a visual graph representing
/// an execution leading up to a bug.
/// </summary>
/// <param name="isEnabled">If true, then enables trace visualization.</param>
@ -873,15 +894,6 @@ namespace Microsoft.Coyote
return this;
}
/// <summary>
/// Updates the configuration to enable weak scheduling suppression during testing.
/// </summary>
public Configuration WithWeakSchedulingSuppressionEnabled(bool isEnabled = true)
{
this.IsSchedulingSuppressionWeak = isEnabled;
return this;
}
/// <summary>
/// Updates the configuration to allow the runtime to check for actor quiescence
/// outside the scope of the testing engine.

118
Source/Core/Runtime/CompilerServices/SignalAwaitable.cs
Просмотреть файл

@ -1,118 +0,0 @@
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
using System;
using System.Runtime.CompilerServices;
namespace Microsoft.Coyote.Runtime.CompilerServices
{
/// <summary>
/// Provides an awaitable object that pauses the executing operation until a signal happens.
/// </summary>
/// <remarks>This type is intended for compiler use only.</remarks>
[System.ComponentModel.EditorBrowsable(System.ComponentModel.EditorBrowsableState.Never)]
public readonly struct SignalAwaitable
{
/// <summary>
/// The paused operation awaiter.
/// </summary>
private readonly SignalAwaiter Awaiter;
/// <summary>
/// Initializes a new instance of the <see cref="SignalAwaitable"/> struct.
/// </summary>
internal SignalAwaitable(CoyoteRuntime runtime, ControlledOperation op, string name) =>
this.Awaiter = new SignalAwaiter(runtime, op, name);
/// <summary>
/// Returns an awaiter for this awaitable object.
/// </summary>
/// <returns>The awaiter.</returns>
public SignalAwaiter GetAwaiter() => this.Awaiter;
/// <summary>
/// Provides an awaiter that that pauses the this.Operationly executing operation until a signal happens.
/// </summary>
/// <remarks>This type is intended for compiler use only.</remarks>
public struct SignalAwaiter : IControllableAwaiter, ICriticalNotifyCompletion, INotifyCompletion
{
/// <summary>
/// The runtime managing the paused operation.
/// </summary>
private readonly CoyoteRuntime Runtime;
/// <summary>
/// The paused operation.
/// </summary>
private readonly ControlledOperation Operation;
/// <summary>
/// The name of the signal being awaited.
/// </summary>
private readonly string Name;
/// <summary>
/// The yield awaiter.
/// </summary>
private readonly YieldAwaitable.YieldAwaiter Awaiter;
/// <summary>
/// True if the awaiter has completed, else false.
/// </summary>
#pragma warning disable CA1822 // Mark members as static
public bool IsCompleted => false;
#pragma warning restore CA1822 // Mark members as static
/// <inheritdoc/>
bool IControllableAwaiter.IsControlled => true;
/// <summary>
/// Initializes a new instance of the <see cref="SignalAwaiter"/> struct.
/// </summary>
internal SignalAwaiter(CoyoteRuntime runtime, ControlledOperation op, string name)
{
this.Runtime = runtime;
this.Operation = op;
this.Name = name;
this.Awaiter = default;
}
/// <summary>
/// Ends asynchronously waiting for the completion of the awaiter.
/// </summary>
public void GetResult() => this.Awaiter.GetResult();
/// <summary>
/// Sets the action to perform when the controlled task completes.
/// </summary>
public void OnCompleted(Action continuation)
{
if (this.Runtime is null || this.Operation is null)
{
this.Awaiter.OnCompleted(continuation);
}
else
{
this.Runtime.Schedule(continuation, preCondition: this.WaitSignal);
}
}
/// <summary>
/// Schedules the continuation action that is invoked when the controlled task completes.
/// </summary>
public void UnsafeOnCompleted(Action continuation)
{
if (this.Runtime is null || this.Operation is null)
{
this.Awaiter.UnsafeOnCompleted(continuation);
}
else
{
this.Runtime.Schedule(continuation, preCondition: this.WaitSignal);
}
}
private void WaitSignal() => SchedulingPoint.Wait(this.Name);
}
}
}

37
Source/Core/Runtime/CoyoteRuntime.cs
Просмотреть файл

@ -145,16 +145,6 @@ namespace Microsoft.Coyote.Runtime
/// </summary>
private readonly HashSet<string> UncontrolledInvocations;
/// <summary>
/// Map from signal names to their corresponding counters.
/// </summary>
internal readonly Dictionary<string, int> SignalMap;
/// <summary>
/// Map from operation ids to the name of the signal they are awaiting.
/// </summary>
internal readonly Dictionary<ulong, string> OperationSignalAwaiters;
/// <summary>
/// The currently scheduled operation during systematic testing.
/// </summary>
@ -330,8 +320,6 @@ namespace Microsoft.Coyote.Runtime
this.ControlledTasks = new ConcurrentDictionary<Task, ControlledOperation>();
this.UncontrolledTasks = new ConcurrentDictionary<Task, string>();
this.UncontrolledInvocations = new HashSet<string>();
this.SignalMap = new Dictionary<string, int>();
this.OperationSignalAwaiters = new Dictionary<ulong, string>();
this.CompletionSource = new TaskCompletionSource<bool>();
if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)
@ -1325,27 +1313,6 @@ namespace Microsoft.Coyote.Runtime
break;
}
if (enabledOpsCount is 0 && this.OperationMap.Values.Any(op => op.Status is OperationStatus.Suppressed))
{
if (this.Configuration.IsSchedulingSuppressionWeak)
{
// Enable all suppressed operations, to avoid deadlocking the program.
foreach (var op in this.OperationMap.Values)
{
if (op.Status is OperationStatus.Suppressed)
{
op.Status = OperationStatus.Enabled;
}
}
this.OperationSignalAwaiters.Clear();
}
else
{
this.NotifyAssertionFailure("Only suppressed operations remain.");
}
}
this.LogWriter.LogDebug("[coyote::debug] There are {0} enabled operations in runtime '{1}'.",
enabledOpsCount, this.Id);
this.MaxConcurrencyDegree = Math.Max(this.MaxConcurrencyDegree, enabledOpsCount);
@ -2079,7 +2046,7 @@ namespace Microsoft.Coyote.Runtime
if (this.Scheduler.IsMaxStepsReached)
{
string message = $"Scheduling steps bound of {this.Scheduler.StepCount} reached.";
if (this.Configuration.ConsiderDepthBoundHitAsBug)
if (this.Configuration.FailOnMaxStepsBound)
{
this.NotifyAssertionFailure(message);
}
@ -2637,8 +2604,6 @@ namespace Microsoft.Coyote.Runtime
this.SpecificationMonitors.Clear();
this.TaskLivenessMonitors.Clear();
this.StateHashingFunctions.Clear();
this.SignalMap.Clear();
this.OperationSignalAwaiters.Clear();
if (!(this.Extension is NullRuntimeExtension))
{

8
Source/Core/Runtime/Operations/ControlledOperation.cs
Просмотреть файл

@ -70,6 +70,13 @@ namespace Microsoft.Coyote.Runtime
/// </summary>
internal string LastAccessedSharedState;
/// <summary>
/// A comparer that checks if the shared state being accessed when this
/// operation last executed is equal with another shared state that is
/// being accessed by some other operation.
/// </summary>
internal IEqualityComparer<string> LastAccessedSharedStateComparer;
/// <summary>
/// True if the source of this operation is uncontrolled, else false.
/// </summary>
@ -109,6 +116,7 @@ namespace Microsoft.Coyote.Runtime
this.LastSchedulingPoint = SchedulingPointType.Start;
this.LastHashedProgramState = 0;
this.LastAccessedSharedState = string.Empty;
this.LastAccessedSharedStateComparer = null;
this.IsSourceUncontrolled = false;
this.IsDependencyUncontrolled = false;

5
Source/Core/Runtime/Operations/OperationStatus.cs
Просмотреть файл

@ -38,11 +38,6 @@ namespace Microsoft.Coyote.Runtime
/// </summary>
PausedOnReceive,
/// <summary>
/// The operation is suppressed until it is resumed.
/// </summary>
Suppressed,
/// <summary>
/// The operation is completed.
/// </summary>

9
Source/Core/Runtime/Scheduling/OperationScheduler.cs
Просмотреть файл

@ -98,9 +98,14 @@ namespace Microsoft.Coyote.Runtime
this.Portfolio = new LinkedList<Strategy>();
this.Reducers = new List<IScheduleReducer>();
if (configuration.IsSharedStateReductionEnabled)
if (configuration.IsExecutionTraceCycleReductionEnabled)
{
this.Reducers.Add(new SharedStateReducer());
this.Reducers.Add(new TraceCycleReducer());
}
if (configuration.IsPartialOrderSamplingEnabled)
{
this.Reducers.Add(new PartialOrderReducer());
}
this.IsReplaying = this.SchedulingPolicy is SchedulingPolicy.Interleaving && prefixTrace.Length > 0;

38
Source/Core/Runtime/Scheduling/Reducers/PartialOrderReducer.cs Normal file
Просмотреть файл

@ -0,0 +1,38 @@
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
using System.Collections.Generic;
using System.Linq;
namespace Microsoft.Coyote.Runtime
{
/// <summary>
/// A reducer that prioritizes non-racy access scheduling decisions to try force
/// racy operations interleave.
/// </summary>
internal sealed class PartialOrderReducer : IScheduleReducer
{
/// <summary>
/// Initializes a new instance of the <see cref="PartialOrderReducer"/> class.
/// </summary>
internal PartialOrderReducer()
{
}
/// <inheritdoc/>
public IEnumerable<ControlledOperation> ReduceOperations(IEnumerable<ControlledOperation> ops, ControlledOperation current)
{
// Find all operations that are not invoking a 'READ' or 'WRITE' scheduling decision,
// and if there are any, then return them. This effectively helps racy scheduling
// decisions to happen as close to each other as possible, which helps to find bugs
// that are caused by the interleaving of these operations.
var noReadOrWriteSchedulingOps = ops.Where(op => !SchedulingPoint.IsReadOrWrite(op.LastSchedulingPoint));
if (noReadOrWriteSchedulingOps.Any())
{
return noReadOrWriteSchedulingOps.ToArray();
}
return ops;
}
}
}

23
Source/Core/Runtime/Scheduling/Reducers/SharedStateReducer.cs
Просмотреть файл

@ -34,17 +34,16 @@ namespace Microsoft.Coyote.Runtime
}
/// <inheritdoc/>
public IEnumerable<ControlledOperation> ReduceOperations(IEnumerable<ControlledOperation> ops,
ControlledOperation current)
public IEnumerable<ControlledOperation> ReduceOperations(IEnumerable<ControlledOperation> ops, ControlledOperation current)
{
// Find all operations that are not invoking a user-defined scheduling decision.
var noUserDefinedSchedulingOps = ops.Where(
op => !SchedulingPoint.IsUserDefined(op.LastSchedulingPoint));
if (noUserDefinedSchedulingOps.Any())
var noReadOrWriteSchedulingOps = ops.Where(
op => !SchedulingPoint.IsReadOrWrite(op.LastSchedulingPoint));
if (noReadOrWriteSchedulingOps.Any())
{
// One or more operations exist that are not invoking a user-defined
// scheduling decision, so return them.
return noUserDefinedSchedulingOps;
return noReadOrWriteSchedulingOps;
}
else
{
@ -60,13 +59,13 @@ namespace Microsoft.Coyote.Runtime
if (!ops.Any(op => op.LastSchedulingPoint is SchedulingPointType.Interleave ||
op.LastSchedulingPoint is SchedulingPointType.Yield))
{
// Find if there are any read-only accesses. Note that this is just an approximation
// based on current knowledge. An access that is considered read-only might not be
// considered anymore in later steps or iterations once the known 'READ' and 'WRITE'
// access sets have been updated.
// Find if there are any read/write-only accesses. Note that this is just an approximation based on
// current knowledge. An access that is considered read/write-only might not be considered anymore
// in later steps or iterations once the known 'READ' and 'WRITE' access sets have been updated.
var readOnlyAccessOps = readAccessOps.Where(op => !this.WriteAccesses.Any(
state => state.StartsWith(op.LastAccessedSharedState) ||
op.LastAccessedSharedState.StartsWith(state)));
state => op.LastAccessedSharedStateComparer?.Equals(op.LastAccessedSharedState, state) ??
op.LastAccessedSharedState == state));
if (readOnlyAccessOps.Any())
{
// Return all read-only access operations.

58
Source/Core/Runtime/Scheduling/Reducers/TraceCycleReducer.cs Normal file
Просмотреть файл

@ -0,0 +1,58 @@
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
using System.Collections.Generic;
using System.Linq;
namespace Microsoft.Coyote.Runtime
{
/// <summary>
/// A reducer that analyzes cycles in the execution trace to reduce the set of operations
/// to be scheduled at each scheduling step.
/// </summary>
internal sealed class TraceCycleReducer : IScheduleReducer
{
/// <summary>
/// Set of states that have been 'READ' accessed. States are removed from the set
/// when they are 'WRITE' accessed.
/// </summary>
private readonly HashSet<string> RepeatedReadAccesses;
/// <summary>
/// Initializes a new instance of the <see cref="TraceCycleReducer"/> class.
/// </summary>
internal TraceCycleReducer()
{
this.RepeatedReadAccesses = new HashSet<string>();
}
/// <inheritdoc/>
public IEnumerable<ControlledOperation> ReduceOperations(IEnumerable<ControlledOperation> ops, ControlledOperation current)
{
// Find all operations that perform 'WRITE' accesses.
var writeAccessOps = ops.Where(op => op.LastSchedulingPoint is SchedulingPointType.Write).ToArray();
// Filter out all 'READ' operations that are repeatedly 'READ' accessing shared state when there is a 'WRITE' access.
var filteredOps = ops.Where(op => op.LastSchedulingPoint is SchedulingPointType.Read &&
this.RepeatedReadAccesses.Any(state => op.LastAccessedSharedState == state) &&
writeAccessOps.Any(wop =>
wop.LastAccessedSharedStateComparer?.Equals(wop.LastAccessedSharedState, op.LastAccessedSharedState) ??
wop.LastAccessedSharedState == op.LastAccessedSharedState)).ToArray();
if (current.LastSchedulingPoint is SchedulingPointType.Read)
{
// The current operation is a 'READ' access, so add it to the set of repeated read accesses.
this.RepeatedReadAccesses.Add(current.LastAccessedSharedState);
}
else if (current.LastSchedulingPoint is SchedulingPointType.Write)
{
// The current operation is a 'WRITE' access, so remove it from the set of repeated read accesses.
this.RepeatedReadAccesses.RemoveWhere(state =>
current.LastAccessedSharedStateComparer?.Equals(current.LastAccessedSharedState, state) ??
current.LastAccessedSharedState == state);
}
return ops.Except(filteredOps);
}
}
}

98
Source/Core/Runtime/Scheduling/SchedulingPoint.cs
Просмотреть файл

@ -68,7 +68,7 @@ namespace Microsoft.Coyote.Runtime
/// <param name="comparer">
/// Checks if the read shared state is equal with another shared state that is being accessed concurrently.
/// </param>
public static void Read(string state, IEqualityComparer<string> comparer = default)
public static void Read(string state, IEqualityComparer<string> comparer = null)
{
var runtime = CoyoteRuntime.Current;
if (runtime.SchedulingPolicy != SchedulingPolicy.None &&
@ -76,7 +76,11 @@ namespace Microsoft.Coyote.Runtime
{
if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving)
{
current.LastAccessedSharedState = state;
current.LastAccessedSharedStateComparer = comparer;
runtime.ScheduleNextOperation(current, SchedulingPointType.Read, isSuppressible: false);
current.LastAccessedSharedState = string.Empty;
current.LastAccessedSharedStateComparer = null;
}
else if (runtime.SchedulingPolicy is SchedulingPolicy.Fuzzing)
{
@ -92,7 +96,7 @@ namespace Microsoft.Coyote.Runtime
/// <param name="comparer">
/// Checks if the written shared state is equal with another shared state that is being accessed concurrently.
/// </param>
public static void Write(string state, IEqualityComparer<string> comparer = default)
public static void Write(string state, IEqualityComparer<string> comparer = null)
{
var runtime = CoyoteRuntime.Current;
if (runtime.SchedulingPolicy != SchedulingPolicy.None &&
@ -100,7 +104,11 @@ namespace Microsoft.Coyote.Runtime
{
if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving)
{
current.LastAccessedSharedState = state;
current.LastAccessedSharedStateComparer = comparer;
runtime.ScheduleNextOperation(current, SchedulingPointType.Write, isSuppressible: false);
current.LastAccessedSharedState = string.Empty;
current.LastAccessedSharedStateComparer = null;
}
else if (runtime.SchedulingPolicy is SchedulingPolicy.Fuzzing)
{
@ -109,85 +117,6 @@ namespace Microsoft.Coyote.Runtime
}
}
/// <summary>
/// Waits for a signal to a resource with the specified name.
/// </summary>
[System.ComponentModel.EditorBrowsable(System.ComponentModel.EditorBrowsableState.Never)]
public static void Wait(string name)
{
var runtime = CoyoteRuntime.Current;
if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving &&
runtime.TryGetExecutingOperation(out ControlledOperation current))
{
using (runtime.EnterSynchronizedSection())
{
if (!runtime.SignalMap.TryGetValue(name, out var signal))
{
runtime.SignalMap.Add(name, 1);
}
runtime.SignalMap[name]--;
if (runtime.SignalMap[name] is 0)
{
runtime.LogWriter.LogDebug("[coyote::debug] Operation '{0}' is waiting a signal for '{1}'.",
current.Name, name);
runtime.SignalMap[name] = 1;
current.Status = OperationStatus.Suppressed;
runtime.OperationSignalAwaiters.Add(current.Id, name);
runtime.ScheduleNextOperation(current, SchedulingPointType.Default, isSuppressible: false);
}
}
}
}
/// <summary>
/// Waits asynchronously for a signal to a resource with the specified name.
/// </summary>
[System.ComponentModel.EditorBrowsable(System.ComponentModel.EditorBrowsableState.Never)]
public static SignalAwaitable WaitAsync(string name)
{
var runtime = CoyoteRuntime.Current;
if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving &&
runtime.TryGetExecutingOperation(out ControlledOperation current))
{
return new SignalAwaitable(runtime, current, name);
}
return new SignalAwaitable(null, null, name);
}
/// <summary>
/// Signals a resource with the specified name.
/// </summary>
[System.ComponentModel.EditorBrowsable(System.ComponentModel.EditorBrowsableState.Never)]
public static void Signal(string name)
{
var runtime = CoyoteRuntime.Current;
if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving &&
runtime.TryGetExecutingOperation(out ControlledOperation current))
{
using (runtime.EnterSynchronizedSection())
{
foreach (var kvp in runtime.OperationSignalAwaiters.Where(kvp => kvp.Value == name).ToList())
{
var op = runtime.GetOperationWithId(kvp.Key);
runtime.LogWriter.LogDebug("[coyote::debug] Operation '{0}' is signaled for '{1}'.",
op.Name, name);
op.Status = OperationStatus.Enabled;
runtime.OperationSignalAwaiters.Remove(kvp.Key);
}
if (!runtime.SignalMap.TryGetValue(name, out var signal))
{
runtime.SignalMap.Add(name, 0);
}
runtime.SignalMap[name]++;
runtime.ScheduleNextOperation(current, SchedulingPointType.Default, isSuppressible: false);
}
}
}
/// <summary>
/// Suppresses interleavings until <see cref="Resume"/> is invoked.
/// </summary>
@ -249,5 +178,12 @@ namespace Microsoft.Coyote.Runtime
type is SchedulingPointType.Yield ||
type is SchedulingPointType.Read ||
type is SchedulingPointType.Write;
/// <summary>
/// Returns true if the specified scheduling point is a 'READ' or 'WRITE' operation.
/// </summary>
internal static bool IsReadOrWrite(SchedulingPointType type) =>
type is SchedulingPointType.Read ||
type is SchedulingPointType.Write;
}
}

10
Source/Core/Testing/Interleaving/PrioritizationStrategy.cs
Просмотреть файл

@ -99,14 +99,8 @@ namespace Microsoft.Coyote.Testing.Interleaving
if (ops.Select(op => op.Group).Distinct().Skip(1).Any())
{
// Change the priority of the highest priority operation group.
// If the shared-state reduction is enabled, check if there is at least
// one 'WRITE' operation, before trying to change the priority.
if (!this.Configuration.IsSharedStateReductionEnabled ||
ops.Any(op => op.LastSchedulingPoint is SchedulingPointType.Write))
{
this.PrioritizeNextOperationGroup(ops);
this.NumPriorityChangePoints++;
}
this.PrioritizeNextOperationGroup(ops);
this.NumPriorityChangePoints++;
// Get the operations that belong to the highest priority group.
OperationGroup nextGroup = this.GetOperationGroupWithHighestPriority(ops);

2
Source/Test/SystematicTesting/TestingEngine.cs
Просмотреть файл

@ -585,7 +585,7 @@ namespace Microsoft.Coyote.SystematicTesting
}
/// <summary>
/// Gathers the exploration strategy statistics from the specified runtimne.
/// Gathers the exploration strategy statistics from the specified runtime.
/// </summary>
private void GatherTestingStatistics(CoyoteRuntime runtime)
{

31
Tools/Coyote/Cli/CommandLineParser.cs
Просмотреть файл

@ -333,9 +333,16 @@ namespace Microsoft.Coyote.Cli
Arity = ArgumentArity.Zero
};
var reduceSharedStateOption = new Option<bool>(
name: "--reduce-shared-state",
description: "Enable shared state reduction based on 'READ' and 'WRITE' scheduling points.")
var reduceExecutionTraceCyclesOption = new Option<bool>(
name: "--reduce-execution-trace-cycles",
description: "Enable execution trace cycle detection and reduction heuristics.")
{
Arity = ArgumentArity.Zero
};
var samplePartialOrdersOption = new Option<bool>(
name: "--partial-order-sampling",
description: "Enable partial-order sampling based on 'READ' and 'WRITE' scheduling points.")
{
Arity = ArgumentArity.Zero
};
@ -474,8 +481,8 @@ namespace Microsoft.Coyote.Cli
};
var failOnMaxStepsOption = new Option<bool>(
name: "--fail-on-maxsteps",
description: "Reaching the specified max-steps is considered a bug.")
name: "--fail-on-max-steps",
description: "Reaching the specified max-steps is treated as a bug.")
{
Arity = ArgumentArity.Zero
};
@ -547,7 +554,8 @@ namespace Microsoft.Coyote.Cli
this.AddOption(command, serializeCoverageInfoOption);
this.AddOption(command, graphOption);
this.AddOption(command, xmlLogOption);
this.AddOption(command, reduceSharedStateOption);
this.AddOption(command, reduceExecutionTraceCyclesOption);
this.AddOption(command, samplePartialOrdersOption);
this.AddOption(command, seedOption);
this.AddOption(command, livenessTemperatureThresholdOption);
this.AddOption(command, timeoutDelayOption);
@ -996,8 +1004,11 @@ namespace Microsoft.Coyote.Cli
case "xml-trace":
this.Configuration.IsXmlLogEnabled = true;
break;
case "reduce-shared-state":
this.Configuration.IsSharedStateReductionEnabled = true;
case "reduce-execution-trace-cycles":
this.Configuration.IsExecutionTraceCycleReductionEnabled = true;
break;
case "partial-order-sampling":
this.Configuration.IsPartialOrderSamplingEnabled = true;
break;
case "seed":
this.Configuration.RandomGeneratorSeed = (uint)result.GetValueOrDefault<int>();
@ -1059,8 +1070,8 @@ namespace Microsoft.Coyote.Cli
case "log-uncontrolled-invocation-stack-traces":
this.Configuration.WithUncontrolledInvocationStackTraceLoggingEnabled();
break;
case "fail-on-maxsteps":
this.Configuration.ConsiderDepthBoundHitAsBug = true;
case "fail-on-max-steps":
this.Configuration.FailOnMaxStepsBound = true;
break;
case "explore":
this.Configuration.RunTestIterationsToCompletion = true;