Using --memlimit to forbid OOMs

Fix in theta-start.sh Reverted theta-start.sh Updated theta-start.sh
ftsrg · Nov 14, 2024 · cf0967c · cf0967c
1 parent 2447102
commit cf0967c
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 2 deletions.
diff --git a/scripts/theta-start.sh b/scripts/theta-start.sh
@@ -34,7 +34,7 @@ remove_property() {
 }
 
 if [ "$1" == "--version" ]; then
-    LD_LIBRARY_PATH=$scriptdir/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar --version
+    LD_LIBRARY_PATH=$scriptdir/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar --version || echo $VERIFIER_VERSION
 else
     modified_args=$(remove_property "${@:2}")
     property=$(cat .property && rm .property)

diff --git a/...ojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt b/...ojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt
@@ -77,12 +77,16 @@ class InProcessChecker<F : SpecFrontendConfig, B : SpecBackendConfig>(
         getGson(xcfa).toJson(processConfig)
       }
 
+    val heapSize =
+      "-Xmx${if(config.backendConfig.memlimit == 0L) 1420L else config.backendConfig.memlimit/1024/1024 }m"
+    logger.write(Logger.Level.INFO, "Starting process with $heapSize of heap\n")
+
     val pb =
       NuProcessBuilder(
         listOf(
             ProcessHandle.current().info().command().orElse("java"),
             "-Xss120m",
-            "-Xmx14210m",
+            heapSize,
             "-cp",
             File(XcfaCli::class.java.protectionDomain.codeSource.location.toURI()).absolutePath,
             XcfaCli::class.qualifiedName,

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
@@ -179,6 +179,11 @@ data class BackendConfig<T : SpecBackendConfig>(
   var timeoutMs: Long = 0,
   @Parameter(names = ["--in-process"], description = "Run analysis in process")
   var inProcess: Boolean = false,
+  @Parameter(
+    names = ["--memlimit"],
+    description = "Maximum memory to use when --in-process (in bytes, 0 for default)",
+  )
+  var memlimit: Long = 0L,
   override var specConfig: T? = null,
 ) : SpecializableConfig<T> {
 

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt
@@ -59,6 +59,7 @@ fun boundedPortfolio25(
       backendConfig =
         BackendConfig(
           backend = Backend.BOUNDED,
+          memlimit = portfolioConfig.backendConfig.memlimit,
           solverHome = portfolioConfig.backendConfig.solverHome,
           timeoutMs = 0,
           specConfig =
@@ -93,6 +94,7 @@ fun boundedPortfolio25(
       backendConfig =
         BackendConfig(
           backend = Backend.MDD,
+          memlimit = portfolioConfig.backendConfig.memlimit,
           solverHome = portfolioConfig.backendConfig.solverHome,
           timeoutMs = 0,
           specConfig =