fixed memory leak in the testing runtime (#213)

Source/Core/Actors/ActorExecutionContext.cs

@@ -797,6 +797,11 @@ namespace Microsoft.Coyote.Actors
         /// </summary>
         internal sealed class Mock : ActorExecutionContext
         {
+            /// <summary>
+            /// Set of all created actor ids.
+            /// </summary>
+            private readonly ConcurrentDictionary<ActorId, byte> ActorIds;
+
             /// <summary>
             /// Map that stores all unique names and their corresponding actor ids.
             /// </summary>
@@ -820,6 +825,7 @@ namespace Microsoft.Coyote.Actors
                 IRandomValueGenerator valueGenerator, LogWriter logWriter)
                 : base(configuration, runtime, specificationEngine, valueGenerator, logWriter)
             {
+                this.ActorIds = new ConcurrentDictionary<ActorId, byte>();
                 this.NameValueToActorId = new ConcurrentDictionary<string, ActorId>();
                 this.ProgramCounterMap = new ConcurrentDictionary<ActorId, int>();
             }
@@ -829,7 +835,9 @@ namespace Microsoft.Coyote.Actors
             {
                 // It is important that all actor ids use the monotonically incrementing
                 // value as the id during testing, and not the unique name.
-                return this.NameValueToActorId.GetOrAdd(name, key => this.CreateActorId(type, key));
+                var id = this.NameValueToActorId.GetOrAdd(name, key => this.CreateActorId(type, key));
+                this.ActorIds.TryAdd(id, 0);
+                return id;
             }
 
             /// <inheritdoc/>
@@ -932,6 +940,7 @@ namespace Microsoft.Coyote.Actors
                 if (id is null)
                 {
                     id = this.CreateActorId(type, name);
+                    this.ActorIds.TryAdd(id, 0);
                 }
                 else
                 {
@@ -1158,8 +1167,7 @@ namespace Microsoft.Coyote.Actors
                             this.ResetProgramCounter(actor);
                         }
 
-                        IODebug.WriteLine("<ScheduleDebug> Completed operation {0} on task '{1}'.", actor.Id, Task.CurrentId);
-                        op.OnCompleted();
+                        this.Runtime.CompleteOperation(op);
 
                         // The actor is inactive or halted, schedule the next enabled operation.
                         this.Runtime.ScheduleNextOperation(AsyncOperationType.Stop);
@@ -1462,6 +1470,13 @@ namespace Microsoft.Coyote.Actors
                 {
                     this.NameValueToActorId.Clear();
                     this.ProgramCounterMap.Clear();
+                    foreach (var id in this.ActorIds)
+                    {
+                        // Unbind the runtime to avoid memory leaks if the user holds the id.
+                        id.Key.Bind(null);
+                    }
+
+                    this.ActorIds.Clear();
                 }
 
                 base.Dispose(disposing);

Source/Core/Actors/ActorId.cs

@@ -12,13 +12,34 @@ namespace Microsoft.Coyote.Actors
     /// Unique actor id.
     /// </summary>
     [DataContract]
+#if !DEBUG
     [DebuggerStepThrough]
+#endif
     public sealed class ActorId : IEquatable<ActorId>, IComparable<ActorId>
     {
+        /// <summary>
+        /// The execution context of the actor with this id.
+        /// </summary>
+        private ActorExecutionContext Context;
+
         /// <summary>
         /// The runtime that executes the actor with this id.
         /// </summary>
-        public IActorRuntime Runtime { get; private set; }
+        public IActorRuntime Runtime
+        {
+            get
+            {
+                if (this.Context == null)
+                {
+#pragma warning disable CA1065 // Do not raise exceptions in unexpected locations
+                    throw new InvalidOperationException($"Cannot use actor id '{this.Name}' of type '{this.Type}' " +
+                        "after the runtime has been disposed.");
+#pragma warning restore CA1065 // Do not raise exceptions in unexpected locations
+                }
+
+                return this.Context;
+            }
+        }
 
         /// <summary>
         /// Unique id, when <see cref="NameValue"/> is empty.
@@ -54,20 +75,20 @@ namespace Microsoft.Coyote.Actors
         /// </summary>
         internal ActorId(Type type, ulong value, string name, ActorExecutionContext context, bool useNameForHashing = false)
         {
-            this.Runtime = context;
+            this.Context = context;
             this.Type = type.FullName;
             this.Value = value;
 
             if (useNameForHashing)
             {
                 this.NameValue = name;
-                this.Runtime.Assert(!string.IsNullOrEmpty(this.NameValue), "The actor name cannot be null when used as id.");
+                this.Context.Assert(!string.IsNullOrEmpty(this.NameValue), "The actor name cannot be null when used as id.");
                 this.Name = this.NameValue;
             }
             else
             {
                 this.NameValue = string.Empty;
-                this.Runtime.Assert(this.Value != ulong.MaxValue, "Detected actor id overflow.");
+                this.Context.Assert(this.Value != ulong.MaxValue, "Detected actor id overflow.");
                 this.Name = string.Format(CultureInfo.InvariantCulture, "{0}({1})",
                     string.IsNullOrEmpty(name) ? this.Type : name, this.Value.ToString());
             }
@@ -78,7 +99,7 @@ namespace Microsoft.Coyote.Actors
         /// </summary>
         internal void Bind(ActorExecutionContext context)
         {
-            this.Runtime = context;
+            this.Context = context;
         }
 
         /// <summary>

Source/Core/IO/Logging/InMemoryLogger.cs

@@ -125,5 +125,18 @@ namespace Microsoft.Coyote.IO
                 return this.Builder.ToString();
             }
         }
+
+        /// <summary>
+        /// Releases the resources used by the logger.
+        /// </summary>
+        protected override void Dispose(bool disposing)
+        {
+            if (disposing)
+            {
+                this.Builder.Clear();
+            }
+
+            base.Dispose(disposing);
+        }
     }
 }

Source/Core/Runtime/CoyoteRuntime.cs

@@ -372,8 +372,7 @@ namespace Microsoft.Coyote.Runtime
                             }
                         }
 
-                        IO.Debug.WriteLine("<ScheduleDebug> Completed operation {0} on task '{1}'.", op.Name, Task.CurrentId);
-                        op.OnCompleted();
+                        this.CompleteOperation(op);
 
                         // Task has completed, schedule the next enabled operation, which terminates exploration.
                         this.ScheduleNextOperation(AsyncOperationType.Stop);
@@ -552,8 +551,7 @@ namespace Microsoft.Coyote.Runtime
             }
             finally
             {
-                IO.Debug.WriteLine("<ScheduleDebug> Completed operation '{0}' on task '{1}'.", op.Name, Task.CurrentId);
-                op.OnCompleted();
+                this.CompleteOperation(op);
 
                 // Set the result task completion source to notify to the awaiters that the operation
                 // has been completed, and schedule the next enabled operation.
@@ -666,8 +664,7 @@ namespace Microsoft.Coyote.Runtime
             }
             finally
             {
-                IO.Debug.WriteLine("<ScheduleDebug> Completed operation '{0}' on task '{1}'.", op.Name, Task.CurrentId);
-                op.OnCompleted();
+                this.CompleteOperation(op);
 
                 // Set the result task completion source to notify to the awaiters that the operation
                 // has been completed, and schedule the next enabled operation.
@@ -1494,6 +1491,16 @@ namespace Microsoft.Coyote.Runtime
             this.ThrowExecutionCanceledExceptionIfDetached();
         }
 
+        internal void CompleteOperation(AsyncOperation op)
+        {
+            lock (this.SyncObject)
+            {
+                IO.Debug.WriteLine("<ScheduleDebug> Completed the operation of '{0}' on task '{1}'.", op.Name, Task.CurrentId);
+                op.Status = AsyncOperationStatus.Completed;
+                ExecutingOperation.Value = null;
+            }
+        }
+
         /// <summary>
         /// Tries to enable the specified operation.
         /// </summary>
@@ -2202,8 +2209,12 @@ namespace Microsoft.Coyote.Runtime
             if (disposing)
             {
                 this.OperationIdCounter = 0;
+                this.OperationMap.Clear();
+                this.TaskMap.Clear();
+
                 this.DefaultActorExecutionContext.Dispose();
                 this.SpecificationEngine.Dispose();
+                this.ScheduleTrace.Dispose();
 
                 if (this.SchedulingPolicy is SchedulingPolicy.Systematic)
                 {

Source/Core/Runtime/Operations/AsyncOperation.cs

@@ -48,14 +48,6 @@ namespace Microsoft.Coyote.Runtime
             this.Type = AsyncOperationType.Start;
         }
 
-        /// <summary>
-        /// Invoked when the operation completes.
-        /// </summary>
-        internal virtual void OnCompleted()
-        {
-            this.Status = AsyncOperationStatus.Completed;
-        }
-
         /// <summary>
         /// Tries to enable the operation, if it is not already enabled.
         /// </summary>

Source/Core/Runtime/Scheduling/OperationScheduler.cs

@@ -85,6 +85,12 @@ namespace Microsoft.Coyote.Runtime
                     this.ReplayStrategy = replayStrategy;
                     this.IsReplayingSchedule = true;
                 }
+
+                // Wrap the strategy inside a liveness checking strategy.
+                if (this.Configuration.IsLivenessCheckingEnabled)
+                {
+                    this.Strategy = new TemperatureCheckingStrategy(this.Configuration, this.Strategy as SystematicStrategy);
+                }
             }
             else if (this.SchedulingPolicy is SchedulingPolicy.Fuzzing)
             {
@@ -102,11 +108,9 @@ namespace Microsoft.Coyote.Runtime
         /// </summary>
         internal void SetSpecificationEngine(SpecificationEngine specificationEngine)
         {
-            if (this.SchedulingPolicy is SchedulingPolicy.Systematic &&
-                this.Configuration.IsLivenessCheckingEnabled)
+            if (this.Strategy is TemperatureCheckingStrategy temperatureCheckingStrategy)
             {
-                this.Strategy = new TemperatureCheckingStrategy(this.Configuration, specificationEngine,
-                    this.Strategy as SystematicStrategy);
+                temperatureCheckingStrategy.SetSpecificationEngine(specificationEngine);
             }
         }
 

Source/Core/Testing/Systematic/LivenessCheckingStrategy.cs

@@ -15,26 +15,19 @@ namespace Microsoft.Coyote.Testing.Systematic
         /// <summary>
         /// The configuration.
         /// </summary>
-        protected Configuration Configuration;
-
-        /// <summary>
-        /// Responsible for checking specifications.
-        /// </summary>
-        protected SpecificationEngine SpecificationEngine;
+        protected readonly Configuration Configuration;
 
         /// <summary>
         /// Strategy used for scheduling decisions.
         /// </summary>
-        protected SystematicStrategy SchedulingStrategy;
+        protected readonly SystematicStrategy SchedulingStrategy;
 
         /// <summary>
         /// Initializes a new instance of the <see cref="LivenessCheckingStrategy"/> class.
         /// </summary>
-        internal LivenessCheckingStrategy(Configuration configuration, SpecificationEngine specificationEngine,
-            SystematicStrategy strategy)
+        internal LivenessCheckingStrategy(Configuration configuration, SystematicStrategy strategy)
         {
             this.Configuration = configuration;
-            this.SpecificationEngine = specificationEngine;
             this.SchedulingStrategy = strategy;
         }
 

Source/Core/Testing/Systematic/TemperatureCheckingStrategy.cs

@@ -15,22 +15,34 @@ namespace Microsoft.Coyote.Testing.Systematic
     /// </summary>
     internal sealed class TemperatureCheckingStrategy : LivenessCheckingStrategy
     {
+        /// <summary>
+        /// Responsible for checking specifications.
+        /// </summary>
+        private SpecificationEngine SpecificationEngine;
+
         /// <summary>
         /// Initializes a new instance of the <see cref="TemperatureCheckingStrategy"/> class.
         /// </summary>
-        internal TemperatureCheckingStrategy(Configuration configuration, SpecificationEngine specificationEngine,
-            SystematicStrategy strategy)
-            : base(configuration, specificationEngine, strategy)
+        internal TemperatureCheckingStrategy(Configuration configuration, SystematicStrategy strategy)
+            : base(configuration, strategy)
         {
         }
 
+        /// <summary>
+        /// Sets the specification engine.
+        /// </summary>
+        internal void SetSpecificationEngine(SpecificationEngine specificationEngine)
+        {
+            this.SpecificationEngine = specificationEngine;
+        }
+
         /// <inheritdoc/>
         internal override bool GetNextOperation(IEnumerable<AsyncOperation> ops, AsyncOperation current,
             bool isYielding, out AsyncOperation next)
         {
             if (this.IsFair())
             {
-                this.SpecificationEngine.CheckLivenessThresholdExceeded();
+                this.SpecificationEngine?.CheckLivenessThresholdExceeded();
             }
 
             return this.SchedulingStrategy.GetNextOperation(ops, current, isYielding, out next);
@@ -41,7 +53,7 @@ namespace Microsoft.Coyote.Testing.Systematic
         {
             if (this.IsFair())
             {
-                this.SpecificationEngine.CheckLivenessThresholdExceeded();
+                this.SpecificationEngine?.CheckLivenessThresholdExceeded();
             }
 
             return this.SchedulingStrategy.GetNextBooleanChoice(current, maxValue, out next);
@@ -52,7 +64,7 @@ namespace Microsoft.Coyote.Testing.Systematic
         {
             if (this.IsFair())
             {
-                this.SpecificationEngine.CheckLivenessThresholdExceeded();
+                this.SpecificationEngine?.CheckLivenessThresholdExceeded();
             }
 
             return this.SchedulingStrategy.GetNextIntegerChoice(current, maxValue, out next);

Source/Core/Testing/Traces/ScheduleTrace.cs

@@ -13,7 +13,7 @@ namespace Microsoft.Coyote.Testing
     /// Class implementing a program schedule trace. A trace is a series
     /// of transitions from some initial state to some end state.
     /// </summary>
-    internal sealed class ScheduleTrace : IEnumerable, IEnumerable<ScheduleStep>
+    internal sealed class ScheduleTrace : IEnumerable, IEnumerable<ScheduleStep>, IDisposable
     {
         /// <summary>
         /// The steps of the schedule trace.
@@ -258,5 +258,13 @@ namespace Microsoft.Coyote.Testing
 
             return new ScheduleTrace(scheduleDump);
         }
+
+        /// <summary>
+        /// Disposes the schedule trace.
+        /// </summary>
+        public void Dispose()
+        {
+            this.Steps.Clear();
+        }
     }
 }

Source/Test/SystematicTesting/TestMethodInfo.cs

@@ -243,15 +243,40 @@ namespace Microsoft.Coyote.SystematicTesting
                     $"'{attribute.FullName}'. '{testMethods.Count}' test methods were found instead.");
             }
 
-            if (testMethods[0].ReturnType != typeof(void) ||
-                testMethods[0].ContainsGenericParameters ||
-                testMethods[0].IsAbstract || testMethods[0].IsVirtual ||
-                testMethods[0].IsConstructor ||
-                !testMethods[0].IsPublic || !testMethods[0].IsStatic ||
-                testMethods[0].GetParameters().Length != 0)
+            string error = null;
+            if (testMethods[0].ReturnType != typeof(void))
             {
-                throw new InvalidOperationException("Incorrect test method declaration. Please " +
-                    "declare the test method as follows:\n" +
+                error = "The test method return type is not void.";
+            }
+            else if (testMethods[0].IsGenericMethod)
+            {
+                error = "The test method is generic.";
+            }
+            else if (testMethods[0].ContainsGenericParameters)
+            {
+                error = "The test method inherits generic parameters which is not supported.";
+            }
+            else if (testMethods[0].IsAbstract)
+            {
+                error = "The test method is abstract.";
+            }
+            else if (testMethods[0].IsVirtual)
+            {
+                error = "The test method is virtual.";
+            }
+            else if (testMethods[0].IsConstructor)
+            {
+                error = "The test method is a constructor.";
+            }
+            else if (testMethods[0].GetParameters().Length != 0)
+            {
+                error = "The test method has unexpected parameters.";
+            }
+
+            if (error != null)
+            {
+                throw new InvalidOperationException(error + " Please " +
+                    "declare it as follows:\n" +
                     $"  [{attribute.FullName}] public static void " +
                     $"{testMethods[0].Name}() {{ ... }}");
             }

Source/Test/SystematicTesting/TestingEngine.cs

@@ -576,6 +576,7 @@ namespace Microsoft.Coyote.SystematicTesting
                 }
 
                 // Cleans up the runtime before the next iteration starts.
+                runtimeLogger?.Close();
                 runtimeLogger?.Dispose();
                 runtime?.Dispose();
             }

Tests/Tests.Actors.BugFinding/GC/FinalizerTests.cs

@@ -0,0 +1,114 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Threading.Tasks;
+using Microsoft.Coyote.Runtime;
+using Microsoft.Coyote.SystematicTesting;
+using Xunit;
+using Xunit.Abstractions;
+
+namespace Microsoft.Coyote.Actors.BugFinding.Tests
+{
+    public class FinalizerTests : BaseActorBugFindingTest
+    {
+        public FinalizerTests(ITestOutputHelper output)
+            : base(output)
+        {
+        }
+
+        private class GCTracker
+        {
+            internal bool IsFinalized;
+        }
+
+        private class SetupEvent : Event
+        {
+            internal readonly GCTracker Tracker;
+
+            internal SetupEvent(GCTracker tracker)
+            {
+                this.Tracker = tracker;
+            }
+        }
+
+        public class A : Actor
+        {
+            private GCTracker Tracker;
+
+            protected override Task OnInitializeAsync(Event initialEvent)
+            {
+                this.Tracker = (initialEvent as SetupEvent).Tracker;
+                return Task.CompletedTask;
+            }
+
+            ~A()
+            {
+                this.Tracker.IsFinalized = true;
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestActorFinalizerInvoked()
+        {
+            var tracker = new GCTracker();
+
+            var config = this.GetConfiguration().WithTestingIterations(2);
+            TestingEngine engine = TestingEngine.Create(config, (IActorRuntime r) =>
+            {
+                var setup = new SetupEvent(tracker);
+                r.CreateActor(typeof(A), setup);
+            });
+
+            engine.Run();
+
+            // Force a full GC.
+            GC.Collect(2);
+            GC.WaitForFullGCComplete();
+            GC.WaitForPendingFinalizers();
+            Assert.True(tracker.IsFinalized, "Finalizer was not called.");
+        }
+
+        public class M : StateMachine
+        {
+            private GCTracker Tracker;
+
+            [Start]
+            [OnEntry(nameof(InitOnEntry))]
+            public class Init : State
+            {
+            }
+
+            private void InitOnEntry(Event e)
+            {
+                this.Tracker = (e as SetupEvent).Tracker;
+            }
+
+            ~M()
+            {
+                this.Tracker.IsFinalized = true;
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestStateMachineFinalizerInvoked()
+        {
+            var tracker = new GCTracker();
+
+            var config = this.GetConfiguration().WithTestingIterations(2);
+            TestingEngine engine = TestingEngine.Create(config, (IActorRuntime r) =>
+            {
+                var setup = new SetupEvent(tracker);
+                r.CreateActor(typeof(M), setup);
+            });
+
+            engine.Run();
+
+            // Force a full GC.
+            GC.Collect(2);
+            GC.WaitForFullGCComplete();
+            GC.WaitForPendingFinalizers();
+            Assert.True(tracker.IsFinalized, "Finalizer was not called.");
+        }
+    }
+}

Tests/Tests.Actors/GC/MemoryLeakTests.cs

@@ -7,7 +7,7 @@ using System.Threading.Tasks;
 using Xunit;
 using Xunit.Abstractions;
 
-namespace Microsoft.Coyote.Actors.Tests.StateMachines
+namespace Microsoft.Coyote.Actors.Tests
 {
     public class MemoryLeakTests : BaseActorTest
     {

global.json

@@ -1,5 +1,5 @@
 {
   "sdk": {
-    "version": "5.0.301"
+    "version": "5.0.302"
   }
 }