Test your AI Agents with the all-new Agent to Agent Testing Platform.Learn More

How to use Dispose method of Microsoft.Coyote.Runtime.ControlledOperation class

Best Coyote code snippet using Microsoft.Coyote.Runtime.ControlledOperation.Dispose

CoyoteRuntime.cs

Source:CoyoteRuntime.cs

...639                            try640                            {641                                pendingOp.Value.Wait();642                            }643                            catch (ObjectDisposedException)644                            {645                                // The handler was disposed, so we can ignore this exception.646                            }647                        }648                        IO.Debug.WriteLine("[coyote::debug] Waking up thread '{0}'.", Thread.CurrentThread.ManagedThreadId);649                    }650                    pendingOp.Value.Dispose();651                    this.PendingStartOperationMap.Remove(pendingOp.Key);652                }653            }654        }655        /// <summary>656        /// Pauses the execution of the specified operation.657        /// </summary>658        /// <remarks>659        /// It is assumed that this method is invoked by the same thread executing the operation660        /// and that it runs in the scope of a <see cref="SynchronizedSection"/>.661        /// </remarks>662        private void PauseOperation(ControlledOperation op)663        {664            // Only pause the operation if it is not already completed and it is currently executing on this thread.665            if (op.Status != OperationStatus.Completed && op == ExecutingOperation.Value)666            {667                // Do not allow the operation to wake up, unless its currently scheduled and enabled or the runtime stopped running.668                while (!(op == this.ScheduledOperation && op.Status is OperationStatus.Enabled) && this.ExecutionStatus is ExecutionStatus.Running)669                {670                    IO.Debug.WriteLine("[coyote::debug] Sleeping operation '{0}' of group '{1}' on thread '{2}'.",671                        op.Name, op.Group, Thread.CurrentThread.ManagedThreadId);672                    using (SynchronizedSection.Exit(this.RuntimeLock))673                    {674                        op.WaitSignal();675                    }676                    IO.Debug.WriteLine("[coyote::debug] Waking up operation '{0}' of group '{1}' on thread '{2}'.",677                        op.Name, op.Group, Thread.CurrentThread.ManagedThreadId);678                }679            }680        }681        /// <summary>682        /// Pauses the currently executing operation until the specified condition gets resolved.683        /// </summary>684        internal void PauseOperationUntil(ControlledOperation current, Func<bool> condition, bool isConditionControlled = true, string debugMsg = null)685        {686            using (SynchronizedSection.Enter(this.RuntimeLock))687            {688                if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)689                {690                    // Only proceed if there is an operation executing on the current thread and691                    // the condition is not already resolved.692                    current ??= this.GetExecutingOperation();693                    while (current != null && !condition() && this.ExecutionStatus is ExecutionStatus.Running)694                    {695                        IO.Debug.WriteLine("[coyote::debug] Operation '{0}' of group '{1}' is waiting for {2} on thread '{3}'.",696                            current.Name, current.Group, debugMsg ?? "condition to get resolved", Thread.CurrentThread.ManagedThreadId);697                        // TODO: can we identify when the dependency is uncontrolled?698                        current.PauseWithDependency(condition, isConditionControlled);699                        this.ScheduleNextOperation(current, SchedulingPointType.Pause);700                    }701                }702            }703        }704        /// <summary>705        /// Asynchronously pauses the currently executing operation until the specified condition gets resolved.706        /// </summary>707        internal PausedOperationAwaitable PauseOperationUntilAsync(Func<bool> condition, bool resumeAsynchronously)708        {709            using (SynchronizedSection.Enter(this.RuntimeLock))710            {711                if (this.SchedulingPolicy is SchedulingPolicy.Interleaving &&712                    this.TryGetExecutingOperation(out ControlledOperation current))713                {714                    return new PausedOperationAwaitable(this, current, condition, resumeAsynchronously);715                }716            }717            return new PausedOperationAwaitable(this, null, condition, resumeAsynchronously);718        }719        /// <summary>720        /// Schedules the next enabled operation, which can include the currently executing operation.721        /// </summary>722        /// <param name="current">The currently executing operation, if there is one.</param>723        /// <param name="type">The type of the scheduling point.</param>724        /// <param name="isSuppressible">True if the interleaving can be suppressed, else false.</param>725        /// <param name="isYielding">True if the current operation is yielding, else false.</param>726        /// <remarks>727        /// An enabled operation is one that is not paused nor completed.728        /// </remarks>729        internal void ScheduleNextOperation(ControlledOperation current, SchedulingPointType type, bool isSuppressible = true, bool isYielding = false)730        {731            using (SynchronizedSection.Enter(this.RuntimeLock))732            {733                // Wait for all recently created operations to start executing.734                this.WaitOperationsStart();735                if (this.ExecutionStatus != ExecutionStatus.Running ||736                    this.SchedulingPolicy != SchedulingPolicy.Interleaving)737                {738                    // Cannot schedule the next operation if the scheduler is not attached,739                    // or if the scheduling policy is not systematic.740                    return;741                }742                // Check if the currently executing thread is uncontrolled.743                bool isThreadUncontrolled = false;744                if (current is null && !this.IsThreadControlled(Thread.CurrentThread))745                {746                    if (this.LastPostponedSchedulingPoint is SchedulingPointType.Pause ||747                        this.LastPostponedSchedulingPoint is SchedulingPointType.Complete)748                    {749                        // A scheduling point was postponed due to a potential deadlock, which has750                        // now been resolved, so resume it on this uncontrolled thread.751                        current = this.ScheduledOperation;752                        type = this.LastPostponedSchedulingPoint.Value;753                        IO.Debug.WriteLine("[coyote::debug] Resuming scheduling point '{0}' of operation '{1}' in uncontrolled thread '{2}'.",754                            type, current, Thread.CurrentThread.ManagedThreadId);755                    }756                    else if (type is SchedulingPointType.Create || type is SchedulingPointType.ContinueWith)757                    {758                        // This is a scheduling point that was invoked because a new operation was759                        // created by an uncontrolled thread, so postpone the scheduling point and760                        // resume it on the next available controlled thread.761                        IO.Debug.WriteLine("[coyote::debug] Postponing scheduling point '{0}' in uncontrolled thread '{1}'.",762                            type, Thread.CurrentThread.ManagedThreadId);763                        this.LastPostponedSchedulingPoint = type;764                        return;765                    }766                    isThreadUncontrolled = true;767                }768                // If the current operation was provided as argument to this method, or it is null, then this769                // is a controlled thread, so get the currently executing operation to proceed with scheduling.770                current ??= this.GetExecutingOperation();771                if (current is null)772                {773                    // Cannot proceed without having access to the currently executing operation.774                    return;775                }776                if (current != this.ScheduledOperation)777                {778                    // The currently executing operation is not scheduled, so send it to sleep.779                    this.PauseOperation(current);780                    return;781                }782                if (this.IsSchedulerSuppressed && this.LastPostponedSchedulingPoint is null &&783                    isSuppressible && current.Status is OperationStatus.Enabled)784                {785                    // Suppress the scheduling point.786                    IO.Debug.WriteLine("[coyote::debug] Suppressing scheduling point in operation '{0}'.", current.Name);787                    return;788                }789                this.Assert(!this.IsSpecificationInvoked, "Executing a specification monitor must be atomic.");790                // Checks if the scheduling steps bound has been reached.791                this.CheckIfSchedulingStepsBoundIsReached();792                // Update metadata related to this scheduling point.793                current.LastSchedulingPoint = type;794                this.LastPostponedSchedulingPoint = null;795                if (this.Configuration.IsProgramStateHashingEnabled)796                {797                    // Update the current operation with the hashed program state.798                    current.LastHashedProgramState = this.GetHashedProgramState();799                }800                // Try to enable any operations with resolved dependencies before asking the801                // scheduler to choose the next one to schedule.802                IEnumerable<ControlledOperation> ops = this.OperationMap.Values;803                if (!this.TryEnableOperationsWithResolvedDependencies(current))804                {805                    if (this.IsUncontrolledConcurrencyDetected &&806                        this.Configuration.IsPartiallyControlledConcurrencyAllowed)807                    {808                        // TODO: optimize and make this more fine-grained.809                        // If uncontrolled concurrency is detected, then do not check for deadlocks directly,810                        // but instead leave it to the background deadlock detection timer and postpone the811                        // scheduling point, which might get resolved from an uncontrolled thread.812                        IO.Debug.WriteLine("[coyote::debug] Postponing scheduling point '{0}' of operation '{1}' due to potential deadlock.",813                            type, current);814                        this.LastPostponedSchedulingPoint = type;815                        this.PauseOperation(current);816                        return;817                    }818                    // Check if the execution has deadlocked.819                    this.CheckIfExecutionHasDeadlocked(ops);820                }821                if (this.Configuration.IsLivenessCheckingEnabled && this.Scheduler.IsScheduleFair)822                {823                    // Check if the liveness threshold has been reached if scheduling is fair.824                    this.CheckLivenessThresholdExceeded();825                }826                if (!this.Scheduler.GetNextOperation(ops, current, isYielding, out ControlledOperation next))827                {828                    // The scheduler hit the scheduling steps bound.829                    this.Detach(ExecutionStatus.BoundReached);830                }831                IO.Debug.WriteLine("[coyote::debug] Scheduling operation '{0}' of group '{1}'.", next.Name, next.Group);832                if (current != next)833                {834                    // Pause the currently scheduled operation, and enable the next one.835                    this.ScheduledOperation = next;836                    next.Signal();837                    this.PauseOperation(current);838                }839                else if (isThreadUncontrolled)840                {841                    // If the current operation is the next operation to schedule, and the current thread842                    // is uncontrolled, then we need to signal the current operation to resume execution.843                    next.Signal();844                }845            }846        }847        /// <summary>848        /// Delays the currently executing operation for a non-deterministically chosen amount of time.849        /// </summary>850        /// <remarks>851        /// The delay is chosen non-deterministically by an underlying fuzzing strategy.852        /// If a delay of 0 is chosen, then the operation is not delayed.853        /// </remarks>854        internal void DelayOperation(ControlledOperation current)855        {856            using (SynchronizedSection.Enter(this.RuntimeLock))857            {858                if (this.ExecutionStatus != ExecutionStatus.Running)859                {860                    throw new ThreadInterruptedException();861                }862                if (current != null || this.TryGetExecutingOperation(out current))863                {864                    // Choose the next delay to inject. The value is in milliseconds.865                    int delay = this.GetNondeterministicDelay(current, (int)this.Configuration.MaxFuzzingDelay);866                    IO.Debug.WriteLine("[coyote::debug] Delaying operation '{0}' on thread '{1}' by {2}ms.",867                        current.Name, Thread.CurrentThread.ManagedThreadId, delay);868                    // Only sleep the executing operation if a non-zero delay was chosen.869                    if (delay > 0)870                    {871                        var previousStatus = current.Status;872                        current.Status = OperationStatus.PausedOnDelay;873                        using (SynchronizedSection.Exit(this.RuntimeLock))874                        {875                            Thread.SpinWait(delay);876                        }877                        current.Status = previousStatus;878                    }879                }880            }881        }882        /// <summary>883        /// Completes the specified operation.884        /// </summary>885        internal void CompleteOperation(ControlledOperation op)886        {887            op.ExecuteContinuations();888            using (SynchronizedSection.Enter(this.RuntimeLock))889            {890                IO.Debug.WriteLine("[coyote::debug] Completed operation '{0}' of group '{1}' on thread '{2}'.",891                    op.Name, op.Group, Thread.CurrentThread.ManagedThreadId);892                op.Status = OperationStatus.Completed;893            }894        }895        /// <summary>896        /// Tries to reset the specified controlled operation so that it can start executing again.897        /// This is only allowed if the operation is already completed.898        /// </summary>899        /// <param name="op">The operation to reset.</param>900        internal bool TryResetOperation(ControlledOperation op)901        {902            using (SynchronizedSection.Enter(this.RuntimeLock))903            {904                if (op.Status is OperationStatus.Completed)905                {906                    IO.Debug.WriteLine("[coyote::debug] Resetting operation '{0}' of group '{1}' from thread '{2}'.",907                        op.Name, op.Group, Thread.CurrentThread.ManagedThreadId);908                    op.Status = OperationStatus.None;909                    if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)910                    {911                        // Assign an event handler so that the next scheduling decision cannot be912                        // made until this operation starts executing to avoid race conditions.913                        this.PendingStartOperationMap.Add(op, new ManualResetEventSlim(false));914                    }915                    return true;916                }917            }918            return false;919        }920        /// <summary>921        /// Suppresses scheduling points until <see cref="ResumeScheduling"/> is invoked,922        /// unless a scheduling point must occur naturally.923        /// </summary>924        internal void SuppressScheduling()925        {926            using (SynchronizedSection.Enter(this.RuntimeLock))927            {928                IO.Debug.WriteLine("[coyote::debug] Suppressing scheduling of enabled operations in runtime '{0}'.", this.Id);929                this.IsSchedulerSuppressed = true;930            }931        }932        /// <summary>933        /// Resumes scheduling points that were suppressed by invoking <see cref="SuppressScheduling"/>.934        /// </summary>935        internal void ResumeScheduling()936        {937            using (SynchronizedSection.Enter(this.RuntimeLock))938            {939                IO.Debug.WriteLine("[coyote::debug] Resuming scheduling of enabled operations in runtime '{0}'.", this.Id);940                this.IsSchedulerSuppressed = false;941            }942        }943        /// <summary>944        /// Sets a checkpoint in the currently explored execution trace, that allows replaying all945        /// scheduling decisions until the checkpoint in subsequent iterations.946        /// </summary>947        internal void CheckpointExecutionTrace()948        {949            using (SynchronizedSection.Enter(this.RuntimeLock))950            {951                ExecutionTrace trace = this.Scheduler.CheckpointExecutionTrace();952                IO.Debug.WriteLine("[coyote::debug] Set checkpoint in current execution path with length '{0}' in runtime '{1}'.",953                    trace.Length, this.Id);954            }955        }956        /// <inheritdoc/>957        public bool RandomBoolean() => this.GetNextNondeterministicBooleanChoice(null, null);958        /// <summary>959        /// Returns the next nondeterministic boolean choice.960        /// </summary>961        internal bool GetNextNondeterministicBooleanChoice(string callerName, string callerType)962        {963            using (SynchronizedSection.Enter(this.RuntimeLock))964            {965                bool result;966                if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)967                {968                    // Checks if the current operation is controlled by the runtime.969                    this.GetExecutingOperation();970                    // Checks if the scheduling steps bound has been reached.971                    this.CheckIfSchedulingStepsBoundIsReached();972                    if (this.SchedulingPolicy is SchedulingPolicy.Interleaving &&973                        this.Configuration.IsLivenessCheckingEnabled && this.Scheduler.IsScheduleFair)974                    {975                        // Check if the liveness threshold has been reached if scheduling is fair.976                        this.CheckLivenessThresholdExceeded();977                    }978                    if (this.Configuration.IsProgramStateHashingEnabled)979                    {980                        // Update the current operation with the hashed program state.981                        this.ScheduledOperation.LastHashedProgramState = this.GetHashedProgramState();982                    }983                    if (!this.Scheduler.GetNextBoolean(this.ScheduledOperation, out result))984                    {985                        this.Detach(ExecutionStatus.BoundReached);986                    }987                }988                else989                {990                    result = this.ValueGenerator.Next(2) is 0 ? true : false;991                }992                this.LogWriter.LogRandom(result, callerName, callerType);993                return result;994            }995        }996        /// <inheritdoc/>997        public int RandomInteger(int maxValue) => this.GetNextNondeterministicIntegerChoice(maxValue, null, null);998        /// <summary>999        /// Returns the next nondeterministic integer choice.1000        /// </summary>1001        internal int GetNextNondeterministicIntegerChoice(int maxValue, string callerName, string callerType)1002        {1003            using (SynchronizedSection.Enter(this.RuntimeLock))1004            {1005                int result;1006                if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)1007                {1008                    // Checks if the current operation is controlled by the runtime.1009                    this.GetExecutingOperation();1010                    // Checks if the scheduling steps bound has been reached.1011                    this.CheckIfSchedulingStepsBoundIsReached();1012                    if (this.SchedulingPolicy is SchedulingPolicy.Interleaving &&1013                        this.Configuration.IsLivenessCheckingEnabled && this.Scheduler.IsScheduleFair)1014                    {1015                        // Check if the liveness threshold has been reached if scheduling is fair.1016                        this.CheckLivenessThresholdExceeded();1017                    }1018                    if (this.Configuration.IsProgramStateHashingEnabled)1019                    {1020                        // Update the current operation with the hashed program state.1021                        this.ScheduledOperation.LastHashedProgramState = this.GetHashedProgramState();1022                    }1023                    if (!this.Scheduler.GetNextInteger(this.ScheduledOperation, maxValue, out result))1024                    {1025                        this.Detach(ExecutionStatus.BoundReached);1026                    }1027                }1028                else1029                {1030                    result = this.ValueGenerator.Next(maxValue);1031                }1032                this.LogWriter.LogRandom(result, callerName, callerType);1033                return result;1034            }1035        }1036        /// <summary>1037        /// Returns a controlled nondeterministic delay for the specified operation.1038        /// </summary>1039        private int GetNondeterministicDelay(ControlledOperation op, int maxDelay)1040        {1041            using (SynchronizedSection.Enter(this.RuntimeLock))1042            {1043                // Checks if the scheduling steps bound has been reached.1044                this.CheckIfSchedulingStepsBoundIsReached();1045                // Choose the next delay to inject.1046                if (!this.Scheduler.GetNextDelay(this.OperationMap.Values, op, maxDelay, out int next))1047                {1048                    this.Detach(ExecutionStatus.BoundReached);1049                }1050                return next;1051            }1052        }1053        /// <summary>1054        /// Tries to enable any operations that have their dependencies resolved. It returns1055        /// true if there is at least one operation enabled, else false.1056        /// </summary>1057        /// <remarks>1058        /// It is assumed that this method runs in the scope of a <see cref="SynchronizedSection"/>.1059        /// </remarks>1060        private bool TryEnableOperationsWithResolvedDependencies(ControlledOperation current)1061        {1062            IO.Debug.WriteLine("[coyote::debug] Trying to enable any operation with resolved dependencies in runtime '{0}'.", this.Id);1063            int attempt = 0;1064            int delay = (int)this.Configuration.UncontrolledConcurrencyResolutionDelay;1065            uint maxAttempts = this.Configuration.UncontrolledConcurrencyResolutionAttempts;1066            uint enabledOpsCount = 0;1067            while (true)1068            {1069                // Cache the count of enabled operations from the previous attempt.1070                uint previousEnabledOpsCount = enabledOpsCount;1071                enabledOpsCount = 0;1072                uint statusChanges = 0;1073                bool isRootDependencyUnresolved = false;1074                bool isAnyDependencyUnresolved = false;1075                foreach (var op in this.OperationMap.Values)1076                {1077                    var previousStatus = op.Status;1078                    if (op.IsPaused)1079                    {1080                        this.TryEnableOperation(op);1081                        if (previousStatus == op.Status)1082                        {1083                            IO.Debug.WriteLine("[coyote::debug] Operation '{0}' of group '{1}' has status '{2}'.",1084                                op.Name, op.Group, op.Status);1085                            if (op.IsPaused && op.IsDependencyUncontrolled)1086                            {1087                                if (op.IsRoot)1088                                {1089                                    isRootDependencyUnresolved = true;1090                                }1091                                else1092                                {1093                                    isAnyDependencyUnresolved = true;1094                                }1095                            }1096                        }1097                        else1098                        {1099                            IO.Debug.WriteLine("[coyote::debug] Operation '{0}' of group '{1}' changed status from '{2}' to '{3}'.",1100                                op.Name, op.Group, previousStatus, op.Status);1101                            statusChanges++;1102                        }1103                    }1104                    if (op.Status is OperationStatus.Enabled)1105                    {1106                        enabledOpsCount++;1107                    }1108                }1109                // Heuristics for handling a partially controlled execution.1110                if (this.IsUncontrolledConcurrencyDetected &&1111                    this.Configuration.IsPartiallyControlledConcurrencyAllowed)1112                {1113                    // Compute the delta of enabled operations from the previous attempt.1114                    uint enabledOpsDelta = attempt is 0 ? 0 : enabledOpsCount - previousEnabledOpsCount;1115                    // This value is true if the current operation just completed and has uncontrolled source.1116                    bool isSourceUnresolved = current.Status is OperationStatus.Completed && current.IsSourceUncontrolled;1117                    // We consider the concurrency to be unresolved if there were no new enabled operations1118                    // or status changes in this attempt, and one of the following cases holds:1119                    // - If there are no enabled operations, then the concurrency is unresolved if1120                    //   the current operation was just completed and has uncontrolled source, or1121                    //   if there are any unresolved dependencies.1122                    // - If there are enabled operations, then the concurrency is unresolved if1123                    //   there are any (non-root) unresolved dependencies.1124                    bool isNoEnabledOpsCaseResolved = enabledOpsCount is 0 &&1125                        (isSourceUnresolved || isAnyDependencyUnresolved || isRootDependencyUnresolved);1126                    bool isSomeEnabledOpsCaseResolved = enabledOpsCount > 0 && isAnyDependencyUnresolved;1127                    bool isConcurrencyUnresolved = enabledOpsDelta is 0 && statusChanges is 0 &&1128                        (isNoEnabledOpsCaseResolved || isSomeEnabledOpsCaseResolved);1129                    // Retry if there is unresolved concurrency and attempts left.1130                    if (++attempt < maxAttempts && isConcurrencyUnresolved)1131                    {1132                        // Implement a simple retry logic to try resolve uncontrolled concurrency.1133                        IO.Debug.WriteLine("[coyote::debug] Pausing controlled thread '{0}' to try resolve uncontrolled concurrency.",1134                            Thread.CurrentThread.ManagedThreadId);1135                        using (SynchronizedSection.Exit(this.RuntimeLock))1136                        {1137                            Thread.SpinWait(delay);1138                        }1139                        continue;1140                    }1141                }1142                break;1143            }1144            IO.Debug.WriteLine("[coyote::debug] There are {0} enabled operations in runtime '{1}'.", enabledOpsCount, this.Id);1145            this.MaxConcurrencyDegree = Math.Max(this.MaxConcurrencyDegree, enabledOpsCount);1146            return enabledOpsCount > 0;1147        }1148        /// <summary>1149        /// Tries to enable the specified operation, if its dependencies have been resolved.1150        /// </summary>1151        /// <remarks>1152        /// It is assumed that this method runs in the scope of a <see cref="SynchronizedSection"/>.1153        /// </remarks>1154        private bool TryEnableOperation(ControlledOperation op)1155        {1156            if (op.Status is OperationStatus.PausedOnDelay && op is DelayOperation delayedOp)1157            {1158                if (delayedOp.Delay > 0)1159                {1160                    delayedOp.Delay--;1161                }1162                // The operation is delayed, so it is enabled either if the delay completes1163                // or if no other operation is enabled.1164                if (delayedOp.Delay is 0 ||1165                    !this.OperationMap.Any(kvp => kvp.Value.Status is OperationStatus.Enabled))1166                {1167                    delayedOp.Delay = 0;1168                    delayedOp.Status = OperationStatus.Enabled;1169                    return true;1170                }1171                return false;1172            }1173            // If the operation is paused, then check if its dependency has been resolved.1174            return op.TryEnable();1175        }1176        /// <summary>1177        /// Pauses the scheduled controlled operation until either the uncontrolled task completes,1178        /// it tries to invoke an uncontrolled scheduling point, or the timeout expires.1179        /// </summary>1180        /// <remarks>1181        /// It is assumed that this method runs in the scope of a <see cref="SynchronizedSection"/>.1182        /// </remarks>1183        private void TryPauseAndResolveUncontrolledTask(Task task)1184        {1185            if (this.IsThreadControlled(Thread.CurrentThread))1186            {1187                // A scheduling point from an uncontrolled thread has not been postponed yet, so pause the execution1188                // of the current operation to try give time to the uncontrolled concurrency to be resolved.1189                if (this.LastPostponedSchedulingPoint is null)1190                {1191                    int attempt = 0;1192                    int delay = (int)this.Configuration.UncontrolledConcurrencyResolutionDelay;1193                    uint maxAttempts = this.Configuration.UncontrolledConcurrencyResolutionAttempts;1194                    while (attempt++ < maxAttempts && !task.IsCompleted)1195                    {1196                        IO.Debug.WriteLine("[coyote::debug] Pausing controlled thread '{0}' to try resolve uncontrolled concurrency.",1197                            Thread.CurrentThread.ManagedThreadId);1198                        using (SynchronizedSection.Exit(this.RuntimeLock))1199                        {1200                            Thread.SpinWait(delay);1201                        }1202                        if (this.LastPostponedSchedulingPoint.HasValue)1203                        {1204                            // A scheduling point from an uncontrolled thread has been postponed,1205                            // so stop trying to resolve the uncontrolled concurrency.1206                            break;1207                        }1208                    }1209                }1210                if (this.LastPostponedSchedulingPoint.HasValue)1211                {1212                    IO.Debug.WriteLine("[coyote::debug] Resuming controlled thread '{0}' with uncontrolled concurrency resolved.",1213                        Thread.CurrentThread.ManagedThreadId);1214                    this.ScheduleNextOperation(default, this.LastPostponedSchedulingPoint.Value, isSuppressible: false);1215                }1216            }1217        }1218        /// <summary>1219        /// Returns the currently executing <see cref="ControlledOperation"/>,1220        /// or null if no such operation is executing.1221        /// </summary>1222        internal ControlledOperation GetExecutingOperation()1223        {1224            using (SynchronizedSection.Enter(this.RuntimeLock))1225            {1226                var op = ExecutingOperation.Value;1227                if (op is null)1228                {1229                    this.NotifyUncontrolledCurrentThread();1230                }1231                return op;1232            }1233        }1234        /// <summary>1235        /// Returns the currently executing <see cref="ControlledOperation"/> of the1236        /// specified type, or null if no such operation is executing.1237        /// </summary>1238        internal TControlledOperation GetExecutingOperation<TControlledOperation>()1239            where TControlledOperation : ControlledOperation1240        {1241            using (SynchronizedSection.Enter(this.RuntimeLock))1242            {1243                var op = ExecutingOperation.Value;1244                if (op is null)1245                {1246                    this.NotifyUncontrolledCurrentThread();1247                }1248                return op is TControlledOperation expected ? expected : default;1249            }1250        }1251        /// <summary>1252        /// Tries to return the currently executing <see cref="ControlledOperation"/>,1253        /// or false if no such operation is executing.1254        /// </summary>1255        internal bool TryGetExecutingOperation(out ControlledOperation op)1256        {1257            op = this.GetExecutingOperation();1258            return op != null;1259        }1260        /// <summary>1261        /// Returns the <see cref="ControlledOperation"/> associated with the specified1262        /// operation id, or null if no such operation exists.1263        /// </summary>1264        internal ControlledOperation GetOperationWithId(ulong operationId)1265        {1266            using (SynchronizedSection.Enter(this.RuntimeLock))1267            {1268                this.OperationMap.TryGetValue(operationId, out ControlledOperation op);1269                return op;1270            }1271        }1272        /// <summary>1273        /// Returns the <see cref="ControlledOperation"/> of the specified type that is associated1274        /// with the specified operation id, or null if no such operation exists.1275        /// </summary>1276        internal TControlledOperation GetOperationWithId<TControlledOperation>(ulong operationId)1277            where TControlledOperation : ControlledOperation1278        {1279            using (SynchronizedSection.Enter(this.RuntimeLock))1280            {1281                if (this.OperationMap.TryGetValue(operationId, out ControlledOperation op) &&1282                    op is TControlledOperation expected)1283                {1284                    return expected;1285                }1286            }1287            return default;1288        }1289        /// <summary>1290        /// Returns all registered operations.1291        /// </summary>1292        /// <remarks>1293        /// This operation is thread safe because the systematic testing1294        /// runtime serializes the execution.1295        /// </remarks>1296        private IEnumerable<ControlledOperation> GetRegisteredOperations()1297        {1298            using (SynchronizedSection.Enter(this.RuntimeLock))1299            {1300                return this.OperationMap.Values;1301            }1302        }1303        /// <summary>1304        /// Returns the next available unique operation id.1305        /// </summary>1306        /// <returns>Value representing the next available unique operation id.</returns>1307        internal ulong GetNextOperationId() =>1308            // Atomically increments and safely wraps the value into an unsigned long.1309            (ulong)Interlocked.Increment(ref this.OperationIdCounter) - 1;1310        /// <summary>1311        /// Returns the current hashed state of the execution.1312        /// </summary>1313        /// <remarks>1314        /// The hash is updated in each execution step.1315        /// </remarks>1316        private int GetHashedProgramState()1317        {1318            unchecked1319            {1320                int hash = 19;1321                foreach (var operation in this.GetRegisteredOperations().OrderBy(op => op.Id))1322                {1323                    if (operation is ActorOperation actorOperation)1324                    {1325                        int operationHash = 31 + actorOperation.Actor.GetHashedState(this.SchedulingPolicy);1326                        operationHash = (operationHash * 31) + actorOperation.LastSchedulingPoint.GetHashCode();1327                        hash *= operationHash;1328                    }1329                    else1330                    {1331                        hash *= 31 + operation.LastSchedulingPoint.GetHashCode();1332                    }1333                }1334                foreach (var monitor in this.SpecificationMonitors)1335                {1336                    hash *= 31 + monitor.GetHashedState();1337                }1338                return hash;1339            }1340        }1341        /// <inheritdoc/>1342        public void RegisterMonitor<T>()1343            where T : Specifications.Monitor =>1344            this.TryCreateMonitor(typeof(T));1345        /// <summary>1346        /// Tries to create a new <see cref="Specifications.Monitor"/> of the specified <see cref="Type"/>.1347        /// </summary>1348        private bool TryCreateMonitor(Type type)1349        {1350            if (this.SchedulingPolicy != SchedulingPolicy.None ||1351                this.Configuration.IsMonitoringEnabledInInProduction)1352            {1353                using (SynchronizedSection.Enter(this.RuntimeLock))1354                {1355                    // Only one monitor per type is allowed.1356                    if (!this.SpecificationMonitors.Any(m => m.GetType() == type))1357                    {1358                        var monitor = (Specifications.Monitor)Activator.CreateInstance(type);1359                        monitor.Initialize(this.Configuration, this, this.LogWriter);1360                        monitor.InitializeStateInformation();1361                        this.SpecificationMonitors.Add(monitor);1362                        if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)1363                        {1364                            this.SuppressScheduling();1365                            this.IsSpecificationInvoked = true;1366                            monitor.GotoStartState();1367                            this.IsSpecificationInvoked = false;1368                            this.ResumeScheduling();1369                        }1370                        else1371                        {1372                            monitor.GotoStartState();1373                        }1374                        return true;1375                    }1376                }1377            }1378            return false;1379        }1380        /// <inheritdoc/>1381        public void Monitor<T>(Event e)1382            where T : Specifications.Monitor =>1383            this.InvokeMonitor(typeof(T), e, null, null, null);1384        /// <summary>1385        /// Invokes the specified <see cref="Specifications.Monitor"/> with the specified <see cref="Event"/>.1386        /// </summary>1387        internal void InvokeMonitor(Type type, Event e, string senderName, string senderType, string senderStateName)1388        {1389            if (this.SchedulingPolicy != SchedulingPolicy.None ||1390                this.Configuration.IsMonitoringEnabledInInProduction)1391            {1392                using (SynchronizedSection.Enter(this.RuntimeLock))1393                {1394                    Specifications.Monitor monitor = null;1395                    foreach (var m in this.SpecificationMonitors)1396                    {1397                        if (m.GetType() == type)1398                        {1399                            monitor = m;1400                            break;1401                        }1402                    }1403                    if (monitor != null)1404                    {1405                        this.Assert(e != null, "Cannot invoke monitor '{0}' with a null event.", type.FullName);1406                        if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)1407                        {1408                            this.SuppressScheduling();1409                            this.IsSpecificationInvoked = true;1410                            monitor.MonitorEvent(e, senderName, senderType, senderStateName);1411                            this.IsSpecificationInvoked = false;1412                            this.ResumeScheduling();1413                        }1414                        else1415                        {1416                            monitor.MonitorEvent(e, senderName, senderType, senderStateName);1417                        }1418                    }1419                }1420            }1421        }1422        /// <inheritdoc/>1423        public void Assert(bool predicate)1424        {1425            if (!predicate)1426            {1427                string msg = "Detected an assertion failure.";1428                if (this.SchedulingPolicy is SchedulingPolicy.None)1429                {1430                    throw new AssertionFailureException(msg);1431                }1432                this.NotifyAssertionFailure(msg);1433            }1434        }1435        /// <inheritdoc/>1436        public void Assert(bool predicate, string s, object arg0)1437        {1438            if (!predicate)1439            {1440                var msg = string.Format(CultureInfo.InvariantCulture, s, arg0?.ToString());1441                if (this.SchedulingPolicy is SchedulingPolicy.None)1442                {1443                    throw new AssertionFailureException(msg);1444                }1445                this.NotifyAssertionFailure(msg);1446            }1447        }1448        /// <inheritdoc/>1449        public void Assert(bool predicate, string s, object arg0, object arg1)1450        {1451            if (!predicate)1452            {1453                var msg = string.Format(CultureInfo.InvariantCulture, s, arg0?.ToString(), arg1?.ToString());1454                if (this.SchedulingPolicy is SchedulingPolicy.None)1455                {1456                    throw new AssertionFailureException(msg);1457                }1458                this.NotifyAssertionFailure(msg);1459            }1460        }1461        /// <inheritdoc/>1462        public void Assert(bool predicate, string s, object arg0, object arg1, object arg2)1463        {1464            if (!predicate)1465            {1466                var msg = string.Format(CultureInfo.InvariantCulture, s, arg0?.ToString(), arg1?.ToString(), arg2?.ToString());1467                if (this.SchedulingPolicy is SchedulingPolicy.None)1468                {1469                    throw new AssertionFailureException(msg);1470                }1471                this.NotifyAssertionFailure(msg);1472            }1473        }1474        /// <inheritdoc/>1475        public void Assert(bool predicate, string s, params object[] args)1476        {1477            if (!predicate)1478            {1479                var msg = string.Format(CultureInfo.InvariantCulture, s, args);1480                if (this.SchedulingPolicy is SchedulingPolicy.None)1481                {1482                    throw new AssertionFailureException(msg);1483                }1484                this.NotifyAssertionFailure(msg);1485            }1486        }1487        /// <summary>1488        /// Creates a liveness monitor that checks if the specified task eventually completes execution successfully.1489        /// </summary>1490        internal void MonitorTaskCompletion(Task task)1491        {1492            if (this.SchedulingPolicy is SchedulingPolicy.Interleaving &&1493                task.Status != TaskStatus.RanToCompletion)1494            {1495                var monitor = new TaskLivenessMonitor(task);1496                this.TaskLivenessMonitors.Add(monitor);1497            }1498        }1499        /// <summary>1500        /// Starts running a background monitor that checks for potential deadlocks.1501        /// </summary>1502        private void StartMonitoringDeadlocks() => Task.Factory.StartNew(this.CheckIfExecutionHasDeadlockedAsync,1503            this.CancellationSource.Token, TaskCreationOptions.LongRunning, TaskScheduler.Default);1504        /// <summary>1505        /// Returns true if the specified thread is controlled, else false.1506        /// </summary>1507        private bool IsThreadControlled(Thread thread)1508        {1509            string name = thread?.Name;1510            return name != null && this.ControlledThreads.ContainsKey(name);1511        }1512        /// <summary>1513        /// Returns true if the specified task is uncontrolled, else false.1514        /// </summary>1515        internal bool IsTaskUncontrolled(Task task) =>1516            task != null && !task.IsCompleted && !this.ControlledTasks.ContainsKey(task);1517        /// <summary>1518        /// Checks if the awaited task is uncontrolled.1519        /// </summary>1520        internal bool CheckIfAwaitedTaskIsUncontrolled(Task task)1521        {1522            if (this.IsTaskUncontrolled(task))1523            {1524                this.NotifyUncontrolledTaskWait(task);1525                return true;1526            }1527            return false;1528        }1529        /// <summary>1530        /// Checks if the task returned from the specified method is uncontrolled.1531        /// </summary>1532        internal bool CheckIfReturnedTaskIsUncontrolled(Task task, string methodName)1533        {1534            if (this.IsTaskUncontrolled(task))1535            {1536                this.NotifyUncontrolledTaskReturned(task, methodName);1537                return true;1538            }1539            return false;1540        }1541        /// <summary>1542        /// Checks if the execution has deadlocked. This happens when there are no more enabled operations,1543        /// but there is one or more paused operations that are waiting some resource to complete.1544        /// </summary>1545        private void CheckIfExecutionHasDeadlocked(IEnumerable<ControlledOperation> ops)1546        {1547            if (ops.Any(op => op.Status is OperationStatus.Enabled))1548            {1549                // There are still enabled operations, so the execution is not deadlocked.1550                return;1551            }1552            var pausedOperations = ops.Where(op => op.Status is OperationStatus.Paused).ToList();1553            var pausedOnResources = ops.Where(op => op.Status is OperationStatus.PausedOnResource).ToList();1554            var pausedOnReceiveOperations = ops.Where(op => op.Status is OperationStatus.PausedOnReceive).ToList();1555            var totalCount = pausedOperations.Count + pausedOnResources.Count + pausedOnReceiveOperations.Count;1556            if (totalCount is 0)1557            {1558                // There are no paused operations, so the execution is not deadlocked.1559                return;1560            }1561            // To simplify the error message, remove the root operation, unless it is the only one that is paused.1562            if (totalCount > 1)1563            {1564                pausedOperations.RemoveAll(op => op.IsRoot);1565                pausedOnResources.RemoveAll(op => op.IsRoot);1566                pausedOnReceiveOperations.RemoveAll(op => op.IsRoot);1567            }1568            StringBuilder msg;1569            if (this.IsUncontrolledConcurrencyDetected)1570            {1571                msg = new StringBuilder("Potential deadlock detected.");1572            }1573            else1574            {1575                msg = new StringBuilder("Deadlock detected.");1576            }1577            if (pausedOperations.Count > 0)1578            {1579                for (int idx = 0; idx < pausedOperations.Count; idx++)1580                {1581                    msg.Append(string.Format(CultureInfo.InvariantCulture, " {0}", pausedOperations[idx].Name));1582                    if (idx == pausedOperations.Count - 2)1583                    {1584                        msg.Append(" and");1585                    }1586                    else if (idx < pausedOperations.Count - 1)1587                    {1588                        msg.Append(',');1589                    }1590                }1591                msg.Append(pausedOperations.Count is 1 ? " is " : " are ");1592                msg.Append("paused on a dependency, but no other controlled operations are enabled.");1593            }1594            if (pausedOnResources.Count > 0)1595            {1596                for (int idx = 0; idx < pausedOnResources.Count; idx++)1597                {1598                    msg.Append(string.Format(CultureInfo.InvariantCulture, " {0}", pausedOnResources[idx].Name));1599                    if (idx == pausedOnResources.Count - 2)1600                    {1601                        msg.Append(" and");1602                    }1603                    else if (idx < pausedOnResources.Count - 1)1604                    {1605                        msg.Append(',');1606                    }1607                }1608                msg.Append(pausedOnResources.Count is 1 ? " is " : " are ");1609                msg.Append("waiting to acquire a resource that is already acquired, ");1610                msg.Append("but no other controlled operations are enabled.");1611            }1612            if (pausedOnReceiveOperations.Count > 0)1613            {1614                for (int idx = 0; idx < pausedOnReceiveOperations.Count; idx++)1615                {1616                    msg.Append(string.Format(CultureInfo.InvariantCulture, " {0}", pausedOnReceiveOperations[idx].Name));1617                    if (idx == pausedOnReceiveOperations.Count - 2)1618                    {1619                        msg.Append(" and");1620                    }1621                    else if (idx < pausedOnReceiveOperations.Count - 1)1622                    {1623                        msg.Append(',');1624                    }1625                }1626                msg.Append(pausedOnReceiveOperations.Count is 1 ? " is " : " are ");1627                msg.Append("waiting to receive an event, but no other controlled operations are enabled.");1628            }1629            if (this.IsUncontrolledConcurrencyDetected)1630            {1631                msg.Append(" Due to the presence of uncontrolled concurrency in the test, ");1632                msg.Append("Coyote cannot accurately determine if this is a real deadlock or not.");1633                if (!this.Configuration.ReportPotentialDeadlocksAsBugs)1634                {1635                    this.Logger.WriteLine($"[coyote::test] {msg}");1636                    this.Detach(ExecutionStatus.Deadlocked);1637                }1638                msg.Append(" If you believe that this is not a real deadlock, you can disable reporting ");1639                msg.Append("potential deadlocks as bugs by setting '--skip-potential-deadlocks' or ");1640                msg.Append("'Configuration.WithPotentialDeadlocksReportedAsBugs(false)'.");1641            }1642            this.NotifyAssertionFailure(msg.ToString());1643        }1644        /// <summary>1645        /// Periodically checks if the execution has deadlocked.1646        /// </summary>1647        private async Task CheckIfExecutionHasDeadlockedAsync()1648        {1649            var info = new SchedulingActivityInfo();1650            IO.Debug.WriteLine("[coyote::debug] Started periodic monitoring for potential deadlocks in runtime '{0}'.", this.Id);1651            while (true)1652            {1653                try1654                {1655                    await Task.Delay(TimeSpan.FromMilliseconds(this.Configuration.DeadlockTimeout), this.CancellationSource.Token);1656                    using (SynchronizedSection.Enter(this.RuntimeLock))1657                    {1658                        if (this.ExecutionStatus != ExecutionStatus.Running)1659                        {1660                            break;1661                        }1662                        if (info.OperationCount == this.OperationMap.Count &&1663                            info.StepCount == this.Scheduler.StepCount)1664                        {1665                            string msg = "Potential deadlock detected. The periodic deadlock detection monitor was used, " +1666                                "so Coyote cannot accurately determine if this is a real deadlock or not. If you believe " +1667                                "that this is not a real deadlock, you can try increase the deadlock detection timeout " +1668                                "by setting '--deadlock-timeout N' or 'Configuration.WithDeadlockTimeout(N)'.";1669                            if (this.Configuration.ReportPotentialDeadlocksAsBugs)1670                            {1671                                msg += " Alternatively, you can disable reporting potential deadlocks as bugs by setting " +1672                                "'--skip-potential-deadlocks' or 'Configuration.WithPotentialDeadlocksReportedAsBugs(false)'.";1673                                this.NotifyAssertionFailure(msg);1674                            }1675                            else1676                            {1677                                this.Logger.WriteLine($"[coyote::test] {msg}");1678                                this.Detach(ExecutionStatus.Deadlocked);1679                            }1680                        }1681                        else1682                        {1683                            // Passed check, so continue with the next timeout period.1684                            IO.Debug.WriteLine("[coyote::debug] Passed periodic check for potential deadlocks in runtime '{0}'.", this.Id);1685                            info.OperationCount = this.OperationMap.Count;1686                            info.StepCount = this.Scheduler.StepCount;1687                            if (this.LastPostponedSchedulingPoint is SchedulingPointType.Pause ||1688                                this.LastPostponedSchedulingPoint is SchedulingPointType.Complete)1689                            {1690                                // A scheduling point was postponed due to a potential deadlock, so try to check if it has been resolved.1691                                this.ScheduleNextOperation(default, this.LastPostponedSchedulingPoint.Value, isSuppressible: false);1692                            }1693                        }1694                    }1695                }1696                catch (TaskCanceledException)1697                {1698                    break;1699                }1700            }1701        }1702        /// <summary>1703        /// Checks for liveness errors.1704        /// </summary>1705#if !DEBUG1706        [DebuggerHidden]1707#endif1708        internal void CheckLivenessErrors()1709        {1710            foreach (var monitor in this.TaskLivenessMonitors)1711            {1712                if (!monitor.IsSatisfied)1713                {1714                    string msg = string.Format(CultureInfo.InvariantCulture,1715                        "Found liveness bug at the end of program execution.\nThe stack trace is:\n{0}",1716                        FormatSpecificationMonitorStackTrace(monitor.StackTrace));1717                    this.NotifyAssertionFailure(msg);1718                }1719            }1720            // Checks if there is a specification monitor stuck in a hot state.1721            foreach (var monitor in this.SpecificationMonitors)1722            {1723                if (monitor.IsInHotState(out string stateName))1724                {1725                    string msg = string.Format(CultureInfo.InvariantCulture,1726                        "{0} detected liveness bug in hot state '{1}' at the end of program execution.",1727                        monitor.GetType().FullName, stateName);1728                    this.NotifyAssertionFailure(msg);1729                }1730            }1731        }1732        /// <summary>1733        /// Checks if a liveness monitor exceeded its threshold and, if yes, it reports an error.1734        /// </summary>1735        internal void CheckLivenessThresholdExceeded()1736        {1737            foreach (var monitor in this.TaskLivenessMonitors)1738            {1739                if (monitor.IsLivenessThresholdExceeded(this.Configuration.LivenessTemperatureThreshold))1740                {1741                    string msg = string.Format(CultureInfo.InvariantCulture,1742                        "Found potential liveness bug at the end of program execution.\nThe stack trace is:\n{0}",1743                        FormatSpecificationMonitorStackTrace(monitor.StackTrace));1744                    this.NotifyAssertionFailure(msg);1745                }1746            }1747            foreach (var monitor in this.SpecificationMonitors)1748            {1749                if (monitor.IsLivenessThresholdExceeded(this.Configuration.LivenessTemperatureThreshold))1750                {1751                    string msg = $"{monitor.Name} detected potential liveness bug in hot state '{monitor.CurrentStateName}'.";1752                    this.NotifyAssertionFailure(msg);1753                }1754            }1755        }1756        /// <summary>1757        /// Checks if the scheduling steps bound has been reached. If yes,1758        /// it stops the scheduler and kills all enabled machines.1759        /// </summary>1760        private void CheckIfSchedulingStepsBoundIsReached()1761        {1762            if (this.Scheduler.IsMaxStepsReached)1763            {1764                string message = $"Scheduling steps bound of {this.Scheduler.StepCount} reached.";1765                if (this.Configuration.ConsiderDepthBoundHitAsBug)1766                {1767                    this.NotifyAssertionFailure(message);1768                }1769                else1770                {1771                    IO.Debug.WriteLine($"[coyote::debug] {message}");1772                    this.Detach(ExecutionStatus.BoundReached);1773                }1774            }1775        }1776        /// <summary>1777        /// Notify that an exception was not handled.1778        /// </summary>1779        internal void NotifyUnhandledException(Exception ex, string message)1780        {1781            using (SynchronizedSection.Enter(this.RuntimeLock))1782            {1783                if (this.ExecutionStatus != ExecutionStatus.Running)1784                {1785                    return;1786                }1787                if (this.UnhandledException is null)1788                {1789                    this.UnhandledException = ex;1790                }1791                this.NotifyAssertionFailure(message);1792            }1793        }1794        /// <summary>1795        /// Notify that an assertion has failed.1796        /// </summary>1797#if !DEBUG1798        [DebuggerHidden]1799#endif1800        internal void NotifyAssertionFailure(string text)1801        {1802            using (SynchronizedSection.Enter(this.RuntimeLock))1803            {1804                if (this.ExecutionStatus is ExecutionStatus.Running)1805                {1806                    this.BugReport = text;1807                    this.LogWriter.LogAssertionFailure($"[coyote::error] {text}");1808                    this.RaiseOnFailureEvent(new AssertionFailureException(text));1809                    if (this.Configuration.AttachDebugger)1810                    {1811                        Debugger.Break();1812                    }1813                    this.Detach(ExecutionStatus.BugFound);1814                }1815            }1816        }1817        /// <summary>1818        /// Notify that an uncontrolled invocation was detected.1819        /// </summary>1820        internal void NotifyUncontrolledInvocation(string methodName)1821        {1822            using (SynchronizedSection.Enter(this.RuntimeLock))1823            {1824                if (this.SchedulingPolicy != SchedulingPolicy.None)1825                {1826                    this.UncontrolledInvocations.Add(methodName);1827                }1828                if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)1829                {1830                    string message = $"Invoking '{methodName}' is not intercepted and controlled during " +1831                        "testing, so it can interfere with the ability to reproduce bug traces.";1832                    this.TryHandleUncontrolledConcurrency(message, methodName);1833                }1834            }1835        }1836        /// <summary>1837        /// Notify that the currently executing thread is uncontrolled.1838        /// </summary>1839        private void NotifyUncontrolledCurrentThread()1840        {1841            if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)1842            {1843                // TODO: figure out if there is a way to get more information about the creator of the1844                // uncontrolled thread to ease the user debugging experience.1845                string message = $"Executing thread '{Thread.CurrentThread.ManagedThreadId}' is not intercepted and " +1846                    "controlled during testing, so it can interfere with the ability to reproduce bug traces.";1847                this.TryHandleUncontrolledConcurrency(message);1848            }1849        }1850        /// <summary>1851        /// Notify that an uncontrolled task is being waited.1852        /// </summary>1853        private void NotifyUncontrolledTaskWait(Task task)1854        {1855            using (SynchronizedSection.Enter(this.RuntimeLock))1856            {1857                if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)1858                {1859                    // TODO: figure out if there is a way to get more information about the creator of the1860                    // uncontrolled task to ease the user debugging experience.1861                    string message = $"Waiting task '{task.Id}' that is not intercepted and controlled during " +1862                        "testing, so it can interfere with the ability to reproduce bug traces.";1863                    if (this.TryHandleUncontrolledConcurrency(message) &&1864                        this.UncontrolledTasks.Add(task))1865                    {1866                        this.TryPauseAndResolveUncontrolledTask(task);1867                    }1868                }1869            }1870        }1871        /// <summary>1872        /// Notify that an uncontrolled task was returned.1873        /// </summary>1874        private void NotifyUncontrolledTaskReturned(Task task, string methodName)1875        {1876            using (SynchronizedSection.Enter(this.RuntimeLock))1877            {1878                if (this.SchedulingPolicy != SchedulingPolicy.None)1879                {1880                    this.UncontrolledInvocations.Add(methodName);1881                }1882                if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)1883                {1884                    string message = $"Invoking '{methodName}' returned task '{task.Id}' that is not intercepted and " +1885                        "controlled during testing, so it can interfere with the ability to reproduce bug traces.";1886                    if (this.TryHandleUncontrolledConcurrency(message, methodName) &&1887                        this.UncontrolledTasks.Add(task))1888                    {1889                        this.TryPauseAndResolveUncontrolledTask(task);1890                    }1891                }1892            }1893        }1894        /// <summary>1895        /// Invoked when uncontrolled concurrency is detected. Based on the test configuration, it can try1896        /// handle the uncontrolled concurrency, else it terminates the current test iteration.1897        /// </summary>1898        private bool TryHandleUncontrolledConcurrency(string message, string methodName = default)1899        {1900            if (this.Configuration.IsPartiallyControlledConcurrencyAllowed)1901            {1902                IO.Debug.WriteLine($"[coyote::debug] {message}");1903                this.IsUncontrolledConcurrencyDetected = true;1904                return true;1905            }1906            else if (this.Configuration.IsSystematicFuzzingFallbackEnabled)1907            {1908                IO.Debug.WriteLine($"[coyote::debug] {message}");1909                this.IsUncontrolledConcurrencyDetected = true;1910                this.Detach(ExecutionStatus.ConcurrencyUncontrolled);1911            }1912            else1913            {1914                this.NotifyAssertionFailure(FormatUncontrolledConcurrencyExceptionMessage(message, methodName));1915            }1916            return false;1917        }1918        /// <summary>1919        /// Throws an <see cref="AssertionFailureException"/> exception containing the specified exception.1920        /// </summary>1921        internal void WrapAndThrowException(Exception exception, string s, params object[] args)1922        {1923            string msg = string.Format(CultureInfo.InvariantCulture, s, args);1924            string message = string.Format(CultureInfo.InvariantCulture,1925                "Exception '{0}' was thrown in {1}: {2}\n" +1926                "from location '{3}':\n" +1927                "The stack trace is:\n{4}",1928                exception.GetType(), msg, exception.Message, exception.Source, exception.StackTrace);1929            if (this.SchedulingPolicy is SchedulingPolicy.None)1930            {1931                throw new AssertionFailureException(message, exception);1932            }1933            this.NotifyUnhandledException(exception, message);1934        }1935        /// <summary>1936        /// Formats the message of the uncontrolled concurrency exception.1937        /// </summary>1938        private static string FormatUncontrolledConcurrencyExceptionMessage(string message, string methodName = default)1939        {1940            var mockMessage = methodName is null ? string.Empty : $" either replace or mock '{methodName}', or";1941            return $"{message} As a workaround, you can{mockMessage} use the '--no-repro' command line option " +1942                "(or the 'Configuration.WithNoBugTraceRepro()' method) to ignore this error by disabling bug " +1943                $"trace repro. Learn more at http://aka.ms/coyote-no-repro.\n{new StackTrace()}";1944        }1945        /// <summary>1946        /// Processes an unhandled exception in the specified controlled operation.1947        /// </summary>1948        internal void ProcessUnhandledExceptionInOperation(ControlledOperation op, Exception exception)1949        {1950            // Complete the failed operation. This is required so that the operation1951            // does not throw if it detaches.1952            op.Status = OperationStatus.Completed;1953            if (exception.GetBaseException() is ThreadInterruptedException)1954            {1955                // Ignore this exception, its thrown by the runtime.1956                IO.Debug.WriteLine("[coyote::debug] Controlled thread '{0}' executing operation '{1}' was interrupted.",1957                    Thread.CurrentThread.ManagedThreadId, op.Name);1958            }1959            else1960            {1961                string message;1962                string trace = FormatExceptionStackTrace(exception);1963                if (op is ActorOperation actorOp)1964                {1965                    message = string.Format(CultureInfo.InvariantCulture,1966                        $"Unhandled exception in actor '{actorOp.Name}'. {trace}");1967                }1968                else1969                {1970                    message = $"Unhandled exception. {trace}";1971                }1972                // Report the unhandled exception.1973                this.NotifyUnhandledException(exception, message);1974            }1975        }1976        /// <summary>1977        /// Formats the stack trace of the specified exception.1978        /// </summary>1979        private static string FormatExceptionStackTrace(Exception exception)1980        {1981            string[] lines = exception.ToString().Split(new[] { Environment.NewLine }, StringSplitOptions.None);1982            for (int i = 0; i < lines.Length; i++)1983            {1984                if (lines[i].StartsWith("   at Microsoft.Coyote.Rewriting", StringComparison.Ordinal))1985                {1986                    lines[i] = string.Empty;1987                }1988            }1989            return string.Join(Environment.NewLine, lines.Where(line => !string.IsNullOrEmpty(line)));1990        }1991        /// <summary>1992        /// Formats the specified stack trace of a specification monitor.1993        /// </summary>1994        private static string FormatSpecificationMonitorStackTrace(StackTrace trace)1995        {1996            StringBuilder sb = new StringBuilder();1997            string[] lines = trace.ToString().Split(new[] { Environment.NewLine }, StringSplitOptions.None);1998            foreach (var line in lines)1999            {2000                if ((line.Contains("at Microsoft.Coyote.Specifications") ||2001                    line.Contains("at Microsoft.Coyote.Runtime")) &&2002                    !line.Contains($"at {typeof(Specification).FullName}.{nameof(Specification.Monitor)}"))2003                {2004                    continue;2005                }2006                sb.AppendLine(line);2007            }2008            return sb.ToString();2009        }2010        /// <summary>2011        /// Raises the <see cref="OnFailure"/> event with the specified <see cref="Exception"/>.2012        /// </summary>2013        internal void RaiseOnFailureEvent(Exception exception)2014        {2015            if (this.Configuration.AttachDebugger)2016            {2017                Debugger.Break();2018                this.Configuration.AttachDebugger = false;2019            }2020            this.OnFailure?.Invoke(exception);2021        }2022        /// <summary>2023        /// Populates the specified test report.2024        /// </summary>2025        internal void PopulateTestReport(ITestReport report)2026        {2027            using (SynchronizedSection.Enter(this.RuntimeLock))2028            {2029                bool isBugFound = this.ExecutionStatus is ExecutionStatus.BugFound;2030                report.SetSchedulingStatistics(isBugFound, this.BugReport, this.OperationMap.Count,2031                    (int)this.MaxConcurrencyDegree, this.Scheduler.StepCount, this.Scheduler.IsMaxStepsReached,2032                    this.Scheduler.IsScheduleFair);2033                if (isBugFound)2034                {2035                    report.SetUnhandledException(this.UnhandledException);2036                }2037                report.SetUncontrolledInvocations(this.UncontrolledInvocations);2038            }2039        }2040        /// <summary>2041        /// Sets up the context of the executing controlled thread, allowing future retrieval2042        /// of runtime related data from the same thread, as well as across threads that share2043        /// the same asynchronous control flow.2044        /// </summary>2045        private void SetCurrentExecutionContext(ControlledOperation op)2046        {2047            ThreadLocalRuntime.Value = this;2048            AsyncLocalRuntime.Value = this;2049            this.SetControlledSynchronizationContext();2050            // Assign the specified controlled operation to the executing thread, and2051            // associate the operation group, if any, with the current context.2052            ExecutingOperation.Value = op;2053            OperationGroup.SetCurrent(op.Group);2054        }2055        /// <summary>2056        /// Removes any runtime related data from the context of the executing controlled thread.2057        /// </summary>2058        private static void CleanCurrentExecutionContext()2059        {2060            ExecutingOperation.Value = null;2061            AsyncLocalRuntime.Value = null;2062            ThreadLocalRuntime.Value = null;2063            OperationGroup.RemoveFromContext();2064        }2065        /// <summary>2066        /// Sets the synchronization context to the controlled synchronization context.2067        /// </summary>2068        private void SetControlledSynchronizationContext() =>2069            SynchronizationContext.SetSynchronizationContext(this.SyncContext);2070        /// <inheritdoc/>2071        public void RegisterLog(IRuntimeLog log) => this.LogWriter.RegisterLog(log);2072        /// <inheritdoc/>2073        public void RemoveLog(IRuntimeLog log) => this.LogWriter.RemoveLog(log);2074        /// <inheritdoc/>2075        public void Stop() => this.IsRunning = false;2076        /// <summary>2077        /// Detaches the scheduler and interrupts all controlled operations.2078        /// </summary>2079        /// <remarks>2080        /// It is assumed that this method runs in the scope of a <see cref="SynchronizedSection"/>.2081        /// </remarks>2082        private void Detach(ExecutionStatus status)2083        {2084            if (this.ExecutionStatus != ExecutionStatus.Running)2085            {2086                return;2087            }2088            try2089            {2090                if (status is ExecutionStatus.PathExplored)2091                {2092                    this.Logger.WriteLine($"[coyote::test] Exploration finished in runtime '{this.Id}' [reached the end of the test method].");2093                }2094                else if (status is ExecutionStatus.BoundReached)2095                {2096                    this.Logger.WriteLine($"[coyote::test] Exploration finished in runtime '{this.Id}' [reached the given bound].");2097                }2098                else if (status is ExecutionStatus.Deadlocked)2099                {2100                    this.Logger.WriteLine($"[coyote::test] Exploration finished in runtime '{this.Id}' [detected a potential deadlock].");2101                }2102                else if (status is ExecutionStatus.ConcurrencyUncontrolled)2103                {2104                    this.Logger.WriteLine($"[coyote::test] Exploration finished in runtime '{this.Id}' [detected uncontrolled concurrency].");2105                }2106                else if (status is ExecutionStatus.BugFound)2107                {2108                    this.Logger.WriteLine($"[coyote::test] Exploration finished in runtime '{this.Id}' [found a bug using the '{0}' strategy].",2109                        this.Configuration.SchedulingStrategy);2110                }2111                this.ExecutionStatus = status;2112                this.CancellationSource.Cancel();2113                // Complete any remaining operations at the end of the schedule.2114                foreach (var op in this.OperationMap.Values)2115                {2116                    if (op.Status != OperationStatus.Completed)2117                    {2118                        op.Status = OperationStatus.Completed;2119                        // Interrupt the thread executing this operation.2120                        if (op == ExecutingOperation.Value)2121                        {2122                            throw new ThreadInterruptedException();2123                        }2124                        else if (this.ThreadPool.TryGetValue(op.Id, out Thread thread))2125                        {2126                            thread.Interrupt();2127                        }2128                    }2129                }2130            }2131            finally2132            {2133                // Check if the completion source is completed, else set its result.2134                if (!this.CompletionSource.Task.IsCompleted)2135                {2136                    this.IsRunning = false;2137                    this.CompletionSource.SetResult(true);2138                }2139            }2140        }2141        /// <summary>2142        /// Disposes runtime resources.2143        /// </summary>2144        private void Dispose(bool disposing)2145        {2146            if (disposing)2147            {2148                RuntimeProvider.Deregister(this.Id);2149                using (SynchronizedSection.Enter(this.RuntimeLock))2150                {2151                    foreach (var op in this.OperationMap.Values)2152                    {2153                        op.Dispose();2154                    }2155                    foreach (var handler in this.PendingStartOperationMap.Values)2156                    {2157                        handler.Dispose();2158                    }2159                    this.ThreadPool.Clear();2160                    this.OperationMap.Clear();2161                    this.PendingStartOperationMap.Clear();2162                    this.ControlledThreads.Clear();2163                    this.ControlledTasks.Clear();2164                    this.UncontrolledTasks.Clear();2165                    this.UncontrolledInvocations.Clear();2166                    this.SpecificationMonitors.Clear();2167                    this.TaskLivenessMonitors.Clear();2168                    this.DefaultActorExecutionContext.Dispose();2169                    this.ControlledTaskScheduler.Dispose();2170                    this.SyncContext.Dispose();2171                    this.CancellationSource.Dispose();2172                }2173                if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)2174                {2175                    // Note: this makes it possible to run a Controlled unit test followed by a production2176                    // unit test, whereas before that would throw "Uncontrolled Task" exceptions.2177                    // This does not solve mixing unit test type in parallel.2178                    Interlocked.Decrement(ref ExecutionControlledUseCount);2179                }2180            }2181        }2182        /// <summary>2183        /// Disposes runtime resources.2184        /// </summary>2185        public void Dispose()2186        {2187            this.Dispose(true);2188            GC.SuppressFinalize(this);2189        }2190    }2191}...

Monitor.cs

Source:Monitor.cs

...587            internal void Exit()588            {589                var op = this.Resource.Runtime.GetExecutingOperation();590                this.Resource.Runtime.Assert(this.LockCountMap.ContainsKey(op),591                    "Cannot invoke Dispose without acquiring the lock.");592                this.LockCountMap[op]--;593                if (this.LockCountMap[op] is 0)594                {595                    // Only release the lock if the invocation is not reentrant.596                    this.LockCountMap.Remove(op);597                    this.UnlockNextReady();598                    this.Resource.Runtime.ScheduleNextOperation(op, SchedulingPointType.Release);599                }600                int useCount = SystemInterlocked.Decrement(ref this.UseCount);601                if (useCount is 0 && Cache[this.SyncObject].Value == this)602                {603                    // It is safe to remove this instance from the cache.604                    Cache.TryRemove(this.SyncObject, out _);605                }606            }607            /// <summary>608            /// Releases resources used by the synchronized block.609            /// </summary>610            protected void Dispose(bool disposing)611            {612                if (disposing)613                {614                    this.Exit();615                }616            }617            /// <summary>618            /// Releases resources used by the synchronized block.619            /// </summary>620            public void Dispose()621            {622                this.Dispose(true);623                GC.SuppressFinalize(this);624            }625            /// <summary>626            /// The type of a pulse operation.627            /// </summary>628            private enum PulseOperation629            {630                /// <summary>631                /// Pulses the next waiting operation.632                /// </summary>633                Next,634                /// <summary>635                /// Pulses all waiting operations.636                /// </summary>...

ControlledOperation.cs

Source:ControlledOperation.cs

...122            {123                this.SyncEvent.Wait();124                this.SyncEvent.Reset();125            }126            catch (ObjectDisposedException)127            {128                // The handler was disposed, so we can ignore this exception.129            }130        }131        /// <summary>132        /// Signals this operation to resume its execution.133        /// </summary>134        internal void Signal() => this.SyncEvent.Set();135        /// <summary>136        /// Sets a callback that executes the next continuation of this operation.137        /// </summary>138        internal void SetContinuationCallback(Action callback) => this.Continuations.Enqueue(callback);139        /// <summary>140        /// Pauses this operation and sets a callback that returns true when the141        /// dependency causing the pause has been resolved.142        /// </summary>143        internal void PauseWithDependency(Func<bool> callback, bool isControlled)144        {145            this.Status = OperationStatus.Paused;146            this.Dependency = callback;147            this.IsDependencyUncontrolled = !isControlled;148        }149        /// <summary>150        /// Tries to enable this operation if its dependency has been resolved.151        /// </summary>152        internal bool TryEnable()153        {154            if (this.Status is OperationStatus.Paused && (this.Dependency?.Invoke() ?? true))155            {156                this.Dependency = null;157                this.IsDependencyUncontrolled = false;158                this.Status = OperationStatus.Enabled;159            }160            return this.Status is OperationStatus.Enabled;161        }162        /// <summary>163        /// Returns the hashed state of this operation for the specified policy.164        /// </summary>165        internal virtual int GetHashedState(SchedulingPolicy policy) => 0;166        /// <summary>167        /// Determines whether the specified object is equal to the current object.168        /// </summary>169        public override bool Equals(object obj)170        {171            if (obj is ControlledOperation op)172            {173                return this.Id == op.Id;174            }175            return false;176        }177        /// <summary>178        /// Returns the hash code for this instance.179        /// </summary>180        public override int GetHashCode() => this.Id.GetHashCode();181        /// <summary>182        /// Returns a string that represents the current operation id.183        /// </summary>184        public override string ToString() => this.Name;185        /// <summary>186        /// Indicates whether the specified <see cref="ControlledOperation"/> is equal187        /// to the current <see cref="ControlledOperation"/>.188        /// </summary>189        public bool Equals(ControlledOperation other) => this.Equals((object)other);190        /// <summary>191        /// Indicates whether the specified <see cref="ControlledOperation"/> is equal192        /// to the current <see cref="ControlledOperation"/>.193        /// </summary>194        bool IEquatable<ControlledOperation>.Equals(ControlledOperation other) => this.Equals(other);195        /// <summary>196        /// Releases any held resources.197        /// </summary>198        public void Dispose()199        {200            this.SyncEvent.Dispose();201        }202    }203}...

Dispose

Using AI Code Generation

1using Microsoft.Coyote;2using Microsoft.Coyote.Runtime;3using Microsoft.Coyote.Tasks;4using System;5using System.Threading.Tasks;6{7    {8        static void Main(string[] args)9        {10            ControlledOperation op = new ControlledOperation();11            Task task = Task.Run(() => { Console.WriteLine("Hello World!"); });12            op.Wait(task);13            op.Dispose();14            Console.ReadLine();15        }16    }17}18using Microsoft.Coyote;19using Microsoft.Coyote.Runtime;20using Microsoft.Coyote.Tasks;21using System;22using System.Threading.Tasks;23{24    {25        static void Main(string[] args)26        {27            ControlledOperation op = new ControlledOperation();28            Task task = Task.Run(() => { Console.WriteLine("Hello World!"); });29            op.Wait(task);30            op.Dispose();31            Console.ReadLine();32        }33    }34}35using Microsoft.Coyote;36using Microsoft.Coyote.Runtime;37using Microsoft.Coyote.Tasks;38using System;39using System.Threading.Tasks;40{41    {42        static void Main(string[] args)43        {44            ControlledOperation op = new ControlledOperation();45            Task task = Task.Run(() => { Console.WriteLine("Hello World!"); });46            op.Wait(task);47            op.Dispose();48            Console.ReadLine();49        }50    }51}52using Microsoft.Coyote;53using Microsoft.Coyote.Runtime;54using Microsoft.Coyote.Tasks;55using System;56using System.Threading.Tasks;57{58    {59        static void Main(string[] args)60        {61            ControlledOperation op = new ControlledOperation();62            Task task = Task.Run(() => { Console.WriteLine("Hello World!"); });63            op.Wait(task);64            op.Dispose();65            Console.ReadLine();66        }67    }68}

Automation Testing Tutorials

Learn to execute automation testing from scratch with LambdaTest Learning Hub. Right from setting up the prerequisites to run your first automation test, to following best practices and diving deeper into advanced test scenarios. LambdaTest Learning Hubs compile a list of step-by-step guides to help you be proficient with different test automation frameworks i.e. Selenium, Cypress, TestNG etc.