From 9feac998b73fb30d3fa1bcdf858e8a1b47466585 Mon Sep 17 00:00:00 2001
From: Kevin Zehrer <103638980+kzdev-net@users.noreply.github.com>
Date: Tue, 30 Jul 2024 15:50:23 -0500
Subject: [PATCH] Added a ResetCache call to the Monitor.SynchronizedBlock
 class to clear out the object/Synchronized block cache. Added an end
 iteration callback registration to the TestingEngine constructor that will
 clear out the Monitor.SynchronizedBlock cache after each iteration to be sure
 no entries carry over across iterations for cases such as the max step bound
 being hit and all controlled operations being abruptly stopped.

---
 Source/Test/Rewriting/Types/Threading/Monitor.cs | 7 +++++++
 Source/Test/SystematicTesting/TestingEngine.cs   | 5 +++++
 2 files changed, 12 insertions(+)

diff --git a/Source/Test/Rewriting/Types/Threading/Monitor.cs b/Source/Test/Rewriting/Types/Threading/Monitor.cs
index bab1dd3bf..4d0a7563e 100644
--- a/Source/Test/Rewriting/Types/Threading/Monitor.cs
+++ b/Source/Test/Rewriting/Types/Threading/Monitor.cs
@@ -429,6 +429,13 @@ private SynchronizedBlock(CoyoteRuntime runtime, object syncObject)
                 this.DebugName = $"lock({this.ResourceId})";
             }
 
+            /// <summary>
+            /// Called to clear out the cache of synchronized blocks in cases where an iteration
+            /// may have been aborted and the cache is no longer valid, and may even hold old
+            /// values that would otherwise not get cleaned up and could impact future iterations.
+            /// </summary>
+            internal static void ResetCache () => Cache.Clear();
+
             /// <summary>
             /// Creates a new <see cref="SynchronizedBlock"/> for synchronizing access
             /// to the specified object and enters the lock.
diff --git a/Source/Test/SystematicTesting/TestingEngine.cs b/Source/Test/SystematicTesting/TestingEngine.cs
index c28441361..3cd574746 100644
--- a/Source/Test/SystematicTesting/TestingEngine.cs
+++ b/Source/Test/SystematicTesting/TestingEngine.cs
@@ -21,6 +21,8 @@
 using Microsoft.Coyote.Telemetry;
 using Microsoft.Coyote.Visualization;
 
+using SynchronizedBlock = Microsoft.Coyote.Rewriting.Types.Threading.Monitor.SynchronizedBlock;
+
 namespace Microsoft.Coyote.SystematicTesting
 {
     /// <summary>
@@ -201,6 +203,9 @@ private TestingEngine(Configuration configuration, TestMethodInfo testMethodInfo
 
             // Create a client for gathering and sending optional telemetry data.
             TelemetryClient = TelemetryClient.GetOrCreate(this.Configuration, this.LogWriter);
+
+            // Register to clean up the Monitor SynchronizedBlock cache.
+            this.RegisterEndIterationCallBack(_ => SynchronizedBlock.ResetCache());
         }
 
         /// <summary>