[Tests] Add performance tests to establish a thread contention baseline

that TLC shows for liveness checking (with and without tableaux). More
precisely the time each TLC worker thread spends in the WAITING and
BLOCKED state must not exceed more than empirically obtained upper bounds.

tlatools/customBuild.xml

@@ -269,14 +269,14 @@
 		</javac>
 		<!-- copy class.dir to path with whitespace -->
 		<!-- this is required by some tests to make sense -->
-		<!-- even throw a non digit in -->
+		<!-- even throw a "+" and whitespace into the mix -->
 		<property name="ws.class.dir" value="TLA+ Tools" />
 		<copy todir="${ws.class.dir}">
 			<fileset dir="${class.dir}" />
 		</copy>
 		<!-- run junit tests on tlatools.jar -->
 		<mkdir dir="${test.reports}/onJarLong" />
-		<junit printsummary="yes" haltonfailure="no" haltonerror="no" maxmemory="1024m">
+		<junit printsummary="yes" haltonfailure="no" haltonerror="no" maxmemory="4096m" forkmode="perTest" fork="yes">
 			<classpath refid="project.classpath" />
 			<classpath>
 				<pathelement location="lib/junit-4.8.2.jar" />
@@ -288,6 +288,16 @@
 
 			<batchtest fork="yes" todir="${test.reports}/onJarLong">
 				<fileset dir="${test.dir}-long">
+					<exclude name="**/MultiThreadedSpecTest.java"/>
+					
+					<!-- The following tests take way too long (hours) -->
+					<!-- Reactivate when you start working on the fingerprint sets -->
+					<exclude name="**/DiskFPSetTest.java"/>
+					<exclude name="**/FPSetTest.java"/>
+					<exclude name="**/MSBDiskFPSetTest.java"/>
+					<exclude name="**/OffHeapDiskFPSetTest.java"/>
+					<exclude name="**/DiskStateQueueTest.java"/>
+					
 					<include name="**/*Test*.java" />
 				</fileset>
 			</batchtest>

tlatools/src/tlc2/tool/AbstractChecker.java

@@ -29,6 +29,8 @@ import util.FilenameToStream;
  */
 public abstract class AbstractChecker implements Cancelable
 {
+    public static final String NEXT_LIVECHECK = AbstractChecker.class.getName() + ".nextLiveCheck";
+
 	protected static final boolean LIVENESS_STATS = Boolean.getBoolean(Liveness.class.getPackage().getName() + ".statistics");
 	
     // SZ Mar 9, 2009: static modifier removed
@@ -86,7 +88,13 @@ public abstract class AbstractChecker implements Cancelable
         // performed.  This value of 1000 sounds low, but since the value is
         // doubled after each check up to a maximum of 640K (a number embedded
         // in several places in the code), it probably doesn't much matter.
-        this.nextLiveCheck = 1000;
+        //
+		// The default of 1000 states can be overridden with a system property.
+		// This is e.g. used by unit tests to prevent periodic liveness checking
+		// (setting nextLiveCheck to Long.MAX_VALUE) and force TLC to check
+		// liveness only at the end of model checking. This gives predictable
+		// results required by unit tests.
+        this.nextLiveCheck = Long.getLong(NEXT_LIVECHECK, 1000);
         this.numOfGenStates = new AtomicLong(0);
         this.errState = null;
         this.predErrState = null;

tlatools/src/tlc2/tool/Worker.java

@@ -5,6 +5,9 @@
 
 package tlc2.tool;
 
+import java.util.HashSet;
+import java.util.Set;
+
 import tlc2.output.EC;
 import tlc2.output.MP;
 import tlc2.tool.queue.IStateQueue;
@@ -13,11 +16,17 @@ import tlc2.util.ObjLongTable;
 import tlc2.value.Value;
 
 public class Worker extends IdThread implements IWorker {
+	
+	private static final Set<ThreadListener> THREAD_LISTENERS = new HashSet<ThreadListener>();
+	
+	public static void addThreadListener(ThreadListener listener) {
+		THREAD_LISTENERS.add(listener);
+	}
+	
 	/**
-   * Multi-threading helps only when running on multiprocessors. TLC
-   * can pretty much eat up all the cycles of a processor running
-   * single threaded.  We expect to get linear speedup with respect
-   * to the number of processors.
+	 * Multi-threading helps only when running on multiprocessors. TLC can
+	 * pretty much eat up all the cycles of a processor running single threaded.
+	 * We expect to get linear speedup with respect to the number of processors.
 	 */
 	private ModelChecker tlc;
 	private IStateQueue squeue;
@@ -60,6 +69,7 @@ public class Worker extends IdThread implements IWorker {
    * updates the state set and state queue.
 	 */
 	public final void run() {
+		final long startTime = System.currentTimeMillis();
 		TLCState curState = null;
 		try {
 			while (true) {
@@ -72,21 +82,34 @@ public class Worker extends IdThread implements IWorker {
 					this.squeue.finishAll();
 					return;
 				}
-	if (this.tlc.doNext(curState, this.astCounts)) return;
-				}
+				if (this.tlc.doNext(curState, this.astCounts))
+					return;
 			}
-    catch (Throwable e) {
+		} catch (Throwable e) {
 			// Something bad happened. Quit ...
 			// Assert.printStack(e);
 			synchronized (this.tlc) {
 				if (this.tlc.setErrState(curState, null, true)) {
-	    MP.printError(EC.GENERAL, e);  // LL changed call 7 April 2012
+					MP.printError(EC.GENERAL, e); // LL changed call 7 April
+													// 2012
 				}
 				this.squeue.finishAll();
 				this.tlc.notify();
 			}
 			return;
+		} finally {
+			for (ThreadListener listener : THREAD_LISTENERS) {
+				listener.terminated(this, System.currentTimeMillis() - startTime);
+			}
 		}
 	}
 	
+	/**
+	 * A ThreadListener is notified of when the Worker thread terminates. The
+	 * notification includes the execution time of the thread.
+	 */
+	public static interface ThreadListener {
+
+		void terminated(final Thread thread, final long runningTime);
+	}
 }

tlatools/test-long/tlc2/tool/liveness/MultiThreadedSpecTest.java

+/*******************************************************************************
+ * Copyright (c) 2015 Microsoft Research. All rights reserved. 
+ *
+ * The MIT License (MIT)
+ * 
+ * Permission is hereby granted, free of charge, to any person obtaining a copy 
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is furnished to do
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software. 
+ * 
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ *   Markus Alexander Kuppe - initial API and implementation
+ ******************************************************************************/
+
+package tlc2.tool.liveness;
+
+import java.lang.management.ManagementFactory;
+import java.lang.management.ThreadInfo;
+import java.lang.management.ThreadMXBean;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.concurrent.BrokenBarrierException;
+import java.util.concurrent.CountDownLatch;
+import java.util.concurrent.TimeUnit;
+import java.util.concurrent.TimeoutException;
+
+import tlc2.output.EC;
+import tlc2.tool.AbstractChecker;
+import tlc2.tool.Worker;
+
+/**
+ * This test takes about four minutes with 32 cores on an EC2 cr1.8xlarge instance.
+ * On a Thinkpad T430s it takes eight times as long and uses up 4GB of memory (see customBuild.xml).
+ * 
+ * The purpose of this test is to establish a thread contention baseline that TLC shows for
+ * liveness checking (with and without tableaux). More precisely the time each TLC worker
+ * thread spends in the WAITING and BLOCKED state must not exceed more than waitedRatio and
+ * blockedRatio. The current values for waitedRatio and blockedRatio have been obtained empirically.
+ */
+public abstract class MultiThreadedSpecTest extends ModelCheckerTestCase {
+
+	private final String statesGenerated;
+	private final String distinctStatesGenerated;
+	private final List<PerformanceResult> performanceResults = new ArrayList<PerformanceResult>();
+	private final CountDownLatch latch = new CountDownLatch(getNumberOfThreads());
+	private final double waitedRatio;
+	private final double blockedRatio;
+	
+	public MultiThreadedSpecTest(String spec, String path, String statesGenerated, String distinctStatesGenerated, double blockedRatio, double waitedRatio) {
+		super(spec, path);
+		this.statesGenerated = statesGenerated;
+		this.distinctStatesGenerated = distinctStatesGenerated;
+		this.blockedRatio = blockedRatio;
+		this.waitedRatio = waitedRatio;
+	}
+
+	public MultiThreadedSpecTest(String spec, String path, String[] extraArguments, String statesGenerated, String distinctStatesGenerated, double blockedRatio, double waitedRatio) {
+		super(spec, path, extraArguments);
+		this.statesGenerated = statesGenerated;
+		this.distinctStatesGenerated = distinctStatesGenerated;
+		this.blockedRatio = blockedRatio;
+		this.waitedRatio = waitedRatio;
+	}
+
+	public void testSpec() throws BrokenBarrierException, InterruptedException, TimeoutException {
+		// ModelChecker has finished and generated the expected amount of states
+		assertTrue(recorder.recorded(EC.TLC_FINISHED));
+		assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, statesGenerated, distinctStatesGenerated));
+		
+		// Assert it has found the temporal violation and also a counter example
+		assertTrue(recorder.recorded(EC.TLC_TEMPORAL_PROPERTY_VIOLATED));
+		assertTrue(recorder.recorded(EC.TLC_COUNTER_EXAMPLE));
+		
+		// Assert the error trace
+		assertTrue(recorder.recorded(EC.TLC_STATE_PRINT3));
+		
+		// Allow TLC worker threads to take 10 seconds to shutdown and report
+		// their PerformanceResults to us. TLC's master thread has no reason to
+		// wait for the final termination of all worker threads once it has
+		// received the signal from one of them. After all the VM itself is
+		// going to shutdown after TLC is done printing results.
+		latch.await(10, TimeUnit.SECONDS);
+
+		// Except as many results as we have started worker threads.
+		assertEquals(getNumberOfThreads(), performanceResults.size());
+		
+		// None of the workers threads should have been blocked or waiting for
+		// more than 25%
+		for (PerformanceResult result : performanceResults) {
+			assertTrue(String.format("Blocked(%s): %.3f", result.getThreadName(), result.getBlockedRatio()),
+					result.getBlockedRatio() < blockedRatio);
+			assertTrue(String.format("Waiting(%s): %.3f", result.getThreadName(), result.getWaitedRatio()),
+					result.getWaitedRatio() < waitedRatio);
+		}
+	}
+	
+	public void setUp() {
+		// Set the number of states before TLC (periodically) checks liveness to
+		// the largest possible value. This essentially stops TLC for checking
+		// liveness during model checking and delays it until the end when one
+		// final liveness check is run. We only then get deterministic behavior
+		// needed by this test to e.g. check the number of states generated...
+		System.setProperty(AbstractChecker.NEXT_LIVECHECK, Long.toString(Long.MAX_VALUE));
+		
+		final ThreadMXBean threadBean = ManagementFactory.getThreadMXBean();
+		// Enable contention thread statistics to have the JVM measure
+		// BlockedTime and WaitedTime.
+		threadBean.setThreadContentionMonitoringEnabled(true);
+
+		// Register a listener hot for the termination of the TLC worker
+		// threads. 
+		// Using ThreadMXBean to lookup all threads after TLC has
+		// finished has the potential that the JVM deleted the worker threads
+		// before this test gets a chance to collect statistics.
+		Worker.addThreadListener(new Worker.ThreadListener() {
+			public synchronized void terminated(final Thread thread, final long runningTime) {
+				final ThreadInfo threadInfo = threadBean.getThreadInfo(thread.getId());
+				double d = threadInfo.getBlockedTime() / (runningTime * 1.0d);
+				double d2 = threadInfo.getWaitedTime() / (runningTime * 1.0d);
+				performanceResults.add(new PerformanceResult(thread.getName(), d, d2));
+				latch.countDown();
+			}
+		});
+		
+		super.setUp();
+	}
+	
+	protected int getNumberOfThreads() {
+		// Run this test with as many threads possible to hopefully spot concurrency issues.
+		return Runtime.getRuntime().availableProcessors();
+	}
+	
+	private static class PerformanceResult {
+
+		private final double blockedRatio;
+		private final double waitedRatio;
+		private final String threadName;
+
+		public PerformanceResult(String threadName, double blockedRatio, double waitedRatio) {
+			this.threadName = threadName;
+			this.blockedRatio = blockedRatio;
+			this.waitedRatio = waitedRatio;
+		}
+
+		public double getWaitedRatio() {
+			return waitedRatio;
+		}
+
+		public double getBlockedRatio() {
+			return blockedRatio;
+		}
+		
+		public String getThreadName() {
+			return threadName;
+		}
+	}
+}

tlatools/test-long/tlc2/tool/liveness/NoTableauSpecTest.java

@@ -23,37 +23,11 @@
  * Contributors:
  *   Markus Alexander Kuppe - initial API and implementation
  ******************************************************************************/
-
 package tlc2.tool.liveness;
 
-import tlc2.output.EC;
-
-/**
- * This takes about four minutes with 32 cores on an EC2 cr1.8xlarge instance.
- * On a Thinkpad T430s it takes eight times as long.
- */
-public class NoTableauSpecTest extends ModelCheckerTestCase {
+public class NoTableauSpecTest extends MultiThreadedSpecTest {
 
 	public NoTableauSpecTest() {
-		super("MC", "VoteProof");
-	}
-	
-	public void testSpec() {
-		// ModelChecker has finished and generated the expected amount of states
-		assertTrue(recorder.recorded(EC.TLC_FINISHED));
-		assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "137297983", "693930"));
-		
-		// Assert it has found the temporal violation and also a counter example
-		assertTrue(recorder.recorded(EC.TLC_TEMPORAL_PROPERTY_VIOLATED));
-		assertTrue(recorder.recorded(EC.TLC_COUNTER_EXAMPLE));
-		
-		// Assert the error trace
-		assertTrue(recorder.recorded(EC.TLC_STATE_PRINT3));
-	}
-
-	protected String getNumberOfThreads() {
-		// Run this test with as many threads possible to hopefully spot concurrency issues.
-		int availableProcessors = Runtime.getRuntime().availableProcessors();
-		return Integer.toString(availableProcessors);
+		super("MC", "VoteProof", "137297983", "693930", 0.25d, 0.25d);
 	}
 }

tlatools/test-long/tlc2/tool/liveness/TableauSpecTest.java

+/*******************************************************************************
+ * Copyright (c) 2015 Microsoft Research. All rights reserved. 
+ *
+ * The MIT License (MIT)
+ * 
+ * Permission is hereby granted, free of charge, to any person obtaining a copy 
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is furnished to do
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software. 
+ * 
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ *   Markus Alexander Kuppe - initial API and implementation
+ ******************************************************************************/
+package tlc2.tool.liveness;
+
+public class TableauSpecTest extends MultiThreadedSpecTest {
+
+	public TableauSpecTest() {
+		super("MC", "EWD840", new String[] {"-maxSetSize", "9000000"}, "540765192", "10487806", 0.3d, 0.3d);
+	}
+}

tlatools/test-model/EWD840/EWD840.tla

+------------------------------- MODULE EWD840 -------------------------------
+EXTENDS Naturals
+
+CONSTANT N
+ASSUME NAssumption == N \in Nat \ {0}
+
+VARIABLES active, color, tpos, tcolor
+Nodes == 0 .. N-1
+Color == {"white", "black"}
+
+TypeOK ==
+  /\ active \in [Nodes -> BOOLEAN]
+  /\ color \in [Nodes -> Color]
+  /\ tpos \in Nodes
+  /\ tcolor \in Color
+
+(* Initially the token is at node 0, and it is black. There
+   are no constraints on the status and color of the nodes. *)
+Init ==
+  /\ active \in [Nodes -> BOOLEAN]
+  /\ color \in [Nodes -> Color]
+  /\ tpos = 0
+  /\ tcolor = "black"
+
+InitiateProbe ==
+  /\ tpos = 0
+  /\ tcolor = "black" \/ color[0] = "black"
+  /\ tpos' = N-1
+  /\ tcolor' = "white"
+  /\ color' = [color EXCEPT ![0] = "white"]
+  /\ UNCHANGED <<active>>
+
+PassToken(i) == 
+  /\ tpos = i
+  /\ ~ active[i]
+        \/ color[i] = "black"
+        \/ tcolor = "black"
+  /\ tpos' = i-1
+  /\ tcolor' = IF color[i] = "black" THEN "black" ELSE tcolor
+  /\ color' = [color EXCEPT ![i] = "white"]
+  /\ UNCHANGED <<active>>
+
+SendMsg(i) ==
+  /\ active[i]
+  /\ \E j \in Nodes \ {i} :
+        /\ active' = [active EXCEPT ![j] = TRUE]
+        /\ color' = [color EXCEPT ![i] = IF j>i THEN "black" ELSE @]
+  /\ UNCHANGED <<tpos, tcolor>>
+
+Deactivate(i) ==
+  /\ active[i]
+  /\ active' = [active EXCEPT ![i] = FALSE]
+  /\ UNCHANGED <<color, tpos, tcolor>>
+
+Next ==
+  \/ InitiateProbe
+  \/ \E i \in Nodes \ {0} : PassToken(i)
+  \/ \E i \in Nodes : SendMsg(i) \/ Deactivate(i)
+
+System ==
+  \/ InitiateProbe
+  \/ \E i \in Nodes \ {0} : PassToken(i)
+
+vars == <<active, color, tpos, tcolor>>
+
+Fairness == WF_vars(System)
+
+Spec == Init /\ [][Next]_vars (*/\ Fairness*)
+
+LInv == [][Next]_vars => WF_vars(System)
+
+-----------------------------------------------------------------------------
+
+NeverBlack == \A i \in Nodes : color[i] # "black"
+
+NeverChangeColor == [][ \A i \in Nodes : UNCHANGED color[i] ]_vars
+
+terminationDetected ==
+  /\ tpos = 0 /\ tcolor = "white"
+  /\ color[0] = "white" /\ ~ active[0]
+  /\ color[1] = "white"
+
+TerminationDetection ==
+  terminationDetected => \A i \in Nodes : ~ active[i]
+
+Liveness ==
+  /\ (\A i \in Nodes : ~ active[i]) ~> terminationDetected
+
+AllNodesTerminateIfNoMessages ==
+  <>[][~ \E i \in Nodes : SendMsg(i)]_vars
+  => <>(\A i \in Nodes : ~ active[i])
+
+Inv == 
+  \/ P0:: \A i \in Nodes : tpos < i => ~ active[i]
+  \/ P1:: \E j \in 0 .. tpos : color[j] = "black"
+  \/ P2:: tcolor = "black"
+
+=============================================================================

tlatools/test-model/EWD840/MC.cfg

+\* CONSTANT definitions
+CONSTANT
+N <- const_143073460396411000
+\* SPECIFICATION definition
+SPECIFICATION
+spec_143073460397412000
+\* PROPERTY definition
+PROPERTY
+prop_143073460398413000
+\* Generated on Mon May 04 12:16:43 CEST 2015
\ No newline at end of file

tlatools/test-model/EWD840/MC.tla

+---- MODULE MC ----
+EXTENDS EWD840, TLC
+
+\* CONSTANT definitions @modelParameterConstants:0N
+const_143073460396411000 == 
+10
+----
+
+\* SPECIFICATION definition @modelBehaviorSpec:0
+spec_143073460397412000 ==
+Spec
+----
+\* PROPERTY definition @modelCorrectnessProperties:0
+prop_143073460398413000 ==
+Liveness
+----
+=============================================================================
+\* Modification History
+\* Created Mon May 04 12:16:43 CEST 2015 by markus

tlatools/test/tlc2/tool/liveness/ModelCheckerTestCase.java

@@ -23,7 +23,6 @@
  * Contributors:
  *   Markus Alexander Kuppe - initial API and implementation
  ******************************************************************************/
-
 package tlc2.tool.liveness;
 
 import java.io.File;
@@ -72,15 +71,27 @@ public abstract class ModelCheckerTestCase extends TestCase {
 			final TLC tlc = new TLC();
 			// * We want *no* deadlock checking to find the violation of the
 			// temporal formula
-			// * We use a single worker to simplify debugging by taking out
-			// threading
+			// * We use (unless overridden) a single worker to simplify
+			// debugging by taking out threading
 			// * MC is the name of the TLA+ specification to be checked (the file
 			// is placed in TEST_MODEL
-			final List<String> args = new ArrayList<String>(4);
+			final List<String> args = new ArrayList<String>(6);
+			
+			// *Don't* check for deadlocks. All tests are interested in liveness
+			// checks which are shielded away by deadlock checking. TLC finds a
+			// deadlock (if it exists) before it finds most liveness violations.
 			args.add("-deadlock");
+			
 			args.add("-workers");
-			args.add(getNumberOfThreads());
+			args.add(Integer.toString(getNumberOfThreads()));
+			
+			// Never create checkpoints. They distort performance tests and are
+			// of no use anyway.
+			args.add("-checkpoint");
+			args.add("0");
+
 			args.addAll(Arrays.asList(extraArguments));
+			
 			args.add(spec);
 			tlc.handleParameters(args.toArray(new String[args.size()]));
 			
@@ -88,11 +99,11 @@ public abstract class ModelCheckerTestCase extends TestCase {
 			tlc.process();
 			
 		} catch (Exception e) {
-			fail();
+			fail(e.getMessage());
 		}
 	}
 
-	protected String getNumberOfThreads() {
-		return "1";
+	protected int getNumberOfThreads() {
+		return 1;
 	}
 }