Fix unit test error reporting and support -Dthreads=N parameter (#903)

Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Apr 11, 2024 · f135b2c · f135b2c
1 parent 8fa1f19
commit f135b2c
Show file tree

Hide file tree

Showing 4 changed files with 49 additions and 28 deletions.
diff --git a/.github/scripts/parse-unit-test-output.py b/.github/scripts/parse-unit-test-output.py
@@ -83,8 +83,16 @@ def parallel_match_to_report(match):
     ]
 
 reports = sorted(reports, key=lambda report: report.runtime, reverse=True)
-failures = [report.name for report in reports if report.failure_count > 0]
-duplicates = [k for k, v in Counter(report.name for report in reports).items() if v > 1]
+failures = [
+    report.name
+    for report in reports
+    if report.failure_count > 0 or report.error_count > 0
+]
+duplicates = [
+    test_name
+    for test_name, run_count in Counter(report.name for report in reports).items()
+    if run_count > 1
+]
 
 print(f'Test count: {len(reports)}')
 print(f'Failure count: {len(failures)}')
@@ -113,6 +121,8 @@ def node_text(node):
         print(f'TEST NAME: {test_case.attrib["name"]}')
         for failure in test_case.iter('failure'):
             print(f'FAILURE:\n{node_text(failure)}')
+        for error in test_case.iter('error'):
+            print(f'ERROR:\n{node_text(error)}')
     for output in tree.iter('system-out'):
         print(f'SYSTEM.OUT:\n{node_text(output)}')
     for err_output in tree.iter('system-err'):

diff --git a/.github/workflows/pr.yml b/.github/workflows/pr.yml
@@ -23,17 +23,23 @@ jobs:
         git status
         diff_count=$(git status --porcelain=v1 2>/dev/null | wc -l)
         exit $diff_count
-    - name: Build & Test Tools
+    - name: Build tools and unit tests
+      run: ant -f tlatools/org.lamport.tlatools/customBuild.xml compile compile-test dist
+    - name: Run unit tests
       run: |
-        set -o pipefail
-        ant -f tlatools/org.lamport.tlatools/customBuild.xml compile compile-test test dist 2>&1 | tee test-output.txt
-        echo "export BUILD_UT_EXIT_CODE=$?" >> $GITHUB_ENV
-    - name: Summarize Unit Tests
+        set +e # Ensure UT failure does not immediately terminate CI
+        set -o pipefail # Ensure UT failure is propagated through tee command
+        ant -f tlatools/org.lamport.tlatools/customBuild.xml test 2>&1 | tee test-output.txt
+        ut_exit_code=$?
+        echo "Unit test exit code: $ut_exit_code"
+        echo "UT_EXIT_CODE=$ut_exit_code" >> $GITHUB_ENV # Export UT result to CI env var
+    - name: Summarize unit tests
       run: |
+        echo "Unit test exit code: $UT_EXIT_CODE"
         python .github/scripts/parse-unit-test-output.py        \
           test-output.txt                                       \
           tlatools/org.lamport.tlatools/target/surefire-reports
-        exit $BUILD_UT_EXIT_CODE
+        exit $UT_EXIT_CODE
     - name: Clone tlaplus/CommunityModules
       uses: actions/checkout@v4
       with:

diff --git a/tlatools/org.lamport.tlatools/customBuild.xml b/tlatools/org.lamport.tlatools/customBuild.xml
@@ -393,16 +393,14 @@
 			</patternset>
 		</unzip>
 
-
-
 		<!-- create a JAR file for the users -->
 		<mkdir dir="${dist.dir}" />
 		<jar destfile="${dist.file}" level="9">
 			<fileset dir="${class.dir}" includes="**/*" excludes="
 					**/*.jpg,
 					README.txt,
-				    heapstats.jfc,
-				    jpf.properties,
+					heapstats.jfc,
+					jpf.properties,
 					tlc2/tool/fp/*.tla,
 					tlc2/value/*.tla,
 					pcal/*.tla,
@@ -435,7 +433,7 @@
 				<attribute name="Implementation-Version" value="${version} ${TODAY}" />
 				<attribute name="Implementation-Vendor" value="Microsoft Corp." />
 				<!-- The jar files contains many main classes (SANY, TEX, pcal, ...) --> 
-                <!-- but lets consider TLC the one users primarily use. --> 
+				<!-- but lets consider TLC the one users primarily use. --> 
 				<attribute name="Main-class" value="tlc2.TLC" />
 				<attribute name="Class-Path" value="CommunityModules-deps.jar CommunityModules.jar" />
 				<!-- Git revision -->
@@ -482,8 +480,8 @@
 		</javac>
 		<!-- Include auxilliary files when compiling classes. -->
 		<copy todir="${test.class.dir}">
-		   <fileset dir="${test.dir}" includes="**/*.dot"/>
-		   <fileset dir="${test.dir}" includes="**/*.dump"/>
+			<fileset dir="${test.dir}" includes="**/*.dot"/>
+			<fileset dir="${test.dir}" includes="**/*.dump"/>
 		</copy>		
 		<!-- copy class.dir to path with whitespace -->
 		<!-- this is required by some tests to make sense -->
@@ -494,16 +492,22 @@
 		</copy>
 	</target>
 
-	<!-- Unit tests which due to their nature cannot be run in parallel. -->
-	<target name="sequential-test" unless="test.skip">
+	<!-- Runs all unit tests -->
+	<target name="test" unless="test.skip">
 		<property runtime="runtime"/>
+		<condition property="threadLimit" value="${threads}" else="${runtime.availableProcessors}">
+			<isset property="threads"/>
+		</condition>
+		<echo>Running tests across ${threadLimit} threads</echo>
+		<!-- run junit tests -->
 		<mkdir dir="${test.reports}" />
+		<!-- First run unit tests which due to their nature cannot be run in parallel. -->
 		<junit
 			printsummary="yes"
 			showoutput="no"
 			haltonfailure="${test.halt}"
 			haltonerror="${test.halt}"
-			failureproperty="sequential-test.failed"
+			failureproperty="unit-test.failed"
 			forkmode="perTest"
 			fork="yes"
 			threads="1"
@@ -535,7 +539,7 @@
 			<sysproperty key="basedir" value="${basedir}/"/>
 			<sysproperty key="tlc2.tool.fp.FPSet.impl" value="tlc2.tool.fp.OffHeapDiskFPSet"/>
 			<sysproperty key="util.FileUtil.milliseconds" value="true"/>
-			<sysproperty key="tlc2.tool.distributed.TLCWorker.threadCount" value="${runtime.availableProcessors}"/>
+			<sysproperty key="tlc2.tool.distributed.TLCWorker.threadCount" value="${threadLimit}"/>
 			<!-- Distributed TLC tests must be run sequentially because they bind
 					 exclusively to a port on the system. -->
 			<batchtest fork="yes" todir="${test.reports}">
@@ -547,14 +551,8 @@
 				</fileset>
 			</batchtest>
 		</junit>
-		<fail message="Sequential unit test failures." if="sequential-test.failed" />
-	</target>
 
-	<!-- Executes unit tests in parallel. -->
-	<target name="test" unless="test.skip" depends="sequential-test">
-		<property runtime="runtime"/>
-		<!-- run junit tests -->
-		<mkdir dir="${test.reports}" />
+		<!-- Run rest of unit tests in parallel -->
 		<!-- forkmode used to be "perBatch" on Java 1.8 using the util.IsolatedTestCaseRunner.
 		     This concept broken with Java11 for unknown reasons which is why forkmode has been
 		     changed to perTest to run each test in a separate VM.  This is slower compared to
@@ -567,7 +565,7 @@
 			failureproperty="unit-test.failed"
 			forkmode="perTest"
 			fork="yes"
-			threads="${runtime.availableProcessors}"
+			threads="${threadLimit}"
 		>
 			<!-- enable all assertions -->
 			<jvmarg value="-ea"/>

diff --git a/tlatools/org.lamport.tlatools/test/tlc2/tool/liveness/ModelCheckerTestCase.java b/tlatools/org.lamport.tlatools/test/tlc2/tool/liveness/ModelCheckerTestCase.java
@@ -171,8 +171,15 @@ public void setUp() {
 				args.add("1");
 			}
 
+			// Some tests require a large number of threads to successfully
+			// test their desired property. They request this by overriding
+			// the getNumberOfThreads() method. This can lead to over-
+			// subscribing system cores when running tests in parallel, but
+			// is usually okay because the tests run for only a second or so.
+			// If a test runs for a longer period of time using many threads
+			// then it should be run sequentially instead of in parallel.
 			args.add("-workers");
-			args.add(Integer.toString(getNumberOfThreads()));
+			args.add(Integer.toString(this.getNumberOfThreads()));
 
 			// Never create checkpoints. They distort performance tests and are
 			// of no use anyway.