From 4111431a169b96d0b2eb850fd6fb4416cf5af4ff Mon Sep 17 00:00:00 2001
From: Calvin Loncaric <marvinx03@gmail.com>
Date: Thu, 9 Apr 2020 21:41:04 -0700
Subject: [PATCH] Allow "-workers auto" to automatically detect available
parallelism
[Feature][TLC][Changelog]
---
tlatools/org.lamport.tlatools/src/tlc2/TLC.java | 12 ++++++++----
1 file changed, 8 insertions(+), 4 deletions(-)
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/TLC.java b/tlatools/org.lamport.tlatools/src/tlc2/TLC.java
index b4d1dfb6c..2e3e38ada 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/TLC.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/TLC.java
@@ -747,7 +747,9 @@ public class TLC {
{
try
{
- int num = Integer.parseInt(args[index]);
+ int num = args[index].strip().toLowerCase().equals("auto")
+ ? Runtime.getRuntime().availableProcessors()
+ : Integer.parseInt(args[index]);
if (num < 1)
{
printErrorMsg("Error: at least one worker required.");
@@ -757,12 +759,12 @@ public class TLC {
index++;
} catch (Exception e)
{
- printErrorMsg("Error: worker number required. But encountered " + args[index]);
+ printErrorMsg("Error: worker number or 'auto' required. But encountered " + args[index]);
return false;
}
} else
{
- printErrorMsg("Error: expect an integer for -workers option.");
+ printErrorMsg("Error: expect an integer or 'auto' for -workers option.");
return false;
}
} else if (args[index].equals("-dfid"))
@@ -1438,7 +1440,9 @@ public class TLC {
"an absolute path to a file in which to log user output (for\n"
+ "example, that which is produced by Print)", true));
sharedArguments.add(new UsageGenerator.Argument("-workers", "num",
- "the number of TLC worker threads; defaults to 1", true));
+ "the number of TLC worker threads; defaults to 1. Use 'auto'\n"
+ + "to automatically select the number of threads based on the\n"
+ + "number of available cores.", true));
sharedArguments.add(new UsageGenerator.Argument("SPEC", null));
--
GitLab