How to use ToString method of Microsoft.Coyote.Runtime.OperationGroup class

Best Coyote code snippet using Microsoft.Coyote.Runtime.OperationGroup.ToString

CoyoteRuntime.cs

Source:CoyoteRuntime.cs Github

copy

Full Screen

...418 {419 CleanCurrentExecutionContext();420 }421 });422 thread.Name = Guid.NewGuid().ToString();423 thread.IsBackground = true;424 // TODO: optimize by reusing threads instead of creating a new thread each time?425 this.ThreadPool.AddOrUpdate(op.Id, thread, (id, oldThread) => thread);426 this.ControlledThreads.AddOrUpdate(thread.Name, op, (threadName, oldOp) => op);427 thread.Start();428 }429 }430 /// <summary>431 /// Schedules the specified delay to be executed asynchronously.432 /// </summary>433#if !DEBUG434 [DebuggerStepThrough]435#endif436 internal Task ScheduleDelay(TimeSpan delay, CancellationToken cancellationToken)437 {438 if (delay.TotalMilliseconds is 0)439 {440 // If the delay is 0, then complete synchronously.441 return Task.CompletedTask;442 }443 // TODO: support cancellations during testing.444 if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)445 {446 uint timeout = (uint)this.GetNextNondeterministicIntegerChoice((int)this.Configuration.TimeoutDelay, null, null);447 if (timeout is 0)448 {449 // If the delay is 0, then complete synchronously.450 return Task.CompletedTask;451 }452 // TODO: cache the dummy delay action to optimize memory.453 ControlledOperation op = this.CreateControlledOperation(timeout);454 return this.TaskFactory.StartNew(state =>455 {456 var delayedOp = state as ControlledOperation;457 delayedOp.Status = OperationStatus.PausedOnDelay;458 this.ScheduleNextOperation(delayedOp, SchedulingPointType.Yield);459 },460 op,461 cancellationToken,462 this.TaskFactory.CreationOptions | TaskCreationOptions.DenyChildAttach,463 this.TaskFactory.Scheduler);464 }465 if (!this.TryGetExecutingOperation(out ControlledOperation current))466 {467 // Cannot fuzz the delay of an uncontrolled operation.468 return Task.Delay(delay, cancellationToken);469 }470 // TODO: we need to come up with something better!471 // Fuzz the delay.472 return Task.Delay(TimeSpan.FromMilliseconds(473 this.GetNondeterministicDelay(current, (int)delay.TotalMilliseconds)));474 }475 /// <summary>476 /// Unwraps the specified task.477 /// </summary>478 internal Task UnwrapTask(Task<Task> task)479 {480 var unwrappedTask = task.Unwrap();481 if (this.ControlledTasks.TryGetValue(task, out ControlledOperation op))482 {483 this.ControlledTasks.TryAdd(unwrappedTask, op);484 }485 return unwrappedTask;486 }487 /// <summary>488 /// Unwraps the specified task.489 /// </summary>490 internal Task<TResult> UnwrapTask<TResult>(Task<Task<TResult>> task)491 {492 var unwrappedTask = task.Unwrap();493 if (this.ControlledTasks.TryGetValue(task, out ControlledOperation op))494 {495 this.ControlledTasks.TryAdd(unwrappedTask, op);496 }497 return unwrappedTask;498 }499 /// <summary>500 /// Registers the specified task as a known controlled task.501 /// </summary>502 internal void RegisterKnownControlledTask(Task task)503 {504 if (this.SchedulingPolicy != SchedulingPolicy.None)505 {506 this.ControlledTasks.TryAdd(task, null);507 }508 }509 /// <summary>510 /// Creates a new controlled operation with an optional delay.511 /// </summary>512 internal ControlledOperation CreateControlledOperation(uint delay = 0)513 {514 using (SynchronizedSection.Enter(this.RuntimeLock))515 {516 // Assign the operation group associated with the execution context of the517 // current thread, if such a group exists, else the group of the currently518 // executing operation, if such an operation exists.519 OperationGroup group = OperationGroup.Current ?? ExecutingOperation.Value?.Group;520 // Create a new controlled operation using the next available operation id.521 ulong operationId = this.GetNextOperationId();522 ControlledOperation op = delay > 0 ?523 new DelayOperation(operationId, $"Delay({operationId})", delay, this) :524 new ControlledOperation(operationId, $"Op({operationId})", group, this);525 if (operationId > 0 && !this.IsThreadControlled(Thread.CurrentThread))526 {527 op.IsSourceUncontrolled = true;528 }529 return op;530 }531 }532 /// <summary>533 /// Creates a new user-defined controlled operation from the specified builder.534 /// </summary>535 internal ControlledOperation CreateUserDefinedOperation(IOperationBuilder builder)536 {537 using (SynchronizedSection.Enter(this.RuntimeLock))538 {539 // Create a new controlled operation using the next available operation id.540 ulong operationId = this.GetNextOperationId();541 var op = new UserDefinedOperation(this, builder, operationId);542 if (operationId > 0 && !this.IsThreadControlled(Thread.CurrentThread))543 {544 op.IsSourceUncontrolled = true;545 }546 return op;547 }548 }549 /// <summary>550 /// Registers the specified newly created controlled operation.551 /// </summary>552 /// <param name="op">The newly created operation to register.</param>553 internal void RegisterNewOperation(ControlledOperation op)554 {555 using (SynchronizedSection.Enter(this.RuntimeLock))556 {557 if (this.ExecutionStatus != ExecutionStatus.Running)558 {559 return;560 }561#if NETSTANDARD2_0 || NETFRAMEWORK562 if (!this.OperationMap.ContainsKey(op.Id))563 {564 this.OperationMap.Add(op.Id, op);565 }566#else567 this.OperationMap.TryAdd(op.Id, op);568#endif569 // Assign the operation as a member of its group.570 op.Group.RegisterMember(op);571 if (this.OperationMap.Count is 1)572 {573 // This is the first operation registered, so schedule it.574 this.ScheduledOperation = op;575 }576 else577 {578 // As this is not the first operation getting created, assign an event579 // handler so that the next scheduling decision cannot be made until580 // this operation starts executing to avoid race conditions.581 this.PendingStartOperationMap.Add(op, new ManualResetEventSlim(false));582 }583 IO.Debug.WriteLine("[coyote::debug] Created operation '{0}' of group '{1}' on thread '{2}'.",584 op.Name, op.Group, Thread.CurrentThread.ManagedThreadId);585 }586 }587 /// <summary>588 /// Starts the execution of the specified controlled operation.589 /// </summary>590 /// <param name="op">The operation to start executing.</param>591 /// <remarks>592 /// This method performs a handshake with <see cref="WaitOperationsStart"/>.593 /// </remarks>594 internal void StartOperation(ControlledOperation op)595 {596 // Configures the execution context of the current thread with data597 // related to the runtime and the operation executed by this thread.598 this.SetCurrentExecutionContext(op);599 using (SynchronizedSection.Enter(this.RuntimeLock))600 {601 IO.Debug.WriteLine("[coyote::debug] Started operation '{0}' of group '{1}' on thread '{2}'.",602 op.Name, op.Group, Thread.CurrentThread.ManagedThreadId);603 op.Status = OperationStatus.Enabled;604 if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)605 {606 // If this operation has an associated handler that notifies another awaiting607 // operation about this operation starting its execution, then set the handler.608 if (this.PendingStartOperationMap.TryGetValue(op, out ManualResetEventSlim handler))609 {610 handler.Set();611 }612 // Pause the operation as soon as it starts executing to allow the runtime613 // to explore a potential interleaving with another executing operation.614 this.PauseOperation(op);615 }616 }617 }618 /// <summary>619 /// Waits for all recently created operations to start executing.620 /// </summary>621 /// <remarks>622 /// This method performs a handshake with <see cref="StartOperation"/>. It is assumed that this623 /// method is invoked by the same thread executing the operation and that it runs in the scope624 /// of a <see cref="SynchronizedSection"/>.625 /// </remarks>626 private void WaitOperationsStart()627 {628 if (this.SchedulingPolicy is SchedulingPolicy.Interleaving)629 {630 while (this.PendingStartOperationMap.Count > 0)631 {632 var pendingOp = this.PendingStartOperationMap.First();633 while (pendingOp.Key.Status is OperationStatus.None && this.ExecutionStatus is ExecutionStatus.Running)634 {635 IO.Debug.WriteLine("[coyote::debug] Sleeping thread '{0}' until operation '{1}' of group '{2}' starts.",636 Thread.CurrentThread.ManagedThreadId, pendingOp.Key.Name, pendingOp.Key.Group);637 using (SynchronizedSection.Exit(this.RuntimeLock))638 {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>...

Full Screen

Full Screen

ControlledOperation.cs

Source:ControlledOperation.cs Github

copy

Full Screen

...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()...

Full Screen

Full Screen

OperationGroup.cs

Source:OperationGroup.cs Github

copy

Full Screen

...101 public override int GetHashCode() => this.Id.GetHashCode();102 /// <summary>103 /// Returns a string that represents the current group id.104 /// </summary>105 public override string ToString() => this.Id.ToString();106 /// <summary>107 /// Indicates whether the specified <see cref="OperationGroup"/> is equal108 /// to the current <see cref="OperationGroup"/>.109 /// </summary>110 public bool Equals(OperationGroup other) => this.Equals((object)other);111 /// <summary>112 /// Indicates whether the specified <see cref="OperationGroup"/> is equal113 /// to the current <see cref="OperationGroup"/>.114 /// </summary>115 bool IEquatable<OperationGroup>.Equals(OperationGroup other) => this.Equals(other);116 /// <summary>117 /// Removes this operation group from the local context.118 /// </summary>119 internal static void RemoveFromContext()...

Full Screen

Full Screen

ToString

Using AI Code Generation

copy

Full Screen

1using System;2using System.Collections.Generic;3using System.Linq;4using System.Text;5using System.Threading.Tasks;6{7 {8 static void Main(string[] args)9 {10 Microsoft.Coyote.Runtime.OperationGroup opGroup = new Microsoft.Coyote.Runtime.OperationGroup();11 Console.WriteLine(opGroup.ToString());12 Console.WriteLine("Press any key to exit.");13 Console.ReadKey();14 }15 }16}17using System;18using System.Collections.Generic;19using System.Linq;20using System.Text;21using System.Threading.Tasks;22{23 {24 static void Main(string[] args)25 {26 Microsoft.Coyote.Runtime.OperationGroup opGroup = new Microsoft.Coyote.Runtime.OperationGroup();27 Console.WriteLine(opGroup.ToString());28 Console.WriteLine("Press any key to exit.");29 Console.ReadKey();30 }31 }32}33using System;34using System.Collections.Generic;35using System.Linq;36using System.Text;37using System.Threading.Tasks;38{39 {40 static void Main(string[] args)41 {42 Microsoft.Coyote.Runtime.OperationGroup opGroup = new Microsoft.Coyote.Runtime.OperationGroup();43 Console.WriteLine(opGroup.ToString());44 Console.WriteLine("Press any key to exit.");45 Console.ReadKey();46 }47 }48}49using System;50using System.Collections.Generic;51using System.Linq;52using System.Text;53using System.Threading.Tasks;54{55 {56 static void Main(string[] args)57 {58 Microsoft.Coyote.Runtime.OperationGroup opGroup = new Microsoft.Coyote.Runtime.OperationGroup();59 Console.WriteLine(opGroup.ToString());60 Console.WriteLine("Press any key to exit.");61 Console.ReadKey();62 }63 }64}65using System;66using System.Collections.Generic;67using System.Linq;68using System.Text;69using System.Threading.Tasks;70{71 {72 static void Main(string[] args)73 {

Full Screen

Full Screen

ToString

Using AI Code Generation

copy

Full Screen

1using System;2using System.Collections.Generic;3using System.Linq;4using System.Text;5using System.Threading.Tasks;6using Microsoft.Coyote;7using Microsoft.Coyote.Actors;8using Microsoft.Coyote.Runtime;9using Microsoft.Coyote.Specifications;10using Microsoft.Coyote.Tasks;11{12 {13 static void Main(string[] args)14 {15 var opGroup = new OperationGroup();16 opGroup.Add(1, "Hello");17 opGroup.Add(2, "World");18 opGroup.Add(3, "!");19 Console.WriteLine(opGroup.ToString());20 Console.ReadLine();21 }22 }23}

Full Screen

Full Screen

ToString

Using AI Code Generation

copy

Full Screen

1Microsoft.Coyote.Runtime.OperationGroup opGroup = new Microsoft.Coyote.Runtime.OperationGroup();2string str = opGroup.ToString();3Microsoft.Coyote.Runtime.OperationId opId = new Microsoft.Coyote.Runtime.OperationId();4string str = opId.ToString();5Microsoft.Coyote.Runtime.OperationInfo opInfo = new Microsoft.Coyote.Runtime.OperationInfo();6string str = opInfo.ToString();7Microsoft.Coyote.Runtime.OperationInfo opInfo = new Microsoft.Coyote.Runtime.OperationInfo();8string str = opInfo.ToString();9Microsoft.Coyote.Runtime.OperationInfo opInfo = new Microsoft.Coyote.Runtime.OperationInfo();10string str = opInfo.ToString();11Microsoft.Coyote.Runtime.OperationInfo opInfo = new Microsoft.Coyote.Runtime.OperationInfo();12string str = opInfo.ToString();13Microsoft.Coyote.Runtime.OperationInfo opInfo = new Microsoft.Coyote.Runtime.OperationInfo();14string str = opInfo.ToString();15Microsoft.Coyote.Runtime.OperationInfo opInfo = new Microsoft.Coyote.Runtime.OperationInfo();16string str = opInfo.ToString();17Microsoft.Coyote.Runtime.OperationInfo opInfo = new Microsoft.Coyote.Runtime.OperationInfo();18string str = opInfo.ToString();19Microsoft.Coyote.Runtime.OperationInfo opInfo = new Microsoft.Coyote.Runtime.OperationInfo();20string str = opInfo.ToString();

Full Screen

Full Screen

ToString

Using AI Code Generation

copy

Full Screen

1using System;2using Microsoft.Coyote;3using Microsoft.Coyote.Actors;4using Microsoft.Coyote.Tasks;5using Microsoft.Coyote.Runtime;6using Microsoft.Coyote.IO;7using System.Threading.Tasks;8using System.Threading;9{10 {11 }12 {13 }14 {15 }16 {17 }18 {19 }20 {21 }22 {23 }24 {25 }26 {27 }28 {29 }30 {31 }32 {33 }34 {35 }36 {37 }38 {39 }40 {41 }42 {43 }44 {45 }46 {47 }48 {49 }50 {51 }52 {53 }54 {55 }56 {57 }58 {59 }60 {61 }62 {63 }64 {65 }66 {67 }68 {69 }70 {71 }72 {73 }74 {75 }76 {77 }78 {79 }80 {81 }82 {83 }

Full Screen

Full Screen

ToString

Using AI Code Generation

copy

Full Screen

1using Microsoft.Coyote;2using Microsoft.Coyote.Specifications;3using Microsoft.Coyote.SystematicTesting;4using Microsoft.Coyote.Tasks;5using System;6using System.Threading.Tasks;7{8 {9 public static async Task Main()10 {11 var test = Task.Run(() => { });12 var config = Configuration.Create();13 config.TestingIterations = 1;14 config.MaxSchedulingSteps = 100;15 config.MaxFairSchedulingSteps = 100;16 config.MaxUnfairSchedulingSteps = 100;17 config.MaxStepsFromAnyEntryToExit = 100;18 config.MaxStepsFromAnyEntryToExit = 100;

Full Screen

Full Screen

ToString

Using AI Code Generation

copy

Full Screen

1using System;2using Microsoft.Coyote.Runtime;3{4 public static void Main()5 {6 OperationGroup opGroup = new OperationGroup(1, "Hello");7 Console.WriteLine(opGroup.ToString());8 }9}

Full Screen

Full Screen

ToString

Using AI Code Generation

copy

Full Screen

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

Full Screen

Full Screen

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.

LambdaTest Learning Hubs:

YouTube

You could also refer to video tutorials over LambdaTest YouTube channel to get step by step demonstration from industry experts.

Run Coyote automation tests on LambdaTest cloud grid

Perform automation testing on 3000+ real desktop and mobile devices online.

Most used method in OperationGroup

Try LambdaTest Now !!

Get 100 minutes of automation test minutes FREE!!

Next-Gen App & Browser Testing Cloud

Was this article helpful?

Helpful

NotHelpful