Support for internal async test harness and async tests (#432)

Author: pdeligia

Source/Core/Configuration.cs

@@ -517,17 +517,15 @@ protected Configuration()
         }
 
         /// <summary>
-        /// Creates a new configuration.
+        /// Creates a new configuration with default values.
         /// </summary>
-        /// <returns>Configuration</returns>
         public static Configuration Create()
         {
             return new Configuration();
         }
 
         /// <summary>
-        /// Updates the configuration with verbose output enabled
-        /// and returns it.
+        /// Updates the configuration with verbose output enabled or disabled.
         /// </summary>
         /// <param name="isVerbose">If true, then messages are logged.</param>
         public Configuration WithVerbosityEnabled(bool isVerbose = true)
@@ -537,8 +535,7 @@ public Configuration WithVerbosityEnabled(bool isVerbose = true)
         }
 
         /// <summary>
-        /// Updates the configuration with verbose output enabled
-        /// and returns it.
+        /// Updates the configuration with verbose output enabled or disabled.
         /// </summary>
         /// <param name="level">The verbosity level.</param>
         [Obsolete("WithVerbosityEnabled(int level) is deprecated; use WithVerbosityEnabled(bool isVerbose) instead.")]
@@ -549,49 +546,44 @@ public Configuration WithVerbosityEnabled(int level)
         }
 
         /// <summary>
-        /// Updates the configuration with debugging information enabled
-        /// or disabled and returns it.
+        /// Updates the configuration with the specified scheduling strategy.
         /// </summary>
-        /// <param name="isEnabled">Is debugging enabled</param>
-        /// <returns>Configuration</returns>
-        public Configuration WithDebuggingEnabled(bool isEnabled = true)
+        /// <param name="strategy">The scheduling strategy.</param>
+        public Configuration WithStrategy(SchedulingStrategy strategy)
         {
-            Debug.IsEnabled = isEnabled;
+            this.SchedulingStrategy = strategy;
             return this;
         }
 
         /// <summary>
-        /// Updates the configuration with the scheduling strategy
-        /// and returns it.
+        /// Updates the configuration with the specified number of iterations to perform.
         /// </summary>
-        /// <param name="strategy">SchedulingStrategy</param>
-        /// <returns>Configuration</returns>
-        public Configuration WithStrategy(SchedulingStrategy strategy)
+        /// <param name="iterations">The number of iterations to perform.</param>
+        public Configuration WithNumberOfIterations(int iterations)
         {
-            this.SchedulingStrategy = strategy;
+            this.SchedulingIterations = iterations;
             return this;
         }
 
         /// <summary>
-        /// Updates the configuration with the number of iterations
-        /// and returns it.
+        /// Updates the configuration with the specified number of scheduling steps
+        /// to perform per iteration (for both fair and unfair schedulers).
         /// </summary>
-        /// <param name="iterations">Number of iterations</param>
-        /// <returns>Configuration</returns>
-        public Configuration WithNumberOfIterations(int iterations)
+        /// <param name="maxSteps">The scheduling steps to perform per iteration.</param>
+        public Configuration WithMaxSteps(int maxSteps)
         {
-            this.SchedulingIterations = iterations;
+            this.MaxSchedulingSteps = maxSteps;
             return this;
         }
 
         /// <summary>
         /// Indicates whether the requested C# version is supported for for rewriting.
         /// </summary>
-        /// <param name="major">The major version required</param>
-        /// <param name="minor">The minor version required</param>
+        /// <param name="major">The required major version.</param>
+        /// <param name="minor">The required minor version.</param>
         public bool IsRewriteCSharpVersion(int major, int minor)
         {
-            // Return true if not set
+            // Return true if not set.
             return this.RewriteCSharpVersion.Major == 0
                 || this.RewriteCSharpVersion >= new Version(major, minor);
         }

Source/Core/IO/Logging/MachineLogger.cs

@@ -232,7 +232,7 @@ public virtual void OnPop(MachineId machineId, string currStateName, string rest
         /// <param name="restoredStateName">The name of the state being re-entered, if any</param>
         public virtual string FormatOnPopString(MachineId machineId, string currStateName, string restoredStateName)
         {
-            var curStateName = string.IsNullOrEmpty(currStateName) ? "[not recorded]" : currStateName;
+            currStateName = string.IsNullOrEmpty(currStateName) ? "[not recorded]" : currStateName;
             var reenteredStateName = restoredStateName ?? string.Empty;
             return $"<PopLog> Machine '{machineId}' popped state '{currStateName}' and reentered state '{reenteredStateName}'.";
         }
@@ -341,7 +341,7 @@ public virtual void OnWait(MachineId machineId, string currStateName, params Typ
         /// <param name="eventTypes">The types of the events being waited for, if any.</param>
         public virtual string FormatOnWaitString(MachineId machineId, string currStateName, params Type[] eventTypes)
         {
-            string eventNames = string.Empty;
+            string eventNames;
             if (eventTypes.Length == 0)
             {
                 eventNames = "'<missing>'";

Source/Core/Properties/InternalsVisibleTo.cs

@@ -68,6 +68,12 @@
     "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
     "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
     "3bc97f9e")]
+[assembly: InternalsVisibleTo("PSharpTestLauncher,PublicKey=" +
+    "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
+    "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
+    "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
+    "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
+    "3bc97f9e")]
 
 // Tests
 [assembly: InternalsVisibleTo("Microsoft.PSharp.Core.Tests,PublicKey=" +
@@ -106,9 +112,3 @@
     "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
     "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
     "3bc97f9e")]
-[assembly: InternalsVisibleTo("Microsoft.PSharp.Tests.Launcher,PublicKey=" +
-    "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
-    "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
-    "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
-    "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
-    "3bc97f9e")]

Source/Core/Runtime/MachineRuntime.cs

@@ -577,14 +577,6 @@ internal virtual void NotifyDefaultHandlerFired(Machine machine)
             // Override to implement the notification.
         }
 
-        /// <summary>
-        /// Logs the specified text.
-        /// </summary>
-        protected internal virtual void Log(string format, params object[] args)
-        {
-            this.Logger.WriteLine(format, args);
-        }
-
         /// <summary>
         /// Installs the specified <see cref="ILogger"/>.
         /// </summary>

Source/Core/Runtime/Machines/AsyncMachine.cs

@@ -6,6 +6,8 @@
 using System;
 using System.ComponentModel;
 
+using Microsoft.PSharp.IO;
+
 namespace Microsoft.PSharp.Runtime
 {
     /// <summary>
@@ -31,6 +33,11 @@ public abstract class AsyncMachine
         /// </summary>
         protected internal Guid OperationGroupId { get; set; }
 
+        /// <summary>
+        /// The logger installed to the P# runtime.
+        /// </summary>
+        protected ILogger Logger => this.Runtime.Logger;
+
         /// <summary>
         /// Initializes this machine.
         /// </summary>

Source/Core/Runtime/Machines/Machine.cs

@@ -111,11 +111,6 @@ public abstract class Machine : AsyncMachine
         /// </summary>
         private bool OnExceptionRequestedGracefulHalt;
 
-        /// <summary>
-        /// The logger installed to the P# runtime.
-        /// </summary>
-        protected ILogger Logger => this.Runtime.Logger;
-
         /// <summary>
         /// Gets the <see cref="Type"/> of the current state.
         /// </summary>
@@ -856,14 +851,12 @@ private async Task ExecuteAction(CachedAction cachedAction)
                 if (innerException is ExecutionCanceledException)
                 {
                     this.IsHalted = true;
-                    Debug.WriteLine("<Exception> ExecutionCanceledException was " +
-                        $"thrown from Machine '{this.Id}'.");
+                    Debug.WriteLine($"<Exception> ExecutionCanceledException was thrown from Machine '{this.Id}'.");
                 }
                 else if (innerException is TaskSchedulerException)
                 {
                     this.IsHalted = true;
-                    Debug.WriteLine("<Exception> TaskSchedulerException was " +
-                        $"thrown from Machine '{this.Id}'.");
+                    Debug.WriteLine($"<Exception> TaskSchedulerException was thrown from Machine '{this.Id}'.");
                 }
                 else if (this.OnExceptionRequestedGracefulHalt)
                 {
@@ -1539,7 +1532,7 @@ private bool OnExceptionHandler(string methodName, Exception ex)
         {
             if (ex is ExecutionCanceledException)
             {
-                // internal exception, used by PsharpTester
+                // Internal exception, used during testing.
                 return false;
             }
 

Source/Core/Runtime/Specifications/Monitor.cs

@@ -6,7 +6,6 @@
 using System;
 using System.Collections.Concurrent;
 using System.Collections.Generic;
-using System.Diagnostics;
 using System.Linq;
 using System.Linq.Expressions;
 using System.Reflection;
@@ -195,7 +194,7 @@ protected void Goto(Type s)
         {
             // If the state is not a state of the monitor, then report an error and exit.
             this.Assert(StateTypeMap[this.GetType()].Any(val => val.DeclaringType.Equals(s.DeclaringType) && val.Name.Equals(s.Name)),
-                "Monitor '{0}' is trying to transition to non-existing state '{1}'.", this.Id, s.Name);
+                "Monitor '{0}' is trying to transition to non-existing state '{1}'.", this.GetType().Name, s.Name);
             this.Raise(new GotoStateEvent(s));
         }
 
@@ -297,7 +296,7 @@ private void HandleEvent(Event e)
         /// <summary>
         /// Invokes an action.
         /// </summary>
-        [DebuggerStepThrough]
+        [System.Diagnostics.DebuggerStepThrough]
         private void Do(string actionName)
         {
             MethodInfo action = this.ActionMap[actionName];
@@ -308,7 +307,7 @@ private void Do(string actionName)
         /// <summary>
         /// Executes the on entry function of the current state.
         /// </summary>
-        [DebuggerStepThrough]
+        [System.Diagnostics.DebuggerStepThrough]
         private void ExecuteCurrentStateOnEntry()
         {
             this.Runtime.NotifyEnteredState(this);
@@ -330,7 +329,7 @@ private void ExecuteCurrentStateOnEntry()
         /// <summary>
         /// Executes the on exit function of the current state.
         /// </summary>
-        [DebuggerStepThrough]
+        [System.Diagnostics.DebuggerStepThrough]
         private void ExecuteCurrentStateOnExit(string eventHandlerExitActionName)
         {
             this.Runtime.NotifyExitedState(this);
@@ -360,7 +359,7 @@ private void ExecuteCurrentStateOnExit(string eventHandlerExitActionName)
         /// <summary>
         /// Executes the specified action.
         /// </summary>
-        [DebuggerStepThrough]
+        [System.Diagnostics.DebuggerStepThrough]
         private void ExecuteAction(MethodInfo action)
         {
             try
@@ -598,7 +597,7 @@ internal void InitializeStateInformation()
                         (state.IsCold && !state.IsHot) ||
                         (!state.IsCold && state.IsHot) ||
                         (!state.IsCold && !state.IsHot),
-                        "State '{0}' of monitor '{1}' cannot be both cold and hot.", type.FullName, this.Id);
+                        "State '{0}' of monitor '{1}' cannot be both cold and hot.", type.FullName, this.GetType().Name);
 
                     StateMap[monitorType].Add(state);
                 }
@@ -655,8 +654,8 @@ internal void InitializeStateInformation()
             }
 
             var initialStates = StateMap[monitorType].Where(state => state.IsStart).ToList();
-            this.Assert(initialStates.Count != 0, "Monitor '{0}' must declare a start state.", this.Id);
-            this.Assert(initialStates.Count == 1, "Monitor '{0}' can not declare more than one start states.", this.Id);
+            this.Assert(initialStates.Count != 0, "Monitor '{0}' must declare a start state.", this.GetType().Name);
+            this.Assert(initialStates.Count == 1, "Monitor '{0}' can not declare more than one start states.", this.GetType().Name);
 
             this.ConfigureStateTransitions(initialStates.Single());
             this.State = initialStates.Single();
@@ -750,7 +749,7 @@ private void ReportUnhandledException(Exception ex, string actionName)
         {
             var state = this.CurrentState is null ? "<unknown>" : this.CurrentStateName;
             this.Runtime.WrapAndThrowException(ex, $"Exception '{ex.GetType()}' was thrown " +
-                $"in monitor '{this.Id}', state '{state}', action '{actionName}', " +
+                $"in monitor '{this.GetType().Name}', state '{state}', action '{actionName}', " +
                 $"'{ex.Source}':\n" +
                 $"   {ex.Message}\n" +
                 $"The stack trace is:\n{ex.StackTrace}");
@@ -761,7 +760,7 @@ private void ReportUnhandledException(Exception ex, string actionName)
         /// </summary>
         internal HashSet<string> GetAllStates()
         {
-            this.Assert(StateMap.ContainsKey(this.GetType()), "Monitor '{0}' hasn't populated its states yet.", this.Id);
+            this.Assert(StateMap.ContainsKey(this.GetType()), "Monitor '{0}' hasn't populated its states yet.", this.GetType().Name);
 
             var allStates = new HashSet<string>();
             foreach (var state in StateMap[this.GetType()])
@@ -777,7 +776,7 @@ internal HashSet<string> GetAllStates()
         /// </summary>
         internal HashSet<Tuple<string, string>> GetAllStateEventPairs()
         {
-            this.Assert(StateMap.ContainsKey(this.GetType()), "Monitor '{0}' hasn't populated its states yet.", this.Id);
+            this.Assert(StateMap.ContainsKey(this.GetType()), "Monitor '{0}' hasn't populated its states yet.", this.GetType().Name);
 
             var pairs = new HashSet<Tuple<string, string>>();
             foreach (var state in StateMap[this.GetType()])

Source/Core/Utilities/Profiler.cs

@@ -28,16 +28,16 @@ public void StartMeasuringExecutionTime()
         /// </summary>
         public void StopMeasuringExecutionTime()
         {
-            this.StopWatch.Stop();
+            if (this.StopWatch != null)
+            {
+                this.StopWatch.Stop();
+            }
         }
 
         /// <summary>
         /// Returns profilling results.
         /// </summary>
-        /// <returns>Seconds</returns>
-        public double Results()
-        {
-            return this.StopWatch.Elapsed.TotalSeconds;
-        }
+        public double Results() =>
+            this.StopWatch != null ? this.StopWatch.Elapsed.TotalSeconds : 0;
     }
 }

Source/SharedObjects/SharedCounter/MockSharedCounter.cs

@@ -29,7 +29,7 @@ public MockSharedCounter(int value, SystematicTestingRuntime runtime)
         {
             this.Runtime = runtime;
             this.CounterMachine = this.Runtime.CreateMachine(typeof(SharedCounterMachine));
-            var currentMachine = this.Runtime.GetCurrentMachine();
+            var currentMachine = this.Runtime.GetExecutingMachine<Machine>();
             this.Runtime.SendEvent(this.CounterMachine, SharedCounterEvent.SetEvent(currentMachine.Id, value));
             currentMachine.Receive(typeof(SharedCounterResponseEvent)).Wait();
         }
@@ -55,7 +55,7 @@ public void Decrement()
         /// </summary>
         public int GetValue()
         {
-            var currentMachine = this.Runtime.GetCurrentMachine();
+            var currentMachine = this.Runtime.GetExecutingMachine<Machine>();
             this.Runtime.SendEvent(this.CounterMachine, SharedCounterEvent.GetEvent(currentMachine.Id));
             var response = currentMachine.Receive(typeof(SharedCounterResponseEvent)).Result;
             return (response as SharedCounterResponseEvent).Value;
@@ -66,7 +66,7 @@ public int GetValue()
         /// </summary>
         public int Add(int value)
         {
-            var currentMachine = this.Runtime.GetCurrentMachine();
+            var currentMachine = this.Runtime.GetExecutingMachine<Machine>();
             this.Runtime.SendEvent(this.CounterMachine, SharedCounterEvent.AddEvent(currentMachine.Id, value));
             var response = currentMachine.Receive(typeof(SharedCounterResponseEvent)).Result;
             return (response as SharedCounterResponseEvent).Value;
@@ -77,7 +77,7 @@ public int Add(int value)
         /// </summary>
         public int Exchange(int value)
         {
-            var currentMachine = this.Runtime.GetCurrentMachine();
+            var currentMachine = this.Runtime.GetExecutingMachine<Machine>();
             this.Runtime.SendEvent(this.CounterMachine, SharedCounterEvent.SetEvent(currentMachine.Id, value));
             var response = currentMachine.Receive(typeof(SharedCounterResponseEvent)).Result;
             return (response as SharedCounterResponseEvent).Value;
@@ -88,7 +88,7 @@ public int Exchange(int value)
         /// </summary>
         public int CompareExchange(int value, int comparand)
         {
-            var currentMachine = this.Runtime.GetCurrentMachine();
+            var currentMachine = this.Runtime.GetExecutingMachine<Machine>();
             this.Runtime.SendEvent(this.CounterMachine, SharedCounterEvent.CasEvent(currentMachine.Id, value, comparand));
             var response = currentMachine.Receive(typeof(SharedCounterResponseEvent)).Result;
             return (response as SharedCounterResponseEvent).Value;