[C# backend] Enforce memory limit

Track memory usage and enforce memory limit using CLI option --memout <double>
p-org · May 20, 2024 · e30dd73 · e30dd73
1 parent 43a9803
commit e30dd73
Show file tree

Hide file tree

Showing 4 changed files with 54 additions and 18 deletions.
diff --git a/Src/PChecker/CheckerCore/Scheduling/TestingProcessScheduler.cs b/Src/PChecker/CheckerCore/Scheduling/TestingProcessScheduler.cs
@@ -172,7 +172,7 @@ private void EmitTestReport()
             }
 
             Console.WriteLine(GlobalTestReport.GetText(_checkerConfiguration, "..."));
-            Console.WriteLine($"... Elapsed {Profiler.Results()} sec.");
+            Console.WriteLine($"... Elapsed {Profiler.GetElapsedTime():0.##} sec and used {Profiler.GetMaxMemoryUsage():0.##} GB.");
 
             if (GlobalTestReport.InternalErrors.Count > 0)
             {

diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs
@@ -362,20 +362,28 @@ public void Run()
             }
             catch (AggregateException aex)
             {
-                aex.Handle((ex) =>
+                if (aex.InnerException is OutOfMemoryException)
                 {
-                    Debug.WriteLine(ex.Message);
-                    Debug.WriteLine(ex.StackTrace);
-                    return true;
-                });
-
-                if (aex.InnerException is FileNotFoundException)
-                {
-                    Error.ReportAndExit($"{aex.InnerException.Message}");
+                    Logger.WriteLine("... Checker ran out of memory.");
                 }
+                else
+                {
+                    aex.Handle((ex) =>
+                    {
+                        Debug.WriteLine(ex.Message);
+                        Debug.WriteLine(ex.StackTrace);
+                        return true;
+                    });
+
+                    if (aex.InnerException is FileNotFoundException)
+                    {
+                        Error.ReportAndExit($"{aex.InnerException.Message}");
+                    }
 
-                Error.ReportAndExit("Exception thrown during testing outside the context of an actor, " +
-                                    "possibly in a test method. Please use /debug /v:2 to print more information.");
+
+                    Error.ReportAndExit("Exception thrown during testing outside the context of an actor, " +
+                                        "possibly in a test method. Please use /debug /v:2 to print more information.");
+                }
             }
             catch (Exception ex)
             {
@@ -422,11 +430,17 @@ _checkerConfiguration.SchedulingStrategy is "probabilistic" ||
                             break;
                         }
 
+                        if (Profiler.GetCurrentMemoryUsage() > _checkerConfiguration.MemoryLimit)
+                        {
+                            throw new OutOfMemoryException();
+                        }
+
                         // Runs a new testing schedule.
                         RunNextIteration(i);
 
                         if (IsReplayModeEnabled || (!_checkerConfiguration.PerformFullExploration &&
-                                                    TestReport.NumOfFoundBugs > 0) || !Strategy.PrepareForNextIteration())
+                                                    TestReport.NumOfFoundBugs > 0) ||
+                            !Strategy.PrepareForNextIteration())
                         {
                             break;
                         }
@@ -620,7 +634,7 @@ public string GetReport()
                 report.AppendFormat("... Reproduced {0} bug{1}.", TestReport.NumOfFoundBugs,
                     TestReport.NumOfFoundBugs == 1 ? string.Empty : "s");
                 report.AppendLine();
-                report.Append($"... Elapsed {Profiler.Results()} sec.");
+                report.Append($"... Elapsed {Profiler.GetElapsedTime():0.##} sec and used {Profiler.GetMaxMemoryUsage():0.##} GB.");
                 return report.ToString();
             }
 
@@ -744,7 +758,7 @@ public void TryEmitTraces(string directory, string file)
                 }
             }
 
-            Logger.WriteLine($"... Elapsed {Profiler.Results()} sec.");
+            Logger.WriteLine($"... Elapsed {Profiler.GetElapsedTime():0.##} sec and used {Profiler.GetMaxMemoryUsage():0.##} GB.");
         }
 
         /// <summary>

diff --git a/Src/PChecker/CheckerCore/Utilities/Profiler.cs b/Src/PChecker/CheckerCore/Utilities/Profiler.cs
@@ -1,7 +1,9 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
+using System;
 using System.Diagnostics;
+using PChecker.IO.Logging;
 
 namespace PChecker.Utilities
 {
@@ -11,6 +13,7 @@ namespace PChecker.Utilities
     public class Profiler
     {
         private Stopwatch StopWatch;
+        private static double maxMemoryUsed = 0.0;
 
         /// <summary>
         /// Starts measuring execution time.
@@ -33,9 +36,28 @@ public void StopMeasuringExecutionTime()
         }
 
         /// <summary>
-        /// Returns profilling results.
+        /// Returns profiling results.
         /// </summary>
-        public double Results() =>
+        public double GetElapsedTime() =>
             StopWatch != null ? StopWatch.Elapsed.TotalSeconds : 0;
+
+        /// <summary>
+        /// Get memory usage in gigabytes.
+        /// </summary>
+        public double GetCurrentMemoryUsage()
+        {
+            double memUsed = GC.GetTotalMemory(false) / 1024.0 / 1024.0 / 1024.0;
+            if (memUsed > maxMemoryUsed)
+                maxMemoryUsed = memUsed;
+            return memUsed;
+        }
+
+        /// <summary>
+        /// Get max memory usage in gigabytes.
+        /// </summary>
+        public static double GetMaxMemoryUsage()
+        {
+            return maxMemoryUsed;
+        }
     }
 }
diff --git a/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs b/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs
@@ -40,7 +40,7 @@ internal PCheckerOptions()
 
             var basicGroup = Parser.GetOrCreateGroup("Basic", "Basic options");
             basicGroup.AddArgument("timeout", "t", "Timeout in seconds (disabled by default)", typeof(uint));
-            basicGroup.AddArgument("memout", null, "Memory limit in Giga bytes (disabled by default)", typeof(double)).IsHidden = true;
+            basicGroup.AddArgument("memout", "m", "Memory limit in Giga bytes (disabled by default)", typeof(double));
             basicGroup.AddArgument("outdir", "o", "Dump output to directory (absolute or relative path)");
             basicGroup.AddArgument("verbose", "v", "Enable verbose log output during exploration", typeof(bool));
             basicGroup.AddArgument("debug", "d", "Enable debugging", typeof(bool)).IsHidden = true;