Skip to content

Commit

Permalink
Cache result of file IO to speed up TLC running in debugger.
Browse files Browse the repository at this point in the history
[Feature][TLC][Debugger]
  • Loading branch information
lemmy committed Mar 9, 2021
1 parent fe7cb8b commit 6b2a79b
Showing 1 changed file with 7 additions and 3 deletions.
10 changes: 7 additions & 3 deletions tlatools/org.lamport.tlatools/src/tlc2/debug/TLCStackFrame.java
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,6 @@
******************************************************************************/
package tlc2.debug;

import java.io.File;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
Expand All @@ -49,6 +48,9 @@

class TLCStackFrame extends StackFrame {

// Not thread-safe because TLCDebugger is assumed to take care of synchronization!
private static final Map<SemanticNode, String> PATH_CACHE = new HashMap<>();

public static final String SCOPE = "Context";

// It would be easier to use hashCode instead of passing a random generator
Expand Down Expand Up @@ -90,8 +92,10 @@ public TLCStackFrame(SemanticNode node, Context ctxt, final Tool tool) {

final Source source = new Source();
source.setName(node.getLocation().source());
final File moduleFile = tool.getResolver().resolve(node.getTreeNode().getFilename(), true);
source.setPath(moduleFile.getAbsolutePath().toString());
// resolve(..) triggers a file-system round-trip (IO), which is obviously too
// expensive!!! Thus, cache the result.
source.setPath(PATH_CACHE.computeIfAbsent(node,
n -> tool.getResolver().resolve(n.getTreeNode().getFilename(), true).getAbsolutePath().toString()));
setSource(source);

this.stackId = rnd.nextInt(Integer.MAX_VALUE - 1) + 1;
Expand Down

0 comments on commit 6b2a79b

Please sign in to comment.