Add sequential unit test target

Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Apr 2, 2024 · 24b651f · 24b651f
1 parent 2156654
commit 24b651f
Show file tree

Hide file tree

Showing 2 changed files with 65 additions and 22 deletions.
diff --git a/.github/scripts/parse-unit-test-output.py b/.github/scripts/parse-unit-test-output.py
@@ -55,15 +55,19 @@ def 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]
 
 print(f'Test count: {len(reports)}')
+print(f'Failure count: {len(failures)}')
+print('Longest-running tests:')
+for report in reports[slice(20)]:
+    print(f'{report.runtime:5.1f} sec | {report.name}')
 
 def node_text(node):
     text = node.text
     return text.strip() if text is not None else None
 
-print('Failures:\n')
-failures = [report.name for report in reports if report.failure_count > 0]
+print('\nFailures:\n')
 for test_name in failures:
     print(f'TEST CLASS: {test_name}')
     tree = ET.parse(f'{sys.argv[2]}/TEST-{test_name}.xml')
@@ -78,7 +82,3 @@ def node_text(node):
         print(f'SYSTEM.ERR:\n{node_text(err_output)}')
     print()
 
-print('Longest-running tests:')
-for report in reports[slice(20)]:
-    print(f'{report.runtime:5.1f} sec | {report.name}')
-
diff --git a/tlatools/org.lamport.tlatools/customBuild.xml b/tlatools/org.lamport.tlatools/customBuild.xml
@@ -461,16 +461,68 @@
 		</copy>
 	</target>
 
-	<!-- Executes accompanying unit tests -->
-	<target name="test" unless="test.skip">
+	<!-- Unit tests which due to their nature cannot be run in parallel. -->
+	<target name="sequential-test" unless="test.skip">
+		<property runtime="runtime"/>
+		<mkdir dir="${test.reports}" />
+		<junit
+			printsummary="yes"
+			showoutput="no"
+			haltonfailure="${test.halt}"
+			haltonerror="${test.halt}"
+			failureproperty="sequential-test.failed"
+			forkmode="perTest"
+			fork="yes"
+			threads="1"
+		>
+			<jvmarg value="-ea"/>
+			<jvmarg value="-XX:MaxDirectMemorySize=512k"/>
+			<jvmarg value="-XX:+UseParallelGC"/>
+			<classpath>
+				<pathelement location="lib/junit-4.12.jar" />
+				<pathelement location="lib/hamcrest-core-1.3.jar" />
+				<pathelement path="${class.dir}" />
+				<pathelement path="${test.class.dir}" />
+				<pathelement path="test-model/" />
+			</classpath>
+			<formatter type="xml" />
+			<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}"/>
+			<!-- Distributed TLC tests must be run sequentially because they bind
+					 exclusively to a port on the system. -->
+			<batchtest fork="yes" todir="${test.reports}">
+				<fileset dir="${test.dir}">
+					<include name="tlc2/tool/distributed/**/*Test*.java" />
+					<!-- These fail for some reason. -->
+					<exclude name="**/DistributedTLCTestCase.java" />
+					<exclude name="**/TLCServerTestCase.java" />
+				</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}" />
 		<!-- 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
 		     running all tests in a single VM. -->
-		<junit printsummary="yes" haltonfailure="${test.halt}" showoutput="no" haltonerror="${test.halt}"  forkmode="perTest" fork="yes" threads="${runtime.availableProcessors}">
+		<junit
+			printsummary="yes"
+			showoutput="no"
+			haltonfailure="${test.halt}"
+			haltonerror="${test.halt}"
+			failureproperty="unit-test.failed"
+			forkmode="perTest"
+			fork="yes"
+			threads="${runtime.availableProcessors}"
+		>
 			<!-- enable all assertions -->
 			<jvmarg value="-ea"/>
 			<jvmarg value="-XX:MaxDirectMemorySize=512k"/>
@@ -506,7 +558,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="4"/>
+			<sysproperty key="tlc2.tool.distributed.TLCWorker.threadCount" value="1"/>
 			<!-- The tests below can be tricked into running in a single VM by fiddling with the classloader 
 			     to reload and thus initialize all classes for each tests. -->
 			<batchtest fork="yes" todir="${test.reports}">
@@ -523,6 +575,8 @@
 					<exclude name="tlc2/tool/UserModuleOverrideTest.java" />
 					<exclude name="tlc2/tool/UserModuleOverrideFromJarTest.java" />
 					<exclude name="tlc2/tool/UserModuleOverrideAnnotationTest.java" />
+					<!-- Bind to a port on the system so cannot be run in parallel. -->
+					<exclude name="tlc2/tool/distributed/**/*Test*.java" />
 
 					<exclude name="**/PCalTest.java" />
 					<exclude name="**/SANYTest.java" />
@@ -536,8 +590,6 @@
 					<exclude name="**/TraceExpressionSpecSafetyTest.java" />
 					<exclude name="**/SuiteTestCase.java" />
 					<exclude name="**/SuiteETestCase.java" />
-					<exclude name="**/DistributedTLCTestCase.java" />
-					<exclude name="**/TLCServerTestCase.java" />
 					<exclude name="**/SuccessfulSimulationTestCase.java" />
 					<exclude name="**/AbstractExampleTestCase.java" />
 					<exclude name="**/AbstractCoverageTest.java" />
@@ -589,16 +641,6 @@
 					<include name="tlc2/tool/UserModuleOverrideTest.java" />
 				</fileset>
 			</batchtest>
-			<batchtest fork="yes" todir="${test.reports}">
-				<fileset dir="${test.dir}">
-					<include name="tlc2/tool/distributed/TLCSetTest.java" />
-				</fileset>
-			</batchtest>
-			<batchtest fork="yes" todir="${test.reports}">
-				<fileset dir="${test.dir}">
-					<include name="tlc2/tool/distributed/DistributedDoInitFunctorEvalExceptionTest.java" />
-				</fileset>
-			</batchtest>
 			<batchtest fork="yes" todir="${test.reports}">
 				<fileset dir="${test.dir}">
 					<include name="tlc2/TLCTest.java"/>
@@ -609,6 +651,7 @@
 
 		<!-- remove copied class.dir -->
 		<delete dir="${ws.class.dir}" deleteonexit="true"/>
+		<fail message="Unit test failures." if="unit-test.failed" />
 	</target>
 
 	<!-- Executes a given set of unit test. -->