All-or-nothing strategy when allocating memory in LiveWorker.

[Refactor][TLC]

tlatools/src/tlc2/tool/liveness/LiveWorker.java

@@ -202,9 +202,18 @@ public class LiveWorker implements Callable<Boolean> {
 		final int slen = this.oos.getCheckState().length;
 		final int alen = this.oos.getCheckAction().length;
 		
+		
+		// Synchronize all LiveWorker instances to consistently read free
+		// memory. This method is only called during initialization of SCC
+		// search, thus synchronization should not cause significant thread
+		// contention. We want a single LW to successfully allocate both
+		// dfsStack *and* comStack.
+		final IntStack dfsStack;
+		final IntStack comStack;
+		synchronized (LiveWorker.class) {
 			// Tarjan's stack
 			// Append thread id to name for unique disk files during concurrent SCC search
-		final IntStack dfsStack = getStack(liveCheck.getMetaDir(), "dfs" + this.id);
+			dfsStack = getStack(liveCheck.getMetaDir(), "dfs" + this.id);
 			
 			// comStack is only being added to during the deep first search. It is passed
 			// to the checkComponent method while in DFS though. Note that the nodes pushed
@@ -213,7 +222,8 @@ public class LiveWorker implements Callable<Boolean> {
 			//
 			// See tlc2.tool.liveness.LiveWorker.DetailedFormatter.toString(MemIntStack)
 			// which is useful during debugging.
-		final IntStack comStack = getStack(liveCheck.getMetaDir(), "com" + this.id);
+			comStack = getStack(liveCheck.getMetaDir(), "com" + this.id);
+		}
 
 		// Generate the SCCs and check if they contain a "bad" cycle.
 		while (nodeQueue.size() > 0) {
@@ -462,11 +472,6 @@ public class LiveWorker implements Callable<Boolean> {
 	}
 
 	private IntStack getStack(final String metaDir, final String name) throws IOException {
-		// Synchronize all LiveWorker instances to consistently read free
-		// memory. This method is only called during initialization of SCC
-		// search, thus synchronization should not cause significant thread
-		// contention.
-		synchronized (LiveWorker.class) {
 		// It is unlikely that the stacks will fit into memory if the
 		// size of the behavior graph is larger relative to the available
 		// memory. Also take the total number of simultaneously running
@@ -491,7 +496,6 @@ public class LiveWorker implements Callable<Boolean> {
 		// disk-backed SynchronousDiskIntStack.
 		return new MemIntStack(metaDir, name);
 	}
-	}
 
 	/**
 	 * For currentPEM, this method checks if the current SCC satisfies its AEs