option to treat data nondeterminism with warnings (#434)

Source/Core/Configuration.cs

@@ -83,6 +83,14 @@ namespace Microsoft.Coyote
         [DataMember]
         internal bool IsPartiallyControlledConcurrencyAllowed;
 
+        /// <summary>
+        /// If this option is enabled and uncontrolled data non-determinism is detected, then the
+        /// runtime will attempt to partially control the data non-determinism of the application,
+        /// instead of immediately failing with an error.
+        /// </summary>
+        [DataMember]
+        internal bool IsPartiallyControlledDataNondeterminismAllowed;
+
         /// <summary>
         /// If this option is enabled, the systematic fuzzing policy is used during testing.
         /// </summary>
@@ -291,6 +299,7 @@ namespace Microsoft.Coyote
             this.RandomGeneratorSeed = null;
             this.PortfolioMode = PortfolioMode.Fair;
             this.IsPartiallyControlledConcurrencyAllowed = true;
+            this.IsPartiallyControlledDataNondeterminismAllowed = true;
             this.IsSystematicFuzzingEnabled = false;
             this.IsSystematicFuzzingFallbackEnabled = true;
             this.MaxFuzzingDelay = 1000;
@@ -512,6 +521,16 @@ namespace Microsoft.Coyote
             return this;
         }
 
+        /// <summary>
+        /// Updates the configuration with partially controlled data non-determinism allowed or disallowed.
+        /// </summary>
+        /// <param name="isAllowed">If true, then partially controlled data non-determinism is allowed.</param>
+        public Configuration WithPartiallyControlledDataNondeterminismAllowed(bool isAllowed = true)
+        {
+            this.IsPartiallyControlledDataNondeterminismAllowed = isAllowed;
+            return this;
+        }
+
         /// <summary>
         /// Updates the configuration with systematic fuzzing enabled or disabled.
         /// </summary>

Source/Core/Runtime/CoyoteRuntime.cs

@@ -2107,7 +2107,7 @@ namespace Microsoft.Coyote.Runtime
                         $"is invoking the {methodName} synchronization method, which can cause deadlocks during testing.";
                     if (this.Configuration.IsSystematicFuzzingFallbackEnabled)
                     {
-                        this.LogWriter.LogDebug("[coyote::debug] {0}", message);
+                        this.LogWriter.LogWarning("[coyote::warning] {0}", message);
                         this.IsUncontrolledConcurrencyDetected = true;
                         this.Detach(ExecutionStatus.ConcurrencyUncontrolled);
                     }
@@ -2135,17 +2135,17 @@ namespace Microsoft.Coyote.Runtime
                 {
                     string message = $"Invoking '{methodName}' introduces data non-determinism that is not intercepted " +
                         "and controlled during testing, so it can interfere with the ability to reproduce bug traces.";
-                    if (this.Configuration.IsPartiallyControlledConcurrencyAllowed ||
+                    if (this.Configuration.IsPartiallyControlledDataNondeterminismAllowed ||
                         this.Configuration.IsSystematicFuzzingFallbackEnabled)
                     {
                         if (this.Configuration.IsUncontrolledInvocationStackTraceLoggingEnabled)
                         {
-                            this.LogWriter.LogDebug("[coyote::debug] {0}{1}{2}", message, Environment.NewLine,
+                            this.LogWriter.LogWarning("[coyote::warning] {0}{1}{2}", message, Environment.NewLine,
                                 FormatUncontrolledStackTrace(new StackTrace()));
                         }
                         else
                         {
-                            this.LogWriter.LogDebug("[coyote::debug] {0}", message);
+                            this.LogWriter.LogWarning("[coyote::warning] {0}", message);
                         }
                     }
                     else
@@ -2247,12 +2247,12 @@ namespace Microsoft.Coyote.Runtime
             {
                 if (this.Configuration.IsUncontrolledInvocationStackTraceLoggingEnabled)
                 {
-                    this.LogWriter.LogDebug("[coyote::debug] {0}{1}{2}", message, Environment.NewLine,
+                    this.LogWriter.LogWarning("[coyote::warning] {0}{1}{2}", message, Environment.NewLine,
                         FormatUncontrolledStackTrace(new StackTrace()));
                 }
                 else
                 {
-                    this.LogWriter.LogDebug("[coyote::debug] {0}", message);
+                    this.LogWriter.LogWarning("[coyote::warning] {0}", message);
                 }
 
                 this.IsUncontrolledConcurrencyDetected = true;

Source/Test/Rewriting/Passes/Rewriting/UncontrolledInvocationRewritingPass.cs

@@ -192,6 +192,12 @@ namespace Microsoft.Coyote.Rewriting
                     isDataNondeterministic = true;
                     return true;
                 }
+                else if (type.Name is nameof(System.Guid) && member != null &&
+                    member.Name is nameof(System.Guid.NewGuid))
+                {
+                    isDataNondeterministic = true;
+                    return true;
+                }
             }
 
             return false;

Source/Test/SystematicTesting/Reports/TraceReport.cs

@@ -65,6 +65,7 @@ namespace Microsoft.Coyote.SystematicTesting
             report.Settings.LivenessTemperatureThreshold = configuration.LivenessTemperatureThreshold;
             report.Settings.IsLockAccessRaceCheckingEnabled = configuration.IsLockAccessRaceCheckingEnabled;
             report.Settings.IsPartiallyControlledConcurrencyAllowed = configuration.IsPartiallyControlledConcurrencyAllowed;
+            report.Settings.IsPartiallyControlledDataNondeterminismAllowed = configuration.IsPartiallyControlledDataNondeterminismAllowed;
             report.Settings.UncontrolledConcurrencyResolutionAttempts = configuration.UncontrolledConcurrencyResolutionAttempts;
             report.Settings.UncontrolledConcurrencyResolutionDelay = configuration.UncontrolledConcurrencyResolutionDelay;
 
@@ -105,6 +106,7 @@ namespace Microsoft.Coyote.SystematicTesting
                 configuration.LivenessTemperatureThreshold = report.Settings.LivenessTemperatureThreshold;
                 configuration.IsLockAccessRaceCheckingEnabled = report.Settings.IsLockAccessRaceCheckingEnabled;
                 configuration.IsPartiallyControlledConcurrencyAllowed = report.Settings.IsPartiallyControlledConcurrencyAllowed;
+                configuration.IsPartiallyControlledDataNondeterminismAllowed = report.Settings.IsPartiallyControlledDataNondeterminismAllowed;
                 configuration.UncontrolledConcurrencyResolutionAttempts = report.Settings.UncontrolledConcurrencyResolutionAttempts;
                 configuration.UncontrolledConcurrencyResolutionDelay = report.Settings.UncontrolledConcurrencyResolutionDelay;
 
@@ -244,6 +246,11 @@ namespace Microsoft.Coyote.SystematicTesting
             /// </summary>
             public bool IsPartiallyControlledConcurrencyAllowed { get; set; }
 
+            /// <summary>
+            /// Value specifying if partially controlled data non-determinism is allowed or not.
+            /// </summary>
+            public bool IsPartiallyControlledDataNondeterminismAllowed { get; set; }
+
             /// <summary>
             /// Value that controls how many times the runtime can check if each instance
             /// of uncontrolled concurrency has resolved during testing before timing out.

Tools/Coyote/Cli/CommandLineParser.cs

@@ -412,11 +412,23 @@ namespace Microsoft.Coyote.Cli
                 Arity = ArgumentArity.Zero
             };
 
-            var noPartialControlOption = new Option<bool>(
-                name: "--no-partial-control",
-                description: "Disallow partially controlled concurrency during controlled testing.")
+            var allowedPartialControlModes = new HashSet<string>
             {
-                Arity = ArgumentArity.Zero
+                "none",
+                "concurrency",
+                "data"
+            };
+
+            var partialControlOption = new Option<string>(
+                name: "--partial-control",
+                description: "Set the partial controlled mode to use during testing. If set to 'concurrency' then " +
+                    "only concurrency can be partially controlled. If set to 'data' then only data non-determinism " +
+                    "can be partially controlled. If set to 'none' then partially controlled testing is disabled. " +
+                    "By default, both concurrency and data non-determinism can be partially controlled. " +
+                    $"Allowed values are {string.Join(", ", allowedPartialControlModes)}.")
+            {
+                ArgumentHelpName = "MODE",
+                Arity = ArgumentArity.ExactlyOne
             };
 
             var noReproOption = new Option<bool>(
@@ -485,6 +497,7 @@ namespace Microsoft.Coyote.Cli
             maxFuzzDelayOption.AddValidator(result => ValidateOptionValueIsUnsignedInteger(result));
             uncontrolledConcurrencyResolutionAttemptsOption.AddValidator(result => ValidateOptionValueIsUnsignedInteger(result));
             uncontrolledConcurrencyResolutionDelayOption.AddValidator(result => ValidateOptionValueIsUnsignedInteger(result));
+            partialControlOption.AddValidator(result => ValidateOptionValueIsAllowed(result, allowedPartialControlModes));
 
             // Build command.
             var command = new Command("test", "Run tests using the Coyote systematic testing engine.\n" +
@@ -514,7 +527,7 @@ namespace Microsoft.Coyote.Cli
             this.AddOption(command, skipPotentialDeadlocksOption);
             this.AddOption(command, skipLockRacesOption);
             this.AddOption(command, noFuzzingFallbackOption);
-            this.AddOption(command, noPartialControlOption);
+            this.AddOption(command, partialControlOption);
             this.AddOption(command, noReproOption);
             this.AddOption(command, logUncontrolledInvocationStackTracesOption);
             this.AddOption(command, failOnMaxStepsOption);
@@ -978,8 +991,25 @@ namespace Microsoft.Coyote.Cli
                     case "no-fuzzing-fallback":
                         this.Configuration.IsSystematicFuzzingFallbackEnabled = false;
                         break;
-                    case "no-partial-control":
-                        this.Configuration.IsPartiallyControlledConcurrencyAllowed = false;
+                    case "partial-control":
+                        string mode = result.GetValueOrDefault<string>();
+                        switch (mode)
+                        {
+                            case "concurrency":
+                                this.Configuration.IsPartiallyControlledConcurrencyAllowed = true;
+                                this.Configuration.IsPartiallyControlledDataNondeterminismAllowed = false;
+                                break;
+                            case "data":
+                                this.Configuration.IsPartiallyControlledConcurrencyAllowed = false;
+                                this.Configuration.IsPartiallyControlledDataNondeterminismAllowed = true;
+                                break;
+                            case "none":
+                            default:
+                                this.Configuration.IsPartiallyControlledConcurrencyAllowed = false;
+                                this.Configuration.IsPartiallyControlledDataNondeterminismAllowed = false;
+                                break;
+                        }
+
                         break;
                     case "log-uncontrolled-invocation-stack-traces":
                         this.Configuration.WithUncontrolledInvocationStackTraceLoggingEnabled();