From 0696d2e7768c2256f8ff60f6f03dd152a785e654 Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <tlaplus.net@lemmster.de>
Date: Tue, 24 Mar 2020 16:46:27 -0700
Subject: [PATCH] Fall back to conservative memory allocation if LiveWorker
runs into OutOfMemoryError. If conservative allocation succeeds, liveness
checking will be slow.
[Feature][Bug]
---
.../src/tlc2/tool/liveness/LiveWorker.java | 45 ++++++++++++-------
.../tlc2/util/SynchronousDiskIntStack.java | 2 +-
2 files changed, 30 insertions(+), 17 deletions(-)
diff --git a/tlatools/src/tlc2/tool/liveness/LiveWorker.java b/tlatools/src/tlc2/tool/liveness/LiveWorker.java
index e62ea5068..21f23c196 100644
--- a/tlatools/src/tlc2/tool/liveness/LiveWorker.java
+++ b/tlatools/src/tlc2/tool/liveness/LiveWorker.java
@@ -477,24 +477,37 @@ public class LiveWorker implements Callable<Boolean> {
// memory. Also take the total number of simultaneously running
// workers into account that have to share the available memory
// among each other.
- final double freeMemoryInBytes = (Runtime.getRuntime().freeMemory() / (numWorkers * 1d));
- final long graphSizeInBytes = this.dg.getSizeOnDisk();
- final double ratio = graphSizeInBytes / freeMemoryInBytes;
- if (ratio > TLCGlobals.livenessGraphSizeThreshold) {
- // Double SDIS's bufSize/pageSize by how much the graph size
- // overshoots the free memory size, but limit page size to 1gb.
- // Also, don't allocate more than what is available.
- final int capacityInBytes = SynchronousDiskIntStack.BufSize << Math.min((int) ratio, 5);
- if (capacityInBytes < freeMemoryInBytes) {
- return new SynchronousDiskIntStack(metaDir, name, capacityInBytes);
- } else {
- // Use default SDIS which is 32mb of in-memory size
- return new SynchronousDiskIntStack(metaDir, name);
+ try {
+ final double freeMemoryInBytes = (Runtime.getRuntime().freeMemory() / (numWorkers * 1d));
+ final long graphSizeInBytes = this.dg.getSizeOnDisk();
+ final double ratio = graphSizeInBytes / freeMemoryInBytes;
+ if (ratio > TLCGlobals.livenessGraphSizeThreshold) {
+ // Double SDIS's bufSize/pageSize by how much the graph size
+ // overshoots the free memory size, but limit page size to 1gb.
+ // Also, don't allocate more than what is available.
+ final int capacityInBytes = SynchronousDiskIntStack.BufSize << Math.min((int) ratio, 5);
+ if (capacityInBytes < freeMemoryInBytes) {
+ return new SynchronousDiskIntStack(metaDir, name, capacityInBytes);
+ } else {
+ // Use default SDIS which is 32mb of in-memory size
+ return new SynchronousDiskIntStack(metaDir, name);
+ }
}
+ // If the disk graph as a whole fits into memory, do not use a
+ // disk-backed SynchronousDiskIntStack.
+ return new MemIntStack(metaDir, name);
+ } catch (final OutOfMemoryError oom) {
+ System.gc();
+ // If the allocation above failed, be more conservative. If it fails to
+ // allocate even 16mb, TLC will subsequently terminate with a message about insufficient
+ // memory.
+ final SynchronousDiskIntStack sdis = new SynchronousDiskIntStack(metaDir, name,
+ SynchronousDiskIntStack.BufSize / 2);
+ MP.printWarning(EC.GENERAL,
+ "Liveness checking will be extremely slow because TLC is running low on memory.\n"
+ + "Try allocating more memory to the Java pool (heap) in future TLC runs.");
+ return sdis;
}
- // If the disk graph as a whole fits into memory, do not use a
- // disk-backed SynchronousDiskIntStack.
- return new MemIntStack(metaDir, name);
}
/**
diff --git a/tlatools/src/tlc2/util/SynchronousDiskIntStack.java b/tlatools/src/tlc2/util/SynchronousDiskIntStack.java
index 15c34bfea..b66120433 100644
--- a/tlatools/src/tlc2/util/SynchronousDiskIntStack.java
+++ b/tlatools/src/tlc2/util/SynchronousDiskIntStack.java
@@ -55,7 +55,7 @@ public class SynchronousDiskIntStack implements IntStack {
public SynchronousDiskIntStack(String diskdir, String name, int capacity) {
// Hard-limit capacity to 1gb per page file
- capacity = Math.min(BufSizeMax, Math.max(capacity, BufSize));
+ capacity = Math.min(BufSizeMax, capacity);
this.filePrefix = diskdir + FileUtil.separator + name;
this.bufSize = capacity;
this.buf = new int[capacity];
--
GitLab