Merged PR 2754: fixed a bug in the task testing runtime

Source/Core/SystematicTesting/ControlledRuntime.cs

@@ -8,6 +8,7 @@ using System.Diagnostics;
 using System.Globalization;
 using System.Linq;
 using System.Reflection;
+using System.Runtime.ExceptionServices;
 using System.Threading.Tasks;
 using Microsoft.Coyote.Actors;
 using Microsoft.Coyote.Actors.Mocks;
@@ -159,7 +160,7 @@ namespace Microsoft.Coyote.SystematicTesting
             var op = new TaskOperation(operationId, this.Scheduler);
             this.Scheduler.RegisterOperation(op);
 
-            Task task = new Task(async () =>
+            Task task = new Task(() =>
             {
                 try
                 {
@@ -169,6 +170,7 @@ namespace Microsoft.Coyote.SystematicTesting
 
                     this.Scheduler.StartOperation(op);
 
+                    Task resultTask = null;
                     if (testMethod is Action<IActorRuntime> actionWithRuntime)
                     {
                         actionWithRuntime(this);
@@ -179,29 +181,34 @@ namespace Microsoft.Coyote.SystematicTesting
                     }
                     else if (testMethod is Func<IActorRuntime, Task> functionWithRuntime)
                     {
-                        Task resultTask = functionWithRuntime(this);
-                        op.OnWaitTask(resultTask);
-                        await resultTask;
+                        resultTask = functionWithRuntime(this);
                     }
                     else if (testMethod is Func<Task> function)
                     {
-                        Task resultTask = function();
-                        op.OnWaitTask(resultTask);
-                        await resultTask;
+                        resultTask = function();
                     }
                     else if (testMethod is Func<IActorRuntime, CoyoteTasks.Task> functionWithRuntime2)
                     {
-                        await functionWithRuntime2(this);
+                        resultTask = functionWithRuntime2(this).UncontrolledTask;
                     }
                     else if (testMethod is Func<CoyoteTasks.Task> function2)
                     {
-                        await function2();
+                        resultTask = function2().UncontrolledTask;
                     }
                     else
                     {
                         throw new InvalidOperationException($"Unsupported test delegate of type '{testMethod.GetType()}'.");
                     }
 
+                    if (resultTask != null)
+                    {
+                        op.OnWaitTask(resultTask);
+                        if (resultTask.Exception != null)
+                        {
+                            ExceptionDispatchInfo.Capture(resultTask.Exception).Throw();
+                        }
+                    }
+
                     IO.Debug.WriteLine("<ScheduleDebug> Completed operation {0} on task '{1}'.", op.Name, Task.CurrentId);
                     op.OnCompleted();
 
@@ -519,35 +526,35 @@ namespace Microsoft.Coyote.SystematicTesting
         /// </summary>
         private void ProcessUnhandledExceptionInOperation(AsyncOperation op, Exception ex)
         {
-            Exception innerException = ex;
-            while (innerException is TargetInvocationException)
+            Exception exception = ex;
+            while (exception is TargetInvocationException)
             {
-                innerException = innerException.InnerException;
+                exception = exception.InnerException;
             }
 
-            if (innerException is AggregateException)
+            if (exception is AggregateException)
             {
-                innerException = innerException.InnerException;
+                exception = exception.InnerException;
             }
 
-            if (innerException is ExecutionCanceledException || innerException is TaskSchedulerException)
+            if (exception is ExecutionCanceledException || exception is TaskSchedulerException)
             {
                 IO.Debug.WriteLine("<Exception> {0} was thrown from operation '{1}'.",
-                    innerException.GetType().Name, op.Name);
+                    exception.GetType().Name, op.Name);
             }
-            else if (innerException is ObjectDisposedException)
+            else if (exception is ObjectDisposedException)
             {
                 IO.Debug.WriteLine("<Exception> {0} was thrown from operation '{1}' with reason '{2}'.",
-                    innerException.GetType().Name, op.Name, ex.Message);
+                    exception.GetType().Name, op.Name, ex.Message);
             }
             else
             {
                 // Report the unhandled exception.
                 string message = string.Format(CultureInfo.InvariantCulture,
-                    $"Exception '{ex.GetType()}' was thrown in operation {op.Name}, " +
-                    $"'{ex.Source}':\n" +
-                    $"   {ex.Message}\n" +
-                    $"The stack trace is:\n{ex.StackTrace}");
+                    $"Exception '{exception.GetType()}' was thrown in operation {op.Name}, " +
+                    $"'{exception.Source}':\n" +
+                    $"   {exception.Message}\n" +
+                    $"The stack trace is:\n{exception.StackTrace}");
                 this.Scheduler.NotifyAssertionFailure(message, killTasks: true, cancelExecution: false);
             }
         }

Source/Core/SystematicTesting/TaskController.cs

@@ -979,24 +979,28 @@ namespace Microsoft.Coyote.SystematicTesting
         private static bool IsCurrentOperationExecutingAsynchronously()
         {
             StackTrace st = new StackTrace(false);
+            bool result = false;
             for (int i = 0; i < st.FrameCount; i++)
             {
                 // Traverse the stack trace to find if the current operation is executing an asynchronous state machine.
                 MethodBase method = st.GetFrame(i).GetMethod();
-                if (typeof(SystemCompiler.IAsyncStateMachine).IsAssignableFrom(method.DeclaringType) && method.Name is "MoveNext")
-                {
-                    // The operation is executing the `MoveNext` of an asynchronous state machine.
-                    return true;
-                }
-                else if (method.DeclaringType == typeof(SystemCompiler.AsyncVoidMethodBuilder) &&
+                if (method.DeclaringType == typeof(SystemCompiler.AsyncVoidMethodBuilder) &&
                     (method.Name is "AwaitOnCompleted" || method.Name is "AwaitUnsafeOnCompleted"))
                 {
                     // The operation is executing the root of an async void method, so we need to inline.
-                    return false;
+                    break;
+                }
+                else if (method.Name is "MoveNext" &&
+                    method.DeclaringType.Namespace != typeof(ControlledRuntime).Namespace &&
+                    typeof(SystemCompiler.IAsyncStateMachine).IsAssignableFrom(method.DeclaringType))
+                {
+                    // The operation is executing the `MoveNext` of an asynchronous state machine.
+                    result = true;
+                    break;
                 }
             }
 
-            return false;
+            return result;
         }
 
         /// <summary>

Tests/Production.Tests/Tasks/Scheduling/AsyncCallStackTests.cs

@@ -2,7 +2,6 @@
 // Licensed under the MIT License.
 
 using System.Diagnostics;
-
 #if BINARY_REWRITE
 using System.Threading.Tasks;
 #else
@@ -41,8 +40,7 @@ namespace Microsoft.Coyote.Production.Tests.Tasks
                         frameCount = st.FrameCount;
                     }
 
-                    Specification.Assert(st.FrameCount <= frameCount,
-                        $"Async call stack size increased from {frameCount} to {st.FrameCount} in iteration {i}.");
+                    Specification.Assert(st.FrameCount < frameCount + 5, $"Call stack size of {st.FrameCount} in iteration {i}.");
                 }
             },
             configuration: GetConfiguration());

Tests/Production.Tests/Tasks/TaskInterleavingsTests.cs

@@ -1,6 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
+using System;
 using System.Collections.Generic;
 #if BINARY_REWRITE
 using System.Threading.Tasks;
@@ -190,7 +191,34 @@ namespace Microsoft.Coyote.Production.Tests.Tasks
         public void TestExploreAllInterleavings()
         {
             SortedSet<string> results = new SortedSet<string>();
-            bool found = false;
+
+            string success = "Explored interleavings.";
+            this.TestWithError(async (runtime) =>
+            {
+                InMemoryLogger log = new InMemoryLogger();
+
+                Task task1 = Task.Run(async () =>
+                {
+                    log.WriteLine(">foo");
+                    await Task.Delay(runtime.RandomInteger(10));
+                    log.WriteLine("<foo");
+                });
+
+                Task task2 = Task.Run(async () =>
+                {
+                    log.WriteLine(">bar");
+                    await Task.Delay(runtime.RandomInteger(10));
+                    log.WriteLine("<bar");
+                });
+
+                await Task.WhenAll(task1, task2);
+
+                results.Add(log.ToString());
+                Specification.Assert(results.Count < 6, success);
+            },
+            configuration: GetConfiguration().WithTestingIterations(1000),
+            expectedError: success);
+
             string expected = @">bar
 <bar
 >foo
@@ -222,41 +250,9 @@ namespace Microsoft.Coyote.Production.Tests.Tasks
 <bar
 ";
             expected = expected.NormalizeNewLines();
-            var success = "Found all interleavings";
 
-            this.TestWithError(async (runtime) =>
-            {
-                if (!found)
-                {
-                    InMemoryLogger log = new InMemoryLogger();
-
-                    Task task1 = Task.Run(async () =>
-                    {
-                        log.WriteLine(">foo");
-                        await Task.Delay(runtime.RandomInteger(10));
-                        log.WriteLine("<foo");
-                    });
-
-                    Task task2 = Task.Run(async () =>
-                    {
-                        log.WriteLine(">bar");
-                        await Task.Delay(runtime.RandomInteger(10));
-                        log.WriteLine("<bar");
-                    });
-
-                    await Task.WhenAll(task1, task2);
-
-                    results.Add(log.ToString());
-
-                    var temp = string.Join("\n", results).NormalizeNewLines();
-                    if (expected == temp)
-                    {
-                        throw new System.Exception(success);
-                    }
-                }
-            },
-            configuration: GetConfiguration().WithTestingIterations(1000).WithPCTStrategy(true),
-            errorChecker: (e) => e.Contains(success));
+            string actual = string.Join("\n", results).NormalizeNewLines();
+            Assert.Equal(expected, actual);
         }
     }
 }

Tests/SystematicTesting.Tests/Runtime/ThrowExceptionFromEntryPointTests.cs

@@ -3,6 +3,7 @@
 
 using System;
 using Microsoft.Coyote.Actors;
+using Microsoft.Coyote.Tasks;
 using Xunit;
 using Xunit.Abstractions;
 
@@ -24,7 +25,28 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Runtime
         }
 
         [Fact(Timeout = 5000)]
-        public void TestThrowExceptionTestFromEntryPoint()
+        public void TestThrowExceptionFromEntryPoint()
+        {
+            this.TestWithException<InvalidOperationException>(r =>
+            {
+                throw new InvalidOperationException();
+            },
+            replay: true);
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestThrowExceptionFromAsyncEntryPoint()
+        {
+            this.TestWithException<InvalidOperationException>(async r =>
+            {
+                await Task.CompletedTask;
+                throw new InvalidOperationException();
+            },
+            replay: true);
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestThrowExceptionFromEntryPointWithActor()
         {
             this.TestWithException<InvalidOperationException>(r =>
             {
@@ -33,15 +55,5 @@ namespace Microsoft.Coyote.SystematicTesting.Tests.Runtime
             },
             replay: true);
         }
-
-        [Fact(Timeout = 5000)]
-        public void TestThrowExceptionTestFromEntryPointNoMachines()
-        {
-            this.TestWithException<InvalidOperationException>(r =>
-            {
-                throw new InvalidOperationException();
-            },
-            replay: true);
-        }
     }
 }