Skip to content
Permalink
Browse files

Fall back to conservative growth rate if exponential growth causes an

OutOfMemoryError in NodePtrTable.

[Feature][TLC]
  • Loading branch information
lemmy committed Mar 24, 2020
1 parent 0696d2e commit e2f99e6c4f7dc1c0bdd298c9f864fcf9416cac30
Showing with 17 additions and 3 deletions.
  1. +17 −3 tlatools/src/tlc2/tool/liveness/NodePtrTable.java
@@ -111,8 +111,12 @@ public void resetElems() {

/* Double the table when the table is full by the threshhold. */
private final void grow() {
final int newLength = 2 * this.length + 1;
grow(newLength);
}

private final void grow(final int newLength) {
try {
final int newLength = 2 * this.length + 1;
final long[] oldKeys = this.keys;
final long[] oldElems = this.elems;
this.keys = new long[newLength];
@@ -146,8 +150,18 @@ private final void grow() {
// Handle OOM error locally because grow is on the code path of safety checking
// (LiveCheck#addInit/addNext...).
System.gc();
MP.printError(EC.SYSTEM_OUT_OF_MEMORY, t);
System.exit(1);
if (newLength <= this.length + 1) {
MP.printError(EC.SYSTEM_OUT_OF_MEMORY, t);
System.exit(1);
}
try {
// It doesn't buy us much, but - as fallback - do not grow capacity
// exponentially.
grow(newLength - (newLength >> 2));
} catch (OutOfMemoryError inner) {
MP.printError(EC.SYSTEM_OUT_OF_MEMORY, inner);
System.exit(1);
}
}
}

0 comments on commit e2f99e6

Please sign in to comment.
You can’t perform that action at this time.